Questions tagged [smt-solvers]
Solver programs for the Satisfiability Modulo Theories (SMT). The SMT problem is a decision problem for logical formulas with combinations of background theories expressed in classical first-order logic with equality.
41
questions
0
votes
0
answers
14
views
How do static analysis tools automate separation logic?
I understand separation logic as a form of verification method, similar to Hoare logic. That is, they allow to reason about statements of the form $\{P\} C \{Q\}$, where $C$ is an instruction, and $P$ ...
1
vote
1
answer
77
views
A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?
I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster.
My implementation ...
1
vote
0
answers
86
views
SMT solver gives up on seemingly trivial problem
I expected CVC5 to produce a proof given the following problem in TPTP format.
Why does CVC5 give up on the TPTP problem, but works just fine on the same problem given in SMT-LIB2?
In human words, the ...
2
votes
1
answer
64
views
What is the difference in heap configurations? Separation logic with CVC5 SMT solver
I am figuring out separation logic and trying to run simple examples in CVC5 smt solver. I am missing some core understanding of how pointers and values are treated there and I don't know where to ...
1
vote
1
answer
89
views
Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?
I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
1
vote
2
answers
529
views
How does the SMT solver Z3 handle conditional statements in a constraint?
I have a constraint system which I seek to find solutions for.
The constraints consist of lesser/equal inequalities which have a difference of two minimum expressions on their right side, for example:
...
0
votes
0
answers
38
views
Specific quantifier elimination for real algebraic numbers
It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
0
votes
1
answer
65
views
Domain of discourse vs First-order theory
In the question (Validity of predicate logic formulas) I see the following way of expressing:
"The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
1
vote
0
answers
96
views
SMT validity solvers/ quantifier elimination in Ocaml
I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
1
vote
1
answer
148
views
Are there any solvers that can handle non-linearity?
I need a way to solve linear and non-linear inequalities over the natural numbers. So equations like this should be solveable:
$\forall n, p, q \in \mathbb{N}. q \cdot (1 + n^p) \leq q$
From what I ...
2
votes
1
answer
58
views
How to represent bottom element (integer domains) in SMT formula
I'm doing some work with static analysis and need to represent local variables as SMT formulas. In general this is fairly straight forward, depending on the domain of the static analysis. However, ...
0
votes
0
answers
56
views
SAT solvers that can compute prime implicants and/or minimization
I'm looking into computing the prime implicants of a Boolean function. I have found many different algorithms in the literature, many of them relying on SAT solvers. However, I have not been able to ...
1
vote
1
answer
67
views
Assign few binary variables to make all polynomials identically zero
I have 50 polynomials $f_i$ over binary variables $(x_1,\ldots,x_{100})$. Also $f_i(0,0,\ldots,0)=0$
for any $i \in [1,50]$. I want to assign few variables so that all $f_i$ will be
identically zero. ...
0
votes
2
answers
136
views
Tutorials/resources for building a toy SMT solver
I've built a rudimentary SAT Solver from scratch, and wanted to do the same with SMT solvers as well.
While I've found two toy SMT Solver implementations in Haskell and Ocaml, but no tutorials or ...
0
votes
1
answer
36
views
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
a. Decidable
b. At least expressive as propositional logic
c. NP-complete
a) Decidable: no, some first order ...
2
votes
2
answers
110
views
Constraint satisfaction problem: solve system, then evaluate whether many additional constraints are satisfied one at a time
I have a system that consists of binary inequality constraints between variables, plus some indicator variables that can assume only two values:
...
1
vote
2
answers
209
views
Automated reasoning with real numbers
I have a large number of equivalences which look like:
$(a \leq 0.54 \wedge b \geq 0.12) \vee (c \gt 0.98)$ $\Leftrightarrow$ $(x \leq 0.25) \vee (x \gt 0.91 \wedge y \geq 0.01)$
This is just an ...
3
votes
1
answer
50
views
How to leverage the fact that I'm solving 1000's of very similar SMT instances?
I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array. Then, my program takes as input k << 100,000 new clauses, and adds ...
1
vote
1
answer
887
views
What are the differences between symbolic execution and SAT solvers?
My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
2
votes
1
answer
61
views
Proving that a property is k-inductive with an SMT solver (parametric resettable counter)
I'm following the slides at https://homepage.cs.uiowa.edu/~tinelli/talks/FT-11.pdf where Tinelli explains how k-induction works in the context of SMT based model checking.
A parametric and resettable ...
0
votes
0
answers
57
views
Program synthesis based on function properties
I am fairly new at program synthesis and the use of SMT solvers for this purpose. Given a function g, I want to generate all the functions f and h such that the following holds:
f . g = h . f
Are ...
4
votes
1
answer
329
views
Check if two items are equal after replacing
Let's say that an item is either a natural number or a list of items. Examples of items are:
1
[2]
[4, [3, 1], 3, 4]
A rule states that two items are equal. For example:
1 = 2
3 = [3, 1]
[4, 3] = [...
0
votes
1
answer
25
views
Generating graph with complex structure
I want to generate a bunch of graphs of about 100 nodes, where each node is a categorial variable. I want the graphs to satisfy complex properties, like, "if a node of type A is connected to a node ...
1
vote
0
answers
174
views
General Understanding of SMT Solving Across Multiple Theories
My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
-2
votes
1
answer
281
views
How a SMT / SAT Solver Generates Valuations for this Example
First, an example of a set of constraints which turned out not to be solvable (I don't think):
...
2
votes
0
answers
184
views
Passing arrays vs functions as arguments in SMT?
In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions.
In the theory of arrays, ...
0
votes
1
answer
89
views
Objective function and constraint satisfaction over a set of multi-attributes elements
I'm looking for an approach to solve a problem consisting of maximizing an objective function over a set of discrete elements, while respecting a set of constraints.
To illustrate my point, I'll try ...
2
votes
1
answer
3k
views
Bit Blasting Algorithm
I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example:
Assume our bit-vectors ...
4
votes
2
answers
1k
views
How could an SMT solver be implemented as simple as possible?
I'm trying to figure out how an SMT solver works as simple as possible.
Let's assume we have a simple input program with symbolic values x and ...
0
votes
0
answers
178
views
When to use SAT vs solving?
Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver?
Is there any guidance anyone can offer about which ...
0
votes
1
answer
60
views
Verification condition in case of array theory
As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it:
Generate VC's from the program.
Solve ...
3
votes
3
answers
238
views
Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?
I'm a little unfamiliar with graph theory, and I found an interesting problem in my work that I do not know if its already well-known or can be easily mapped to another one. If I were to express the ...
4
votes
0
answers
51
views
How the $EX(f)$ is evaluated in symbolic model checking?
I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs.
I was trying to ...
7
votes
1
answer
255
views
Framework or tools to generate theorem prover/solver/reasoner for new logic
I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
1
vote
1
answer
220
views
Using SMT Solvers in formula checking
I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement.
Suppose we have a list of three-...
6
votes
1
answer
785
views
Exponential example for simplex used in SMT solvers
The original simplex algorithm requires an exponential number of pivot operations in the worst case, e.g., if run on the Klee-Minty example [3,4].
What about the simplex algorithm used in SMT solvers ...
2
votes
1
answer
53
views
SMT solves with functions for free varibles
So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions ...
5
votes
2
answers
467
views
Using SMT solvers to generate random solutions to given predicate
I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, *
The algorithm I want should produce ...
5
votes
0
answers
188
views
Introduction to bounded model checking that describes model generation
Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
18
votes
3
answers
3k
views
Why is unification so important to inference engines?
I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.
I keep reading about the Unification Algorithm.
...
16
votes
2
answers
462
views
Why do some inference engines need human assistance while others don't?
I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.
Why is it that automated theorem provers, i.e. ACL2,...