--- /dev/null
+/********************* */
+/*! \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<ReasonId>& conflict);
+};
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
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) {
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;
d_assertionIndex(c, 0)
{}
virtual ~SubtheorySolver() {}
-
virtual bool check(Theory::Effort e) = 0;
virtual void explain(TNode literal, std::vector<TNode>& 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() {
** 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"
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) {
if (node.getKind() == kind::EQUAL) {
d_equalityEngine.addTriggerEquality(node);
- d_slicer->processEquality(node);
+ // d_slicer->processEquality(node);
} else {
d_equalityEngine.addTerm(node);
}
}
}
-Node CoreSolver::getBaseDecomposition(TNode a) {
+Node CoreSolver::getBaseDecomposition(TNode a, std::vector<TNode>& explanation) {
std::vector<Node> 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;
}
// 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<TNode> 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());
// 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);
return false;
}
+ // make sure to assert the new splits
+ std::vector<Node> 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;
}
// 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) {
*/
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;
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;
/** FIXME: for debugging purposes only */
context::CDList<TNode> d_assertions;
- __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> d_normalFormCache;
Slicer* d_slicer;
context::CDO<bool> 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<TNode>& explanation);
+public:
+ CoreSolver(context::Context* c, TheoryBV* bv);
bool isCoreTheory() { return d_isCoreTheory; }
void setMasterEqualityEngine(eq::EqualityEngine* eq);
void preRegister(TNode node);
}
return EQUALITY_UNKNOWN;
}
+ bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
};
+++ /dev/null
-/********************* */
-/*! \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<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 EqualitySolver::addAssertions(const std::vector<TNode>& 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<TNode> 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<TNode>::const_iterator it = d_assertions.begin();
- for (; it!= d_assertions.end(); ++it) {
- Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert "
- << *it << ")\n";
- }
- }
- set<Node> termSet;
- d_bv->computeRelevantTerms(termSet);
- m->assertEqualityEngine(&d_equalityEngine, &termSet);
-}
+++ /dev/null
-/********************* */
-/*! \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<TNode> d_assertions;
-public:
-
- EqualitySolver(context::Context* c, TheoryBV* bv);
- 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;
- }
-};
-
-
-}
-}
-}
--- /dev/null
+/********************* */
+/*! \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<TNode>& assumptions) {
+
+}
+
+bool InequalitySolver::propagate(Theory::Effort e) {
+
+}
--- /dev/null
+/********************* */
+/*! \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<TNode>& assumptions);
+};
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
#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;
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();
}
* 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());
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.
* @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);
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;
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<ExplanationId>& 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
*
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 )
++(d_statistics.d_numSplits);
}
+TermId UnionFind::getTopLevel(TermId id) const {
+ __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> >::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);
getDecomposition(high_child, decomp);
}
}
+
+void UnionFind::getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf,
+ std::vector<ExplanationId>& 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<ExplanationId>& 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.
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();
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) {
}
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);
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;
}
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];
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<Node>& 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<TNode, TermId, TNodeHashFunction >::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<Node>& decomp, std::vector<TNode>& explanation) {
Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
Index high = utils::getSize(node) - 1;
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<ExplanationId> 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;
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<Node>& 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) {
#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
typedef Index TermId;
+typedef TermId ExplanationId;
extern const TermId UndefinedId;
class CDBase;
}
return true;
}
- friend class CDBase;
};
-class CDBase : public context::ContextNotifyObj {
- context::Context* d_ctx;
- context::CDO<unsigned> d_undoIndex;
-
- std::vector<unsigned> 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
*
TermId id;
Index high;
Index low;
+ ExtractTerm()
+ : id (UndefinedId),
+ high(UndefinedId),
+ low(UndefinedId)
+ {}
ExtractTerm(TermId i, Index h, Index l)
: id (i),
high(h),
{
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<unsigned> 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 {
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; }
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());
/// map from TermId to the nodes that represent them
std::vector<Node> d_nodes;
- /// a term is in this set if it is its own representative
- //CDTermSet d_representatives;
+ __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> > d_idToExtract;
+ __gnu_cxx::hash_map<ExtractTerm, TermId, ExtractTermHashFunction > d_extractToId;
void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
+ void getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp, std::vector<ExplanationId>& 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);
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) ||
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<ExplanationId>& explanation);
void split(TermId term, Index i);
-
void getNormalForm(const ExtractTerm& term, NormalForm& nf);
+ void getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf, std::vector<ExplanationId>& explanation);
void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
void ensureSlicing(const ExtractTerm& term);
Index getBitwidth(TermId id) const {
void contextNotifyPop() {
backtrack();
}
- bool hasNewSplit() { return d_newSplit; }
- void resetNewSplit() { d_newSplit = false; }
-
friend class Slicer;
};
+class CoreSolver;
+
class Slicer {
- __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
+ __gnu_cxx::hash_map<TermId, TNode, __gnu_cxx::hash<TermId> > d_idToNode;
__gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
__gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+ __gnu_cxx::hash_map<TNode, ExplanationId, TNodeHashFunction> d_explanationToId;
+ std::vector<TNode> d_explanations;
UnionFind d_unionFind;
- ExtractTerm registerTerm(TNode node);
+
+ context::CDQueue<Node> d_newSplits;
+ context::CDO<unsigned> 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<Node>& decomp);
+ void getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& 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<Node>& splits);
static void splitEqualities(TNode node, std::vector<Node>& equalities);
static unsigned d_numAddedEqualities;
- inline bool hasNewSplit() { return d_unionFind.hasNewSplit(); }
- inline void resetNewSplit() { d_unionFind.resetNewSplit(); }
};
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() {}
}
-
EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
{
if (options::bitvectorEagerBitblast()) {
context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
- Slicer d_slicer;
BitblastSolver d_bitblastSolver;
+ // TODO generalize to multiple subtheories
CoreSolver d_coreSolver;
public:
--- /dev/null
+(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
+))))))))))))))))
projects / cvc5.git / commitdiff