CodePlexProject Hosting for Open Source Software

active questions tagged z3 - Stack Overflow News Feed

Saturday, October 3, 2015 | From
active questions tagged z3 - Stack Overflow

I am new to Z3 solver and SMTLib2. I want to obtain expressions for each variable in the constraints. Assume, I have this program.

```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))
```

Using `get-value`

, I can obtain the value for `z`

that satisfies all the constraints. But, how can I get the expression for
`z`

. Something like `z=y+11`

.

I find that using `simplify`

, I can simplify the constraints but is there anyway to get expression for each variable in the constraints.

Saturday, October 3, 2015 | From
active questions tagged z3 - Stack Overflow

I am new to Z3 solver and SMTLib2. I want to obtain expressions for each variable in the constraints. Assume, I have this program.

```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))
```

Using `get-value`

, I can obtain the value for `z`

that satisfies all the constraints. But, how can I get the expression for
`z`

. Something like `z=y+11`

.

I find that using `simplify`

, I can simplify the constraints but is there anyway to get expression for each variable in the constraints.

Friday, October 2, 2015 | From
active questions tagged z3 - Stack Overflow

I have written two Sudoku solvers in Z3, once using 81 variables, and once using a function that maps x and y coordinates to the number in square[x][y].

I guess one could also use an Array instead.

What is the difference between having a python array of Z3 variables, having a Z3 array or having a function in Z3?

When should I use which?

Thursday, October 1, 2015 | From
active questions tagged z3 - Stack Overflow

Executing the following query on Z3 solver

```
(assert (exists ((c0_s Int) (c1_s Int) (c2_s Int))
(and
(= (+ c0 c1 c2) 5) (>= c0 0) (>= c1 1) (>= c2 1)
(= c0_s c0) (= c1_s (- c1 1)) (= c2_s (+ c2 1))
(= c2_s 3) (= (+ c0_s c1_s) 2)
))
)
(apply (then qe ctx-solver-simplify propagate-ineqs))
```

results the follwing result

```
(goals
(goal
(>= c0 0)
(<= c0 2)
(>= c1 1)
(<= c1 3)
(<= (+ (* (- 1) c0) (* (- 1) c1)) (- 3))
(<= (+ c1 c0) 3)
(= c2 2)
:precision precise :depth 3)
)
```

where I was expecting a result from the Z3 solver like this,

```
(goals
(goal
(>= c0 0)
(<= c0 2)
(>= c1 1)
(<= c1 3)
(= (+ c1 c0) 3)
(= c2 2)
:precision precise :depth 3)
)
```

Is there a way I could achieve this? and can anyone explain Why Z3 solver is producing such complex result instead of as expected?

Tuesday, September 29, 2015 | From
active questions tagged z3 - Stack Overflow

I am inferring a Function(var1) and I only care about the values of this function when 0 <= var1 <= 10 and I know, when 0 <= var <= 10, 0 <= Function(var1) <= 10.

A common way (I guess) to constrain the search space of the Function is something like asserting constraints like (in z3py):

```
for i in range(11):
solver.add(And(Function(i)>=0,Function(i)<=10))
```

My question is that: is there a better way so that I can constrain the search space of Function? Something like setting upperbound/lowerbound of this Function by nature?

My intuitions are that: since I have a lot other constraints for this Function, I feel like if I could constrain the search space of Function by nature, many impossible assignment might be automatically avoided by the solver, and the time spent on the inference might be reduced. I am not sure if this makes sense.

Tuesday, September 29, 2015 | From
active questions tagged z3 - Stack Overflow

In `homebrew`

, if I choose to install `z3`

, I get the following result:

```
▶ brew install z3
Error: Formulae found in multiple taps:
* homebrew/science/z3
* mht208/formal/z3
Please use the fully-qualified name e.g. homebrew/science/z3 to refer the formula.
```

On one hand the `homebrew`

formula might seem to be more canonical because that's the main repository (or whatever one calls the top-level item in
`homebrew`

), but on the other hand `mht208`

is the developer of
`z3`

as near as I can tell. Is there an easy way to determine which of these two has either the latest version or the most stable version?

Edited to add additional information:

When I run `brew info`

on each fully-qualified name, I get the following results:

