active questions tagged z3 - Stack Overflow News Feed 
Monday, May 25, 2015  |  From active questions tagged z3 - Stack Overflow




I am using z3py. I am trying to check the satisfiability for different problems with different sizes and verify the scalability of the proposed method. However, to do that I need to know the memory consumed by the solver for each problem. Is there a way to access the memory or make the z3py print it in the STATISTICS section. Thank you so much in advance.



Friday, May 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am really new to Z3 and SMT solvers.
I have the following problem which I don't know how to code in Z3py.



In the above block diagram, N contains set of nodes.



In the above diagram N is set of nodes, thus N = {Node1, Node2, Node3, Node4, Node5, Node6, Node7}



I is set of Inputs, I = {I1, I2, I3, I4}



O is set of Outputs, O = {O1, O2, O3}



G is a group where for any consecutive 2 outputs (Oi, Oj), if Oi is first output generated and Oj is second output generated then, Gk is set of nodes that were scheduled after the generation of Oi and before the generation of Oj, but if Oj was generated before Oi then Gk contains all the blocks that were scheduled before Oj was generated.
The scheduling of the nodes is given by another program.
For example in the above block diagram the scheduling of nodes along with generation of output is as follows:



  • First node scheduled = Node1
  • Second node scheduled = Node2
  • Third node scheduled = Node5
  • Output generated = O1
  • Fourth node scheduled = Node3
  • Fifth node scheduled = Node6
  • Output generated = O2
  • Sixth node scheduled = Node4
  • Fifth node scheduled = Node7
  • Output generated = O3

Thus from above we can say that G1 for (O1, O2) is = {Node3, Node6}



But G2 for (O2, O1) is = {Node1, Node2, Node5}



To execute each node we need a task, a task can implement 1 node or a set of nodes at a time.



Noder,i denotes ith node in group Gr.
Taskr,m denotes mth task in group Gr.



The boolean variables (can either be 0 or 1) :



  • fNoder,iTaskr,m represents if
    Noder,i is mapped to Taskr,m
  • DNNoder,iNodes,j represents if
    Nodes,j depends on Noder,i i.e. if there is a path from Noder,i to Nodes,j
  • DTTaskr,mTasks,n represents if
    Tasks,n depends on Taskr,m
  • MTaskr,m represents if there is any node mapped on to Taskr,m

Based on the above information I have to formulate the following equations in SMT.



  1. Minimize ( Σr,m
    MTaskr,m )
  2. MTaskr,m >=
    fNoder,iTaskr,m (for all i)
  3. Σm
    fNoder,iTaskr,m = 1 (for all r != I,O)
    example: fNoder,iTaskr,m + fNoder,iTaskr,m+1 + fNoder,iTaskr,m+2 = 1 + 0 + 0 = This tells us that Noder,i is mapped to Taskr,m since fNoder,iTaskr,m = 1 (only one node can be mapped to 1 task at a time but a task can be mapped to several nodes at a time)
  4. fNoder,iTasks,m = 0 (for all r != s)
  5. fNoder,iTaskr,m = 1 (for all r = I,O and m = i)
  6. fNoder,iTaskr,m = 0 (for all r = I,O and m != i)
  7. DTTaskr,mTasks,n >= fNoder,iTaskr,m + fNodes,jTasks,n + DNNoder,iNodes,j - 2
  8. DTTaskr,mTasks,n >= DTTaskr,mTaskt,l + DTTaskt,lTasks,n - 1
  9. DTTaskr,mTasks,n + DTTasks,nTaskr,m <= 1

I don't understand how to represent the variables and these formulas in SMT format.



Friday, May 22, 2015  |  From active questions tagged z3 - Stack Overflow




How can I get real python values from a Z3 model?



E.g.



p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
s.check()
print s.model()[x]
print s.model()[p]


prints



-1.4142135623?
False


but those are Z3 objects and not python float/bool objects.



I know that I can check boolean values using is_true/is_false, but how can I elegantly convert ints/reals/... back to usable values (without going through strings and cutting away this extra ? symbol, for example).



Thursday, May 21, 2015  |  From active questions tagged z3 - Stack Overflow




How I can write sqrt function in smt-libv2 format.



