diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-12-10 20:48:51 -0500 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-12-10 20:48:51 -0500 |
commit | 67af0bb961e42ab84c5f82245809ea12e2c12758 (patch) | |
tree | e2ac08edd8f3db204a712b87cf9532eb43f6b709 | |
parent | a8a471141d2fca4428b7c016ea4494d9925fc544 (diff) |
ported my bv-core branch from svn to git
-rw-r--r-- | src/theory/bv/Makefile.am | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 251 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 104 | ||||
-rw-r--r-- | src/theory/bv/kinds | 2 | ||||
-rw-r--r-- | src/theory/bv/slicer.cpp | 474 | ||||
-rw-r--r-- | src/theory/bv/slicer.h | 373 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 59 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 9 | ||||
-rw-r--r-- | src/util/bitvector.h | 11 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 10 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 19 | ||||
-rw-r--r-- | src/util/utility.h | 9 |
15 files changed, 1306 insertions, 30 deletions
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 669cbe9e0..686cc7e83 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -13,12 +13,16 @@ libbv_la_SOURCES = \ bitblaster.h \ bitblaster.cpp \ bv_subtheory.h \ - bv_subtheory_eq.h \ + bv_subtheory_eq.h \ bv_subtheory_eq.cpp \ + bv_subtheory_core.h \ + bv_subtheory_core.cpp \ bv_subtheory_bitblast.h \ bv_subtheory_bitblast.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ + slicer.h \ + slicer.cpp \ theory_bv.h \ theory_bv.cpp \ theory_bv_rewrite_rules.h \ diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index fbf9a45ee..bd76dd6d4 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -346,7 +346,7 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { BVDebug("bitvector-bb") << " with bits " << toString(bits); } - bb->storeVariable(node); + bb->storeVariable(node); } void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 21b389508..fb4394673 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -164,9 +164,9 @@ public: } bool isSharedTerm(TNode node); -private: - +private: + class Statistics { public: IntStat d_numTermClauses, d_numAtomClauses; diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 4dbba0797..a256b6001 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -33,7 +33,8 @@ namespace bv { enum SubTheory { SUB_EQUALITY = 1, - SUB_BITBLAST = 2 + SUB_BITBLAST = 2, + SUB_CORE = 3 }; inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp new file mode 100644 index 000000000..2252fc274 --- /dev/null +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -0,0 +1,251 @@ +/********************* */ +/*! \file bv_subtheory_eq.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): lianah + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "theory/bv/bv_subtheory_eq.h" + +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/slicer.h" +#include "theory/model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer) + : SubtheorySolver(c, bv), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_assertions(c), + d_slicer(slicer), + d_isCoreTheory(c, true) +{ + if (d_useEqualityEngine) { + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + } +} + +void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + +void CoreSolver::preRegister(TNode node) { + if (!d_useEqualityEngine) + return; + + if (node.getKind() == kind::EQUAL) { + d_equalityEngine.addTriggerEquality(node); + } else { + d_equalityEngine.addTerm(node); + } +} + + +void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) { + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } +} + +bool CoreSolver::decomposeFact(TNode fact) { + Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; + // FIXME: are this the right things to assert? + // assert decompositions since the equality engine does not know the semantics of + // concat: + // a == a_1 concat ... concat a_k + // b == b_1 concat ... concat b_k + TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; + + TNode a = eq[0]; + TNode b = eq[1]; + std::vector<Node> a_decomp; + std::vector<Node> b_decomp; + d_slicer->getBaseDecomposition(a, a_decomp); + d_slicer->getBaseDecomposition(b, b_decomp); + + Assert (a_decomp.size() == b_decomp.size()); + + Node new_a = utils::mkConcat(a_decomp); + Node new_b = utils::mkConcat(b_decomp); + + NodeManager* nm = NodeManager::currentNM(); + Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a); + Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b); + + bool ok = true; + ok = assertFact(a_eq_new_a, utils::mkTrue()); + if (!ok) return false; + ok = assertFact(b_eq_new_b, utils::mkTrue()); + if (!ok) return false; + ok = assertFact(fact, fact); + if (!ok) return false; + + if (fact.getKind() == kind::EQUAL) { + // assert the individual equalities as well + // a_i == b_i + for (unsigned i = 0; i < a_decomp.size(); ++i) { + Node eq_i = nm->mkNode(kind::EQUAL, a_decomp[i], b_decomp[i]); + ok = assertFact(eq_i, fact); + if (!ok) return false; + } + } + return true; +} + +bool CoreSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) { + Trace("bitvector::core") << "CoreSolver::addAssertions \n"; + Assert (!d_bv->inConflict()); + + bool ok = true; + std::vector<Node> core_eqs; + for (unsigned i = 0; i < assertions.size(); ++i) { + TNode fact = assertions[i]; + + // update whether we are in the core fragment + // FIXME: move isCoreTerm into CoreSolver + if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) { + d_isCoreTheory = false; + } + ok = decomposeFact(fact); + if (!ok) + return false; + } + + return true; +} + +bool CoreSolver::assertFact(TNode fact, TNode reason) { + Debug("bv-slicer") << "CoreSolver::assertFact fact=" << fact << endl; + Debug("bv-slicer") << " reason=" << reason << endl; + // Notify the equality engine + if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) { + Trace("bitvector::core") << " (assert " << fact << ")\n"; + //d_assertions.push_back(fact); + bool negated = fact.getKind() == kind::NOT; + TNode predicate = negated ? fact[0] : fact; + if (predicate.getKind() == kind::EQUAL) { + if (negated) { + // dis-equality + d_equalityEngine.assertEquality(predicate, false, reason); + } else { + // equality + d_equalityEngine.assertEquality(predicate, true, reason); + } + } else { + // Adding predicate if the congruence over it is turned on + if (d_equalityEngine.isFunctionKind(predicate.getKind())) { + d_equalityEngine.assertPredicate(predicate, !negated, reason); + } + } + } + + // checking for a conflict + if (d_bv->inConflict()) { + return false; + } + return true; +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { + BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_solver.storePropagation(equality); + } else { + return d_solver.storePropagation(equality.notNode()); + } +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { + BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; + if (value) { + return d_solver.storePropagation(predicate); + } else { + return d_solver.storePropagation(predicate.notNode()); + } +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + if (value) { + return d_solver.storePropagation(t1.eqNode(t2)); + } else { + return d_solver.storePropagation(t1.eqNode(t2).notNode()); + } +} + +void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { + d_solver.conflict(t1, t2); +} + +bool CoreSolver::storePropagation(TNode literal) { + return d_bv->storePropagation(literal, SUB_EQUALITY); +} + +void CoreSolver::conflict(TNode a, TNode b) { + std::vector<TNode> assumptions; + d_equalityEngine.explainEquality(a, b, true, assumptions); + d_bv->setConflict(mkAnd(assumptions)); +} + +void CoreSolver::collectModelInfo(TheoryModel* m) { + if (Debug.isOn("bitvector-model")) { + context::CDList<TNode>::const_iterator it = d_assertions.begin(); + for (; it!= d_assertions.end(); ++it) { + Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert " + << *it << ")\n"; + } + } + set<Node> termSet; + d_bv->computeRelevantTerms(termSet); + m->assertEqualityEngine(&d_equalityEngine, &termSet); +} diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h new file mode 100644 index 000000000..20b42d61c --- /dev/null +++ b/src/theory/bv/bv_subtheory_core.h @@ -0,0 +1,104 @@ +/********************* */ +/*! \file bv_subtheory_eq.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): lianah, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#pragma once + +#include "cvc4_private.h" +#include "theory/bv/bv_subtheory.h" +#include "context/cdhashmap.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class Slicer; + +/** + * Bitvector equality solver + */ +class CoreSolver : public SubtheorySolver { + + enum FactSource { + AXIOM = 0, // this is asserting that a node is equal to its decomposition + ASSERTION = 1, // externally visible assertion + SPLIT = 2 // fact resulting from a split + }; + + // NotifyClass: handles call-back from congruence closure module + + class NotifyClass : public eq::EqualityEngineNotify { + CoreSolver& d_solver; + + public: + NotifyClass(CoreSolver& solver): d_solver(solver) {} + bool eqNotifyTriggerEquality(TNode equality, bool value); + bool eqNotifyTriggerPredicate(TNode predicate, bool value); + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); + void eqNotifyConstantTermMerge(TNode t1, TNode t2); + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { } + void eqNotifyPostMerge(TNode t1, TNode t2) { } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } +}; + + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equality engine */ + eq::EqualityEngine d_equalityEngine; + + /** Store a propagation to the bv solver */ + bool storePropagation(TNode literal); + + /** Store a conflict from merging two constants */ + void conflict(TNode a, TNode b); + + /** FIXME: for debugging purposes only */ + context::CDList<TNode> d_assertions; + Slicer* d_slicer; + context::CDO<bool> d_isCoreTheory; + + bool assertFact(TNode fact, TNode reason); + bool decomposeFact(TNode fact); +public: + bool isCoreTheory() {return d_isCoreTheory; } + CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void preRegister(TNode node); + bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); + void explain(TNode literal, std::vector<TNode>& assumptions); + void collectModelInfo(TheoryModel* m); + void addSharedTerm(TNode t) { + d_equalityEngine.addTriggerTerm(t, THEORY_BV); + } + EqualityStatus getEqualityStatus(TNode a, TNode b) { + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + return EQUALITY_UNKNOWN; + } +}; + + +} +} +} diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 2faa12437..052e477ea 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -8,7 +8,7 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" typechecker "theory/bv/theory_bv_type_rules.h" properties finite -properties check propagate +properties check propagate presolve rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp new file mode 100644 index 000000000..73cad53b8 --- /dev/null +++ b/src/theory/bv/slicer.cpp @@ -0,0 +1,474 @@ +/********************* */ +/*! \file slicer.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector theory. + ** + ** Bitvector theory. + **/ + +#include "theory/bv/slicer.h" +#include "util/integer.h" +#include "util/utility.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace std; + +void Base::decomposeNode(TNode node, std::vector<Node>& decomp) { + Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl; + Index low = 0; + Index high = utils::getSize(node) - 1; + if (node.getKind() == kind::BITVECTOR_EXTRACT) { + low = utils::getExtractLow(node); + high = utils::getExtractHigh(node); + node = node[0]; + } + Index index = low; + for (Index i = low; i <= high; ++i) { + if (isCutPoint(i)) { + // make sure the extract is pushed down before concat + Node slice = Rewriter::rewrite(utils::mkExtract(node, i, index)); + index = i + 1; + decomp.push_back(slice); + Debug("bv-slicer") << slice <<" "; + } + } + Debug("bv-slicer") << endl; +} + +/** + * Adds a cutPoint at Index i and splits the corresponding Splinter + * + * @param i the index where the cut point will be introduced + * @param sp the splinter pointer corresponding to the splinter to be sliced + * @param low_splinter the resulting bottom part of the splinter + * @param top_splinter the resulting top part of the splinter + */ +void Slice::split(Index i, SplinterPointer& sp, Splinter*& low_splinter, Splinter*& top_splinter) { + Debug("bv-slicer") << "Slice::split " << this->debugPrint() << "\n"; + Assert (!d_base.isCutPoint(i)); + d_base.sliceAt(i); + + Splinter* s = NULL; + Slice::const_iterator it = begin(); + bool lt, gt; + for (; it != end(); ++it) { + lt = (it->second)->getHigh() >= i; + gt = (it->second)->getLow() <= i; + if (gt && lt) { + s = it->second; + break; + } + } + + Assert (s != NULL); + + sp = s->getPointer(); + Index low = s->getLow(); + Index high = s->getHigh(); + // creating the two splinter fragments + low_splinter = new Splinter(i, low); + top_splinter = new Splinter(high, i+1); + + addSplinter(low, low_splinter); + addSplinter(i+1, top_splinter); + Debug("bv-slicer") << " to " << this->debugPrint() << "\n"; +} + +void Slice::addSplinter(Index i, Splinter* sp) { + Assert (i == sp->getLow() && sp->getHigh() < d_bitwidth); + + if (i != 0) { + d_base.sliceAt(i - 1); + } + d_base.debugPrint(); + // free the memory associated with the previous splinter + if (d_splinters.find(i) != d_splinters.end()) { + delete d_splinters[i]; + } + d_splinters[i] = sp; +} + +std::string Slice::debugPrint() { + std::ostringstream os; + os << d_base.debugPrint(); + os << "{ "; + for (Slice::const_iterator it = begin(); it != end(); ++it) { + Splinter* s = (*it).second; + os << "[" << s->getLow() << ":" << s->getHigh() <<"]"; + Assert ((*it).first == s->getLow()); + Assert (s->getLow() == 0 || d_base.isCutPoint(s->getLow() - 1)); + SplinterPointer sp = s->getPointer(); + if (s->getPointer() != Undefined) { + os << "->" << sp.debugPrint(); + } + os << " "; + } + os << "}"; + return os.str(); +} + +void SliceBlock::computeBlockBase(std::vector<RootId>& queue) { + Debug("bv-slicer") << "SliceBlock::computeBlockBase for block" << d_rootId << endl; + Debug("bv-slicer") << this->debugPrint() << endl; + + // at this point d_base has all the cut points in the individual slices + for (unsigned row = 0; row < d_block.size(); ++row) { + Slice* slice = d_block[row]; + const Base base = slice->getBase(); + Base new_cut_points = base.diffCutPoints(d_base); + // use the cut points from the base to split the current slice + for (unsigned i = 0; i < d_bitwidth; ++i) { + if (new_cut_points.isCutPoint(i) && i != d_bitwidth - 1) { + Debug("bv-slicer") << " adding cut point at " << i << " for row " << row << endl; + // split this slice (this updates the slice's base) + Splinter* bottom, *top = NULL; + SplinterPointer sp; + slice->split(i, sp, bottom, top); + + if (sp != Undefined) { + // if we do need to split something else split it + Debug("bv-slicer") <<" must split " << sp.debugPrint(); + Slice* slice = d_slicer->getSlice(sp); + Splinter* s = d_slicer->getSplinter(sp); + Index cutPoint = s->getLow() + i; + Splinter* new_bottom = new Splinter(cutPoint, s->getLow()); + Splinter* new_top = new Splinter(s->getHigh(), cutPoint + 1); + new_bottom->setPointer(SplinterPointer(d_rootId, row, bottom->getLow())); + new_top->setPointer(SplinterPointer(d_rootId, row, top->getLow())); + + slice->addSplinter(new_bottom->getLow(), new_bottom); + slice->addSplinter(new_top->getLow(), new_top); + + bottom->setPointer(SplinterPointer(sp.term, sp.row, new_bottom->getLow())); + top->setPointer(SplinterPointer(sp.term, sp.row, new_top->getLow())); + // update base for block + d_slicer->getSliceBlock(sp)->sliceBaseAt(cutPoint); + // add to queue of blocks that have changed base + Debug("bv-slicer") << " adding block to queue: " << sp.term << endl; + queue.push_back(sp.term); + } + } + } + } + + Debug("bv-slicer") << "base computed: " << d_rootId << endl; + Debug("bv-slicer") << this->debugPrint() << endl; + Debug("bv-slicer") << "SliceBlock::computeBlockBase done. \n"; + +} + +std::string SliceBlock::debugPrint() { + std::ostringstream os; + os << "Width " << d_bitwidth << endl; + os << "Base " << d_base.debugPrint() << endl; + for (SliceBlock::const_iterator it = begin(); it!= end(); ++it) { + os << (*it)->debugPrint() << endl; + } + return os.str(); +} + +Slicer::Slicer() + : d_simpleEqualities(), + d_roots(), + d_numRoots(0), + d_nodeRootMap(), + d_rootBlocks(), + d_coreTermCache() +{} + +RootId Slicer::makeRoot(TNode n) { + Assert (n.getKind() != kind::BITVECTOR_EXTRACT && n.getKind() != kind::BITVECTOR_CONCAT); + if (d_nodeRootMap.find(n) != d_nodeRootMap.end()) { + return d_nodeRootMap[n]; + } + RootId id = d_roots.size(); + d_nodeRootMap[n] = id; + d_roots.push_back(n); + d_rootBlocks.push_back(new SliceBlock(id, utils::getSize(n), this)); + Assert (d_roots.size() == d_rootBlocks.size()); + + Debug("bv-slicer") << "Slicer::makeRoot " << n << " -> " << id << endl; + return id; +} + +void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) { + Assert (node.getKind() == kind::EQUAL); + TNode t1 = node[0]; + TNode t2 = node[1]; + + uint32_t width = utils::getSize(t1); + + Base base1(width); + if (t1.getKind() == kind::BITVECTOR_CONCAT) { + unsigned size = 0; + for (int i = t1.getNumChildren(); i >= 0; --i) { + size = size + utils::getSize(t1[i]); + base1.sliceAt(size); + } + } + + Base base2(width); + if (t2.getKind() == kind::BITVECTOR_CONCAT) { + unsigned size = 0; + for (int i = t2.getNumChildren(); i >= 0; --i) { + size = size + utils::getSize(t2[i]); + base2.sliceAt(size); + } + } + + base1.sliceWith(base2); + if (base1 != Base(width)) { + // we split the equalities according to the base + int last = 0; + for (unsigned i = 1; i < utils::getSize(t1); ++i) { + if (base1.isCutPoint(i)) { + Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, last, i - 1)); + Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, last, i - 1)); + last = i; + Assert (utils::getSize(extract1) == utils::getSize(extract2)); + equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); + } + } + } else { + // just return same equality + equalities.push_back(node); + } +} + +void Slicer::processEquality(TNode node) { + Assert (node.getKind() == kind::EQUAL); + Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl; + std::vector<Node> equalities; + splitEqualities(node, equalities); + for (unsigned i = 0; i < equalities.size(); ++i) { + Debug("bv-slicer") << " splitEqualities " << node << endl; + registerSimpleEquality(equalities[i]); + d_simpleEqualities.push_back(equalities[i]); + } +} + +void Slicer::registerSimpleEquality(TNode eq) { + Assert (eq.getKind() == kind::EQUAL); + Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl; + TNode a = eq[0]; + TNode b = eq[1]; + + RootId id_a = registerTerm(a); + RootId id_b = registerTerm(b); + + unsigned low_a = 0; + unsigned low_b = 0; + + if (a.getKind() == kind::BITVECTOR_EXTRACT) { + low_a = utils::getExtractLow(a); + } + + if (b.getKind() == kind::BITVECTOR_EXTRACT) { + low_b = utils::getExtractLow(b); + } + + if (id_a == id_b) { + // we are in the special case a[i0:j0] = a[i1:j1] + Index high_a = utils::getExtractHigh(a); + Index high_b = utils::getExtractHigh(b); + + unsigned intersection_low = std::max(low_a, low_b); + unsigned intersection_high = std::min(high_a, high_b); + if (intersection_low <= intersection_high) { + // if the two extracts intersect + unsigned intersection_size = intersection_high - intersection_low + 1; + // gcd between overlapping area and difference + unsigned diff = low_a > low_b ? low_a - low_b : low_b - low_a; + unsigned granularity = gcd(intersection_size, diff); + SliceBlock* block_a = d_rootBlocks[id_a]; + Assert (a.getKind() == kind::BITVECTOR_EXTRACT); + unsigned size = utils::getSize(a[0]); + + Slice* slice = new Slice(size); + unsigned low = low_a > low_b ? low_b : low_a; + unsigned high = high_a > high_b ? high_a : high_b; + Splinter* prev_splinter = NULL; + // the row the new slice will be in + unsigned block_row = block_a->getSize(); + for (unsigned i = low; i < high; i+=granularity) { + Splinter* s = new Splinter(i+ granularity-1, i); + slice->addSplinter(i, s); + // update splinter pointers to reflect entailed equalities + if (prev_splinter!= NULL) { + // the previous splinter will be equal to the current + prev_splinter->setPointer(SplinterPointer(id_a, block_row, i)); + } + prev_splinter = s; + } + // make sure to splinters for the extremities + if (low!= 0) { + Splinter* s = new Splinter(low -1 , 0); + slice->addSplinter(0, s); + } + if (high + granularity <= size) { + Splinter* s = new Splinter(size - 1, high + 1); + slice->addSplinter(high+1, s); + } + block_a->addSlice(slice); + return; + } + } + + Slice* slice_a = makeSlice(a); + Slice* slice_b = makeSlice(b); + + SliceBlock* block_a = d_rootBlocks[id_a]; + SliceBlock* block_b = d_rootBlocks[id_b]; + + uint32_t row_a = block_a->addSlice(slice_a); + uint32_t row_b = block_b->addSlice(slice_b); + + SplinterPointer sp_a = SplinterPointer(id_a, row_a, low_a); + SplinterPointer sp_b = SplinterPointer(id_b, row_b, low_b); + + slice_a->getSplinter(low_a)->setPointer(sp_b); + slice_b->getSplinter(low_b)->setPointer(sp_a); +} + +Slice* Slicer::makeSlice(TNode node) { + //Assert (d_sliceSet.find(node) == d_sliceSet.end()); + + Index bitwidth = utils::getSize(node); + Index low = 0; + Index high = bitwidth -1; + if (node.getKind() == kind::BITVECTOR_EXTRACT) { + low = utils::getExtractLow(node); + high = utils::getExtractHigh(node); + bitwidth = utils::getSize(node[0]); + } + Splinter* splinter = new Splinter(high, low); + Slice* slice = new Slice(bitwidth); + slice->addSplinter(low, splinter); + if (low != 0) { + Splinter* bottom_splinter = new Splinter(low-1, 0); + slice->addSplinter(0, bottom_splinter); + } + if (high != bitwidth - 1) { + Splinter* top_splinter = new Splinter(bitwidth - 1, high + 1); + slice->addSplinter(high+1, top_splinter); + } + return slice; +} + + +RootId Slicer::registerTerm(TNode node) { + if (node.getKind() == kind::BITVECTOR_EXTRACT ) { + node = node[0]; + Assert (isRootTerm(node)); + } + // setting up the data-structures for the root term + RootId id = makeRoot(node); + return id; +} + +bool Slicer::isCoreTerm(TNode node) { + if (d_coreTermCache.find(node) == d_coreTermCache.end()) { + Kind kind = node.getKind(); + if (kind != kind::BITVECTOR_EXTRACT && + kind != kind::BITVECTOR_CONCAT && + kind != kind::EQUAL && kind != kind::NOT) { + d_coreTermCache[node] = false; + return false; + } else { + // we need to recursively check whether the term is a root term or not + bool isCore = true; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + isCore = isCore && isCoreTerm(node[i]); + } + d_coreTermCache[node] = isCore; + return isCore; + } + } + return d_coreTermCache[node]; +} + +bool Slicer::isRootTerm(TNode node) { + Kind kind = node.getKind(); + return kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT; +} + +// Base Slicer::getBase(TNode node) { +// Assert (d_bases.find(node) != d_bases.end()); +// return d_bases[node]; +// } + +// void Slicer::updateBase(TNode node, const Base& base) { +// Assert (d_bases.find(node) != d_bases.end()); +// d_bases[node] = d_bases[node].bitwiseOr(base); +// } + + +void Slicer::computeCoarsestBase() { + Debug("bv-slicer") << "theory::bv::Slicer::computeCoarsestBase " << endl; + std::vector<RootId> queue; + for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { + SliceBlock* block = d_rootBlocks[i]; + block->computeBlockBase(queue); + } + + Debug("bv-slicer") << " processing queue of size " << queue.size() << endl; + while (!queue.empty()) { + // process split candidate + RootId current = queue.back(); + queue.pop_back(); + SliceBlock* block = d_rootBlocks[current]; + block->computeBlockBase(queue); + } + debugCheckBase(); +} + + +void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) { + TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; + Assert (isRootTerm(root)); + Base base = getSliceBlock(getRootId(root))->getBase(); + base.decomposeNode(node, decomp); +} + +void Slicer::debugCheckBase() { + // iterate through blocks and check that the block base is the same as each slice base + for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { + SliceBlock* block = d_rootBlocks[i]; + Base block_base = block->getBase(); + SliceBlock::const_iterator it = block->begin(); + for (; it != block->end(); ++it) { + Slice* slice = *it; + Base diff_points = slice->getBase().diffCutPoints(block_base); + Assert (diff_points == Base(block->getBitwidth())); + Slice::const_iterator slice_it = slice->begin(); + for (; slice_it!= slice->end(); ++slice_it) { + Splinter* splinter = (*slice_it).second; + const SplinterPointer& sp = splinter->getPointer(); + if (sp != Undefined) { + Splinter* other = getSplinter(sp); + Assert (splinter->getBitwidth() == other->getBitwidth()); + } + } + } + } +} + + + + + + diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h new file mode 100644 index 000000000..33bc26b5a --- /dev/null +++ b/src/theory/bv/slicer.h @@ -0,0 +1,373 @@ +/********************* */ +/*! \file slicer.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector theory. + ** + ** Bitvector theory. + **/ + +#include "cvc4_private.h" + +#include <vector> +#include <list> +#include <ext/hash_map> +#include "util/bitvector.h" +#include "expr/node.h" +#include "theory/bv/theory_bv_utils.h" +#ifndef __CVC4__THEORY__BV__SLICER_BV_H +#define __CVC4__THEORY__BV__SLICER_BV_H + + +namespace CVC4 { + +namespace theory { +namespace bv { + +typedef uint32_t RootId; +typedef uint32_t SplinterId; +typedef uint32_t Index; + +class Base { + uint32_t d_size; + CVC4::BitVector d_repr; +public: + Base(uint32_t size) + : d_size(size) { + Assert (size > 1); + d_repr = BitVector(size - 1, 0u); + } + + Base(const BitVector& repr) + : d_size(repr.getSize() + 1), + d_repr(repr) { + Assert (d_size > 1); + } + + /** + * Marks the base by adding a cut between index and index + 1 + * + * @param index + */ + void sliceAt(Index index) { + Assert (index < d_size - 1); + d_repr = d_repr.setBit(index); + } + + void sliceWith(const Base& other) { + Assert (d_size == other.d_size); + d_repr = d_repr | other.d_repr; + } + + void decomposeNode(TNode node, std::vector<Node>& decomp); + + bool isCutPoint(Index index) { + Assert (index < d_size); + // the last cut point is implicit + if (index == d_size - 1) + return true; + return d_repr.isBitSet(index); + } + + Base diffCutPoints(const Base& other) const { + return Base(other.d_repr ^ d_repr); + } + + bool operator==(const Base& other) const { + return d_repr == other.d_repr; + } + bool operator!=(const Base& other) const { + return !(*this == other); + } + std::string debugPrint() { + std::ostringstream os; + os << "["; + bool first = true; + for (Index i = 0; i < d_size - 1; ++i) { + if (isCutPoint(i)) { + if (first) + first = false; + else + os <<"| "; + + os << i ; + } + } + os << "]"; + return os.str(); + } + +}; + + +struct SplinterPointer { + RootId term; + uint32_t row; + Index index; + + SplinterPointer() + : term(-1), + row(-1), + index(-1) + {} + + SplinterPointer(RootId t, uint32_t r, Index i) + : term(t), + row(r), + index(i) + {} + + bool operator==(const SplinterPointer& other) const { + return term == other.term && index == other.index && row == other.row; + } + bool operator!=(const SplinterPointer& other) const { + return !(*this == other); + } + + std::string debugPrint() { + std::ostringstream os; + os << "(id" << term << ", row" << row <<", i" << index << ")"; + return os.str(); + } + +}; + +static const SplinterPointer Undefined = SplinterPointer(-1, -1, -1); + +class Splinter { + // start and end indices in slice + Index d_low; + Index d_high; + + // keeps track of splinter this splinter is equal to + // equal to Undefined if there is none + SplinterPointer d_pointer; + +public: + Splinter(uint32_t high, uint32_t low) : + d_low(low), + d_high(high), + d_pointer(Undefined) + { + Assert (high >= low); + } + + void setPointer(const SplinterPointer& pointer) { + Assert (d_pointer == Undefined); + d_pointer = pointer; + } + + const SplinterPointer& getPointer() const { + return d_pointer; + } + + Index getLow() const { return d_low; } + Index getHigh() const {return d_high; } + uint32_t getBitwidth() const { return d_high - d_low; } +}; + +class Slice { + uint32_t d_bitwidth; + // map from the beginning of a splinter to the actual splinter id + std::map<Index, Splinter*> d_splinters; + Base d_base; + +public: + Slice(uint32_t bitwidth) + : d_bitwidth(bitwidth), + d_splinters(), + d_base(bitwidth) + {} + /** + * Split the slice by adding a cut point between indices i and i+1 + * + * @param i index where to cut + * @param id the id of the root term this slice belongs to + * @param row the row of the SliceBlock this Slice belongs to + */ + void split(Index i, SplinterPointer& sp, Splinter*& low_splinter, Splinter*& top_splinter); + /** + * Add splinter sp at Index i. If a splinter already exists there + * replace it and free the memory it occupied. + * + * @param i index where splinter starts + * @param sp new splinter + */ + void addSplinter(Index i, Splinter* sp); + /** + * Return the splinter starting at Index start. + * + * @param start + * + * @return + */ + Splinter* getSplinter (Index start) { + Assert (d_splinters.find(start) != d_splinters.end()); + return d_splinters[start]; + } + const Base& getBase() const { return d_base; } + + typedef std::map<Index, Splinter*>::const_iterator const_iterator; + std::map<Index, Splinter*>::const_iterator begin() { + return d_splinters.begin(); + } + std::map<Index, Splinter*>::const_iterator end() { + return d_splinters.end(); + } + std::string debugPrint(); +}; + +class Slicer; + +class SliceBlock { + uint32_t d_bitwidth; + RootId d_rootId; /**< the id of the root term this block corresponds to */ + std::vector<Slice*> d_block; /**< the slices in the block */ + Base d_base; /**< the base corresponding to this block containing all the cut points. + Invariant: the base should contain all the cut-points in the slices*/ + Slicer* d_slicer; // FIXME: more elegant way to do this + +public: + + + SliceBlock(RootId rootId, uint32_t bitwidth, Slicer* slicer) + : d_bitwidth(bitwidth), + d_rootId(rootId), + d_block(), + d_base(bitwidth), + d_slicer(slicer) + {} + + uint32_t addSlice(Slice* slice) { + // update the base with the cut-points in the slice + Debug("bv-slice") << "SliceBlock::addSlice Block"<< d_rootId << " adding slice " << slice->debugPrint() << std::endl; + d_base.sliceWith(slice->getBase()); + d_block.push_back(slice); + return d_block.size() - 1; + } + + Slice* getSlice(uint32_t row) const { + Assert (row < d_block.size()); + return d_block[row]; + } + /** + * Propagate all the cut points in the Base to all the Slices. If one of the + * splinters that needs to get cut has a pointer to a splinter in a different + * block that splinter will also be split. + * + * @param queue other blocks that changed their base. + */ + void computeBlockBase(std::vector<RootId>& queue); + + void sliceBaseAt(Index i) { + d_base.sliceAt(i); + } + typedef std::vector<Slice*>::const_iterator const_iterator; + std::vector<Slice*>::const_iterator begin() { + return d_block.begin(); + } + std::vector<Slice*>::const_iterator end() { + return d_block.end(); + } + + uint32_t getBitwidth() const { + return d_bitwidth; + } + Base& getBase() { + return d_base; + } + + unsigned getSize() const { + return d_block.size(); + } + std::string debugPrint(); +}; + +typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> RootTermCache; + +typedef __gnu_cxx::hash_map<TNode, RootId, TNodeHashFunction> NodeRootIdMap; +typedef std::vector<TNode> Roots; + +typedef __gnu_cxx::hash_map<TNode, SplinterId, TNodeHashFunction> NodeSplinterIdMap; +typedef std::vector<Splinter*> Splinters; + +typedef std::vector<SliceBlock*> SliceBlocks; + +class Slicer { + std::vector<TNode> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */ + Roots d_roots; + uint32_t d_numRoots; + NodeRootIdMap d_nodeRootMap; + /* Indexed by Root Id */ + SliceBlocks d_rootBlocks; + RootTermCache d_coreTermCache; +public: + Slicer(); + void computeCoarsestBase(); + /** + * Takes an equality that is of the following form: + * a1 a2 ... an = b1 b2 ... bk + * where ai, and bi are either variables or extracts over variables, + * and consecutive extracts have been merged. + * + * @param node + */ + void processEquality(TNode node); + bool isCoreTerm(TNode node); +private: + void registerSimpleEquality(TNode node); + void splitEqualities(TNode node, std::vector<Node>& equalities); + TNode addSimpleTerm(TNode t); + bool isRootTerm(TNode node); + + TNode getRoot(RootId id) {return d_roots[id]; } + + RootId getRootId(TNode node) { + Assert (d_nodeRootMap.find(node) != d_nodeRootMap.end()); + return d_nodeRootMap[node]; + } + + RootId registerTerm(TNode node); + RootId makeRoot(TNode n); + Slice* makeSlice(TNode node); + + void debugCheckBase(); +public: + Slice* getSlice(const SplinterPointer& sp) { + Assert (sp != Undefined); + SliceBlock* sb = d_rootBlocks[sp.term]; + return sb->getSlice(sp.row); + } + + Splinter* getSplinter(const SplinterPointer& sp) { + Slice* slice = getSlice(sp); + return slice->getSplinter(sp.index); + } + + SliceBlock* getSliceBlock(RootId id) { + Assert (id < d_rootBlocks.size()); + return d_rootBlocks[id]; + } + + SliceBlock* getSliceBlock(const SplinterPointer& sp) { + return getSliceBlock(sp.term); + } + + void getBaseDecomposition(TNode node, std::vector<Node>& decomp); + +}; /* Slicer class */ + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BV__SLICER_BV_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7acb93cc2..c4e16545f 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,6 +17,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/bv/slicer.h" #include "theory/valuation.h" #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" @@ -39,8 +40,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), + d_slicer(), d_bitblastSolver(c, this), - d_equalitySolver(c, this), + d_coreSolver(c, this, &d_slicer), d_statistics(), d_conflict(c, false), d_literalsToPropagate(c), @@ -52,7 +54,7 @@ TheoryBV::~TheoryBV() {} void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalitySolver.setMasterEqualityEngine(eq); + d_coreSolver.setMasterEqualityEngine(eq); } TheoryBV::Statistics::Statistics(): @@ -72,15 +74,19 @@ TheoryBV::Statistics::~Statistics() { } void TheoryBV::preRegisterTerm(TNode node) { - BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; + Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; if (options::bitvectorEagerBitblast()) { // don't use the equality engine in the eager bit-blasting return; } + if (node.getKind() == kind::EQUAL) { + d_slicer.processEquality(node); + } + d_bitblastSolver.preRegister(node); - d_equalitySolver.preRegister(node); + d_coreSolver.preRegister(node); } void TheoryBV::sendConflict() { @@ -88,7 +94,7 @@ void TheoryBV::sendConflict() { if (d_conflictNode.isNull()) { return; } else { - BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); d_conflictNode = Node::null(); @@ -97,7 +103,7 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; // if we are already in conflict just return the conflict if (inConflict()) { @@ -111,17 +117,20 @@ void TheoryBV::check(Effort e) Assertion assertion = get(); TNode fact = assertion.assertion; new_assertions.push_back(fact); - BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; + Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; } if (!inConflict()) { // sending assertions to the equality solver first - d_equalitySolver.addAssertions(new_assertions, e); + d_coreSolver.addAssertions(new_assertions, e); } - if (!inConflict()) { - // sending assertions to the bitblast solver - d_bitblastSolver.addAssertions(new_assertions, e); + // FIXME: this is not quite correct as it does not take into account cardinality constraints + if (!d_coreSolver.isCoreTheory()) { + if (!inConflict()) { + // sending assertions to the bitblast solver + d_bitblastSolver.addAssertions(new_assertions, e); + } } if (inConflict()) { @@ -132,13 +141,13 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); // Assert (fullModel); // can only query full model - d_equalitySolver.collectModelInfo(m); + d_coreSolver.collectModelInfo(m); d_bitblastSolver.collectModelInfo(m); } void TheoryBV::propagate(Effort e) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; + Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; if (inConflict()) { return; @@ -152,7 +161,7 @@ void TheoryBV::propagate(Effort e) { } if (!ok) { - BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl; + Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl; setConflict(); } } @@ -184,7 +193,6 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu return PP_ASSERT_STATUS_UNSOLVED; } - Node TheoryBV::ppRewrite(TNode t) { if (RewriteRule<BitwiseEq>::applies(t)) { @@ -194,6 +202,10 @@ Node TheoryBV::ppRewrite(TNode t) return t; } +void TheoryBV::presolve() { + Debug("bitvector") << "TheoryBV::presolve" << endl; + d_slicer.computeCoarsestBase(); +} bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { @@ -224,7 +236,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain // * equality engine can propagate eagerly bool ok = true; - if (subtheory == SUB_EQUALITY) { + if (subtheory == SUB_CORE) { d_out->propagate(literal); if (!ok) { setConflict(); @@ -239,19 +251,19 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { // Ask the appropriate subtheory for the explanation - if (propagatedBy(literal, SUB_EQUALITY)) { - BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; - d_equalitySolver.explain(literal, assumptions); + if (propagatedBy(literal, SUB_CORE)) { + Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; + d_coreSolver.explain(literal, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLAST)); - BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; + Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; d_bitblastSolver.explain(literal, assumptions); } } Node TheoryBV::explain(TNode node) { - BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; + Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; // Ask for the explanation @@ -271,18 +283,19 @@ void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { - d_equalitySolver.addSharedTerm(t); + d_coreSolver.addSharedTerm(t); } } + EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { if (options::bitvectorEagerBitblast()) { return EQUALITY_UNKNOWN; } - EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b); + EqualityStatus status = d_coreSolver.getEqualityStatus(a, b); if (status == EQUALITY_UNKNOWN) { status = d_bitblastSolver.getEqualityStatus(a, b); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e38f3568c..c16e854cc 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -28,7 +28,9 @@ #include "context/cdqueue.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/bv_subtheory_eq.h" +#include "theory/bv/bv_subtheory_core.h" #include "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/slicer.h" namespace CVC4 { namespace theory { @@ -43,8 +45,11 @@ class TheoryBV : public Theory { context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; + Slicer d_slicer; + BitblastSolver d_bitblastSolver; - EqualitySolver d_equalitySolver; + CoreSolver d_coreSolver; + public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); @@ -67,6 +72,7 @@ public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); Node ppRewrite(TNode t); + void presolve(); private: class Statistics { @@ -137,6 +143,7 @@ private: friend class Bitblaster; friend class BitblastSolver; friend class EqualitySolver; + friend class CoreSolver; };/* class TheoryBV */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2c178ec2e..5df632ff4 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -178,6 +178,17 @@ public: Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } + + BitVector setBit(uint32_t i) const { + CheckArgument(i < d_size, i); + Integer res = d_value.setBit(i); + return BitVector(d_size, res); + } + + bool isBitSet(uint32_t i) const { + CheckArgument(i < d_size, i); + return d_value.isBitSet(i); + } BitVector unsignedDiv (const BitVector& y) const { CheckArgument(d_size == y.d_size, y); diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 211c40741..e2a8f4a62 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -218,6 +218,16 @@ public: return Integer( d_value << ipow); } + bool isBitSet(uint32_t i) const { + return !extractBitRange(1, i).isZero(); + } + + Integer setBit(uint32_t i) const { + cln::cl_I mask(1); + mask = mask << i; + return Integer(cln::logior(d_value, mask)); + } + Integer oneExtend(uint32_t size, uint32_t amount) const { DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); cln::cl_byte range(amount, size); diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index bebd0e1e2..d6882b6ac 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -137,6 +137,7 @@ public: return *this; } + Integer bitwiseOr(const Integer& y) const { mpz_class result; mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); @@ -170,6 +171,24 @@ public: return Integer( result ); } + /** + * Returns the Integer obtained by setting the ith bit of the + * current Integer to 1. + * + * @param bit + * + * @return + */ + Integer setBit(uint32_t i) const { + mpz_class res = d_value; + mpz_setbit(res.get_mpz_t(), i); + return Integer(res); + } + + bool isBitSet(uint32_t i) const { + return !extractBitRange(1, i).isZero(); + } + /** * Returns the integer with the binary representation of size bits * extended with amount 1's diff --git a/src/util/utility.h b/src/util/utility.h index 5ce185b5b..72213764f 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -67,6 +67,15 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre return (match2 == last) ? match : last; } +template <class T> +inline T gcd(T a, T b) { + while (b != 0) { + a = b; + b = a % b; + } + return a; +} + }/* CVC4 namespace */ |