Satisfiability Modulo Theories

Section 1

Z3

• A state-of-art Satisfiability Modulo Theories (SMT) solver
  
  
  
  
• On GitHub: https://github.com/Z3prover/z3.git
  • MIT open source license
  • Developments: Scalable simplex solver, Strings, Horn clauses, floating points, SAT extensions

Some Z3 Applications

• Program Verification
  • VCC, Everest, Dafny, Havoc, Leon
    
    
• Symbolic Execution
  • SAGE, Pex, KLEE
    
    
• Software Model Checking
  • Static Driver Verifier, Smash, SeaHorn
    
    
• Configurations
  • Network Verification with SecGuru
  • Dynamics Product Configuration

Microsoft Tools using Z3

SAT/SMT examples

• Book draft by Dennis Yurichev

Basic SAT

  Tie, Shirt = Bools('Tie Shirt')
  s = Solver()
  s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))
  print s.check()
  print s.model()

Basic SMT

I = IntSort()
f = Function('f', I, I)
x, y, z = Ints('x y z')
A = Array('A',I,I)

fml = Implies(x + 2 == y, f(Select(Store(A, x, 3), y - 2)) == f(y - x + 1))

s = Solver()
s.add(Not(fml))
print s.check()

SMT in a nutshell

Is formula satisfiable under theory ?

SMT solvers use specialized algorithms for .

Complexity

SAT/SMT

Logics and Theories

Logics

• Sorts -

• - signature of sorted constant, functions

  • Functions are sorted .
  • Constants are nullary functions

  • Predicates are functions with range

• Terms and predicates are built from functions over

• Connectives and Quantifiers

  • - and, - or
  • - negation, - implication
  • - quantifiers

Extended SAT queries

Slide is by Joao Marques-Silva

Logical Queries - SAT+

sat unsat

model (clausal) proof

correction set core

local min correction set local min core

min correction set min core

Logical Queries

Progress in SAT, SMT, and ATP

Progress in SAT Solving

Progress in ATP

Progress in SMT Solving

Equality and Uninterpreted functions

EUF

  (declare-sort A)
  (declare-fun f (A) A)
  (declare-const x A)
  (assert (= (f (f x)) x))
  (assert (= (f (f (f x))) x))
  (check-sat)
  
  (assert (not (= (f x) x)))
  (check-sat)

Deciding Equality

Disequalities

Variants of union-find are effective to decide equality.

Free functions

Congruence rule

Naming sub-terms

Applying Congruence (1)

Applying Congruence (2)

EUF Models

A satisfiable version:

EUF Models (II)

• Associate a distinct value with each equivalence class.

Linear Arithmetic

(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)
(get-model) ; display the model  

Linear Arithmetic Example

Algorithmic Fragments of Arithmetic

Other Fragments of Arithmetic

• NIA - There is no decision procedure for integer polynomial constraints

  • Z3 falls back to incomplete heuristics
  • NIA over bounded integers may get translated to bit-vector constraints

  
  Other theories that admit custom solvers:

• Bi-linear real arithmetic

• Non-unit two-variable per inequality

• At most one unit positive variable per inequality (Horn)

An Overview of Arithmetic Theories

Bellman-Ford - a selection

(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) ...))
(assert (and (>= t21 0) ...))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or ... (>= t21 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) ...))
(check-sat)
(get-model) ; display the model  

Bellman-Ford

Solve difference logic using graph Bellman-Ford network flow algorithm. Negative cycle unsat.

General form Simplex [21]

General form and

Only bounds (e.g., ) are asserted during search.

From Definitions to a Tableau

- are basic (dependent)
- are non-basic

Pivoting

• Value of non-basic variable can be chosen between and .
• Value of basic variable is a function of non-basic variable values.
• Pivoting swaps basic and non-basic variables.
  • used to get values of basic variables within bounds.

Pivoting example

- are basic (dependent)
- are non-basic

Initial values:

Bounds :

, make non-basic.
- are basic (dependent)
- are non-basic

Arrays

(define-sort A () (Array Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun a1 () A)

(push)
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
(assert (not (= x y)))
(check-sat)
(pop)

(define-fun all1_array () A ((as const A) 1))
(simplify (select all1_array x))

(define-sort IntSet () (Array Int Bool))
(declare-fun a () IntSet)
(declare-fun b () IntSet)
(declare-fun c () IntSet)
(push) ; illustrate map
(assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a))))))
(check-sat)
(pop)    

Arrays

Arrays as Combinators [46]

  A = Array(Index, Elem) # array sort 
  
  a[i]             # index array 'a' at index 'i'
                   # Select(a, i)
  
  Store(a, i, v)   # update array 'a' with value 'v' at index 'i'
                   # = lambda j: If(i == j, v, a[j])
    
  Const(v, A)      # constant array
                   # = lambda j: v
  
  Map(f, a)        # map function 'f' on values of 'a'
                   # = lambda j: f(a[j])

  Ext(a, b)        # Extensionality
                   # Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

Array Decision Procedure

Example Store(a, i, v)

• Each occurrence of Store(a, i, v) and b[j],
  • Assert Store(a, i, v)[j] == If(i == j, v, a[j])

  • Assert Store(a, i, v)[i] == v

• Each shared occurrences of :
  • Assert .

Array Decision Procedure (2)

Example Store(a, i, v)

• Each occurrence of Store(a, i, v) and b[j],
  • Assert Store(a, i, v)[j] == If(i == j, v, a[j])

  • Assert Store(a, i, v)[i] == v

• Each shared occurrences of :

  • Assert .

• Suppose we are given a model satisfying all asserted equalities.
  • assigns values to terms.
  • Extend:
  • Claim: satisfies Store axioms.

Efficient Array Decision Procedures

• Use current partial interpretation to guide axiom instantiation.

• Rough sketch:

  • If (congruent) in current state
    • Assert .
  • If in current state
    • Assert

• Also important to limit set of pairs.

  • Z3 uses relevancy propagation to prune don't care literals
  • Boolector uses dual propagation to extract small implicant

Bit-Vectors

(define-fun is-power-of-two ((x (_ BitVec 4))) Bool 
  (= #x0 (bvand x (bvsub x #x1))))
(declare-const a (_ BitVec 4))
(assert 
 (not (= (is-power-of-two a) 
         (or (= a #x0) 
             (= a #x1) 
             (= a #x2) 
             (= a #x4) 
             (= a #x8)))))
(check-sat)

Bit-Vector demo

Bit-Vector Adder Encoding

Bit-Vector Multiplier Encoding

Floating point example

(declare-fun X () (_ FloatingPoint 11 53))

(assert (fp.isNormal X))
(assert (not (fp.isSubnormal X)))
(assert (not (fp.isZero X)))
(assert (not (fp.isInfinite X)))
(assert (not (fp.isNaN X)))
(assert (not (fp.isNegative X)))
(assert (fp.isPositive X))

(check-sat)
(get-model)

Floating Points demo

Sequence Example

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof b a))
(assert (str.suffixof c a))
(assert (= (str.len a) (+ (str.len b) (str.len c))))
(assert (not (= a (str.++ b c))))
(check-sat)  

Sequences and Strings

Queues

Algebraic Data-types

   (declare-datatypes () ((Tree Empty (Node (left Tree) (data Int) (right Tree)))))

   (declare-const t Tree)
   (assert (not (= t Empty)))
   (check-sat)
   (get-model)

sat
(model 
  (define-fun t () Tree
    (Node Empty 0 Empty))
)

Algebraic Data-types demo

Non-linear Arithmetic [34]

NLSAT example

; Code written by TheoryGuru
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(declare-fun v7 () Real)
(declare-fun v8 () Real)
(declare-fun v9 () Real)
(declare-fun v10 () Real)
(declare-fun v11 () Real)
(declare-fun v12 () Real)

; define true assumption
(assert (and 
(> (* 2 v11 v6 v9) (+ (* v12 (^ v6 2)) (* v8 (^ v9 2))))
(> (+ (* 2 v10 v11 v4 v6) (* v12 v5 (^ v6 2)) (* -2 v12 v4 v6 v7) (* v12 (^ v4 2) v8) (* -2 v11 v5 v6 v9) (* 2 v11 v4 v7 v9) (* 2 v10 v6 v7 v9) (* v5 v8 (^ v9 2))) (+ (* (^ v11 2) (^ v4 2)) (* (^ v10 2) (^ v6 2)) (* 2 v10 v4 v8 v9) (* (^ v7 2) (^ v9 2))))
(> v1 0)
(> v2 0)
(> v3 0)
(> v4 0)
(> v6 0)
(> v9 0)
(= (+ (* v1 v11) (* v3 v7) (* v2 v8)) 0)
(= (+ (* v1 v12) (* v11 v2) (* v10 v3)) 0)
(= (+ (* v1 v10) (* v3 v5) (* v2 v7)) 0)
))

; define negative of the hypothesis
(assert (not (>= (* v5 v8) (^ v7 2))))

(check-sat)
(exit)

NLSAT demo

Duality - model/proof repair

Duality - connecting glue

Duality - propagation

CDCL(T) by example

CDCL(T) by example (2)

CDCL(T) by example (3)

CDCL(T) by example (4)