active questions tagged z3 - Stack Overflow News Feed 
Thursday, May 5, 2016  |  From active questions tagged z3 - Stack Overflow




I have a question about the Z3/SMTLib API.



The key SMT subroutine required by the liquid-types
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,



  1. Is there an API that would let me do the above?
  2. Would query2 be faster than the loop in query1 above?

Wednesday, May 4, 2016  |  From active questions tagged z3 - Stack Overflow




The title says it all. I try to present -1 as the following: (_ bv-1 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.



Tuesday, May 3, 2016  |  From active questions tagged z3 - Stack Overflow




I'm trying to write constraints similar to the ones in here about the builtin sequences in Z3:



(declare-fun a () (Seq Int))
(declare-fun 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)))))

(check-sat)


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?



Monday, May 2, 2016  |  From active questions tagged z3 - Stack Overflow




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?



Sunday, May 1, 2016  |  From active questions tagged z3 - Stack Overflow




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:



(declare-fun 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) ) ))
(check-sat)


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 auto-config to no avail. Any recommendations for how to reason about something like the above? Thanks!



Sunday, May 1, 2016  |  From active questions tagged z3 - Stack Overflow




I'm trying to get all the theory lemmas (meaning T-valid 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 time-consuming. 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?



Saturday, April 30, 2016  |  From active questions tagged z3 - Stack Overflow




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



Thursday, April 28, 2016  |  From active questions tagged z3 - Stack Overflow




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?



Thursday, April 28, 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



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



Thursday, April 28, 2016  |  From active questions tagged z3 - Stack Overflow




Is there any way in z3 to use an array which contains values of different types? Something like:



(declare-sort 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?



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




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?



(declare-rel A (Int Int (Array Int Int)))
(declare-rel q1 (Int Int  (Array Int Int)))
(declare-const a1 (Array Int Int))
(declare-var a Int) 
(declare-var b Int)
(declare-var 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 :print-certificate true)


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




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 thread-local storage. I wonder is there any way to adapt z3 to windows xp.



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




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?



(declare-rel A (Int Int (Array Int Int)))
(declare-rel q1 (Int Int  (Array Int Int)))
(declare-const a1 (Array Int Int))
(declare-var a Int) 
(declare-var b Int)
(declare-var 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 :print-certificate true)


Saturday, April 23, 2016  |  From active questions tagged z3 - Stack Overflow




Here is the input



Example 1



(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* a a)))
(assert (not (= b (^ a 2))))
(check-sat)


Example 2



(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* (^ a n) a)))
(assert (not (= b (^ a (+ n 1)))))
(check-sat)


It returns unknown almost instantaneously.



Saturday, April 23, 2016  |  From active questions tagged z3 - Stack Overflow




I am having troubles proving the following law with LiquidHaskell:



DeMorgan's law



It is known as (one of) DeMorgan's law, and simply states that the negation of oring two values must be the same as anding 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 2009-15 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:16-48: 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 2009-15.



Saturday, April 23, 2016  |  From active questions tagged z3 - Stack Overflow




Here is the input



Example 1



(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* a a)))
(assert (not (= b (^ a 2))))
(check-sat)


Example 2



(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* (^ a n) a)))
(assert (not (= b (^ a (+ n 1)))))
(check-sat)


It returns unknown almost instantaneously.



Thursday, April 21, 2016  |  From active questions tagged z3 - Stack Overflow




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 re-creating 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 re-solving what it already knows?



Wednesday, April 20, 2016  |  From active questions tagged z3 - Stack Overflow




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:



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

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

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



Wednesday, April 20, 2016  |  From active questions tagged z3 - Stack Overflow




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:



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

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

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



Wednesday, April 20, 2016  |  From active questions tagged z3 - Stack Overflow




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?



(declare-sort Record)

(declare-fun storeR (Record String Int) Record)
(declare-fun 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))))


 (declare-const r Record)
 (assert (= (selectR r "number") 1))
 (check-sat)


 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.