CodePlexProject Hosting for Open Source Software

active questions tagged z3 - Stack Overflow News Feed

Thursday, September 3, 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.

Thursday, September 3, 2015 | From
active questions tagged z3 - Stack Overflow

I have installed:

- Latest version of why3: 0.86.1
- Latest version of frama-c: Sodium-20150201
- Jessie3 plugin for frama-c taken from the Why3 tarball
- Z3 4.3.1 (from the github tag)
- A bunch of other solvers
`why3 config --detect`

:

```
Found prover Alt-Ergo version 0.95.2, Ok.
Found prover CVC3 version 2.4.1, Ok.
Found prover Gappa version 1.2.0, Ok.
Found prover Simplify version 1.5.4 (old version, please consider upgrading).
Found prover Spass version 3.7, Ok.
Found prover Z3 version 4.3.1 (old version, please consider upgrading).
Found prover Coq version 8.4pl3, Ok.
warning: Warning: prover Yices version 2.4.1 is not known to be supported.
warning: Warning: prover veriT version 201506 is not known to be supported.
warning: Warning: prover Yices version Yices is not known to be supported.
7 provers detected and 3 provers detected with unsupported version
== Found /usr/local/lib/why3/plugins/dimacs.cmxs ==
== Found /usr/local/lib/why3/plugins/genequlin.cmxs ==
== Found /usr/local/lib/why3/plugins/tptp.cmxs ==
Save config to /home/necto/.why3.conf
```

Now trying to run Jessie3:

```
$frama-c -jessie3 discriminant.c
```

Yields:

```
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing discriminant.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] failure: Prover Z3,3.2 not installed or not configured
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.AbortFatal("jessie3")
[kernel] Current source was: discriminant.c:47
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 79, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
```

Note: The same message, but about the `Z3,4.3.1`

I had when I first installed the brand new Z3 from master branch in their github repo.

Do I really need two versions of Z3 (`4.3.1`

and `3.2`

) simultaneously to run the Jessie3 plugin? How can I install both of them?

Wednesday, September 2, 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(10):
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, the time spent on the inference might be reduced. I am not sure if this makes sense.

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

Below solution i am not able to implement in java. Please help me. Below is snippet code which i am trying to implement.

I found the same question:

Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

```
BitVecExpr a = ctx.mkBVConst("a",8);
BitVecExpr b = ctx.mkBVConst("b",8);
BitVecExpr c = ctx.mkBVConst("c",8);
Solver s = ctx.mkSolver();
//s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b))); // I am able to get distinct value for a and b for XOR.
//s.add(ctx.mkEq(c,ctx.mkBVOR(b,a))); // If i swap the position of the a and b then i was able to generate distinct pattern. For example for this add method of OR my code was working.
s.add(ctx.mkEq(c,ctx.mkBVOR(a,b))); // Not working getting same model.
s.add(ctx.mkEq(c,ctx.mkBV(11,8)));
if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}
BitVecExpr test1[] = {a,b};
s.add(ctx.mkDistinct(test1)); // If i use this line then only i get distinct pattern
if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}
```

Also i don't have model()[] method in java.In java i have getModel() method without any arguments.

One more question. How can we implement '!=' inside add. For example.

s.add(Or(a != s.model()[a], b != s.model()[b]))

For == we have mkEq() method, But i was unable to find any method related to '!='.

I tried using:

s.add(ctx.mkOr(ctx.mkEq(a,ctx.mkNot(s.getModel())),ctx.mkEq(a,ctx.mkNot(s.getModel()))));

For which i am getting compilation error. Which i should get because its not possible to implement in that way.

Monday, August 31, 2015 | From
active questions tagged z3 - Stack Overflow

How does one use the 'repeat' and 'rotate_left' bitvector operations?

More generally, where can I find detailed documentation of bitvector operations in the SMT2 scripting format used by Z3?

Everything I find seems to just go to tutorials, or broken links:

