CodePlexProject Hosting for Open Source Software

active questions tagged z3 - Stack Overflow News Feed

Monday, December 15, 2014 | From
active questions tagged z3 - Stack Overflow

Suppose I wish to encode something like the following expression using the Z3 python API:

```
(bv-redand
(bv-or
(bv-xnor symbolic_bit_0
(bv-concat src_ip dst_ip src_port dst_port))
symbolic_dc_0)))))
```

How would I do this?

It appears I must do something like:

```
And(~(symbolic_bit_0 ^ Concat(src_ip dst_ip src_port dst_port)) | symbolic_dc_0)
```

But the outermost And doesn't seem to work. One hack I can think of is to avoid the And and instead compare with all 1s, but is there a better way of doing this?

As a side note, is there a way to directly specify a Xnor b instead of ~(a ^ b)?

Monday, December 15, 2014 | From
active questions tagged z3 - Stack Overflow

Suppose I wish to encode something like the following expression using the Z3 python API:

```
(bv-redand
(bv-or
(bv-xnor symbolic_bit_0
(bv-concat src_ip dst_ip src_port dst_port))
symbolic_dc_0)))))
```

How would I do this?

It appears I must do something like:

```
And(~(symbolic_bit_0 ^ Concat(src_ip dst_ip src_port dst_port)) | symbolic_dc_0)
```

But the outermost And doesn't seem to work. One hack I can think of is to avoid the And and instead compare with all 1s, but is there a better way of doing this?

As a side note, is there a way to directly specify a Xnor b instead of ~(a ^ b)?

Sunday, December 14, 2014 | From
active questions tagged z3 - Stack Overflow

Does anybody please know if there's a way to interact with a function through z3py that I've already defined in Z3 and parsed using parse_smt2_string ? I'm a Z3 and python and Z3Py newbie so apologies if this is obvious, but I've not found any similar questions on here so far...

I've tried things of the form:

`original = """ `

(define-fun MyFun () Real

....

)

