While trying to solve large nonlinear real arithmetic problems, I track every assertion using answer literals and explicit implications, as recommended in other posts. It should be equivalent to using the (! (...) :named p1) syntax of the SMT2 format. It seems, though, that both methods are handled differently internally.
The following SMT2 code gives an UNKNOWN result, with explanation "(incomplete (theory arithmetic))":
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const p5 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (=> p5 (< x3 0.0)))
(check-sat p1 p2 p3)
(get-info:reason-unknown)
On the other hand, the following SMT2 code gives the correct answer, UNSAT, and produces an informative unsat core (p4, p5):
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (! (= x1 (/ 1.0 (* x2 x2))) :named p1))
(assert (! (not (= x2 0.0)) :named p2))
(assert (! (= x3 (* 2.0 x1)) :named p3))
(assert (! (= x3 5.0) :named p4))
(assert (! (< x3 0) :named p5))
(check-sat)
(get-unsat-core)
;(get-model)
My specific questions are:
- How can this differing behavior be explained? What is recommended practice for tracking nonlinear real equations and inequalities?
- What would be the equivalent OCaml API call for the (! (...) :named p1) syntax of SMT2? Is it assert_and_track?
I am using Z3 version 4.3.2 from the ml-ng branch under Linux.
Many thanks!