https://github.com/Z3Prover/z3/wiki/Documentation

http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html

Trying to understand "repeat", "rotate_left", and "rotate_right" by guessing has been frustating. I cannot figure out how to use them. For example

```
(display (repeat #b01))
(display (repeat #b01 3))
(display (repeat 3))
(display (rotate_left #b0001 2))
```

gives

```
"repeat expects one non-zero integer parameter"
"repeat expects one argument"
"operator is applied to arguments of the wrong sort"
"rotate left expects one argument"
```

Where is the documentation? Hoping they didn't explain because all of this is standard, I also looked at smt-lib.org but that doesn't list these details either. So frustrating.

Saturday, August 29, 2015 | From
active questions tagged z3 - Stack Overflow

Below solution i am not able to implement in java. Please help me. Below is snippet code which i am trying to implement.

I found the same question:

Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

```
BitVecExpr a = ctx.mkBVConst("a",8);
BitVecExpr b = ctx.mkBVConst("b",8);
BitVecExpr c = ctx.mkBVConst("c",8);
Solver s = ctx.mkSolver();
//s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b))); // I am able to get distinct value for a and b for XOR.
//s.add(ctx.mkEq(c,ctx.mkBVOR(b,a))); // If i swap the position of the a and b then i was able to generate distinct pattern. For example for this add method of OR my code was working.
s.add(ctx.mkEq(c,ctx.mkBVOR(a,b))); // Not working getting same model.
s.add(ctx.mkEq(c,ctx.mkBV(11,8)));
if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}
BitVecExpr test1[] = {a,b};
s.add(ctx.mkDistinct(test1)); // If i use this line then only i get distinct pattern
if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}
```

Also i don't have model()[] method in java.In java i have getModel() method without any arguments.

One more question. How can we implement '!=' inside add. For example.

s.add(Or(a != s.model()[a], b != s.model()[b]))

For == we have mkEq() method, But i was unable to find any method related to '!='.

I tried using:

s.add(ctx.mkOr(ctx.mkEq(a,ctx.mkNot(s.getModel())),ctx.mkEq(a,ctx.mkNot(s.getModel()))));

For which i am getting compilation error. Which i should get because its not possible to implement in that way.

Friday, August 28, 2015 | From
active questions tagged z3 - Stack Overflow

I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:

```
(declare-const f Bool)
(assert (or (= f true) (= f false)))
```

In this propositional case there are two satisfying assignments: `f->true`

and
`f->false`

. Because Z3 (and SMT solvers in general) will only try to find one satisfying model, finding all solutions is not directly possible.
Here I found a useful command called `(next-sat)`

, but it seems that the latest version of Z3 no longer supports this. This is bit unfortunate for me, and in general I think the command is quite useful. Is there another way of doing this?

Friday, August 28, 2015 | From
active questions tagged z3 - Stack Overflow

I would like to ask how I can encode functions whose ranges are set of subsets.

For example, I have a set Proc = {1, 2, 3} and a set Number = {4, 5, 6}. And now I would like to declare a function "fcn" from Proc to a set of subsets of Number. I intend to use 8 variables for each subsets of Number by declaring:

```
(declare-fun var1 (Int) Bool)
(assert (= (var1 4) true))
(assert (= (var1 5) true))
(assert (= (var1 6) true))
...
(declare-fun var8 (Int) Bool)
(assert (= (var8 4) false))
(assert (= (var8 5) false))
(assert (= (var8 6) false))
```

I guess, "fcn" should be (declare-fun fcn (Int) ...). Unfortunately, I don't kown how to declare the range of "fcn".

Thank you very much.

Thursday, August 27, 2015 | From
active questions tagged z3 - Stack Overflow

We are experiencing widely diverging SAT times for two (nearly) equivalent formulas.

Examples in SMT-LIBv2 are available here:

https://gist.github.com/martin-neuhaeusser/e67999b63f749e5ecf1e

