Stack Overflow
Stack Overflow

Questions tagged [z3]

Z3 is a high-performance theorem prover being developed at Microsoft Research.

Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers.

Some key features of Z3 are:

  • High-performance theorem prover
  • Integrating efficient constraint solving technologies
  • Checking satisfiability of logical formulas with quantifiers
  • Highly customizable with an extensive API
  • Including support for custom theories

For more information about Z3, visit the Z3 homepage or try Z3 in your browser.

See also Z3 tutorial guide for more in-depth introduction about Z3.

2824 questions
54
votes
1 answer

How incremental solving works in Z3?

I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following: There are two ways to use Z3 for incremental solving: one is push/pop(stack) mode, the other is using assumptions.…
Tianhai Liu
  • 795
  • 5
  • 10
47
votes
1 answer

Difference between Z3 and coq

I am wondering if someone can tell me the difference between Z3 and coq? Seems to me that coq is a proof assistant in that it requires the user to fill in the proof steps, whereas Z3 does not have that requirement. But seems like coq also has auto…
JRR
  • 6,014
  • 6
  • 39
  • 59
40
votes
2 answers

Z3: finding all satisfying models

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…
marczoid
  • 1,365
  • 2
  • 12
  • 20
35
votes
2 answers

Windows: Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")

I am running into the following error when using a python script (oyente) that uses Z3 (which I've built in the Visual Studio command prompt): File "C:\Python27\Lib\site-packages\oyente\z3\z3core.py", line 23, in lib raise…
ZhouW
  • 1,187
  • 3
  • 16
  • 39
35
votes
1 answer

How does Z3 handle non-linear integer arithmetic?

I am aware that the theory of integers with multiplication is generically undecidable. Nevertheless, in certain instances, Z3 does return a model. I am curious to know how this is done. Does it have something to do with the new decision procedure…
Arvind Haran
  • 710
  • 7
  • 14
24
votes
4 answers

(Z3Py) checking all solutions for equation

In Z3Py, how can I check if equation for given constraints have only one solution? If more than one solution, how can I enumerate them?
user313885
21
votes
2 answers

Reasoning about reals

I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values: class Test { //@ requires b > 0; void a(double b) { } void b() { a(2.4); } } I have already found out OpenJML uses AUFLIA…
nhaarman
  • 98,571
  • 55
  • 246
  • 278
20
votes
1 answer

K-out-of-N constraint in Z3Py

I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,..,xN. I want to express the constraint that exactly K out of N of them should be true. How can I do that, in Z3Py? Is there any built-in support for…
D.W.
  • 3,382
  • 7
  • 44
  • 110
19
votes
3 answers

Finding all the combinations of free polyominoes within a specific area with a SAT-solver (Python)

I am new to the world of SAT solvers and would need some guidance regarding the following problem. Considering that: ❶ I have a selection of 14 adjacent cells in a 4*4 grid ❷ I have 5 polyominoes (A, B, C, D, E) of sizes 4, 2, 5, 2 and 1 ❸ these…
solub
  • 1,291
  • 17
  • 40
18
votes
1 answer

Z3/Python getting python values from model

How can I get real python values from a Z3 model? E.g. p = Bool('p') x = Real('x') s = Solver() s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p)) s.check() print s.model()[x] print s.model()[p] prints -1.4142135623? False but those are Z3…
sqx
  • 183
  • 1
  • 1
  • 5
14
votes
1 answer

Equivalent of define-fun in Z3 API

Using Z3 with the textual format, I can use define-fun to define functions for reuse later on. For example: (define-fun mydiv ((x Real) (y Real)) Real (if (not (= y 0.0)) (/ x y) 0.0)) I wonder how to create define-fun with Z3 API (I…
pad
  • 41,040
  • 7
  • 92
  • 166
14
votes
2 answers

Has anyone tried proving Z3 with Z3 itself?

Has anyone tried proving Z3 with Z3 itself? Is it even possible, to prove that Z3 is correct, using Z3? More theoretical, is it possible to prove that tool X is correct, using X itself?
Longfei Zhu
  • 149
  • 3
14
votes
1 answer

Defining a Theory of Sets with Z3/SMT-LIB2

I'm trying to define a theory of sets (union, intersection etc.) for Z3 using the SMTLIB interface. Unfortunately, my current definition hangs z3 for a trivial query, so I guess I'm missing some simple option/flags. here's the permalink: …
Ranjit Jhala
  • 1,242
  • 8
  • 18
12
votes
2 answers

Symbolic theory proving using SBV and Haskell

I'm using SBV (with Z3 backend) in Haskell to create some theory provers. I want to check if forall x and y with given constrains (like x + y = y + x, where + is a "plus operator", not addition) some other terms are valid. I want to define axioms…
Wojciech Danilo
  • 11,573
  • 17
  • 66
  • 132
10
votes
2 answers

Use of term rewriting in decision procedures for bit-vector arithmetic

I am working on a project whose focus is the use of term rewriting to solve/simplify fixed-size bit-vector arithmetic problems, which is something useful to do as a prior step to some decision procedure such as those based on bit-blasting. The term…
iago
  • 277
  • 1
  • 10
1
2 3
…
99 100