Note:
To get a maximum of two values, i found a useful link here: Use Z3 and SMT-LIB to get a maximum of two values.



Thursday, May 21, 2015  |  From active questions tagged z3 - Stack Overflow




This smt2 script gives unsat if I use
(check-sat-using (then simplify solve-eqs (repeat bit-blast) (! smt :bv.enable_int2bv true :arith.euclidean_solver true))), and gives sat if I remove :arith.euclidean_solver true. The expected result is sat.
Z3 version 4.4.0



Thank you in advance.



Thursday, May 21, 2015  |  From active questions tagged z3 - Stack Overflow




Given the following simplified quantifiers, with the Z3 options set according to those generated by Boogie (full details below), I get "unknown" as a result:



(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
  :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
  (G x) (F x))
  :pattern ((F x))
))))
(check-sat)


My understanding for what (I think) Z3 would do with this problem, is skolemise the existential (not forall), which would yield ground instances of both F and G. Given these in the e-graph, we should be able to instantiate the other quantifier, and get unsat. I can see that Z3 probably has to case-split to do this, but I would expect this case-splitting to take place after removing the quantifier and populating the e-graph.



Instead, the first quantifier doesn't get instantiated in the above problem. I've made a number of observations:



  1. Swapping the order of the (F x) and (G x) terms in the first quantifier results in "unsat" without any quantifier instantiations (I suppose some simplification spots the similarity between the two quantified assertions?).
  2. Swapping the order of the (G x) and (F x) terms in the second quantifier (as well as those in the first) results in "unsat" with a single quantifier instantiation (which is the behaviour I'd expect in general).
  3. Changing the smt.case_split option affects the behaviour. Set to 3 (as chosen by Boogie) or 5, we get "unknown". Set to 0,1,2 or 4, I get "unsat".

It would be great to understand the scenarios above, and why (in the failing cases) these terms don't always make it to the e-graph after skolemisation. I'm not sure what the effects of changing the case_split option are in general. At the moment, I don't think Boogie allows that to be changed (and overrides any choice made on the command-line). But I have the feeling that the e-graph should get the information in all cases, ideally.



Here's the full file (removing most of the options set doesn't seem to make a difference to the failing cases, except for the smt.case_split one):



(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
;(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.QI.COST |"(+ weight generation)"|)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
(set-option :TIMEOUT 0)
(set-option :smt.QI.PROFILE true)
(set-option :smt.CASE_SPLIT 3)
; done setting options


(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
   :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
(G x) (F x))
  :pattern ((F x))
))))
(check-sat)


Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




I created a std::map of z3::expr and int pair, and wanted to store different expressions. However, when I was storing expression of different kinds, say first a 64-bit vector and then a 32-bit vector, compilers throwed a z3::exception and complaining invalid function application for bvslt, sort mismatch on argument at position 2, expected (_ BitVec 64) but given (_ BitVec 32). It wont complain if I store expr with 64bitvec only or 32 bitvec only. I don't know how this bvslt comes from in storing two independent expressions.



So my question is that is there any way I can store expr with different sorts into a map?



Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




My problem is as followed,



Environment: 64 bit windows 7, vs 2010, z3-4.3.2



First, compiled Z3 from source(download from z3 homepage ), this step is ok and without any mistake (from the command window);



Second, tested the c++ example under the “src/example”, first, test function find_model_example1(), compile, link, this is no warning, and error. However, got stuck when run. Then, after I debug step by step, stuck at the second statement, “context c”;



1, std::cout << "find_model_example1\n";
2, context c;
3, expr x = c.int_const("x");


Keep going with F11 at this statement, it stuck at function “reinterpret_cast” , line 424 in api_context.cpp, keep going with F11, in the constructor of “context” :“context(config_params *, bool)”, function “m_replay_stack” will call function “copy_core”(vector.h), which triggered 0xC00000005 error.



Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




We look for a number of the form efghiihgfe which is the product of two numbers of the form 999ab and 99qcd.



We use the following code



 (declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const p Int)
(declare-const q Int)


(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))


(assert (= (* (+ 99900 (* 10 a) b  )  (+ 99000 (* 100 q) (* 10 c)  d  ))      
           (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)    ) )




