Adding missing files...

1 files changed, 665 insertions, 0 deletions

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<unc_preprocess_stack_element> 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<TNode> 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<bool>(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<Rational>(1));
+              if (other == nm->mkConst<Rational>(-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<Rational>(0));
+              if (Rewriter::rewrite(test) != nm->mkConst<bool>(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>(BitVectorExtract(0,0));
+            vector<Node> children;
+            children.push_back(other);
+            Node test = nm->mkNode(extractOp, children);
+            BitVector one(1,unsigned(1));
+            test = test.eqNode(nm->mkConst<BitVector>(one));
+            if (Rewriter::rewrite(test) != nm->mkConst<bool>(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<BitVector>(bv)));
+            if (test == nm->mkConst<bool>(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<Node>& assertions)
+{
+  d_context->push();
+
+  vector<Node>::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();
+}