Merging CAV14 paper bit-vector work.

1 files changed, 108 insertions, 0 deletions

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
new file mode 100644
index 000000000..af35c0499
--- /dev/null
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -0,0 +1,108 @@
+/*********************                                                        */
+/*! \file bv_eager_solver.h
+ ** \verbatim
+ ** Original author: Liana Hadarean 
+ ** Major contributors: none
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Eager bit-blasting solver. 
+ **
+ ** Eager bit-blasting solver.
+ **/
+
+#include "theory/bv/bv_eager_solver.h"
+#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/eager_bitblaster.h"
+#include "theory/bv/aig_bitblaster.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+EagerBitblastSolver::EagerBitblastSolver()
+  : d_assertionSet()
+  , d_bitblaster(NULL)
+  , d_aigBitblaster(NULL)
+  , d_useAig(options::bitvectorAig())
+{}
+
+EagerBitblastSolver::~EagerBitblastSolver() {
+  if (d_useAig) {
+    Assert (d_bitblaster == NULL); 
+    delete d_aigBitblaster;
+  }
+  else {
+    Assert (d_aigBitblaster == NULL); 
+    delete d_bitblaster;
+  }
+}
+
+void EagerBitblastSolver::turnOffAig() {
+  Assert (d_aigBitblaster == NULL &&
+          d_bitblaster == NULL);
+  d_useAig = false;
+}
+
+void EagerBitblastSolver::initialize() {
+  Assert(!isInitialized());
+  if (d_useAig) {
+    d_aigBitblaster = new AigBitblaster();
+  } else {
+    d_bitblaster = new EagerBitblaster();
+  }
+}
+
+bool EagerBitblastSolver::isInitialized() {
+  bool init = d_aigBitblaster != NULL || d_bitblaster != NULL;
+  if (init) {
+    Assert (!d_useAig || d_aigBitblaster);
+    Assert (d_useAig || d_bitblaster);
+  }
+  return init;
+}
+
+void EagerBitblastSolver::assertFormula(TNode formula) {
+  Assert (isInitialized());
+  Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
+  d_assertionSet.insert(formula);
+  //ensures all atoms are bit-blasted and converted to AIG
+  if (d_useAig) 
+    d_aigBitblaster->bbFormula(formula);
+  else
+    d_bitblaster->bbFormula(formula);
+}
+
+bool EagerBitblastSolver::checkSat() {
+  Assert (isInitialized());
+  std::vector<TNode> assertions; 
+  for (AssertionSet::const_iterator it = d_assertionSet.begin(); it != d_assertionSet.end(); ++it) {
+    assertions.push_back(*it); 
+  }
+  if (!assertions.size())
+    return true;
+  
+  if (d_useAig) {
+    Node query = utils::mkAnd(assertions); 
+    return d_aigBitblaster->solve(query);
+  }
+  
+  return d_bitblaster->solve(); 
+}
+
+bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) {
+  Assert (isInitialized());
+  if (formulas.size() != d_assertionSet.size())
+    return false; 
+  for (unsigned i = 0; i < formulas.size(); ++i) {
+    Assert (formulas[i].getKind() == kind::BITVECTOR_EAGER_ATOM);
+    TNode formula = formulas[i][0];
+    if (d_assertionSet.find(formula) == d_assertionSet.end())
+      return false; 
+  }
+  return true; 
+}