(check-sat)
(get-model)

(eval (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e))


and the output is



    (model
  (define-fun q () Int
    6)
  (define-fun p () Int
    0)
  (define-fun i () Int
    0)
  (define-fun h () Int
    6)
  (define-fun g () Int
    6)
  (define-fun f () Int
    9)
  (define-fun e () Int
    9)
  (define-fun d () Int
    1)
  (define-fun c () Int
    8)
  (define-fun b () Int
    9)
  (define-fun a () Int
    7)
)
9966006699


To verify that 9966006699 is the maxim we run the code



 (declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const p Int)
(declare-const q Int)


(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))


(assert (= (* (+ 99900 (* 10 a) b  )  (+ 99000 (* 100 q) (* 10 c)  d  ))      
           (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)    ) )


(assert  (> (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)   9966006699 ))

(check-sat)


and the output is



unsat


Please let me know if there is a more efficient program with Z3 to solve the problem.



Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




all, I am a newer to use Z3. I wrote this smt2 file, but the result return unknown, what is wrong in my file?



(set-option :fixedpoint.engine datalog)

(define-sort site () (_ BitVec 3))

(declare-rel pointsto (Int Int)) ;used to get all points-to relation
(declare-rel dcall (Int Int)) ;used to label all function call or assignment
(declare-rel derived (Int Int))  ;used to get h1->hk
(declare-rel assign (Int Int))

(declare-var vs Int)
(declare-var vd Int)
(declare-var ss Int)
(declare-var sd Int)
(declare-var sm Int)

;;;;; definition of derived ;;;
(rule (=> (dcall vs vd) (pointsto vs vd)))
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd) ) (derived ss sd)))          
(rule (=> (and (derived ss sm) (derived sm sd)) (derived ss sd)))

;facts 0-999 for var, 999** for addr
;(rule (dcall 3 6));src and sink
(rule (dcall 3 4))
(rule (dcall 4 6))

(rule (pointsto 0 9992))
(rule (pointsto 1 9991))
(rule (pointsto 2 9991))
(rule (pointsto 3 99948))
(rule (pointsto 4 99950))
(rule (pointsto 5 99928))
(rule (pointsto 6 9999))

(query (derived 99948 9999))


Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




Can someone kindly point out why the final query doesn't have output?



Basically I tell Z3 if vs-)vd and vs->ss and vd->sd, then sd is derived from ss.



(set-option :fixedpoint.engine datalog)
(define-sort site () (_ BitVec 3))

(declare-rel pointsto (Int site))
(declare-rel dcall (Int Int))
(declare-rel derived (site site))

(declare-var vs Int)
(declare-var vd Int)
(declare-var ss site)
(declare-var sd site)

;;;;; definition of derived ;;
(rule (=> (and (dcall vs vd) (pointsto vs ss) (pointsto vd sd)) (derived ss sd)))          

