Can't prove "true" in smtlib format?

[Elarnon]

When given the following smtlib file:

$ cat true.smtlib2
(assert true)
(check-sat)

AltErgo 2.4.0 answers:

; File "true.smtlib2", line 2, characters 1-12: I don't know (0.0074) (0 steps) (goal g_1)

unknown

which seems… quite cautious. What is surprising is that when given (what I believe is) the same trivial goal in its native format:

$ cat true.altergo
goal g: true

I get:

File "true.altergo", line 1, characters 9-13: Valid (0.0078) (0 steps) (goal g)

This also reproduces on the online version and looks like a bug? I tried a couple examples but couldn't get AltErgo to answer "Valid" on any files in smtlib format; is this expected?

[Stevendeo]

Hello,

This surprisingly is not a bug. When Alt-Ergo attempts to prove a '.altergo' file, it will attempt to validate the goals. true is true, which is fine. Alt-Ergo actually works on SMT formulas by trying to prove their negation. IKeep in mind that Alt-Ergo will never (for now) answer SAT. It only can return Unsat (which corresponds to Valid) or Unknown. If the negation is true, the formula is Unsat, hence Valid.

Try

$ cat true.smtlib2
(assert false)
(check-sat)

It should return "Valid".

[mattiasdrp]

Hi, I'm not working on this project anymore but here's why this is not an issue:

• Alt-Ergo has been designed to work on quantified formulas (its main goal was to be the SMT solver used by Why3 that focuses on deductive program verification).
• The proof of quantified formulas is undecidable:
  • If you prove that a problem is unsat it's obvious that even by adding new formulas the problem will remain unsat
  • If the current state of your prover is that the problem is not unsat (meaning it's sat or valid), you may add new formulas by instantiating quantified formulas in your problem that make your problem unsat

When proving a formula F in smt-lib2 format, Alt-Ergo will try to prove that the formula F is unsat:

• if F is unsat, no model can satisfy F meaning that F is really unsat
• if F is "sat" we don't know for sure if F is sat because F could be unsat but we didn't instantiate enough to find the unsatisfiability, so "unknown"

When proving a formula F in native format, Alt-Ergo will try to prove that it's negation not F is unsat:

• if not F is unsat, no model can satisfy not F meaning that F is valid
• if not F is "sat" we don't know for sure if F is sat because not F is not valid or F is unsat because not F is valid so Alt-Ergo answers "unknown".

In your example, you're trying to check the satisfiability of true. In smt-lib2, Alt-Ergo will check that true is not unsat, it will succeed but since there's nothing as of now to tell Alt-Ergo that there are no quantifiers, it will just answer "unknown" In native format, Alt-Ergo will check that the negation of true is not unsat but false is inherently unsat so the goal is valid

It should be clear at this point that if a solver answers "sat" when dealing with quantifiers you should be cautious about the result, it may be really sat or it may be sat at this point

Now, if you want to go further:

(declare-fun p () Bool)
(assert (or p (not p)))
(check-sat)

will return:

; File "test.smt2", line 3, characters 1-12: I don't know (0.0015) (0 steps) (goal g_1) unknown

When

logic p:bool
goal g: p or (not p)

will return:

File "test.ae", line 2, characters 9-21: Valid (0.0016) (0 steps) (goal g)

Because the negation of p or (not p) is (not p) and p, this is unsat so the original formula is valid

But if you write

logic p:bool
goal g: p and (not p)

you will get:

File "test.ae", line 2, characters 9-22: I don't know (0.0000) (0 steps) (goal g)

Because the negation of p and (not p) is (not p) or p which is not unsat but AE can't be sure it's valid, sat or not yet proven unsat so the honest answer is unknown.

This is a bit complicated but it has to do with the undecidability of first-order logic with quantifiers.

Summary: if you want to prove that a formula is valid in smt-lib format, check that it's negation is unsat.

Example, if I want to prove that for all x and y, x <= y or x >= y, if I check this formula directly:

(declare-fun x () Int)
(declare-fun y () Int)
(assert (or (<= x y) (>= x y)))
(check-sat)

will return

; File "test.smt2", line 4, characters 1-12: I don't know (0.0021) (2 steps) (goal g_1) unknown

But if I write instead

(declare-fun x () Int)
(declare-fun y () Int)
(assert (and (> x y) (< x y)))
(check-sat)

I will have:

; File "test.smt2", line 3, characters 1-31: Inconsistent assumption (0.0016) (1 steps) ; File "test.smt2", line 4, characters 1-12: Valid (0.0017) (1 steps) (goal g_1) unsat

(your context is now filled with an unsat formula so the following (check-sat) will always return unsat)

[Elarnon]

Right, I did not think that Alt-Ergo would be performing automatic negations in one format but not the other, although it does seem obvious in retrospect. I guess this is just Alt-Ergo not producing models, then. Thanks for the detailed explanation!

[mattiasdrp]

You're welcome :-)

[mattiasdrp]

@Elarnon If you want to try models in Alt-Ergo, check the models branch by the way ;-)