active questions tagged z3  Stack Overflow News Feed
I have a question about the Z3/SMTLib API.
The key SMT subroutine required by the liquidtypes
tools is the following query:
INPUT: A "background" formula P
, A list of "goal" formulas Qs = [Q1,...,Qn]
OUTPUT: Largest Qs' \subset Qs s.t. forall Q in Qs', P => Q.
Currently, we compute this in the obvious fashion:
def query1(P, Qs):
Qs' := []
ASSERT(P)
for Q in Qs:
PUSH()
ASSERT (not Q)
if CHECKUNSAT():
Qs'.add(Q)
POP()
return Qs'
My question: is there some faster way to do via MaxSAT?
def query2(P, Qs):
F = (Hard P) /\ ((Soft ~Q1) \/ ... \/ (Soft ~QN))
Rs = MaxSat(F)
Qs' = Qs  Rs
return Qs'
That is Hard
means you must satisfy P
and
Soft
means that maximize the number of ~Qi
that can also
be satisfied. Specifically,
 Is there an API that would let me do the above?
 Would
query2
be faster than the loop in query1
above?
The title says it all. I try to present 1 as the following: (_ bv1 32)
, and z3 complains.
How do I present constraint such as 3x  5y <= 10
in bit vector? For some reason, I do not want to use linear integer.
I'm trying to write constraints similar to the ones in
here about the builtin sequences in Z3:
(declarefun a () (Seq Int))
(declarefun b () (Seq Int))
(assert (= a (seq.++ (seq.unit 1) (seq.unit 2))))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i (seq.len a))) (= (seq.at a i) (seq.at b i)))))
(checksat)
I may be doing this the wrong way but I am getting the following exception:
NOT IMPLEMENTED YET!
z3(58638,0x7fff7a662000) malloc: *** error for object 0x10746bd1d: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
Abort trap: 6
In general, can Z3 build models for constraints that describe "sequence comprehension", i.e., map and filter on the builtin sequences?
Is there any way to define inheritance between sorts in z3? (I'm using the Python API)
I'm trying to model two different types of events, write events and read events; for each of them I use a Sort (WriteSort and
ReadSort). However I would like to have a "sum" Sort (EventSort) that is either a write or a read event.
I'm defining functions with the following domain:
f1 = Function('f1', WriteSort, WriteSort, BoolSort())
f2 = Function('f2', ReadSort, ReadSort, BoolSort())
f3 = Function('f3', EventSort, EventSort, BoolSort())
One possibility would be to define EventSort as and abstract datatype, but then the domain of all my functions should be (EventSort x EventSort) and the only way I see to restrict such domain is doing it manually.
Is there anyway to define both WriteSort and ReadSort as "subsort" of
EventSort?
I am trying to reason about a function "find" in Z3, which takes as input an Array
a which maps Ints to Ints, and another Int i. It should return the smallest Int
j such that a[j] = i, or 1 if no such j exists. My code for this is below:
(declarefun find ((Array Int Int) Int) Int)
(assert (forall ((a (Array Int Int)) (i Int)(j Int)(k Int))
(ite (=> (and (= (select a j) i) (= (select a k) i))
(or (= j k) (< j k))
)
(= (find a i) j)
(= (find a i) 1) ) ))
(checksat)
Unsurprisingly, Z3 returns "unknown" for the code above. I do not think patterns can be used in this instance since patterns require variables to be in the scope of a function symbol, and therefore equality is excluded. I've also tried disabling mbqi and
autoconfig to no avail. Any recommendations for how to reason about something like the above? Thanks!
I'm trying to get all the theory lemmas (meaning Tvalid statements that, together with the original formula, are unsat in a boolean encoding) used in an unsat proof produced by z3.
Since z3 proof contains some complicated theory based inference rules, taking only Z3_OP_PR_TH_LEMMA is not enough.
Currently I'm reading the entire proof, taking all TH_LEMMAs, and also translating some inference rules (such as symmetry, transitivity, etc).
It seems that this is very timeconsuming. The printed proof is quite short, but it uses 'let' expressions, and perhaps this explains the difference between the length of the proof as it is printed, and the time it takes us to process it with arg(i). Is
there a direct way to get all the lemmas, or an efficient way to explore the proof expression?
I have problem with my experia z3 and i can't fix it! I looking for help now. I try to unlock my bootloader but fastboot give me message
FAILED (remote: Command not allowed) someone who know how to fix this problem ?
Cheers
Is there any way to define inheritance between sorts in z3? (I'm using the Python API)
I'm trying to model two different types of events, write events and read events; for each of them I use a Sort (WriteSort and
ReadSort). However I would like to have a "sum" Sort (EventSort) that is either a write or a read event.
I'm defining functions with the following domain:
f1 = Function('f1', WriteSort, WriteSort, BoolSort())
f2 = Function('f2', ReadSort, ReadSort, BoolSort())
f3 = Function('f3', EventSort, EventSort, BoolSort())
One possibility would be to define EventSort as and abstract datatype, but then the domain of all my functions should be (EventSort x EventSort) and the only way I see to restrict such domain is doing it manually.
Is there anyway to define both WriteSort and ReadSort as "subsort" of
EventSort?
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/doclib/docannotationssearch.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
Edit Sorry to bother, I've beed diving into this recently once again. Anyway I think this might be usefull to others. I've been finding that I actually have to call the
Optimize.upper
method in order to get the upper bound, and the model is still not the one that corresponds to this upper bound. I've been able to add it as a new constraint, and call a solver (without optimization, just SAT), but that's probably
not the best idea. By reading
this I feel like I should call Optimize.update_upper
after the solver times out, but the python interface has no such method (?). At least I can get the upper bound, and the corresponding model now (at the cost of unneccessary computations
I guess).
Is there any way in z3 to use an array which contains values of different types? Something like:
(declaresort Record () (Array String Entry))
where Entry above could be either a String or an Int. I understand that using parameterized types I could create separate instances of arrays which can contain only Strings or only Ints. Is it possible to contain both sorts within a single array?
I am using array as a parameter to a relation in z3 fixedpoint solver. I am trying to get array value in the certificate which satisfies my query. When I run this on z3 it throws an error stating
Uninterpreted 'a1' in A(#1,#0,#3).
Why is array being treated as uninterpreted? Does this imply uninterpreted functions cannot be used as arguments to a relation in fixedpoint solver?
(declarerel A (Int Int (Array Int Int)))
(declarerel q1 (Int Int (Array Int Int)))
(declareconst a1 (Array Int Int))
(declarevar a Int)
(declarevar b Int)
(declarevar i Int)
(rule (=> (A (+ a 1) b (store a1 i 2)) (A a b a1)))
(rule (=> (= a b) (A a b a1)))
(rule (=> (and (A a b a1) (= a 0) (= b 1)) (q1 a b a1)))
(query q1 :printcertificate true)
Recently, I tried to use z3 on a 32bit windows xp, and when I load z3dll using java api, it threw error message as follow:
WindowsError: [Error 998] Invalid access to memory location.
I noticed that, Z3 dosen't support Windows XP because of threadlocal storage. I wonder is there any way to adapt z3 to windows xp.
I am using array as a parameter to a relation in z3 fixedpoint solver. I am trying to get array value in the certificate which satisfies my query. When I run this on z3 it throws an error stating
Uninterpreted 'a1' in A(#1,#0,#3).
Why is array being treated as uninterpreted? Does this imply uninterpreted functions cannot be used as arguments to a relation in fixedpoint solver?
(declarerel A (Int Int (Array Int Int)))
(declarerel q1 (Int Int (Array Int Int)))
(declareconst a1 (Array Int Int))
(declarevar a Int)
(declarevar b Int)
(declarevar i Int)
(rule (=> (A (+ a 1) b (store a1 i 2)) (A a b a1)))
(rule (=> (= a b) (A a b a1)))
(rule (=> (and (A a b a1) (= a 0) (= b 1)) (q1 a b a1)))
(query q1 :printcertificate true)
Here is the input
Example 1
(declarevar a Int)
(declarevar b Int)
(declarevar n Int)
(assert (= b (* a a)))
(assert (not (= b (^ a 2))))
(checksat)
Example 2
(declarevar a Int)
(declarevar b Int)
(declarevar n Int)
(assert (= b (* (^ a n) a)))
(assert (not (= b (^ a (+ n 1)))))
(checksat)
It returns unknown almost instantaneously.
I am having troubles proving the following law with LiquidHaskell:
It is known as (one of) DeMorgan's law, and simply states that the negation of
or
ing two values must be the same as and
ing the negation of each. It's been proven for a long time, and is an example in LiquidHaskell's
tutorial. I am following along in the tutorial, but fail to get the following code to pass:
 Test.hs
module Main where
main :: IO ()
main = return ()
(==>) :: Bool > Bool > Bool
False ==> False = True
False ==> True = True
True ==> True = True
True ==> False = False
(<=>) :: Bool > Bool > Bool
False <=> False = True
False <=> True = False
True <=> True = True
True <=> False = False
{@ type TRUE = {v:Bool  Prop v} @}
{@ type FALSE = {v:Bool  not (Prop v)} @}
{@ deMorgan :: Bool > Bool > TRUE @}
deMorgan :: Bool > Bool > Bool
deMorgan a b = not (a  b) <=> (not a && not b)
When running liquid Test.hs
, I get the following output:
LiquidHaskell Copyright 200915 Regents of the University of California. All Rights Reserved.
**** DONE: Parsed All Specifications ******************************************
**** DONE: Loaded Targets *****************************************************
**** DONE: Extracted Core using GHC *******************************************
Working 0% [.................................................................]
Done solving.
**** DONE: solve **************************************************************
**** DONE: annotate ***********************************************************
**** RESULT: UNSAFE ************************************************************
Test.hs:23:1648: Error: Liquid Type Mismatch
23  deMorgan a b = not (a  b) <=> (not a && not b)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Inferred type
VV : Bool
not a subtype of Required type
VV : {VV : Bool  Prop VV}
In Context
Now I'm by no means a LiquidHaskell expert, but I'm pretty sure something must be wrong. I have convinced myself that the identity holds a few years ago, but to make sure I called the function with every possible input, and eventually ran
λ: :l Test.hs
λ: import Test.QuickCheck
λ: quickCheck deMorgan
>>> +++ OK, passed 100 tests.
So I don't seem to have a typo in the Haskell code, the error must lie in the LiquidHaskell specification. It seems that LiquidHaskell cannot infer that the resulting
Bool
is strictly TRUE
:
Inferred type
VV : Bool
not a subtype of Required type
VV : {VV : Bool  Prop VV}
What is my mistake here? Any help is appreciated!
PS: I'm using the z3
solver, and running GHC 7.10.3. LiquidHaskell version is
200915
.
Here is the input
Example 1
(declarevar a Int)
(declarevar b Int)
(declarevar n Int)
(assert (= b (* a a)))
(assert (not (= b (^ a 2))))
(checksat)
Example 2
(declarevar a Int)
(declarevar b Int)
(declarevar n Int)
(assert (= b (* (^ a n) a)))
(assert (not (= b (^ a (+ n 1)))))
(checksat)
It returns unknown almost instantaneously.
I'm running into a situation where I'd really love a copy feature for the Z3 Solver. By this I mean, I have a solver instantiated with some constraints. I now want to copy it so that I have two
independent solvers. At the moment, I'm doing this by creating a new solver and just iterating over s.assertions and adding them back in. For small solvers this is fine. For larger solvers, this can severely impact the time make a copy as Z3 is recreating
work it has already done.
While this isn't a show stopper, it would be very beneficial to be able to copy the solver directly. The normal deepcopy method throws an error about not being able to deepcopy ctypes (which makes sense), so I'm guessing any better solution would have to
be implemented by z3 or z3py proper.
Anyone know of a more efficient way to copy the solver as stated and not incur the overhead of Z3 resolving what it already knows?
I would like to know if it is possible to bound the range of values of a universally quantified variable in Z3.
For example, let's assume that I have a variable of type Real called "time" which is used to model the time in the system.
Let's say that I have an assertion which says that the value of some unary function "func1" shall always be between 1 and 100. The function takes the input the time variable. Expressed in Z3, I have encoded the property as following:

ForAll(time, And(func1(time) >= 1, func1(time) <= 100))
Please note that I explicitly need the time variable to be universally quantified, because I want the Z3 go give me unsat if I inject property of following type:

Exists(time, func1(time) == 101)
As far as my understanding goes for Z3, all the constants have mathematical (theoretical) and not computer (practical) implementation i.e. their values are not bound (unfortunately I cannot point to the resource where I have read this at the moment). Assume
that with time I model time in my systems, and according to the system constrains it cannot run for more than x hours, which I can use and say that value of time is between 0 and x*60'*60 to give the maximum execution time in seconds. I know that I can assert
the allowed values for time with the following assertion:

And(time >= 0, time <= x*60*60)
but will it affect the universal quantification given in 1?
Consequently, this should lead to a situation where if property 2 is injected and for value of time I specify
x*60*60 + 1
, it should not be unset since the ForAll
is valid only for the values of time.
I would like to know if it is possible to bound the range of values of a universally quantified variable in Z3.
For example, let's assume that I have a variable of type Real called "time" which is used to model the time in the system.
Let's say that I have an assertion which says that the value of some unary function "func1" shall always be between 1 and 100. The function takes the input the time variable. Expressed in Z3, I have encoded the property as following:

ForAll(time, And(func1(time) >= 1, func1(time) <= 100))
Please note that I explicitly need the time variable to be universally quantified, because I want the Z3 go give me unsat if I inject property of following type:

Exists(time, func1(time) == 101)
As far as my understanding goes for Z3, all the constants have mathematical (theoretical) and not computer (practical) implementation i.e. their values are not bound (unfortunately I cannot point to the resource where I have read this at the moment). Assume
that with time I model time in my systems, and according to the system constrains it cannot run for more than x hours, which I can use and say that value of time is between 0 and x*60'*60 to give the maximum execution time in seconds. I know that I can assert
the allowed values for time with the following assertion:

And(time >= 0, time <= x*60*60)
but will it affect the universal quantification given in 1?
Consequently, this should lead to a situation where if property 2 is injected and for value of time I specify
x*60*60 + 1
, it should not be unset since the ForAll
is valid only for the values of time.
I'm trying to implement my own version of arrays in Z3, called "Records". They're just Arrays which are indexed by strings. I keep receiving a timeout for the code below and I can't figure out why. I know I could just use normal arrays but I'd like to determine
the problem with this code.
I have an assertion for each of the basic array select/store axioms. any idea as to what's wrong?
(declaresort Record)
(declarefun storeR (Record String Int) Record)
(declarefun selectR (Record String) Int)
;selct/store axioms for records
(assert (forall ((r Record)(s String)(i Int))
(= (selectR (storeR r s i) s) i)))
(assert (forall ((r Record)(s String)(q String) (i Int))
(or (= s q) (= (selectR (storeR r s i) q) (selectR r q) ))))
(assert (forall ((r Record)(q Record))
(=> (forall ((s String)) (= (selectR r s) (selectR q s))) (= r q))))
(declareconst r Record)
(assert (= (selectR r "number") 1))
(checksat)
active questions tagged z3  Stack Overflow News Feed