Propagating Disjunction of Equalities To propagate disjunctions we perform a case split: If a disjunction Ev..vEn is discovered: Save the current state of the prover for i=1 to n{ broadcast E if no contradiction arises then return "satisfiable" restore the saved prover state return "unsatisfiable" Prof.Necula CS 294-8 Lecture 12 11
Prof. Necula CS 294-8 Lecture 12 11 Propagating Disjunction of Equalities • To propagate disjunctions we perform a case split: • If a disjunction E1 … En is discovered: Save the current state of the prover for i = 1 to n { broadcast Ei if no contradiction arises then return “satisfiable” restore the saved prover state } return “unsatisfiable
Handling Non-Convex Theories Case splitting is expensive Must backtrack(performance--) Must implement all satisfiability procedures in incremental fashion(simplicity -- 。 In some cases the splitting can be prohibitive: Take pointers for example. upd(upd((upd(m,ix)..nx),inx)= upd((upd(m,j1,x),...jn-1,x) sel(m,i)≠×入.Asel(m,i)≠× entails vj≠kij≠ik (a conjunction of length n entails n2 disjuncts) Prof.Necula CS 294-8 Lecture 12 12
Prof. Necula CS 294-8 Lecture 12 12 Handling Non-Convex Theories • Case splitting is expensive – Must backtrack (performance --) – Must implement all satisfiability procedures in incremental fashion (simplicity --) • In some cases the splitting can be prohibitive: – Take pointers for example. upd(upd(…(upd(m, i1 , x), …, in-1 , x), in , x) = upd(…(upd(m, j1 , x), …, jn-1 , x) sel(m, i1 ) x … sel(m, in ) x entails j k i j ik (a conjunction of length n entails n2 disjuncts)
Forward vs.Backward Theorem Proving Prof.Necula CS 294-8 Lecture 12 13
Prof. Necula CS 294-8 Lecture 12 13 Forward vs. Backward Theorem Proving
Forward vs.Backward Theorem Proving The state of a prover can be expressed as: H1A.AHn→？G Given the hypotheses H;try to derive goal G A forward theorem prover derives new hypotheses,in hope of deriving G -IfH1A.AHn→H then move to state H1A.AHAH→？G -Success state:H1∧.∧G∧.Hn→？G A forward theorem prover uses heuristics to reach G Or it can exhaustively derive everything that is derivable Prof.Necula CS 294-8 Lecture 12 14
Prof. Necula CS 294-8 Lecture 12 14 Forward vs. Backward Theorem Proving • The state of a prover can be expressed as: H1 … Hn ? G – Given the hypotheses Hi try to derive goal G • A forward theorem prover derives new hypotheses, in hope of deriving G – If H1 … Hn H then move to state H1 … Hn H ? G – Success state: H1 … G … Hn ? G • A forward theorem prover uses heuristics to reach G – Or it can exhaustively derive everything that is derivable !