active questions tagged z3 - Stack Overflow News Feed 
Thursday, September 18, 2014  |  From active questions tagged z3 - Stack Overflow




Z3 now has a satisfiability engine for nonlinear real arithmetic based on cylindrical algebraic decomposition.



Is there any way to obtain the result of quantifier elimination, as opposed to mere satisfiability testing?



The following does not work:



from z3 import *
b,c,x = Reals('b c x')
f = Exists(x, b*x+c==0);
print Tactic('qe')(f).as_expr();


I would like to get something like Or(b!=0, And(b==0, c==0)).



Thanks.



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




I previously used Z3's API to define an enumerated type like so



let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|])


which enumerates the elements of a type T as being "a" "b" and "c" (and nothing else). However I am now trying to do something similar but via SMT-LIB rather than the API and I am running into a problem of Z3 complaining about quantifiers. The program I am using (Boogie) generates the following smt



...
(declare-sort T@T 0)
(declare-fun a() T@T)
(declare-fun b() T@T)
(declare-fun c() T@T)
(assert (forall ((x T@T) ) 
    (! (or
          (= x a)
          (= x b)
          (= x c)
       )
       :qid |gen.28:15|
       :skolemid |1|
     )))
...


The assertion is the type closure axiom that asserts that the type has no other members. But when I send this (along with other stuff) to Z3, after thinking about it a bit, returns



WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5
unknown
(:reason-unknown (incomplete quantifiers))


Notes: 1. I have MBQI turned on. 2. Boogie has an option called "z3types" but it doesn't seem to make any difference



What is the SMT-LIB equivalent of the MkEnumSort API call?



thanks



P.S. I have tried with RELEVANCY set to both 1 and 2 and I still get the warning about relevancy (CASE_SPLIT is set to 3)



Saturday, September 13, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3 as SAT solver for a tough satisfiability problem encoded in CNF/DIMACS format.



Would it make sense to randomize the input in order to increase the chance to find a solution:



  • Shuffle the order of CNF clauses
  • Sort/shuffle the numbering of input
    variables

Measurements (100 test runs per solver and sorting mode) for a smaller problem with Z3, Cryptominisat and Clasp:



enter image description here



For Z3, sorting/randomization does not look promising for my example which is probably not representative.



I have not found a random seed commandline parameter which influences the SAT module of Z3.
Parameter "random_seed" only seems to control the SMT solver.



Friday, September 12, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3 as SAT solver for a tough satisfiability problem encoded in CNF/DIMACS format.



Would it make sense to randomize the input in order to increase the chance to find a solution:



  • Shuffle the order of CNF clauses
  • Sort/shuffle the numbering of input
    variables

    (I have tried to put the primary input variables first - without visible effect)

I have not found a random seed commandline parameter which influences the SAT module of Z3.
Parameter "random_seed" only seems to control the SMT solver.



Wednesday, September 10, 2014  |  From active questions tagged z3 - Stack Overflow




Suppose I want to extract all sub-formulas(predicates, terms) from a given constraint with the type of BoolExpr and here are two examples:



(f(x)=2 and f(y)=3) or (f(z)=1 and f(y)=3)
The output should be f(x)=2, f(y)=3 and f(z)=1.

(p and q) or (p or r) and (p and (q or r))
The output should be p, q and r.


A naive way would be traversing the entire AST and recording all the unique sub-formulas. This is unpleasant when there are bunch of redundant nodes in the AST and we have to perform such extraction frequently.
I was wondering if there exists a clean and efficient way to do this.



I am using the Java API for Z3.



Wednesday, September 10, 2014  |  From active questions tagged z3 - Stack Overflow




Suppose I want to extract all sub-formulas(predicates, terms) from a given constraint with the type of BoolExpr and here are two examples:



(f(x)=2 and f(y)=3) or (f(z)=1 and f(y)=3)
The output should be f(x)=2, f(y)=3 and f(z)=1.

(p and q) or (p or r) and (p and (q or r))
The output should be p, q and r.


A naive way would be traversing the entire AST and recording all the unique sub-formulas. This is unpleasant when there are bunch of redundant nodes in the AST and we have to perform such extraction frequently.
I was wondering if there exists a clean and efficient way to do this.



I am using the Java API for Z3.



Tuesday, September 09, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3py and trying to get the set of all the variables in any constraint in a Solver. I can call Solver.assertions() to get an ASTVector, then loop over this vector and get objects of type BoolRef, for example, but then I'm stuck. How can I recursively iterate over an assertion, a BoolRef instance for example, to get the individual variables?



Tuesday, September 09, 2014  |  From active questions tagged z3 - Stack Overflow




I was looking at document of class expr of Z3 C++ API from following link
http://research.microsoft.com/en-us/um/redmond/projects/z3/classz3_1_1expr.html.



I found that for predicate operator such us ">" , ">=" and "<=", for bit vector it only performed signed operation. For example in operator ">=", source code is



{
        check_context(a, b);
        Z3_ast r;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_ge(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r =Z3_mk_bvsge(a.ctx(), a, b);//This statement only did signed version, there actually is a Z3_mk_bvuge in C API
        }
        else {
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
}


Does this mean if I want to distinguish between signed and unsigned operation I can only use C API?



Tuesday, September 09, 2014  |  From active questions tagged z3 - Stack Overflow




I was looking at document of class expr of Z3 C++ API from following link
http://research.microsoft.com/en-us/um/redmond/projects/z3/classz3_1_1expr.html.



I found that for predicate operator such us ">" , ">=" and "<=", for bit vector it only performed signed operation. For example in operator ">=", source code is



{
        check_context(a, b);
        Z3_ast r;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_ge(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r =Z3_mk_bvsge(a.ctx(), a, b);//This statement only did signed version, there actually is a Z3_mk_bvuge in C API
        }
        else {
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
}


Does this mean if I want to distinguish between signed and unsigned operation I can only use C API?



Friday, September 05, 2014  |  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).



Friday, September 05, 2014  |  From active questions tagged z3 - Stack Overflow




I have say 10 boolean variables. I want the model to be satisfiable if exactly 3 of them are true.



How would I encode this as a SAT problem? One way would to create the all the possible combinations and then or them together. Is there a better or more concise way to express this?



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




I have say 10 boolean variables. I want the model to be satisfiable if exactly 3 of them are true.



How would I encode this as a SAT problem? One way would to create the all the possible combinations and then or them together. Is there a better or more concise way to express this?



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




I have say 10 boolean variables. I want the model to be satisfiable if exactly 3 of them are true.



How would I encode this as a SAT problem? One way would to create the all the possible combinations and then or them together. Is there a better or more concise way to express this?



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




The problem in relational algebra REL051+1.p reads



  File     : REL051+1 : TPTP v6.1.0. Released v4.0.0.
% Domain   : Relation Algebra
% Problem  : Dense linear ordering


Using TPTP syntax with fof the corresponding code is



fof(f01,axiom,(
    ! [A] : o(A,A) )).

fof(f02,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ~ o(B,A) ) )).

fof(f03,axiom,(
    ! [A,B,C] :
      ( ( o(A,B)
        & o(B,C) )
     => o(A,C) ) )).

fof(f04,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ( o(A,f(A,B))
        & o(f(A,B),B) ) ) )).

fof(f05,axiom,(
    ! [A,B] :
      ( f(A,B) != A
      & f(A,B) != B ) )).

fof(f06,axiom,(
    ! [A,B] :
      ( o(A,B)
      | o(B,A) ) )).


As you can see in TPTP all ATPs are not able to prove such problem.



This theorem was proved with Z3 using the following SMT-LIB



(declare-sort S)
(declare-fun o (S S) Bool)
(declare-fun f (S S) S)
(assert (forall ((A S)) (o A A) ))
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (not (o B A)))   ) )
(assert (forall ((A S) (B S) (C S)) (implies (and (o A B) (o B C)) 
                                             (o A C))   ) )
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (and (o A (f A B)) (o (f A B) B)))   ) )
(declare-fun B () S)
(assert (forall ((A S)) (and (distinct (f A B) A) 
                                   (distinct (f A B) B))    ) )

(assert (forall ((A S)) (or (o A B) (o B A)) ) )

(check-sat)


and the corresponding output is



sat


My question is: The proof with Z3 is correct?



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




I was trying out the PDR engine in Z3 and I'm not sure which version of Z3 to use.



The "official" master branch from git seems to work but is dated Nov 2012. I'm sure there have been improvements since then. The unstable branch, on the other hand, "may contain unstable and/or untested code", which seems to be true.



What would be the most recent "stable" version of the engine?



For example



(declare-rel R (Real Real))
(declare-var x Real)
(declare-var y Real)

(rule 
  (=> (and (= x 0) (= y 0)) (R x y)) 
)

(rule 
  (=> (R x y) (R (+ x 1) (+ y 1)))
)

(query 
  (and (R x y) (not (= x y)))
)


Above works in master, returning unsat, but in the unstable branch the engine wanders off not solving the problem. Same holds for the example from a recent CAV paper.



Monday, September 01, 2014  |  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).



