Stack Overflow
Stack Overflow

Questions tagged [z3py]

Python interface for the Z3 Theorem Prover

z3py - Python interface for the Z3 Theorem Prover. Z3 is a high-performance theorem prover. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers.

834 questions
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
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
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
9
votes
1 answer

Multi-threaded Z3?

I'm working on a Python project, where I'm currently trying to speed things up in some horrible ways: I set up my Z3 solvers, then I fork the process, and have Z3 perform the solve in the child process and pass a pickle-able representation of the…
Zardus
  • 316
  • 2
  • 7
9
votes
1 answer

Z3py: how to get the list of variables from a formula?

In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula? Thanks.
user311703
  • 1,113
  • 2
  • 14
  • 25
8
votes
2 answers

Python -- Optimize system of inequalities

I am working on a program in Python in which a small part involves optimizing a system of equations / inequalities. Ideally, I would have wanted to do as can be done in Modelica, write out the equations and let the solver take care of it. The…
Gerome Pistre
  • 457
  • 6
  • 15
7
votes
1 answer

z3: solve the Eight Queens puzzle

I'm using Z3 to solve the Eight Queens puzzle. I know that each queen can be represented by a single integer in this problem. But, when I represent a queen by two integers as following: from z3 import * X = [[Int("x_%s_%s" % (i+1, j+1)) for j in…
Tan
  • 115
  • 7
7
votes
2 answers

How to use Z3py and Sympy together

I am trying to perform some symbolic calculation on matrices (with symbols as an entries of matrices), and after that I will have a number of possible solution. My goal is to select solutions/ solution based upon constraints. for example, M is a…
user3196876
  • 187
  • 1
  • 12
6
votes
1 answer

Solving formulas in parallel with z3

Let's say I have a z3 solver with a certain number of asserted constraints that are satisfiable. Let S be a set of constraints, I would like to verify for every constraint in S whether the formula is still satisfiable when adding the constraint to…
Michael Blondin
  • 160
  • 7
6
votes
1 answer

How to use Z3 SMT-LIB online to solve problems with Operational Amplifiers

In a previous post some problems involving operational amplifiers were solved using Z3Py online. But now that Z3Py online is out of service I am trying to solve such problems using Z3 SMT-LIB online. Example 1: Find the value of R in the following…
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
6
votes
2 answers

Check overflow with Z3

I'm new to Z3 and I was checking the online python tutorial. Then I thought I could check overflow behavior in BitVecs. I wrote this code: x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) and I was expecting [y…
Braulio Horta
  • 160
  • 10
6
votes
1 answer

Need help understanding the equation

Have the equation Pell x*x - 193 * y*y = 1 in z3py: x = BitVec('x',64) y = BitVec('y',64) solve(x*x - 193 * y*y == 1, x > 0, y > 0) Result: [y = 2744248620923429728, x = 8169167793018974721] Why? P.S. Valid answer: [y = 448036604040, x =…
Sergey Fe
  • 63
  • 4
5
votes
1 answer

How get a a value from a Lambda expression?

I'm experimenting with z3 in python. I have the following model: (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert…
Alberto
  • 446
  • 5
  • 14
5
votes
2 answers

How to use z3 BitVec or Int as an array index?

I want to use a Int vector as an array index. python. array = [12,45,66,34] s= Solver() x = Int('x') s.add(array[x] == 66) so the x should be 2.. how can i do it?
pandaos
  • 51
  • 1
  • 3
5
votes
1 answer

Does Z3py support "String" and "Sequence"

In Z3, it supports String and Sequence. But does Z3py supports them as well, or we have to use string or list from Python? From the latest release, it seemed that the new version did support the theories of String and Sequence, but I don't know how…
Kun
  • 101
  • 3
1
2 3
…
55 56