summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/cnf_stream.cpp7
-rw-r--r--src/theory/theory_engine.cpp48
-rw-r--r--src/theory/theory_engine.h7
-rw-r--r--test/unit/theory/theory_engine_white.h43
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<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];
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
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<theory::bv::TheoryBV*>(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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback