What Theories Can be Combined? Only theories without common interpreted symbols But Ok if one theory takes the symbol uninterpreted Only certain theories can be combined Consider (Z,+,and Equality -Consider:1≤×≤2Λa=1Ab=2∧f(X)≠f(a)Af(X)≠f(b) No equalities and no contradictions are discovered yet,unsatisfiable A theory is non-convex when a set of literals entails a dis junction of equalities without entailing any single equality Prof.Necula CS 294-8 Lecture 12 9Prof. Necula CS 294-8 Lecture 12 9 What Theories Can be Combined? • Only theories without common interpreted symbols – But Ok if one theory takes the symbol uninterpreted • Only certain theories can be combined – Consider (Z, +, ·) and Equality – Consider: 1  x  2  a = 1  b = 2  f(x)  f(a)  f(x)  f(b) – No equalities and no contradictions are discovered – Yet, unsatisfiable • A theory is non-convex when a set of literals entails a disjunction of equalities without entailing any single equality