Clever Geek Handbook

Doesn't "check-sat" support boolean function as guess?

In the following example, I tried to use an uninterpreted boolean function like "(declare-const p (Int) Bool)" rather than a single Boolean constant for each guess. But it doesn't work (it gives a compilation error).

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(declare-fun p (Int) Bool) 
             ;(declare-const p1 Bool) 
             ;(declare-const p2 Bool)
             ; (declare-const p3 Bool)

;; We assert (=> p C) to track C using p
(declare-const x Int)
(declare-const y Int)
(assert (=> (p 1) (> x 10)))
;; An Boolean constant may track more than one formula
(assert (=> (p 1) (> y x)))

(assert (=> (p 2) (< y 5)))
(assert (=> (p 3) (> y 0)))

(check-sat (p 1) (p 2) (p 3))
(get-unsat-core)

Output

Z3(18, 16): ERROR: invalid check-sat command, 'not' expected, assumptions must be Boolean literals
Z3(19, 19): ERROR: unsat core is not available

I understand that it is not possible to use (not supported) to use a Boolean function. Is there any reason for this? Is there any other way to do this?

+3


source to share


1 answer


We have this limitation because the Z3 applies a lot of simplifications before solving the problem. Some of them will rewrite formulas and terms. The problem that the Z3 actually solved is very often different from the input problem. We would ditch the simplistic assumptions to the original assumptions, or introduce auxiliary variables. The restriction on boolean literals avoids this problem and makes the interface very clean. Note that this limitation does not constrain expressiveness. If you find it too annoying to declare many booleans to keep track of different statements. I suggest you take a look at a new Python interface for Z3 called Z3Py. It is much more convenient than SMT 2.0. Here's your example in Z3Py: http://rise4fun.com/Z3Py/cL In this example, instead of creating an uninterpretable predicate p

, "vector" (actually a Python list), it creates boolean constants.

Z3Py online tutorial contains many examples.



In Z3Py, you can also implement an approach that creates helper variables. Here is a script that does the trick. I have defined a function check_ext

that does all the plumbing. http://rise4fun.com/Z3Py/B4

+3


source






More articles:


All Articles