CodePlexProject Hosting for Open Source Software

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