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

ECE750T-28:Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures forCombination TheoriesVijay Ganesh(Original notes from Isil Dillig)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories1/44MotivationISo far, learned about decision procedures for useful theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 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 Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IThis formula does not belong to any individual theoryVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IThis formula does not belong to any individual theoryIBut it does belong, for instance, to combination of T= and TZVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2IGiven decision procedures for T1 and T2 , we want a decision procedure todecide satisfiability of formulas in T1 ∪ T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2IGiven decision procedures for T1 and T2 , we want a decision procedure todecide satisfiability of formulas in T1 ∪ T2IToday’s lecture: Learn about Nelson-Oppen method for constructingdecision procedure for combined theory T1 ∪ T2 from individual decisionprocedures for T1 and T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44Nelson-Oppen OverviewVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2IThen, combine T1 ∪ T2 and T3 again using Nelson-OppenVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2IThen, combine T1 ∪ T2 and T3 again using Nelson-OppenIHowever, Nelson-Oppen imposes some restrictions on theories that can becombinedVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1.

Only allows combining quantifier-free fragmentsVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1. Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNFVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1.

Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNF3. Signatures can only share equality: Σ1 ∩ Σ2 = {=}Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1. Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNF3.