CODEWITHSUNDEEP
z3
Ashiq
Ashiq

Reputation: 307

Does not 'check-sat' support Boolean function as assumption?

In the following example, I tried to use uninterpreted Boolean function like "(declare-const p (Int) Bool)" rather than single Boolean constant for each assumption. But it does not work (it gives 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 (unsupported) to use Boolean function. Is there any reason behind that? Is there different way to do that?

Upvotes: 3

Views: 505

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

We have this restriction because Z3 applies many simplifications before it solves a problem. Some of them will rewrite formulas and terms. The problem that is actually solved by Z3 is very often quite different from the input problem. We would have trace back the simplified assumptions to the original assumptions, or introduce auxiliary variables. Restricting to Boolean literals avoids this issue, and makes the interface very clean. Note that this restriction does not limit the expressiveness. If you think it is too annoying to declare many Boolean variables to track different assertions. I suggest you take a look at the new Python front-end for Z3 called Z3Py. It is much more convenient to use than SMT 2.0. Here is your example in Z3Py: http://rise4fun.com/Z3Py/cL In this example, instead of creating an uninterpreted predicate p, a "vector" (actually, it is a Python list) o Boolean constants is created.

The Z3Py online tutorial contains many examples.

It is also possible to implement in Z3Py the approach that creates auxiliary variables. Here is the script that does the trick. I defined a function check_ext that does all the plumbing. http://rise4fun.com/Z3Py/B4

Upvotes: 3

Related Questions