Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories Clark W. Barrett Ph.D. Dissertation Defense Department of Computer Science Stanford University August 2001 The Problem: First-Order Logic First-Order Logic is a mathematical system for making precise statements. Statements in first-order logic are made up of the following pieces: Variables x, y Constants 0, John, Functions f (x ), x + y Predicates p (x ), x > y, x = y Boolean connectives , , , Quantifiers , Example: “Every rectangle is a square” x. (Rectangle (x ) Square(x)) The Problem: First-Order Theories A first-order theory is a set of first-order statements about a related set of constants, functions, and predicates. A theory of arithmetic might include the following statements about 0 and +: x. ( x + 0 = x ) x,y. (x + y = y + x ) The Problem: Validity An expression is valid if every possible way of interpreting it results in a true statement. x=x p(x ) p(x ) x = y f (x ) = f (y ) f (x ) = f (y ) x = y Valid Valid Valid Invalid An expression is valid in a theory if every possible way of interpreting it in that theory results in a true statement. x 0 Invalidinin Valid positive the theory real arithmetic of real arithmetic The Problem: Validity Checking Suppose T is a first-order theory and is a first-order formula We write T = as an abbreviation for “ is valid in T ” A classical result in Computer Science states that in general, the question of whether T = is undecidable. It is impossible to write a program that can always figure out whether T = However, given appropriate restrictions on T and , a program can automatically decide T = We consider theories T such that T = is decidable when is quantifier-free. Motivation Many interesting and practical problems can be solved by checking the validity of a formula in some theory. As evidence of this claim, consider the following widelyused tools tools which include decision procedures for checking validity PVS [Owre et al. ‘92] STeP [Manna et al. ‘96, Bjørner ‘99] ESC [Detlefs et al. ‘98] Mona [Klarlund and Møller ‘98] SVC [Barrett et al. ‘96] The SVC Story Roots in processor verification [Burch and Dill ‘94] [Jones et al. ‘95] Internal use at Stanford Symbolic simulation [Su et al. ‘98] Software specification checking [Park et al. ‘98] Infinite-state model checking [Das and Dill ‘01] External use since public release in 1998 Model Checking [Boppana et al. ‘99] Theorem prover proof assistance [Heilmann ‘99] Integration into programming languages [Day et al. ‘99] Many others The SVC Story Despite its success, SVC has many limitations Gaps in theoretical understanding Outgrown its original software architecture Unnecessarily slow performance in some cases This thesis is the result of ongoing efforts to address these limitations. New contributions to underlying theory A flexible and efficient implementation Techniques for faster and more robust performance Outline Validity Checking Overview The Problem Motivation The SVC Story Top-Level Algorithm Methods for Combining Theories Implementation Adapting Techniques from Propositional Satisfiability Contributions and Conclusions Top-Level Algorithm Consider the following formula in the theory of arithmetic x>y true y > x x = y true y>x x=y false y > x x = y y>x x=y Step 1: Choose an atomic formula Step 2: Consider two cases: Replace the atomic formula with true Replace the atomic formula is with false Step 3: Simplify Top-Level Algorithm Consider the following formula in the theory of arithmetic x>y y>x true y > x x = y x=y false y > x x = y y>x x=y true xy yx xy true x=y true false This formula is unsatisfiable Validity Checking Overview A literal is an atomic formula or its negation The validity checker is built on top of a core decision procedure for satisfiability in T of a set of literals. The method for checking satisfiability will vary greatly depending on the theory in question The most powerful technique for producing a satisfiability procedure is by combining other satisfiability procedures Outline Validity Checking Overview Methods for Combining Theories The Problem Shostak’s Method The Nelson-Oppen Method A Combined Method Implementation Adapting Techniques from Propositional Satisfiability Contributions and Conclusions The Problem Consider the following theories: Real linear arithmetic: +,-,0,1,…, Arrays: s[i], update(s,i,v) Uninterpreted functions and predicates: f (x ), p(x ),… And the following set of literals in the combined theory: p (y ) s = update (t, i, 0 ) x - y - z = 0 z + s[i ] = f (x - y ) p (x - f (f (z ) ) ) Question: a method towith decide satisfiability Two main Given approaches, each advantages and of literals in each theory, how do we decide the satisfiability of literals disadvantages in the combined theory? Shostak [Shostak ‘84] Nelson-Oppen [Nelson and Oppen ‘79] Shostak’s Method Has formed an ongoing strand of research Originally published in 1984 [Shostak ‘84] Several clarifying papers since then [Cyrluk et al. ‘96] [Ruess and Shankar ‘01] Used in several automated deduction systems PVS, STeP, SVC Unfortunately, remains difficult to understand Details are nonintuitive Simple proof of correctness has been especially elusive Contribution : A new presentation of a key subset of Shostak’s original algorithm. Shostak’s Method: Canonizer There are two main components in a Shostak satisfiability procedure: the canonizer and the solver. The canonizer rewrites terms into a unique form T = a = b canon (a ) = canon (b ) Example: canonizer for linear arithmetic Combines like terms canon (x + x ) = 2x Imposes an ordering on the variables canon (y + x ) = x + y Shostak’s Method: Solver A set of equations E is said to be in solved form if the lefthand side of each equation is a variable which appears only once in E in solved form x = y+z w=z-a v = 3y + b not in solved form x =y+z w =z+x 2v = 3y + b S means replace each left-hand side variable occurring in S with its corresponding right-hand side E (w + x + y + z ) = z - a + y + z + y + z Shostak’s Method: Solver The solver transforms an equation into an equisatisfiable set of equations in solved form If T = a b , then solve (a = b ) = { false } Otherwise: solve (a = b ) = a set of equations E in solved form T = (a = b x. E ) x is a set of fresh variables appearing in E, but not in a or b. Example: solver for real linear arithmetic solve (x - y - z = 0 ) = { x = y + z } solve (x + 1 = x - 1 ) = { false } The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Use a generalization of Gaussian elimination with back substitution The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Choose matrix row Select an equation from Apply E as a substitution to Solve to get E’ Apply E’ as a substitution to E Add E’ to E -x - 3y + 2z = -1 x - y - 6z = 1 2x + y - 10z = 3 E 1 3 2 1 1 6 2 1 10 1 1 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply E as a substitution to Apply previous rows Solve to get E’ Apply E’ as a substitution to E Add E’ to E -x - 3y + 2z = -1 x - y - 6z = 1 2x + y - 10z = 3 E 1 3 2 1 1 6 2 1 10 1 1 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E x = -3y + 2z +1 x - y - 6z = 1 2x + y - 10z = 3 E 1 3 2 1 1 6 2 1 10 1 1 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Choose matrix row Select an equation from Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E x - y - 6z = 1 2x + y - 10z = 3 x = -3y + 2z +1 1 3 2 1 1 6 2 1 10 1 1 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply E as a substitution to Apply previous rows Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E -3y +2z +1-y -6z =1 x = -3y + 2z +1 2x + y - 10z = 3 1 3 2 0 4 4 2 1 10 1 0 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E y = -z 2x + y - 10z = 3 x = -3y + 2z +1 1 0 2 3 2 1 1 1 10 1 0 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E 1 x = -3(-z) +2z +1 y = -z 0 2x + y - 10z = 3 2 0 5 1 1 1 10 1 0 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Choose matrix row Select an equation from Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E 2x + y - 10z = 3 E x = 5z +1 y = -z 1 0 2 0 5 1 1 1 10 1 0 3 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply E as a substitution to Apply previous rows Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E 2(5z +1)+(-z )-10z=3 x = 5z +1 y = -z 1 0 0 0 5 1 1 0 1 1 0 1 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Solve to get E’ Make pivot 1 Apply E’ as a substitution to E Apply to previous rows Add E’ to E z = -1 E x = 5z +1 y = -z 1 0 0 0 5 1 1 0 1 1 0 1 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E z = -1 E x = 5(-1) +1 y = -(-1) 1 0 0 0 1 0 0 0 1 4 1 1 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Select an equation from Choose matrix row Apply previous rows Apply E as a substitution to Make pivot 1 Solve to get E’ Apply E’ as a substitution to E Apply to previous rows Add E’ to E E x = -4 y =1 z = -1 1 0 0 0 1 0 0 0 1 4 1 1 The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Step 2: Use this set of equations together with the canonizer to check if any disequality is violated For each a b Check if canon (E (a ) ) = canon (E (b ) ) E x = -4 y =1 z = -1 42 42 2y - 10x 6(z - 2x) 2(1)-10(-4)6(-1-2(-4)) The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Step 2: Use this set of equations together with the canonizer to check if any disequality is violated For each a b Check if canon (E (a ) ) = canon (E (b ) ) E x = 5z +1 y = -z 4z 1 (5z 4z + z1-z 1 -+4y x1-4(-z) +1) The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Step 2: Use this set of equations together with the canonizer to check if any disequality is violated For each a b Check if canon (E (a ) ) = canon (E (b ) ) Technical detail: If there is more than one disequality, the theory must be convex Shostak’s Method: Combining Theories In what sense is this algorithm a method for combining theories? Two Shostak theories T1 and T2 can often be combined to form a new Shostak theory T = T2 T2 Compose canonizers: canon = canon1 o canon2 Often, solvers can also be combined Treat terms from other theory as variables Repeatedly apply solvers from each theory until resulting set of equations is in solved form Shostak’s Method: Contributions Shostak’s original algorithm is much more complicated because it includes a decision procedure for the theory of pure equality with uninterpreted functions Why is the simplified version a contribution? Can be applied directly to produce decision procedures, even combinations of decision procedures Much easier to understand and prove correct Provides intuition for understanding the original algorithm Provides the foundation for a generalization of the original Shostak method based on a variation of Nelson-Oppen Nelson-Oppen Developed for the Stanford Pascal Verifier [Nelson and Oppen ‘79] [Nelson ‘80, Oppen ‘80] Tinelli and Harandi discovered a new (simpler) proof and an important optimization [Tinelli and Harandi ‘96] Used in real systems ESC EHDM [von Henke et al. ‘88] Vampyre [http://www-cad.eecs.berkeley.edu/~rupak/Vampyre] Nelson-Oppen Unlike Shostak, Nelson-Oppen does not impose a specific strategy on individual theories Instead of a solver and canonizer, Each theory provides a complete satisfiability procedure Technical detail: Each theory must be stably infinite There are two phases in the version of Nelson-Oppen presented by Tinelli and Harandi Purification phase Check phase Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions p (y ) s = update (t, i, 0 ) x-y-z=0 z + s[i ] = f (x - y ) p (x - f (f (z ) ) ) j =0 Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions p (y ) j =0 s = update (t, i, j ) k = s[i ] x-y-z=j z + s[i ] = f (x - y ) p (x - f (f (z ) ) ) Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions p (y ) j =0 s = update (t, i, j ) k = s[i ] x-y-z=j l =x-y z + k = f (x - y ) m=z +k p (x - f (f (z ) ) ) Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions p (y ) j =0 s = update (t, i, j ) k = s[i ] l-z=j l =x-y m = f (l ) m=z +k p (x - f (f (z ) ) ) Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions p (y ) j =0 s = update (t, i, j ) k = s[i ] l-z=j l =x-y m = f (l ) m=z +k p (v ) n = f (f (z ) ) ) v =x-n Nelson-Oppen: Purification Phase Transform a set of literals in a combined theory to an equisatisfiable set of literals such that each literal is pure : A pure literal contains symbols from only a single theory Consider again the following set of literals in a combined theory of arithmetic, arrays, and uninterpreted functions l-z=j s = update (t, i, j ) p (y ) j =0 k = s[i ] m = f (l ) l =x-y p (v ) m=z +k n = f (f (z ) ) ) v =x-n Nelson-Oppen: Check Phase Definitions Shared variables are variables that appear in literals from more than one theory Shared: l, z, j, y, m, k, v, n Unshared: x, s, t, i An arrangement of a set is a set of equalities that partitions the set into equivalence classes p (y ) s = update (t, i, j ) l-z=j Suppose S = { a , b , c } m = f (l ) k = s[i ] j =0 Some arrangements of S p (v ) l =x-y { a b , a c , b c } {{a},{b},{c}} n = f (f (z ) ) ) m=z +k { a = b , a c , b c } {{a,b},{c}} v =x-n { a = b , a = c , b = c } {{a,b,c}} Nelson-Oppen: Check Phase Choose an arrangement A of the shared variables For each theory, check if the set of literals pure in that theory together with the arrangement A is satisfiable If an arrangement exists that is compatible with each set of literals, then the original set of literals is satisfiable in the combined theory Arithmetic l-z=j j =0 l =x-y m=z+k v =x-n Arrays s = update (t, i, j ) k = s[i ] A (l, z, j, y, m, k, v, n ) Uninterpreted p (y ) m = f (l ) p (v ) n = f (f (z ) ) ) Nelson-Oppen: A Variation Contribution : A Variation of Nelson-Oppen The purification phase can be eliminated Instead, simply partition the formulas according to the outer-most symbol p (y ) s = update (t, i, 0 ) Arithmetic Arrays Uninterpreted x - yx--zy=-0z = 0 s = update (t, i, 0 ) p (y ) z + s[i p (x - f (f (z ) ) ) z +] = s[if ](x=-f y (x)- y ) p (x - f (f (z ) ) ) Nelson-Oppen: A Variation Contribution : A Variation of Nelson-Oppen The purification phase can be eliminated Instead, simply partition the formulas according to the outer-most symbol Choose an arrangement A of the shared terms which appear in a term or formula belonging to another theory For each theory, check if the set of literals assigned to that theory together with the arrangement is satisfiable Terms with foreign symbols are treated as variables Arithmetic Arrays Uninterpreted x-y-z=0 s = update (t, i, 0 ) p (y ) z + s[i ] = f (x - y ) p (x - f (f (z ) ) ) A (s[i ], x - y, f (x - y ), 0, y, z, f (f (z ) ), x - f (f (z ) ) ) Nelson-Oppen: A Variation Contribution : A Variation of Nelson-Oppen The purification phase can be eliminated Instead, simply partition the formulas according to the outer-most symbol Choose an arrangement A of the shared terms which appear in a term or formula belonging to another theory For each theory, check if the set of literals assigned to that theory together with the arrangement is satisfiable Terms with foreign symbols are treated as variables Contributions of this variation Fewer formulas given to each theory Easier to implement Easier to combine with Shostak Combining Shostak and Nelson-Oppen Theory requirements Shostak requires convexity Nelson-Oppen requires stable-infiniteness Contribution : The following theorem relates the two Every convex first-order theory with no trivial models is stably-infinite The proof is based on first-order compactness Note: if a convex theory does admit trivial models, it can usually be modified to include the non-triviality axiom: x,y. x y Combining Shostak and Nelson-Oppen Contribution : An algorithm for combining the two methods Equalities are processed according to the Shostak algorithm to get a set of equalities E in solved form All literals are partitioned as in the Nelson-Oppen variation The key idea is to consider the partial arrangement induced on the shared terms S by canon and E : A= : { a = b a,b S canon (E(a )) = canon (E(b )) } An arrangement A is chosen as in the Nelson-Oppen variation, but this arrangement must include A= This arrangement is automatically consistent with E The non-Shostak theories are checked for consistency with the arrangement as before Outline Validity Checking Overview Methods for Combining Theories Implementation Adapting Techniques from Propositional Satisfiability Contributions and Conclusions Implementation: Approach Based on Nelson-Oppen and Shostak combination Online algorithm Optimizations A Union-Find data structure and an Update List are used to efficiently keep track of both E and A simultaneously Simplify phase added Each new formula is simplified Enables rewrites that can reduce the number of shared terms Flexible theory interface Accommodates Nelson-Oppen theories, Shostak theories, and more Implementation: Interface Recall the top-level algorithm x>y true y > x x = y y>x x=y false y > x x = y true y>x x=y Choose an atomic formula Consider two cases: Add to the set of choices made and simplify Add to the set of choices made and simplify Repeat until formula is true or set of choices is unsatisfiable Interface from top-level : AddFact, Simplify, Satisfiable Top-level code Satisfiable Setup Term AddFact Assert Formula Assert Assert Equalities Setup CheckSat Assert Solve Update Theory-specific code AddSharedTerm Simplify Rewrite Rewrite p(y), s = update(t, i, 0), x -y -z = 0, z + s[i] = f (x - y), p(x -f (f (z))) Top-level code p(y) Satisfiable p(y) AddFact p(y) Assert Simplify p(y) p(y) Setup Term y Assert Formula Assert Equalities Rewrite p(y) Uninterpreted y p(y) Arrays Arithmetic (Shostak) Update List E p(y), s = update(t, i, 0), x -y -z = 0, z + s[i] = f (x - y), p(x -f (f (z))) Top-level code s = update(t, i, 0) Satisfiable AddFact Assert Simplify s = update(t, i, 0) Setup Term 0 Assert Formula s = ... Assert Equalities Rewrite s = update(t, i, 0) Uninterpreted y p(y) Arrays Arithmetic (Shostak) Update List E 0 s = update(t, i, 0) s = update(t, i, 0) p(y), s = update(t, i, 0), x -y -z = 0, z + s[i] = f (x - y), p(x -f (f (z))) Top-level code x -y -z = 0 Satisfiable Assert AddFact x -y = z0 x =-z y+ Setup Term y+z Assert Formula x = ... Simplify x=y+z Assert Equalities Rewrite x=y+z Uninterpreted y p(y) Arrays Arithmetic (Shostak) Update List E 0 s = update(t, i, 0) s = update(t, i, 0) y + z x=y+z p(y), s = update(t, i, 0), x -y -z = 0, z + s[i] = f (x - y), p(x -f (f (z))) Top-level code z + s[i] = f (x - y) z+s[i]= ... Satisfiable AddFact Assert Simplify z = f (z) z = f (z) f (z) Setup Term Assert z=f (z) Assert Formula Equalities z = f (z) Uninterpreted y p(y) z f (z ) z = f (z) Arrays y s[i] z x0 Rewrite xz - s[i] y 0 Arithmetic (Shostak) Update List E 0 s = update(t, i, 0) s = update(t, i, 0) y + z x=y+z z = f (z) p(y), s = update(t, i, 0), x -y -z = 0, z + s[i] = f (x - y), p(x -f (f (z))) Top-level code p(x -f (f (z))) p(x -…) Satisfiable Assert AddFact Simplify p (y ) -f (z) z (z)) fy(z)xf (f p (y ) Setup Term Assert Formula p (y ) Uninterpreted y p(y) z f (z ) z = f (z) p (y ) Arrays Assert Equalities Rewrite z(z)) f (f fx (z) -f (z) f (z) y Arithmetic (Shostak) Update List E 0 s = update(t, i, 0) s = update(t, i, 0) y + z = y + f (z) x = y + f (z) z = f (z) Implementation: Contributions Better implementation of Nelson-Oppen Online algorithm Each theory only needs to consider a subset of the shared terms Simplify phase Can reduce number of shared terms Equality reasoning is only done once Simple algorithm with detailed proof Flexible theory interface Combined with Shostak Generalizes original Shostak algorithm Efficient: same data structure for E and A Outline Validity Checking Overview Methods for Combining Theories Implementation Adapting Techniques from Propositional Satisfiability The Problem Combining with SAT Results Contributions and Conclusions The Problem Recall the top-level algorithm x>y true y > x x = y y>x x=y false y > x x = y true y>x x=y Choose an atomic formula Consider two cases: Add to the set of choices made and simplify Add to the set of choices made and simplify Repeat until formula is true or set of choices is unsatisfiable The Problem The choice of which atomic formula to try next can make a dramatic difference in performance SVC includes clever heuristics that improve performance significantly We are convinced that better performance is possible Equivalent formulas can vary significantly in performance Research in a related area, Boolean satisfiability (SAT), has advanced significantly Strategy : Find a way to apply SAT techniques to first-order validity checking Combining with SAT: Approach Generate SAT problem from validity-checking problem Negate the formula whose validity is in question Extract Boolean structure from resulting formula Convert to CNF [Larabee ‘92] Run SAT on converted formula If SAT reports unsatisfiabile, the formula is valid The inverse is not true A satisfying assignment must be checked for first-order consistency Combining with SAT: Initial Results Implementation GRASP SAT engine [Silva ‘96] SVC2 Initial results were disappointing Examples of interest could not be proved by just considering Boolean structure SAT techniques do not compensate for the loss of information resulting from translation to SAT Idea : Incrementally give SAT more information Combining with SAT: Conflict Clauses A conflict clause captures a minimal set of decisions that lead to a conflict and keeps SAT from ever making the same set of choices f (x ) = f (y ) y > x x y true y > x x y false y > x x y y>x xy true Unsatisfiable f (x ) f (y ) yx x=y true xy true false Combining with SAT: Conflict Clauses How do we get a conflict clause from the first-order satisfiability algorithm Using all decisions too slow Black-box minimization methods too slow Solution : Use proof-production! Aaron Stump has extended several SVC decision procedures to produce a proof for every result deduced By looking at what assumptions are used in a proof of inconsistency, a conflict clause can be obtained Results Test Case SVC (no heuristics) Decisions SVC (current heuristics) Time (s) Decisions Time(s) SVC2 with SAT Decisions Time(s) fb_var_12_11 17484 6.8 14386 6.0 257 0.8 fb_var_5_11 73484 29.0 60236 25.3 279 0.8 fb_var_6_12 25156 8.0 19533 5.9 79 0.1 pp-bloaddata-a 93637 55.4 902 1.9 894 5.8 pp-bloaddata 344893 292.9 35491 18.5 629 4.1 pp-dmem2 361854 293.6 47989 26.3 775 6.0 3547 2 3484 1.9 174 0.5 260 0.3 384 0.4 1244 10.0 dlx-dmem 2809 1.8 655 0.8 2149 30.1 dlx-regfile 989 0.9 936 1.1 40999 1132 pp-invariant dlx-pc Results: Preliminary Conclusions Naïve approach does not work well Adding conflict clauses results in dramatic speed-ups on several examples Most helpful on formulas with more Boolean structure Still more work to be done Find out source of performance problems Compare to related work [Goel et al. ‘98] [Bryant et al. ‘99] Outline Validity Checking Overview Methods for Combining Theories Implementation Adapting Techniques from Propositional Satisfiability Contributions and Conclusions Thesis Contributions A new presentation of the core of Shostak’s algorithm Easier to understand and prove correct Can be applied directly to produce decision procedures Forms the foundation of a generalization A new variation of Nelson-Oppen Eliminates purification phase Fewer formulas given to each theory Easier to implement Easier to combine with Shostak A new algorithm combining Shostak and Nelson-Oppen Theoretical result relating convex and stable-infinite Generalization of Shostak’s original method Thesis Contributions A detailed and provably correct implementation Online Optimized to eliminate redundant equality reasoning Optimized to reduce number of shared terms Flexible theory API Faster search by combining with SAT Methodology and implementation for extracting CNF Better performance via conflict clauses Conflict clauses from proofs (with Aaron Stump) Dramatic improvements on several examples Future Work Relaxing restrictions on theories and formulas Non-disjoint signatures Non-stably-infinite theories Formulas with quantifiers Individual Theories Efficient implementation for Presburger arithmetic Better techniques for accommodating third-party decision procedures SAT Understand cases where combination with SAT fails Acknowledgements Advisor: David Dill Orals Committee: John Gill, Zohar Manna, John Mitchell, Natarajan Shankar Stanford Associates: Aaron Stump, Jeremy Levitt, Satyaki Das, Jeffrey Xsu, Robert Jones, Vijay Ganesh, Kanna Shimizu, Husam Abu-Haimed, Jens Skakkebæk, David Park, Shankar Govindaraju, Madan Musuvathi, Chris Wilson Others: Cesare Tinelli SVC Users Personal: Friends and family Validity Checking Overview Top-level Algorithm CheckValid(h,c) IF c = true THEN RETURN TRUE; CheckValid(h,c) IF !Satisfiable(h) THEN RETURN FALSE; IF IF c c = = true falseTHEN THENRETURN RETURNTRUE; FALSE; IF !Satisfiable(h) THEN RETURN subgoals := ApplyTactic(h,c); FALSE; IF c = false RETURN FALSE; FOREACH (h,c)THEN in subgoals DO subgoals := ApplyTactic(h,c); IF !CheckValid(h,c) THEN RETURN FALSE; FOREACH (h,c) in subgoals DO RETURN TRUE; IF !CheckValid(h,c) THEN RETURN FALSE; RETURN TRUE; ApplyTactic(h,c) Let e be an atomic formula appearing in c; h1 := AddFact(h,e); If CheckValid( T, ) = TRUE , then T = c1 := Simplify(h1,c); h2 := AddFact(h,!e); c2 := Simplify(h2,c); RETURN {(h1,c1),(h2,c2)}; Shostak’s Method: Convexity A set of literals S is convex in a theory T if T S does not entail any disjunction of equalities without entailing one of the equalities itself A theory T is convex if every set of literals in the language of T is convex in T Shostak’s Method: Requirements on T Shostak Theory T Signature of T contains no predicate symbols T is convex Canonizer such that a,b. T = a =b iff a = b Solver such that if T = a b , then a =b { false } Otherwise: a =b = a set of equations E in solved form T = a =b x. E, where x is the set of variables appearing in E, but not in a or b. The variables in x are guaranteed to be fresh. The Simplified Algorithm Given a set of equations and disequations Step 1: Use the solver to convert into an equisatisfiable set of equations E in solved form Step 2: Use this set of equations together with the canonizer to check if any disequality is violated Suppose a b canon (E (a ) ) = canon (E (b ) ) T = E (a ) = E (b ) T E = a = b T E { a b } is unsatisfiable Technical detail: The method is complete only for convex theories Shostak’s Method: The Algorithm Shostak,,, := ; WHILE DO BEGIN Remove some equality a = b from ; Let a’:= a and b’:= b; Let ’:= a’= b’; IF ’ = false THEN RETURN FALSE; Let := ’ U ’; END IF a = b for some a b in THEN RETURN FALSE; ELSE RETURN TRUE; Shostak(,,,) = TRUE iff is satisfiable in T Nelson-Oppen: Definitions Theories must be stably-infinite A theory T is stably-infinite if every quantifier-free formula is satisfiable in T iff it is satisfiable in an infinite model of T Terminology for combinations of theories Theories T1, T2, … Tn with signatures 1, 2, … n As with Shostak, signatures must be disjoint Members of i are called i-symbols An expression containing only i-symbols is called pure An i-term is a constant i-symbol, an application of a functional i-symbol, or an i-variable Each variable is associated arbitrarily with a theory Nelson-Oppen: Definitions Terminology for combinations of theories (continued) An i-predicate is the application of a predicate i-symbol An atomic i-formula is an i-predicate or an equation whose left-hand side is an i-term An i-literal is an atomic i-formula or its negation An occurrence of a term is i-alien if it is a j-term (i j) and all its super-terms are i-terms If S is a set of terms, then an arrangement of S is a set of equations and disequations induced by a partition of S S = { a , b , c } Partition P = { { a , b } , { c } } Arrangement : { a = b , a c , b c } Nelson-Oppen: Purification Phase NO-Purify() WHILE != DO BEGIN Let be some i-literal in ; IF is pure THEN Remove from ; i := i U {}; ELSE Let t be an i-alien j-term in ; Replace every occurrence of t in with a new j-variable z; := U { j = t }; ENDIF END RETURN 1^…^n; is satisfiable in T iff 1 ^ 2 ^ … n is satisfiable in T Nelson-Oppen: Check Phase NO-Check(1,...n,Sat1,…,Satn) Let S be the set of variables which appear in more than one i; Let A be an arrangement of S; sat := TRUE; FOREACH i DO BEGIN sat := sat ^ Sati(i^A); END RETURN sat; The second step is non-deterministic 1 ^ 2 ^ … n is satisfiable in T iff it is possible for NO-Check to return TRUE If the theories are convex, the algorithm can be determinized inexpensively Nelson-Oppen: A Variation NO-Check(,Sat1,…,Satn) Let S be the set of terms which are i-alien in either an i-literal or an i-term in ; Let A be an arrangement of S; sat := TRUE; FOREACH set of i-literals i in DO BEGIN sat := sat ^ Sati(i^A); END RETURN sat; The purification phase can be eliminated S is a set of terms rather than a set of variables In calls to Sati , i-alien terms are treated as variables Combining Shostak and Nelson-Oppen NO-Shostak(,,,SatNO) Let S be the set of shared terms; Let be the 1-equalities, the 1-disequalities, and NO the 2-literals in ; := ; LOOP BEGIN IF !SatNO(NO^A=) THEN RETURN FALSE; ELSE IF !SatNO(NO^A) THEN Choose a,b from S such that T2NOA |= a=b, but a=b A= ELSE IF = THEN BREAK; ELSE Remove some equality a = b from ; Let a’:= (a) and b’:= (b); Let ’:= (a’= b’); IF ’ = {false} THEN RETURN FALSE; Let := ’() U ’; END IF A THEN RETURN TRUE; ELSE RETURN FALSE; Combining Shostak and Nelson-Oppen NO-Shostak(,,) := ;S := ; LOOP BEGIN IF t1=f(x1,…,xn), t2=f(y1,…,yn) with t1,t2 in S and norm(xi)=norm(yi) but norm(t1) != norm(t2) THEN a := t1, b := t2; ELSE IF = THEN RETURN TRUE; ELSE Remove some equality a = b from ; Let a’:= can(a) and b’:= can(b); Add each sub-term of a’,b’ to S; Let ’:= (a’= b’); IF ’ = {false} THEN RETURN FALSE; Let := ’() U ’; END RETURN TRUE; Individual Theories SVC contains decision procedures for a number of individual theories Pure equality with uninterpreted functions Real linear arithmetic Arrays Bit-vectors Records In our efforts to revisit and improve these decision procedures, a number of interesting issues were uncovered Finite domains Strategies for arithmetic Finite Domains Theoretical technicalitiy Cannot directly combine a theory with only finite models Not stably-infinite Union of theories likely to actually be inconsistent Solution: Form an extended theory whose relativized reduct with respect to a new predicate P is the theory with a finite domain. Implementation strategy for nonconvexity Keep track of the terms for which P holds Use graph coloring to determine satisfiability Arithmetic Suppose we want to handle linear arithmetic formulas with mixed variable types: some real and some integer. One approach is the following: Split weak inequalities into the disjunction of an equation and a strong inequality Use Shostak-style solver to eliminate all equations that can be solved for a real variable Use Fourier-Motzkin techniques to eliminate all real variables from inequalities Eliminate disequalities which can be solved for a real variable What’s left can be done with Presburger decision procedures Math symbols ()

Descargar
# Checking Validity of Quantifier