diff options
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 10 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 116 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 12 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 72 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 32 |
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() {} + +}; + +} +} +} |