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?

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?

Recently I am learning SMT solver. Although SMT solver is a new concept to me, it reminds me of logic programming, e.g. Prolog and minikanren. So I tried a classic example of logic programming in S...

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 im...

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, ...

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 ...

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 equa...

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/ solu...

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 ...

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 pro...

I'm trying to influence the randomness of results for model values generated by Z3. As far as I understand, the options for this are very limited: in case of linear arithmetic, the simplex solver d...

I have been trying to solve a small problem which includes absolute value of some terms. In z3 there is no support for abs() function. In python there is, but I eventually i have to pass it to z3py...

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 onlin...

I am using Z3's python api to do some kind of incremental solving. I push constraints to the solver iteratively while checking for unsatisfiability at each step using solver.push() command. I want ...

Suppose that a is an integer of 8-bit of value 254. If a is a signed integer, it is actually considered -2. In contrary, if a is unsigned, it remains 254. I am trying to model this signed/unsigned...

Over the years I keep track of solving technology - and I maintain a blog post about applying them to a specific puzzle - the "crossing ladders". To get to the point, I accidentally found out abo...

In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula? Thanks.

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.mode...

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 = 81691677930189747...