From 62ec86743289b26241d69b1701d4b3f547ee2bed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 22 Jul 2010 21:55:28 +0000 Subject: [PATCH] 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. --- src/prop/cnf_stream.cpp | 7 ++++ src/theory/theory_engine.cpp | 48 ++++++++++++++------------ src/theory/theory_engine.h | 7 ++++ test/unit/theory/theory_engine_white.h | 43 +++++++++++------------ 4 files changed, 61 insertions(+), 44 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9136a73c3..e95322348 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -364,6 +364,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { case AND: nodeLit = handleAnd(node); break; + case EQUAL: + if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) { + nodeLit = handleIff(node[0].iffNode(node[1])); + } else { + nodeLit = convertAtom(node); + } + break; default: { //TODO make sure this does not contain any boolean substructure 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()) { + 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()) { - 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]; 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 @@ -246,6 +246,13 @@ public: delete d_sharedTermManager; } + /** + * 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. * diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 570fa74a4..7f0e7d2db 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -96,7 +96,7 @@ public: RewriteResponse preRewrite(TNode n, bool topLevel) { if(s_expected.empty()) { - cout << std::endl + cout << std::endl << Expr::setdepth(-1) << "didn't expect anything more, but got" << std::endl << " PRE " << topLevel << " " << identify() << " " << n << std::endl; } @@ -109,7 +109,7 @@ public: expected.d_theory != this || expected.d_node != n || expected.d_topLevel != topLevel) { - cout << std::endl + cout << std::endl << Expr::setdepth(-1) << "HAVE PRE " << topLevel << " " << identify() << " " << n << std::endl << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl; } @@ -124,7 +124,7 @@ public: RewriteResponse postRewrite(TNode n, bool topLevel) { if(s_expected.empty()) { - cout << std::endl + cout << std::endl << Expr::setdepth(-1) << "didn't expect anything more, but got" << std::endl << " POST " << topLevel << " " << identify() << " " << n << std::endl; } @@ -137,7 +137,7 @@ public: expected.d_theory != this || expected.d_node != n || expected.d_topLevel != topLevel) { - cout << std::endl + cout << std::endl << Expr::setdepth(-1) << "HAVE POST " << topLevel << " " << identify() << " " << n << std::endl << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl; } @@ -208,7 +208,7 @@ public: d_theoryEngine->d_theoryOfTable. registerTheory(reinterpret_cast(d_bv)); - Debug.on("theory-rewrite"); + //Debug.on("theory-rewrite"); } void tearDown() { @@ -294,56 +294,55 @@ public: // We WOULD expect that the commented-out calls were made, except // for the cache FakeTheory::expect(PRE, d_bool, n, true); - FakeTheory::expect(PRE, d_uf, f1eqf2, true); - FakeTheory::expect(PRE, d_uf, f1, false); + FakeTheory::expect(PRE, d_arith, f1eqf2, true); + FakeTheory::expect(PRE, d_uf, f1, true); FakeTheory::expect(PRE, d_builtin, f, true); FakeTheory::expect(POST, d_builtin, f, true); FakeTheory::expect(PRE, d_arith, one, true); FakeTheory::expect(POST, d_arith, one, true); - FakeTheory::expect(POST, d_uf, f1, false); - FakeTheory::expect(PRE, d_uf, f2, false); + FakeTheory::expect(POST, d_uf, f1, true); + FakeTheory::expect(PRE, d_uf, f2, true); //FakeTheory::expect(PRE, d_builtin, f, true); //FakeTheory::expect(POST, d_builtin, f, true); FakeTheory::expect(PRE, d_arith, two, true); FakeTheory::expect(POST, d_arith, two, true); - FakeTheory::expect(POST, d_uf, f2, false); - FakeTheory::expect(POST, d_uf, f1eqf2, true); + FakeTheory::expect(POST, d_uf, f2, true); + FakeTheory::expect(POST, d_arith, f1eqf2, true); FakeTheory::expect(PRE, d_bool, or1, false); FakeTheory::expect(PRE, d_bool, and1, false); - FakeTheory::expect(PRE, d_uf, ffxeqgy, true); - FakeTheory::expect(PRE, d_uf, ffx, false); + FakeTheory::expect(PRE, d_arith, ffxeqgy, true); + FakeTheory::expect(PRE, d_uf, ffx, true); FakeTheory::expect(PRE, d_uf, fx, false); //FakeTheory::expect(PRE, d_builtin, f, true); //FakeTheory::expect(POST, d_builtin, f, true); FakeTheory::expect(PRE, d_arith, x, true); FakeTheory::expect(POST, d_arith, x, true); FakeTheory::expect(POST, d_uf, fx, false); - FakeTheory::expect(POST, d_uf, ffx, false); - FakeTheory::expect(PRE, d_uf, gy, false); + FakeTheory::expect(POST, d_uf, ffx, true); + FakeTheory::expect(PRE, d_uf, gy, true); FakeTheory::expect(PRE, d_builtin, g, true); FakeTheory::expect(POST, d_builtin, g, true); FakeTheory::expect(PRE, d_arith, y, true); FakeTheory::expect(POST, d_arith, y, true); - FakeTheory::expect(POST, d_uf, gy, false); - FakeTheory::expect(POST, d_uf, ffxeqgy, true); + FakeTheory::expect(POST, d_uf, gy, true); + FakeTheory::expect(POST, d_arith, ffxeqgy, true); FakeTheory::expect(PRE, d_uf, z1eqz2, true); FakeTheory::expect(PRE, d_uf, z1, false); FakeTheory::expect(POST, d_uf, z1, false); FakeTheory::expect(PRE, d_uf, z2, false); FakeTheory::expect(POST, d_uf, z2, false); FakeTheory::expect(POST, d_uf, z1eqz2, true); - // tricky one: ffx is in cache but for a non-topLevel ! - FakeTheory::expect(PRE, d_uf, ffx, true); + //FakeTheory::expect(PRE, d_uf, ffx, true); //FakeTheory::expect(PRE, d_uf, fx, false); //FakeTheory::expect(POST, d_uf, fx, false); - FakeTheory::expect(POST, d_uf, ffx, true); + //FakeTheory::expect(POST, d_uf, ffx, true); FakeTheory::expect(POST, d_bool, and1, false); - FakeTheory::expect(PRE, d_uf, ffxeqf1, true); + FakeTheory::expect(PRE, d_arith, ffxeqf1, true); //FakeTheory::expect(PRE, d_uf, ffx, false); //FakeTheory::expect(POST, d_uf, ffx, false); //FakeTheory::expect(PRE, d_uf, f1, false); //FakeTheory::expect(POST, d_uf, f1, false); - FakeTheory::expect(POST, d_uf, ffxeqf1, true); + FakeTheory::expect(POST, d_arith, ffxeqf1, true); FakeTheory::expect(POST, d_bool, or1, false); FakeTheory::expect(POST, d_bool, n, true); nOut = d_theoryEngine->rewrite(n); -- 2.30.2