CodePlexProject Hosting for Open Source Software

active questions tagged z3 - Stack Overflow News Feed

Tuesday, March 31, 2015 | From
active questions tagged z3 - Stack Overflow

The link mentioned in the online tutorial doesn't contain any link to opt branch:

```
http://z3.codeplex.com/
```

and also there isn't any page under download section... Is it possible to get the binaries for windows/linux?

Thanks

Monday, March 30, 2015 | From
active questions tagged z3 - Stack Overflow

We look for a number of the form `efghiihgfe`

which is the product of two numbers of the form
`999ab`

and `99qcd`

.

We use the following code

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const p Int)
(declare-const q Int)
(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))
(assert (= (* (+ 99900 (* 10 a) b ) (+ 99000 (* 100 q) (* 10 c) d ))
(+ (* (^ 10 9) e) (* (^ 10 8) f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5) i)
(* (^ 10 4) i) (* 1000 h ) (* 100 g) (* 10 f) e) ) )
(check-sat)
(get-model)
(eval (+ (* (^ 10 9) e) (* (^ 10 8) f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5) i)
(* (^ 10 4) i) (* 1000 h ) (* 100 g) (* 10 f) e))
```

and the output is

```
(model
(define-fun q () Int
6)
(define-fun p () Int
0)
(define-fun i () Int
0)
(define-fun h () Int
6)
(define-fun g () Int
6)
(define-fun f () Int
9)
(define-fun e () Int
9)
(define-fun d () Int
1)
(define-fun c () Int
8)
(define-fun b () Int
9)
(define-fun a () Int
7)
)
9966006699
```

To verify that `9966006699`

is the maxim we run the code

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const p Int)
(declare-const q Int)
(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))
(assert (= (* (+ 99900 (* 10 a) b ) (+ 99000 (* 100 q) (* 10 c) d ))
(+ (* (^ 10 9) e) (* (^ 10 8) f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5) i)
(* (^ 10 4) i) (* 1000 h ) (* 100 g) (* 10 f) e) ) )
(assert (> (+ (* (^ 10 9) e) (* (^ 10 8) f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5) i)
(* (^ 10 4) i) (* 1000 h ) (* 100 g) (* 10 f) e) 9966006699 ))
(check-sat)
```

and the output is

```
unsat
```

Please let me know if there is a more efficient program with Z3 to solve the problem.

Sunday, March 29, 2015 | From
active questions tagged z3 - Stack Overflow

Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.

The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is
`993 * 913 = 906609`

.

In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of
`604406`

.

How can I change my code so that the maximal value of `906609`

is found?

I've tried using `(maximize (* p q))`

, but that reports an error, saying
`Objective function '(* p q)' is not supported`

. I can tweak the range of
`a`

, but I'm looking for a way to have Z3 do that for me.

What I have so far is:

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const p Int)
(declare-const q Int)
(declare-const pq Int)
(define-fun satisfy ((pq Int)) Bool
(and
(<= 1 a 9)
(<= 0 b 9)
(<= 0 c 9)
(<= 100 p 999)
(<= p q 999)
(= pq
(* p q)
(+ (* 100001 a)
(* 10010 b)
(* 1100 c)))))
(assert (satisfy pq))
; Does not work:
;(maximize (* p q))
(check-sat)
(get-model)
```

Running this with `z3 -smt2 e4.smt2`

as-is produces:

```
sat
(model
(define-fun q () Int
913)
(define-fun p () Int
662)
(define-fun c () Int
4)
(define-fun b () Int
0)
(define-fun a () Int
6)
(define-fun pq () Int
604406)
)
```

Sunday, March 29, 2015 | From
active questions tagged z3 - Stack Overflow

Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.

The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is
`993 * 913 = 906609`

.

In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of
`604406`

.

How can I change my code so that the maximal value of `906609`

is found?

I've tried using `(maximize (* p q))`

, but that reports an error, saying
`Objective function '(* p q)' is not supported`

. I can tweak the range of
`a`

, but I'm looking for a way to have Z3 do that for me.

What I have so far is:

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const p Int)
(declare-const q Int)
(declare-const pq Int)
(define-fun satisfy ((pq Int)) Bool
(and
(<= 1 a 9)
(<= 0 b 9)
(<= 0 c 9)
(<= 100 p 999)
(<= p q 999)
(= pq
(* p q)
(+ (* 100001 a)
(* 10010 b)
(* 1100 c)))))
(assert (satisfy pq))
; Does not work:
;(maximize (* p q))
(check-sat)
(get-model)
```

