Merge branch 'master' of https://github.com/CVC4/CVC4

15 files changed, 217 insertions, 92 deletions

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 80736caa5..9e814b358 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -290,7 +290,7 @@ simpleTerm[CVC4::Expr& expr]
   : variable[expr]
   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
   | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(
-        MK_CONST(AntlrInput::tokenText($DISTINCT_OBJECT))); }
+        AntlrInput::tokenText($DISTINCT_OBJECT)); }
 ;
 
 functionTerm[CVC4::Expr& expr]
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index adaca892f..6b7adbbf7 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -21,6 +21,7 @@
 
 #include "parser/parser.h"
 #include "expr/command.h"
+#include "util/hash.h"
 #include <ext/hash_set>
 #include <cassert>
 
@@ -42,7 +43,7 @@ class Tptp : public Parser {
   Expr d_uts_op;
   // The set of expression that already have a bridge
   std::hash_set<Expr, ExprHashFunction> d_r_converted;
-  std::hash_set<Expr, ExprHashFunction> d_s_converted;
+  std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
 
   //TPTP directory where to find includes
   // empty if none could be determined
@@ -87,32 +88,12 @@ public:
     return ret;
   }
 
-  inline Expr convertStrToUnsorted(Expr expr){
-    ExprManager * em = getExprManager();
-
-    // Create the conversion function If they doesn't exists
-    if(d_stu_op.isNull()){
-      Type t;
-      //Conversion from string to unsorted
-      t = em->mkFunctionType(em->stringType(), d_unsorted);
-      d_stu_op = em->mkVar("$$stu",t);
-      preemptCommand(new DeclareFunctionCommand("$$stu", d_stu_op, t));
-      //Conversion from unsorted to string
-      t = em->mkFunctionType(d_unsorted, em->stringType());
-      d_uts_op = em->mkVar("$$uts",t);
-      preemptCommand(new DeclareFunctionCommand("$$uts", d_uts_op, t));
+  inline Expr convertStrToUnsorted(std::string str) {
+    Expr& e = d_distinct_objects[str];
+    if(e.isNull()) {
+      e = getExprManager()->mkConst(UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1));
     }
-    // Add the inverse in order to show that over the elements that
-    // appear in the problem there is a bijection between unsorted and
-    // rational
-    Expr ret = em->mkExpr(kind::APPLY_UF,d_stu_op,expr);
-    if ( d_s_converted.find(expr) == d_s_converted.end() ){
-      d_s_converted.insert(expr);
-      Expr eq = em->mkExpr(kind::EQUAL,expr,
-                           em->mkExpr(kind::APPLY_UF,d_uts_op,ret));
-      preemptCommand(new AssertCommand(eq));
-    };
-    return ret;
+    return e;
   }
 
 public:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 35db0975e..0d9d63d91 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -749,8 +749,8 @@ SmtEngine::~SmtEngine() throw() {
 
     // global push/pop around everything, to ensure proper destruction
     // of context-dependent data structures
-    d_context->pop();
-    d_userContext->pop();
+    d_context->popto(0);
+    d_userContext->popto(0);
 
     if(d_assignments != NULL) {
       d_assignments->deleteSelf();
@@ -771,18 +771,18 @@ SmtEngine::~SmtEngine() throw() {
 
     d_definedFunctions->deleteSelf();
 
-    delete d_stats;
-
-    delete d_private;
 
     delete d_theoryEngine;
     delete d_propEngine;
     delete d_decisionEngine;
 
-    delete d_userContext;
-
+    delete d_stats;
     delete d_statisticsRegistry;
 
+    delete d_private;
+
+    delete d_userContext;
+
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 53cdd3fdc..801893107 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -87,6 +87,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_decisionRequests(c),
   d_permRef(c),
   d_modelConstraints(c),
+  d_lemmasSaved(c),
   d_inCheckModel(false)
 {
   StatisticsRegistry::registerStat(&d_numRow);
@@ -1294,6 +1295,10 @@ void TheoryArrays::checkModel(Effort e)
   while (!d_lemmas.empty()) {
     Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl;
     d_out->lemma(d_lemmas.back());
+#ifdef CVC4_ASSERTIONS
+    Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end());
+    d_lemmasSaved.insert(d_lemmas.back());
+#endif
     d_lemmas.pop_back();
   }
   Assert(getSatContext()->getLevel() == d_topLevel);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 39fd90012..e0191ccc9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -358,6 +358,7 @@ class TheoryArrays : public Theory {
   // List of nodes that need permanent references in this context
   context::CDList<Node> d_permRef;
   context::CDList<Node> d_modelConstraints;
+  context::CDHashSet<Node, NodeHashFunction > d_lemmasSaved;
   std::vector<Node> d_lemmas;
 
   Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index d6aa51aba..9867ccd4e 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -22,6 +22,72 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+/**
+ * flattenNode looks for children of same kind, and if found merges
+ * them into the parent.
+ *
+ * It simultaneously handles a couple of other optimizations: 
+ * - trivialNode - if found during exploration, return that node itself
+ *    (like in case of OR, if "true" is found, makes sense to replace
+ *     whole formula with "true")
+ * - skipNode - as name suggests, skip them
+ *    (like in case of OR, you may want to skip any "false" nodes found)
+ *
+ * Use a null node if you want to ignore any of the optimizations.
+ */
+RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
+{
+  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+
+  node_set visited;
+  visited.insert(skipNode);
+
+  std::vector<TNode> toProcess;
+  toProcess.push_back(n);
+
+  Kind k = n.getKind();
+  typedef std::vector<TNode> ChildList;
+  ChildList childList;   //TNode should be fine, since 'n' is still there
+
+  for (unsigned i = 0; i < toProcess.size(); ++ i) {
+    TNode current = toProcess[i];
+    for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
+      TNode child = current[j];
+      if(visited.find(child) != visited.end()) {
+        continue;
+      } else if(child == trivialNode) {
+        return RewriteResponse(REWRITE_DONE, trivialNode);
+      } else {
+        visited.insert(child);
+        if(child.getKind() == k)
+          toProcess.push_back(child);
+        else
+          childList.push_back(child);
+      }
+    }
+  }
+  if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
+  if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]);
+
+  /* Trickery to stay under number of children possible in a node */
+  NodeManager* nodeManager = NodeManager::currentNM();
+  static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
+  if (childList.size() < MAX_CHILDREN) {
+    Node retNode = nodeManager->mkNode(k, childList);
+    return RewriteResponse(REWRITE_DONE, retNode);
+  } else {
+    Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) );
+    NodeBuilder<> nb(k);
+    ChildList::iterator cur = childList.begin(), next, en = childList.end();
+    while( cur != en ) {
+      next = min(cur + MAX_CHILDREN, en);
+      nb << (nodeManager->mkNode(k, ChildList(cur, next) ));
+      cur = next;
+    }
+    return RewriteResponse(REWRITE_DONE, nb.constructNode());
+  }
+}
+
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
   Node tt = nodeManager->mkConst(true);
