From b70ccff4de0a23bdf11c70002d10a2cc0795a91c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 25 Aug 2018 21:09:22 -0700 Subject: [PATCH] Refactor unconstrained simplification pass (#2374) --- src/Makefile.am | 12 +- .../passes}/unconstrained_simplifier.cpp | 585 +++++++++++------- .../passes}/unconstrained_simplifier.h | 42 +- src/preprocessing/preprocessing_pass.h | 1 + .../preprocessing_pass_context.h | 3 + src/smt/smt_engine.cpp | 35 +- src/theory/theory_engine.cpp | 10 - src/theory/theory_engine.h | 6 - 8 files changed, 408 insertions(+), 286 deletions(-) rename src/{theory => preprocessing/passes}/unconstrained_simplifier.cpp (60%) rename src/{theory => preprocessing/passes}/unconstrained_simplifier.h (56%) diff --git a/src/Makefile.am b/src/Makefile.am index e0a9fb807..3681280ec 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -65,6 +65,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/apply_substs.h \ preprocessing/passes/apply_to_const.cpp \ preprocessing/passes/apply_to_const.h \ + preprocessing/passes/bool_to_bv.cpp \ + preprocessing/passes/bool_to_bv.h \ preprocessing/passes/bv_abstraction.cpp \ preprocessing/passes/bv_abstraction.h \ preprocessing/passes/bv_ackermann.cpp \ @@ -75,6 +77,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_gauss.h \ preprocessing/passes/bv_intro_pow2.cpp \ preprocessing/passes/bv_intro_pow2.h \ + preprocessing/passes/bv_to_bool.cpp \ + preprocessing/passes/bv_to_bool.h \ preprocessing/passes/extended_rewriter_pass.cpp \ preprocessing/passes/extended_rewriter_pass.h \ preprocessing/passes/global_negate.cpp \ @@ -89,10 +93,6 @@ libcvc4_la_SOURCES = \ preprocessing/passes/nl_ext_purify.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ - preprocessing/passes/bool_to_bv.cpp \ - preprocessing/passes/bool_to_bv.h \ - preprocessing/passes/bv_to_bool.cpp \ - preprocessing/passes/bv_to_bool.h \ preprocessing/passes/quantifiers_preprocess.cpp \ preprocessing/passes/quantifiers_preprocess.h \ preprocessing/passes/quantifier_macros.cpp \ @@ -115,6 +115,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/symmetry_detect.h \ preprocessing/passes/synth_rew_rules.cpp \ preprocessing/passes/synth_rew_rules.h \ + preprocessing/passes/unconstrained_simplifier.cpp \ + preprocessing/passes/unconstrained_simplifier.h \ preprocessing/preprocessing_pass.cpp \ preprocessing/preprocessing_pass.h \ preprocessing/preprocessing_pass_context.cpp \ @@ -244,8 +246,6 @@ libcvc4_la_SOURCES = \ theory/type_enumerator.h \ theory/type_set.cpp \ theory/type_set.h \ - theory/unconstrained_simplifier.cpp \ - theory/unconstrained_simplifier.h \ theory/valuation.cpp \ theory/valuation.h \ theory/arith/approx_simplex.cpp \ diff --git a/src/theory/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp similarity index 60% rename from src/theory/unconstrained_simplifier.cpp rename to src/preprocessing/passes/unconstrained_simplifier.cpp index 41529760b..6bb46f3f2 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -11,44 +11,46 @@ ** ** \brief Simplifications based on unconstrained variables ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. **/ +#include "preprocessing/passes/unconstrained_simplifier.h" -#include "theory/unconstrained_simplifier.h" - -#include "theory/rewriter.h" -#include "theory/logic_info.h" #include "smt/smt_statistics_registry.h" +#include "theory/logic_info.h" +#include "theory/rewriter.h" -using namespace std; -using namespace CVC4; -using namespace theory; +namespace CVC4 { +namespace preprocessing { +namespace passes { +using namespace CVC4::theory; -UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context, - const LogicInfo& logicInfo) - : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), - d_context(context), d_substitutions(context), d_logicInfo(logicInfo) +UnconstrainedSimplifier::UnconstrainedSimplifier( + PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "unconstrained-simplifier"), + d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), + d_context(preprocContext->getDecisionContext()), + d_substitutions(preprocContext->getDecisionContext()), + d_logicInfo(preprocContext->getLogicInfo()) { smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); } - UnconstrainedSimplifier::~UnconstrainedSimplifier() { smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); } - -struct unc_preprocess_stack_element { +struct unc_preprocess_stack_element +{ TNode node; TNode parent; unc_preprocess_stack_element(TNode n) : node(n) {} unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {} -};/* struct unc_preprocess_stack_element */ - +}; /* struct unc_preprocess_stack_element */ void UnconstrainedSimplifier::visitAll(TNode assertion) { @@ -64,10 +66,13 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) toVisit.pop_back(); TNodeCountMap::iterator find = d_visited.find(current); - if (find != d_visited.end()) { - if (find->second == 1) { + if (find != d_visited.end()) + { + if (find->second == 1) + { d_visitedOnce.erase(current); - if (current.isVar()) { + if (current.isVar()) + { d_unconstrained.erase(current); } } @@ -78,14 +83,18 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) d_visited[current] = 1; d_visitedOnce[current] = parent; - if (current.getNumChildren() == 0) { - if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) { + if (current.getNumChildren() == 0) + { + if (current.getKind() == kind::VARIABLE + || current.getKind() == kind::SKOLEM) + { d_unconstrained.insert(current); } } - else { - for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { - TNode childNode = *child_it; + else + { + for (TNode childNode : current) + { toVisit.push_back(unc_preprocess_stack_element(childNode, current)); } } @@ -94,18 +103,19 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString()); + Node n = NodeManager::currentNM()->mkSkolem( + "unconstrained", + t, + "a new var introduced because of unconstrained variable " + + var.toString()); return n; } - void UnconstrainedSimplifier::processUnconstrained() { - TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end(); - vector workList; - for ( ; it != iend; ++it) { - workList.push_back(*it); - } + NodeManager* nm = NodeManager::currentNM(); + + vector workList(d_unconstrained.begin(), d_unconstrained.end()); Node currentSub; TNode parent; bool swap; @@ -116,65 +126,94 @@ void UnconstrainedSimplifier::processUnconstrained() TNode current = workList.back(); workList.pop_back(); - for (;;) { + for (;;) + { Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); parent = d_visitedOnce[current]; - if (!parent.isNull()) { + if (!parent.isNull()) + { swap = isSigned = strict = false; bool checkParent = false; - switch (parent.getKind()) { - - // If-then-else operator - any two unconstrained children makes the parent unconstrained - case kind::ITE: { - Assert(parent[0] == current || parent[1] == current || parent[2] == current); - bool uCond = parent[0] == current || d_unconstrained.find(parent[0]) != d_unconstrained.end(); - bool uThen = parent[1] == current || d_unconstrained.find(parent[1]) != d_unconstrained.end(); - bool uElse = parent[2] == current || d_unconstrained.find(parent[2]) != d_unconstrained.end(); - if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + switch (parent.getKind()) + { + // If-then-else operator - any two unconstrained children makes the + // parent unconstrained + case kind::ITE: + { + Assert(parent[0] == current || parent[1] == current + || parent[2] == current); + bool uCond = + parent[0] == current + || d_unconstrained.find(parent[0]) != d_unconstrained.end(); + bool uThen = + parent[1] == current + || d_unconstrained.find(parent[1]) != d_unconstrained.end(); + bool uElse = + parent[2] == current + || d_unconstrained.find(parent[2]) != d_unconstrained.end(); + if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (uThen) { - if (parent[1] != current) { - if (parent[1].isVar()) { + if (uThen) + { + if (parent[1] != current) + { + if (parent[1].isVar()) + { currentSub = parent[1]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[1])); currentSub = d_substitutions.apply(parent[1]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } } - else if (parent[2] != current) { - if (parent[2].isVar()) { + else if (parent[2] != current) + { + if (parent[2].isVar()) + { currentSub = parent[2]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[2])); currentSub = d_substitutions.apply(parent[2]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - else if (uCond) { + else if (uCond) + { Cardinality card = parent.getType().getCardinality(); - if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { - // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result - // is unconstrained + if (card.isFinite() && !card.isLargeFinite() + && card.getFiniteCardinality() == 2) + { + // Special case: condition is unconstrained, then and else are + // different, and total cardinality of the type is 2, then the + // result is unconstrained Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - if (test == NodeManager::currentNM()->mkConst(false)) { + if (test == nm->mkConst(false)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); @@ -185,24 +224,30 @@ void UnconstrainedSimplifier::processUnconstrained() break; } - // Comparisons that return a different type - assuming domains are larger than 1, any - // unconstrained child makes parent unconstrained as well + // Comparisons that return a different type - assuming domains are + // larger than 1, any unconstrained child makes parent unconstrained as + // well case kind::EQUAL: - if (parent[0].getType() != parent[1].getType()) { + if (parent[0].getType() != parent[1].getType()) + { TNode other = (parent[0] == current) ? parent[1] : parent[0]; - if (current.getType().isSubtypeOf(other.getType())) { + if (current.getType().isSubtypeOf(other.getType())) + { break; } } - if( parent[0].getType().isDatatype() ){ + if (parent[0].getType().isDatatype()) + { TypeNode tn = parent[0].getType(); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton( tn.toType() ) ){ - //domain size may be 1 + if (dt.isRecursiveSingleton(tn.toType())) + { + // domain size may be 1 break; } } - if( parent[0].getType().isBoolean() ){ + if (parent[0].getType().isBoolean()) + { checkParent = true; break; } @@ -212,18 +257,21 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::GT: case kind::GEQ: { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - Assert(parent[0] != parent[1] && - (parent[0] == current || parent[1] == current)); - if (currentSub.isNull()) { + Assert(parent[0] != parent[1] + && (parent[0] == current || parent[1] == current)); + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; } - else { + else + { currentSub = Node(); } break; @@ -236,24 +284,28 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::UMINUS: ++d_numUnconstrainedElim; Assert(parent[0] == current); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; break; - // Unary operators that propagate unconstrainedness and return a different type + // Unary operators that propagate unconstrainedness and return a + // different type case kind::BITVECTOR_EXTRACT: ++d_numUnconstrainedElim; Assert(parent[0] == current); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; break; - // Operators returning same type requiring all children to be unconstrained + // Operators returning same type requiring all children to be + // unconstrained case kind::AND: case kind::OR: case kind::IMPLIES: @@ -263,13 +315,16 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_NOR: { bool allUnconstrained = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode child : parent) + { + if (d_unconstrained.find(child) == d_unconstrained.end()) + { allUnconstrained = false; break; } } - if (allUnconstrained) { + if (allUnconstrained) + { checkParent = true; } } @@ -283,135 +338,177 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: { + case kind::BITVECTOR_SMOD: + { bool allUnconstrained = true; bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { allUnconstrained = false; break; } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { allDifferent = false; break; } } } - if (allUnconstrained && allDifferent) { + if (allUnconstrained && allDifferent) + { checkParent = true; } break; } - // Requires all children to be unconstrained and different, and returns a different type + // Requires all children to be unconstrained and different, and returns + // a different type case kind::BITVECTOR_CONCAT: { bool allUnconstrained = true; bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { allUnconstrained = false; break; } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { allDifferent = false; break; } } } - if (allUnconstrained && allDifferent) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (allUnconstrained && allDifferent) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; } - else { + else + { currentSub = Node(); } } } break; - // N-ary operators returning same type requiring at least one child to be unconstrained + // N-ary operators returning same type requiring at least one child to + // be unconstrained case kind::PLUS: case kind::MINUS: - if (current.getType().isInteger() && - !parent.getType().isInteger()) { + if (current.getType().isInteger() && !parent.getType().isInteger()) + { break; } case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: case kind::BITVECTOR_PLUS: - case kind::BITVECTOR_SUB: - checkParent = true; - break; + case kind::BITVECTOR_SUB: checkParent = true; break; - // Multiplication/division: must be non-integer and other operand must be non-zero - case kind::MULT: { + // Multiplication/division: must be non-integer and other operand must + // be non-zero + case kind::MULT: case kind::DIVISION: + { Assert(parent.getNumChildren() == 2); TNode other; - if (parent[0] == current) { + if (parent[0] == current) + { other = parent[1]; } - else { + else + { Assert(parent[1] == current); other = parent[0]; } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - if (current.getType().isInteger() && other.getType().isInteger()) { - Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger()); - if (parent.getKind() == kind::DIVISION) { + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + if (current.getType().isInteger() && other.getType().isInteger()) + { + Assert(parent.getKind() == kind::DIVISION + || parent.getType().isInteger()); + if (parent.getKind() == kind::DIVISION) + { break; } } ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - else { - // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained - if (parent.getKind() == kind::DIVISION && current == parent[1]) { + else + { + // if only the denominator of a division is unconstrained, can't + // set it to 0 so the result is not unconstrained + if (parent.getKind() == kind::DIVISION && current == parent[1]) + { break; } - NodeManager* nm = NodeManager::currentNM(); - // if we are an integer, the only way we are unconstrained is if we are a MULT by -1 - if (current.getType().isInteger()) { + // if we are an integer, the only way we are unconstrained is if + // we are a MULT by -1 + if (current.getType().isInteger()) + { // div/mult by 1 should have been simplified Assert(other != nm->mkConst(1)); - if (other == nm->mkConst(-1)) { - // div by -1 should have been simplified + // div by -1 should have been simplified + if (other != nm->mkConst(-1)) + { + break; + } + else + { Assert(parent.getKind() == kind::MULT); Assert(parent.getType().isInteger()); } - else { - break; - } } - else { - // TODO: could build ITE here + else + { + // TODO(#2377): could build ITE here Node test = other.eqNode(nm->mkConst(0)); - if (Rewriter::rewrite(test) != nm->mkConst(false)) { + if (Rewriter::rewrite(test) != nm->mkConst(false)) + { break; } } ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; @@ -425,97 +522,120 @@ void UnconstrainedSimplifier::processUnconstrained() { bool found = false; bool done = false; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if ((*child_it) == current) { - if (found) { + + for (TNode child : parent) + { + if (child == current) + { + if (found) + { done = true; break; } found = true; continue; } - else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) { - continue; - } - else { - NodeManager* nm = NodeManager::currentNM(); - Node extractOp = nm->mkConst(BitVectorExtract(0,0)); + else if (d_unconstrained.find(child) == d_unconstrained.end()) + { + Node extractOp = + nm->mkConst(BitVectorExtract(0, 0)); vector children; - children.push_back(*child_it); + children.push_back(child); Node test = nm->mkNode(extractOp, children); - BitVector one(1,unsigned(1)); + BitVector one(1, unsigned(1)); test = test.eqNode(nm->mkConst(one)); - if (Rewriter::rewrite(test) != nm->mkConst(true)) { + if (Rewriter::rewrite(test) != nm->mkConst(true)) + { done = true; break; } } } - if (done) { + if (done) + { break; } checkParent = true; break; } - // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained + // Uninterpreted function - if domain is infinite, no quantifiers are + // used, and any child is unconstrained, result is unconstrained case kind::APPLY_UF: - if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) { + if (d_logicInfo.isQuantified() + || !current.getType().getCardinality().isInfinite()) + { break; } - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } - if (parent.getType() != current.getType()) { + if (parent.getType() != current.getType()) + { currentSub = newUnconstrainedVar(parent.getType(), currentSub); } current = parent; } - else { + else + { currentSub = Node(); } break; // Array select - if array is unconstrained, so is result case kind::SELECT: - if (parent[0] == current) { + if (parent[0] == current) + { ++d_numUnconstrainedElim; Assert(current.getType().isArray()); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } - currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub); + currentSub = newUnconstrainedVar( + current.getType().getArrayConstituentType(), currentSub); current = parent; } break; - // Array store - if both store and value are unconstrained, so is resulting store + // Array store - if both store and value are unconstrained, so is + // resulting store case kind::STORE: - if (((parent[0] == current && - d_unconstrained.find(parent[2]) != d_unconstrained.end()) || - (parent[2] == current && - d_unconstrained.find(parent[0]) != d_unconstrained.end()))) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (((parent[0] == current + && d_unconstrained.find(parent[2]) != d_unconstrained.end()) + || (parent[2] == current + && d_unconstrained.find(parent[0]) + != d_unconstrained.end()))) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (parent[0] != current) { - if (parent[0].isVar()) { + if (parent[0] != current) + { + if (parent[0].isVar()) + { currentSub = parent[0]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[0])); currentSub = d_substitutions.apply(parent[0]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } @@ -531,24 +651,19 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_SLT: case kind::BITVECTOR_SGE: case kind::BITVECTOR_SGT: - case kind::BITVECTOR_SLE: { + case kind::BITVECTOR_SLE: + { // Tuples over (signed, swap, strict). - switch (parent.getKind()) { - case kind::BITVECTOR_UGE: - break; - case kind::BITVECTOR_ULT: - strict = true; - break; - case kind::BITVECTOR_ULE: - swap = true; - break; + switch (parent.getKind()) + { + case kind::BITVECTOR_UGE: break; + case kind::BITVECTOR_ULT: strict = true; break; + case kind::BITVECTOR_ULE: swap = true; break; case kind::BITVECTOR_UGT: swap = true; strict = true; break; - case kind::BITVECTOR_SGE: - isSigned = true; - break; + case kind::BITVECTOR_SGE: isSigned = true; break; case kind::BITVECTOR_SLT: isSigned = true; strict = true; @@ -562,54 +677,62 @@ void UnconstrainedSimplifier::processUnconstrained() swap = true; strict = true; break; - default: - Unreachable(); + default: Unreachable(); } TNode other; bool left = false; - if (parent[0] == current) { + if (parent[0] == current) + { other = parent[1]; left = true; - } else { + } + else + { Assert(parent[1] == current); other = parent[0]; } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - } else { + } + else + { currentSub = Node(); } - } else { + } + else + { unsigned size = current.getType().getBitVectorSize(); BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0)); - if (swap == left) { + if (swap == left) + { bv = ~bv; } - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - NodeManager* nm = NodeManager::currentNM(); Node test = Rewriter::rewrite(other.eqNode(nm->mkConst(bv))); - if (test == nm->mkConst(false)) { + if (test == nm->mkConst(false)) + { break; } - if (strict) { - currentSub = currentSub.andNode(test.notNode()); - } else { - currentSub = currentSub.orNode(test); - } + currentSub = strict ? currentSub.andNode(test.notNode()) + : currentSub.orNode(test); // Delay adding this substitution - see comment at end of function delayQueueLeft.push_back(current); delayQueueRight.push_back(currentSub); @@ -619,40 +742,46 @@ void UnconstrainedSimplifier::processUnconstrained() break; } - // Do nothing + // Do nothing case kind::BITVECTOR_SIGN_EXTEND: case kind::BITVECTOR_ZERO_EXTEND: case kind::BITVECTOR_REPEAT: case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: - default: - break; + default: break; } - if( checkParent ){ - //run for various cases from above - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (checkParent) + { + // run for various cases from above + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - if (current == parent && d_visited[parent] == 1) { + if (current == parent && d_visited[parent] == 1) + { d_unconstrained.insert(parent); continue; } } - if (!currentSub.isNull()) { + if (!currentSub.isNull()) + { Assert(currentSub.isVar()); d_substitutions.addSubstitution(current, currentSub, false); } - if (workList.empty()) { + if (workList.empty()) + { break; } current = workList.back(); @@ -666,9 +795,11 @@ void UnconstrainedSimplifier::processUnconstrained() // substitution very quickly (never invalidating the substitution cache). // Bitvector comparisons are more complicated and may require // back-substitution and cache-invalidation. So we do these last. - while (!delayQueueLeft.empty()) { + while (!delayQueueLeft.empty()) + { left = delayQueueLeft.back(); - if (!d_substitutions.hasSubstitution(left)) { + if (!d_substitutions.hasSubstitution(left)) + { right = d_substitutions.apply(delayQueueRight.back()); d_substitutions.addSubstitution(delayQueueLeft.back(), right); } @@ -677,21 +808,27 @@ void UnconstrainedSimplifier::processUnconstrained() } } - -void UnconstrainedSimplifier::processAssertions(vector& assertions) +PreprocessingPassResult UnconstrainedSimplifier::applyInternal( + AssertionPipeline* assertionsToPreprocess) { + d_preprocContext->spendResource(options::preprocessStep()); + + std::vector& assertions = assertionsToPreprocess->ref(); + d_context->push(); - vector::iterator it = assertions.begin(), iend = assertions.end(); - for (; it != iend; ++it) { - visitAll(*it); + for (const Node& assertion : assertions) + { + visitAll(assertion); } - if (!d_unconstrained.empty()) { + if (!d_unconstrained.empty()) + { processUnconstrained(); // d_substitutions.print(Message.getStream()); - for (it = assertions.begin(); it != iend; ++it) { - (*it) = Rewriter::rewrite(d_substitutions.apply(*it)); + for (Node& assertion : assertions) + { + assertion = Rewriter::rewrite(d_substitutions.apply(assertion)); } } @@ -701,4 +838,10 @@ void UnconstrainedSimplifier::processAssertions(vector& assertions) d_visited.clear(); d_visitedOnce.clear(); d_unconstrained.clear(); + + return PreprocessingPassResult::NO_CONFLICT; } + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/theory/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h similarity index 56% rename from src/theory/unconstrained_simplifier.h rename to src/preprocessing/passes/unconstrained_simplifier.h index b13311e2a..658834ee3 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -11,37 +11,48 @@ ** ** \brief Simplifications based on unconstrained variables ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. **/ #include "cvc4_private.h" -#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H +#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #include #include -#include #include +#include "context/context.h" #include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/statistics_registry.h" namespace CVC4 { +namespace preprocessing { +namespace passes { -/* Forward Declarations */ -class LogicInfo; +class UnconstrainedSimplifier : public PreprocessingPass +{ + public: + UnconstrainedSimplifier(PreprocessingPassContext* preprocContext); + ~UnconstrainedSimplifier() override; -class UnconstrainedSimplifier { + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + private: /** number of expressions eliminated due to unconstrained simplification */ IntStat d_numUnconstrainedElim; - typedef std::unordered_map TNodeCountMap; - typedef std::unordered_map TNodeMap; - typedef std::unordered_set TNodeSet; + using TNodeCountMap = std::unordered_map; + using TNodeMap = std::unordered_map; + using TNodeSet = std::unordered_set; TNodeCountMap d_visited; TNodeMap d_visitedOnce; @@ -55,13 +66,10 @@ class UnconstrainedSimplifier { void visitAll(TNode assertion); Node newUnconstrainedVar(TypeNode t, TNode var); void processUnconstrained(); - -public: - UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo); - ~UnconstrainedSimplifier(); - void processAssertions(std::vector& assertions); }; -} +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 #endif diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 97fa32d17..4143f2d4b 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -39,6 +39,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine_scope.h" #include "smt/term_formula_removal.h" +#include "theory/logic_info.h" #include "theory/substitutions.h" namespace CVC4 { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a289752fa..96e554680 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -43,6 +43,7 @@ class PreprocessingPassContext DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + context::Context* getDecisionContext() { return d_smt->d_context; } RemoveTermFormulas* getIteRemover() { return d_iteRemover; } void spendResource(unsigned amount) @@ -50,6 +51,8 @@ class PreprocessingPassContext d_resourceManager->spendResource(amount); } + const LogicInfo& getLogicInfo() { return d_smt->d_logic; } + /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0497c2814..02e9892e2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -97,6 +97,7 @@ #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" +#include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -204,8 +205,6 @@ struct SmtEngineStatistics { IntStat d_numMiplibAssertionsRemoved; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent in simplifying ITEs */ - TimerStat d_unconstrainedSimpTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; /** time spent converting to CNF */ @@ -238,7 +237,6 @@ struct SmtEngineStatistics { d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), @@ -257,7 +255,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); @@ -278,7 +275,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); @@ -580,9 +576,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify based on unconstrained values - void unconstrainedSimp(); - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. @@ -2676,6 +2669,8 @@ void SmtEnginePrivate::finishInit() new SynthRewRulesPass(d_preprocessingPassContext.get())); std::unique_ptr sepSkolemEmp( new SepSkolemEmp(d_preprocessingPassContext.get())); + std::unique_ptr unconstrainedSimplifier( + new UnconstrainedSimplifier(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("apply-substs", std::move(applySubsts)); d_preprocessingPassRegistry.registerPass("apply-to-const", @@ -2720,6 +2715,8 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); d_preprocessingPassRegistry.registerPass("quantifier-macros", std::move(quantifierMacros)); + d_preprocessingPassRegistry.registerPass("unconstrained-simplifier", + std::move(unconstrainedSimplifier)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -3255,13 +3252,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::unconstrainedSimp() { - TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); - spendResource(options::preprocessStep()); - Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; - d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); -} - void SmtEnginePrivate::traceBackToAssertions(const std::vector& nodes, std::vector& assertions) { const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); for(vector::const_iterator i = nodes.begin(); i != nodes.end(); ++i) { @@ -3745,14 +3735,10 @@ bool SmtEnginePrivate::simplifyAssertions() // Unconstrained simplification if(options::unconstrainedSimp()) { - Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } - dumpAssertions("post-unconstrained", d_assertions); - Trace("smt") << "POST unconstrainedSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -4027,12 +4013,9 @@ void SmtEnginePrivate::processAssertions() { // Unconstrained simplification if(options::unconstrainedSimp()) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; - dumpAssertions("pre-unconstrained-simp", d_assertions); d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); - unconstrainedSimp(); - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; - dumpAssertions("post-unconstrained-simp", d_assertions); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } if(options::bvIntroducePow2()) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c87a4be02..d75f7843d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,7 +49,6 @@ #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -#include "theory/unconstrained_simplifier.h" #include "util/resource_manager.h" using namespace std; @@ -315,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) @@ -360,9 +358,6 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); - - delete d_unconstrainedSimp; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2146,11 +2141,6 @@ void TheoryEngine::getExplanation(std::vector& explanationVector }); } -void TheoryEngine::ppUnconstrainedSimp(vector& assertions) -{ - d_unconstrainedSimp->processAssertions(assertions); -} - void TheoryEngine::setUserAttribute(const std::string& attr, Node n, const std::vector& node_values, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 71a0234ed..65402f0a6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -99,7 +99,6 @@ namespace theory { class DecisionEngine; class RemoveTermFormulas; -class UnconstrainedSimplifier; /** * This is essentially an abstraction for a collection of theories. A @@ -827,9 +826,6 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass simplifying unconstrained expressions */ - UnconstrainedSimplifier* d_unconstrainedSimp; - /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: void staticInitializeBVOptions(const std::vector& assertions); @@ -838,8 +834,6 @@ public: /** Returns false if an assertion simplified to false. */ bool donePPSimpITE(std::vector& assertions); - void ppUnconstrainedSimp(std::vector& assertions); - SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } -- 2.30.2