Running this with `z3 -smt2 e4.smt2`

as-is produces:

```
sat
(model
(define-fun q () Int
913)
(define-fun p () Int
662)
(define-fun c () Int
4)
(define-fun b () Int
0)
(define-fun a () Int
6)
(define-fun pq () Int
604406)
)
```

Sunday, March 29, 2015 | From
active questions tagged z3 - Stack Overflow

This smt2 script gives UNSAT if I use

(check-sat-using (then simplify solve-eqs (repeat bit-blast) (! smt :bv.enable_int2bv true :arith.euclidean_solver true))), and gives SAT if I remove ":arith.euclidean_solver true". The expected result is SAT.

Z3 version 4.4.0

Thank you in advance.

Sunday, March 29, 2015 | From
active questions tagged z3 - Stack Overflow

Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.

The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is
`993 * 913 = 906609`

.

In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of
`604406`

.

How can I change my code so that the maximal value of `906609`

is found?

I've tried using `(maximize (* p q))`

, but that reports an error, saying
`Objective function '(* p q)' is not supported`

. I can tweak the range of
`a`

, but I'm looking for a way to have Z3 do that for me.

What I have so far is:

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const p Int)
(declare-const q Int)
(declare-const pq Int)
(define-fun satisfy ((pq Int)) Bool
(and
(<= 1 a 9)
(<= 0 b 9)
(<= 0 c 9)
(<= 100 p 999)
(<= p q 999)
(= pq
(* p q)
(+ (* 100001 a)
(* 10010 b)
(* 1100 c)))))
(assert (satisfy pq))
; Does not work:
;(maximize (* p q))
(check-sat)
(get-model)
```

Running this with `z3 -smt2 e4.smt2`

as-is produces:

```
sat
(model
(define-fun q () Int
913)
(define-fun p () Int
662)
(define-fun c () Int
4)
(define-fun b () Int
0)
(define-fun a () Int
6)
(define-fun pq () Int
604406)
)
```

Friday, March 27, 2015 | From
active questions tagged z3 - Stack Overflow

`993 * 913 = 906609`

.

`604406`

.

`906609`

is found?

I've tried using `(maximize (* p q))`

, but that reports an error, saying
`Objective function '(* p q)' is not supported`

. I can tweak the range of
`a`

, but I'm looking for a way to have Z3 do that for me.

What I have so far is:

```
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const p Int)
(declare-const q Int)
(declare-const pq Int)
(define-fun satisfy ((pq Int)) Bool
(and
(<= 1 a 9)
(<= 0 b 9)
(<= 0 c 9)
(<= 100 p 999)
(<= p q 999)
(= pq
(* p q)
(+ (* 100001 a)
(* 10010 b)
(* 1100 c)))))
(assert (satisfy pq))
; Does not work:
;(maximize (* p q))
(check-sat)
(get-model)
```

Running this with `z3 -smt2 e4.smt2`

as-is produces:

```
sat
(model
(define-fun q () Int
913)
(define-fun p () Int
662)
(define-fun c () Int
4)
(define-fun b () Int
0)
(define-fun a () Int
6)
(define-fun pq () Int
604406)
)
```

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

A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.

The following SMT2 example returns SAT with the correct model:

```
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)
```

The following semantically equivalent example returns unknown:

```
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(check-sat p1 p2 p3 p4)
(get-model)
```

Moreover, the model query returns a model, which is incorrect!

Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.

It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).

Am I missing something? Thank you!

PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).

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

A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.

The following SMT2 example returns SAT with the correct model:

```
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)
```

The following semantically equivalent example returns unknown:

```
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(check-sat p1 p2 p3 p4)
(get-model)
```

Moreover, the model query returns a model, which is incorrect!

Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.

It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).

Am I missing something? Thank you!

PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).

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

While trying to solve large nonlinear real arithmetic problems, I track every assertion using answer literals and explicit implications, as recommended in other posts. It should be equivalent to using the (! (...) :named p1) syntax of the SMT2 format. It seems, though, that both methods are handled differently internally.

The following SMT2 code gives an UNKNOWN result, with explanation "(incomplete (theory arithmetic))":

```
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const p5 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (=> p5 (< x3 0.0)))
(check-sat p1 p2 p3)
(get-info:reason-unknown)
```

On the other hand, the following SMT2 code gives the correct answer, UNSAT, and produces an informative unsat core (p4, p5):

```
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (! (= x1 (/ 1.0 (* x2 x2))) :named p1))
(assert (! (not (= x2 0.0)) :named p2))
(assert (! (= x3 (* 2.0 x1)) :named p3))
(assert (! (= x3 5.0) :named p4))
(assert (! (< x3 0) :named p5))
(check-sat)
(get-unsat-core)
;(get-model)
```

My specific questions are:

- How can this differing behavior be explained? What is recommended practice for tracking nonlinear real equations and inequalities?
- What would be the equivalent OCaml API call for the (! (...) :named p1) syntax of SMT2? Is it assert_and_track?

I am using Z3 version 4.3.2 from the ml-ng branch under Linux.

Many thanks!

Saturday, March 21, 2015 | From
active questions tagged z3 - Stack Overflow

My problem is as followed,

Environment: 64 bit windows 7, vs 2010, z3-4.3.2

First, compiled Z3 from source(download from z3 homepage ), this step is ok and without any mistake (from the command window);

Second, tested the c++ example under the “src/example”, first, test function find_model_example1(), compile, link, this is no warning, and error. However, got stuck when run. Then, after I debug step by step, stuck at the second statement, “context c”;

```
1, std::cout << "find_model_example1\n";
2, context c;
3, expr x = c.int_const("x");
```

Keep going with F11 at this statement, it stuck at function “reinterpret_cast” , line 424 in api_context.cpp, keep going with F11, in the constructor of “context” :“context(config_params *, bool)”, function “m_replay_stack” will call function “copy_core”(vector.h), which triggered 0xC00000005 error.

Saturday, March 21, 2015 | From
active questions tagged z3 - Stack Overflow

I'm trying to build Z3 newest version (v4.3.2) on Mac OS X 10.10.2.

Downloading the latest source from http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?he ProjectName=z3&changeSetId=cee7dd39444c9060186df79c2a2c7f8845de415b to follow the command in http://z3.codeplex.com/SourceControl/latest#README.

```
CXX=clang++ CC=clang python scripts/mk_make.py
cd build
make
sudo make install
```

The build and installation seems to be OK, however, when I tried to run the example.py, I got this error.

```
Traceback (most recent call last):
File "example.py", line 3, in <module>
x = Real('x')
File "/Library/Python/2.7/site-packages/z3.py", line 2774, in Real
ctx = _get_ctx(ctx)
File "/Library/Python/2.7/site-packages/z3.py", line 210, in _get_ctx
return main_ctx()
File "/Library/Python/2.7/site-packages/z3.py", line 205, in main_ctx
_main_ctx = Context()
File "/Library/Python/2.7/site-packages/z3.py", line 151, in __init__
conf = Z3_mk_config()
File "/Library/Python/2.7/site-packages/z3core.py", line 1036, in Z3_mk_config
r = lib().Z3_mk_config()
File "/Library/Python/2.7/site-packages/z3core.py", line 24, in lib
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.__del__ of <z3.Context instance at 0x227800>> ignored
```

I added `export Z3_LIBRARY_PATH=/Library/Python/2.7/site-packages/`

in the environment variables, and tried 64 bit python with
`arch -x86_64 python example.py`

to get the same results.

From
Using Z3Py With Python 3.3, I tried to copy the `libz3.a/dylib/java.dylib`

files into the
`/Library/Python/2.7/site-packages`

, but without success.

What might be wrong?

Saturday, March 21, 2015 | From
active questions tagged z3 - Stack Overflow

Given the following input

```
(set-option :auto_config false)
(set-option :smt.mbqi false)
(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)
(define-fun FOO () Bool
(forall ((i Int)) (!
(implies
(and (<= 0 i) (< i (len x)))
(exists ((j Int)) (!
(implies
(and (<= 0 j) (< j (len x)))
(> (idx x j) 0))))))))
(assert FOO)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
```

Z3 4.3.2 x64 reports `unsat`

for the first `check-sat`

(as expected), but
`unknown`

for the second. If the commented `push`

/`pop`

s are uncommented, both
`check-sat`

s yield `unknown`

.

My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second
`check-sat`

. The latter could also explain why both `check-sat`

s yield
`unknown`

if `push`

/`pop`

is used because Z3 will (as far as I understand) switch to incremental mode on first
`push`

.

**Question:** Is it a bug or an expected consequence?

Saturday, March 21, 2015 | From
active questions tagged z3 - Stack Overflow

The `ctx-solver-simplify`

tactic only works for bool variables, so how would I deal with variables over finite domain (e.g., which tactics to use)? For example, if
`z`

can only take 3 values `0,1,2`

, then how to simplify ```
Or(z==0,z==1,z==2)
```

to `true`

?

Also, even for bool expressions, the tactic `ctx-solver-simplify`

doesn't simplify completely. For example:

```
x,y,z = z3.Bools('x y z')
c1 = z3.And(x==True,y==True,z==True)
c2 = z3.And(x==True,y==True,z==False)
c3 = z3.And(x==True,y==False,z==True)
c4 = z3.And(x==True,y==True,z==False)
z3.Tactic('ctx-solver-simplify')(z3.Or([c1,c2,c3,c4]))
[[Or(And(x, z), And(x == True, y == True, z == False))]]
```

How do I get something like `And(x, Or(z, y))`

?

Thanks !

Saturday, March 21, 2015 | From
active questions tagged z3 - Stack Overflow

Are the numbers returned by `(get-info :all-statistics)`

accumulated across multiple calls to
`check-sat`

, and across multiple `push`

-`pop`

scopes? Or are they reset at each
`check-sat`

(or at `push`

or `pop`

)?

Phrased differently, if I get statistics at various points during a run of Z3, and if a certain statistics, e.g.`quant-instantiations`

always has the same value, can I then conclude that no quantifier instantiation happened in between getting
these statistics?

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

Given the following input

```
(set-option :auto_config false)
(set-option :smt.mbqi false)
(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)
(define-fun FOO () Bool
(forall ((i Int)) (!
(implies
(and (<= 0 i) (< i (len x)))
(exists ((j Int)) (!
(implies
(and (<= 0 j) (< j (len x)))
(> (idx x j) 0))))))))
(assert FOO)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
```

Z3 4.3.2 x64 reports `unsat`

for the first `check-sat`

(as expected), but
`unknown`

for the second. If the commented `push`

/`pop`

s are uncommented, both
`check-sat`

s yield `unknown`

.

My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second
`check-sat`

. The latter could also explain why both `check-sat`

s yield
`unknown`

if `push`

/`pop`

is used because Z3 will (as far as I understand) switch to incremental mode on first
`push`

.

**Question:** Is it a bug or an expected consequence?

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

In Z3, soft constraints can be implemented by placing the actual constraint
`P`

on the right-hand side of an implication whose left-hand side is a fresh boolean variable, e.g.
`assert (=> b1 P)`

. Constraints can then be "switched on" per ```
check-sat
```

by listing `b`

s which are to be considered true, e.g.
`(check-sat b1)`

.

**Question:** What happens with such constraints `P`

if their guard variable
`b`

is **not** included in a `check-sat`

? I assume Z3 treats
`b`

's value as unknown, and then branches over the implication/over ```
b
```

's value - is that correct?

**Background:** The background of my question is that I use Z3 in incremental mode (`push`

/`pop`

blocks), and that I check assertions
`P`

by `(push)(assert (not P))(check-sat)(pop)`

; if the ```
check-sat
```

is `unsat`

then `P`

holds.

I thought about using soft constraints instead, i.e. to replace each such `push`

/`pop`

block by
`(declare-const b_i Int)(assert (=> b_i P))(check-sat b_i)`

. Each ```
b_i
```

would only be used once. However, if Z3 may branch over all previous ```
b_j
```

, then it sounds as if that might potentially slow down Z3 quite a bit - hence my question.

(P.S.: I am aware of this answer by Leo, which says that soft constraints might also reduce performance because certain optimisations might not be applicable.)

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

I am trying to evaluate resultant matrix by asserting constraint on matrix multiplication using z3py API. The following method works for matrix addition. Following is the code, which have 3 matrices: x, y, and sol.

sol is the addition of x and y (sol==x+y), I am interested to restrict the values of resultant matrix (sol) to zero, and check which unknown values in "x" and "y" yield resultant matrix to be zero. Following is the list comprehension approach for addition.

```
from z3 import*
x = [ [Real("x_%s_%s" %(i+1, j+1)) for j in range(2) ] for i in range(2)]
y = [ [Real("y_%s_%s" %(i+1, j+1)) for j in range(2) ] for i in range(2)]
sol = [ [Real("sol_%s_%s" %(i+1, j+1)) for j in range(2) ] for i in range(2)]
addition = [sol[i][j]==x[i][j]+y[i][j] for i in range(2) for j in range(2) ]
s = Solver()
s.add(addition)
s.add(x[0][0]>=0)
s.add(x[0][1]>=0)
s.add(x[1][0]>=0)
s.add(x[1][1]>=1)
s.add(And(y[0][0]>=0, y[0][0]<=2))
s.add(And(y[0][1]>=0, y[0][0]<=2))
s.add(And(y[1][0]>=0, y[0][0]<=2))
s.add(And(y[1][1]>=0, y[0][0]<=2))
s.add(sol[0][0]==0)
s.add(sol[0][1]==0)
s.add(sol[1][0]==0)
s.add(sol[1][1]==0)
if s.check()==sat:
m =s.model()
print SAT,'\n', m
result=[[ m.evaluate(sol[i][j]) for i in range (2)] for j in range (2)]
print result
if (s.check()==unsat):
print "UNSAT, no model exists"
```

Now, is there any way in list comprehension through which I can assert matrix multiplication? (sol==x*y)...?

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

I need to use `Z3_parse_smtlib2_string`

to parse some SMTLIB strings into Z3 using the C++ API, and the use the Z3 C++ API to find the unsat core of this.

I know that there are other ways to find the unsat core as described here and here that are easier and less cumbersome, but I really want to be able to do this using only data structures parsed from strings to Z3. The reason is that I am trying to automate something using Z3.

It is obvious that if I passed this SMTLIB program into Z3, it is UNSAT.

```
(declare-const p0 Bool)
(assert(= p0 true)) (assert(= p0 false))
(assert (exists ((x Int)) (= 3 x)))
```

What I want to do, is to be able to get the unsat core programmatically using Z3. What I did was to read each of those lines separately into Z3 and give them a name using
`solver.add(expr, name)`

, using the program below.

```
void my_test() {
context c1;
solver s(c1);
std::string declare = "(declare-const p0 Bool)";
std::string testing = "(assert(= p0 true)) (assert(= p0 false))";
std::string obvious = "(assert (exists ((x Int)) (= 3 x)))";
Z3_ast parsed1 = Z3_parse_smtlib2_string(c1, declare.c_str(), 0,0,0,0,0,0);
expr e1(c1, parsed1);
Z3_ast parsed2 = Z3_parse_smtlib2_string(c1, testing.c_str(), 0,0,0,0,0,0);
expr e2(c1, parsed2);
std::cout << "what: " << e2 << std::endl;
Z3_ast parsed3 = Z3_parse_smtlib2_string(c1, obvious.c_str(), 0,0,0,0,0,0);
expr e3(c1, parsed3);
s.add(e1, "declare");
s.add(e2, "testing");
s.add(e3, "obvious");
if (s.check() == z3::sat) {
std::cout << "SAT!\n";
model m = s.get_model();
std::cout << m << std::endl;
} else {
std::cout << "UNSAT!\n";
expr_vector core = s.unsat_core();
std::cout << core << "\n";
std::cout << "size: " << core.size() << "\n";
for (unsigned i = 0; i < core.size(); i++) {
std::cout << core[i] << "\n";
}
}
}
```

I expect to get the unsat core to be just `declare`

, since that is clearly false, while the other expressions are clearly valid. However, Z3 gives me this response:

```
(error "line 1 column 11: unknown constant p0")
(error "line 1 column 31: unknown constant p0")
what: true
SAT!
(define-fun testing () Bool
true)
(define-fun declare () Bool
true)
(define-fun obvious () Bool
true)
```

Which is clearly wrong, since `declare`

, which references `(assert(= p0 true)) (assert(= p0 false))`

, is SAT! Obviously this should be UNSAT. Also, I do in fact declare
`p0`

, but Z3 doesn't seem to know that I declared it already.

Any ideas what I'm doing wrong?

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

Given the following input

```
(set-option :auto_config false)
(set-option :smt.mbqi false)
(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)
(define-fun FOO () Bool
(forall ((i Int)) (!
(implies
(and (<= 0 i) (< i (len x)))
(exists ((j Int)) (!
(implies
(and (<= 0 j) (< j (len x)))
(> (idx x j) 0))))))))
(assert FOO)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
; (push)
(assert (not FOO))
(check-sat)
; (pop)
```

Z3 4.3.2 x64 reports `unsat`

for the first `check-sat`

(as expected), but
`unknown`

for the second. If the commented `push`

/`pop`

s are uncommented, both
`check-sat`

s yield `unknown`

.

My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second
`check-sat`

. The latter could also explain why both `check-sat`

s yield
`unknown`

if `push`

/`pop`

is used because Z3 will (as far as I understand) switch to incremental mode on first
`push`

.

**Question:** Is it a bug or an expected consequence?

active questions tagged z3 - Stack Overflow News Feed

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