active questions tagged z3 - Stack Overflow News Feed 
Tuesday, February 9, 2016  |  From active questions tagged z3 - Stack Overflow




Given the following code:



from z3 import *
a,b,c = BitVecs('a b c', 32)
f1 = Exists([a, b, c], And(a + b == c, a < b, c == 1337))
f2 = And(a + b == c, a < b, c == 1337)
prove(f1 == f2)


I would assume that z3 implicitly existential quantifies a, b and c, in this example. Why aren't the two formulas equal, what is the difference?



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




I'm currently working on a model counting approach with the SMT solver Z3. Does anyone know how Z3 does generate the models for e.g. the sort of linear arithmetics (LIA)? Which algorithm is used and where can I find the source code for that algorithm?



Thanks,
Yannic



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




When I run Z3's JavaExample.java to test the java bindings, I get the following error:



Exception in thread "main" java.lang.UnsatisfiedLinkError:Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\git\z3\build\libz3java.dll: The operating system cannot run %1
    at java.lang.ClassLoader$NativeLibrary.load(Native Method)
    at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1938)
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1854)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at com.microsoft.z3.Native.<clinit>(Native.java:14)
    at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
    at JavaExample.main(JavaExample.java:2347)


What could be causing this?



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




Given the following code:



from z3 import *
a,b,c = BitVecs('a b c', 32)
f1 = Exists([a, b, c], And(a + b == c, a < b, c == 1337))
f2 = And(a + b == c, a < b, c == 1337)
prove(f1 == f2)


I would assume that z3 implicitly existential quantifies a, b and c, in this example. Why aren't the two formulas equal, what is the difference?



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




I am trying to use Z3's java binding, particularly trying to run the Java example JavaExample.java that's distributed in Z3's 4.4.2 version.



JavaExample.java was compiling fine when I was using the 4.4.2 com.microsoft.z3.jar file. However, it would not run because the default libz3java.dll was 32-bit and my environment is 64-bit. I tried building a 64-bit Z3 with the -x flag for its Makefile maker scripts/mk_make.py but that generated an error when I ran nmake (posted about that here).



Anyway, I then downloaded the binary for Z3 4.3.2 version, which contained a 64-bit libz3java.dll. However, now JavaExample.java doesn't compile, generating a ton of errors, such as:



FiniteDomainNum cannot be resolved to a type    Z3Example.java  line 2222


for line



FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s);


There are hundreds of such errors.



The jar file is properly included in the Eclipse project, just like the 4.4.2 was when JavaExample.java was compiling.



Any help on getting this going? Thanks.



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




I am running JavaExample.java provided with Z3 4.4.2 but I get the following output and then error:



Z3 Major Version: 4
Z3 Full Version: 4.3.2.0
SimpleExample
Opt
Exception in thread "main" java.lang.UnsatisfiedLinkError: com.microsoft.z3.Native.INTERNALmkOptimize(J)J
    at com.microsoft.z3.Native.INTERNALmkOptimize(Native Method)
    at com.microsoft.z3.Native.mkOptimize(Native.java:5208)
    at com.microsoft.z3.Optimize.<init>(Optimize.java:262)
    at com.microsoft.z3.Context.mkOptimize(Context.java:3043)
    at Z3Example.optimizeExample(Z3Example.java:2323)
    at Z3Example.main(Z3Example.java:2362)


To be fair, I am using the 64-bit libz3java.dll provided with 4.3.2, while using the jar file com.microsoft.z3.jar from version 4.4.2, because that was the only combination that I managed to get working (this details those problems). Could that be the version difference the reason for this error, or is there something else?



Monday, February 8, 2016  |  From active questions tagged z3 - Stack Overflow




I followed the instructions to build Z3 on a 64-bit Windows 8.1 system with Visual Studio Community 2015 by running



python scripts/mk_make.py -x


but when I run nmake, I get the following error:



C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8848): error C3861:
 '_InterlockedIncrement64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8879): error C3861:
 '_InterlockedDecrement64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8915): error C3861:
 '_InterlockedExchange64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8969): error C3861:
 '_InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(8979): error C3861:
 '_InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(9026): error C3861:
 '_InterlockedAnd64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(9036): error C3861:
 '_InterlockedOr64': identifier not found
C:\Program Files (x86)\Windows Kits\8.1\include\um\winbase.h(9046): error C3861:
 '_InterlockedXor64': identifier not found
NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 14.0
\VC\BIN\cl.EXE"' : return code '0x2'
Stop.


Any idea on how to fix this?



Friday, February 5, 2016  |  From active questions tagged z3 - Stack Overflow




I'm currently working on a model counting approach with the SMT solver Z3. Does anyone know how Z3 does generate the models for e.g. the sort of linear arithmetics (LIA)? Which algorithm is used and where can I find the source code for that algorithm?



Thanks,
Yannic



Friday, February 5, 2016  |  From active questions tagged z3 - Stack Overflow




I try to use the z3 solver for a minimization problem. I was trying to get a timeout, and return the best solution so far. I use the python API, and the timeout option "smt.timeout" with



set_option("smt.timeout", 1000) # 1s timeout


This actually times out after about 1 second. However a larger timeout does not provide a smaller objective. I ended up turning on the verbosity with



set_option("verbose", 2)


And I think that z3 successively evaluates larger values of my objective, until the problem is satisfiable:



(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...


I thus have the two questions:



  • Can I on contrary tell z3 to start with the upper bound, and successively return models with a smaller value for my objective function (just like for instance Minizinc annotations indomain_max http://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html)
  • It still looks like the solver returns a satisfiable instance of my problem. How is it found? If it's trying to evaluates larger values of my objective successively, it should not have found a satisfiable instance yet when the timeout occurs...

edit: In the opt.maxres log, the upper bound never shrinks.



For the record, I found a more verbose description of the options in the source here opt_params.pyg



Wednesday, February 3, 2016  |  From active questions tagged z3 - Stack Overflow




This is a simplified code using the similar implementation idea as the z3py code for another problem I am trying to solve which is more complex and takes about 1 minute to run.



The intuition of the following code is to translate the array of integers in the inputArray into the array of months defined as EnumSort, which is essentially to infer the model of monthArray.



from z3 import *
s = Solver()

Month,(Jan,Feb,Mar,Apr,May,Jun,Jul,Aug,Sep,Oct,Nov,Dec)=EnumSort('Month',['Jan','Feb','Mar','Apr','May','Jun','Jul','Aug','Sep','Oct','Nov','Dec'])
monthArray = Array('monthArray',IntSort(), Month)
inputArray = Array('inputArray',IntSort(),IntSort())
tempArray = Array('tempArray',IntSort(),IntSort())

intArray = [1,3,6,7,8,3,5,6,3,12,11,5,2,5,7,3,7,3,2,7,12,4,5,1,10,9]
for idx,num in enumerate(intArray):
    tempArray = Store(tempArray,idx,num)

s.add(inputArray==tempArray)

length = Int('length')
s.add(length == len(intArray))
i = Int('i')
s.add(ForAll(i,Implies(And(i>=0,i<length),And(
    Implies(inputArray[i]==1,monthArray[i]==Jan),
    Implies(inputArray[i]==2,monthArray[i]==Feb),
    Implies(inputArray[i]==3,monthArray[i]==Mar),
    Implies(inputArray[i]==4,monthArray[i]==Apr),
    Implies(inputArray[i]==5,monthArray[i]==May),
    Implies(inputArray[i]==6,monthArray[i]==Jun),
    Implies(inputArray[i]==7,monthArray[i]==Jul),
    Implies(inputArray[i]==8,monthArray[i]==Aug),
    Implies(inputArray[i]==9,monthArray[i]==Sep),
    Implies(inputArray[i]==10,monthArray[i]==Oct),
    Implies(inputArray[i]==11,monthArray[i]==Nov),
    Implies(inputArray[i]==12,monthArray[i]==Dec)
    ))))

print s.check()
print s.model()


Could anyone give me some suggestions about the ways to improve the time efficiency using this code as an example? Thanks.



Edit:
SMT language output by calling Solver.to_smt2()



(set-info :status unknown)
(declare-datatypes () ((Month (Jan ) (Feb ) (Mar ) (Apr ) (May ) (Jun ) (Jul ) (Aug ) (Sep ) (Oct ) (Nov ) (Dec ))))
(declare-fun inputArray () (Array Int Int))
(declare-fun length () Int)
(declare-fun monthArray () (Array Int Month))
(assert
(= (select inputArray 0) 1))
(assert
(= (select inputArray 1) 3))
(assert
(= (select inputArray 2) 6))
(assert
(= (select inputArray 3) 7))
(assert
(= (select inputArray 4) 8))
(assert
(= (select inputArray 5) 3))
(assert
(= (select inputArray 6) 5))
(assert
(= (select inputArray 7) 6))
(assert
(= (select inputArray 8) 3))
(assert
(= (select inputArray 9) 12))
(assert
(= (select inputArray 10) 11))
(assert
(= (select inputArray 11) 5))
(assert
(= (select inputArray 12) 2))
(assert
(= (select inputArray 13) 5))
(assert
(= (select inputArray 14) 7))
(assert
(= (select inputArray 15) 3))
(assert
(= (select inputArray 16) 7))
(assert
(= (select inputArray 17) 3))
(assert
(= (select inputArray 18) 2))
(assert
(= (select inputArray 19) 7))
(assert
(= (select inputArray 20) 12))
(assert
(= (select inputArray 21) 4))
(assert
(= (select inputArray 22) 5))
(assert
(= (select inputArray 23) 1))
(assert
(= (select inputArray 24) 10))
(assert
(= (select inputArray 25) 9))
(assert
(= length 26))
(assert
(forall ((i Int) )(let (($x172 (=> (= (select inputArray i) 12) (= (select monthArray i) Dec))))
(let (($x175 (=> (= (select inputArray i) 11) (= (select monthArray i) Nov))))
(let (($x178 (=> (= (select inputArray i) 10) (= (select monthArray i) Oct))))
(let (($x181 (=> (= (select inputArray i) 9) (= (select monthArray i) Sep))))
(let (($x184 (=> (= (select inputArray i) 8) (= (select monthArray i) Aug))))
(let (($x187 (=> (= (select inputArray i) 7) (= (select monthArray i) Jul))))
(let (($x190 (=> (= (select inputArray i) 6) (= (select monthArray i) Jun))))
(let (($x193 (=> (= (select inputArray i) 5) (= (select monthArray i) May))))
(let (($x196 (=> (= (select inputArray i) 4) (= (select monthArray i) Apr))))
(let (($x199 (=> (= (select inputArray i) 3) (= (select monthArray i) Mar))))
(let (($x202 (=> (= (select inputArray i) 2) (= (select monthArray i) Feb))))
(let (($x205 (=> (= (select inputArray i) 1) (= (select monthArray i) Jan))))
(=> (and (>= i 0) (< i length)) (and $x205 $x202 $x199 $x196 $x193 $x190 $x187 $x184 $x181 $x178 $x175 $x172)))))))))))))))
)
(check-sat)


Tuesday, February 2, 2016  |  From active questions tagged z3 - Stack Overflow




My apologies if this question is ill-phrased but I'm trying to use z3 (in python with the language binding) to solve some nonlinear equations, but unfortunately neither the qfnra-nlsat nor the general solver could solve the following system unless a, b and c are all given:



    y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002 
    y > 0.0


I tried with the following tactic:



    t = z3.Then('simplify', 'qfnra-nlsat')


and I also tried substituting the nonlinear parts with some intermediate names and add the exponential parts back in later with incremental solver using push(). But z3 basically gets stuck (longer than 1 hour as far as I tried) in both cases.



I'm a newbie to CSP and the theoretical background involved, sorry if this is a dumb question but I'm wondering if such nonlinearity is beyond (empirically) solvable by z3 or I'm not using it correctly? Thanks!



Edit:



Here's the python code that fails on my machine:



    import z3
    a = z3.Real('a')
    b = z3.Real('b')
    c = z3.Real('c') 
    y = z3.Real('y')

    eq = [ 
        y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002,
        y >= 0.0 
    ]

    t = z3.Then('simplify', 'qfnra-nlsat')
    s = t.solver()
    s.add(eq)
    r = s.check()
    print r
    m = s.model()
    print m


Here's the output:



    unknown
    [y = 1/500 ]


Edit:



It seems that the latest code from z3 git repo is kinda broken. I tried with 4.4.1 release and it all worked out.



A follow up question though, if I just add one more constraint below:



    a == 16.0


And z3 gets stuck, which I could not understand...It seems that the additional constraint above is pretty trivial, an initial guess of b and c being both 1s should solve the system, but I guess that's not how z3 works? Any idea on how to solve the system with this new constraint?



Monday, February 1, 2016  |  From active questions tagged z3 - Stack Overflow




I used ParseSMTLIB2File to parse an smt2 file Context.smt2 which has declarations of datatypes, constants, and functions; e.g.



    ; Sort Declarations
    (declare-sort tla_sort_Str)
    (declare-const x tla_sort_Str)
    (declare-const y tla_sort_Str)
    (declare-const z tla_sort_Str)


And then, I used ParseSMTLIB2String to parse a string "(assert (= x y))". The following is my code:



     BoolExpr expr = ctx.parseSMTLIB2File("Context.smt2", null, null, null, null);
     String str = "(assert (= x y))";
     BoolExpr assert = ctx.parseSMTLIB2String(str, null, null, null, null);


Unfortunately, I received an error. I guess the reason is that ctx doesn't know what tla_sort_Str, x and y are. If no, how can I pass information in Context.smt2 to parseSMTLIB2String? Thank you very much.



Monday, February 1, 2016  |  From active questions tagged z3 - Stack Overflow




Is there a z3 c++ api for direct query of a theory decision procedure?



Meaning, given a set of theory predicates, I would like to check whether they are conflicting in some given theory, without calling the z3 prover on their conjunction.



For example, I would like to check whether the following set of predicates in equality logic are conflicting:
x=y, y=z, x!=z



Monday, February 1, 2016  |  From active questions tagged z3 - Stack Overflow




I am trying to use Z3 C++ API to perform a projection operation on a system of linear inequalities. The projection will give back a system of linear inequalities (on real numbers). I understand that this is what Fourier-Motzkin elimination algorithm does, and Z3 has an implementation of this algorithm. I have tried using



expr qf = ..; //system of linear inequalities with existential quantifiers
goal g(qf);
tactic qe_tac = tactic(c, "qe"); // quantifier elimination
apply_result r = qe_tac(g);
goal result_goal = r[0];
std::cout << "result_goal: " << result_goal.as_expr() << std::endl;


The good news is that this outputs an expression which has no quantifiers. The bad news is that it is not a system of linear inequalities as it contains some disjunctions. For example, for the simple formula:
$\exists a. x1 <= a && a <= x2$, I get the following output:



Quantified formula2:(exists ((a1 Real)) (and (<= x1 a) (<= a x2)))
result_goal2: (let ((a!1 (not (<= 0.0 (+ x1 (* (- 1.0) x2))))))
(or (<= (+ x1 (* (- 1.0) x2)) 0.0) a!1))


I have tried "fm" tactic, but that doesn't do any quantifier elimination. I have also tried "qe" tactic in conjunction with the "simplify" tactic but the result goal still has disjunctions. Is there a method to get the result goal as a system of linear inequalities?



Monday, February 1, 2016  |  From active questions tagged z3 - Stack Overflow




My apologies if this question is ill-phrased but I'm trying to use z3 (in python with the language binding) to solve some nonlinear equations, but unfortunately neither the qfnra-nlsat nor the general solver could solve the following system unless a, b and c are all given:



    y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002 
    y > 0.0


I tried with the following tactic:



    t = z3.Then('simplify', 'qfnra-nlsat')


and I also tried substituting the nonlinear parts with some intermediate names and add the exponential parts back in later with incremental solver using push(). But z3 basically gets stuck (longer than 1 hour as far as I tried) in both cases.



I'm a newbie to CSP and the theoretical background involved, sorry if this is a dumb question but I'm wondering if such nonlinearity is beyond (empirically) solvable by z3 or I'm not using it correctly? Thanks!



Sunday, January 31, 2016  |  From active questions tagged z3 - Stack Overflow




I don't understand the meaning of the underscore, e.g. in these (unrelated) expressions



[source]



(display (_ bv20 8))
(declare-const x (_ BitVec 64))


or this:



(declare-fun a () (Array (_ BitVec 32) (_ BitVec 7)))


[source]



What does the "_" mean?



Friday, January 29, 2016  |  From active questions tagged z3 - Stack Overflow




My apologies if this question is ill-phrased but I'm trying to use z3 (in python with the language binding) to solve some nonlinear equations, but unfortunately neither the qfnra-nlsat nor the general solver could solve the following system unless a, b and c are all given:



    y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002 
    y > 0.0


I tried with the following tactic:



    t = z3.Then('simplify', 'qfnra-nlsat')


and I also tried substituting the nonlinear parts with some intermediate names and add the exponential parts back in later with incremental solver using push(). But z3 basically gets stuck (longer than 1 hour as far as I tried) in both cases.



I'm a newbie to CSP and the theoretical background involved, sorry if this is a dumb question but I'm wondering if such nonlinearity is beyond (empirically) solvable by z3 or I'm not using it correctly? Thanks!



Wednesday, January 27, 2016  |  From active questions tagged z3 - Stack Overflow




I used ParseSMTLIB2File to parse an smt2 file Context.smt2 which has declarations of datatypes, constants, and functions; e.g.



    ; Sort Declarations
    (declare-sort tla_sort_Str)
    (declare-const x tla_sort_Str)
    (declare-const y tla_sort_Str)
    (declare-const z tla_sort_Str)


And then, I used ParseSMTLIB2String to parse a string "(assert (= x y))". The following is my code:



     BoolExpr expr = ctx.parseSMTLIB2File("Context.smt2", null, null, null, null);
     String str = "(assert (= x y))";
     BoolExpr assert = ctx.parseSMTLIB2String(str, null, null, null, null);


Unfortunately, I received an error. I guess the reason is that ctx doesn't know what tla_sort_Str, x and y are. If no, how can I pass information in Context.smt2 to parseSMTLIB2String? Thank you very much.



Tuesday, January 26, 2016  |  From active questions tagged z3 - Stack Overflow




There are many references made to a tool for debugging Z3 traces called the "Z3 Axiom Profiler". I have found code which is part of the VCC project, that appears to be the axiom profiler and is three years old. Is building from these VCC sources the correct way to obtain the profiler, or is there a more recent version somewhere?



Monday, January 25, 2016  |  From active questions tagged z3 - Stack Overflow




I have worked on a 5-valued propositional logic, where there exists five instead of just two truth values, and I would like to use Z3 to reason about this logic.



For the sake of simplicity, assume that the truth values are elements of the set {0,...,4} (this is actually a simplification, but should suffice to illustrate my question), which is equipped with the natural order on these elements. Since this logic is no longer binary, operators need to be defined differently, obviously. Examples of the operators are as follows:



  • a and b = min{a, b}
  • a or b = max{a, b}
  • not a = 4 - a

Now, I would like to use Z3 to reason about (quantifier free) formulas in this logic, such as a or (not b). However, I don't know what (a) the simplest and (b) the most efficient way would be to teach Z3 this.



I guess one straightforward solution would be to use enumeration sorts (although I did not yet manage to define them without getting an error) to model the truth values and macros to define the operators. Would that be the route to go?



 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.