6 Combination of decision procedures (Презентации лекций), страница 4

Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories16/44Shared vs. Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories16/44Shared vs. Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories16/44Shared vs.

Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableIConsider the following purified formula:w1 = x + y ∧ y = 1 ∧ w2 = 2 ∧ w1 = f (x ) ∧ f (x ) 6= f (w2 )|{z}|{z}TZVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringT=Lecture 16: Decision Procedures for Combination Theories16/44Shared vs. Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableIConsider the following purified formula:w1 = x + y ∧ y = 1 ∧ w2 = 2 ∧ w1 = f (x ) ∧ f (x ) 6= f (w2 )|{z}|{z}TZIT=Which variables are shared?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories16/44Shared vs.

Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableIConsider the following purified formula:w1 = x + y ∧ y = 1 ∧ w2 = 2 ∧ w1 = f (x ) ∧ f (x ) 6= f (w2 )|{z}|{z}TZIT=Which variables are shared? w1 , x , w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories16/44Shared vs. Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableIConsider the following purified formula:w1 = x + y ∧ y = 1 ∧ w2 = 2 ∧ w1 = f (x ) ∧ f (x ) 6= f (w2 )|{z}|{z}TZIWhich variables are shared? w1 , x , w2IWhich variables are unshared?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringT=Lecture 16: Decision Procedures for Combination Theories16/44Shared vs.

Unshared VariablesIAfter purification, we have decomposed a formula F into two pureformulas F1 and F2IIf x occurs in both F1 and F2 , x is called shared variableIIf y occurs only in F1 or only in F2 , it is called unshared variableIConsider the following purified formula:w1 = x + y ∧ y = 1 ∧ w2 = 2 ∧ w1 = f (x ) ∧ f (x ) 6= f (w2 )|{z}|{z}TZIWhich variables are shared? w1 , x , w2IWhich variables are unshared? yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringT=Lecture 16: Decision Procedures for Combination Theories16/44Two Phases of Nelson-OppenIRecall: Nelson-Oppen method has two different phases:1. Purification: Seperate formula F in T1 ∪ T2 into two formulas F1 in T1and F2 in T22.

Equality propagation: Propagate all relevant equalities between theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories17/44Two Phases of Nelson-OppenIRecall: Nelson-Oppen method has two different phases:1. Purification: Seperate formula F in T1 ∪ T2 into two formulas F1 in T1and F2 in T22. Equality propagation: Propagate all relevant equalities between theoriesITalk about second phase nextVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories17/44Two Phases of Nelson-OppenIRecall: Nelson-Oppen method has two different phases:1.

Purification: Seperate formula F in T1 ∪ T2 into two formulas F1 in T1and F2 in T22. Equality propagation: Propagate all relevant equalities between theoriesITalk about second phase nextIBut this phase is different for convex vs. non-convex theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories17/44Two Phases of Nelson-OppenIRecall: Nelson-Oppen method has two different phases:1. Purification: Seperate formula F in T1 ∪ T2 into two formulas F1 in T1and F2 in T22. Equality propagation: Propagate all relevant equalities between theoriesITalk about second phase nextIBut this phase is different for convex vs.

non-convex theoriesISo, need to talk about convex and non-convex theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories17/44Convex TheoriesITheory T is called convex if for every conjunctive formula F :Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories18/44Convex TheoriesITheory T is called convex if for every conjunctive formula F :IIf F ⇒Vijay Ganesh(Original notes from Isil Dillig),Wni=1 xi= yi for finite nECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories18/44Convex TheoriesITheory T is called convex if for every conjunctive formula F :WnIIf F ⇒IThen, F ⇒ xi = yi for some i ∈ [1, n]Vijay Ganesh(Original notes from Isil Dillig),i=1 xi= yi for finite nECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories18/44Convex TheoriesIITheory T is called convex if for every conjunctive formula F :WnIIf F ⇒IThen, F ⇒ xi = yi for some i ∈ [1, n]i=1 xi= yi for finite nThus, in convex theory, if F implies disjunction of equalities, F alsoimplies at least one of these equalities on its ownVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories18/44Convex TheoriesITheory T is called convex if for every conjunctive formula F :WnIIf F ⇒IThen, F ⇒ xi = yi for some i ∈ [1, n]i=1 xi= yi for finite nIThus, in convex theory, if F implies disjunction of equalities, F alsoimplies at least one of these equalities on its ownIIf a theory does not satisfy this condition, it is called non-convexVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories18/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2? noIIs TZ convex?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2? noIIs TZ convex? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2? noIIs TZ convex? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Examples of Convex and Non-Convex TheoriesIExample: Consider formula 1 ≤ x ∧ x ≤ 2 in TZIDoes it imply x = 1 ∨ x = 2? yesIDoes it imply x = 1? noIDoes it imply x = 2? noIIs TZ convex? noITheory of equality T= is convexVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories19/44Nelson-Oppen for Convex vs Non-Convex TheoriesICombining decision procedures for two convex theories is easier and moreefficientVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories20/44Nelson-Oppen for Convex vs Non-Convex TheoriesICombining decision procedures for two convex theories is easier and moreefficientIIntuition: When we have convexity, there are fewer facts that need to becommunicated between theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories20/44Nelson-Oppen for Convex vs Non-Convex TheoriesICombining decision procedures for two convex theories is easier and moreefficientIIntuition: When we have convexity, there are fewer facts that need to becommunicated between theoriesIUnfortunately, some theories of interest such as TZ and theory of arraysare non-convexVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories20/44Nelson-Oppen for Convex vs Non-Convex TheoriesICombining decision procedures for two convex theories is easier and moreefficientIIntuition: When we have convexity, there are fewer facts that need to becommunicated between theoriesIUnfortunately, some theories of interest such as TZ and theory of arraysare non-convexIIf one of the theories we want to combine is non-convex, decisionprocedure for combination theory is much less efficentVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories20/44Nelson-Oppen for Convex vs Non-Convex TheoriesICombining decision procedures for two convex theories is easier and moreefficientIIntuition: When we have convexity, there are fewer facts that need to becommunicated between theoriesIUnfortunately, some theories of interest such as TZ and theory of arraysare non-convexIIf one of the theories we want to combine is non-convex, decisionprocedure for combination theory is much less efficentIWe’ll first talk about Nelson-Oppen method for convex theories, then fornon-convex theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories20/44Nelson-Oppen Method for Convex TheoriesIGiven formula F in T1 ∪ T2 (T1 , T2 convex), want to decide if F issatisfiableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories21/44Nelson-Oppen Method for Convex TheoriesIGiven formula F in T1 ∪ T2 (T1 , T2 convex), want to decide if F issatisfiableIFirst, purify F into F1 and F2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories21/44Nelson-Oppen Method for Convex TheoriesIGiven formula F in T1 ∪ T2 (T1 , T2 convex), want to decide if F issatisfiableIFirst, purify F into F1 and F2IRun decision procedures for T1 , T2 to decide sat.