"""

f = parse_smt2_string (original)

s = Solver()

s.add(f)

MyFun = Function('MyFun')

s.push()

s.add(MyFun <= 0.4)

s.check()

s.pop()

s.push()

s.add(MyFun >= 0.8)

s.check()

s.pop()

But this returns different results to if I add the assertions into the Z3 string I'm parsing. I think it's because it's not recognising that MyFun in python is the same as in the string. So presumably, I'm defining the function incorrectly, but I can't work
out what I'm doing wrong. I've also tried `MyFun = Function('MyFun', RealSort())`

but that didn't work....

Can anyone help me out please? :)

Thursday, December 11, 2014 | From
active questions tagged z3 - Stack Overflow

I am trying to access the value of an element from the model that I am receiving from
`Z3py`

, so that I can use it later for comparison. But it seems like it's not working.

```
from z3 import*
from networkx import*
from random import*
G=nx.Graph()
G.add_node('n1')
G.add_node('n2')
G.add_node('n3')
G.add_node('n4')
G.add_node('n5')
G.add_node('n6')
G.add_edge('n1', 'n2')
G.add_edge('n2', 'n3')
G.add_edge('n3', 'n4')
G.add_edge('n3', 'n5')
G.add_edge('n3', 'n6')
G.add_edge('n1', 'n6')
G.add_edge('n2', 'n5')
paths = list (nx.all_simple_paths(G, source='n1', target='n4', cutoff=5))
r11=paths[0]
r22=paths[1]
r33=paths[2]
n1 = Int('n1')
n2 = Int('n2')
n3 = Int('n3')
n4 = Int('n4')
n5 = Int('n5')
n6 = Int('n6')
r1 = Int('r1')
r2 = Int('r2')
r3 = Int('r3')
r12= Bool('r12')
s=Solver()
s.add(n1>=0)
s.add(n2>=0)
s.add(n3>=0)
s.add(n4>=0)
s.add(n5>=0)
s.add(n6>=0)
s.add(n1<=1)
s.add(n2<=1)
s.add(n3<=1)
s.add(n4<=1)
s.add(n5<=1)
s.add(n6<=1)
s.add(n1==1)
s.add(n4==1)
s.add(r1==n1*n2*n3*n4)
s.add(r2==n1*n2*n5*n3*n4 )
s.add(r3==n1*n6*n3*n4)
s.add( r12== (Or ( r1==1, r2==1, r3==1)) )
s.add(r12==True)
model = s.model()
if model[r1] == 1:
print "model[r1] is: ", model[r1]
s.add(r1==0)
elif (model[r2]== 1):
s.add(2==0)
elif (model[r3]== 1):
s.add(r3==0)
```

`model`

is a satisfiable solution model returned by `Z3py`

of the form:

```
e.g. [r1=0, r2=1, r3=1]
```

Now given the fact that I have these values `[r1=0, r2=1, r3=1]`

in model the
`if`

condition:

```
if model[r1] == 1:
```

should never become `True`

if in `model`

`r1=0`

but it is still executing

```
print "model[r1] is: ", model[r1]
```

which means that `if model[r1] == 1`

is always becoming `True`

regardless of whether
`r1`

is `0`

or `1`

.

Any help? What should I do if I want to use `model[r1]`

in comparison? Or how to access the value of
`r1`

for comparison, where `r1`

, `r2`

, `r3`

are
`Z3py.Int`

s.

Thursday, December 11, 2014 | From
active questions tagged z3 - Stack Overflow

I am trying to access the value of an element in list so that I can use it later for comparison. But it seems like it's not working.

```
if model[r1] == 1:
print "model[r1] is: ", model[r1]
current_route = r11
s.add(r1==0)
elif (model[r2]== 1):
current_route = r22
s.add(2==0)
elif (model[r3]== 1):
current_route = r33
s.add(r3==0)
```

`model`

is a list of the form:

```
[r1=0, r2=1, r3=1]
```

Now given the fact that I have these values `[r1=0, r2=1, r3=1]`

in model the if condition:

```
if model[r1] == 1:
```

should never become `True`

if in `model`

`r1=0`

but it is still executing

```
print "model[r1] is: ", model[r1]
```

which mean `if model[r1] == 1`

is always becoming `True`

regardless of
`r1`

is `0`

or `1`

.

Any help? What should I do if I want to use `model[r1]`

in comparison?

Saturday, December 06, 2014 | From
active questions tagged z3 - Stack Overflow

I've built z3 as described here using the ml-ng branch. Everything seems to have completed fine, except when I want to use z3 in the OCaml toplevel (I try to use the FindLib #require command to import what's needed) I get this error:

**Error: The external function `n_is_null' is not available**

any ideas on what this is, and how I would go about successfully using z3 in the toplevel?

Thursday, December 04, 2014 | From
active questions tagged z3 - Stack Overflow

Find that the performance of Z3 (unstable version) java API is inconsistent. For certain benchmarks, sometimes it took less then 5sec, sometimes it took more than 60sec. Wonder if there's something random there?

Thursday, December 04, 2014 | From
active questions tagged z3 - Stack Overflow

I need to generate a graph from the output of the z3 model. Any one have an idea about a method or tools that can generate graph from z3-SMT model.

Thank you!

Wednesday, December 03, 2014 | From
active questions tagged z3 - Stack Overflow

Any one have an idea about a method or tools that can generate graph from z3-SMT model.

Wednesday, December 03, 2014 | From
active questions tagged z3 - Stack Overflow

:A variable x is defined as an int sort by

(declare-const x Int)

Is there any method to convert the x into a bitvector sort? Because sometimes x involves bit operations such as &, |, ^ that int theory cannot handle.

I do not want to define the variable x as a bitvector in the beginning because I suppose the operations (e.g., +, -, *, /) supported by int theory except bit operations run much faster than those operations supported in bitvectors.

So actually, I want to covert int sort into bitvector sort or vise vesa in demand.

Thanks.

Ting Chen

Tuesday, December 02, 2014 | From
active questions tagged z3 - Stack Overflow

:A variable x is defined as an int sort by

(declare-const x Int)

Is there any method to convert the x into a bitvector sort? Because sometimes x involves bit operations such as &, |, ^ that int theory cannot handle.

I do not want to define the variable x as a bitvector in the beginning because I suppose the operations (e.g., +, -, *, /) supported by int theory except bit operations run much faster than those operations supported in bitvectors.

So actually, I want to covert int sort into bitvector sort or vise vesa in demand.

Thanks.

Ting Chen

Tuesday, December 02, 2014 | From
active questions tagged z3 - Stack Overflow

:A variable x is defined as an int sort by

(declare-const x Int)

Is there any method to convert the x into a bitvector sort? Because sometimes x involves bit operations such as &, |, ^ that int theory cannot handle.

I do not want to define the variable x as a bitvector in the beginning because I suppose the operations (e.g., +, -, *, /) supported by int theory except bit operations run much faster than those operations supported in bitvectors.

So actually, I want to covert int sort into bitvector sort or vise vesa in demand.

Thanks.

Ting Chen

Tuesday, December 02, 2014 | From
active questions tagged z3 - Stack Overflow

```
(declare-const x Real)
(declare-fun f (Real) Real)
(assert (= (f 1.0) 0.0))
(assert (= (* x x) (* 1.0 1.0)))
(check-sat)
(get-model)
```

I have two independent assertions one in non-linear arithmetic and other uninterpreted functions. Z3 gives a "model is not available" to the problem above. Is there a way to set the logic to something that can handle both at the same time? Thank you.

Tuesday, December 02, 2014 | From
active questions tagged z3 - Stack Overflow

I've built z3 as described here using the ml-ng branch. Everything seems to have completed fine, except when I want to use z3 in the OCaml toplevel (I try to use the FindLib #require command to import what's needed) I get this error:

**Error: The external function `n_is_null' is not available**

any ideas on what this is, and how I would go about successfully using z3 in the toplevel?

Tuesday, December 02, 2014 | From
active questions tagged z3 - Stack Overflow

I've built z3 as described here using the ml-ng branch. Everything seems to have completed fine, except when I want to use z3 in the OCaml toplevel (I try to use the FindLib #require command to import what's needed) I get this error:

**Error: The external function `n_is_null' is not available**

any ideas on what this is, and how I would go about successfully using z3 in the toplevel?

Sunday, November 30, 2014 | From
active questions tagged z3 - Stack Overflow

As part of a reverse engineering exercise, I'm trying to write a Z3 solver to find a username and password that satisfy the program below. This is especially tough because the z3py tutorial that everyone refers to (rise4fun) is down.

```
#include <iostream>
#include <string>
using namespace std;
int main() {
string name, pass;
cout << "Name: ";
cin >> name;
cout << "Pass: ";
cin >> pass;
int sum = 0;
for (size_t i = 0; i < name.size(); i++) {
char c = name[i];
if (c < 'A') {
cout << "Lose: char is less than A" << endl;
return 1;
}
if (c > 'Z') {
sum += c - 32;
} else {
sum += c;
}
}
int r1 = 0x5678 ^ sum;
int r2 = 0;
for (size_t i = 0; i < pass.size(); i++) {
char c = pass[i];
c -= 48;
r2 *= 10;
r2 += c;
}
r2 ^= 0x1234;
cout << "r1: " << r1 << endl;
cout << "r2: " << r2 << endl;
if (r1 == r2) {
cout << "Win" << endl;
} else {
cout << "Lose: r1 and r2 don't match" << endl;
}
}
```

I got that code from the assembly of a binary, and while it may be wrong I want to focus on writing the solver. I'm starting with the first part, just calculating
`r1`

, and this is what I have:

```
from z3 import *
s = Solver()
sum = Int('sum')
name = Array('name', IntSort(), IntSort())
for c in name:
s.add(c < 65)
if c > 90:
sum += c - 32
else:
sum += c
r1 = Xor(sum, 0x5678)
print s.check()
print s.model()
```

All I'm asserting is that there are no letters less than 'A' in the array, so I expect to get back an array of any size that has numbers greater than 65.

Obviously this is completely wrong, mainly because it infinite loops. Also, I'm not sure I'm calculating sum correctly, because I don't know if it's initialized to 0. Could someone help figure out how to get this first loop working?

**EDIT:** I was able to get a z3 script that is close to the C++ code shown above:

```
from z3 import *
s = Solver()
sum = 0
name = Array('name', BitVecSort(32), BitVecSort(32))
i = Int('i')
for i in xrange(0, 1):
s.add(name[i] >= 65)
s.add(name[i] < 127)
if name[i] > 90:
sum += name[i] - 32
else:
sum += name[i]
r1 = sum ^ 0x5678
passwd = Array('passwd', BitVecSort(32), BitVecSort(32))
r2 = 0
for i in xrange(0, 5):
s.add(passwd[i] < 127)
s.add(passwd[i] >= 48)
c = passwd[i] - 48
r2 *= 10
r2 += c
r2 ^= 0x1234
s.add(r1 == r2)
print s.check()
print s.model()
```

This code was able to give me a correct username and password. However, I hardcoded the lengths of one for the username and five for the password. How would I change the script so I wouldn't have to hard code the lengths? And how would I generate a different solution each time I run the program?

Friday, November 28, 2014 | From
active questions tagged z3 - Stack Overflow

By some reasons I have to use C++ API and C API of Z3 together. In C++ API, reference counting of Z3 objects are well maintained and I needn't to worry about making mistakes. However I have to manually maintain reference counting for Z3 objects when I use
C API because C++ API uses `Z3_mk_context_rc`

to create the context. I have several problems on reference counting maintenance in Z3.

(1) If the reference counting of a `Z3_ast`

is reduced to 0, what is responsible to release the memory of this
`Z3_ast`

? And when?

(2) The code below

```
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
Z3_ast res = Z3_mk_eq(c,x,y);
#ifdef FAULT_CLAUSE
expr z = c.int_const("z");
expr u = c.int_const("u");
Z3_ast fe = Z3_mk_eq(c,z,u);
#endif
std::cout << Z3_ast_to_string(c,res) << std::endl;
}
void main()
{
config cfg;
cfg.set("MODEL", true);
cfg.set("PROOF", true);
context c(cfg);
rctry(c)；
}
```

Although I didn't increase reference count for AST referenced by `res`

, the program works well. If
`FAULT_CLAUSE`

is defined, program still works, but it will output ```
(= z u)
```

instead of `(= x y)`

. How to explain this?

Thank you!

Friday, November 28, 2014 | From
active questions tagged z3 - Stack Overflow

By some reasons I have to use C++ API and C API of Z3 together. In C++ API, reference counting of Z3 objects are well maintained and I needn't to worry about making mistakes. However I have to manually maintain reference counting for Z3 objects when I use
C API because C++ API uses `Z3_mk_context_rc`

to create the context. I have several problems on reference counting maintenance in Z3.

(1) If the reference counting of a `Z3_ast`

is reduced to 0, what is responsible to release the memory of this
`Z3_ast`

? And when?

(2) The code below

```
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
Z3_ast res = Z3_mk_eq(c,x,y);
#ifdef FAULT_CLAUSE
expr z = c.int_const("z");
expr u = c.int_const("u");
Z3_ast fe = Z3_mk_eq(c,z,u);
#endif
std::cout << Z3_ast_to_string(c,res) << std::endl;
}
void main()
{
config cfg;
cfg.set("MODEL", true);
cfg.set("PROOF", true);
context c(cfg);
rctry(c)；
}
```

Although I didn't increase reference count for AST referenced by `res`

, the program works well. If
`FAULT_CLAUSE`

is defined, program still works, but it will output ```
(= z u)
```

instead of `(= x y)`

. How to explain this?

Thank you!

Friday, November 28, 2014 | From
active questions tagged z3 - Stack Overflow

By some reasons I have to use C++ API and C API of Z3 together. In C++ API, reference counting of Z3 objects are well maintained and I needn't to worry about making mistakes. However I have to manually maintain reference counting for Z3 objects when I use
C API because C++ API uses `Z3_mk_context_rc`

to create the context. I have several problems on reference counting maintenance in Z3.

(1) If the reference counting of a `Z3_ast`

is reduced to 0, what is responsible to release the memory of this
`Z3_ast`

? And when?

(2) The code below

```
Z3_ast temp;
void rctry(context & c)
{
expr x = c.int_const("x");
expr y = c.int_const("y");
Z3_ast res = Z3_mk_eq(c,x,y);
temp = res;
#ifdef FAULT_CLAUSE
Z3_dec_ref(c, temp);
#endif
}
void main()
{
config cfg;
cfg.set("MODEL", true);
cfg.set("PROOF", true);
context c(cfg);
rctry(c);
std::cout << Z3_ast_to_string(c, temp) << std::endl;
}
```

Although I didn't increase reference count for AST referenced by `temp`

, the program works well. Even
`FAULT_CLAUSE`

is defined, program still works. How to explain?

Thursday, November 27, 2014 | From
active questions tagged z3 - Stack Overflow

Actually I am stucked by a problem which needs some details on Z3 solver's implementation:

**The objective:**

To have a function calculating the integer part of a real number. The return type must be a 'Real'. (for example, intpart(3.14) returns 3.0 or 3.00 whatever the precision).

The signature is therefore `(declare-func intpart((Real)) Real)`

**The constraint: (context)**

As far as I know the the theory Ints_Reals will lead to 'unknown' very easily, the choice i eager to make is to eliminate completely the usage of integer in the model, by using only either Bool or Real. I suppose this will reduce the possibility that the solver (whatever the standard one or the 'nlsat' one) returns 'unknown'.

**The problem I encountered:**

I tried firstly the embeded command 'to_int' and 'to_real':

```
(declare-fun intpart((Real i)) Real
(to_real (to_int i))
)
```

or directly

```
(declare-fun intpart((Real i)) Real
(to_real i)
)
```

(just because i found that it seems the 'to_real' also implicitly cut the fractional part)

but both of the two solutions will make the 'nlsat' solver directly into 'unknown' for a given non-linear real-only arithmetic system.

If i replace the function by

```
(declare-fun intpart((Real i)) Real
i
)
```

the 'nlsat' solver solve the problem very quickly and never give out 'unknown'. This seems to me that
**'to_int' or 'to_real' will implicitly engage the 'Ints' theory and therefore make the solver to undecidability**.

**Workaround exists, but not practical**

Of course since I note this problem, I begin to find some workaround. The only one I achieved is to use Fourier series of the 'floor' function. However the problem is that:

- Even when the sine function reaches the highest precision (10-12), the series must have at least k=1000 to retain a precision of (10-4), which is too expensive for the solver.
- Worse is that no native sine in Z3, which obligates me to have also a taylor series implementation of this function, which can only give a precision of (10-6) with tradeoff of performance.

So to sum up, the workaround works, but not useful at all because its unacceptable precision.

**So could anyone help ? Thanks in advance**

active questions tagged z3 - Stack Overflow News Feed

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