```
▶ brew info homebrew/science/z3
homebrew/science/z3: stable 4.4.0 (bottled), HEAD
A high-performance theorem prover
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.4.0_1 (50 files, 38M) *
Poured from bottle
From: https://github.com/Homebrew/homebrew-science/blob/master/z3.rb
▶ brew info mht208/formal/z3
mht208/formal/z3: stable 4.4.0
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.4.0_1 (50 files, 38M) *
Poured from bottle
From: https://github.com/mht208/homebrew-formal/blob/master/z3.rb
==> Dependencies
Build: autoconf ✔
==> Options
--with-ocaml
Build ocaml bindings with the ocaml from Homebrew.
--with-opam
Build ocaml bindings with the ocaml from OPAM.
```

So, in theory, these both *seem* to be the same version (`4.4.0_1`

), except that the
`mht208`

version has some options and depends on `autoconf`

(which is already installed). This also leads to the question of whether it makes a difference how the
`ocaml`

bindings are built (both `ocaml`

and `opam`

are already installed).

Tuesday, September 29, 2015 | From
active questions tagged z3 - Stack Overflow

I am very interested in vZ solver after reading the paper "vZ - Maximal Satisfaction with Z3". I compiled the vZ solver from the unsatable branch at commit 04266fc from https://github.com/Z3Prover/z3/tree/unstable. However, vZ returns "Segmentation fault" for several input SMT formulas, one example can be found here. However, this example formula can be online solved by Rise4Fun. Maybe the local version of vZ has problems. Could you do me a favor to tell me the commit number of vZ in Rise4Fun? Then I can use it locally. Thanks in advance!

Monday, September 28, 2015 | From
active questions tagged z3 - Stack Overflow

Here is my code:

```
from z3 import *
a = BitVecVal(5,3)
b = BitVecVal(8,3)
print a
print b
s = Solver()
s.add(a<b)
print s.check()
print s.model()
```

The output is

```
5
0
sat
```

Could someone help me understand why 'a' is smaller than 'b'?

Monday, September 28, 2015 | From
active questions tagged z3 - Stack Overflow

Is there a way to run Z3 solver from javascript? Or is there a better SMT solver that I can be used in JavaScript?

Sunday, September 27, 2015 | From
active questions tagged z3 - Stack Overflow

I try make a simple example for checking bytes in fixed array. I read also Z3 tutorials but i can't get it working. Here is may scenario:

I have fixed byte array with length of 16: T(16)

I have these conditions to check:

```
A = (T(16) + 1) And 0x0F
T(A) = 0x76
0x01 <= A <= 0x7F
```

It mean take byte from `T(16)`

add `1`

, make `AND`

with
`0x0F`

, and assign result number to variable `A`

.

Now check if in array `T`

on position `A`

`T(A)`

is number
`0x76`

. Also `A`

can be between values `0x01`

and
`0x7F`

.

These conditions are repeating for more positions in array, but I need get it working just for first case. The goal of this is: find right order of known bytes in fixed array based on given equations.

I try it with this script but doesn't work.

Error: operator is applied to arguments of the wrong sort.

```
(declare-const t (Array Int Int))
(declare-const a Int)
; A = (t(16) + 1) And 0x0F
(assert (= a (bvand (+ (select t 16) 1) #x0F)))
; t(A) = 0x76
(assert (= (select t a) #x76))
(check-sat)
;(get-model)
```

Example:

on `T(16)`

is value `0x14`

, + 1 = `0x15`

, ```
AND
```

`0x0F`

= `0x05`

, on `T(0x05)`

should be value
`0x76`

.

Thank you.

Saturday, September 26, 2015 | From
active questions tagged z3 - Stack Overflow

I'm interested in the vZ solver described in the paper:

νZ - An Optimizing SMT Solver. Nikolaj Bjørner, Anh-Dung Phan, Lars Fleckenstein. TACAS 2015.

How can I download either the binary or source code of the solver?

Thank.

Wednesday, September 23, 2015 | From
active questions tagged z3 - Stack Overflow