@@ -35,55 +101,30 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     break;
   }
   case kind::OR: {
-    if (n.getNumChildren() == 2) {
-      if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
-      if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]);
-      if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    bool done = true;
+    TNode::iterator i = n.begin(), iend = n.end();
+    for(; i != iend; ++i) {
+      if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
+      if (*i == ff) done = false;
+      if ((*i).getKind() == kind::OR) done = false;
     }
-    else {
-      bool done = true;
-      TNode::iterator i = n.begin(), iend = n.end();
-      for(; i != iend; ++i) {
-        if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
-        if (*i == ff) done = false;
-      }
-      if (!done) {
-        NodeBuilder<> nb(kind::OR);
-        for(i = n.begin(); i != iend; ++i) {
-          if (*i != ff) nb << *i;
-        }
-        if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, ff);
-        if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-        return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
-      }
+    if (!done) {
+      return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff);
     }
     break;
   }
   case kind::AND: {
-    //TODO: Why REWRITE_AGAIN here?
-    if (n.getNumChildren() == 2) {
-      if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
-      if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
-      if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    bool done = true;
+    TNode::iterator i = n.begin(), iend = n.end();
+    for(; i != iend; ++i) {
+      if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
+      if (*i == tt) done = false;
+      if ((*i).getKind() == kind::AND) done = false;
     }
-    else {
-      bool done = true;
-      TNode::iterator i = n.begin(), iend = n.end();
-      for(; i != iend; ++i) {
-        if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
-        if (*i == tt) done = false;
-      }
-      if (!done) {
-        NodeBuilder<> nb(kind::AND);
-        for(i = n.begin(); i != iend; ++i) {
-          if (*i != tt) {
-            nb << *i;
-          }
-        }
-        if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, tt);
-        if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-        return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
-      }
+    if (!done) {
+      RewriteResponse ret = flattenNode(n, /*trivialNode = */ ff, /* skipNode = */ tt);
+      Debug("bool-flatten") << n << ": " << ret.node << std::endl;
+      return ret;
     }
     break;
   }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d8a784544..997244c40 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -31,7 +31,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_bitblaster(new Bitblaster(c, bv)),
     d_bitblastQueue(c),
-    d_statistics()
+    d_statistics(),
+    d_validModelCache(c, true)
 {}
 
 BitblastSolver::~BitblastSolver() {
@@ -87,6 +88,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   // Processing assertions  
   while (!done()) {
     TNode fact = get();
+    d_validModelCache = false;
     Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
     if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
@@ -138,8 +140,46 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
   return d_bitblaster->collectModelInfo(m); 
 }
 
-Node BitblastSolver::getModelValue(TNode node) {
-  Node val = d_bitblaster->getVarValue(node);
-  Assert (val != Node() || d_bv->isSharedTerm(node));
+Node BitblastSolver::getModelValue(TNode node)
+{
+  if (!d_validModelCache) {
+    d_modelCache.clear();
+    d_validModelCache = true;
+  }
+  return getModelValueRec(node);
+}
+
+Node BitblastSolver::getModelValueRec(TNode node)
+{
+  Node val;
+  if (node.isConst()) {
+    return node;
+  }
+  NodeMap::iterator it = d_modelCache.find(node);
+  if (it != d_modelCache.end()) {
+    val = (*it).second;
+    Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
+    return val;
+  }
+  if (d_bv->isLeaf(node)) {
+    val = d_bitblaster->getVarValue(node);
+    if (val == Node()) {
+      // If no value in model, just set to 0
+      val = utils::mkConst(utils::getSize(node), (unsigned)0);
+    }
+  } else {
+    NodeBuilder<> valBuilder(node.getKind());
+    if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      valBuilder << node.getOperator();
+    }
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      valBuilder << getModelValueRec(node[i]);
+    }
+    val = valBuilder;
+    val = Rewriter::rewrite(val);
+  }
+  Assert(val.isConst());
+  d_modelCache[node] = val;
+  Debug("bitvector-model") << node << " => " << val <<"\n";
   return val; 
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 1fab621cd..819b3d62c 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -19,7 +19,7 @@
 #pragma once
 
 #include "theory/bv/bv_subtheory.h"
-
+#include "theory/substitutions.h"
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -41,6 +41,12 @@ class BitblastSolver : public SubtheorySolver {
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
   Statistics d_statistics; 
+
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_modelCache;
+  context::CDO<bool> d_validModelCache;
+  Node getModelValueRec(TNode node);
+
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index a1c8f0e9a..c0546f892 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -387,17 +387,26 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node CoreSolver::getModelValue(TNode var) {
+  // we don't need to evaluate bv expressions and only look at variable values
+  // because this only gets called when the core theory is complete (i.e. no other bv
+  // function symbols are currently asserted)
+  Assert (d_slicer->isCoreTerm(var)); 
+  
+  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";  
   Assert (isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);
+  Node result = Node(); 
   if (repr.getKind() == kind::CONST_BITVECTOR) {
-    return repr; 
-  }
-  if (d_modelValues.find(repr) == d_modelValues.end()) {
+    result = repr; 
+  } else if (d_modelValues.find(repr) == d_modelValues.end()) {
     // it may be a shared term that never gets asserted
+    // result is just Null
     Assert(d_bv->isSharedTerm(var));
-    return Node(); 
+  } else {
+    result = d_modelValues[repr]; 
   }
-  return d_modelValues[repr]; 
+  Debug("bitvector-model") << " => " << result <<"\n"; 
+  return result; 
 }
 
 CoreSolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 40093f070..f45250f5b 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -178,13 +178,18 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
+  Assert (isInequalityOnly(var)); 
+  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";  
   Assert (isComplete());
+  Node result = Node(); 
   if (!d_inequalityGraph.hasValueInModel(var)) {
     Assert (d_bv->isSharedTerm(var));
-    return Node(); 
+  } else {
+    BitVector val = d_inequalityGraph.getValueInModel(var);
+    result = utils::mkConst(val);
   }
-  BitVector val = d_inequalityGraph.getValueInModel(var);
-  return utils::mkConst(val); 
+  Debug("bitvector-model") << " => " << result <<"\n";  
+  return result; 
 }
 
 InequalitySolver::Statistics::Statistics()
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 96b5d2928..fe02b230e 100644
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -37,7 +37,10 @@ CVC_TESTS = \
 	preprocess_09.cvc \
 	preprocess_10.cvc \
 	preprocess_11.cvc \
-	preprocess_12.cvc
+	preprocess_12.cvc \
+	preprocess_13.cvc \
+	preprocess_14.cvc \
+	preprocess_15.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 
diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc
new file mode 100644
index 000000000..7a2ed7dd8
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_13.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9))))))))));
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc b/test/regress/regress0/preprocess/preprocess_14.cvc
new file mode 100644
index 000000000..04a6f4c50
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_14.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a6 AND (a7 AND (a8 AND a9))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc b/test/regress/regress0/preprocess/preprocess_15.cvc
new file mode 100644
index 000000000..30df35e53
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_15.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a3 AND (a6 AND (a7 AND (a8 AND a9)))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index e71dcb41d..ccba0164a 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -55,7 +55,7 @@ public:
     d_addClauseCalled(false) {
   }
 
-  SatVariable newVar(bool theoryAtom) {
+  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) {
     return d_nextVar++;
   }