summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/type_checker_template.cpp3
-rw-r--r--src/theory/bv/Makefile.am6
-rw-r--r--src/theory/bv/bitblast_strategies.cpp2
-rw-r--r--src/theory/bv/bitblaster.cpp19
-rw-r--r--src/theory/bv/bitblaster.h7
-rw-r--r--src/theory/bv/bv_subtheory.h27
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp19
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h2
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp278
-rw-r--r--src/theory/bv/bv_subtheory_core.h108
-rw-r--r--src/theory/bv/kinds2
-rw-r--r--src/theory/bv/slicer.cpp684
-rw-r--r--src/theory/bv/slicer.h338
-rw-r--r--src/theory/bv/theory_bv.cpp61
-rw-r--r--src/theory/bv/theory_bv.h9
-rw-r--r--src/theory/bv/theory_bv_utils.h39
-rw-r--r--src/util/bitvector.h14
-rw-r--r--src/util/index.h1
-rw-r--r--src/util/integer_cln_imp.h10
-rw-r--r--src/util/integer_gmp_imp.h19
-rw-r--r--src/util/utility.h1
21 files changed, 1594 insertions, 55 deletions
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 16f9ba917..4d9cbc60d 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -39,6 +39,9 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
case kind::BUILTIN:
typeNode = nodeManager->builtinOperatorType();
break;
+ case kind::BITVECTOR_EXTRACT_OP :
+ typeNode = nodeManager->builtinOperatorType();
+ break;
${typerules}
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 a952b2929..773685997 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) {
Debug("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.cpp b/src/theory/bv/bitblaster.cpp
index 4f5325e10..cc589c5c3 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -412,6 +412,23 @@ bool Bitblaster::isSharedTerm(TNode node) {
return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
}
+bool Bitblaster::hasValue(TNode a) {
+ Assert (d_termCache.find(a) != d_termCache.end());
+ Bits bits = d_termCache[a];
+ for (int i = bits.size() -1; i >= 0; --i) {
+ SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ if (bit_value == SAT_VALUE_UNKNOWN)
+ return false;
+ } else {
+ return false;
+ }
+ }
+ return true;
+}
+
Node Bitblaster::getVarValue(TNode a) {
Assert (d_termCache.find(a) != d_termCache.end());
Bits bits = d_termCache[a];
@@ -436,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
__gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
for (; it!= d_variables.end(); ++it) {
TNode var = *it;
- if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
+ if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var)) {
Node const_value = getVarValue(var);
Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
<< var << " "
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 21b389508..84a67e884 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -124,7 +124,8 @@ class Bitblaster {
// division is bitblasted in terms of constraints
// so it needs to use private bitblaster interface
void bbUdiv(TNode node, Bits& bits);
- void bbUrem(TNode node, Bits& bits);
+ void bbUrem(TNode node, Bits& bits);
+ bool hasValue(TNode a);
public:
void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
void bbTerm(TNode node, Bits& bits);
@@ -164,9 +165,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..d95aaa873 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) {
@@ -71,19 +72,31 @@ protected:
/** The bit-vector theory */
TheoryBV* d_bv;
-
+ context::CDQueue<TNode> d_assertionQueue;
+ context::CDO<uint32_t> d_assertionIndex;
public:
SubtheorySolver(context::Context* c, TheoryBV* bv) :
d_context(c),
- d_bv(bv)
+ d_bv(bv),
+ d_assertionQueue(c),
+ 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 collectModelInfo(TheoryModel* m) = 0;
+ bool done() { return d_assertionQueue.size() == d_assertionIndex; }
+ TNode get() {
+ Assert (!done());
+ TNode res = d_assertionQueue[d_assertionIndex];
+ d_assertionIndex = d_assertionIndex + 1;
+ return res;
+ }
+ void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
- virtual bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0;
- virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
- virtual void preRegister(TNode node) {}
- virtual void collectModelInfo(TheoryModel* m) = 0;
};
}
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 501aafb29..2f76e32d3 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -52,22 +52,21 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
d_bitblaster->explain(literal, assumptions);
}
-bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
- Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+bool BitblastSolver::check(Theory::Effort e) {
//// Eager bit-blasting
if (options::bitvectorEagerBitblast()) {
- for (unsigned i = 0; i < assertions.size(); ++i) {
- TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
+ while (!done()) {
+ TNode assertion = get();
+ TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
if (atom.getKind() != kind::BITVECTOR_BITOF) {
d_bitblaster->bbAtom(atom);
}
+ return true;
}
- return true;
}
//// Lazy bit-blasting
-
// bit-blast enqueued nodes
while (!d_bitblastQueue.empty()) {
TNode atom = d_bitblastQueue.front();
@@ -75,9 +74,9 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
d_bitblastQueue.pop();
}
- // propagation
- for (unsigned i = 0; i < assertions.size(); ++i) {
- TNode fact = assertions[i];
+ // Processinga ssertions
+ while (!done()) {
+ TNode fact = get();
if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
// Some atoms have not been bit-blasted yet
d_bitblaster->bbAtom(fact);
@@ -103,7 +102,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
}
}
- // solving
+ // Solving
if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
Assert(!d_bv->inConflict());
Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 3396d813b..318fdd230 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -42,7 +42,7 @@ public:
~BitblastSolver();
void preRegister(TNode node);
- bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+ bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
EqualityStatus getEqualityStatus(TNode a, TNode b);
void collectModelInfo(TheoryModel* m);
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
new file mode 100644
index 000000000..2e1320d1a
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -0,0 +1,278 @@
+/********************* */
+/*! \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_normalFormCache(),
+ d_slicer(slicer),
+ d_isCoreTheory(c, true),
+ d_baseChanged(false),
+ d_checkCalled(false)
+{
+ 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_EXTRACT);
+ // 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);
+ d_slicer->processEquality(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);
+ }
+}
+
+Node CoreSolver::getBaseDecomposition(TNode a) {
+ 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);
+ Node new_a = utils::mkConcat(a_decomp);
+ return new_a;
+}
+
+bool CoreSolver::decomposeFact(TNode fact) {
+ Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+ // 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];
+
+ // 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);
+
+ 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;
+
+ if (fact.getKind() == kind::EQUAL) {
+ // 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);
+ if (!ok) return false;
+ }
+ }
+ }
+ return true;
+}
+
+bool CoreSolver::check(Theory::Effort e) {
+ d_checkCalled = true;
+ Trace("bitvector::core") << "CoreSolver::check \n";
+ Assert (!d_bv->inConflict());
+
+ bool ok = true;
+ std::vector<Node> core_eqs;
+ while (! done()) {
+ TNode fact = get();
+
+ // update whether we are in the core fragment
+ if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
+ d_isCoreTheory = false;
+ }
+
+ // 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);
+ }
+ if (!ok)
+ return false;
+ }
+
+ return true;
+}
+
+bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
+ Debug("bv-slicer") << "CoreSolver::assertFactToEqualityEngine 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) {
+ Debug("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) {
+ Debug("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_CORE);
+}
+
+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..d5235a864
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -0,0 +1,108 @@
+/********************* */
+/*! \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;
+class Base;
+/**
+ * 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;
+ __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);
+ bool isCoreTheory() { return d_isCoreTheory; }
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void preRegister(TNode node);
+ bool check(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..ac668ab20
--- /dev/null
+++ b/src/theory/bv/slicer.cpp
@@ -0,0 +1,684 @@
+/********************* */
+/*! \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 "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;
+
+
+const TermId CVC4::theory::bv::UndefinedId = -1;
+
+/**
+ * Base
+ *
+ */
+Base::Base(uint32_t size)
+ : d_size(size),
+ d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
+{
+ Assert (d_size > 0);
+}
+
+
+void Base::sliceAt(Index index) {
+ Index vector_index = index / 32;
+ Assert (vector_index < d_size);
+ Index int_index = index % 32;
+ uint32_t bit_mask = utils::pow2(int_index);
+ d_repr[vector_index] = d_repr[vector_index] | bit_mask;
+}
+
+void Base::undoSliceAt(Index index) {
+ Index vector_index = index / 32;
+ Assert (vector_index < d_size);
+ Index int_index = index % 32;
+ uint32_t bit_mask = utils::pow2(int_index);
+ d_repr[vector_index] = d_repr[vector_index] ^ bit_mask;
+}
+
+void Base::sliceWith(const Base& other) {
+ Assert (d_size == other.d_size);
+ for (unsigned i = 0; i < d_repr.size(); ++i) {
+ d_repr[i] = d_repr[i] | other.d_repr[i];
+ }
+}
+
+bool Base::isCutPoint (Index index) const {
+ // there is an implicit cut point at the end and begining of the bv
+ if (index == d_size || index == 0)
+ return true;
+
+ Index vector_index = index / 32;
+ Assert (vector_index < d_size);
+ Index int_index = index % 32;
+ uint32_t bit_mask = utils::pow2(int_index);
+
+ return (bit_mask & d_repr[vector_index]) != 0;
+}
+
+void Base::diffCutPoints(const Base& other, Base& res) const {
+ Assert (d_size == other.d_size && res.d_size == d_size);
+ for (unsigned i = 0; i < d_repr.size(); ++i) {
+ Assert (res.d_repr[i] == 0);
+ res.d_repr[i] = d_repr[i] ^ other.d_repr[i];
+ }
+}
+
+bool Base::isEmpty() const {
+ for (unsigned i = 0; i< d_repr.size(); ++i) {
+ if (d_repr[i] != 0)
+ return false;
+ }
+ return true;
+}
+
+std::string Base::debugPrint() const {
+ std::ostringstream os;
+ os << "[";
+ bool first = true;
+ for (int i = d_size - 1; i >= 0; --i) {
+ if (isCutPoint(i)) {
+ if (first)
+ first = false;
+ else
+ os <<"| ";
+
+ os << i ;
+ }
+ }
+ os << "]";
+ return os.str();
+}
+
+/**
+ * ExtractTerm
+ *
+ */
+
+std::string ExtractTerm::debugPrint() const {
+ ostringstream os;
+ os << "id" << id << "[" << high << ":" << low <<"] ";
+ return os.str();
+}
+
+/**
+ * NormalForm
+ *
+ */
+
+std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const {
+ Assert (index < base.getBitwidth());
+ Index count = 0;
+ for (unsigned i = 0; i < decomp.size(); ++i) {
+ Index size = uf.getBitwidth(decomp[i]);
+ if ( count + size > index && index >= count) {
+ return pair<TermId, Index>(decomp[i], count);
+ }
+ count += size;
+ }
+ Unreachable();
+}
+
+
+
+std::string NormalForm::debugPrint(const UnionFind& uf) const {
+ ostringstream os;
+ os << "NF " << base.debugPrint() << endl;
+ os << "(";
+ for (int i = decomp.size() - 1; i>= 0; --i) {
+ os << decomp[i] << "[" << uf.getBitwidth(decomp[i]) <<"]";
+ os << (i != 0? ", " : "");
+ }
+ os << ") \n";
+ return os.str();
+}
+/**
+ * UnionFind::Node
+ *
+ */
+
+std::string UnionFind::Node::debugPrint() const {
+ ostringstream os;
+ os << "Repr " << d_repr << " ["<< d_bitwidth << "] ";
+ os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl;
+ return os.str();
+}
+
+
+/**
+ * UnionFind
+ *
+ */
+TermId UnionFind::addTerm(Index bitwidth) {
+ 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;
+}
+/**
+ * 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) {
+ Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
+ << " " << t2.debugPrint() << endl;
+ Assert (t1.getBitwidth() == t2.getBitwidth());
+
+ NormalForm nf1(t1.getBitwidth());
+ NormalForm nf2(t2.getBitwidth());
+
+ getNormalForm(t1, nf1);
+ getNormalForm(t2, nf2);
+
+ Assert (nf1.decomp.size() == nf2.decomp.size());
+ Assert (nf1.base == nf2.base);
+
+ for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
+ merge (nf1.decomp[i], nf2.decomp[i]);
+ }
+}
+
+/**
+ * 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) {
+ Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl;
+ ++(d_statistics.d_numMerges);
+ t1 = find(t1);
+ t2 = find(t2);
+
+ if (t1 == t2)
+ return;
+
+ Assert (! hasChildren(t1) && ! hasChildren(t2));
+ setRepr(t1, t2);
+ recordOperation(UnionFind::MERGE, t1);
+ //d_representatives.erase(t1);
+ d_statistics.d_numRepresentatives += -1;
+}
+
+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;
+}
+/**
+ * Splits the representative of the term between i-1 and i
+ *
+ * @param id the id of the term
+ * @param i the index we are splitting at
+ *
+ * @return
+ */
+void UnionFind::split(TermId id, Index i) {
+ Debug("bv-slicer-uf") << "UnionFind::split " << id << " at " << i << endl;
+ id = find(id);
+ Debug("bv-slicer-uf") << " node: " << d_nodes[id].debugPrint() << endl;
+
+ if (i == 0 || i == getBitwidth(id)) {
+ // nothing to do
+ return;
+ }
+
+ 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);
+ setChildren(id, top_id, bottom_id);
+ recordOperation(UnionFind::SPLIT, id);
+ } else {
+ Index cut = getCutPoint(id);
+ if (i < cut )
+ split(getChild(id, 0), i);
+ else
+ split(getChild(id, 1), i - cut);
+ }
+ ++(d_statistics.d_numSplits);
+}
+
+void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
+ nf.clear();
+ getDecomposition(term, nf.decomp);
+ // 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::getDecomposition(const ExtractTerm& term, Decomposition& decomp) {
+ // making sure the term is aligned
+ TermId id = find(term.id);
+
+ 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);
+ getDecomposition(child_ex, decomp);
+ }
+ 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);
+ getDecomposition(child_ex, decomp);
+ }
+ else {
+ // the extract is split over the two children
+ ExtractTerm low_child(getChild(id, 0), cut - 1, term.low);
+ getDecomposition(low_child, decomp);
+ ExtractTerm high_child(getChild(id, 1), term.high - cut, 0);
+ getDecomposition(high_child, decomp);
+ }
+}
+/**
+ * May cause reslicings of the decompositions. Must not assume the decompositons
+ * are the current normal form.
+ *
+ * @param d1
+ * @param d2
+ * @param common
+ */
+void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposition& decomp2, TermId common) {
+ Debug("bv-slicer") << "UnionFind::handleCommonSlice common = " << common << endl;
+ Index common_size = getBitwidth(common);
+ // find starting points of common slice
+ Index start1 = 0;
+ for (unsigned j = 0; j < decomp1.size(); ++j) {
+ if (decomp1[j] == common)
+ break;
+ start1 += getBitwidth(decomp1[j]);
+ }
+
+ Index start2 = 0;
+ for (unsigned j = 0; j < decomp2.size(); ++j) {
+ if (decomp2[j] == common)
+ break;
+ start2 += getBitwidth(decomp2[j]);
+ }
+ if (start1 > start2) {
+ Index temp = start1;
+ start1 = start2;
+ start2 = temp;
+ }
+
+ if (start2 - start1 < common_size) {
+ Index overlap = start1 + common_size - start2;
+ Assert (overlap > 0);
+ Index diff = common_size - overlap;
+ Assert (diff >= 0);
+ Index granularity = utils::gcd(diff, overlap);
+ // split the common part
+ for (unsigned i = 0; i < common_size; i+= granularity) {
+ split(common, i);
+ }
+ }
+
+}
+
+void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2) {
+ Debug("bv-slicer") << "UnionFind::alignSlicings " << term1.debugPrint() << endl;
+ Debug("bv-slicer") << " " << term2.debugPrint() << endl;
+ NormalForm nf1(term1.getBitwidth());
+ NormalForm nf2(term2.getBitwidth());
+
+ getNormalForm(term1, nf1);
+ getNormalForm(term2, nf2);
+
+ Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth());
+
+ // first check if the two have any common slices
+ std::vector<TermId> intersection;
+ utils::intersect(nf1.decomp, nf2.decomp, intersection);
+ for (unsigned i = 0; i < intersection.size(); ++i) {
+ // handle common slice may change the normal form
+ handleCommonSlice(nf1.decomp, nf2.decomp, intersection[i]);
+ }
+ // propagate cuts to a fixpoint
+ bool changed;
+ Base cuts(term1.getBitwidth());
+ do {
+ changed = false;
+ // we need to update the normal form which may have changed
+ getNormalForm(term1, nf1);
+ getNormalForm(term2, nf2);
+
+ // align the cuts points of the two slicings
+ // FIXME: this can be done more efficiently
+ cuts.sliceWith(nf1.base);
+ cuts.sliceWith(nf2.base);
+
+ for (unsigned i = 0; i < cuts.getBitwidth(); ++i) {
+ if (cuts.isCutPoint(i)) {
+ if (!nf1.base.isCutPoint(i)) {
+ pair<TermId, Index> pair1 = nf1.getTerm(i, *this);
+ split(pair1.first, i - pair1.second);
+ changed = true;
+ }
+ if (!nf2.base.isCutPoint(i)) {
+ pair<TermId, Index> pair2 = nf2.getTerm(i, *this);
+ split(pair2.first, i - pair2.second);
+ changed = true;
+ }
+ }
+ }
+ } while (changed);
+}
+/**
+ * Given an extract term a[i:j] makes sure a is sliced
+ * at indices i and j.
+ *
+ * @param term
+ */
+void UnionFind::ensureSlicing(const ExtractTerm& term) {
+ //Debug("bv-slicer") << "Slicer::ensureSlicing " << term.debugPrint() << endl;
+ TermId id = find(term.id);
+ split(id, term.high + 1);
+ split(id, term.low);
+}
+
+void UnionFind::backtrack() {
+ return;
+ int size = d_undoStack.size();
+ for (int i = size; i > d_undoStackIndex.get(); --i) {
+ Operation op = d_undoStack.back();
+ Assert (!d_undoStack.empty());
+ d_undoStack.pop_back();
+ if (op.op == UnionFind::MERGE) {
+ undoMerge(op.id);
+ } else {
+ Assert (op.op == UnionFind::SPLIT);
+ undoSplit(op.id);
+ }
+ }
+}
+
+void UnionFind::undoMerge(TermId id) {
+ TermId repr = getRepr(id);
+ Assert (repr != id);
+ setRepr(id, UndefinedId);
+}
+
+void UnionFind::undoSplit(TermId id) {
+ Assert (hasChildren(id));
+ setChildren(id, UndefinedId, UndefinedId);
+}
+
+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);
+}
+
+void UnionFind::getBase(TermId id, Base& base, Index offset) {
+ id = find(id);
+ if (!hasChildren(id))
+ return;
+ TermId id1 = find(getChild(id, 1));
+ TermId id0 = find(getChild(id, 0));
+ Index cut = getCutPoint(id);
+ base.sliceAt(cut + offset);
+ getBase(id1, base, cut + offset);
+ getBase(id0, base, offset);
+}
+
+
+/**
+ * Slicer
+ *
+ */
+
+ExtractTerm Slicer::registerTerm(TNode node) {
+ Index low = 0, high = utils::getSize(node) - 1;
+ TNode n = node;
+ if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+ n = node[0];
+ high = utils::getExtractHigh(node);
+ low = utils::getExtractLow(node);
+ }
+ if (d_nodeToId.find(n) == d_nodeToId.end()) {
+ TermId id = d_unionFind.addTerm(utils::getSize(n));
+ d_nodeToId[n] = id;
+ d_idToNode[id] = n;
+ }
+ TermId id = d_nodeToId[n];
+ ExtractTerm res(id, high, low);
+ Debug("bv-slicer") << "Slicer::registerTerm " << node << " => " << res.debugPrint() << endl;
+ return res;
+}
+
+void Slicer::processEquality(TNode eq) {
+ Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
+
+ Assert (eq.getKind() == kind::EQUAL);
+ TNode a = eq[0];
+ TNode b = eq[1];
+ ExtractTerm a_ex= registerTerm(a);
+ ExtractTerm b_ex= registerTerm(b);
+
+ d_unionFind.ensureSlicing(a_ex);
+ 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) {
+ Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
+
+ Index high = utils::getSize(node) - 1;
+ Index low = 0;
+ TNode top = node;
+ if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+ high = utils::getExtractHigh(node);
+ 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);
+
+ // construct actual extract nodes
+ Index current_low = 0;
+ Index current_high = 0;
+ for (unsigned i = 0; i < nf.decomp.size(); ++i) {
+ Index current_size = d_unionFind.getBitwidth(nf.decomp[i]);
+ current_high += current_size;
+ Node current = Rewriter::rewrite(utils::mkExtract(node, current_high - 1, current_low));
+ current_low += current_size;
+ decomp.push_back(current);
+ }
+
+ Debug("bv-slicer") << "as [";
+ for (unsigned i = 0; i < decomp.size(); ++i) {
+ Debug("bv-slicer") << decomp[i] <<" ";
+ }
+ Debug("bv-slicer") << "]" << endl;
+
+}
+
+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 &&
+ node.getMetaKind() != kind::metakind::VARIABLE &&
+ kind != kind::CONST_BITVECTOR) {
+ 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];
+}
+unsigned Slicer::d_numAddedEqualities = 0;
+
+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) {
+ int size = 0;
+ // no need to count the last child since the end cut point is implicit
+ for (int i = t1.getNumChildren() - 1; i >= 1 ; --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() - 1; i >= 1; --i) {
+ size = size + utils::getSize(t2[i]);
+ base2.sliceAt(size);
+ }
+ }
+
+ base1.sliceWith(base2);
+ if (!base1.isEmpty()) {
+ // 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 = utils::mkExtract(t1, i-1, last);
+ Node extract2 = utils::mkExtract(t2, i-1, last);
+ 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);
+ }
+ 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];
+ }
+ // 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));
+ }
+ TermId id = d_nodeToId[node];
+ Base base(d_unionFind.getBitwidth(id));
+ d_unionFind.getBase(id, base, 0);
+ return base;
+}
+
+std::string UnionFind::debugPrint(TermId id) {
+ ostringstream os;
+ if (hasChildren(id)) {
+ TermId id1 = find(getChild(id, 1));
+ TermId id0 = find(getChild(id, 0));
+ os << debugPrint(id1);
+ os << debugPrint(id0);
+ } else {
+ if (getRepr(id) == UndefinedId) {
+ os <<"id"<< id <<"[" << getBitwidth(id) <<"] ";
+ } else {
+ os << debugPrint(find(id));
+ }
+ }
+ return os.str();
+}
+
+UnionFind::Statistics::Statistics():
+ d_numNodes("theory::bv::slicer::NumberOfNodes", 0),
+ d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
+ d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
+ d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
+ d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
+ d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
+{
+ StatisticsRegistry::registerStat(&d_numRepresentatives);
+ StatisticsRegistry::registerStat(&d_numSplits);
+ StatisticsRegistry::registerStat(&d_numMerges);
+ StatisticsRegistry::registerStat(&d_avgFindDepth);
+ StatisticsRegistry::registerStat(&d_numAddedEqualities);
+}
+
+UnionFind::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numRepresentatives);
+ StatisticsRegistry::unregisterStat(&d_numSplits);
+ StatisticsRegistry::unregisterStat(&d_numMerges);
+ StatisticsRegistry::unregisterStat(&d_avgFindDepth);
+ StatisticsRegistry::unregisterStat(&d_numAddedEqualities);
+}
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
new file mode 100644
index 000000000..6e09d971b
--- /dev/null
+++ b/src/theory/bv/slicer.h
@@ -0,0 +1,338 @@
+/********************* */
+/*! \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 <math.h>
+
+#include "util/bitvector.h"
+#include "util/statistics_registry.h"
+#include "util/index.h"
+#include "expr/node.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "context/context.h"
+#include "context/cdhashset.h"
+#include "context/cdo.h"
+
+#ifndef __CVC4__THEORY__BV__SLICER_BV_H
+#define __CVC4__THEORY__BV__SLICER_BV_H
+
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+
+
+typedef Index TermId;
+extern const TermId UndefinedId;
+
+class CDBase;
+
+/**
+ * Base
+ *
+ */
+class Base {
+ Index d_size;
+ std::vector<uint32_t> d_repr;
+ void undoSliceAt(Index index);
+public:
+ Base (Index size);
+ void sliceAt(Index index);
+
+ void sliceWith(const Base& other);
+ bool isCutPoint(Index index) const;
+ void diffCutPoints(const Base& other, Base& res) const;
+ bool isEmpty() const;
+ std::string debugPrint() const;
+ Index getBitwidth() const { return d_size; }
+ void clear() {
+ for (unsigned i = 0; i < d_repr.size(); ++i) {
+ d_repr[i] = 0;
+ }
+ }
+ bool operator==(const Base& other) const {
+ if (other.getBitwidth() != getBitwidth())
+ return false;
+ for (unsigned i = 0; i < d_repr.size(); ++i) {
+ if (d_repr[i] != other.d_repr[i])
+ return false;
+ }
+ 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
+ *
+ */
+typedef context::CDHashSet<uint32_t, std::hash<uint32_t> > CDTermSet;
+typedef std::vector<TermId> Decomposition;
+
+struct ExtractTerm {
+ TermId id;
+ Index high;
+ Index low;
+ ExtractTerm(TermId i, Index h, Index l)
+ : id (i),
+ high(h),
+ low(l)
+ {
+ Assert (h >= l && id != UndefinedId);
+ }
+ Index getBitwidth() const { return high - low + 1; }
+ std::string debugPrint() const;
+};
+
+class UnionFind;
+
+struct NormalForm {
+ Base base;
+ Decomposition decomp;
+
+ NormalForm(Index bitwidth)
+ : base(bitwidth),
+ decomp()
+ {}
+ /**
+ * Returns the term in the decomposition on which the index i
+ * falls in
+ * @param i
+ *
+ * @return
+ */
+ std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const;
+ std::string debugPrint(const UnionFind& uf) const;
+ void clear() { base.clear(); decomp.clear(); }
+};
+
+
+class UnionFind : public context::ContextNotifyObj {
+ class Node {
+ Index d_bitwidth;
+ TermId d_ch1, d_ch0;
+ TermId d_repr;
+ public:
+ Node(Index b)
+ : d_bitwidth(b),
+ d_ch1(UndefinedId),
+ d_ch0(UndefinedId),
+ d_repr(UndefinedId)
+ {}
+
+ TermId getRepr() const { return d_repr; }
+ Index getBitwidth() const { return d_bitwidth; }
+ bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
+
+ TermId getChild(Index i) const {
+ Assert (i < 2);
+ return i == 0? d_ch0 : d_ch1;
+ }
+ void setRepr(TermId id) {
+ Assert (! hasChildren());
+ d_repr = id;
+ }
+ void setChildren(TermId ch1, TermId ch0) {
+ // Assert (d_repr == UndefinedId && !hasChildren());
+ d_ch1 = ch1;
+ d_ch0 = ch0;
+ }
+ std::string debugPrint() const;
+ };
+
+ /// 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;
+
+ void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
+ 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();
+ }
+ TermId getChild(TermId id, Index i) const {
+ Assert (id < d_nodes.size());
+ return d_nodes[id].getChild(i);
+ }
+ Index getCutPoint(TermId id) const {
+ return getBitwidth(getChild(id, 0));
+ }
+ bool hasChildren(TermId id) const {
+ Assert (id < d_nodes.size());
+ return d_nodes[id].hasChildren();
+ }
+ /// setter methods for the internal nodes
+ void setRepr(TermId id, TermId new_repr) {
+ Assert (id < d_nodes.size());
+ d_nodes[id].setRepr(new_repr);
+ }
+ void setChildren(TermId id, TermId ch1, TermId ch0) {
+ Assert ((ch1 == UndefinedId && ch0 == UndefinedId) ||
+ (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0)));
+ d_nodes[id].setChildren(ch1, ch0);
+ }
+
+ /* Backtracking mechanisms */
+
+ enum OperationKind {
+ MERGE,
+ SPLIT
+ };
+
+ struct Operation {
+ OperationKind op;
+ TermId id;
+ Operation(OperationKind o, TermId i)
+ : op(o), id(i) {}
+ };
+
+ std::vector<Operation> d_undoStack;
+ context::CDO<unsigned> d_undoStackIndex;
+
+ void backtrack();
+ void undoMerge(TermId id);
+ void undoSplit(TermId id);
+ void recordOperation(OperationKind op, TermId term);
+ virtual ~UnionFind() throw(AssertionException) {}
+ class Statistics {
+ public:
+ IntStat d_numNodes;
+ IntStat d_numRepresentatives;
+ IntStat d_numSplits;
+ IntStat d_numMerges;
+ AverageStat d_avgFindDepth;
+ ReferenceStat<unsigned> d_numAddedEqualities;
+ Statistics();
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+ bool d_newSplit;
+public:
+ UnionFind(context::Context* ctx)
+ : ContextNotifyObj(ctx),
+ d_nodes(),
+ d_undoStack(),
+ d_undoStackIndex(ctx),
+ d_statistics()
+ {}
+
+ TermId addTerm(Index bitwidth);
+ void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2);
+ void merge(TermId t1, TermId t2);
+ TermId find(TermId t1);
+ void split(TermId term, Index i);
+
+ void getNormalForm(const ExtractTerm& term, NormalForm& nf);
+ void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
+ void ensureSlicing(const ExtractTerm& term);
+ Index getBitwidth(TermId id) const {
+ Assert (id < d_nodes.size());
+ return d_nodes[id].getBitwidth();
+ }
+ void getBase(TermId id, Base& base, Index offset);
+ std::string debugPrint(TermId id);
+
+ void contextNotifyPop() {
+ backtrack();
+ }
+ bool hasNewSplit() { return d_newSplit; }
+ void resetNewSplit() { d_newSplit = false; }
+
+ friend class Slicer;
+};
+
+class Slicer {
+ __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
+ __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+ __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+ UnionFind d_unionFind;
+ ExtractTerm registerTerm(TNode node);
+public:
+ Slicer(context::Context* ctx)
+ : d_idToNode(),
+ d_nodeToId(),
+ d_coreTermCache(),
+ d_unionFind(ctx)
+ {}
+
+ void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
+ void processEquality(TNode eq);
+ bool isCoreTerm (TNode node);
+ Base getTopLevelBase(TNode node);
+ 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(); }
+};
+
+
+}/* 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 57a77c0d2..5d034287d 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(c),
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():
@@ -71,6 +73,8 @@ TheoryBV::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_solveTimer);
}
+
+
void TheoryBV::preRegisterTerm(TNode node) {
Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
@@ -78,9 +82,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
// don't use the equality engine in the eager bit-blasting
return;
}
-
+
d_bitblastSolver.preRegister(node);
- d_equalitySolver.preRegister(node);
+ d_coreSolver.preRegister(node);
}
void TheoryBV::sendConflict() {
@@ -105,25 +109,23 @@ void TheoryBV::check(Effort e)
return;
}
- // getting the new assertions
- std::vector<TNode> new_assertions;
while (!done()) {
- Assertion assertion = get();
- TNode fact = assertion.assertion;
- new_assertions.push_back(fact);
- Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
+ TNode fact = get().assertion;
+ d_coreSolver.assertFact(fact);
+ d_bitblastSolver.assertFact(fact);
}
+ bool ok = true;
if (!inConflict()) {
- // sending assertions to the equality solver first
- d_equalitySolver.addAssertions(new_assertions, e);
+ ok = d_coreSolver.check(e);
}
- if (!inConflict()) {
- // sending assertions to the bitblast solver
- d_bitblastSolver.addAssertions(new_assertions, e);
+ Assert (!ok == inConflict());
+ if (!inConflict() && !d_coreSolver.isCoreTheory()) {
+ ok = d_bitblastSolver.check(e);
}
-
+
+ Assert (!ok == inConflict());
if (inConflict()) {
sendConflict();
}
@@ -132,9 +134,8 @@ 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) {
@@ -187,16 +188,25 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
return PP_ASSERT_STATUS_UNSOLVED;
}
-
Node TheoryBV::ppRewrite(TNode t)
{
if (RewriteRule<BitwiseEq>::applies(t)) {
Node result = RewriteRule<BitwiseEq>::run<false>(t);
return Rewriter::rewrite(result);
}
+
+ if (t.getKind() == kind::EQUAL) {
+ std::vector<Node> equalities;
+ Slicer::splitEqualities(t, equalities);
+ return utils::mkAnd(equalities);
+ }
+
return t;
}
+void TheoryBV::presolve() {
+ Debug("bitvector") << "TheoryBV::presolve" << endl;
+}
bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
{
@@ -227,7 +237,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();
@@ -242,9 +252,9 @@ 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)) {
- Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
- d_equalitySolver.explain(literal, assumptions);
+ if (propagatedBy(literal, SUB_CORE)) {
+ Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl;
+ d_coreSolver.explain(literal, assumptions);
} else {
Assert(propagatedBy(literal, SUB_BITBLAST));
Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
@@ -274,18 +284,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..3e14584ed 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,10 +25,11 @@
#include "context/cdhashset.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
-#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 +44,10 @@ 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 +70,7 @@ public:
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
Node ppRewrite(TNode t);
+ void presolve();
private:
class Statistics {
@@ -137,6 +141,7 @@ private:
friend class Bitblaster;
friend class BitblastSolver;
friend class EqualitySolver;
+ friend class CoreSolver;
};/* class TheoryBV */
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 7d851d0fb..e5a7bbb84 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -31,6 +31,12 @@ namespace theory {
namespace bv {
namespace utils {
+inline uint32_t pow2(uint32_t power) {
+ Assert (power < 32);
+ uint32_t one = 1;
+ return one << power;
+}
+
inline unsigned getExtractHigh(TNode node) {
return node.getOperator().getConst<BitVectorExtract>().high;
}
@@ -67,11 +73,11 @@ inline Node mkAnd(std::vector<TNode>& children) {
std::set<TNode> distinctChildren;
distinctChildren.insert(children.begin(), children.end());
- if (children.size() == 0) {
+ if (distinctChildren.size() == 0) {
return mkTrue();
}
- if (children.size() == 1) {
+ if (distinctChildren.size() == 1) {
return *children.begin();
}
@@ -406,6 +412,35 @@ inline std::string vectorToString(const std::vector<Node>& nodes) {
return out.str();
}
+// FIXME: dumb code
+inline void intersect(const std::vector<uint32_t>& v1,
+ const std::vector<uint32_t>& v2,
+ std::vector<uint32_t>& intersection) {
+ for (unsigned i = 0; i < v1.size(); ++i) {
+ bool found = false;
+ for (unsigned j = 0; j < v2.size(); ++j) {
+ if (v2[j] == v1[i]) {
+ found = true;
+ break;
+ }
+ }
+ if (found) {
+ intersection.push_back(v1[i]);
+ }
+ }
+}
+
+template <class T>
+inline T gcd(T a, T b) {
+ while (b != 0) {
+ T t = b;
+ b = a % t;
+ a = t;
+ }
+ return a;
+}
+
+
}
}
}
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 4cbcba50e..c9661c0c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,10 +178,23 @@ 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);
+ }
+
/**
* Total division function that returns 0 when the denominator is 0.
*/
BitVector unsignedDivTotal (const BitVector& y) const {
+
CheckArgument(d_size == y.d_size, y);
if (y.d_value == 0) {
return BitVector(d_size, 0u);
@@ -190,6 +203,7 @@ public:
CheckArgument(y.d_value > 0, y);
return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}
+
/**
* Total division function that returns 0 when the denominator is 0.
*/
diff --git a/src/util/index.h b/src/util/index.h
index 4c03af5b0..252f7066b 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -21,6 +21,7 @@
#include <stdint.h>
#include <boost/static_assert.hpp>
+#include <limits>
namespace CVC4 {
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index b5452ae00..81c0428cb 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 176604268..85d49f921 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..089be478d 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,7 +67,6 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
return (match2 == last) ? match : last;
}
-
}/* CVC4 namespace */
#endif /* __CVC4__UTILITY_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback