SC Chapter 5 SMT Solving

Algorithm for phi^UF in polynomial time

1. Replace f(a) by x_f(a)

2. Assume that for all a,b in Dⁿ that f(a)!=f(b) → a!=b

1. Ackermann’s and 2. Bryant’s

1. phi^E := phi_flat \land phi_cong with phi_flat is a flattening of phi^UF and phi_cong is a conjunction of constraints for functional congruence

2. phi^E := phi_cong → phi_flat [which is the proper definition

1. Every F(x) is replaced by f_x in phi_flat

2. Every G(F(x)) is replaced by g_fx in phi_flat

1. or all pairs F(x),F(y) insert (x=y→f_x=f_y) into phi_cong

2. For all pairs G(F(x)),G(F(y)) insert (x=y→fx=fy \land fx=fy→g_fx=g_fy) into phi_cong

3. For all paris F(a,x),F(b,y) insert ((a=b \land x=y) → f_ax=f_by) into phi_cong

1. Consider cases Fi*

2. Values of function are compared

3. Free mappings are considered fi and exchanged with F

1. E-graphs and 2. Sparse Method

1. Extract set E= (dashed) and E!= (solid)

2. Equality graph G^E(phi^E) = <V,E=,E!=>

3. Ignores boolean structure of phi^E representing an abstraction

1. Edges of E=

2. Written as x=*z with (x,z) not in E=

A equality path and one edge from E!=

1. If a disequality edge exists

2. For every two nodes x,y x=*y x!=*y holds

3. Simple if the smallest cycle

1. Replace all edges which are not part of a CC with false or true regarding if they are solid or dashed

2. Repeat this process till solved

Transform phi^E to phi^PL

1. Replace equalities by boolean variables into phi_sk // So-called over-approximative propositional skeleton

2. Add transitivity constraints into phi_trans for each cycle in E-Graph // Otherwise they are lost

3. Check phi^PL := phi_sk \land phi_trans

1. Only simple cycles

2. Only chord-free simple cycles

3. Make a graph chordal

1. Iff every cycle of length 4 or more has one chord

2. Only constraint triangles (polynomial effort)

1. Create phi_sk

2. Make a chordal version of G^E(phi^E)

3. phi_trans = true

4. Add to phi_trans for each triangle (ex \land ey) → ez

5. Return phi_sk \land phi_trans

1. Model bit-level operations (F and P) by boolean circuits

2. Use Tseitin’s encoding to generate phi^PL

3. Use SAT solver

4. Convert solution back to the theory

5. Efficient solution e.g. Clarke et al. With CBMC

Switches between SAT solver and theory

1. Put boolean abstraction of phi into SAT solver

2. If unsatisfiable return UNSAT

3. Put (in)equation set into theory solver

4. If satisfiable return SAT

5. Put explanation into SAT solver and move to step 2.

1. Each constraint is a boolean variable

2. Solve the PL formula with variable order and first false

1. Find conflicting true constraints

2. Compute a partition defining the equivalence classes of terms // Uninterpreted functions get their own equivalence classes

Add conflicting constraints to PL formula

1. Init with no (dis)equations, empty partition and state=SAT

2. Put boolean abstraction of phi in CNF into SAT solver

3. If solution return SAT elseif unsatisfiable return UNSAT

4. Put (in)equation set into theory solver(s)

5. Put (partial) SAT or UNSAT explanation into SAT solver and move to step 3.

1. Be incremental using previous for next check

2. Compute (minimal) infeasible subsets for a reason of unsatisfaction

3. Backtrack removing constraints in chronological order

1. For new equation check previous disequations

2. For new disequations check them

Set of equations proving t=t’ and disequation t=t’

1. Some approaches strictly divides between logical structure and theory constraints some not

2. E.g propagate in the SAT-solver bounds on theory variables