diff options
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 116 |
1 files changed, 0 insertions, 116 deletions
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(); |