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

7 files changed, 163 insertions, 56 deletions

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()