I am very interested in vZ solver after reading the paper "vZ - Maximal Satisfaction with Z3". I compiled the vZ solver from the unsatable branch at commit 04266fc from https://github.com/Z3Prover/z3/tree/unstable. However, vZ returns "Segmentation fault" for several input SMT formulas, one example can be found here. However, this example formula can be online solved by Rise4Fun. Maybe the local version of vZ has problems. Could you do me a favor to tell me the commit number of vZ in Rise4Fun? Then I can use it locally. Thanks in advance!

Sunday, September 20, 2015 | From
active questions tagged z3 - Stack Overflow

This is a follow-up question of my earlier question "Is it possible to intrinsically reduce the search space of Function".

I am thinking if it is possible that I can define a sort that contains a set of integers, e.g., integers 1-10.

My intuition is that to reduce search space of Function, instead of defining a Function whose domain sort and range sort are IntSort, I want to define a Function whose domain sort and range sort are a sort that only contains a set of integers of my interest.

Suppose

Saturday, September 19, 2015 | From
active questions tagged z3 - Stack Overflow

I observed that the check time of my logical formulas written in z3py changed a lot (from ~60s to ~30s, about 50%) after I removed "-" in the names of the variables that I defined.

E.g.,

```
vec = IntVector('vec-1',10)
```

to

```
vec = IntVector('vec1',10)
```

Is this something expected? If so, why?

Saturday, September 19, 2015 | From
active questions tagged z3 - Stack Overflow

I observed that the check time of my logical formulas written in z3py changed a lot (from ~60s to ~30s, about 50%) after I removed "-" in the names of the variables that I defined.

E.g.,

```
vec = IntVector('vec-1',10)
```

to

```
vec = IntVector('vec1',10)
```

Is this something expected? If so, why?

Tuesday, September 15, 2015 | From
active questions tagged z3 - Stack Overflow

I am trying to figure out how to get the unsat core using the Java API for Z3. Our scenario is as follows (code is underneath, which works in rise4fun):

- We create the SMT2 input programtically
- The input contains function definitions, datatype declarations, and assertions
- We parse this using the parseSMTLIB2String API
- We ensure that the context and the solver have unsat_core -> true
- Z3 returns UNSAT for the provided input, which is correct
- The UNSAT core is always empty though.
- The same input produces an UNSAT core correctly on rise4fun (x1 x3)

I am guessing I am misusing the API somehow... but not quite sure how/why.

I have noticed that I cannot set the unsat core option in the SMT string that I pass to parseSMTLIB2String, because that is not allowed. I am guessing that is expected.

Can someone point me in the right direction please?

Thanks!!

```
(set-option :smt.macro-finder true)
;; The following is only for rise4fun, i cannot get it
;; to work with the parse SMT Java API
(set-option :produce-unsat-cores true)
(define-sort Ref () Int)
(declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
(declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))
(define-sort Set (T) (Array T Bool))
(define-sort Bag (T) (Array T Int))
(declare-const emptySetOf_Int (Set Int))
(assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))
(declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
(declare-datatypes () ((A (mk-A (x Int)(y Int)))))
(declare-datatypes () ((Any
(lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
(lift-A (sel-A A))
null))
)
(declare-const heap (Array Ref Any))
(define-fun deref ((ref Ref)) Any
(select heap ref)
)
(define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
(is-lift-TopLevelDeclarations (deref this))
)
(define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
(sel-TopLevelDeclarations (deref this))
)
(define-fun deref-is-A ((this Ref)) Bool
(is-lift-A (deref this))
)
(define-fun deref-A ((this Ref)) A
(sel-A (deref this))
)
(define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
(deref-is-TopLevelDeclarations this)
)
(define-fun deref-isa-A ((this Ref)) Bool
(deref-is-A this)
)
(define-fun A!x ((this Ref)) Int
(x (deref-A this))
)
(define-fun A!y ((this Ref)) Int
(y (deref-A this))
)
(define-fun TopLevelDeclarations.inv ((this Ref)) Bool
true
)
(assert (! (forall ((this Ref))
(=> (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
) :named x0))
(define-fun A.inv ((this Ref)) Bool
(and
(> (A!x this) 0)
(> (A!y this) 0)
(< (A!x this) 0)
)
)
(assert (! (forall ((this Ref))
(=> (deref-is-A this) (A.inv this))
) :named x1))
(assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
(assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))
(check-sat)
(get-unsat-core)
```

Tuesday, September 15, 2015 | From
active questions tagged z3 - Stack Overflow

I need to be able to compare two integer expressions, which may include literal integers, addition, unary negation, integer constants, and infinity, and decide if an inequality between them is satisfiable. This is part of a larger program, so there is no way for me to know ahead of time what those expressions will look like.

I have considered defining an integer constant and just letting it take any value, but then I realized that Infinity < 5 would be satisfiable.

I have considered defining a constant and making a universally quantified assertion that it is greater than all integers, but I don't know what Sort I should say it is. If I tell Z3 that the Sort of my Infinity constant is integer, I think it will probably happily go off and try to find me THE LARGEST INTEGER! I'm pretty sure that won't end the way I want.

Tuesday, September 15, 2015 | From
active questions tagged z3 - Stack Overflow

I am trying to figure out how to get the unsat core using the Java API for Z3. Our scenario is as follows (code is underneath, which works in rise4fun):

- We create the SMT2 input programtically
- The input contains function definitions, datatype declarations, and assertions
- We parse this using the parseSMTLIB2String API
- We ensure that the context and the solver have unsat_core -> true
- Z3 returns UNSAT for the provided input, which is correct
- The UNSAT core is always empty though.
- The same input produces an UNSAT core correctly on rise4fun (x1 x3)

I am guessing I am misusing the API somehow... but not quite sure how/why.

I have noticed that I cannot set the unsat core option in the SMT string that I pass to parseSMTLIB2String, because that is not allowed. I am guessing that is expected.

Can someone point me in the right direction please?

Thanks!!

```
(set-option :smt.macro-finder true)
;; The following is only for rise4fun, i cannot get it
;; to work with the parse SMT Java API
(set-option :produce-unsat-cores true)
(define-sort Ref () Int)
(declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
(declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))
(define-sort Set (T) (Array T Bool))
(define-sort Bag (T) (Array T Int))
(declare-const emptySetOf_Int (Set Int))
(assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))
(declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
(declare-datatypes () ((A (mk-A (x Int)(y Int)))))
(declare-datatypes () ((Any
(lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
(lift-A (sel-A A))
null))
)
(declare-const heap (Array Ref Any))
(define-fun deref ((ref Ref)) Any
(select heap ref)
)
(define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
(is-lift-TopLevelDeclarations (deref this))
)
(define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
(sel-TopLevelDeclarations (deref this))
)
(define-fun deref-is-A ((this Ref)) Bool
(is-lift-A (deref this))
)
(define-fun deref-A ((this Ref)) A
(sel-A (deref this))
)
(define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
(deref-is-TopLevelDeclarations this)
)
(define-fun deref-isa-A ((this Ref)) Bool
(deref-is-A this)
)
(define-fun A!x ((this Ref)) Int
(x (deref-A this))
)
(define-fun A!y ((this Ref)) Int
(y (deref-A this))
)
(define-fun TopLevelDeclarations.inv ((this Ref)) Bool
true
)
(assert (! (forall ((this Ref))
(=> (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
) :named x0))
(define-fun A.inv ((this Ref)) Bool
(and
(> (A!x this) 0)
(> (A!y this) 0)
(< (A!x this) 0)
)
)
(assert (! (forall ((this Ref))
(=> (deref-is-A this) (A.inv this))
) :named x1))
(assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
(assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))
(check-sat)
(get-unsat-core)
```

Tuesday, September 15, 2015 | From
active questions tagged z3 - Stack Overflow

I have a number of constraints asserting for bits in BitVec and I wonder what is the most efficient way of asserting constraints for a specific bit in a BitVec?

Assume I want to assert that the 5th bit in a BitVec is 1, is there any way that is more efficient (lower check time) than this?

```
bitvec = BitVec('bitvec',10)
s.add(Extract(5,5,bitvec)==1)
```

Monday, September 14, 2015 | From
active questions tagged z3 - Stack Overflow

What does the Z3 option `hi_div0`

mean? I was unable to find any documentation.

How does that option affect performance and how does it affect semantics?

active questions tagged z3 - Stack Overflow News Feed

Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13