active questions tagged z3 - Stack Overflow News Feed 
Friday, February 27, 2015  |  From active questions tagged z3 - Stack Overflow




When reasoning about polynomial inequalities, Z3 seems to have to first transform the polynomial into monomial form. I'm wondering if there's a setting in the solver that let me define the monomial degree I want my polynomials to be transformed to?



I'm using the z3py interface and I can't find it by searching online.



Thursday, February 26, 2015  |  From active questions tagged z3 - Stack Overflow




I am planning to do some work with the Z3 SMT solver from Microsoft Research that will run on a compute server with an execution time limit. I expect that the job will exceed this limit. The recommended policy for this computing center is to use "checkpoints" and to invoke a series of jobs, each of which picks up the checkpoint from the previous job and continues working. In this way, no process runs for more than the execution time limit, so other users have a chance to run their jobs too, but the total amount of compute time used can exceed the timeout for a single job.



Does Z3 have support for reading and writing checkpoints?



By "checkpoint", I mean a file that serializes (some part of) the internal state of the Z3 solver, such that if the Z3 process writes a checkpoint and exits, and then a second Z3 process is started that reads the checkpoint file, after reading it back the state of the new Z3 process is identical to the state of the previous process (so the solver doesn't start again, but continues solving from where it left off).



As an alternative, instead of checkpointing the entire solver, is it possible to read the database of learned clauses (or other inference databases built internally by Z3)? This could make it possible to do a form of checkpointing by augmenting the input file with learned clauses, although it might not be as efficient as a "real" checkpoint of the entire internal state.



Wednesday, February 25, 2015  |  From active questions tagged z3 - Stack Overflow




I am planning to do some work with the Z3 SMT solver from Microsoft Research that will run on a compute server with an execution time limit. I expect that the job will exceed this limit. The recommended policy for this computing center is to use "checkpoints" and to invoke a series of jobs, each of which picks up the checkpoint from the previous job and continues working. In this way, no process runs for more than the execution time limit, so other users have a chance to run their jobs too, but the total amount of compute time used can exceed the timeout for a single job.



Does Z3 have support for reading and writing checkpoints?



By "checkpoint", I mean a file that serializes (some part of) the internal state of the Z3 solver, such that if the Z3 process writes a checkpoint and exits, and then a second Z3 process is started that reads the checkpoint file, after reading it back the state of the new Z3 process is identical to the state of the previous process (so the solver doesn't start again, but continues solving from where it left off).



As an alternative, instead of checkpointing the entire solver, is it possible to read the database of learned clauses (or other inference databases built internally by Z3)? This could make it possible to do a form of checkpointing by augmenting the input file with learned clauses, although it might not be as efficient as a "real" checkpoint of the entire internal state.



Monday, February 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Edit:



My code is as follows:



from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()


It returns



sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]


I don't understand what I, O, elem!0, elem!1 and k!4 mean and this is clearly not what I expected.



Monday, February 23, 2015  |  From active questions tagged z3 - Stack Overflow




I'm trying to use Why3's Z3 back-end in order to retrieve models that can then be used to derive test cases exhibiting bugs in programs. However, Z3 version 4.3.2 seems unable to answer sat for any Why3 goal. It looks like some of the axiomatic definitions used by Why3 somehow confuse Z3. For instance, the following example (which is a tiny part of what Why3 generates)



(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)


results in timeout with the following command line:



z3 -smt2 model.partial=true file.smt2 -T:10


On the other hand, changing the definition to



(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))


will get me a model (which looks pretty reasonable)



(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)


but if I try to add the next axiom present in the original Why3 file, namely



;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))


again Z3 answers timeout.



Is there something I'm missing in the configuration of Z3? Moreover, in previous versions of Why3, there was an option MODEL_ON_TIMEOUT, which allowed to retrieve a model in such circumstances. Even though there was no guarantee that this was a real model since Z3 could not finish to check it, in practice such models generally contained all the information I needed. However, I haven't found a similar option in 4.3.2. Does it still exist?



Update The last axiom Abs_pos was wrong (I toyed a bit with Why3's output before posting here and ended up pasting an incorrect version of the issue). This is now fixed.



Monday, February 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



My code is as follows:



from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()


It returns



sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]


I don't understand what I, O, elem!0, elem!1 and k!4 mean and this is clearly not what I expected.



Monday, February 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



My code is as follows:



from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()


It returns



sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]


I don't understand what I, O, elem!0, elem!1 and k!4 mean and this is clearly not what I expected.



Monday, February 23, 2015  |  From active questions tagged z3 - Stack Overflow




I'm trying to use Why3's Z3 back-end in order to retrieve models that can then be used to derive test cases exhibiting bugs in programs. However, Z3 version 4.3.2 seems unable to answer sat for any Why3 goal. It looks like some of the axiomatic definitions used by Why3 somehow confuse Z3. For instance, the following example (which is a tiny part of what Why3 generates)



(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)


results in timeout with the following command line:



z3 -smt2 model.partial=true file.smt2 -T:10


On the other hand, changing the definition to



(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))


will get me a model (which looks pretty reasonable)



(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)


but if I try to add the next axiom present in the original Why3 file, namely



(assert
  (not (forall ((x Int)) (<= 0 (abs1 x)))))


again Z3 answers timeout.



Is there something I'm missing in the configuration of Z3? Moreover, in previous versions of Why3, there was an option MODEL_ON_TIMEOUT, which allowed to retrieve a model in such circumstances. Even though there was no guarantee that this was a real model since Z3 could not finish to check it, in practice such models generally contained all the information I needed. However, I haven't found a similar option in 4.3.2. Does it still exist?



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



My code is as follows:



from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()


It returns



sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]


I don't understand what I, O, elem!0, elem!1 and k!4 mean and this is clearly not what I expected.



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I'm not sure about how to create a new datatype by using the command:



(declare-datatypes () ((Name val1 val2 val3))) 


for example here I want for val1 and val2 to be letters, namely "s" and "e", and I want val3 to be an integer, I have tried to write this:



(declare-datatypes () ((M s e Int))) 


but It doesn't work, it says:




invalid datatype declaration.


Any thoughts?
Thanks.



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Sunday, February 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Friday, February 20, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Friday, February 20, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0&lt;=x&lt;k, O[x] = I[x] ) and (ForAll k&lt;=x&lt;length(I)-1, O[x] = I[x+1]) is true


Should I use Array or IntVector, or anything else to represent the input/output array?



Friday, February 20, 2015  |  From active questions tagged z3 - Stack Overflow




I am new to z3py and SMT and I haven't found a good tutorial about z3py.



Here is my problem setting:



Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].



I want to infer k for the operator Delete, which deletes the element at position k in an array, where



Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true



Should I use Array or IntVector, or anything else to represent the input/output array?



Thanks in advance!



Thursday, February 19, 2015  |  From active questions tagged z3 - Stack Overflow




After reading the strategies guide of Z3, and this answer by Leo, I expected that (check-sat) and (check-sat-using smt) are equivalent. However, when running Z3 4.3.2 three times against our test suite (230 SMTLIB2 files), it took 198s/192s/195s seconds with (check-sat), but 275s/283s/270s with (check-sat-using smt). I also tried the nightly build Z3 4.4.0 d3fb5f2a4cda, and the difference was similar.



Why might that be?



A bit more information that might be relevant:



  • Windows 7 x64, Z3 x64
  • All our tests are configured with auto_config false and smt.mbqi false
  • All use quantifiers and uninterpreted functions
  • Some use (non-linear) int and/or real arithmetic
  • All make heavy use of push-pop blocks

Edit: What I ultimately would like to do is to set a timeout for some check-sat calls, but not for all. AFAIK, this is not possible with check-sat itself, but check-sat-using (using-params smt :soft_timeout $timeout) should work. Is that right?



Wednesday, February 18, 2015  |  From active questions tagged z3 - Stack Overflow




After reading the strategies guide of Z3, and this answer by Leo, I expected that (check-sat) and (check-sat-using smt) are equivalent. However, when running Z3 4.3.2 three times against our test suite (230 SMTLIB2 files), it took 198s/192s/195s seconds with (check-sat), but 275s/283s/270s with (check-sat-using smt). I also tried the nightly build Z3 4.4.0 d3fb5f2a4cda, and the difference was similar.



Why might that be?



A bit more information that might be relevant:



  • Windows 7 x64, Z3 x64
  • All our tests are configured with auto_config false and smt.mbqi false
  • All use quantifiers and uninterpreted functions
  • Some use (non-linear) int and/or real arithmetic
  • All make heavy use of push-pop blocks

Wednesday, February 18, 2015  |  From active questions tagged z3 - Stack Overflow




After reading the strategies guide of Z3, and this answer by Leo, I expected that (check-sat) and (check-sat-using smt) are equivalent. However, when running Z3 4.3.2 three times against our test suite (230 SMTLIB2 files), it took 198s/192s/195s seconds with (check-sat), but 275s/283s/270s with (check-sat-using smt). I also tried the nightly build Z3 4.4.0 d3fb5f2a4cda, and the difference was similar.



Why might that be?



A bit more information that might be relevant:



  • Windows 7 x64, Z3 x64
  • All our tests are configured with auto_config false and smt.mbqi false
  • All use quantifiers and uninterpreted functions
  • Some use (non-linear) int and/or real arithmetic
  • All make heavy use of push-pop blocks

 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.