2

Context: I do research on bounded java program verification using z3. I want to get an optimization model on a linearization problem. A standard approach could be incrementally search the model until find a unsat case. But the performance seems be a problem, and it destroys the code portability by introducing JNI, which intergrates z3 c/c++ api to my tool.

Now I want to add constraints on all inputs of a java method. I use quantity arrays (I use theory of array to model heaps). However, z3 always returns "unknown" immediately on a satisfiable problem. It seems that it is impossible to generate model. I notice that there is an option of z3, INST_GEN, then I am trying to understand it. I feed following formulas to z3.

(set-option :INST_GEN true)
(define-sort S () (_ BitVec 2))
(declare-fun s () S)
(assert (= s (_ bv0 2)))

(define-sort A () (Array S S))
(push) ;; 1st case    
(assert (forall ((a A)) (= (select a s) s)))
(check-sat)
(get-model)
(pop)

(push) ;; 2nd case
(declare-fun a () A)
(assert (forall ((t S)) (= (select a t) t)))
(check-sat)
(get-model)
(pop)

(push) ;; 3rd case
(check-sat)
(get-model)
(pop)

In both 1st and 2nd cases, z3 returns "segmentation fault" in Linux, while it crashes in windows 7. Both z3 are version 4.0, x64.

In 3rd case, it is quantify-free, and Z3 successfully generates model

sat 
(model (define-fun s () (_ BitVec 2) #b00) )

My first question is how this option works? Does it enumerate arrays?

Second question is, I notice that z3 could successfully return "unsat" on a unsatisfied problem with quantify arrays. Does z3 support some option or approach to generate a model in a satisfied problem with quantified arrays, with bounded indices and elements? e.g. using if-then-else clause.

Daniel Widdis
  • 8,424
  • 13
  • 41
  • 63
Tianhai Liu
  • 795
  • 5
  • 10

1 Answers1

2

First, the option INST_GEN was part of an experiment. It should not have been exposed to external users. This options was not seriously tested. It will be hidden in future versions. Sorry about that.

Second, in general, Z3 will fail on satisfiable problems that quantify over arrays. The following tutorial (section Quantifiers) describes many fragments where Z3 is complete.

Finally, Z3 has many different engines/solvers. However, only one of them supports incremental solving. Whenever, push/pop commands are used, Z3 will automatically switch to this incremental solver. If we remove the push and pop commands, then Z3 can show the second problem to be satisfiable. Here is a link with the modified example: http://rise4fun.com/Z3/apcQ.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thank you, Leonardo. It helps me a lot. By the way, given an unsatisfied problem in bounded domain, z3 can always return "unsat", is that true? Because, following problem seems be unsatisfiable, but z3 return "unknow". [http://rise4fun.com/Z3/Mxyu](http://rise4fun.com/Z3/Mxyu), The formulas are not quantify over arrays, right? – Tianhai Liu Jul 13 '12 at 15:08
  • No, this is not the case. The list of fragments where Z3 is a decision procedure is described in the Z3 tutorial. Of course, in the future, we can extend that. For example, there is no reason for Z3 failing in the kind of problem described in http://rise4fun.com/Z3/Mxyu – Leonardo de Moura Jul 13 '12 at 15:36