From dd0ca308c3299155bfab89ade6cfd0a70b9abda5 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 5 Jun 2012 14:43:11 +0000 Subject: Adding missing files... --- src/theory/unconstrained_simplifier.cpp | 665 ++++++++++++++++++++++++++++++++ src/theory/unconstrained_simplifier.h | 65 ++++ 2 files changed, 730 insertions(+) create mode 100644 src/theory/unconstrained_simplifier.cpp create mode 100644 src/theory/unconstrained_simplifier.h (limited to 'src') diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp new file mode 100644 index 000000000..b1a944597 --- /dev/null +++ b/src/theory/unconstrained_simplifier.cpp @@ -0,0 +1,665 @@ +/********************* */ +/*! \file unconstrained_simplifier.cpp + ** \verbatim + ** Original author: barrett + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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" + +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) +{ + StatisticsRegistry::registerStat(&d_numUnconstrainedElim); +} + + +UnconstrainedSimplifier::~UnconstrainedSimplifier() +{ + StatisticsRegistry::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 + unc_preprocess_stack_element& stackHead = toVisit.back(); + toVisit.pop_back(); + TNode current = stackHead.node; + + 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] = stackHead.parent; + + if (current.getNumChildren() == 0) { + if (current.isVar()) { + 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()->mkVar(t); + Dump.declareVar(n.toExpr(), "a new var introduced because of unconstrained variable " + var.toString()); + return n; +} + + +void UnconstrainedSimplifier::removeExpr(TNode expr) +{ + ++d_numUnconstrainedElim; + // TNodeCountMap::iterator find = d_visited.find(expr); + // Assert(find != d_visited.end()); + // find->second = find->second - 1; + // if (find->second == 0) { + // 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)); + // !!! + // } +} + + +void UnconstrainedSimplifier::processUnconstrained() +{ + TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end(); + vector workList; + for ( ; it != iend; ++it) { + workList.push_back(*it); + } + TNode current = workList.back(); + Node currentSub; + workList.pop_back(); + + for (;;) { + TNodeMap::iterator itNodeMap; + Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); + TNode parent = d_visitedOnce[current]; + bool swap = false; + bool isSigned = false; + bool strict = false; + if (!parent.isNull()) { + 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)) { + removeExpr(parent); + if (uThen) { + if (parent[1] != current || currentSub.isNull()) { + currentSub = parent[1]; + } + } + else if (parent[2] != current || currentSub.isNull()) { + currentSub = parent[2]; + } + current = parent; + } + else { + currentSub = Node(); + } + } + else if (uCond && parent.getType().getCardinality().isFinite() && parent.getType().getCardinality().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; + if (parent.getType().isBoolean()) { + test = Rewriter::rewrite(parent[1].iffNode(parent[2])); + } + else { + test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + } + if (test == NodeManager::currentNM()->mkConst(false)) { + removeExpr(parent); + 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; + } + } + 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)) { + removeExpr(parent); + 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: + removeExpr(parent); + 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: + removeExpr(parent); + 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) { + if (d_unconstrained.find(parent) == d_unconstrained.end() && + !d_substitutions.hasSubstitution(parent)) { + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + else { + currentSub = Node(); + } + } + } + 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: + case kind::BITVECTOR_UREM: + 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) { + if (d_unconstrained.find(parent) == d_unconstrained.end() && + !d_substitutions.hasSubstitution(parent)) { + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + else { + currentSub = Node(); + } + } + 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)) { + removeExpr(parent); + 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::IFF: + case kind::XOR: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_XNOR: + case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_SUB: + if (d_unconstrained.find(parent) == d_unconstrained.end() && + !d_substitutions.hasSubstitution(parent)) { + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + else { + currentSub = Node(); + } + 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; + } + } + removeExpr(parent); + 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; + } + } + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + break; + } + + // Bitvector MULT - other term must be odd + case kind::BITVECTOR_MULT: { + 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)) { + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + else { + currentSub = Node(); + } + } + else { + NodeManager* nm = NodeManager::currentNM(); + Node extractOp = nm->mkConst(BitVectorExtract(0,0)); + vector children; + children.push_back(other); + Node test = nm->mkNode(extractOp, children); + BitVector one(1,unsigned(1)); + test = test.eqNode(nm->mkConst(one)); + if (Rewriter::rewrite(test) != nm->mkConst(true)) { + break; + } + removeExpr(parent); + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + 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)) { + removeExpr(parent); + 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) { + removeExpr(parent); + 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 uncosntrained, 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)) { + removeExpr(parent); + if (parent[0] != current || currentSub.isNull()) { + currentSub = parent[0]; + } + 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: + strict = true; + case kind::BITVECTOR_UGE: + goto bvineq; + + case kind::BITVECTOR_UGT: + strict = true; + case kind::BITVECTOR_ULE: + swap = true; + goto bvineq; + + case kind::BITVECTOR_SLT: + strict = true; + case kind::BITVECTOR_SGE: + isSigned = true; + goto bvineq; + + case kind::BITVECTOR_SGT: + strict = true; + case kind::BITVECTOR_SLE: + isSigned = true; + swap = true; + + bvineq: { + 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)) { + removeExpr(parent); + 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); + } + parent = TNode(); + } + break; + } + + // These should have been rewritten up front + case kind::BITVECTOR_REPEAT: + case kind::BITVECTOR_ZERO_EXTEND: + case kind::BITVECTOR_ROTATE_LEFT: + case kind::BITVECTOR_ROTATE_RIGHT: + Unreachable(); + break; + + // Do nothing + case kind::BITVECTOR_SIGN_EXTEND: + default: + break; + } + if (current == parent && d_visited[parent] == 1) { + d_unconstrained.insert(parent); + continue; + } + } + if (!currentSub.isNull()) { + d_substitutions.addSubstitution(current, currentSub); + } + if (workList.empty()) { + break; + } + current = workList.back(); + currentSub = Node(); + workList.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(std::cout); + for (it = assertions.begin(); it != iend; ++it) { + (*it) = 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 new file mode 100644 index 000000000..5ce3f672d --- /dev/null +++ b/src/theory/unconstrained_simplifier.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file unconstrained_simplifier.h + ** \verbatim + ** Original author: barrett + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "expr/node.h" +#include "theory/theory.h" +#include "theory/substitutions.h" + +namespace CVC4 { + +class UnconstrainedSimplifier { + + /** number of expressions eliminated due to unconstrained simplification */ + IntStat d_numUnconstrainedElim; + + typedef std::hash_map TNodeCountMap; + typedef std::hash_map TNodeMap; + typedef std::hash_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(); + void removeExpr(TNode node); + +public: + UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo); + ~UnconstrainedSimplifier(); + void processAssertions(std::vector& assertions); +}; + +} + +#endif -- cgit v1.2.3