smt Questions
1
Solved
Suppose I have 2 arrays in a formula whose satisfiability I want to check using z3. If z3 returns sat, I want to read in the first array in the z3 model and pretty print it as a key, value pair and...
1
Solved
I am using the Java-API of Z3 Version 4.3.2 64-bit on Windows 7 as well as Java 7 64-bit, but I don't think Java is a necessity to answer this question.
Right now I am using the following Java cod...
2
Solved
Today I wanted too look into options on SAT solving in haskell. First I tought about writing my own interface to the picosat solver.
Then I found out there is the SBV library.
It's interfaces to Z...
Kelby asked 4/1, 2014 at 21:24
1
Any more or less practical programming language and compiler have to deal with constraints. The most common constraint is types. Usually type derivation and unification is done by a straightforward...
Spearwort asked 15/9, 2013 at 20:8
1
I obtained several statistics from runs of Z3. I need to understand what these mean.
I am rather rusty and non up to date for the recent developments of sat and SMT solving, for this reason I tried...
Nancinancie asked 28/8, 2013 at 15:17
1
Solved
I am using Z3 to extract the unsat-core of an unsatisfiable formula. I am using Z3@Rise interface (web based) to write the following code,
(set-logic QF_LIA)
(set-option :produce-unsat-cores true)...
Cocci asked 8/8, 2013 at 17:25
2
Solved
Say I have
t1<x and x<t2
is it possible to hide variable x so that
t1<t2
in Z3?
1
Solved
I get the following statistics in Z3.
(:added-eqs 24529
:binary-propagations 43837
:bv-bit2core 7115
:bv-conflicts 156
:bv-diseqs 10395
:bv-dynamic-diseqs 10028
:bv->core-eq 10401
:confl...
1
Solved
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 ...
2
I have tried several SMT solvers (CVC3, CVC4 and Z3) on the following seemingly trivial benchmark:
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y...
1
Solved
I'm going through Z3py and have a question with how to use the API in a couple specific cases. The code below is a simplified version of something I would ultimately like to use Z3 for. Some of my ...
1
Solved
I am experimenting with Z3 where I combine the theories of arithmetic, quantifiers and equality. This does not seem to be very efficient, in fact it seems to be more efficient to replace the quanti...
Busch asked 7/11, 2012 at 11:3
1
Solved
I am trying to prove an inductive fact in Z3, an SMT solver by Microsoft. I know that Z3 does not provide this functionality in general, as explained in the Z3 guide (section 8: Datatypes), but it ...
1
Solved
Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem...
Mosaic asked 21/7, 2012 at 13:11
1
Solved
Say given a formula
(t1>=2 or t2>=3) and (t3>=1)
I wish to get its disjunctive normal form
(t1>=2 and t3>=1) or (t2>=3 and t3>=1)
How to achieve this in Z3?
1
Solved
One way to solve optimisation problems is to use an SMT solver to ask whether a (bad) solution exists, then to progressively add tighter cost constraints until the proposition is no longer satisfia...
4
Solved
I have a big boolean formula to solve, due to the reason of the redaction, I have to paste an image here:
Also, I have already a function area to measure the dimension of 4 integers: area(c,d,e,f)...
Impressionist asked 14/12, 2011 at 14:30
1
Solved
While using SMTLIB arrays, I noticed a difference between Z3's understanding of the theory and mine. I am using the SMTLIB array theory [0] which can be found on the official website [1].
I think ...
2
I have a code in z3 which aims to solve an optimization problem for a boolean formula
(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000)
(declare-const a0 Int) (assert (= a0 2))
(declare-const b...
Marlette asked 15/12, 2011 at 0:53
2
Solved
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 proc...
2
Solved
How do I get the maximum of a formula using smt-lib2?
I want something like this:
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= x 2))
(assert (= y 4))
(assert (=...
1
Solved
Here is an SMT-LIB 2.0 benchmark which I executed with z3 :
(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)
(assert (forall ((x Int)) (exists ((X PZ))
(and (MS x X)
(for...
2
Solved
I'm planning some experiments in symbolic execution of C code, using an off-the-shelf SMT solver, and wondering which solver to use; looking at e.g. the SMT contest entrants, and taking only the op...
Mithgarthr asked 7/6, 2011 at 10:33
1
Solved
I am trying to use Z3 to reason about substrings, and have come across some non-intuitive behavior. Z3 returns 'sat' when asked to determine if 'xy' appears within 'xy', but it returns 'unknown' wh...
1
Solved
The SMTLib2 directive (get-info all-statistics) displays several numbers, e.g.
num. conflicts: 4
num. propagations: 0 (binary: 0)
num. qa. inst: 23
In order to test different axiomatisations and...
Ramsgate asked 27/7, 2011 at 8:3
© 2022 - 2025 — McMap. All rights reserved.