theory_bv_rewriter.h \
theory_bv_rewriter.cpp \
equality_engine.h \
- equality_engine.cpp
+ equality_engine.cpp \
+ slice_manager.h
EXTRA_DIST = kinds
* Set the class representative.
*/
inline void setFind(size_t findId) { d_findId = findId; }
-
};
/** Number of asserted equalities we have so far */
context::CDO<size_t> d_assertedEqualitiesCount;
+ /** Number of functions in the system */
+ context::CDO<size_t> d_functionsCount;
+
/**
* We keep a list of asserted equalities. Not among original terms, but
* among the class representatives.
* the owner information.
*/
EqualityEngine(OwnerClass& owner, context::Context* context)
- : d_notify(owner), d_assertedEqualitiesCount(context, 0) {
+ : d_notify(owner), d_assertedEqualitiesCount(context, 0), d_functionsCount(context, 0) {
Debug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl;
}
*/
size_t addTrigger(TNode t1, TNode t2);
+ /**
+ * Adds a new function to the equality engine. The funcions are not of fixed arity!
+ */
+ inline size_t newFunction() { d_functionsCount = d_functionsCount + 1; return d_functionsCount; }
+
};
template <typename OwnerClass, typename NotifyClass>
--- /dev/null
+/*
+ * slice_manager.h
+ *
+ * Created on: Feb 16, 2011
+ * Author: dejan
+ */
+
+#pragma once
+
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/equality_engine.h"
+
+#include <vector>
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/**
+ * Slice manager should keep the database of slices for the core theory leaf terms, for example
+ *
+ * term core leaf terms
+ * ----------------------------------------------
+ * (x + y)[31:0] x + y
+ * a[10:0]@a[11:10]@(b + c)[1:0] a, b, (b + c)
+ * (a << 5)[10] (a << 5)
+ *
+ * If an (dis-)equality is added to the system, we refine the slicing in order to align the extracts, for example
+ *
+ * equality slicing
+ * ----------------------------------------------
+ * x = y x[32,0], y[32,0]
+ * x@y = z x[32,0], y[32,0], z[64,32,0]
+ * x@y = z, x[31:16] = y[15:0] x[32,16,0], y[32,16,0], z[64,48,32,16,0]
+ *
+ * As a result of the slicing the slicing equalities are added to the equality engine, using the (associative)
+ * concat function that is generated for the equality manager, for example
+ *
+ * equality added equalities
+ * ----------------------------------------------
+ * x = y none
+ * x@y = z z = concat(z[63:32],z[31:0])
+ * x@y = z, x[31:16] = y[15:0] z = concat(z[63:32],z[31:0]),
+ * z[63:32] = concat(z[63:48], z[47:32]),
+ * z[31:0] = concat(z[31:16], z[15:0])
+ *
+ * In the last example, since concat is associative, the equality engine will know that z = concat(z[63:48], z[47:32],
+ * z[31:16], z[15:0]).
+ *
+ */
+template <class TheoryBitvector>
+class SliceManager {
+
+ /** The equality engine theory of bit-vectors is using */
+ typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
+
+ /** The theory of bitvectors */
+ TheoryBitvector& d_theoryBitvector;
+
+ /** The equality engine */
+ EqualityEngine& d_equalityEngine;
+
+ /** The id of the concatenation function */
+ size_t d_concatFunctionId;
+
+public:
+
+ SliceManager(TheoryBitvector& theoryBitvector)
+ : d_theoryBitvector(theoryBitvector), d_equalityEngine(theoryBitvector.getEqualityEngine()) {
+ // We register the concatentation with the equality engine
+ d_concatFunctionId = d_equalityEngine.newFunction();
+ }
+
+ inline size_t getConcatFunctionId() const { return d_concatFunctionId; }
+
+ /**
+ * Adds the equality (lhs = rhs) to the slice manager. This will not add the equalities to the equality manager,
+ * but will slice the equality according to the current slicing in order to align all the slices. The terms that
+ * get slices get sent to the theory engine as equalities, i.e if we slice x[10:0] into x[10:5]@x[4:0] equality
+ * engine gets the assertion x[10:0] = concat(x[10:5], x[4:0]).
+ */
+ inline void addEquality(TNode lhs, TNode rhs, std::vector<Node>& lhsSlices, std::vector<Node>& rhsSlices);
+};
+
+
+template <class TheoryBitvector>
+void SliceManager<TheoryBitvector>::addEquality(TNode lhs, TNode rhs, std::vector<Node>& lhsSlices, std::vector<Node>& rhsSlices) {
+ Debug("theory::bv::slicing") << "addEquality(" << lhs << "," << rhs << ")";
+ lhsSlices.push_back(lhs);
+ rhsSlices.push_back(rhs);
+}
+
+} // Namespace bv
+} // Namespace theory
+} // Namespace CVC4
// Do the right stuff
switch (assertion.getKind()) {
case kind::EQUAL: {
- bool ok = d_eqEngine.addEquality(assertion[0], assertion[1]);
- if (!ok) return;
+
+ // Slice the equality
+ std::vector<Node> lhsSlices, rhsSlices;
+ d_sliceManager.addEquality(assertion[0], assertion[1], lhsSlices, rhsSlices);
+ Assert(lhsSlices.size() == rhsSlices.size());
+
+ // Add the equality to the equality engine
+ for (int i = 0, i_end = lhsSlices.size(); i != i_end; ++ i) {
+ bool ok = d_eqEngine.addEquality(lhsSlices[i], rhsSlices[i]);
+ if (!ok) return;
+ }
break;
}
case kind::NOT: {
// We need to check this as the equality trigger might have been true when we made it
TNode equality = assertion[0];
- if (d_eqEngine.areEqual(equality[0], equality[1])) {
- vector<TNode> assertions;
- d_eqEngine.getExplanation(equality[0], equality[1], assertions);
- assertions.push_back(assertion);
- d_out->conflict(mkAnd(assertions));
- return;
+
+ // Slice the equality
+ std::vector<Node> lhsSlices, rhsSlices;
+ d_sliceManager.addEquality(equality[0], equality[1], lhsSlices, rhsSlices);
+ Assert(lhsSlices.size() == rhsSlices.size());
+
+ for (int i = 0, i_end = lhsSlices.size(); i != i_end; ++ i) {
+ if (d_eqEngine.areEqual(lhsSlices[i], rhsSlices[i])) {
+ vector<TNode> assertions;
+ d_eqEngine.getExplanation(lhsSlices[i], rhsSlices[i], assertions);
+ assertions.push_back(assertion);
+ d_out->conflict(mkAnd(assertions));
+ return;
+ }
}
break;
}
#include "theory/theory.h"
#include "context/context.h"
#include "context/cdset.h"
-#include "equality_engine.h"
+#include "theory/bv/equality_engine.h"
+#include "theory/bv/slice_manager.h"
namespace CVC4 {
namespace theory {
}
};
+ typedef EqualityEngine<TheoryBV, EqualityNotify> BvEqualityEngine;
+
private:
+
/** Equality reasoning engine */
- EqualityEngine<TheoryBV, EqualityNotify> d_eqEngine;
+ BvEqualityEngine d_eqEngine;
+
+ /** Slice manager */
+ SliceManager<TheoryBV> d_sliceManager;
/** Equality triggers indexed by ids from the equality manager */
std::vector<Node> d_triggers;
public:
TheoryBV(context::Context* c, OutputChannel& out) :
- Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_assertions(c) {
+ Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_sliceManager(*this), d_assertions(c) {
+ }
+
+ BvEqualityEngine& getEqualityEngine() {
+ return d_eqEngine;
}
void preRegisterTerm(TNode n);
projects / cvc5.git / commitdiff