6 files changed, 42 insertions, 2 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index ad62ade38..8579012ab 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -108,6 +108,13 @@ void Bitblaster::bbAtom(TNode node) {
   }
 }
 
+uint64_t Bitblaster::computeAtomWeight(TNode node) {
+  node = node.getKind() == kind::NOT?  node[0] : node;
+
+  Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
+  uint64_t size = utils::numNodes(atom_bb);
+  return size;
+}
 
 void Bitblaster::bbTerm(TNode node, Bits& bits) {
 
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 2c52a2670..c122c407d 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -165,6 +165,7 @@ public:
   }
 
   bool isSharedTerm(TNode node);
+  uint64_t computeAtomWeight(TNode node);
 
 private:
  
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 997244c40..2308f36a3 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -19,6 +19,8 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/bv/bitblaster.h"
 #include "theory/bv/options.h"
+#include "theory/decision_attributes.h"
+#include "decision/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -58,7 +60,12 @@ void BitblastSolver::preRegister(TNode node) {
     if (options::bitvectorEagerBitblast()) {
       d_bitblaster->bbAtom(node);
     } else {
+      CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
       d_bitblastQueue.push_back(node);
+      if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
+          !node.hasAttribute(theory::DecisionWeightAttr())) {
+        node.setAttribute(theory::DecisionWeightAttr(), d_bitblaster->computeAtomWeight(node));
+      }
     }
   }
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 433223308..c597cb083 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -78,13 +78,15 @@ TheoryBV::Statistics::Statistics():
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
   d_solveTimer("theory::bv::solveTimer"),
   d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0)
+  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
+  d_weightComputationTimer("theory::bv::weightComputationTimer")
 {
   StatisticsRegistry::registerStat(&d_avgConflictSize);
   StatisticsRegistry::registerStat(&d_solveSubstitutions);
   StatisticsRegistry::registerStat(&d_solveTimer);
   StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
   StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
+  StatisticsRegistry::registerStat(&d_weightComputationTimer);
 }
 
 TheoryBV::Statistics::~Statistics() {
@@ -93,6 +95,7 @@ TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_solveTimer);
   StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
   StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
+  StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
 }
 
 
@@ -205,6 +208,7 @@ void TheoryBV::propagate(Effort e) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
     // temporary fix for incremental bit-blasting 
     if (d_valuation.isSatLiteral(literal)) {
+      Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
       ok = d_out->propagate(literal);
     }
   }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8b184f972..481493e13 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -78,6 +78,7 @@ private:
     TimerStat   d_solveTimer;
     IntStat d_numCallsToCheckFullEffort;
     IntStat d_numCallsToCheckStandardEffort; 
+    TimerStat   d_weightComputationTimer;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dffdf10df..174df03ab 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -23,7 +23,7 @@
 #include <vector>
 #include <sstream>
 #include "expr/node_manager.h"
-
+#include "theory/decision_attributes.h"
 
 
 namespace CVC4 {
@@ -493,6 +493,26 @@ inline T gcd(T a, T b) {
 }
 
 
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
+inline uint64_t numNodesAux(TNode node, TNodeSet& seen) {
+  if (seen.find(node) != seen.end())
+    return 0;
+
+  uint64_t size = 1;
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    size += numNodesAux(node[i], seen);
+  }
+  seen.insert(node);
+  return size;
+}
+
+inline uint64_t numNodes(TNode node) {
+  TNodeSet seen;
+  uint64_t size = numNodesAux(node, seen);
+  return size;
+}
+
 }
 }
 }