diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
commit | 22df6e9e8618614e8c33700c55705266912500ae (patch) | |
tree | 20d78676c1e819517f371e8bc5e6363008fc9154 /src/theory/booleans | |
parent | 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff) |
Substantial Changes:
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 118 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 4 |
2 files changed, 102 insertions, 20 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 9867ccd4e..1caa4b429 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -22,6 +22,10 @@ namespace CVC4 { namespace theory { namespace booleans { +RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { + return preRewrite(node); +} + /** * flattenNode looks for children of same kind, and if found merges * them into the parent. @@ -88,6 +92,40 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) } } +// Equality parity returns +// * 0 if no relation between a and b is found +// * 1 if a == b +// * 2 if a == not(b) +// * 3 or b == not(a) +inline int equalityParity(TNode a, TNode b){ + if(a == b){ + return 1; + }else if(a.getKind() == kind::NOT && a[0] == b){ + return 2; + }else if(b.getKind() == kind::NOT && b[0] == a){ + return 3; + }else{ + return 0; + } +} + +inline Node makeNegation(TNode n){ + bool even = false; + while(n.getKind() == kind::NOT){ + n = n[0]; + even = !even; + } + if(even){ + return n; + } else { + if(n.isConst()){ + return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); + }else{ + return n.notNode(); + } + } +} + RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); Node tt = nodeManager->mkConst(true); @@ -132,7 +170,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); - if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); break; } case kind::IFF: @@ -146,10 +184,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { return RewriteResponse(REWRITE_AGAIN, n[0]); } else if(n[0] == ff) { // IFF false x - return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == ff) { // IFF x false - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == n[1]) { // IFF x x return RewriteResponse(REWRITE_DONE, tt); @@ -207,7 +245,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if(kappa.knownLessThanOrEqual(two)){ return RewriteResponse(REWRITE_DONE, ff); }else{ - Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode()); + Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1])); return RewriteResponse(REWRITE_AGAIN, neitherEquality); } } @@ -219,10 +257,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // rewrite simple cases of XOR if(n[0] == tt) { // XOR true x - return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == tt) { // XCR x true - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == ff) { // XOR false x return RewriteResponse(REWRITE_AGAIN, n[1]); @@ -248,33 +286,79 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { 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) { - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + 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); + // } } - if (n[1] == n[2]) { - return RewriteResponse(REWRITE_AGAIN, n[1]); + // 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].iffNode(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[0] == n[1]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2])); - } else if (n[0] == n[2]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff)); - } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2])); - } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt)); + } 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; } diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 96bd2ae29..ac9469980 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -31,9 +31,7 @@ class TheoryBoolRewriter { public: static RewriteResponse preRewrite(TNode node); - static RewriteResponse postRewrite(TNode node) { - return preRewrite(node); - } + static RewriteResponse postRewrite(TNode node); static void init() {} static void shutdown() {} |