Smtlib goal annotation

[joe-hauns]

Allows to parse :goal annotations in SMTLIB for goal oriented proof search strategies. Parsing them can be disabled using an option and is enabled by default.

They can be used like this: (assert (! <formula> :goal <goal-name>))

This is similar to assert-not, but is SMT-LIB standard conform which means that e.g. z3 will still be able to correctly parse problems with these annotations ignoring them.

[mezpusz]

I don't want to nitpick but wouldn't it be less code if you just branched based on res._isGoal here and also set _isGoal directly without mkGoal()?

[joe-hauns]

Yeah true.. I didn't realize that res._isGoal is public. I kind of assume that everything starting with _ is private in vampire, so i created mkGoal() to access it. Feels still a bit more consistent to me in terms of coding style, but I don't care much and can also remove it.

[mezpusz]

The please change it to isGoal if you feel like it, otherwise I'm also okay with the current code.

[MichaelRawson]

Sorry I got to this late, @joe-hauns - I can still review if it would be useful. Agree with @mezpusz 's comment but otherwise looks fine to me, good idea! Maybe we could even push for SMT-LIB standardisation (if it isn't already) as it's eminently useful and not too aggressive. Did you mean to bring in the divisibility stuff?

[quickbeam123]

By the way, from a recent coversation with Martin Desharnais-Schäfer:

Sledgehammer already encodes the information about the conjecture in the
axiom name. For example, the following problem contains one (negated)
conjecture (i.e., conjecture0) and two assumptions (i.e., a1 and a2):

(declare-datatypes ((Nat$ 0)) (((zero$) (suc$ (pred$ Nat$)))))
(declare-fun f$ (Nat$) Nat$)
(declare-fun n$ () Nat$)
(assert (! (not (= (f$ n$) n$)) :named conjecture0))
(assert (! (forall ((?v0 Nat$)) (= (f$ (suc$ ?v0)) (suc$ (f$ ?v0))))
:named a1))
(assert (! (= (f$ zero$) zero$) :named a2))

Just mentioning that this is something we might also want to support in the future. Unless we convince sledgehammer to add :goal for us ...

[joe-hauns]

Sorry I got to this late, @joe-hauns - I can still review if it would be useful. Agree with @mezpusz 's comment but otherwise looks fine to me, good idea! Maybe we could even push for SMT-LIB standardisation (if it isn't already) as it's eminently useful and not too aggressive. Did you mean to bring in the divisibility stuff?

Ah right, no the divisibility stuff slipped in because of merging as I was using the branch using both the divisibility fix (from the other PR) and the goal annotation.
Maybe we want to first merge the divisibilty fix, and then this one, then I don't have to revert and merge again...? :)

[joe-hauns]

By the way, from a recent coversation with Martin Desharnais-Schäfer:

Sledgehammer already encodes the information about the conjecture in the axiom name. For example, the following problem contains one (negated) conjecture (i.e., conjecture0) and two assumptions (i.e., a1 and a2):

(declare-datatypes ((Nat$ 0)) (((zero$) (suc$ (pred$ Nat$)))))
(declare-fun f$ (Nat$) Nat$)
(declare-fun n$ () Nat$)
(assert (! (not (= (f$ n$) n$)) :named conjecture0))
(assert (! (forall ((?v0 Nat$)) (= (f$ (suc$ ?v0)) (suc$ (f$ ?v0))))
:named a1))
(assert (! (= (f$ zero$) zero$) :named a2))

Just mentioning that this is something we might also want to support in the future. Unless we convince sledgehammer to add :goal for us ...

Ah interesting. Well I could implement parsing both, or also just go for only parsing their :named conjectureN. I like having the :goal better as it feels a bit more tidy as it separates the semantics from the name, but I don't care too much tbh!

[quickbeam123]

Let's merge the divisibility fix first ... @mezpusz, I think it's an easy one!
Then looking at this one will become easier too :)

Regarding conjecture tagging in smtlib in general, I also like your ":goal" better, but since we are looking at this right now, I would suggest we implement both (and maybe then argue with the sledgehammer people what the standard should be). Could you please extend the code in this direction?