Questions tagged [z3]

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

Filter by
Sorted by
Tagged with
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, ...
  • 618
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 ...
  • 618
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 ...
  • 529
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,...
  • 25
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
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 (...
  • 1,000
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 ...
  • 5
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 ...
  • 5
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 ...
  • 187
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 ...
  • 5
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 ...
  • 2,536
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 * ...
  • 713
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 (=> ...
  • 461
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 ...
  • 13
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 ...
  • 73
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 ...
  • 618
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 ...
  • 618
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 ...
  • 23.1k
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 ...
  • 410
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 ...
  • 25
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 ...
  • 5
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/~...
  • 618
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,...
  • 301
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 ...
  • 618
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()...
  • 618
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 ...
  • 618
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<=...
  • 618
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 &...
  • 21
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) ...
  • 51
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')...
  • 551
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(...
  • 551
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: (...
  • 3
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 =...
  • 11
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)) ...
  • 618
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 ...
  • 618
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&...
  • 11

1
2 3 4 5
56