From: Andres Noetzli Date: Sun, 26 Aug 2018 04:09:22 +0000 (-0700) Subject: Refactor unconstrained simplification pass (#2374) X-Git-Tag: cvc5-1.0.0~4720 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b70ccff4de0a23bdf11c70002d10a2cc0795a91c;p=cvc5.git Refactor unconstrained simplification pass (#2374) --- 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/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp new file mode 100644 index 000000000..6bb46f3f2 --- /dev/null +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -0,0 +1,847 @@ +/********************* */ +/*! \file unconstrained_simplifier.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Tim King, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \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. + **/ + +#include "preprocessing/passes/unconstrained_simplifier.h" + +#include "smt/smt_statistics_registry.h" +#include "theory/logic_info.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +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 +{ + 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 */ + +void UnconstrainedSimplifier::visitAll(TNode assertion) +{ + // Do a topological sort of the subexpressions and substitute them + vector toVisit; + toVisit.push_back(assertion); + + while (!toVisit.empty()) + { + // The current node we are processing + TNode current = toVisit.back().node; + TNode parent = toVisit.back().parent; + toVisit.pop_back(); + + TNodeCountMap::iterator find = d_visited.find(current); + if (find != d_visited.end()) + { + if (find->second == 1) + { + d_visitedOnce.erase(current); + if (current.isVar()) + { + d_unconstrained.erase(current); + } + } + ++find->second; + continue; + } + + d_visited[current] = 1; + d_visitedOnce[current] = parent; + + if (current.getNumChildren() == 0) + { + if (current.getKind() == kind::VARIABLE + || current.getKind() == kind::SKOLEM) + { + d_unconstrained.insert(current); + } + } + else + { + for (TNode childNode : current) + { + toVisit.push_back(unc_preprocess_stack_element(childNode, current)); + } + } + } +} + +Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) +{ + Node n = NodeManager::currentNM()->mkSkolem( + "unconstrained", + t, + "a new var introduced because of unconstrained variable " + + var.toString()); + return n; +} + +void UnconstrainedSimplifier::processUnconstrained() +{ + NodeManager* nm = NodeManager::currentNM(); + + vector workList(d_unconstrained.begin(), d_unconstrained.end()); + Node currentSub; + TNode parent; + bool swap; + bool isSigned; + bool strict; + vector delayQueueLeft; + vector delayQueueRight; + + TNode current = workList.back(); + workList.pop_back(); + for (;;) + { + Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); + parent = d_visitedOnce[current]; + 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)) + { + ++d_numUnconstrainedElim; + if (uThen) + { + if (parent[1] != current) + { + if (parent[1].isVar()) + { + currentSub = parent[1]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[1])); + currentSub = d_substitutions.apply(parent[1]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + } + else if (parent[2] != current) + { + if (parent[2].isVar()) + { + currentSub = parent[2]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[2])); + currentSub = d_substitutions.apply(parent[2]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + 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 + Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + if (test == nm->mkConst(false)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + } + } + break; + } + + // 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()) + { + TNode other = (parent[0] == current) ? parent[1] : parent[0]; + if (current.getType().isSubtypeOf(other.getType())) + { + break; + } + } + 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 + break; + } + } + if (parent[0].getType().isBoolean()) + { + checkParent = true; + break; + } + case kind::BITVECTOR_COMP: + case kind::LT: + case kind::LEQ: + case kind::GT: + case kind::GEQ: + { + 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()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + break; + } + + // Unary operators that propagate unconstrainedness + case kind::NOT: + case kind::BITVECTOR_NOT: + case kind::BITVECTOR_NEG: + case kind::UMINUS: + ++d_numUnconstrainedElim; + Assert(parent[0] == current); + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + break; + + // Unary operators that propagate unconstrainedness and return a + // different type + case kind::BITVECTOR_EXTRACT: + ++d_numUnconstrainedElim; + Assert(parent[0] == current); + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + break; + + // Operators returning same type requiring all children to be + // unconstrained + case kind::AND: + case kind::OR: + case kind::IMPLIES: + case kind::BITVECTOR_AND: + case kind::BITVECTOR_OR: + case kind::BITVECTOR_NAND: + case kind::BITVECTOR_NOR: + { + bool allUnconstrained = true; + for (TNode child : parent) + { + if (d_unconstrained.find(child) == d_unconstrained.end()) + { + allUnconstrained = false; + break; + } + } + if (allUnconstrained) + { + checkParent = true; + } + } + break; + + // Require all children to be unconstrained and different + case kind::BITVECTOR_SHL: + case kind::BITVECTOR_LSHR: + case kind::BITVECTOR_ASHR: + case kind::BITVECTOR_UDIV_TOTAL: + case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_SDIV: + case kind::BITVECTOR_SREM: + 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()) + { + allUnconstrained = false; + break; + } + 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) + { + checkParent = true; + } + break; + } + + // 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()) + { + allUnconstrained = false; + break; + } + 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)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + } + } + break; + + // 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()) + { + break; + } + case kind::XOR: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_XNOR: + case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_SUB: checkParent = true; break; + + // 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) + { + other = parent[1]; + } + 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) + { + break; + } + } + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + 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]) + { + break; + } + // 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)); + // div by -1 should have been simplified + if (other != nm->mkConst(-1)) + { + break; + } + else + { + Assert(parent.getKind() == kind::MULT); + Assert(parent.getType().isInteger()); + } + } + else + { + // TODO(#2377): could build ITE here + Node test = other.eqNode(nm->mkConst(0)); + if (Rewriter::rewrite(test) != nm->mkConst(false)) + { + break; + } + } + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + break; + } + + // Bitvector MULT - current must only appear once in the children: + // all other children must be unconstrained or odd + case kind::BITVECTOR_MULT: + { + bool found = false; + bool done = false; + + for (TNode child : parent) + { + if (child == current) + { + if (found) + { + done = true; + break; + } + found = true; + continue; + } + else if (d_unconstrained.find(child) == d_unconstrained.end()) + { + Node extractOp = + nm->mkConst(BitVectorExtract(0, 0)); + vector children; + children.push_back(child); + Node test = nm->mkNode(extractOp, children); + BitVector one(1, unsigned(1)); + test = test.eqNode(nm->mkConst(one)); + if (Rewriter::rewrite(test) != nm->mkConst(true)) + { + done = true; + break; + } + } + } + if (done) + { + break; + } + checkParent = true; + break; + } + + // 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()) + { + break; + } + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + if (parent.getType() != current.getType()) + { + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + } + current = parent; + } + else + { + currentSub = Node(); + } + break; + + // Array select - if array is unconstrained, so is result + case kind::SELECT: + if (parent[0] == current) + { + ++d_numUnconstrainedElim; + Assert(current.getType().isArray()); + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar( + current.getType().getArrayConstituentType(), currentSub); + current = parent; + } + break; + + // 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)) + { + ++d_numUnconstrainedElim; + if (parent[0] != current) + { + if (parent[0].isVar()) + { + currentSub = parent[0]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[0])); + currentSub = d_substitutions.apply(parent[0]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + break; + + // Bit-vector comparisons: replace with new Boolean variable, but have + // to also conjoin with a side condition as there is always one case + // when the comparison is forced to be false + case kind::BITVECTOR_ULT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_SLT: + case kind::BITVECTOR_SGE: + case kind::BITVECTOR_SGT: + 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; + case kind::BITVECTOR_UGT: + swap = true; + strict = true; + break; + case kind::BITVECTOR_SGE: isSigned = true; break; + case kind::BITVECTOR_SLT: + isSigned = true; + strict = true; + break; + case kind::BITVECTOR_SLE: + isSigned = true; + swap = true; + break; + case kind::BITVECTOR_SGT: + isSigned = true; + swap = true; + strict = true; + break; + default: Unreachable(); + } + TNode other; + bool left = false; + if (parent[0] == current) + { + other = parent[1]; + left = true; + } + 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)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + } + else + { + unsigned size = current.getType().getBitVectorSize(); + BitVector bv = + isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) + : BitVector(size, unsigned(0)); + if (swap == left) + { + bv = ~bv; + } + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + Node test = + Rewriter::rewrite(other.eqNode(nm->mkConst(bv))); + if (test == nm->mkConst(false)) + { + break; + } + 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); + currentSub = Node(); + parent = TNode(); + } + break; + } + + // 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; + } + 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()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + if (current == parent && d_visited[parent] == 1) + { + d_unconstrained.insert(parent); + continue; + } + } + if (!currentSub.isNull()) + { + Assert(currentSub.isVar()); + d_substitutions.addSubstitution(current, currentSub, false); + } + if (workList.empty()) + { + break; + } + current = workList.back(); + currentSub = Node(); + workList.pop_back(); + } + TNode left; + Node right; + // All substitutions except those arising from bitvector comparisons are + // substitutions t -> x where x is a variable. This allows us to build the + // 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()) + { + left = delayQueueLeft.back(); + if (!d_substitutions.hasSubstitution(left)) + { + right = d_substitutions.apply(delayQueueRight.back()); + d_substitutions.addSubstitution(delayQueueLeft.back(), right); + } + delayQueueLeft.pop_back(); + delayQueueRight.pop_back(); + } +} + +PreprocessingPassResult UnconstrainedSimplifier::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + d_preprocContext->spendResource(options::preprocessStep()); + + std::vector& assertions = assertionsToPreprocess->ref(); + + d_context->push(); + + for (const Node& assertion : assertions) + { + visitAll(assertion); + } + + if (!d_unconstrained.empty()) + { + processUnconstrained(); + // d_substitutions.print(Message.getStream()); + for (Node& assertion : assertions) + { + assertion = Rewriter::rewrite(d_substitutions.apply(assertion)); + } + } + + // to clear substitutions map + d_context->pop(); + + d_visited.clear(); + d_visitedOnce.clear(); + d_unconstrained.clear(); + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h new file mode 100644 index 000000000..658834ee3 --- /dev/null +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file unconstrained_simplifier.h + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H + +#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 { + +class UnconstrainedSimplifier : public PreprocessingPass +{ + public: + UnconstrainedSimplifier(PreprocessingPassContext* preprocContext); + ~UnconstrainedSimplifier() override; + + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /** number of expressions eliminated due to unconstrained simplification */ + IntStat d_numUnconstrainedElim; + + using TNodeCountMap = std::unordered_map; + using TNodeMap = std::unordered_map; + using TNodeSet = std::unordered_set; + + TNodeCountMap d_visited; + TNodeMap d_visitedOnce; + TNodeSet d_unconstrained; + + context::Context* d_context; + theory::SubstitutionMap d_substitutions; + + const LogicInfo& d_logicInfo; + + void visitAll(TNode assertion); + Node newUnconstrainedVar(TypeNode t, TNode var); + void processUnconstrained(); +}; + +} // 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; } diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp deleted file mode 100644 index 41529760b..000000000 --- a/src/theory/unconstrained_simplifier.cpp +++ /dev/null @@ -1,704 +0,0 @@ -/********************* */ -/*! \file unconstrained_simplifier.cpp - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Tim King, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \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. - **/ - - -#include "theory/unconstrained_simplifier.h" - -#include "theory/rewriter.h" -#include "theory/logic_info.h" -#include "smt/smt_statistics_registry.h" - -using namespace std; -using namespace CVC4; -using namespace 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) -{ - smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); -} - - -UnconstrainedSimplifier::~UnconstrainedSimplifier() -{ - smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); -} - - -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 */ - - -void UnconstrainedSimplifier::visitAll(TNode assertion) -{ - // Do a topological sort of the subexpressions and substitute them - vector toVisit; - toVisit.push_back(assertion); - - while (!toVisit.empty()) - { - // The current node we are processing - TNode current = toVisit.back().node; - TNode parent = toVisit.back().parent; - toVisit.pop_back(); - - TNodeCountMap::iterator find = d_visited.find(current); - if (find != d_visited.end()) { - if (find->second == 1) { - d_visitedOnce.erase(current); - if (current.isVar()) { - d_unconstrained.erase(current); - } - } - ++find->second; - continue; - } - - d_visited[current] = 1; - d_visitedOnce[current] = parent; - - 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; - toVisit.push_back(unc_preprocess_stack_element(childNode, current)); - } - } - } -} - -Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) -{ - 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); - } - Node currentSub; - TNode parent; - bool swap; - bool isSigned; - bool strict; - vector delayQueueLeft; - vector delayQueueRight; - - TNode current = workList.back(); - workList.pop_back(); - for (;;) { - Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); - parent = d_visitedOnce[current]; - 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)) { - ++d_numUnconstrainedElim; - if (uThen) { - if (parent[1] != current) { - if (parent[1].isVar()) { - currentSub = parent[1]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[1])); - currentSub = d_substitutions.apply(parent[1]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - } - else if (parent[2] != current) { - if (parent[2].isVar()) { - currentSub = parent[2]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[2])); - currentSub = d_substitutions.apply(parent[2]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - 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 - Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - if (test == NodeManager::currentNM()->mkConst(false)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - } - } - break; - } - - // 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()) { - TNode other = (parent[0] == current) ? parent[1] : parent[0]; - if (current.getType().isSubtypeOf(other.getType())) { - break; - } - } - 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 - break; - } - } - if( parent[0].getType().isBoolean() ){ - checkParent = true; - break; - } - case kind::BITVECTOR_COMP: - case kind::LT: - case kind::LEQ: - case kind::GT: - case kind::GEQ: - { - 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()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - else { - currentSub = Node(); - } - break; - } - - // Unary operators that propagate unconstrainedness - case kind::NOT: - case kind::BITVECTOR_NOT: - case kind::BITVECTOR_NEG: - case kind::UMINUS: - ++d_numUnconstrainedElim; - Assert(parent[0] == current); - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - break; - - // Unary operators that propagate unconstrainedness and return a different type - case kind::BITVECTOR_EXTRACT: - ++d_numUnconstrainedElim; - Assert(parent[0] == current); - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - break; - - // Operators returning same type requiring all children to be unconstrained - case kind::AND: - case kind::OR: - case kind::IMPLIES: - case kind::BITVECTOR_AND: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_NAND: - 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()) { - allUnconstrained = false; - break; - } - } - if (allUnconstrained) { - checkParent = true; - } - } - break; - - // Require all children to be unconstrained and different - case kind::BITVECTOR_SHL: - case kind::BITVECTOR_LSHR: - case kind::BITVECTOR_ASHR: - case kind::BITVECTOR_UDIV_TOTAL: - case kind::BITVECTOR_UREM_TOTAL: - case kind::BITVECTOR_SDIV: - case kind::BITVECTOR_SREM: - 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()) { - allUnconstrained = false; - break; - } - 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) { - checkParent = true; - } - break; - } - - // 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()) { - allUnconstrained = false; - break; - } - 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)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - else { - currentSub = Node(); - } - } - } - break; - - // 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()) { - break; - } - case kind::XOR: - case kind::BITVECTOR_XOR: - case kind::BITVECTOR_XNOR: - case kind::BITVECTOR_PLUS: - case kind::BITVECTOR_SUB: - checkParent = true; - break; - - // 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) { - other = parent[1]; - } - 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) { - break; - } - } - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - 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]) { - 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()) { - // 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 - Assert(parent.getKind() == kind::MULT); - Assert(parent.getType().isInteger()); - } - else { - break; - } - } - else { - // TODO: could build ITE here - Node test = other.eqNode(nm->mkConst(0)); - if (Rewriter::rewrite(test) != nm->mkConst(false)) { - break; - } - } - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - break; - } - - // Bitvector MULT - current must only appear once in the children: - // all other children must be unconstrained or odd - case kind::BITVECTOR_MULT: - { - 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) { - 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)); - vector children; - children.push_back(*child_it); - Node test = nm->mkNode(extractOp, children); - BitVector one(1,unsigned(1)); - test = test.eqNode(nm->mkConst(one)); - if (Rewriter::rewrite(test) != nm->mkConst(true)) { - done = true; - break; - } - } - } - if (done) { - break; - } - checkParent = true; - break; - } - - // 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()) { - break; - } - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - if (parent.getType() != current.getType()) { - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - } - current = parent; - } - else { - currentSub = Node(); - } - break; - - // Array select - if array is unconstrained, so is result - case kind::SELECT: - if (parent[0] == current) { - ++d_numUnconstrainedElim; - Assert(current.getType().isArray()); - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub); - current = parent; - } - break; - - // 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)) { - ++d_numUnconstrainedElim; - if (parent[0] != current) { - if (parent[0].isVar()) { - currentSub = parent[0]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[0])); - currentSub = d_substitutions.apply(parent[0]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - break; - - // Bit-vector comparisons: replace with new Boolean variable, but have - // to also conjoin with a side condition as there is always one case - // when the comparison is forced to be false - case kind::BITVECTOR_ULT: - case kind::BITVECTOR_UGE: - case kind::BITVECTOR_UGT: - case kind::BITVECTOR_ULE: - case kind::BITVECTOR_SLT: - case kind::BITVECTOR_SGE: - case kind::BITVECTOR_SGT: - 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; - case kind::BITVECTOR_UGT: - swap = true; - strict = true; - break; - case kind::BITVECTOR_SGE: - isSigned = true; - break; - case kind::BITVECTOR_SLT: - isSigned = true; - strict = true; - break; - case kind::BITVECTOR_SLE: - isSigned = true; - swap = true; - break; - case kind::BITVECTOR_SGT: - isSigned = true; - swap = true; - strict = true; - break; - default: - Unreachable(); - } - TNode other; - bool left = false; - if (parent[0] == current) { - other = parent[1]; - left = true; - } 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)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } else { - currentSub = Node(); - } - } else { - unsigned size = current.getType().getBitVectorSize(); - BitVector bv = - isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) - : BitVector(size, unsigned(0)); - if (swap == left) { - bv = ~bv; - } - 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)) { - break; - } - if (strict) { - currentSub = currentSub.andNode(test.notNode()); - } else { - currentSub = currentSub.orNode(test); - } - // Delay adding this substitution - see comment at end of function - delayQueueLeft.push_back(current); - delayQueueRight.push_back(currentSub); - currentSub = Node(); - parent = TNode(); - } - break; - } - - // 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; - } - 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()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - if (current == parent && d_visited[parent] == 1) { - d_unconstrained.insert(parent); - continue; - } - } - if (!currentSub.isNull()) { - Assert(currentSub.isVar()); - d_substitutions.addSubstitution(current, currentSub, false); - } - if (workList.empty()) { - break; - } - current = workList.back(); - currentSub = Node(); - workList.pop_back(); - } - TNode left; - Node right; - // All substitutions except those arising from bitvector comparisons are - // substitutions t -> x where x is a variable. This allows us to build the - // 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()) { - left = delayQueueLeft.back(); - if (!d_substitutions.hasSubstitution(left)) { - right = d_substitutions.apply(delayQueueRight.back()); - d_substitutions.addSubstitution(delayQueueLeft.back(), right); - } - delayQueueLeft.pop_back(); - delayQueueRight.pop_back(); - } -} - - -void UnconstrainedSimplifier::processAssertions(vector& assertions) -{ - d_context->push(); - - vector::iterator it = assertions.begin(), iend = assertions.end(); - for (; it != iend; ++it) { - visitAll(*it); - } - - if (!d_unconstrained.empty()) { - processUnconstrained(); - // d_substitutions.print(Message.getStream()); - for (it = assertions.begin(); it != iend; ++it) { - (*it) = Rewriter::rewrite(d_substitutions.apply(*it)); - } - } - - // to clear substitutions map - d_context->pop(); - - d_visited.clear(); - d_visitedOnce.clear(); - d_unconstrained.clear(); -} diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h deleted file mode 100644 index b13311e2a..000000000 --- a/src/theory/unconstrained_simplifier.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file unconstrained_simplifier.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \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. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H - -#include -#include -#include -#include - -#include "expr/node.h" -#include "theory/substitutions.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -/* Forward Declarations */ -class LogicInfo; - -class UnconstrainedSimplifier { - - /** 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; - - TNodeCountMap d_visited; - TNodeMap d_visitedOnce; - TNodeSet d_unconstrained; - - context::Context* d_context; - theory::SubstitutionMap d_substitutions; - - const LogicInfo& d_logicInfo; - - 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); -}; - -} - -#endif