Stack Overflow
Stack Overflow

Questions tagged [smt]

Satisfiability Modulo Theories (SMT) are decision problems for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality.

Satisfiability Modulo Theories (SMT) are decision problems for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality.

A SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories.

SMT problems are usually expressed by the SMT-LIB language and solved by high-performance SMT solvers. For a list of benchmarks, solvers and other information regarding SMT, please visit http://smtlib.org/.

845 questions
54
votes
1 answer

How incremental solving works in Z3?

I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following: There are two ways to use Z3 for incremental solving: one is push/pop(stack) mode, the other is using assumptions.…
Tianhai Liu
  • 795
  • 5
  • 10
40
votes
2 answers

Z3: finding all satisfying models

I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example: (declare-const f Bool) (assert (or (= f true) (= f false))) In this propositional…
marczoid
  • 1,365
  • 2
  • 12
  • 20
22
votes
1 answer

Limits of SMT solvers

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 prover. In recent years, a lot of progress has been…
rwallace
  • 31,405
  • 40
  • 123
  • 242
14
votes
1 answer

Defining a Theory of Sets with Z3/SMT-LIB2

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 simple option/flags. here's the permalink: …
Ranjit Jhala
  • 1,242
  • 8
  • 18
13
votes
2 answers

SAT solving with haskell SBV library: how to generate a predicate from a parsed string?

I want to parse a String that depicts a propositional formula and then find all models of the propositional formula with a SAT solver. Now I can parse a propositional formula with the hatt package; see the testParse function below. I can also run a…
mrsteve
  • 4,082
  • 1
  • 26
  • 63
10
votes
2 answers

Use of term rewriting in decision procedures for bit-vector arithmetic

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 procedure such as those based on bit-blasting. The term…
iago
  • 277
  • 1
  • 10
9
votes
1 answer

Can Z3 be used to reason about substrings?

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' when asked if 'x' is in 'x', or 'x' is in 'xy'. I've…
Katie
  • 93
  • 4
9
votes
0 answers

Which First Order theorem provers are guaranteed to halt on monadic inputs?

Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, and there exist resolution-based methods for deciding…
jmite
  • 8,171
  • 6
  • 40
  • 81
9
votes
1 answer

While loop for Z3 or Smt2

How to convert a simple while loop(c- code) to smt2 language or z3? For ex : int x,a; while(x > 10 && x < 100){ a = x + a; x++; }
hodophile
  • 357
  • 1
  • 5
  • 14
9
votes
1 answer

(get-unsat-core) returns empty in Z3

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) (declare-fun ph1 () Int) (declare-fun ph1p ()…
chinu
  • 239
  • 2
  • 6
9
votes
1 answer

Avoiding quantifiers in Z3

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 quantifiers with all instantiated ground instances when…
marczoid
  • 1,365
  • 2
  • 12
  • 20
8
votes
2 answers

What are the limits of reasoning in quantified arithmetic in SMT?

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 x)))) (check-sat) (exit) The solvers all return…
Liana Hadarean
  • 81
  • 2
7
votes
1 answer

Are floating point SMT logics slower than real ones?

I wrote an application in Haskell that calls Z3 solver to solve constrains with some complex formulas. Thanks to Haskell I can quickly switch the data type I'm working with. When using SBV's AlgReal type for computations, I get results in sensible…
arrowd
  • 33,231
  • 8
  • 79
  • 110
7
votes
1 answer

z3: solve the Eight Queens puzzle

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 import * X = [[Int("x_%s_%s" % (i+1, j+1)) for j in…
Tan
  • 115
  • 7
7
votes
1 answer

Z3: express linear algebra properties

I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed). For example I want to prove that the outcome of an expression is a diagonal matrix or a triangular matrix, or it is positive…
tyr.bentsen
  • 143
  • 1
  • 6
1
2 3
…
56 57