Some background:

The two formulas come from the same abstract post computation in a CEGAR framework. One was generated using the classic weakest precondition algorithm while the other was generated using a more efficient implementation. In a few words, it tries to work around
exponential blowup by introducing intermediate variables.

We use Z3 incrementally in our application and keep our predicates using activation literals on the solver stack.

The WP from the classic algorithm can be simplified and checked in roughly 30ms whereas Z3 (unstable branch) needs at least 1.6 seconds to check the other formula (on my machine). The files in the above link reproduce the behavior of our application.

What is the likely cause of this discrepancy? Can this be avoided?

Is this related to the incremental solver that we use and if so, which tactics can be used to create a (better) incremental solver?

Any help is highly appreciated!

Wednesday, August 26, 2015 | From
active questions tagged z3 - Stack Overflow

My z3py code is doing inference and experiencing some performance (latency) issues. Currently I am trying to come up with some heuristics to prune the search space to hopefully boost the speed of inference.

My question is: do the orders of constraints being asserted affect the orders they are evaluated? In other words, if a constraint can significantly reduce the search space, should I assert it first so that, after being evaluated, many impossible solutions will be rule out at an early stage?

Tuesday, August 25, 2015 | From
active questions tagged z3 - Stack Overflow

I did some experiments with the latest unstable versions of 4.4.1 and concluded that soft assertions just work fine for me as in the example below:

```
(assert(! ((and ( <= P291 200)( >= P291 100))) :named R291mm ))
(assert-soft(! (( = P291 170)) :named R291d ):weight 7)
```

P291 has a min and a max value (100, 200) - defined as hard constraints - and a default, which should be chosen if no other constraints are influencing the value.

With Z3 on the command line console I get the expected results, but as soon as I'm using my DotNet application, read the very same file via ParseSMTLIB2File and feed the expressions to the solver with Assert or AssertAndTrack (other methods are not defined) the soft assertions seem to get ignored. A closer look in the debugger shows that only the hard constraints can be found in Args. So ParseSMTLIB2File seems not to be prepared to read soft constraints.

Do I have to set special options with the context or am I just too early?

If I'm too early :are there plans to make soft constraints available via the DotNet API? If the answer is positive, what will be the timeframe?

Thx

Christian J

Tuesday, August 25, 2015 | From
active questions tagged z3 - Stack Overflow

Or is it purely the solving time? This question is for the case when z3 is being called as an external binary. I am asking this as in some of my examples, the constraint solving time is small and I suspect will become comparable to file read time. Also, how accurate is the total-time for small values (< 1s for example)?

Tuesday, August 25, 2015 | From
active questions tagged z3 - Stack Overflow

In a (rather large) Z3 problem, we have a few axioms of the shape:

`forall xs :: ( (P(xs) ==> (exists ys :: Q(xs,ys))) && ((exists zs :: Q(xs,zs)) ==> P(xs)) )`

All three quantifiers (including the existentials) have explicit triggers provided (omitted here). When running the problem and gathering quantifier statistics, we observed the following data (amongst many other instantiations):

`[quantifier_instances] k!244 : 804 : 3 : 4 `

[quantifier_instances] k!232 : 10760 : 29 : 30

Here, line 244 corresponds to the end of the outer `forall`

quantifier, and line 232 to the end of the
*first* inner `exists`

. Furthermore, there are no reported instantiations of the
*second* inner `exists`

(which I believe Z3 will pull out into a
`forall`

); given the triggers this is surprising.

My understanding is that existentials in this inner position should be skolemised by a function (depending on the outer quantifier). It's not clear to me what quantifier statistics mean for such existentials.

Here are my specific questions:

- Are quantifier statistics meaningful for existential quantifiers (those which remain as existentials - i.e. in positive positions)? If so, what do they mean?
- Does skolemisation of such an existential happen once and for all, or each time the outer quantifier is instantiated? Why is a substantially higher number reported for this quantifier than for the outer forall?
- Does Z3 apply some internal rewriting of this kind of (A==>B)&&(B==>A) assertion? If so, how does that affect quantifier statistics for quantifiers in A and B?

From our point of view, understanding question 2 is most urgent, since we are trying to investigate how the generated existentials affect the performance of the overall problem.

The original smt file is available here:

https://gist.github.com/anonymous/16e489ce5c513e8c4bc6

and a summary of the statistics generated (with Z3 4.4.0, but we observed the same with 4.3.2) is here:

https://gist.github.com/anonymous/ce7b96acf712ac16299e

Tuesday, August 25, 2015 | From
active questions tagged z3 - Stack Overflow

I am beginner, start with Z3 in C# program, because I want to simplify two logic formula to one logic formula. But I don't know how to using Z3 API in C# program?

how I solve this issue? (install and using API in C#)

```
Example:
F1: X > 1
F1: X > 100
=> Solve: X > 100
```

Could you help me please?

Tuesday, August 25, 2015 | From
active questions tagged z3 - Stack Overflow

I am beginner, start with Z3 in C# program, because I want to simplify two logic formula to one logic formula. But I don't know how to using Z3 API in C# program?

how I solve this issue? (install and using API in C#)

```
Example:
F1: X > 1
F1: X > 100
=> Solve: X > 100
```

Could you help me please?

Monday, August 24, 2015 | From
active questions tagged z3 - Stack Overflow

I'm a beginner with Z3. I just have tried some of the examples released in Z3 package, and I have no the other experience any more. I am working with a problem about shortest path in a graph. Can I do it by Z3 ? Thanks you all.

Monday, August 24, 2015 | From
active questions tagged z3 - Stack Overflow

Basically, I want to ask Z3 to give me an arbitrary integer whose value is greater than 10. So I write the following statements:

```
(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))
```

How can I apply this quantifier to my model? I know you can write `(assert (> x 10))`

to achieve this, but I mean I want a quantifier in my model so every time I declare an integer constant whose value is guaranteed to be over 10, so that I
don't have to insert statement `(assert (> x 10))`

for every integer constant that I declared. If I have to use macros to prevent repeating code, what is the actual use of quantifiers?

Sunday, August 23, 2015 | From
active questions tagged z3 - Stack Overflow

I try running example with Z3 API in C# program, but It has a issues below.

Can you help me solve this problem, please?

Thursday, August 20, 2015 | From
active questions tagged z3 - Stack Overflow

I am new to Z3Py (and Z3). The following code returns `unsat`

as expected:

```
from z3 import Ints, Tactic, Exists, And, Implies, ForAll, Bool, Solver, IntSort, BoolSort, Function
s = Solver()
t, a, t0 = Ints('t a t0')
p = Function('p', IntSort(), IntSort(), BoolSort())
facts = [
t >= 1,
t <= 2,
Implies(And([t>0, t <= 1]), p(t, 1) == False),
Implies(And([t>1, t <= 2]), p(t, 1) == True),
]
query = Implies(t == 2, Exists(t0, And([t0 == t, t0 >= 1, t0 <= 2, p(t0, 1) == True])))
f = Implies(And(facts), query)
s.add(Tactic('qe')(Not(f)).as_expr())
print s.check() # unsat means f is valid
```

If I now change `query`

to

```
query = Implies(t == 1, Exists(t0, And([t0 > t, t0 >= 1, t0 <= 2, p(t0, 1) == True])))
```

it prints `sat`

though I was expecting `unsat`

as ```
t0 == 2
```

is the required witness for the quantifier. Would appreciate any insight on this, thank you.

Thursday, August 20, 2015 | From
active questions tagged z3 - Stack Overflow

I try running example with Z3 API in C# program. But It has a issues below.

Can you help me solve this problem, please?

active questions tagged z3 - Stack Overflow News Feed

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