Cardinality constraints

Reply

kornevgen Posted: 09-17-2009 3:40 PM

rated by 0 users

Hi!

I try to use cardinality constraints but Z3 doesn't solve my constraints:

(benchmark test
:logic QF_BV

:extrafuns ((x BitVec[5]) (y1 Int) (y2 Int))

:assumption
(= y1 (ite (= (extract[2:0] x) bv1[3]) 1 0) )

:assumption
(= y2 (ite (= (extract[4:2] x) bv1[3]) 1 0) )

:assumption
(<= 2 (+ y1 y2))

)

And Z3 2.1 returns the following model:

x -> bv1[5]
y1 -> 1
y2 -> 0
sat

However these constraints must be UNSAT !  because it doesn't exist "x" such as x[4:2] == 1 and x[2:0] == 1.

How my constraints can be corrected ?

Reply

Nikolaj Bjorner replied on 09-18-2009 12:12 PM

rated by 0 users

The Z3 release uses auto-configuration when reading SMT files. So when you specify :logic QF_BV, then the only decision procedure that is loaded is the one for bit-vectors. The arithmetic decision procedure is not enabled. Consequently, <= is treated as an uninterpreted function symbol.

You can do:  z3.exe AUTO_CONFIG=false <file.smt>

Or you can just comment out the line ":logic QF_BV" (then auto-configuration is also not used).

Reply

kornevgen replied on 09-18-2009 12:33 PM

rated by 0 users

Thank you very much, Nikolaj !