diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-22 21:55:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-22 21:55:28 +0000 |
commit | 62ec86743289b26241d69b1701d4b3f547ee2bed (patch) | |
tree | fc4d460a9326eaae1e481cf0f48ff6c15738150e /src/theory/theory_engine.h | |
parent | 27a24d7f553a0b3981e18418a67edb3c4bfa52e9 (diff) |
incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems. should discuss at tuesday meeting. resolves bug 187.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bb9131023..fbe9fba16 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -247,6 +247,13 @@ public: } /** + * Get the theory associated to a given TypeNode. + * + * @returns the theory owning the type + */ + theory::Theory* theoryOf(TypeNode t); + + /** * Get the theory associated to a given Node. * * @returns the theory, or NULL if the TNode is |