summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp257
1 files changed, 83 insertions, 174 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c977435ec..79c065d7e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -19,196 +19,82 @@
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
-
#include "theory/valuation.h"
+#include "theory/bv/bv_sat.h"
+
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
+using namespace CVC4::context;
using namespace std;
+using namespace CVC4::theory::bv::utils;
-void TheoryBV::preRegisterTerm(TNode node) {
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
+ : Theory(THEORY_BV, c, u, out, valuation),
+ d_context(c),
+ d_assertions(c),
+ d_bitblaster(new Bitblaster(c) ),
+ d_statistics()
+ {
+ d_true = utils::mkTrue();
+ }
+TheoryBV::~TheoryBV() {
+ delete d_bitblaster;
+}
+TheoryBV::Statistics::Statistics():
+ d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+ d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0)
+{
+ StatisticsRegistry::registerStat(&d_avgConflictSize);
+ StatisticsRegistry::registerStat(&d_solveSubstitutions);
+}
- BVDebug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+TheoryBV::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_avgConflictSize);
+ StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
+}
- if (node.getKind() == kind::EQUAL) {
- d_eqEngine.addTerm(node[0]);
- if (node[0].getKind() == kind::BITVECTOR_CONCAT) {
- for (unsigned i = 0, i_end = node[0].getNumChildren(); i < i_end; ++ i) {
- d_eqEngine.addTerm(node[0][i]);
- }
- }
- d_eqEngine.addTerm(node[1]);
- if (node[1].getKind() == kind::BITVECTOR_CONCAT) {
- for (unsigned i = 0, i_end = node[1].getNumChildren(); i < i_end; ++ i) {
- d_eqEngine.addTerm(node[1][i]);
- }
- }
+void TheoryBV::preRegisterTerm(TNode node) {
- d_normalization[node] = new Normalization(d_context, node);
- }
+ BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+ //marker literal: bitblast all terms before we start
+ d_bitblaster->bitblast(node);
}
void TheoryBV::check(Effort e) {
-
BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
- // Normalization iterators
- NormalizationMap::iterator it = d_normalization.begin();
- NormalizationMap::iterator it_end = d_normalization.end();
-
- // Get all the assertions
- std::vector<TNode> assertionsList;
- while (!done()) {
- // Get the assertion
- TNode assertion = get();
- d_assertions.insert(assertion);
- assertionsList.push_back(assertion);
- }
-
- bool normalizeEqualities = false;
-
- for (unsigned i = 0; i < assertionsList.size(); ++ i) {
-
- TNode assertion = assertionsList[i];
-
- BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
-
- // Do the right stuff
- switch (assertion.getKind()) {
- case kind::EQUAL: {
- // Slice and solve the equality
- bool ok = d_sliceManager.solveEquality(assertion[0], assertion[1]);
- if (!ok) return;
- // Normalize all equalities
- normalizeEqualities = true;
- it = d_normalization.begin();
- it = d_normalization.end();
- break;
+ if (fullEffort(e)) {
+ std::vector<TNode> assertions;
+ while (!done()) {
+ TNode assertion = get();
+ Debug("bitvector") << "assertion " << assertion << "\n";
+ assertions.push_back(assertion);
+ d_bitblaster->bitblast(assertion);
}
- case kind::NOT: {
- if (!normalizeEqualities) {
- // We still need to check this dis-equality, as it might have been pre-registered just now
- // so we didn't have a chance to propagate
- it = d_normalization.find(assertion[0]);
- if (it->second->assumptions.size() == 1) {
- // Just normalize this equality
- normalizeEqualities = true;
- it_end = it;
- it_end ++;
- }
- }
- break;
+
+ std::vector<TNode>::const_iterator it = assertions.begin();
+ for (; it != assertions.end(); ++it) {
+ d_bitblaster->assertToSat(*it);
}
- default:
- Unhandled(assertion.getKind());
- }
- }
-
- if (normalizeEqualities) {
+ bool res = d_bitblaster->solve();
+ if (res == false) {
+ std::vector<TNode> conflictAtoms;
+ d_bitblaster->getConflict(conflictAtoms);
- BVDebug("bitvector") << "Checking for propagations" << std::endl;
-
- NormalizationMap::iterator it = d_normalization.begin();
- NormalizationMap::iterator it_end = d_normalization.end();
- for(; it != it_end; ++ it) {
-
- TNode equality = it->first;
- BVDebug("bitvector") << "Checking " << equality << std::endl;
- Normalization& normalization = *it->second;
+ d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
- // If asserted, we don't care
- if (d_assertions.find(equality) != d_assertions.end()) continue;
-
- // Assumptions
- std::set<TNode> assumptions;
- TNode lhs = normalization.equalities.back()[0];
- TNode rhs = normalization.equalities.back()[1];
- // If already satisfied, do nothing
- if (lhs == rhs) continue;
-
- Node lhsNormalized = d_eqEngine.normalize(lhs, assumptions);
- Node rhsNormalized = d_eqEngine.normalize(rhs, assumptions);
-
- if (lhsNormalized == lhs && rhsNormalized == rhs) continue;
-
- normalization.equalities.push_back(lhsNormalized.eqNode(rhsNormalized));
- normalization.assumptions.push_back(assumptions);
-
- BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl;
- BVDebug("bitvector") << " assumptions " << utils::setToString(assumptions) << std::endl;
-
-
- BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
-
- // If both are equal we can propagate
- bool propagate = lhsNormalized == rhsNormalized;
- // otherwise if both are constants, we propagate negation (if not already there)
- bool propagateNegation = !propagate &&
- lhsNormalized.getKind() == kind::CONST_BITVECTOR && rhsNormalized.getKind() == kind::CONST_BITVECTOR
- && d_assertions.find(equality.notNode()) == d_assertions.end();
- ;
- if (propagate || propagateNegation) {
- Node implied = propagate ? Node(equality) : equality.notNode() ;
- Node impliedNegated = propagate ? equality.notNode() : Node(equality) ;
- // If the negation of what's implied has been asserted, we are in conflict
- if (d_assertions.find(impliedNegated) != d_assertions.end()) {
- BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
- // Construct the assumptions
- for (unsigned i = 0; i < normalization.assumptions.size(); ++ i) {
- assumptions.insert(normalization.assumptions[i].begin(), normalization.assumptions[i].end());
- }
- // Make the conflict
- assumptions.insert(impliedNegated);
- d_out->conflict(mkConjunction(assumptions));
- return;
- }
- // Otherwise we propagate the implication
- else {
- BVDebug("bitvector") << "TheoryBV::check(" << e << "): propagating " << implied << std::endl;
- d_out->propagate(implied);
- d_assertions.insert(implied);
- }
- }
+ Node conflict = mkConjunction(conflictAtoms);
+ d_out->conflict(conflict);
+ return;
}
}
}
-bool TheoryBV::triggerEquality(size_t triggerId) {
- BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl;
- Assert(triggerId < d_triggers.size());
- BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl;
-
- return true;
-
- TNode equality = d_triggers[triggerId];
-
- // If we have just asserted this equality ignore it
- if (d_assertions.contains(equality)) return true;
-
- // If we have a negation asserted, we have a confict
- if (d_assertions.contains(equality.notNode())) {
-
- std::vector<TNode> explanation;
- d_eqEngine.getExplanation(equality[0], equality[1], explanation);
- std::set<TNode> assumptions;
- assumptions.insert(equality.notNode());
- utils::getConjuncts(explanation, assumptions);
- d_out->conflict(utils::mkConjunction(assumptions));
-
- return false;
- }
-
- // Otherwise we propagate this equality
- d_out->propagate(equality);
-
- return true;
-}
Node TheoryBV::getValue(TNode n) {
- NodeManager* nodeManager = NodeManager::currentNM();
+ //NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -216,8 +102,7 @@ Node TheoryBV::getValue(TNode n) {
Unhandled(kind::VARIABLE);
case kind::EQUAL: // 2 args
- return nodeManager->
- mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
+ Unhandled(kind::VARIABLE);
default:
Unhandled(n.getKind());
@@ -229,13 +114,37 @@ Node TheoryBV::explain(TNode node) {
TNode equality = node.getKind() == kind::NOT ? node[0] : node;
Assert(equality.getKind() == kind::EQUAL);
+ Assert(0);
+ return node;
+
+}
- context::CDList< set<TNode> >& vec = d_normalization[equality]->assumptions;
- std::set<TNode> assumptions;
- for (unsigned i = 0; i < vec.size(); ++ i) {
- BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl;
- BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl;
- assumptions.insert(vec[i].begin(), vec[i].end());
+// Node TheoryBV::preprocessTerm(TNode term) {
+// return term; //d_staticEqManager.find(term);
+// }
+
+Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+ switch(in.getKind()) {
+ case kind::EQUAL:
+
+ if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+ ++(d_statistics.d_solveSubstitutions);
+ outSubstitutions.addSubstitution(in[0], in[1]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+ ++(d_statistics.d_solveSubstitutions);
+ outSubstitutions.addSubstitution(in[1], in[0]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ // to do constant propagations
+
+ break;
+ case kind::NOT:
+ break;
+ default:
+ // TODO other predicates
+ break;
}
- return utils::mkConjunction(assumptions);
+ return PP_ASSERT_STATUS_UNSOLVED;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback