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.Ints.



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:



  1. 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.
  2. 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

Comments

No comments yet.