diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/bv_eager_solver.cpp | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/bv_eager_solver.cpp')
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 108 |
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; +} |