From 25ac2c8f4b45e2b299895e97a30790fbf46cf79f Mon Sep 17 00:00:00 2001 From: lianah Date: Sat, 16 Mar 2013 15:48:51 -0400 Subject: [PATCH] started work on the inequality bv subtheory --- src/theory/bv/bv_inequality_graph.h | 54 ++++ src/theory/bv/bv_subtheory.h | 12 +- src/theory/bv/bv_subtheory_core.cpp | 90 ++++--- src/theory/bv/bv_subtheory_core.h | 21 +- src/theory/bv/bv_subtheory_eq.cpp | 185 ------------- src/theory/bv/bv_subtheory_eq.h | 90 ------- src/theory/bv/bv_subtheory_inequality.cpp | 38 +++ src/theory/bv/bv_subtheory_inequality.h | 50 ++++ src/theory/bv/slicer.cpp | 250 +++++++++++++++--- src/theory/bv/slicer.h | 176 +++++++----- src/theory/bv/theory_bv.cpp | 8 +- src/theory/bv/theory_bv.h | 2 +- test/regress/regress0/bv/core/incremental.smt | 24 ++ 13 files changed, 542 insertions(+), 458 deletions(-) create mode 100644 src/theory/bv/bv_inequality_graph.h delete mode 100644 src/theory/bv/bv_subtheory_eq.cpp delete mode 100644 src/theory/bv/bv_subtheory_eq.h create mode 100644 src/theory/bv/bv_subtheory_inequality.cpp create mode 100644 src/theory/bv/bv_subtheory_inequality.h create mode 100644 test/regress/regress0/bv/core/incremental.smt diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h new file mode 100644 index 000000000..2ac22bb5b --- /dev/null +++ b/src/theory/bv/bv_inequality_graph.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file bv_inequality_graph.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-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 "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H +#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H + +#include "context/context.h" +#include "context/cdqueue.h" +#include "theory/uf/equality_engine.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { + + +namespace bv { + +typedef unsigned TermId; +typedef unsigned ReasonId; + +class InequalityGraph { + context::Context d_context; + +public: + + InequalityGraph(context::Context* c) + : d_context(c) + {} + bool addInequality(TermId a, TermId b, ReasonId reason); + bool propagate(); + bool areLessThan(TermId a, TermId b); + void getConflict(std::vector& conflict); +}; + +} +} +} + +#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */ diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index d95aaa873..9e7566ebb 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -32,9 +32,9 @@ class TheoryModel; namespace bv { enum SubTheory { - SUB_EQUALITY = 1, + SUB_CORE = 1, SUB_BITBLAST = 2, - SUB_CORE = 3 + SUB_INEQUALITY = 3 }; inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { @@ -42,9 +42,11 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { case SUB_BITBLAST: out << "BITBLASTER"; break; - case SUB_EQUALITY: - out << "EQUALITY"; + case SUB_CORE: + out << "BV_CORE_SUBTHEORY"; break; + case SUB_INEQUALITY: + out << "BV_INEQUALITY_SUBTHEORY"; default: Unreachable(); break; @@ -83,10 +85,10 @@ public: d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} - virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector& assumptions) = 0; virtual void preRegister(TNode node) {} + virtual void propagate(Effort e) {} virtual void collectModelInfo(TheoryModel* m) = 0; bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 2e1320d1a..f1255e07c 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -14,7 +14,7 @@ ** Algebraic solver. **/ -#include "theory/bv/bv_subtheory_eq.h" +#include "theory/bv/bv_subtheory_core.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" @@ -28,16 +28,13 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; -CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer) +CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_notify(*this), d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), d_assertions(c), - d_normalFormCache(), - d_slicer(slicer), - d_isCoreTheory(c, true), - d_baseChanged(false), - d_checkCalled(false) + d_slicer(new Slicer(c, this)), + d_isCoreTheory(c, true) { if (d_useEqualityEngine) { @@ -85,7 +82,7 @@ void CoreSolver::preRegister(TNode node) { if (node.getKind() == kind::EQUAL) { d_equalityEngine.addTriggerEquality(node); - d_slicer->processEquality(node); + // d_slicer->processEquality(node); } else { d_equalityEngine.addTerm(node); } @@ -102,14 +99,9 @@ void CoreSolver::explain(TNode literal, std::vector& assumptions) { } } -Node CoreSolver::getBaseDecomposition(TNode a) { +Node CoreSolver::getBaseDecomposition(TNode a, std::vector& explanation) { std::vector a_decomp; - // FIXME: hack to do bitwise decomposition - // for (int i = utils::getSize(a) - 1; i>= 0; --i) { - // Node bit = Rewriter::rewrite(utils::mkExtract(a, i, i)); - // a_decomp.push_back(bit); - // } - d_slicer->getBaseDecomposition(a, a_decomp); + d_slicer->getBaseDecomposition(a, a_decomp, explanation); Node new_a = utils::mkConcat(a_decomp); return new_a; } @@ -120,50 +112,56 @@ bool CoreSolver::decomposeFact(TNode fact) { // 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]; + if (fact.getKind() == kind::EQUAL) { + TNode a = fact[0]; + TNode b = fact[1]; - // d_slicer->processEquality(eq); - - Node new_a = getBaseDecomposition(a); - Node new_b = getBaseDecomposition(b); - - Assert (utils::getSize(new_a) == utils::getSize(new_b) && - utils::getSize(new_a) == utils::getSize(a)); - - 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); + d_slicer->processEquality(fact); + std::vector explanation; + Node new_a = getBaseDecomposition(a, explanation); + Node new_b = getBaseDecomposition(b, explanation); - bool ok = true; - ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue()); - if (!ok) return false; - ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue()); - if (!ok) return false; - ok = assertFactToEqualityEngine(fact, fact); - if (!ok) return false; + explanation.push_back(fact); + TNode reason = utils::mkAnd(explanation); - if (fact.getKind() == kind::EQUAL) { + Assert (utils::getSize(new_a) == utils::getSize(new_b) && + utils::getSize(new_a) == utils::getSize(a)); + // FIXME: do we still need to assert these? + 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 = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue()); + if (!ok) return false; + ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue()); + if (!ok) return false; // assert the individual equalities as well // a_i == b_i if (new_a.getKind() == kind::BITVECTOR_CONCAT && new_b.getKind() == kind::BITVECTOR_CONCAT) { - Assert (new_a.getNumChildren() == new_b.getNumChildren()); for (unsigned i = 0; i < new_a.getNumChildren(); ++i) { Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]); - ok = assertFactToEqualityEngine(eq_i, fact); + ok = assertFactToEqualityEngine(eq_i, reason); if (!ok) return false; } } + // merge the two terms in the slicer as well + d_slicer->assertEquality(fact); + } else { + // still need to register the terms + TNode a = fact[0][0]; + TNode b = fact[0][1]; + d_slicer->registerTerm(a); + d_slicer->registerTerm(b); } - return true; + // finally assert the actual fact to the equality engine + return assertFactToEqualityEngine(fact, fact); } bool CoreSolver::check(Theory::Effort e) { - d_checkCalled = true; Trace("bitvector::core") << "CoreSolver::check \n"; Assert (!d_bv->inConflict()); @@ -179,7 +177,6 @@ bool CoreSolver::check(Theory::Effort e) { // only reason about equalities if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) { - TNode eq = fact.getKind() == kind::EQUAL ? fact : fact[0]; ok = decomposeFact(fact); } else { ok = assertFactToEqualityEngine(fact, fact); @@ -188,6 +185,14 @@ bool CoreSolver::check(Theory::Effort e) { return false; } + // make sure to assert the new splits + std::vector new_splits; + d_slicer->getNewSplits(new_splits); + for (unsigned i = 0; i < new_splits.size(); ++i) { + ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue()); + if (!ok) + return false; + } return true; } @@ -197,7 +202,6 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // 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) { diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index d5235a864..230817e13 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -31,14 +31,7 @@ class Base; */ 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; @@ -52,12 +45,12 @@ class CoreSolver : public SubtheorySolver { 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; @@ -69,17 +62,14 @@ class CoreSolver : public SubtheorySolver { /** FIXME: for debugging purposes only */ context::CDList d_assertions; - __gnu_cxx::hash_map d_normalFormCache; Slicer* d_slicer; context::CDO d_isCoreTheory; bool assertFactToEqualityEngine(TNode fact, TNode reason); bool decomposeFact(TNode fact); - Node getBaseDecomposition(TNode a); - bool d_baseChanged; - bool d_checkCalled; -public: - CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer); + Node getBaseDecomposition(TNode a, std::vector& explanation); +public: + CoreSolver(context::Context* c, TheoryBV* bv); bool isCoreTheory() { return d_isCoreTheory; } void setMasterEqualityEngine(eq::EqualityEngine* eq); void preRegister(TNode node); @@ -100,6 +90,7 @@ public: } return EQUALITY_UNKNOWN; } + bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); } }; diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp deleted file mode 100644 index f11b1252b..000000000 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ /dev/null @@ -1,185 +0,0 @@ -/********************* */ -/*! \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/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; - -EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), - d_assertions(c) -{ - 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 EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalityEngine.setMasterEqualityEngine(eq); -} - -void EqualitySolver::preRegister(TNode node) { - if (!d_useEqualityEngine) - return; - - if (node.getKind() == kind::EQUAL) { - d_equalityEngine.addTriggerEquality(node); - } else { - d_equalityEngine.addTerm(node); - } -} - -void EqualitySolver::explain(TNode literal, std::vector& 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 EqualitySolver::addAssertions(const std::vector& assertions, Theory::Effort e) { - Trace("bitvector::equality") << "EqualitySolver::addAssertions \n"; - Assert (!d_bv->inConflict()); - - for (unsigned i = 0; i < assertions.size(); ++i) { - TNode fact = assertions[i]; - - // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) { - Trace("bitvector::equality") << " (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, fact); - } else { - // equality - d_equalityEngine.assertEquality(predicate, true, fact); - } - } else { - // Adding predicate if the congruence over it is turned on - if (d_equalityEngine.isFunctionKind(predicate.getKind())) { - d_equalityEngine.assertPredicate(predicate, !negated, fact); - } - } - } - - // checking for a conflict - if (d_bv->inConflict()) { - return false; - } - } - - return true; -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_solver.storePropagation(equality); - } else { - return d_solver.storePropagation(equality.notNode()); - } -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; - if (value) { - return d_solver.storePropagation(predicate); - } else { - return d_solver.storePropagation(predicate.notNode()); - } -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("bitvector::equality") << "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 EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - d_solver.conflict(t1, t2); -} - -bool EqualitySolver::storePropagation(TNode literal) { - return d_bv->storePropagation(literal, SUB_EQUALITY); -} - -void EqualitySolver::conflict(TNode a, TNode b) { - std::vector assumptions; - d_equalityEngine.explainEquality(a, b, true, assumptions); - d_bv->setConflict(mkAnd(assumptions)); -} - -void EqualitySolver::collectModelInfo(TheoryModel* m) { - if (Debug.isOn("bitvector-model")) { - context::CDList::const_iterator it = d_assertions.begin(); - for (; it!= d_assertions.end(); ++it) { - Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert " - << *it << ")\n"; - } - } - set termSet; - d_bv->computeRelevantTerms(termSet); - m->assertEqualityEngine(&d_equalityEngine, &termSet); -} diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h deleted file mode 100644 index 2b024cfd4..000000000 --- a/src/theory/bv/bv_subtheory_eq.h +++ /dev/null @@ -1,90 +0,0 @@ -/********************* */ -/*! \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" - -namespace CVC4 { -namespace theory { -namespace bv { - -/** - * Bitvector equality solver - */ -class EqualitySolver : public SubtheorySolver { - - // NotifyClass: handles call-back from congruence closure module - - class NotifyClass : public eq::EqualityEngineNotify { - EqualitySolver& d_solver; - - public: - NotifyClass(EqualitySolver& 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 d_assertions; -public: - - EqualitySolver(context::Context* c, TheoryBV* bv); - void setMasterEqualityEngine(eq::EqualityEngine* eq); - void preRegister(TNode node); - bool addAssertions(const std::vector& assertions, Theory::Effort e); - void explain(TNode literal, std::vector& 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/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp new file mode 100644 index 000000000..7ccef5ff1 --- /dev/null +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \file bv_subtheory_inequality.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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_inequality.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.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; + +bool InequalitySolver::check(Theory::Effort e) { + +} +void InequalitySolver::explain(TNode literal, std::vector& assumptions) { + +} + +bool InequalitySolver::propagate(Theory::Effort e) { + +} diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h new file mode 100644 index 000000000..63f9af9e4 --- /dev/null +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file bv_subtheory_inequality.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-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 "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H +#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H + +#include "context/context.h" +#include "context/cdqueue.h" +#include "theory/uf/equality_engine.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { + + +namespace bv { + +class InequalitySolver { + +public: + + InequalitySolver(context::Context* c, TheoryBV* bv) + : SubtheorySolver(c, bv) + {} + + bool check(Theory::Effort e); + void propagate(Effort e); + void explain(TNode literal, std::vector& assumptions); +}; + +} +} +} + +#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index ac668ab20..92166224b 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -19,7 +19,7 @@ #include "theory/bv/slicer.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" - +#include "theory/bv/bv_subtheory_core.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -159,7 +159,7 @@ std::string NormalForm::debugPrint(const UnionFind& uf) const { std::string UnionFind::Node::debugPrint() const { ostringstream os; - os << "Repr " << d_repr << " ["<< d_bitwidth << "] "; + os << "Repr " << d_edge.repr << " ["<< d_bitwidth << "] "; os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; return os.str(); } @@ -169,27 +169,44 @@ std::string UnionFind::Node::debugPrint() const { * UnionFind * */ -TermId UnionFind::addTerm(Index bitwidth) { +TermId UnionFind::addNode(Index bitwidth) { + Assert (bitwidth > 0); Node node(bitwidth); d_nodes.push_back(node); + ++(d_statistics.d_numNodes); TermId id = d_nodes.size() - 1; // d_representatives.insert(id); ++(d_statistics.d_numRepresentatives); - Debug("bv-slicer-uf") << "UnionFind::addTerm " << id << " size " << bitwidth << endl; return id; } + +TermId UnionFind::addExtract(TermId topLevel, Index high, Index low) { + ExtractTerm extract(topLevel, high, low); + if (d_extractToId.find(extract) != d_extractToId.end()) { + return d_extractToId[extract]; + } + + Assert (high >= low); + + TermId id = addNode(high - low + 1); + d_idToExtract[id] = extract; + d_extractToId[extract] = id; + return id; +} + /** * At this point we assume the slicings of the two terms are properly aligned. * * @param t1 * @param t2 */ -void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) { +void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2, TermId reason) { Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n" - << " " << t2.debugPrint() << endl; + << " " << t2.debugPrint() << "\n" + << " with reason " << reason << endl; Assert (t1.getBitwidth() == t2.getBitwidth()); NormalForm nf1(t1.getBitwidth()); @@ -202,10 +219,11 @@ void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) { Assert (nf1.base == nf2.base); for (unsigned i = 0; i < nf1.decomp.size(); ++i) { - merge (nf1.decomp[i], nf2.decomp[i]); + merge (nf1.decomp[i], nf2.decomp[i], reason); } } + /** * Merge the two terms in the union find. Both t1 and t2 * should be root terms. @@ -213,7 +231,7 @@ void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) { * @param t1 * @param t2 */ -void UnionFind::merge(TermId t1, TermId t2) { +void UnionFind::merge(TermId t1, TermId t2, TermId reason) { Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl; ++(d_statistics.d_numMerges); t1 = find(t1); @@ -223,7 +241,7 @@ void UnionFind::merge(TermId t1, TermId t2) { return; Assert (! hasChildren(t1) && ! hasChildren(t2)); - setRepr(t1, t2); + setRepr(t1, t2, reason); recordOperation(UnionFind::MERGE, t1); //d_representatives.erase(t1); d_statistics.d_numRepresentatives += -1; @@ -233,11 +251,26 @@ TermId UnionFind::find(TermId id) { TermId repr = getRepr(id); if (repr != UndefinedId) { TermId find_id = find(repr); - // setRepr(id, find_id); return find_id; } return id; } + +TermId UnionFind::findWithExplanation(TermId id, std::vector& explanation) { + TermId repr = getRepr(id); + + if (repr != UndefinedId) { + TermId reason = getReason(id); + Assert (reason != UndefinedId); + explanation.push_back(reason); + + TermId find_id = findWithExplanation(repr, explanation); + return find_id; + } + return id; +} + + /** * Splits the representative of the term between i-1 and i * @@ -259,10 +292,14 @@ void UnionFind::split(TermId id, Index i) { Assert (i < getBitwidth(id)); if (!hasChildren(id)) { // first time we split this term - TermId bottom_id = addTerm(i); - TermId top_id = addTerm(getBitwidth(id) - i); + TermId bottom_id = addExtract(getTopLevel(id), i - 1, 0); + TermId top_id = addExtract(getTopLevel(id), getBitwidth(id) - 1, i); setChildren(id, top_id, bottom_id); - recordOperation(UnionFind::SPLIT, id); + recordOperation(UnionFind::SPLIT, id); + + if (d_slicer->termInEqualityEngine(id)) { + d_slicer->enqueueSplit(id, i); + } } else { Index cut = getCutPoint(id); if (i < cut ) @@ -273,6 +310,14 @@ void UnionFind::split(TermId id, Index i) { ++(d_statistics.d_numSplits); } +TermId UnionFind::getTopLevel(TermId id) const { + __gnu_cxx::hash_map >::const_iterator it = d_idToExtract.find(id); + if (it != d_idToExtract.end()) { + return (*it).second.id; + } + return id; +} + void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) { nf.clear(); getDecomposition(term, nf.decomp); @@ -319,6 +364,56 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) getDecomposition(high_child, decomp); } } + +void UnionFind::getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf, + std::vector& explanation) { + nf.clear(); + getDecompositionWithExplanation(term, nf.decomp, explanation); + // update nf base + Index count = 0; + for (unsigned i = 0; i < nf.decomp.size(); ++i) { + count += getBitwidth(nf.decomp[i]); + nf.base.sliceAt(count); + } + Debug("bv-slicer-uf") << "UnionFind::getNormalFrom term: " << term.debugPrint() << endl; + Debug("bv-slicer-uf") << " nf: " << nf.debugPrint(*this) << endl; +} + +void UnionFind::getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp, + std::vector& explanation) { + // making sure the term is aligned + TermId id = findWithExplanation(term.id, explanation); + + Assert (term.high < getBitwidth(id)); + // because we split the node, this must be the whole extract + if (!hasChildren(id)) { + Assert (term.high == getBitwidth(id) - 1 && + term.low == 0); + decomp.push_back(id); + return; + } + + Index cut = getCutPoint(id); + + if (term.low < cut && term.high < cut) { + // the extract falls entirely on the low child + ExtractTerm child_ex(getChild(id, 0), term.high, term.low); + getDecompositionWithExplanation(child_ex, decomp, explanation); + } + else if (term.low >= cut && term.high >= cut){ + // the extract falls entirely on the high child + ExtractTerm child_ex(getChild(id, 1), term.high - cut, term.low - cut); + getDecompositionWithExplanation(child_ex, decomp, explanation); + } + else { + // the extract is split over the two children + ExtractTerm low_child(getChild(id, 0), cut - 1, term.low); + getDecompositionWithExplanation(low_child, decomp, explanation); + ExtractTerm high_child(getChild(id, 1), term.high - cut, 0); + getDecompositionWithExplanation(high_child, decomp, explanation); + } +} + /** * May cause reslicings of the decompositions. Must not assume the decompositons * are the current normal form. @@ -428,7 +523,7 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) { void UnionFind::backtrack() { return; int size = d_undoStack.size(); - for (int i = size; i > d_undoStackIndex.get(); --i) { + for (int i = size; i > (int)d_undoStackIndex.get(); --i) { Operation op = d_undoStack.back(); Assert (!d_undoStack.empty()); d_undoStack.pop_back(); @@ -443,8 +538,8 @@ void UnionFind::backtrack() { void UnionFind::undoMerge(TermId id) { TermId repr = getRepr(id); - Assert (repr != id); - setRepr(id, UndefinedId); + Assert (repr != UndefinedId); + setRepr(id, UndefinedId, UndefinedId); } void UnionFind::undoSplit(TermId id) { @@ -453,9 +548,6 @@ void UnionFind::undoSplit(TermId id) { } void UnionFind::recordOperation(OperationKind op, TermId term) { - if (op == SPLIT) { - d_newSplit = true; - } d_undoStackIndex.set(d_undoStackIndex.get() + 1); d_undoStack.push_back(Operation(op, term)); Assert (d_undoStack.size() == d_undoStackIndex); @@ -488,7 +580,7 @@ ExtractTerm Slicer::registerTerm(TNode node) { low = utils::getExtractLow(node); } if (d_nodeToId.find(n) == d_nodeToId.end()) { - TermId id = d_unionFind.addTerm(utils::getSize(n)); + TermId id = d_unionFind.addNode(utils::getSize(n)); d_nodeToId[n] = id; d_idToNode[id] = n; } @@ -500,7 +592,8 @@ ExtractTerm Slicer::registerTerm(TNode node) { void Slicer::processEquality(TNode eq) { Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl; - + + registerEquality(eq); Assert (eq.getKind() == kind::EQUAL); TNode a = eq[0]; TNode b = eq[1]; @@ -511,13 +604,35 @@ void Slicer::processEquality(TNode eq) { d_unionFind.ensureSlicing(b_ex); d_unionFind.alignSlicings(a_ex, b_ex); - d_unionFind.unionTerms(a_ex, b_ex); + Debug("bv-slicer") << "Base of " << a_ex.id <<" " << d_unionFind.debugPrint(a_ex.id) << endl; Debug("bv-slicer") << "Base of " << b_ex.id <<" " << d_unionFind.debugPrint(b_ex.id) << endl; Debug("bv-slicer") << "Slicer::processEquality done. " << endl; } -void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { +void Slicer::assertEquality(TNode eq) { + Assert (eq.getKind() == kind::EQUAL); + ExtractTerm a = registerTerm(eq[0]); + ExtractTerm b = registerTerm(eq[1]); + ExplanationId reason = getExplanationId(eq); + d_unionFind.unionTerms(a, b, reason); +} + +TermId Slicer::getId(TNode node) const { + __gnu_cxx::hash_map::const_iterator it = d_nodeToId.find(node); + Assert (it != d_nodeToId.end()); + return it->second; +} + +void Slicer::registerEquality(TNode eq) { + if (d_explanationToId.find(eq) == d_explanationToId.end()) { + ExplanationId id = d_explanations.size(); + d_explanations.push_back(eq); + d_explanationToId[eq] = id; + } +} + +void Slicer::getBaseDecomposition(TNode node, std::vector& decomp, std::vector& explanation) { Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl; Index high = utils::getSize(node) - 1; @@ -528,10 +643,18 @@ void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { low = utils::getExtractLow(node); top = node[0]; } + Assert (d_nodeToId.find(top) != d_nodeToId.end()); TermId id = d_nodeToId[top]; - NormalForm nf(high-low+1); - d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf); + NormalForm nf(high-low+1); + std::vector explanation_ids; + d_unionFind.getNormalFormWithExplanation(ExtractTerm(id, high, low), nf, explanation_ids); + + for (unsigned i = 0; i < explanation_ids.size(); ++i) { + Assert (hasExplanation(explanation_ids[i])); + TNode exp = getExplanation(explanation_ids[i]); + explanation.push_back(exp); + } // construct actual extract nodes Index current_low = 0; @@ -622,25 +745,68 @@ void Slicer::splitEqualities(TNode node, std::vector& equalities) { d_numAddedEqualities += equalities.size() - 1; } -/** - * Returns the base decomposition of the current term. - * - * @param id - * - * @return - */ -Base Slicer::getTopLevelBase(TNode node) { - if (node.getKind() == kind::BITVECTOR_EXTRACT) { - node = node[0]; + +ExtractTerm UnionFind::getExtractTerm(TermId id) const { + Assert (isExtractTerm(id)); + + return (d_idToExtract.find(id))->second; +} + +bool UnionFind::isExtractTerm(TermId id) const { + return d_idToExtract.find(id) != d_idToExtract.end(); +} + +bool Slicer::hasNode(TermId id) const { + return d_idToNode.find(id) != d_idToNode.end(); +} + +Node Slicer::getNode(TermId id) const { + // if it was an extract + if (d_unionFind.isExtractTerm(id)) { + ExtractTerm extract = d_unionFind.getExtractTerm(id); + Assert (hasNode(extract.id)); + TNode node = d_idToNode.find(extract.id)->second; + Node ex = utils::mkExtract(node, extract.high, extract.low); + return ex; } - // if we haven't seen this node before it must not be sliced yet - if (d_nodeToId.find(node) == d_nodeToId.end()) { - return Base(utils::getSize(node)); + // otherwise must be a top-level term + Assert (hasNode(id)); + return (d_idToNode.find(id))->second; +} + +bool Slicer::termInEqualityEngine(TermId id) { + Node node = getNode(id); + return d_coreSolver->hasTerm(node); +} + +void Slicer::enqueueSplit(TermId id, Index i) { + Node node = getNode(id); + Node bottom = Rewriter::rewrite(utils::mkExtract(node, i -1 , 0)); + Node top = Rewriter::rewrite(utils::mkExtract(node, utils::getSize(node) - 1, i)); + Node eq = utils::mkNode(kind::EQUAL, node, utils::mkConcat(top, bottom)); + d_newSplits.push_back(eq); + Debug("bv-slicer") << "Slicer::enqueueSplit " << eq << endl; +} + +void Slicer::getNewSplits(std::vector& splits) { + for (unsigned i = d_newSplitsIndex; i < d_newSplits.size(); ++i) { + splits.push_back(d_newSplits[i]); } - TermId id = d_nodeToId[node]; - Base base(d_unionFind.getBitwidth(id)); - d_unionFind.getBase(id, base, 0); - return base; + d_newSplitsIndex = d_newSplits.size(); +} + +bool Slicer::hasExplanation(ExplanationId id) const { + return id < d_explanations.size(); +} + +TNode Slicer::getExplanation(ExplanationId id) const { + Assert(hasExplanation(id)); + return d_explanations[id]; +} + +ExplanationId Slicer::getExplanationId(TNode reason) const { + Assert (d_explanationToId.find(reason) != d_explanationToId.end()); + return d_explanationToId.find(reason)->second; } std::string UnionFind::debugPrint(TermId id) { diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 6e09d971b..6bbe2f467 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -32,7 +32,7 @@ #include "context/context.h" #include "context/cdhashset.h" #include "context/cdo.h" - +#include "context/cdqueue.h" #ifndef __CVC4__THEORY__BV__SLICER_BV_H #define __CVC4__THEORY__BV__SLICER_BV_H @@ -45,6 +45,7 @@ namespace bv { typedef Index TermId; +typedef TermId ExplanationId; extern const TermId UndefinedId; class CDBase; @@ -81,49 +82,9 @@ public: } return true; } - friend class CDBase; }; -class CDBase : public context::ContextNotifyObj { - context::Context* d_ctx; - context::CDO d_undoIndex; - - std::vector d_undoStack; - Base d_base; - CDBase(context::Context* ctx, Index bitwidth) - : ContextNotifyObj(ctx), - d_ctx(ctx), - d_undoIndex(d_ctx), - d_undoStack(), - d_base(bitwidth) - {} - void sliceAt(Index i) { - Assert (!d_base.isCutPoint(i)); - d_undoStack.push_back(i); - d_undoIndex.set(d_undoIndex.get() + 1); - d_base.sliceAt(i); - } - bool isCutPoint(Index i) { - return d_base.isCutPoint(i); - } - Index getBitwidth() const {return d_base.getBitwidth(); } - virtual ~CDBase() throw(AssertionException) {} - void contextNotifyPop() { - backtrack(); - } - - void backtrack() { - for (unsigned i = d_undoIndex.get(); i < d_undoStack.size(); ++i) { - Index i = d_undoStack.back(); - d_undoStack.pop_back(); - d_base.undoSliceAt(i); - } - Assert(d_undoIndex.get() == d_undoStack.size()); - } - -}; - /** * UnionFind * @@ -135,6 +96,11 @@ struct ExtractTerm { TermId id; Index high; Index low; + ExtractTerm() + : id (UndefinedId), + high(UndefinedId), + low(UndefinedId) + {} ExtractTerm(TermId i, Index h, Index l) : id (i), high(h), @@ -142,10 +108,24 @@ struct ExtractTerm { { Assert (h >= l && id != UndefinedId); } + bool operator== (const ExtractTerm& other) const { + return id == other.id && high == other.high && low == other.low; + } Index getBitwidth() const { return high - low + 1; } std::string debugPrint() const; + friend class ExtractTermHashFunction; }; +struct ExtractTermHashFunction { + ::std::size_t operator() (const ExtractTerm& t) const { + __gnu_cxx::hash h; + unsigned id = t.id; + unsigned high = t.high; + unsigned low = t.low; + return (h(id) * 7919 + h(high))* 4391 + h(low); + } +}; + class UnionFind; struct NormalForm { @@ -168,21 +148,34 @@ struct NormalForm { void clear() { base.clear(); decomp.clear(); } }; +class Slicer; class UnionFind : public context::ContextNotifyObj { + + struct ReprEdge { + TermId repr; + ExplanationId reason; + ReprEdge() + : repr(UndefinedId), + reason(UndefinedId) + {} + }; + class Node { - Index d_bitwidth; - TermId d_ch1, d_ch0; - TermId d_repr; + Index d_bitwidth; + TermId d_ch1, d_ch0; // the ids of the two children if they exist + ReprEdge d_edge; // points to the representative and stores the explanation + public: Node(Index b) : d_bitwidth(b), d_ch1(UndefinedId), d_ch0(UndefinedId), - d_repr(UndefinedId) + d_edge() {} - - TermId getRepr() const { return d_repr; } + + TermId getRepr() const { return d_edge.repr; } + ExplanationId getReason() const { return d_edge.reason; } Index getBitwidth() const { return d_bitwidth; } bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; } @@ -190,9 +183,10 @@ class UnionFind : public context::ContextNotifyObj { Assert (i < 2); return i == 0? d_ch0 : d_ch1; } - void setRepr(TermId id) { + void setRepr(TermId repr, ExplanationId reason) { Assert (! hasChildren()); - d_repr = id; + d_edge.repr = repr; + d_edge.reason = reason; } void setChildren(TermId ch1, TermId ch0) { // Assert (d_repr == UndefinedId && !hasChildren()); @@ -204,16 +198,21 @@ class UnionFind : public context::ContextNotifyObj { /// map from TermId to the nodes that represent them std::vector d_nodes; - /// a term is in this set if it is its own representative - //CDTermSet d_representatives; + __gnu_cxx::hash_map > d_idToExtract; + __gnu_cxx::hash_map d_extractToId; void getDecomposition(const ExtractTerm& term, Decomposition& decomp); + void getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp, std::vector& explanation); void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common); /// getter methods for the internal nodes TermId getRepr(TermId id) const { Assert (id < d_nodes.size()); return d_nodes[id].getRepr(); } + ExplanationId getReason(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getReason(); + } TermId getChild(TermId id, Index i) const { Assert (id < d_nodes.size()); return d_nodes[id].getChild(i); @@ -225,10 +224,12 @@ class UnionFind : public context::ContextNotifyObj { Assert (id < d_nodes.size()); return d_nodes[id].hasChildren(); } + TermId getTopLevel(TermId id) const; + /// setter methods for the internal nodes - void setRepr(TermId id, TermId new_repr) { + void setRepr(TermId id, TermId new_repr, ExplanationId reason) { Assert (id < d_nodes.size()); - d_nodes[id].setRepr(new_repr); + d_nodes[id].setRepr(new_repr, reason); } void setChildren(TermId id, TermId ch1, TermId ch0) { Assert ((ch1 == UndefinedId && ch0 == UndefinedId) || @@ -269,25 +270,32 @@ class UnionFind : public context::ContextNotifyObj { Statistics(); ~Statistics(); }; - Statistics d_statistics; - bool d_newSplit; + Slicer* d_slicer; public: - UnionFind(context::Context* ctx) + UnionFind(context::Context* ctx, Slicer* slicer) : ContextNotifyObj(ctx), d_nodes(), + d_idToExtract(), + d_extractToId(), d_undoStack(), d_undoStackIndex(ctx), - d_statistics() + d_statistics(), + d_slicer(slicer) {} - TermId addTerm(Index bitwidth); - void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); - void merge(TermId t1, TermId t2); - TermId find(TermId t1); + TermId addNode(Index bitwidth); + TermId addExtract(Index topLevel, Index high, Index low); + ExtractTerm getExtractTerm(TermId id) const; + bool isExtractTerm(TermId id) const; + + void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2, TermId reason); + void merge(TermId t1, TermId t2, TermId reason); + TermId find(TermId t1); + TermId findWithExplanation(TermId id, std::vector& explanation); void split(TermId term, Index i); - void getNormalForm(const ExtractTerm& term, NormalForm& nf); + void getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf, std::vector& explanation); void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2); void ensureSlicing(const ExtractTerm& term); Index getBitwidth(TermId id) const { @@ -300,34 +308,56 @@ public: void contextNotifyPop() { backtrack(); } - bool hasNewSplit() { return d_newSplit; } - void resetNewSplit() { d_newSplit = false; } - friend class Slicer; }; +class CoreSolver; + class Slicer { - __gnu_cxx::hash_map d_idToNode; + __gnu_cxx::hash_map > d_idToNode; __gnu_cxx::hash_map d_nodeToId; __gnu_cxx::hash_map d_coreTermCache; + __gnu_cxx::hash_map d_explanationToId; + std::vector d_explanations; UnionFind d_unionFind; - ExtractTerm registerTerm(TNode node); + + context::CDQueue d_newSplits; + context::CDO d_newSplitsIndex; + CoreSolver* d_coreSolver; + TermId d_termIdCount; public: - Slicer(context::Context* ctx) + Slicer(context::Context* ctx, CoreSolver* coreSolver) : d_idToNode(), d_nodeToId(), d_coreTermCache(), - d_unionFind(ctx) + d_explanationToId(), + d_explanations(), + d_unionFind(ctx, this), + d_newSplits(ctx), + d_newSplitsIndex(ctx, 0), + d_coreSolver(coreSolver) {} - void getBaseDecomposition(TNode node, std::vector& decomp); + void getBaseDecomposition(TNode node, std::vector& decomp, std::vector& explanation); + void registerEquality(TNode eq); + ExtractTerm registerTerm(TNode node); void processEquality(TNode eq); + void assertEquality(TNode eq); bool isCoreTerm (TNode node); - Base getTopLevelBase(TNode node); + + bool hasNode(TermId id) const; + Node getNode(TermId id) const; + TermId getId(TNode node) const; + + bool hasExplanation(ExplanationId id) const; + TNode getExplanation(ExplanationId id) const; + ExplanationId getExplanationId(TNode reason) const; + + bool termInEqualityEngine(TermId id); + void enqueueSplit(TermId id, Index i); + void getNewSplits(std::vector& splits); static void splitEqualities(TNode node, std::vector& equalities); static unsigned d_numAddedEqualities; - inline bool hasNewSplit() { return d_unionFind.hasNewSplit(); } - inline void resetNewSplit() { d_unionFind.resetNewSplit(); } }; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 5d034287d..ed1ba40a8 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -40,15 +40,16 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), - d_slicer(c), d_bitblastSolver(c, this), - d_coreSolver(c, this, &d_slicer), + d_coreSolver(c, this), d_statistics(), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) - {} + { + + } TheoryBV::~TheoryBV() {} @@ -289,7 +290,6 @@ void TheoryBV::addSharedTerm(TNode t) { } - EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { if (options::bitvectorEagerBitblast()) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 3e14584ed..d457571e2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -44,8 +44,8 @@ class TheoryBV : public Theory { context::CDHashSet d_alreadyPropagatedSet; context::CDHashSet d_sharedTermsSet; - Slicer d_slicer; BitblastSolver d_bitblastSolver; + // TODO generalize to multiple subtheories CoreSolver d_coreSolver; public: diff --git a/test/regress/regress0/bv/core/incremental.smt b/test/regress/regress0/bv/core/incremental.smt new file mode 100644 index 000000000..3a9ff85e0 --- /dev/null +++ b/test/regress/regress0/bv/core/incremental.smt @@ -0,0 +1,24 @@ +(benchmark ext_con_004_004_0016.smt +:logic QF_BV +:extrafuns ((v4 BitVec[16])) +:extrafuns ((dummy4 BitVec[1])) +:extrafuns ((a BitVec[16])) +:status unknown +:formula +(flet ($n1 true) +(let (?n2 (extract[15:13] a)) +(let (?n3 (extract[15:14] v4)) +(let (?n4 (concat ?n3 dummy4)) +(flet ($n5 (= ?n2 ?n4)) +(let (?n6 (extract[14:12] a)) +(let (?n7 (extract[13:12] v4)) +(let (?n8 (concat dummy4 ?n7)) +(flet ($n9 (= ?n6 ?n8)) +(flet ($n10 (and $n5 $n9)) +(let (?n11 (extract[14:14] v4)) +(let (?n12 (extract[13:13] v4)) +(flet ($n13 (= ?n11 ?n12)) +(flet ($n14 (not $n13)) +(flet ($n15 (and $n1 $n1 $n1 $n10 $n14)) +$n15 +)))))))))))))))) -- 2.30.2