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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 48 |
1 files changed, 26 insertions, 22 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4fae94254..bf501ec37 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -132,36 +132,40 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { } +Theory* TheoryEngine::theoryOf(TypeNode t) { + // FIXME: we don't yet have a Type-to-Theory map. When we do, + // look up the type of the var and return that Theory (?) + + // The following JUST hacks around this lack of a table + Kind k = t.getKind(); + if(k == kind::TYPE_CONSTANT) { + switch(TypeConstant tc = t.getConst<TypeConstant>()) { + case BOOLEAN_TYPE: + return d_theoryOfTable[kind::CONST_BOOLEAN]; + case INTEGER_TYPE: + return d_theoryOfTable[kind::CONST_INTEGER]; + case REAL_TYPE: + return d_theoryOfTable[kind::CONST_RATIONAL]; + case KIND_TYPE: + default: + Unhandled(tc); + } + } + + return d_theoryOfTable[k]; +} + + Theory* TheoryEngine::theoryOf(TNode n) { Kind k = n.getKind(); Assert(k >= 0 && k < kind::LAST_KIND); if(n.getMetaKind() == kind::metakind::VARIABLE) { - // FIXME: we don't yet have a Type-to-Theory map. When we do, - // look up the type of the var and return that Theory (?) - - //The following JUST hacks around this lack of a table - TypeNode t = n.getType(); - Kind k = t.getKind(); - if(k == kind::TYPE_CONSTANT) { - switch(TypeConstant tc = t.getConst<TypeConstant>()) { - case BOOLEAN_TYPE: - return d_theoryOfTable[kind::CONST_BOOLEAN]; - case INTEGER_TYPE: - return d_theoryOfTable[kind::CONST_INTEGER]; - case REAL_TYPE: - return d_theoryOfTable[kind::CONST_RATIONAL]; - case KIND_TYPE: - default: - Unhandled(tc); - } - } - - return d_theoryOfTable[k]; + return theoryOf(n.getType()); } else if(k == kind::EQUAL) { // equality is special: use LHS - return theoryOf(n[0]); + return theoryOf(n[0].getType()); } else { // use our Kind-to-Theory mapping return d_theoryOfTable[k]; |