From c0324db3ac7e5984c632f46690f58c333b9a42b2 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Thu, 22 Mar 2012 21:45:31 +0000
Subject: Merged updated version of the bitvector theory:   * added
 simplification rewrites

---
 src/theory/bv/theory_bv.cpp | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'src/theory/bv/theory_bv.cpp')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 79c065d7e..45d99f9c9 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -45,48 +45,48 @@ TheoryBV::~TheoryBV() {
 }
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0)
+  d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
+  d_solveTimer("theory::bv::solveTimer")
 {
   StatisticsRegistry::registerStat(&d_avgConflictSize);
   StatisticsRegistry::registerStat(&d_solveSubstitutions);
+  StatisticsRegistry::registerStat(&d_solveTimer); 
 }
 
 TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_avgConflictSize);
   StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
+  StatisticsRegistry::unregisterStat(&d_solveTimer); 
 }
 
 void TheoryBV::preRegisterTerm(TNode node) {
-
   BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
   //marker literal: bitblast all terms before we start
-  d_bitblaster->bitblast(node); 
+  //d_bitblaster->bitblast(node); 
 }
 
 void TheoryBV::check(Effort e) {
-  BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-  if (fullEffort(e)) {
-    std::vector<TNode> assertions; 
+  if (fullEffort(e) && !done()) {
+    Trace("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
+    std::vector<TNode> assertions;
+      
     while (!done()) {
       TNode assertion = get();
-      Debug("bitvector") << "assertion " << assertion << "\n"; 
-      assertions.push_back(assertion);
+      Trace("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; 
       d_bitblaster->bitblast(assertion); 
+      d_bitblaster->assertToSat(assertion); 
     }
-    
-    std::vector<TNode>::const_iterator it = assertions.begin();
-    for (; it != assertions.end(); ++it) {
-      d_bitblaster->assertToSat(*it); 
-    }
+
+    TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); 
     bool res = d_bitblaster->solve();
     if (res == false) {
       std::vector<TNode> conflictAtoms;
       d_bitblaster->getConflict(conflictAtoms);
-
       d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
       
       Node conflict = mkConjunction(conflictAtoms);
       d_out->conflict(conflict);
+      Trace("bitvector") << "TheoryBV::check returns conflict. \n ";
       return; 
     }
   }
-- 
cgit v1.2.3