active questions tagged z3 - Stack Overflow News Feed 
Sunday, April 26, 2015  |  From active questions tagged z3 - Stack Overflow




I've been searching the square root functionality provided by z3. For example, for adding a constraint about a Real number x , that x*x = 2, what is the best way to encode that?



I tried:



(declare-const x Real)
(assert (= 2 (* x x))) 
(check-sat)


The result is unknown. The model is also, unavailable.



However, I am sure there should be a way to satisfy this. I am referring strictly to the extended version of smt-lib 2.0 language and not the python api.



Friday, April 24, 2015  |  From active questions tagged z3 - Stack Overflow




rise4fun z3py is unavailable from several weeks due to some security issues. I tried to find out some resources for learning z3py but ended in vain. Please suggest some resources to learn z3py



Friday, April 24, 2015  |  From active questions tagged z3 - Stack Overflow




I would like to define a piece-wise (linear) function in Z3py, for example, the function f(x) has the form



f(x) = a*x + b when 0 <= x <= 1
f(x) = exp(c*x) when 1 < x <= 2
f(x) = 1/(1+10^x) when 2 < x <= 3
etc.


where a, b and c are constants.



I guess the z3.If() function will be relevant, but as the number of pieces grows, the expression gets convoluted.



My questions is, does Z3pyprovides the if-else statement, or is there an elegant way to define piece-wise function in Z3py?



Friday, April 24, 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))


Thursday, April 23, 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))



Thursday, April 23, 2015  |  From active questions tagged z3 - Stack Overflow




I would like to define a piece-wise (linear) function in z3py, for example, the function f(x) has the form



f(x) = a*x + b when 0 <= x <= 1
f(x) = exp(c*x) when 1 < x <= 2
f(x) = 1/(1+10^x) when 2 < x <= 3
etc.


where a, b, c are constants



I guess the z3.If() function will be relevant, but as the number of pieces grows, the expression gets convoluted.



My questions is, does Z3py provides the If-else statement, or is there an elegant way to define piece-wise function in Z3Py?



Wednesday, April 22, 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.



Wednesday, April 22, 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).



Monday, April 20, 2015  |  From active questions tagged z3 - Stack Overflow




From (Z3: Is it possible to sum up a BitVec and a Real?) , I tried to convert an int to bitvec using



x = Int('x')
reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)


but I always get an error saying " 'Ast' object has no attribute 'ref' ", it seems this function can only convert integer to bitvec, is there any other way to convert Int to bitvec?



Also I know this function is treated as uninterpreted for now, do I need to recompile my local version from (bv-enable-int2bv-propagation option) ?



Thanks in advance!



Monday, April 20, 2015  |  From active questions tagged z3 - Stack Overflow




I'm trying to create some simple examples that use the Z3's Java interpolation API. My intent is to replicate the following SMT-LIB:



(declare-const x Int)
(compute-interpolant (> x 5) (< x 5))


When I give the above SMT-LIB to Z3 on stdin it returns:



unsat
(not (<= x 5))


which is a valid interpolant.



However, when I try to solve the same problem via the Java API:



    System.out.print("Z3 Major Version: ");
    System.out.println(Version.getMajor());
    System.out.print("Z3 Full Version: ");
    System.out.println(Version.getString());
    HashMap<String, String> cfg = new HashMap<String, String>();
    cfg.put("proof", "true");
    cfg.put("model", "true");
    InterpolationContext ictx = new InterpolationContext(cfg);
    Solver s = ictx.mkSolver();
    // A = x > 5
    // B = x < 5
    //Whats Interp(A,B)?
    IntExpr x = ictx.mkIntConst("x");
    IntExpr five = ictx.mkInt(5);
    BoolExpr A = ictx.mkGt(x, five);
    BoolExpr B = ictx.mkLt(x, five);
    BoolExpr iA = ictx.MkInterpolant(A);
    BoolExpr AB = ictx.mkAnd(A, B);
    BoolExpr pat = ictx.mkAnd(iA, B);
    System.out.println("A: " + A);
    System.out.println("B: " + B);
    System.out.println("Pattern: " +  pat);
    Params params = ictx.mkParams();
    s.add(AB);
    //s.add(B);
    s.check();
    Expr proof = s.getProof();         
    Expr[] interps = ictx.GetInterpolant(proof, pat, params);
    for(int i = 0; i < interps.length; i++){
        System.out.println("Interpolant: " + interps[i]);
    }


I get:



Z3 Major Version: 4
Z3 Full Version: 4.4.0.0
A: (> x 5)
B: (< x 5)
Pattern: (and (interp (> x 5)) (< x 5))
Interpolant: true


Am I doing something wrong?



Monday, April 20, 2015  |  From active questions tagged z3 - Stack Overflow




From (Z3: Is it possible to sum up a BitVec and a Real?) , I tried to convert an int to bitvec using



x = Int('x')
reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)


but I always get an error saying " 'Ast' object has no attribute 'ref' ", it seems this function can only convert integer to bitvec, is there any other way to convert Int to bitvec?



Also I know this function is treated as uninterpreted for now, do I need to recompile my local version from (bv-enable-int2bv-propagation option) ?



Thanks in advance!



Monday, April 20, 2015  |  From active questions tagged z3 - Stack Overflow




Browsing Z3 source code, I came across a bunch of files referring to QF_FPA, which seems to stand for quantifier-free, floating-point-arithmetic. However, I don't seem to be able to locate any documentation regarding its state, or how it can be used via various front-ends (in particular SMT-Lib2). Is this an encoding of IEEE-754 FP? If so, which precisions/operations are supported? Any documentation would be most helpful..



Sunday, April 19, 2015  |  From active questions tagged z3 - Stack Overflow




My applicant is originally a SAT problem. Now, I'm trying to do some extension which requires to use some int variables. So the problem becomes a SMT problem. But I encountered a performance problem when using z3 to solve it. As the int variable is bounded (less than 100), it's viable to convert it to a pure SAT problem.



Does anyone know how to apply this tactic in z3 c++ interface?
Or can I use z3 to convert the SMT constraints to SAT formulas firstly and then
try other SAT solvers?

Thanks in advance.



Sunday, April 19, 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))


Sunday, April 19, 2015  |  From active questions tagged z3 - Stack Overflow




Is there any way to extract a SMT-LIB formula, including all the declarations, definitions and constraints into a .smt2 file from the solver/model/context class of the C++ API. I.e. opposite of what the function "Z3_parse_smtlib2_string" does.



Saturday, April 18, 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))


Friday, April 17, 2015  |  From active questions tagged z3 - Stack Overflow




I'm trying to check a simple Timed Automata for reachability using Z3's fixed-point engine.



The TA I'm modeling is:



-->(x = 0 & 0 <= c <= 5) --[c > 2]-->(x = 1)



I want to verify that the state x = 1 & c = 3 is reachable. To do that I input the following into Z3:



(declare-rel T (Int Real Int Real))
(declare-rel REACH (Int Real))
(declare-var x Int) 
(declare-var c Real)
(declare-var nx Int)
(declare-var nc Real)
(declare-var delay Real)
(rule (! (=> (and (= x 0) (> c 2.0)) (T x c 1 c)) :named stepint))
(rule (! (=> (and (REACH x c) (T x c nx nc)) (REACH nx nc)) :named tstep))
(rule (! (=> (and (= c 0.0) (= x 0)) (REACH x c)) :named initialstates))
(rule (! (let ((a!1 (and (>= delay 0.0) (= nc (+ c delay)) (or (not (= x 0)) (< nc 5.0)))))
(=> a!1 (T x c x nc))) :named TICK))

(query (and (REACH x c) (= x 1) (= c 3.0))
 :print-certificate true)


When I run the above in Z3 on rise4fun I get back:



formula false in model: (= REACH_1_0 3.0)
formula false in model: (= REACH_0_0 1)
formula false in model: (= query!0_0_n 1)
formula false in model: (= query!0_1_n 3.0)
sat
(REACH 1 3.0)


Which indicates that x= 1 & c = 3 is reachable. What does "formula false in model mean"? Is this simply informational or is Z3 warning me about potentially poorly formed input?



Wednesday, April 15, 2015  |  From active questions tagged z3 - Stack Overflow




I found the previous releases (tags) on github say "Z3 is licensed under MSR-LA (Microsoft Research License Agreement)".



My question is whether they are also on MIT license now. Could you kindly please clarify? Thanks!



Wednesday, April 15, 2015  |  From active questions tagged z3 - Stack Overflow




I have the following constraint (constr) I want to simplify:



4p+3q<=-10+r AND 4p+3q<=-12+r



p (and similar for r) is created as follows:



Z3_ast p;
Z3_sort ty = Z3_mk_int_sort(ctx)
Z3_symbol s = Z3_mk_string_symbol(ctx, "p");
p = Z3_mk_const(ctx, s, ty)


If i do



Z3_simplify(ctx, constr)


Nothing changes as p and r are integers.



How can I encode the knowledge that p an r are natural numbers (unsigned)?



Simply adding the constraint p >= 0 AND r >= 0 will not help in the context of simplifying my constraint (but of course helps when seeking a solution).



To clarify,



4p+3q<=-10+r AND 4p+3q<=-12+r



should be reduced to:



4p+3q<=-12+r



As it is the hardest to fulfill (implies the other).



UPDATE:
Tried the solution by Taylor on the constraint and it works.
When I try to use the same technique for the following different (somewhat)-pretty-printed constraint:




(([(false AND (0<=5+0epsilon+0q+0p AND false)) OR (0<=5+0epsilon+0q+0p AND [(0+0epsilon+q+0p<=5+0epsilon+0q+0p AND (0+0epsilon+q+0p<=5+0epsilon+0q+0p AND [false OR 0+0epsilon+0q+p<=7+0epsilon+0q+0p])) OR (false AND false) OR (false AND false)])] AND [(false AND (0<=5+0epsilon+0q+0p AND false)) OR (0<=5+0epsilon+0q+0p AND [(0+0epsilon+q+0p<=5+0epsilon+0q+0p AND (0+0epsilon+q+0p<=5+0epsilon+0q+0p AND [false OR 0+0epsilon+0q+p<=7+0epsilon+0q+0p])) OR (false AND false) OR (false AND false)])]) AND epsilon>=0 AND q>=0 AND p>=0)


By Z3_simplify this is reduced to




(q<=5 AND p<=7 AND epsilon>=0 AND q>=0 AND p>=0)


If I create a tactic using ctx-solver-simplify together with a goal and use Z3_apply_result_to_string, I get the following:



(goals
(goal
  (let ((a!1 (+ 5 (* 0 epsilon) (* 0 q) (* 0 p)))
        (a!3 (or false
                 (<= (+ 0 (* 0 epsilon) (* 0 q) p)
                     (+ 7 (* 0 epsilon) (* 0 q) (* 0 p))))))
  (let ((a!2 (<= (+ 0 (* 0 epsilon) q (* 0 p)) a!1)))
    (or (and false (<= 0 a!1) false)
        (and (<= 0 a!1)
             (or (and a!2 a!2 a!3) (and false false) (and false false))))))
  (>= epsilon 0)
  (>= q 0)
  (>= p 0))
)


What can I do to get a simple representation like the one for Z3_simplify?



Wednesday, April 15, 2015  |  From active questions tagged z3 - Stack Overflow




The following c++ api code for z3 results in Segmentation fault: 11
(z3 version 4.4.0 running on Mac OS 10.10.2)



#include "../z3/include/z3++.h"

int main() {
  z3::context c;

  z3::sort A = z3::sort(c);
  z3::expr x = c.constant("x", A);
}


Am I doing something wrong?



 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.