Sunday, August 31, 2014  |  From active questions tagged z3 - Stack Overflow




I'm working on a Python project, where I'm currently trying to speed things up in some horrible ways: I set up my Z3 solvers, then I fork the process, and have Z3 perform the solve in the child process and pass a pickle-able representation of the model back to the parent.



This works great, and represents the first stage of what I'm trying to do: the parent process is now no longer CPU-bound. The next step is to multi-thread the parent, so that we can solve multiple Z3 solvers in parallel.



I'm pretty sure I've mutexed away any concurrent accesses of Z3 in the setup phase, and only one thread should be touching Z3 at any one time. However, despite this, I'm getting random segfaults in libz3.so. It's important to note, at this point, that it's not always the same thread that touches Z3 -- the same object (not the solvers themselves, but the expressions) might be handled by different threads at different times.



My question is, is it possible to multi-thread Z3? There is a brief note here (http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html) saying "It is not safe to access Z3 objects from multiple threads.", which I guess would answer my question, but I'm holding out hope that it means to say that one shouldn't access Z3 from multiple threads simultaneously. Another resource (Again: Installing Z3 + Python on Windows) states, from Leonardo himself, that "Z3 uses thread local storage", which, I guess, would sink this whole undertaking, but a) that answer is from 2012, so maybe things have changed, and b) maybe it uses thread-local storage for some unrelated stuff?



Anyways, is multi-threading Z3 possible (from Python)? I'd hate to have to push the setup phase into the child processes...



Sunday, August 31, 2014  |  From active questions tagged z3 - Stack Overflow




The problem in relational algebra REL052+1.p reads



File     : REL052+1 : TPTP v6.1.0. Released v4.0.0.
% Domain   : Relation Algebra
% Problem  : Non-discrete dense ordering


Using TPTP syntax with fof the corresponding code is



fof(f01,axiom,(
    ! [A] : o(A,A) )).

fof(f02,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ~ o(B,A) ) )).

fof(f03,axiom,(
    ! [A,B,C] :
      ( ( o(A,B)
        & o(B,C) )
     => o(A,C) ) )).

fof(f04,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ( o(A,f(A,B))
        & o(f(A,B),B) ) ) )).

fof(f05,axiom,(
    ! [A,B] :
      ( f(A,B) != A
      & f(A,B) != B ) )).

fof(f06,axiom,(
    ? [A,B] :
      ( o(A,B)
      & A != B ) )).


As you can see in TPTP all ATPs are not able to prove such problem.



This theorem was proved with Z3 using the following SMT-LIB



(declare-sort S)
(declare-fun o (S S) Bool)
(declare-fun f (S S) S)
(assert (forall ((A S)) (o A A) ))
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (not (o B A)))   ) )
(assert (forall ((A S) (B S) (C S)) (implies (and (o A B) (o B C)) 
                                             (o A C))   ) )
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (and (o A (f A B)) (o (f A B) B)))   ) )
(declare-fun B () S)
(assert (forall ((A S)) (and (distinct (f A B) A) 
                                   (distinct (f A B) B))    ) )
(assert (exists ((X S) (Y S)) (and (o X Y) (distinct X Y))) )

(check-sat)


and the corresponding output is



sat


My question is: The proof with Z3 is correct?



Friday, August 29, 2014  |  From active questions tagged z3 - Stack Overflow




I was trying out the PDR engine in Z3 and I'm not sure which version of Z3 to use.



The "official" master branch from git seems to work but is dated Nov 2012. I'm sure there have been improvements since then. The unstable branch, on the other hand, "may contain unstable and/or untested code", which seems to be true.



What would be the most recent "stable" version of the engine?



For example



(declare-rel R (Real Real))
(declare-var x Real)
(declare-var y Real)

(rule 
  (=> (and (= x 0) (= y 0)) (R x y)) 
)

(rule 
  (=> (R x y) (R (+ x 1) (+ y 1)))
)

(query 
  (and (R x y) (not (= x y)))
)


Above works in master, returning unsat, but in the unstable branch the engine wanders off not solving the problem. Same holds for the example from a recent CAV paper.



Thursday, August 28, 2014  |  From active questions tagged z3 - Stack Overflow




I tried around a some time to get a rather simple requirement done:
I declared a new datatype



(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))



where key should act like a primary key in a database, i.e., each different instance of A should have a different key value.
The container of the different instances (functions) looks like the following:



(declare-const A_instances (Array Int A))



So far so good. I tried to create an assertion, such that all instances in A_instances have a different key field. Thus, for each index i in A_instances (key (select A_instances i)) should be distinct. However it returns unknown.



Someone has any suggestions?



 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.