calling solver `veriT` on case-sensitive file systems

[johnyf]

The SMT solver veriT version stable2016 installs an executable by default named as veriT. tlapm calls verit:

https://github.com/tlaplus/v2-tlapm/blob/c3ff57bf7f47c529fc2c8598654ea99fdee9f576/src/oldpm/params.ml#L178-L182

(In the source of version 1.4.3: https://github.com/cartazio/tlaps/blob/562a34c066b636da7b921ae30fc5eacf83608280/src/params.ml#L177-L180)

On file systems that are case-sensitive (e.g., ext4), this call fails to find veriT. Renaming the installed executable avoids this error.

Calling veriT instead of verit would work with the solver's default executable name.

This behavior was observed with tlapm version 1.4.3 (build 34695).

[quicquid]

Hello, this is fixed in the head of the (unfortunately semi-private) v1 repository. We are testing a maintenance release right now, so it should be included in the next release.

If you want to try it yourself before, you can change AUFNIRA to UFLIA in smt2.ml (I tested with the head version which has more changes in the smt backend, so there might still be some issues)

[johnyf]

Thank you for addressing this issue, I changed the logic to "UFLIA" and it works well with veriT.

[quicquid]

I was a bit hesitant when restricting the logic to linear integer arithmetic because there might be some small number of non-linear obligations that Z3 / CVC4 solve. Interestingly enough,

THEOREM \E x \in Nat : x*x + x = 6 BY Z3

is still solved (just by Z3, not by veriT / CVC4 though).

[johnyf]

Thanks for pointing this out, in case reverting to "AUFNIRA" turns out to be necessary for solving any problems. Trying CVC3 with "UFLIA" on some of my existing files indeed failed to prove some theorems, until I reverted to "AUFNIRA".

Z3

In my case when using BY Z3 a backend is selected that generates a file tlapm_*.smt2 that contains:

;; Proof obligation:
;;\E x \in Nat : x * x + x = 6
(set-option :print-success false)
(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :auto-config false) 
(set-option :mbqi true) 
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not (exists ((x Int)) 
        (and true 
    (<= 0 x) 
    (= (+ (* x x) x) 6)))))
;; Main assertions from the proof obligation
(check-sat)
(get-model)

and the theorem gets proved by z3. This file leaves the logic unspecified, and it seems that Z3's default behavior is to choose the logic and solvers by looking at the given formula, as mentioned here (see also here). (To call z3 directly z3 -smt2 nonlinear.tlaps/tlapm_*.smt2)

CVC3

Using BY CVC3, a backend appears to be selected that generates a file tlapm_*.smt that contains:

;; Proof obligation:
;;\E x \in Nat : x * x + x = 6
(set-logic UFLIA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not (exists ((x Int)) 
        (and true 
    (<= 0 x) 
    (= (+ (* x x) x) 6)))))
;; Main assertions from the proof obligation
(check-sat)
(exit)

When CVC3 is given the above file cvc3 -lang smt2 nonlinear.tlaps/tlapm_*.smt, then:

1. using the logic UFLIA it says Parse Error: cannot resolve an identifier: "Int"
2. using the logic AUFNIRA it says "unknown"

(I tried running the smt file also with z3, using z3 -smt nonlinear.tlaps/tlapm_*.smt, but it raises several errors.) The above were obtained using tlapm --cleanfp --debug tempfiles -v nonlinear.tla.

CVC4

Trying CVC4 (https://github.com/CVC4/CVC4/commit/f149cd31f8d96a76b34668eb4cd593aa2b5bb7c8) with cvc4 --lang smt2 nonlinear.tlaps/tlapm_*.smt:

1. using the logic UFLIA it says "unknown"
2. using the logic AUFNIRA it says "unknown".

Yices

Out of curiosity, I tried also yices version 2, with input:

---- MODULE nonlinear ----
EXTENDS Naturals, TLAPS

THEOREM \E x \in Nat:  x*x + x = 6
BY Yices
==========================

It turns out that currently, yices v2 supports only quantifier-free logics (so not "AUFNIRA" or "UFLIA"), even though it does parse their full versions, in anticipation of future extensions.

Side comment about yices: The argument -tc of yices version 1 is not present in yices version 2 (https://github.com/johnyf/tlaps/commit/e26452c92e0f18b55c8b6d62556aa4e456455557).

[johnyf]

Motivated by a comment above, trying Z3 with a specific logic selected shows that indeed Z3 can decide as "unsat" the smt2 input:

;; Proof obligation:
;;\E x \in Nat : x * x + x = 6
(set-logic UFLIA)  ;; this statement was added to the auto-generated smt2 file
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not (exists ((x Int))
        (and true
    (<= 0 x)
    (= (+ (* x x) x) 6)))))
;; Main assertions from the proof obligation
(check-sat)
(get-model)

whereas CVC4 says "unknown" when using "UFLIA" or "AUFNIRA". (I removed the set-option commands because they were raising errors with CVC4).