(rule (dcall 11 12))
(rule (pointsto 11 #b001))
(rule (pointsto 12 #b010))

(query (derived #b001 #b010))


Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




I have a problem to solve that can be translated into difference logic, and rather than implementing a decision procedure, I would like to use z3 for this purpose.
Nevertheless, I run a few examples and I had exponential-like runtimes (even though there is a polytime decision procedure for it). I am new to z3 and I dont know if I am doing something wrong. Here is the code that I am using (c++ api), varing this "max" variable.



int main(int argc, char **argv) {
context c;

solver s(c, "QF_IDL");

int max = 10000;
int prev = 0;
for(int i = 1; i < max; ++i){
    expr x = s.ctx().int_const(std::to_string(i).c_str());
    expr y = s.ctx().int_const(std::to_string(++i).c_str());
    expr pr = s.ctx().int_const(std::to_string(prev).c_str());
    s.add(pr < x);
    s.add(x < y);
    prev = i;
}

s.add(s.ctx().int_const(std::to_string(max-1).c_str()) < s.ctx().int_const(std::to_string(0).c_str()));

clock_t begin = clock();
switch (s.check()) {
    case unsat:   std::cout << "UNSAT"; break;
    case sat:     std::cout << "SAT"; break;
    case unknown: std::cout << "unknown\n"; break;
}

clock_t end = clock();
double elapsed_secs = double(end - begin) / CLOCKS_PER_SEC;

std::cout << "elapsed time: " << elapsed_secs;
}


Many thanks in advance,



Pedro



Wednesday, May 20, 2015  |  From active questions tagged z3 - Stack Overflow




I am really new to Z3 and SMT solvers.
I have the following set of formulas which I don't know how to code in Z3py.



f<sub>n[r][i],a[s][m]</sub> = 0 for all r!= s
f<sub>n[r][i],a[r][m]</sub> = 1 for all r = I,O and m = i
f<sub>n[r][i],a[r][m]</sub> = 0 for all r = I,O and m != i
h<sub>a[r][m],a[s][n]</sub> >= f<sub>n[r][i],a[r][m]</sub> + f<sub>n[s][j],a[s][n]</sub>+Q<sub>n[r][i],n[s][j]</sub> -2
h<sub>a[r][m],a[s][n]</sub> >=  h<sub>a[r][m],a[t][l]</sub> +  h<sub>a[t][l],a[s][n]</sub> -1
h<sub>a[r][m],a[s][n]</sub> +  h<sub>a[s][n],a[r][m]</sub> <= 1


where the variables:



f<sub>n[r][i],a[s][m]</sub> tells if n[r][i] is mapped to a[s][m]
h<sub>a[r][m],a[s][n]</sub> tells if a[s][n] depends on a[r][m]
Q<sub>n[r][i],n[s][j]</sub> tells if n[s][j] depends on n[r][i]


I don't understand how to represent the variables and these formulas in SMT format.



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




last time I asked how to define a function in the Z3 Java API. The reason was that there is no command to define a function in the Java API. The answer was to substitute the argument values of the function for the input values (Z3 Java API defining a function).



Example (what I need):



1. without API (normal smt-file)



(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x))

(assert (< (max2 a b) c))
(assert (>= (max2 a b) c))

(check-sat)


What I do now is something like this:



2. with Java API



Context ctx = new Context();

ArithExpr a = (ArithExpr) ctx.mkConst(ctx.mkSymbol("a"), ctx.getIntSort());
ArithExpr b = (ArithExpr) ctx.mkConst(ctx.mkSymbol("b"), ctx.getIntSort());
ArithExpr c = (ArithExpr) ctx.mkConst(ctx.mkSymbol("c"), ctx.getIntSort());

ArithExpr max2 = (ArithExpr) ctx.mkITE(ctx.mkLe(a, b), b, a);
BoolExpr one = (BoolExpr) ctx.mkLt(max2, c);
BoolExpr two = (BoolExpr) ctx.mkGe(max2, c);


I wonder, if this makes a difference?



I assume that the max2-function in the smt-file (1) is correct and does not have to be re-solved again. But if I do it as in the above java code (2), the solver has to solve the expression of the max2-function ctx.mkITE(ctx.mkLe(a, b), b, a) every time again. Or am I completely wrong and it is not possible, to ignore the expression of the max2-function?



Does anyone have an idea?



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




How does one use the 'repeat' and 'rotate_left' bitvector operations?



More generally, where can I find detailed documentation of bitvector operations in the SMT2 scripting format used by Z3?



Everything I find seems to just go to tutorials, or broken links:

https://github.com/Z3Prover/z3/wiki/Documentation

http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html



Trying to understand "repeat", "rotate_left", and "rotate_right" by guessing has been frustating. I cannot figure out how to use them. For example



(display (repeat #b01))
(display (repeat #b01 3))
(display (repeat 3))
(display (rotate_left #b0001 2))


gives



"repeat expects one non-zero integer parameter"
"repeat expects one argument"
"operator is applied to arguments of the wrong sort"
"rotate left expects one argument"


Where is the documentation? Hoping they didn't explain because all of this is standard, I also looked at smt-lib.org but that doesn't list these details either. So frustrating.



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




I have a 32bit bit vector expression. Somehow I want to do a signed or unsigned extension on this expression to a 64bit bit vector. Is there any API I can use?



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




I got a 'simple' formula that the Z3 solver (python interface) seems unable to handle. It is running for quite some time (30 minutes) and then returning unkown even though I can find a satisfying assignment by hand in under a minute. This is the formula:



[Or(<uc 1.0> == 0, <uc 1.0> == 1),
 Or(<uc 1.1> == 0, <uc 1.1> == 1),
 Or(<uc 1.2> == 0, <uc 1.2> == 1),
 <uc 1.0> + <uc 1.1> + <uc 1.2> == 1,
 Or(<uc 0.0> == 0, <uc 0.0> == 1),
 Or(<uc 0.1> == 0, <uc 0.1> == 1),
 Or(<uc 0.2> == 0, <uc 0.2> == 1),
 <uc 0.0> + <uc 0.1> + <uc 0.2> == 1,
 Or(<uc 2.0> == 0, <uc 2.0> == 1),
 Or(<uc 2.1> == 0, <uc 2.1> == 1),
 Or(<uc 2.2> == 0, <uc 2.2> == 1),
 <uc 2.0> + <uc 2.1> + <uc 2.2> == 1,
 ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000,
                           ForAll(a,
                                  Or(a > 1000,
                                     Or(a < -1000,
                                        And(And(And(True,
                                        a ==
                                        <uc 0.0>*b +
                                        <uc 0.1>*c +
                                        <uc 0.2>*a),
                                        b ==
                                        <uc 1.0>*b +
                                        <uc 1.1>*c +
                                        <uc 1.2>*a),
                                        c ==
                                        <uc 2.0>*b +
                                        <uc 2.1>*c +
                                        <uc 2.2>*a))))))))))]


It may look a bit scary but let me walk you through it.
< uc i.j> are all integer variables. I first specify that they
should be either 0 or 1 and then I'm introducing the constraint
that exactly one of them should be 1 and the others
need to be 0 (using the sum).



In the second part you can ignore all the Or's which bascially just limit my search space for each variable to [-1000, 1000]. I then have the inner most constraints which should imply: < uc 0.2> = 1 < uc 1.0> = 1 < uc 2.1> = 1 and all other = 0. That's all. I'm pretty sure the solver
should be able to solve this but no luck. I can change the sum
constraint to something like Or(< uc 1.0>,< uc 1.1>,< uc 1.2>) which, funny
enough, solves my problem in this case (the solver
returns the correct assignment in seconds) but in general, this is
obviously, not equivalent to what I want to have.



Questions:



  • Is there something like a bit, which I could use instead of Integers?
  • Some recommended way to express the fact that exactly one argument is 1?
  • Some other way to make this solvable without changing the second part of the formula.

Thank you very much!



// Edit: After playing around with a few options I 'solved' it by placing the side conditions after the ForAll condition (just swapping the two lines of code). This shouldn't make a difference at all but now he is finding the correct assignment in 0.5 seconds - what? I also tried the example with 4 variables (a,b,c,d) instead (a,b,c) but then again it runs for hours... Any help? Also chaning the sum with a length And/Or did not work.



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




I'm using Z3 to check some quantified formulas. If I assert the formula via Z3's Java API the MBQI engine might not converge if the formula is unsat. I know that my formulas are not in a fragment of FOL that is known to be decidable, however if I input the same formula via Z3's smt-lib interface it produces an answer quite quickly. I suspect that some option is not being set via the API that is normally active with the normal SMTLIB input or that I'm not adding important meta information to the formulas via the API.



The assertion in the following SMTLIB session was taken directly from the toString of the BoolExpr I'm asserting via the API:



(set-option :smt.mbqi true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi.trace true)
(declare-fun R (Int Int) Bool)
(declare-const |'x| Int)
(declare-const |'y| Int)
(assert 
  (let ((a!1 (forall ((|'x0| Int) (|'y0| Int))
         (= (R |'x0| |'y0|)
            (and (forall ((|'y1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'y0| 0) (= |'y1| 1))
                                       (and (= |'y0| 1) (= |'y1| 3))
                                       (and (= |'y0| 2) (= |'y1| 3))
                                       (and (= |'y0| 0) (= |'y1| 2)))))
                         (a!2 (exists ((|'x1| Int))
                                (and (or (and (= |'x0| 3) (= |'x1| 0))
                                         (and (= |'x0| 1) (= |'x1| 3))
                                         (and (= |'x0| 1) (= |'x1| 2))
                                         (and (= |'x0| 2) (= |'x1| 0))
                                         (and (= |'x0| 0) (= |'x1| 1)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2)))
                 (forall ((|'x1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'x0| 3) (= |'x1| 0))
                                       (and (= |'x0| 1) (= |'x1| 3))
                                       (and (= |'x0| 1) (= |'x1| 2))
                                       (and (= |'x0| 2) (= |'x1| 0))
                                       (and (= |'x0| 0) (= |'x1| 1)))))
                         (a!2 (exists ((|'y1| Int))
                                (and (or (and (= |'y0| 0) (= |'y1| 1))
                                         (and (= |'y0| 1) (= |'y1| 3))
                                         (and (= |'y0| 2) (= |'y1| 3))
                                         (and (= |'y0| 0) (= |'y1| 2)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2))))))))
 (and (= |'x| 0) (= |'y| 0) (R |'x| |'y|) a!1)))
(check-sat)


Interestingly, when I run the above through Z3's SMTLIB interface the MBQI trace is short and looks like this:



(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
...
(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
unsat


However, the trace when run via the API (and the same solver options) looks like:



(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)
(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)


Is the "null" reference indicative of something I'm doing wrong on the API side?



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




Consider the following SMT-LIB code:



(set-option :auto_config false)
(set-option :smt.mbqi false)
; (set-option :smt.case_split 3)
(set-option :smt.qi.profile true)

(declare-const x Int)

(declare-fun trigF (Int Int Int) Bool)
(declare-fun trigF$ (Int Int Int) Bool)
(declare-fun trigG (Int) Bool)
(declare-fun trigG$ (Int) Bool)

; Essentially noise
(declare-const y Int)
(assert (!
  (not (= x y))
  :named foo
))

; Essentially noise
(assert (forall ((x Int) (y Int) (z Int)) (!
  (= (trigF$ x y z) (trigF x y z))
  :pattern ((trigF x y z))
  :qid |limited-F|
)))

; Essentially noise
(assert (forall ((x Int)) (!
  (= (trigG$ x) (trigG x))
  :pattern ((trigG x))
  :qid |limited-G|
)))

; This assumption is relevant
(assert (forall ((a Int) (b Int) (c Int)) (!
  (and
    (trigG a)
    (trigF a b c))
  :pattern ((trigF a b c))
  :qid |bar|
)))


Trying to assert that axiom bar holds, i.e.,



(push)
(assert (not (forall ((a Int) (b Int) (c Int))
  (and
    (trigG a)
    (trigF a b c)))))
(check-sat)
(pop)


fails (Z3 4.3.2 - build hashcode 47ac5c06333b):



unknown
[quantifier_instances]  limited-G :      1 :   0 : 1




Question 1: Why did Z3 only instantiate limited-G but neither limited-F nor bar (which would prove the assertion)?



Question 2: Commenting any of the (useless) assertions foo, limited-F or limited-G allows Z3 to prove the assertion - why is that? (Depending on which are commented, either only bar or bar and limited-F are instantiated.)





In case it is related to the observed behaviour: I would like to set smt.case_split to 3 (my configuration follows the one omitted by MSR's Boogie tool), but Z3 gives me WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5, despite the fact that (set-option :auto_config false).



Tuesday, May 19, 2015  |  From active questions tagged z3 - Stack Overflow




I guess my issue is linked with Read func interp of a z3 array from the z3 model, but still I can't understand how to fix it.



Edit: I think it is also linked with de bruijn index: Understanding the indexing of bound variables in Z3



Here is the small example I have built to explain the problem:



#include <iostream>
#include <sstream>
#include <cassert>
#include "z3++.h"

using namespace z3;

int main(void)
{
    context ctx;
    params p(ctx);
    p.set("MACRO_FINDER",true);

    expr_vector v(ctx);
    sort_vector sv(ctx);
    for(int i = 0; i < 3; i++)
    {
        std::ostringstream o;
        o << "c[" << i << "]";
        expr c = ctx.bv_const(o.str().c_str(),1);
        v.push_back(c);
        sv.push_back(ctx.bv_sort(1));
    }

    expr x = ctx.bv_const("x",8);

    v.push_back(x);
    sv.push_back(ctx.bv_sort(8));

    expr one_bit = ctx.bv_val(1,1);
    expr two = ctx.bv_val(2,8);
    expr one = ctx.bv_val(1,8);
    expr zero = ctx.bv_val(0,8);
    expr fcore = x + ite(v[1] == one_bit , one, zero) + ite(v[2] == one_bit, two, zero); 

    func_decl f = ctx.function("f",sv,ctx.bv_sort(8));

    solver s(ctx);
    s.set(p);
    s.add(forall(v,f(v) == fcore));

    expr_vector t1(ctx);
    expr_vector t2(ctx);
    t1.push_back(v[0]); t1.push_back(v[1]); t1.push_back(v[2]); t1.push_back(ctx.bv_val(0,8));
    t2.push_back(v[0]); t2.push_back(v[1]); t2.push_back(v[2]); t2.push_back(ctx.bv_val(1,8));
    expr constraints = (f(t1) == ctx.bv_val(1,8)) && (f(t2) == ctx.bv_val(2,8));

    s.add(exists(v[0],v[1],v[2],constraints));

    std::cout << "Solver: " << s << "\n\n";
    if(s.check()==sat)
    {
        model m = s.get_model();
        std::cout << "Model: " << m << "\n\n";
        std::cout << "Number of constants: " << m.num_consts() << "\n";

        expr F = m.eval(f(v),true);

        for(size_t i = 0; i < m.num_consts(); ++i)
            std::cout << "\t constant " << i << ": " << "(" << m.get_const_decl(i).name() << ") " << m.get_const_interp(m.get_const_decl(i)) << "\n";

        std::cout << "Number of functions: " << m.num_funcs() << "\n";
        std::cout << "\t" << F << "\n";
    }
    else
        std::cout << "unsat\n";
    return 0;
}


By runing this program, I get the following output:



Solver: (solver
  (forall ((|c[0]| (_ BitVec 1))
           (|c[1]| (_ BitVec 1))
           (|c[2]| (_ BitVec 1))
           (x (_ BitVec 8)))
    (= (f |c[0]| |c[1]| |c[2]| x)
       (bvadd x (ite (= |c[1]| #b1) #x01 #x00) (ite (= |c[2]| #b1) #x02 #x00))))
  (exists ((|c[0]| (_ BitVec 1)) (|c[1]| (_ BitVec 1)) (|c[2]| (_ BitVec 1)))
    (and (= (f |c[0]| |c[1]| |c[2]| #x00) #x01)
         (= (f |c[0]| |c[1]| |c[2]| #x01) #x02))))

Model: (define-fun |c[2]!0| () (_ BitVec 1)
  #b0)
(define-fun |c[1]!1| () (_ BitVec 1)
  #b1)
(define-fun f ((x!1 (_ BitVec 1))
 (x!2 (_ BitVec 1))
 (x!3 (_ BitVec 1))
 (x!4 (_ BitVec 8))) (_ BitVec 8)
  (bvadd x!4 (ite (= #b1 x!3) #x02 #x00) (ite (= #b1 x!2) #x01 #x00)))

Number of constants: 2
         constant 0: (c[2]!0) #b0
         constant 1: (c[1]!1) #b1
         constant 2: (c[0]) #b0
         constant 3: (c[1]) #b0
         constant 4: (c[2]) #b0
         constant 5: (x) #x00
Number of functions: 1
        #x00


I don't get:



  • Why it enumerates 6 constants and not 3 ?
  • How to retrieve the value of the nth constant of vector "v" without parsing their name, which is not the nth constant of the model "m" ?
  • Why c[1] evaluates to 0 while I would have expected it to evaluate to 1 ?
  • What "!x" means in the name of the constant c[2]!0 and c[1]!1 ?

I would like to re-inject evaluations of c[0], c[1] and c[2] into the function f() in order to simplify its expression (I expect to get x+1)



Note: c[0] is not used on purpose...



 active questions tagged z3 - Stack Overflow News Feed 

Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13

Comments

No comments yet.