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_quick_check.cpp | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/bv_quick_check.cpp')
-rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 377 |
1 files changed, 377 insertions, 0 deletions
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp new file mode 100644 index 000000000..1adbb83d9 --- /dev/null +++ b/src/theory/bv/bv_quick_check.cpp @@ -0,0 +1,377 @@ +/********************* */ +/*! \file bv_quick_check.cpp + ** \verbatim + ** Original author: Liana Hadaren + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 Wrapper around the SAT solver used for bitblasting. + ** + ** Wrapper around the SAT solver used for bitblasting. + **/ + +#include "theory/bv/bv_quick_check.h" +#include "theory/bv/theory_bv_utils.h" + +#include "theory/bv/bitblaster_template.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::prop; + +BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv) + : d_ctx(new context::Context()) + , d_bitblaster(new TLazyBitblaster(d_ctx, bv, name, true)) + , d_conflict() + , d_inConflict(d_ctx, false) +{} + + +bool BVQuickCheck::inConflict() { return d_inConflict.get(); } + +uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) { + return d_bitblaster->computeAtomWeight(node, seen); +} + +void BVQuickCheck::setConflict() { + Assert (!inConflict()); + std::vector<TNode> conflict; + d_bitblaster->getConflict(conflict); + Node confl = utils::mkConjunction(conflict); + d_inConflict = true; + d_conflict = confl; +} + +prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) { + Node conflict; + + for (unsigned i = 0; i < assumptions.size(); ++i) { + TNode a = assumptions[i]; + Assert (a.getType().isBoolean()); + d_bitblaster->bbAtom(a); + bool ok = d_bitblaster->assertToSat(a, false); + if (!ok) { + setConflict(); + return SAT_VALUE_FALSE; + } + } + + if (budget == 0) { + bool ok = d_bitblaster->propagate(); + if (!ok) { + setConflict(); + return SAT_VALUE_FALSE; + } + return SAT_VALUE_UNKNOWN; // could check if assignment is full and return SAT_VALUE_TRUE + } + + prop::SatValue res = d_bitblaster->solveWithBudget(budget); + if (res == SAT_VALUE_FALSE) { + setConflict(); + return res; + } + // could be unknown or could be sat + return res; +} + +prop::SatValue BVQuickCheck::checkSat(unsigned long budget) { + prop::SatValue res = d_bitblaster->solveWithBudget(budget); + if (res == SAT_VALUE_FALSE) { + setConflict(); + } + return res; +} + +bool BVQuickCheck::addAssertion(TNode assertion) { + Assert (assertion.getType().isBoolean()); + d_bitblaster->bbAtom(assertion); + // assert to sat solver and run bcp to detect easy conflicts + bool ok = d_bitblaster->assertToSat(assertion, true); + if (!ok) { + setConflict(); + } + return ok; +} + + +void BVQuickCheck::push() { + d_ctx->push(); +} + +void BVQuickCheck::pop() { + d_ctx->pop(); +} + +BVQuickCheck::vars_iterator BVQuickCheck::beginVars() { + return d_bitblaster->beginVars(); +} +BVQuickCheck::vars_iterator BVQuickCheck::endVars() { + return d_bitblaster->endVars(); +} + +Node BVQuickCheck::getVarValue(TNode var) { + return d_bitblaster->getVarValue(var); +} + + +/** + * Constructs a new sat solver which requires throwing out the atomBBCache + * but keeps all the termBBCache + * + */ +void BVQuickCheck::clearSolver() { + popToZero(); + d_bitblaster->clearSolver(); +} + +void BVQuickCheck::popToZero() { + while (d_ctx->getLevel() > 0) { + d_ctx->pop(); + } +} + +void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) { + d_bitblaster->collectModelInfo(model, fullModel); +} + +BVQuickCheck::~BVQuickCheck() { + delete d_bitblaster; +} + +QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget) + : d_solver(solver) + , d_budget(budget) + , d_numCalled(0) + , d_minRatioSum(0) + , d_numConflicts(0) + , d_period(20) + , d_thresh(0.7) + , d_hardThresh(0.9) + , d_statistics(name) +{} +QuickXPlain::~QuickXPlain() {} + +unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high, + std::vector<TNode>& conflict) { + + Assert(!d_solver->getConflict().isNull() && + d_solver->inConflict()); + Node query_confl = d_solver->getConflict(); + + // conflict wasn't actually minimized + if (query_confl.getNumChildren() == high - low + 1) { + return high; + } + + TNodeSet nodes; + for (unsigned i = low; i <= high; i++) { + nodes.insert(conflict[i]); + } + + unsigned write = low; + for (unsigned i = 0; i < query_confl.getNumChildren(); ++i) { + TNode current = query_confl[i]; + // the conflict can have nodes in lower decision levels + if (nodes.find(current) != nodes.end()) { + conflict[write++] = current; + nodes.erase(nodes.find(current)); + } + } + // if all of the nodes in the conflict were on a lower level + if (write == low) { + return low; + } + Assert (write != 0); + unsigned new_high = write - 1; + + for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) { + conflict[write++] = *it; + } + Assert (write -1 == high); + Assert (new_high <= high); + + return new_high; +} + +void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high, + std::vector<TNode>& conflict, + std::vector<TNode>& new_conflict) { + + Assert (low <= high && high < conflict.size()); + + if (low == high) { + new_conflict.push_back(conflict[low]); + return; + } + + // check if top half is unsat + unsigned new_low = (high - low + 1)/ 2 + low; + d_solver->push(); + + for (unsigned i = new_low; i <=high; ++i) { + bool ok = d_solver->addAssertion(conflict[i]); + if (!ok) { + unsigned top = selectUnsatCore(new_low, i, conflict); + d_solver->pop(); + minimizeConflictInternal(new_low, top, conflict, new_conflict); + return; + } + } + + SatValue res = d_solver->checkSat(d_budget); + + if (res == SAT_VALUE_UNKNOWN) { + ++(d_statistics.d_numUnknown); + } else { + ++(d_statistics.d_numSolved); + } + + if (res == SAT_VALUE_FALSE) { + unsigned top = selectUnsatCore(new_low, high, conflict); + d_solver->pop(); + minimizeConflictInternal(new_low, top, conflict, new_conflict); + return; + } + + d_solver->pop(); + unsigned new_high = new_low - 1; + d_solver->push(); + + // check bottom half + for (unsigned i = low; i <= new_high; ++i) { + bool ok = d_solver->addAssertion(conflict[i]); + if (!ok) { + unsigned top = selectUnsatCore(low, i, conflict); + d_solver->pop(); + minimizeConflictInternal(low, top, conflict, new_conflict); + return; + } + } + + res = d_solver->checkSat(d_budget); + + if (res == SAT_VALUE_UNKNOWN) { + ++(d_statistics.d_numUnknown); + } else { + ++(d_statistics.d_numSolved); + } + + if (res == SAT_VALUE_FALSE) { + unsigned top = selectUnsatCore(low, new_high, conflict); + d_solver->pop(); + minimizeConflictInternal(low, top, conflict, new_conflict); + return; + } + + // conflict (probably) contains literals in both halves + // keep bottom half in context (no pop) + minimizeConflictInternal(new_low, high, conflict, new_conflict); + d_solver->pop(); + d_solver->push(); + for (unsigned i = 0; i < new_conflict.size(); ++i) { + bool ok = d_solver->addAssertion(new_conflict[i]); + if (!ok) { + ++(d_statistics.d_numUnknownWasUnsat); + d_solver->pop(); + return; + } + } + minimizeConflictInternal(low, new_high, conflict, new_conflict); + d_solver->pop(); +} + + +bool QuickXPlain::useHeuristic() { + return true; + // d_statistics.d_finalPeriod.setData(d_period); + // // try to minimize conflict periodically + // if (d_numConflicts % d_period == 0) + // return true; + + // if (d_numCalled == 0) { + // return true; + // } + + // if (d_minRatioSum / d_numCalled >= d_thresh && + // d_numCalled <= 20 ) { + // return false; + // } + + // if (d_minRatioSum / d_numCalled >= d_hardThresh) { + // return false; + // } + + // return true; +} + +Node QuickXPlain::minimizeConflict(TNode confl) { + ++d_numConflicts; + + if (!useHeuristic()) { + return confl; + } + + ++d_numCalled; + ++(d_statistics.d_numConflictsMinimized); + TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime); + Assert (confl.getNumChildren() > 2); + std::vector<TNode> conflict; + for (unsigned i = 0; i < confl.getNumChildren(); ++i) { + conflict.push_back(confl[i]); + } + d_solver->popToZero(); + std::vector<TNode> minimized; + minimizeConflictInternal(0, conflict.size() - 1, conflict, minimized); + + double minimization_ratio = ((double) minimized.size())/confl.getNumChildren(); + d_minRatioSum+= minimization_ratio; + + + // if (minimization_ratio >= d_hardThresh) { + // d_period = d_period * 5; + // } + + // if (minimization_ratio <= d_thresh && d_period >= 40) { + // d_period = d_period *0.5; + // } + + // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) { + // d_period = d_period * 2; + // } + d_statistics.d_avgMinimizationRatio.addEntry(minimization_ratio); + return utils::mkAnd(minimized); +} + +QuickXPlain::Statistics::Statistics(const std::string& name) + : d_xplainTime("theory::bv::"+name+"::QuickXplain::Time") + , d_numSolved("theory::bv::"+name+"::QuickXplain::NumSolved", 0) + , d_numUnknown("theory::bv::"+name+"::QuickXplain::NumUnknown", 0) + , d_numUnknownWasUnsat("theory::bv::"+name+"::QuickXplain::NumUnknownWasUnsat", 0) + , d_numConflictsMinimized("theory::bv::"+name+"::QuickXplain::NumConflictsMinimized", 0) + , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0) + , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio") +{ + StatisticsRegistry::registerStat(&d_xplainTime); + StatisticsRegistry::registerStat(&d_numSolved); + StatisticsRegistry::registerStat(&d_numUnknown); + StatisticsRegistry::registerStat(&d_numUnknownWasUnsat); + StatisticsRegistry::registerStat(&d_numConflictsMinimized); + StatisticsRegistry::registerStat(&d_finalPeriod); + StatisticsRegistry::registerStat(&d_avgMinimizationRatio); +} + +QuickXPlain::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_xplainTime); + StatisticsRegistry::unregisterStat(&d_numSolved); + StatisticsRegistry::unregisterStat(&d_numUnknown); + StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat); + StatisticsRegistry::unregisterStat(&d_numConflictsMinimized); + StatisticsRegistry::unregisterStat(&d_finalPeriod); + StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio); +} + |