6 Combination of decision procedures (1185842), страница 6
Текст из файла (страница 6)
Is it SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIWhich variables are shared? allICheck sat of F1 .
Is it SAT? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIWhich variables are shared? allICheck sat of F1 . Is it SAT? yesICheck sat of F2 . Is it SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIWhich variables are shared? allICheck sat of F1 .
Is it SAT? yesICheck sat of F2 . Is it SAT? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIWhich variables are shared? allICheck sat of F1 .
Is it SAT? yesICheck sat of F2 . Is it SAT? yesINow, for each pair of shared variable xi , xj , we query whether F1 or F2imply xi = xjVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contF1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zConsider the query x = y – is it implied by either F1 or F2 ?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yINow, propagate this to T= , so F10 becomes:F10 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yINow, propagate this to T= , so F10 becomes:F10 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yICheck sat of F10 .
Is it SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yINow, propagate this to T= , so F10 becomes:F10 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yICheck sat of F10 . Is it SAT? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yINow, propagate this to T= , so F10 becomes:F10 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yICheck sat of F10 .
Is it SAT? yesIAre we done?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIConsider the query x = y – is it implied by either F1 or F2 ? implied by F2Iy + z ≤ x ∧ 0 ≤ z imply 0 ≤ z ≤ x − y, i.e., y ≤ xISince we also have x ≤ y, TQ implies x = yINow, propagate this to T= , so F10 becomes:F10 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yICheck sat of F10 . Is it SAT? yesIAre we done? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories26/44Example, contF1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zSince F1 changed, need to check if it implies any new equalityVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality? yes, w1 = w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality? yes, w1 = w2INow, we add w1 = w2 to F2 :F2 : w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality? yes, w1 = w2INow, we add w1 = w2 to F2 :F2 : w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IWe recheck sat of F2 .
Is it SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality? yes, w1 = w2INow, we add w1 = w2 to F2 :F2 : w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IWe recheck sat of F2 . Is it SAT? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zISince F1 changed, need to check if it implies any new equalityIDoes it imply a new equality? yes, w1 = w2INow, we add w1 = w2 to F2 :F2 : w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IWe recheck sat of F2 .
Is it SAT? yesIStill not done b/c need to check if F2 implies any new equalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories27/44Example, contF1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2Consider the query w3 = z ?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories28/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IConsider the query w3 = z ?Iw3 = w1 − w2 and w1 = w2 imply w3 = 0Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories28/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IConsider the query w3 = z ?Iw3 = w1 − w2 and w1 = w2 imply w3 = 0ISince x = y, y + z ≤ x implies z ≤ 0Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories28/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IConsider the query w3 = z ?Iw3 = w1 − w2 and w1 = w2 imply w3 = 0ISince x = y, y + z ≤ x implies z ≤ 0ISince z ≤ 0 and 0 ≤ z , we have z = 0Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories28/44Example, contF1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = yw3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w1 = w2IConsider the query w3 = z ?Iw3 = w1 − w2 and w1 = w2 imply w3 = 0ISince x = y, y + z ≤ x implies z ≤ 0ISince z ≤ 0 and 0 ≤ z , we have z = 0IThus, TQ answer ”yes” for query w3 = zVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories28/44Example, contINow, propagate w3 = z to F1 :F1 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = y ∧ w3 = zVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories29/44Example, contINow, propagate w3 = z to F1 :F1 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = y ∧ w3 = zIIs this sat?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories29/44Example, contINow, propagate w3 = z to F1 :F1 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = y ∧ w3 = zIIs this sat?INo, because w3 = z implies f (w3 ) = f (z )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories29/44Example, contINow, propagate w3 = z to F1 :F1 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = y ∧ w3 = zIIs this sat?INo, because w3 = z implies f (w3 ) = f (z )IThis contradicts f (w3 ) 6= f (z )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories29/44Example, contINow, propagate w3 = z to F1 :F1 : w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z ) ∧ x = y ∧ w3 = zIIs this sat?INo, because w3 = z implies f (w3 ) = f (z )IThis contradicts f (w3 ) 6= f (z )IThus, original formula is UNSATVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories29/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesIConsider the following TZ ∪ T= formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesIConsider the following TZ ∪ T= formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IIs this formula SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesIConsider the following TZ ∪ T= formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IIs this formula SAT? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesIConsider the following TZ ∪ T= formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IIs this formula SAT? noILet’s see what happens if we use technique described so farVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Non-Convex TheoriesIUnfortunately, technique discussed so far does not work for non-convextheoriesIConsider the following TZ ∪ T= formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IIs this formula SAT? noILet’s see what happens if we use technique described so farIIf we purify, we get the following formulas:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories30/44Example, contF1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Is F1 SAT?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Is F1 SAT? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :IIs F1 SAT? yesIIs F2 SAT?Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :IIs F1 SAT? yesIIs F2 SAT? yesVijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs F1 SAT? yesIIs F2 SAT? yesIDoes F1 imply a new equality by itself?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs F1 SAT? yesIIs F2 SAT? yesIDoes F1 imply a new equality by itself? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs F1 SAT? yesIIs F2 SAT? yesIDoes F1 imply a new equality by itself? noIDoes F2 imply a new equality by itself?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs F1 SAT? yesIIs F2 SAT? yesIDoes F1 imply a new equality by itself? noIDoes F2 imply a new equality by itself? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Example, contF1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs F1 SAT? yesIIs F2 SAT? yesIDoes F1 imply a new equality by itself? noIDoes F2 imply a new equality by itself? noIThus technique discussed so far returns sat, although formula in unsatVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories31/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownIThus, it is not enough to query individual equality relations betweenvariablesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownIThus, it is not enough to query individual equality relations betweenvariablesIWe also have to query and propagate disjunctions of equalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownIThus, it is not enough to query individual equality relations betweenvariablesIWe also have to query and propagate disjunctions of equalitiesITwo questions:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownIThus, it is not enough to query individual equality relations betweenvariablesIWe also have to query and propagate disjunctions of equalitiesITwo questions:1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
