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

Purification: Seperate formula F in T1 ∪ T2 into two formulas F1 in T1and F2 in T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories8/44Nelson-Oppen OverviewINelson-Oppen method has conceptually 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 Theories8/44Nelson-Oppen OverviewINelson-Oppen method has conceptually 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 theoriesIPurification step is always the same for any arbitrary theoryVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories8/44Nelson-Oppen OverviewINelson-Oppen method has conceptually 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 theoriesIPurification step is always the same for any arbitrary theoryIBut equality propagation is different between convex and non-convextheoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories8/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:1.

F1 belongs only to T1 (is ”pure”)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:1. F1 belongs only to T1 (is ”pure”)2. F2 belong only to T2 (is ”pure”)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:1.

F1 belongs only to T1 (is ”pure”)2. F2 belong only to T2 (is ”pure”)3. F1 ∧ F2 is equisatisfiable as FVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:1. F1 belongs only to T1 (is ”pure”)2. F2 belong only to T2 (is ”pure”)3. F1 ∧ F2 is equisatisfiable as FIResulting formula after purification is not equivalentVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44Purification OverviewIInput to Nelson-Oppen is formula F in T1 ∪ T2IGoal of purification is to separate F into formulas F1 and F2 such that:1.

F1 belongs only to T1 (is ”pure”)2. F2 belong only to T2 (is ”pure”)3. F1 ∧ F2 is equisatisfiable as FIResulting formula after purification is not equivalentIBut since goal is to decide satisfiability, this is good enoughVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories9/44How To PurifyITo purify formula F , exhaustively apply the following:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories10/44How To PurifyITo purify formula F , exhaustively apply the following:1.

Consider term f (. . . , ti , . . .). If f ∈ Σi but ti is not a term in Ti , replace tiwith fresh variable z and conjoin z = tiVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories10/44How To PurifyITo purify formula F , exhaustively apply the following:1. Consider term f (.

. . , ti , . . .). If f ∈ Σi but ti is not a term in Ti , replace tiwith fresh variable z and conjoin z = ti2. Consider predicate p(. . . , ti , . . .). If p ∈ Σi but ti is not a term in Ti ,replace ti with fresh variable w and conjoin w = tiVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories10/44How To PurifyITo purify formula F , exhaustively apply the following:1. Consider term f (.

. . , ti , . . .). If f ∈ Σi but ti is not a term in Ti , replace tiwith fresh variable z and conjoin z = ti2. Consider predicate p(. . . , ti , . . .). If p ∈ Σi but ti is not a term in Ti ,replace ti with fresh variable w and conjoin w = tiILiterals in resulting formula belong to either only T1 or T2 .Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories10/44How To PurifyITo purify formula F , exhaustively apply the following:1. Consider term f (. . . , ti , .

. .). If f ∈ Σi but ti is not a term in Ti , replace tiwith fresh variable z and conjoin z = ti2. Consider predicate p(. . . , ti , . . .). If p ∈ Σi but ti is not a term in Ti ,replace ti with fresh variable w and conjoin w = tiILiterals in resulting formula belong to either only T1 or T2 .IThus, we can write F as a conjunction of formulas F1 in T1 and F2 in T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories10/44Purification Example 1IConsider T= ∪ TQ formula x ≤ f (x ) + 1Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories11/44Purification Example 1IConsider T= ∪ TQ formula x ≤ f (x ) + 1IIs this formula already pure?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories11/44Purification Example 1IConsider T= ∪ TQ formula x ≤ f (x ) + 1IIs this formula already pure? NoVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories11/44Purification Example 1IConsider T= ∪ TQ formula x ≤ f (x ) + 1IIs this formula already pure? NoISince f (x ) is not in TQ , replace with new variable y and add equalityconstraint y = f (x )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories11/44Purification Example 1IConsider T= ∪ TQ formula x ≤ f (x ) + 1IIs this formula already pure? NoISince f (x ) is not in TQ , replace with new variable y and add equalityconstraint y = f (x )IThus, formula after purification:x ≤ y + 1 ∧ y = f (x )| {z }| {z }TQVijay Ganesh(Original notes from Isil Dillig),T=ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories11/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”IIs the term x + g(y) pure?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”IIs the term x + g(y) pure? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”IIs the term x + g(y) pure? noIHow do we purify it?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”IIs the term x + g(y) pure? noIHow do we purify it? replace g(y) with z1 , add constraint z1 = g(y)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example IIIConsider following Σ= ∪ ΣZ formula:f (x + g(y)) ≤ g(a) + f (b)IEasiest to purify ”inside out”IIs the term x + g(y) pure? noIHow do we purify it? replace g(y) with z1 , add constraint z1 = g(y)IResulting formula:f (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories12/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noIHow do we purify?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noIHow do we purify? replace x + z1 with z2 , add constraint z2 = x + z1Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noIHow do we purify? replace x + z1 with z2 , add constraint z2 = x + z1IResulting formula:f (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noIHow do we purify? replace x + z1 with z2 , add constraint z2 = x + z1IResulting formula:f (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IIs formula purified now?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (x + z1 ) ≤ g(a) + f (b) ∧ z1 = g(y)IIs f (x + z1 ) pure? noIHow do we purify? replace x + z1 with z2 , add constraint z2 = x + z1IResulting formula:f (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IIs formula purified now? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories13/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)IHow do we purify?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)IHow do we purify? replace g(a) with z3 and f (b) with z4 , add constraintz3 = g(a) ∧ z4 = f (b)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)IHow do we purify? replace g(a) with z3 and f (b) with z4 , add constraintz3 = g(a) ∧ z4 = f (b)IResulting formula:f (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)IHow do we purify? replace g(a) with z3 and f (b) with z4 , add constraintz3 = g(a) ∧ z4 = f (b)IResulting formula:f (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IIs formula purified now?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ g(a) + f (b) ∧ z1 = g(y) ∧ z2 = x + z1IWhich terms/predicate is impure? g(a) + f (b)IHow do we purify? replace g(a) with z3 and f (b) with z4 , add constraintz3 = g(a) ∧ z4 = f (b)IResulting formula:f (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IIs formula purified now? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories14/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4IHow do we purify?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4IHow do we purify? replace f (z2 ) with z5 , add constraint z5 = f (z2 )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4IHow do we purify? replace f (z2 ) with z5 , add constraint z5 = f (z2 )IResulting formula:z5 ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧z3 = g(a) ∧ z4 = f (b) ∧ z5 = f (z2 )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4IHow do we purify? replace f (z2 ) with z5 , add constraint z5 = f (z2 )IResulting formula:z5 ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧z3 = g(a) ∧ z4 = f (b) ∧ z5 = f (z2 )IIs formula purified now?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Purification Example II, contf (z2 ) ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧ z3 = g(a) ∧ z4 = f (b)IWhich terms/predicate is impure? f (z2 ) ≤ z3 + z4IHow do we purify? replace f (z2 ) with z5 , add constraint z5 = f (z2 )IResulting formula:z5 ≤ z3 + z4 ∧ z1 = g(y) ∧ z2 = x + z1 ∧z3 = g(a) ∧ z4 = f (b) ∧ z5 = f (z2 )IIs formula purified now? Yes, finally!Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories15/44Shared vs.