Questions tagged [z3]
Z3 is a high-performance theorem prover being developed at Microsoft Research.
2,777
questions
0
votes
1
answer
40
views
Can I use quantifier elimination to get models for 'c' in formulae like ∃a.∀b.∃c.∀d. Phi?
Consider I have a formula with the shape: ∃a.∀b.∃c.∀d. Phi, where a,b,c,d belong to some first-order theory T that admits quantifier elimination.
If I would like to get a model of this formula in Z3, ...
0
votes
1
answer
34
views
What does a model in ∃x∀y∃z∀u . F[x, y, z, u] mean?
In Playing with Quantified Satisfaction they state as follows:
Evaluating a quantified formula of the form ∃x∀y∃z∀u . F[x, y, z, u]
can be naturally seen as a game between two parties: the ...
0
votes
1
answer
16
views
datalog_frontend.cpp ..\src\shell\datalog_frontend.cpp(20): fatal error C1083: Cannot open include file: 'iostream': No such file or directory
I want to install z3 on windows 10
I clone the project and do python scripts/mk_make.py
and at the end, I want to run nmake in the build directory of the project but I got the following error
...
0
votes
1
answer
13
views
Modeling crossword-construction in z3
I'm working on a program to generate crossword puzzles. The task is: given a grid, is there a way to fill the grid with letters such that each clue (acrosses and downs) is a valid word?
This can be ...
0
votes
2
answers
38
views
Assign true to all variable except one
I have a list of variables and I want to add constraint to z3 solver such as all variables should be False except one variable should be True ..
a,b,c,d= Bool('a,b,c,d')
s = Solver()
allvariables=[a,b,...
0
votes
0
answers
53
views
Pyinstaller + Z3-solver problem (hidden console)
Hello I am working on tkinter application. In my application I got button. After pressing this button I am doing some z3-solver stuff. My problem is that I wanted to create exe file by using ...
1
vote
1
answer
22
views
z3py: How to write a constraint for an array to be sorted?
I'm trying to create a constraint to create a "sorted" copy of an arrayOld(int, int).
With "sorted" I mean, that:
for any x >= y which have a value stored in arrayOld, it ...
0
votes
2
answers
47
views
Specifying modular arithmetic conditions in Z3
How do I specify a modular artithmetic condition such as
f1 := (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 1 (mod 5)) ∨
(b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 2 (...
0
votes
0
answers
15
views
Z3 best practices for enumeration datatype problems
I am trying to solve an AI planning problem using Z3.
The encoding that I use is made of boolean variables and enumeration datatype. I can have up to millions formulas and variables, and speed is ...
0
votes
1
answer
37
views
How would I import z3 solver in pyodide
I am trying to recreate a python project that uses z3 solver, which is not very supported on JS (especially on html)
I found that I could use pyodide for doing python code and make this project a lot ...
0
votes
1
answer
24
views
Does Z3 solver internally unnests nested function terms
I was wondering if the Z3 solver (perhaps only in some circumstances) uses a graph of a function to unnest a nested function term by introducing a new quantified variable.
For example: f(g(5)) = 10 ...
0
votes
1
answer
34
views
Z3 Get solutions without overflow using bitVecs
I found this post that gives a way of checking for overflow in solutions when adding bitVecs
z3 bitvector overflow checking from python?
However, it only works when only adding 2 bitVecs, is there any ...
0
votes
1
answer
32
views
Z3 gives no or wrong solution when there are a right solution
I am writing a problem with BitVecs as I have to do bit-blasting later. I have a sum constraint. To avoid overflow solutions, e.g. x0 = BitVec('x0',2) and x1 = BitVec('x1',2), x0+x1==2 gives the ...
1
vote
1
answer
26
views
z3 - Assert the # of elements with value x == # of elements with value y?
I have some string constants in z3, e.g.
boxes = [String(x) for x in range(10)]
# Valid values are x or y
for box in boxes:
s.add(Or([box == val for val in 'xy']))
How would I add the constraint ...
0
votes
1
answer
44
views
Dump z3's configuration?
Is there a way to have Z3 dump all its settings when run from the CLI and from Python?
I have a large optimizer (maxsat) program that runs in 2m from the CLI but never finishes when run in Python and ...
0
votes
2
answers
38
views
Bit blasting gives answers that do not live up to the constraints
I am using z3 to do bit blasting. I then solve the problem in a SAT solver, and do reverse bit blasting in order to find out what value the varibles take. However, I find that the solutions I get ...
0
votes
1
answer
27
views
Implementation for decision procedure for the theory of the reals
Is there an implementation for the first-order theory of the reals? I know there exists one technique by Collins based on cylindrical algebraic decomposition but I don't know of any theorem provers ...
1
vote
1
answer
43
views
z3 fails to solve problem with square root
I'm trying to solve simple problem which involves calculating square root, yet for some reason z3 throws an error like failed to solve or z3types.Z3Exception: model is not available
from z3 import *
...
0
votes
1
answer
32
views
Best Z3 tactics for elementary algebra of fields
I want to use Z3 to proof validity of statements like this:
∀ a b: ℤ, ~ b = 0 -> (a / b) ^ 2. = (a * a) / (b * b)
Or in SMT-LIB format:
(declare-fun b () Int)
(declare-fun a () Int)
(assert (=> ...
0
votes
1
answer
32
views
Function seq.fold_left
I am unable to successfully utilize the seq.fold_left function.
(declare-const s (Seq Int))
(declare-const t (Seq Int))
(declare-fun f (Int Int) Int)
(define-fun sum_seq ((s (Seq Int)))
(seq....
0
votes
1
answer
48
views
Is there a good algorithm for the minimal computation of a CNF without extra variables?
I'm currently working on tranforming logical queries for database systems from a DNF form into a CNF form, focussed on queries which have a similar form to
(a and b and c and d and e1) or (a and b and ...
1
vote
1
answer
63
views
Can SMT solver like Z3 prove 1+2+...+n = n(n+1)/2?
The theorem 1+2+...+n = n(n+1)/2 seems to be provable by first translating it to CNFs and repeatedly applying resolution rules to them, as discussed in the introduction section of [1]. I believe this ...
0
votes
0
answers
27
views
How do I obtain IndexedIdentififers and ParametricSorts using Z3 C++ API?
The SMT standard allows identifiers such as
( _ vector-add 4 5)
called indexed identifiers.
It also allows parametric sorts such as
( Set ( _ Bitvec 3))
That combines a parametric sort Set with the ...
0
votes
1
answer
28
views
A Skolem model in Z3 should be unique, but is printing several (and repeated)
I am testing how similar are "assignment"-like models and "Skolem-function"-like models in Z3.
Thus, I proposed an experiment: I will create a formula for which the unique model is ...
0
votes
1
answer
29
views
"Intersection" of two Skolem functions is not as expected in Z3(Py)
Z3(Py) does not “intersect” Skolem functions as I expected.
I will try to explain my doubt using an imaginary problem which is the one that I have been testing on.
Consider a system that has two ...
0
votes
0
answers
35
views
Why is Z3 unable to prove `unsat` for this query, whereas cvc5 succeeds?
I have a (relatively) simple query attached below
(set-logic AUFLIRA)
(set-option :produce-models true)
(declare-sort Loc 0)
(declare-sort HeapChunk 0)
(declare-sort HeapIndex 0)
(declare-fun ...
0
votes
1
answer
48
views
Z3 optimize by index not a value
With greate respect to the answer of @alias there: (Find minimum sum) I would like to solve similar puzzle. Having 4 agents and 4 type of works. Each agent does work on some price (see initial matrix ...
0
votes
1
answer
62
views
Can Z3 fpRealToFP be used for practical floating point accuracy proofs?
I would like to use Z3 to prove the accuracy of certain floating point expressions. My plan was to:
Implement the expression as Reals.
Implement the same expression as Float32().
Use fpRealToFP to ...
2
votes
1
answer
56
views
z3 solver using Sympy symbols
I'm trying to use Z3 to determine if an expression is satisfiable.I have created all equations that I want to use it as constraints using SymPy and the variables are Symbols.
the equations for example
...
0
votes
1
answer
30
views
How to check in Z3py whether the expression contains a specific variable or expression?
I'm using z3py, how do I check whether an expression contains a given variable or expression? For example,
x = Int('x')
expr = x + 1
So, expr should contains variable x.
I've checked the z3.py source ...
0
votes
1
answer
40
views
SMT solvers for real closed fields (e.g., trascendentals and infinitesimals) in practise? Z3, MetiTarski, dReal
I would like to delve into the capability of SMT solvers to deal with trascendental and infinitesimal elements.
Thus, I just read the paper on computing in real closed fields https://www.cl.cam.ac.uk/~...
0
votes
0
answers
40
views
SMT2Lib slows after a non-negativity assert
We're trying to build a solver for a weighted mean function. The code is written in SMT2Lib, and ran by CVC5 or Z3.
However, after adding an assert that indicates the non-negativity of the denominator,...
0
votes
1
answer
97
views
Algorithm to parse an expression and assinging a value that satisfies the conditions
The requirement is to parse a complex expression and assign the value to the variable that satisfies the condition. For e.g.
((!(($weatherResult.cityName=="Seattle")||($weatherResult....
0
votes
1
answer
22
views
How to output more than one Skolem functions in Z3(Py)
I am playing with Skolem functions in Z3-Py. In the following lines, I describe the Skolem function that satisfies the formula Forall x. Exists y. (x>=2) --> (y>1) /\ (y<=x) interpreted ...
0
votes
1
answer
35
views
A model of a simple formula 'Exists([y],ForAll([x],Phi))' should be 'y=2' but Z3 it is returning '[]'
Note the following Z3-Py code:
x, y = Ints('x y')
negS0= (x >= 2)
s1 = (y > 1)
s2 = (y <= x)
s = Solver()
phi = Exists([y],ForAll([x], Implies(negS0, And(s1,s2))))
s.add(phi)
print(s.check()...
2
votes
1
answer
37
views
What does a model mean in a universally quantified formula? Is it a function?
Consider these two formulae:
Exists y. Forall x. (y>x), which is unsat.
Forall x. Exists y. (y>x), which is sat.
Note that we cannot find “models” for the sat formula, e.g., using Z3 it ...
0
votes
1
answer
33
views
In Z3, I cannot understand result of quantifier elimination of Exists y. Forall x. (x>=2) => ((y>1) /\ (y<=x))
In Z3-Py, I am performing quantifier elimination (QE) over the following formulae:
Exists y. Forall x. (x>=2) => ((y>1) /\ (y<=x))
Forall x. Exists y. (x>=2) => ((y>1) /\ (y<=...
0
votes
0
answers
52
views
Z3 compile example with C++
When I compile an example using Z3, it throws me errors of this type: api.lib(api_config_params.obj) : error LNK2001: unresolved external symbol
The example itself:
#include <iostream>
#include &...
0
votes
0
answers
42
views
Z3Py - Calling functions written as Z3 expressions
I am using Z3Py and I have a function which is written as Z3 expressions in Python, can I call that function in another function?
def func1 (a,b,c):
vara = a * b
varb = URem (vara, c)
...
0
votes
0
answers
35
views
Applying Lookahead with z3 Solver
I want to solve a CSP with the help of Lookahead method in z3 Solver. The issue I'm facing is not being convinced that it's invoked by setting an according parameter like s.set("sat....
0
votes
0
answers
29
views
Simulate global variable access with Claripy
I need to simulate this decompiled line of code in a Python script using claripy as solver engine,
*(ulong *)(global_variable + (ulong)((uint)local_variable[local_inedx + 1] & 1) * 8)
...
0
votes
2
answers
62
views
Get list of the available high-level variables in Z3 formula
I wonder if we can get a list of the higher-order free variables in the Z3 formula as they were declared while making the formula.
For example, in the following code:
P1 = Bool('P1')
x, y = Ints('x y')...
0
votes
1
answer
57
views
Representing an SMT formula
Making a Boolean formula in PySMT is simple:
from pysmt.shortcuts import *
from pysmt.typing import INT
x1 = Symbol("x1")
x2 = Symbol("x2")
formula = Or(x1, x2)
model = get_model(...
0
votes
1
answer
43
views
Extracting boolean terms from Z3 model when using quantifiers
I am trying to use Z3 to explore the difference between two predicates, but the model contains exist-expressions where I would expect boolean constants.
I have the following program in smtlib:
(...
0
votes
1
answer
49
views
How to rank solutions using SMT solver like Z3 in formal logic
I am trying to use Z3 (SMT solver) to verify and rank a list of solutions. In verification system,I have some constraints and evaluation criteria and based on that I wanted to rank the solution using ...
1
vote
1
answer
84
views
how to find cube root of 7 with Z3 library
This code returns a good result but Does anyone have an idea how to convert this program to return the same result but in the Z3 solver???
from decimal import *
import time
getcontext().prec = 100
x =...
0
votes
0
answers
29
views
Is there a quantifier elimination functionality in CVC5 or CVC4 (I am using Python API)?
I am using CVC5 in Python and realize that I need something that does the equivalent to the following Z3-Py code:
t = Tactic("qe")
phi = Goal()
phi.add(Exists(var_list, psi))
...
0
votes
1
answer
54
views
Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result
I am starting with dReal and I have a set of questions about it.
These questions are based on the tutorial we can find in https://github.com/dreal/dreal4, section "Python bindings", with the ...
0
votes
0
answers
42
views
Absolute value function in Z3 solver .NET C#
I am using Z3 solver from Microsoft and I am trying to find or implement Abs function using C# .Net wrapper. I found an example in Python (https://github.com/Z3Prover/z3/issues/5747), but I do not ...
1
vote
0
answers
90
views
I am trying to solve the N queens problem using specific constraints in Z3
To solve the N queens problem in Z3 I have 5 combinations of propositional logic. I am struggling to set up the for loops the way they are required.`
from z3 import *
n = 4
Q =[[Bool("x_%s_%s&...