diff options
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 564 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 69 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 5 | ||||
-rw-r--r-- | src/theory/rewriter.h | 2 |
4 files changed, 417 insertions, 223 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index c53610efa..b13cb82b3 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -25,10 +25,30 @@ namespace CVC4 { namespace theory { namespace booleans { -RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { - return preRewrite(node); +void TheoryBoolRewriter::registerRewrites(Rewriter* rewriter) +{ + rewriter->registerPreRewrite(kind::CONST_BOOLEAN, identityRewrite); + rewriter->registerPostRewrite(kind::CONST_BOOLEAN, identityRewrite); + rewriter->registerPreRewrite(kind::NOT, rewriteNot); + rewriter->registerPostRewrite(kind::NOT, rewriteNot); + rewriter->registerPreRewrite(kind::OR, rewriteOr); + rewriter->registerPostRewrite(kind::OR, rewriteOr); + rewriter->registerPreRewrite(kind::AND, rewriteAnd); + rewriter->registerPostRewrite(kind::AND, rewriteAnd); + rewriter->registerPreRewrite(kind::IMPLIES, rewriteImplies); + rewriter->registerPostRewrite(kind::IMPLIES, rewriteImplies); + rewriter->registerPreRewrite(kind::XOR, rewriteXor); + rewriter->registerPostRewrite(kind::XOR, rewriteXor); + rewriter->registerPreRewrite(kind::ITE, rewriteIte); + rewriter->registerPostRewrite(kind::ITE, rewriteIte); + rewriter->registerPreRewriteEqual(THEORY_BOOL, rewriteEqual); + rewriter->registerPostRewriteEqual(THEORY_BOOL, rewriteEqual); } +RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { Unreachable(); } + +RewriteResponse TheoryBoolRewriter::postRewrite(TNode n) { Unreachable(); } + /** * flattenNode looks for children of same kind, and if found merges * them into the parent. @@ -134,243 +154,345 @@ inline Node makeNegation(TNode n){ } } -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::OR: { - bool done = true; - TNode::iterator i = n.begin(), iend = n.end(); - for(; i != iend; ++i) { - if (*i == tt) return RewriteResponse(REWRITE_DONE, tt); - if (*i == ff) done = false; - if ((*i).getKind() == kind::OR) done = false; - } - if (!done) { - return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff); - } - break; - } - case kind::AND: { - bool done = true; - TNode::iterator i = n.begin(), iend = n.end(); - for(; i != iend; ++i) { - if (*i == ff) return RewriteResponse(REWRITE_DONE, ff); - if (*i == tt) done = false; - if ((*i).getKind() == kind::AND) done = false; +RewriteResponse TheoryBoolRewriter::rewriteNot(RewriteEnvironment* re, TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + 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]); + + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteOr(RewriteEnvironment* re, TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + bool done = true; + TNode::iterator i = n.begin(), iend = n.end(); + for (; i != iend; ++i) + { + if (*i == tt) return RewriteResponse(REWRITE_DONE, tt); + if (*i == ff) done = false; + if ((*i).getKind() == kind::OR) done = false; + } + if (!done) + { + return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff); + } + + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteAnd(RewriteEnvironment* re, TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + bool done = true; + TNode::iterator i = n.begin(), iend = n.end(); + for (; i != iend; ++i) + { + if (*i == ff) return RewriteResponse(REWRITE_DONE, ff); + if (*i == tt) done = false; + if ((*i).getKind() == kind::AND) done = false; + } + if (!done) + { + RewriteResponse ret = + flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt); + Debug("bool-flatten") << n << ": " << ret.node << std::endl; + return ret; + } + + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteImplies(RewriteEnvironment* re, + TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); + if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteEqual(RewriteEnvironment* re, + TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + // 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, makeNegation(n[1])); + } + else if (n[1] == ff) + { + // IFF x false + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); + } + 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); + } + else if (n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) + { + // a : (= i x) + // i : (= j k) + // x : (= y z) + + // assume wlog k, z are constants and j is the same symbol as y + // (iff (= j k) (= j z)) + // if k = z + // then (iff (= j k) (= j k)) => true + // else + // (iff (= j k) (= j z)) <=> b + // b : (and (not (= j k)) (not (= j z))) + // (= j k) (= j z) | a b + // f f | t t + // f t | f f + // t f | f f + // t t | * f + // * j cannot equal both k and z in a theory model + TNode t, c; + if (n[0][0].isConst()) + { + c = n[0][0]; + t = n[0][1]; } - if (!done) { - RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt); - Debug("bool-flatten") << n << ": " << ret.node << std::endl; - return ret; + else if (n[0][1].isConst()) + { + c = n[0][1]; + t = n[0][0]; } - break; - } - case kind::IMPLIES: { - if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); - if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); - if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); - if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); - break; - } - case kind::EQUAL: { - // 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, makeNegation(n[1])); - } else if(n[1] == ff) { - // IFF x false - return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); - } 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); - } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) { - // a : (= i x) - // i : (= j k) - // x : (= y z) - - // assume wlog k, z are constants and j is the same symbol as y - // (iff (= j k) (= j z)) - // if k = z - // then (iff (= j k) (= j k)) => true - // else - // (iff (= j k) (= j z)) <=> b - // b : (and (not (= j k)) (not (= j z))) - // (= j k) (= j z) | a b - // f f | t t - // f t | f f - // t f | f f - // t t | * f - // * j cannot equal both k and z in a theory model - TNode t,c; - if (n[0][0].isConst()) { - c = n[0][0]; - t = n[0][1]; + bool matchesForm = false; + bool constantsEqual = false; + if (!c.isNull()) + { + if (n[1][0] == t && n[1][1].isConst()) + { + matchesForm = true; + constantsEqual = (n[1][1] == c); } - else if (n[0][1].isConst()) { - c = n[0][1]; - t = n[0][0]; + else if (n[1][1] == t && n[1][0].isConst()) + { + matchesForm = true; + constantsEqual = (n[1][0] == c); } - bool matchesForm = false; - bool constantsEqual = false; - if (!c.isNull()) { - if (n[1][0] == t && n[1][1].isConst()) { - matchesForm = true; - constantsEqual = (n[1][1] == c); - } - else if (n[1][1] == t && n[1][0].isConst()) { - matchesForm = true; - constantsEqual = (n[1][0] == c); - } + } + if (matchesForm) + { + if (constantsEqual) + { + return RewriteResponse(REWRITE_DONE, tt); } - if(matchesForm){ - if(constantsEqual){ - return RewriteResponse(REWRITE_DONE, tt); - }else{ - Cardinality kappa = t.getType().getCardinality(); - Cardinality two(2l); - if(kappa.knownLessThanOrEqual(two)){ - return RewriteResponse(REWRITE_DONE, ff); - }else{ - Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1])); - return RewriteResponse(REWRITE_AGAIN, neitherEquality); - } + else + { + Cardinality kappa = t.getType().getCardinality(); + Cardinality two(2l); + if (kappa.knownLessThanOrEqual(two)) + { + return RewriteResponse(REWRITE_DONE, ff); + } + else + { + Node neitherEquality = + (makeNegation(n[0])).andNode(makeNegation(n[1])); + return RewriteResponse(REWRITE_AGAIN, neitherEquality); } } } - break; - } - case kind::XOR: { - // rewrite simple cases of XOR - if(n[0] == tt) { - // XOR true x - return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); - } else if(n[1] == tt) { - // XOR x true - return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); - } else if(n[0] == ff) { - // XOR false x + } + + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteXor(RewriteEnvironment* re, TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + // rewrite simple cases of XOR + if (n[0] == tt) + { + // XOR true x + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); + } + else if (n[1] == tt) + { + // XOR x true + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); + } + else if (n[0] == ff) + { + // XOR false x + return RewriteResponse(REWRITE_AGAIN, n[1]); + } + else if (n[1] == ff) + { + // XOR x false + return RewriteResponse(REWRITE_AGAIN, n[0]); + } + else if (n[0] == n[1]) + { + // XOR x x + return RewriteResponse(REWRITE_DONE, ff); + } + else if (n[0].getKind() == kind::NOT && n[0][0] == n[1]) + { + // XOR (NOT x) x + return RewriteResponse(REWRITE_DONE, tt); + } + else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) + { + // XOR x (NOT x) + return RewriteResponse(REWRITE_DONE, tt); + } + return RewriteResponse(REWRITE_DONE, n); +} + +RewriteResponse TheoryBoolRewriter::rewriteIte(RewriteEnvironment* re, TNode n) +{ + NodeManager* nm = re->getNodeManager(); + Node tt = nm->mkConst(true); + Node ff = nm->mkConst(false); + + // non-Boolean-valued ITEs should have been removed in place of + // a variable + // rewrite simple cases of ITE + if (n[0].isConst()) + { + if (n[0] == tt) + { + // ITE true x y + + Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[1]); - } else if(n[1] == ff) { - // XOR x false + } + else + { + Assert(n[0] == ff); + // ITE false x y + Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl; + return RewriteResponse(REWRITE_AGAIN, n[2]); + } + } + else if (n[1].isConst()) + { + if (n[1] == tt && n[2] == ff) + { + Debug("bool-ite") << "n[1] ==tt && n[2] ==ff " << n << ": " << n[0] + << std::endl; return RewriteResponse(REWRITE_AGAIN, n[0]); - } else if(n[0] == n[1]) { - // XOR x x - return RewriteResponse(REWRITE_DONE, ff); - } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { - // XOR (NOT x) x - return RewriteResponse(REWRITE_DONE, tt); - } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { - // XOR x (NOT x) - return RewriteResponse(REWRITE_DONE, tt); } - break; - } - case kind::ITE: { - // non-Boolean-valued ITEs should have been removed in place of - // a variable - // rewrite simple cases of ITE - if (n[0].isConst()) { - if (n[0] == tt) { - // ITE true x y - - Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl; - return RewriteResponse(REWRITE_AGAIN, n[1]); - } else { - Assert(n[0] == ff); - // ITE false x y - Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl; - return RewriteResponse(REWRITE_AGAIN, n[2]); - } - } else if (n[1].isConst()) { - if (n[1] == tt && n[2] == ff) { - Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl; - return RewriteResponse(REWRITE_AGAIN, n[0]); - } - else if (n[1] == ff && n[2] == tt) { - Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl; - return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); - } - // else if(n[1] == ff){ - // Node resp = (n[0].notNode()).andNode(n[2]); - // return RewriteResponse(REWRITE_AGAIN, resp); - // } + else if (n[1] == ff && n[2] == tt) + { + Debug("bool-ite") << "n[1] ==ff && n[2] ==tt " << n << ": " + << n[0].notNode() << std::endl; + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } - // else if (n[2].isConst()) { - // if(n[2] == ff){ - // Node resp = (n[0]).andNode(n[1]); - // return RewriteResponse(REWRITE_AGAIN, resp); - // } + // else if(n[1] ==ff){ + // Node resp = (n[0].notNode()).andNode(n[2]); + // return RewriteResponse(REWRITE_AGAIN, resp); // } + } + // else if (n[2].isConst()) { + // if(n[2] ==ff){ + // Node resp = (n[0]).andNode(n[1]); + // return RewriteResponse(REWRITE_AGAIN, resp); + // } + // } - int parityTmp; - if ((parityTmp = equalityParity(n[1], n[2])) != 0) { - Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); - Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp - << " " << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); + int parityTmp; + if ((parityTmp = equalityParity(n[1], n[2])) != 0) + { + Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); + Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp << " " << n + << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now // } else if (n[0].getKind() == kind::NOT) { // return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1])); - } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){ - // (parityTmp == 1) if n[0] == n[1] - // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1] - - // if n[1] is constant this can loop, this is possible in prewrite - Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]); - Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp - << " " << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){ - // (parityTmp == 1) if n[0] == n[2] - // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2] - Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt); - Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp - << " " << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } else if(n[1].getKind() == kind::ITE && - (parityTmp = equalityParity(n[0], n[1][0])) != 0){ - // (parityTmp == 1) then n : (ite c (ite c x y) z) - // (parityTmp > 1) then n : (ite c (ite (not c) x y) z) or - // n: (ite (not c) (ite c x y) z) - Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]); - Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp - << " " << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } else if(n[2].getKind() == kind::ITE && - (parityTmp = equalityParity(n[0], n[2][0])) != 0){ - // (parityTmp == 1) then n : (ite c x (ite c y z)) - // (parityTmp > 1) then n : (ite c x (ite (not c) y z)) or - // n: (ite (not c) x (ite c y z)) - Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]); - Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp - << " " << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } - break; } - default: - return RewriteResponse(REWRITE_DONE, n); + else if (!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0) + { + // (parityTmp == 1) if n[0] == n[1] + // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1] + + // if n[1] is constant this can loop, this is possible in prewrite + Node resp = n[0].iteNode((parityTmp == 1) ? tt : ff, n[2]); + Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp << " " << n + << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + else if (!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0) + { + // (parityTmp == 1) if n[0] == n[2] + // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2] + Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt); + Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp << " " << n + << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + else if (n[1].getKind() == kind::ITE + && (parityTmp = equalityParity(n[0], n[1][0])) != 0) + { + // (parityTmp == 1) then n : (ite c (ite c x y) z) + // (parityTmp > 1) then n : (ite c (ite (not c) x y) z) or + // n: (ite (not c) (ite c x y) z) + Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]); + Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp << " " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + else if (n[2].getKind() == kind::ITE + && (parityTmp = equalityParity(n[0], n[2][0])) != 0) + { + // (parityTmp == 1) then n : (ite c x (ite c y z)) + // (parityTmp > 1) then n : (ite c x (ite (not c) y z)) or + // n: (ite (not c) x (ite c y z)) + Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]); + Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp << " " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); } return RewriteResponse(REWRITE_DONE, n); } diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 8fc65932e..7ca77eea6 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -20,6 +20,7 @@ #ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H +#include "theory/rewriter.h" #include "theory/theory_rewriter.h" namespace CVC4 { @@ -29,9 +30,73 @@ namespace booleans { class TheoryBoolRewriter : public TheoryRewriter { public: - RewriteResponse preRewrite(TNode node) override; - RewriteResponse postRewrite(TNode node) override; + void registerRewrites(Rewriter* rewriter) override; + RewriteResponse preRewrite(TNode n) override; + RewriteResponse postRewrite(TNode n) override; + private: + /** + * Rewrites nodes of kind `NOT`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteNot(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `OR`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteOr(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `AND`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteAnd(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `IMPLIES`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteImplies(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `EQUAL`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteEqual(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `XOR`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteXor(RewriteEnvironment* re, TNode n); + + /** + * Rewrites nodes of kind `ITE`. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The result of rewriting `n` + */ + static RewriteResponse rewriteIte(RewriteEnvironment* re, TNode n); }; /* class TheoryBoolRewriter */ }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index da06b053c..912ecad1e 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -81,6 +81,11 @@ struct RewriteStackElement { NodeBuilder<> builder; }; +NodeManager* RewriteEnvironment::getNodeManager() +{ + return NodeManager::currentNM(); +} + RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n) { return RewriteResponse(REWRITE_DONE, n); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f7298e1fb..1e87e1a99 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -33,6 +33,8 @@ class RewriterInitializer; */ class RewriteEnvironment { + public: + NodeManager* getNodeManager(); }; /** |