summaryrefslogtreecommitdiff
path: root/src/theory/booleans
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/booleans')
-rw-r--r--src/theory/booleans/Makefile.am4
-rw-r--r--src/theory/booleans/kinds10
-rw-r--r--src/theory/booleans/theory_bool.cpp116
-rw-r--r--src/theory/booleans/theory_bool.h12
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp72
-rw-r--r--src/theory/booleans/theory_bool_rewriter.h32
6 files changed, 118 insertions, 128 deletions
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index c8a9b4dbd..0263ae017 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libbooleans.la
libbooleans_la_SOURCES = \
theory_bool.h \
theory_bool.cpp \
- theory_bool_type_rules.h
+ theory_bool_type_rules.h \
+ theory_bool_rewriter.h \
+ theory_bool_rewriter.cpp
EXTRA_DIST = kinds
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ac6b05881..25ca1cfe3 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -4,7 +4,13 @@
# src/theory/builtin/kinds.
#
-theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
+theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
+
+properties finite
+
+rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
+
+sort BOOLEAN_TYPE "Boolean type"
constant CONST_BOOLEAN \
bool \
@@ -19,3 +25,5 @@ operator IMPLIES 2 "logical implication"
operator OR 2: "logical or"
operator XOR 2 "exclusive or"
operator ITE 3 "if-then-else"
+
+endtheory \ No newline at end of file
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index b1ff472ac..f8071d45d 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -24,122 +24,6 @@ namespace CVC4 {
namespace theory {
namespace booleans {
-RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) {
- if(n.getKind() == kind::IFF) {
- NodeManager* nodeManager = NodeManager::currentNM();
- Node tt = nodeManager->mkConst(true);
- Node ff = nodeManager->mkConst(false);
-
- // rewrite simple cases of IFF
- if(n[0] == tt) {
- // IFF true x
- return RewriteAgain(n[1]);
- } else if(n[1] == tt) {
- // IFF x true
- return RewriteAgain(n[0]);
- } else if(n[0] == ff) {
- // IFF false x
- return RewriteAgain(n[1].notNode());
- } else if(n[1] == ff) {
- // IFF x false
- return RewriteAgain(n[0].notNode());
- } else if(n[0] == n[1]) {
- // IFF x x
- return RewriteComplete(tt);
- } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
- // IFF (NOT x) x
- return RewriteComplete(ff);
- } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
- // IFF x (NOT x)
- return RewriteComplete(ff);
- }
- } else if(n.getKind() == kind::ITE) {
- // non-Boolean-valued ITEs should have been removed in place of
- // a variable
- Assert(n.getType().isBoolean());
-
- NodeManager* nodeManager = NodeManager::currentNM();
-
- // rewrite simple cases of ITE
- if(n[0] == nodeManager->mkConst(true)) {
- // ITE true x y
- return RewriteAgain(n[1]);
- } else if(n[0] == nodeManager->mkConst(false)) {
- // ITE false x y
- return RewriteAgain(n[2]);
- } else if(n[1] == n[2]) {
- // ITE c x x
- return RewriteAgain(n[1]);
- }
- }
-
- return RewriteComplete(n);
-}
-
-
-RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) {
- if(n.getKind() == kind::IFF) {
- NodeManager* nodeManager = NodeManager::currentNM();
- Node tt = nodeManager->mkConst(true);
- Node ff = nodeManager->mkConst(false);
-
- // rewrite simple cases of IFF
- if(n[0] == tt) {
- // IFF true x
- return RewriteComplete(n[1]);
- } else if(n[1] == tt) {
- // IFF x true
- return RewriteComplete(n[0]);
- } else if(n[0] == ff) {
- // IFF false x
- return RewriteAgain(n[1].notNode());
- } else if(n[1] == ff) {
- // IFF x false
- return RewriteAgain(n[0].notNode());
- } else if(n[0] == n[1]) {
- // IFF x x
- return RewriteComplete(tt);
- } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
- // IFF (NOT x) x
- return RewriteComplete(ff);
- } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
- // IFF x (NOT x)
- return RewriteComplete(ff);
- }
-
- if(n[1] < n[0]) {
- // normalize (IFF x y) ==> (IFF y x), if y < x
- return RewriteComplete(n[1].iffNode(n[0]));
- }
- } else if(n.getKind() == kind::ITE) {
- // non-Boolean-valued ITEs should have been removed in place of
- // a variable
- Assert(n.getType().isBoolean());
-
- NodeManager* nodeManager = NodeManager::currentNM();
-
- // rewrite simple cases of ITE
- if(n[0] == nodeManager->mkConst(true)) {
- // ITE true x y
- return RewriteComplete(n[1]);
- } else if(n[0] == nodeManager->mkConst(false)) {
- // ITE false x y
- return RewriteComplete(n[2]);
- } else if(n[1] == n[2]) {
- // ITE c x x
- return RewriteComplete(n[1]);
- }
-
- if(n[0].getKind() == kind::NOT) {
- // rewrite (ITE (NOT c) x y) to (ITE c y x)
- Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]);
- return RewriteComplete(out);
- }
- }
-
- return RewriteComplete(n);
-}
-
Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
NodeManager* nodeManager = NodeManager::currentNM();
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index fa826539c..5d91842d7 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
class TheoryBool : public Theory {
public:
- TheoryBool(int id, context::Context* c, OutputChannel& out) :
- Theory(id, c, out) {
+ TheoryBool(context::Context* c, OutputChannel& out) :
+ Theory(THEORY_BOOL, c, out) {
}
void preRegisterTerm(TNode n) {
@@ -42,17 +42,9 @@ public:
Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
}
- void check(Effort e) { Unimplemented(); }
- void propagate(Effort e) { Unimplemented(); }
- void explain(TNode n, Effort e) { Unimplemented(); }
-
- void presolve(){ Unimplemented(); }
Node getValue(TNode n, TheoryEngine* engine);
- RewriteResponse preRewrite(TNode n, bool topLevel);
- RewriteResponse postRewrite(TNode n, bool topLevel);
-
std::string identify() const { return std::string("TheoryBool"); }
};
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
new file mode 100644
index 000000000..a62bc6fa0
--- /dev/null
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -0,0 +1,72 @@
+#include <algorithm>
+#include "theory/booleans/theory_bool_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+ Node tt = nodeManager->mkConst(true);
+ Node ff = nodeManager->mkConst(false);
+
+ switch(n.getKind()) {
+ case kind::NOT: {
+ if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff);
+ if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt);
+ if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]);
+ break;
+ }
+ case kind::IFF: {
+ // rewrite simple cases of IFF
+ if(n[0] == tt) {
+ // IFF true x
+ return RewriteResponse(REWRITE_AGAIN, n[1]);
+ } else if(n[1] == tt) {
+ // IFF x true
+ return RewriteResponse(REWRITE_AGAIN, n[0]);
+ } else if(n[0] == ff) {
+ // IFF false x
+ return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+ } else if(n[1] == ff) {
+ // IFF x false
+ return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ } else if(n[0] == n[1]) {
+ // IFF x x
+ return RewriteResponse(REWRITE_DONE, tt);
+ } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+ // IFF (NOT x) x
+ return RewriteResponse(REWRITE_DONE, ff);
+ } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+ // IFF x (NOT x)
+ return RewriteResponse(REWRITE_DONE, ff);
+ }
+ break;
+ }
+ case kind::ITE: {
+ // non-Boolean-valued ITEs should have been removed in place of
+ // a variable
+ Assert(n.getType().isBoolean());
+ // rewrite simple cases of ITE
+ if(n[0] == tt) {
+ // ITE true x y
+ return RewriteResponse(REWRITE_AGAIN, n[1]);
+ } else if(n[0] == ff) {
+ // ITE false x y
+ return RewriteResponse(REWRITE_AGAIN, n[2]);
+ } else if(n[1] == n[2]) {
+ // ITE c x x
+ return RewriteResponse(REWRITE_AGAIN, n[1]);
+ }
+ break;
+ }
+ default:
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ return RewriteResponse(REWRITE_DONE, n);
+}
+
+}
+}
+}
+
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
new file mode 100644
index 000000000..62eed9e2b
--- /dev/null
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -0,0 +1,32 @@
+/*
+ * theory_bool_rewriter.h
+ *
+ * Created on: Dec 21, 2010
+ * Author: dejan
+ */
+
+#pragma once
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+class TheoryBoolRewriter {
+
+public:
+
+ static RewriteResponse preRewrite(TNode node);
+ static RewriteResponse postRewrite(TNode node) {
+ return preRewrite(node);
+ }
+
+ static void init() {}
+ static void shutdown() {}
+
+};
+
+}
+}
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback