From c008b0201af83f2781ff4b3af84767927cf8382f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 17 Feb 2011 00:29:26 +0000 Subject: [PATCH] getting ready for slicing bitvectors --- src/theory/bv/Makefile.am | 3 +- src/theory/bv/equality_engine.h | 11 +++- src/theory/bv/slice_manager.h | 95 +++++++++++++++++++++++++++++++++ src/theory/bv/theory_bv.cpp | 33 +++++++++--- src/theory/bv/theory_bv.h | 17 ++++-- 5 files changed, 145 insertions(+), 14 deletions(-) create mode 100644 src/theory/bv/slice_manager.h diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index fdace42b4..db750575f 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -15,6 +15,7 @@ libbv_la_SOURCES = \ theory_bv_rewriter.h \ theory_bv_rewriter.cpp \ equality_engine.h \ - equality_engine.cpp + equality_engine.cpp \ + slice_manager.h EXTRA_DIST = kinds diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 8f596723c..000e93a7b 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -112,7 +112,6 @@ public: * Set the class representative. */ inline void setFind(size_t findId) { d_findId = findId; } - }; @@ -134,6 +133,9 @@ class EqualityEngine { /** Number of asserted equalities we have so far */ context::CDO d_assertedEqualitiesCount; + /** Number of functions in the system */ + context::CDO d_functionsCount; + /** * We keep a list of asserted equalities. Not among original terms, but * among the class representatives. @@ -262,7 +264,7 @@ public: * 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; } @@ -305,6 +307,11 @@ public: */ 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 diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h new file mode 100644 index 000000000..b31f721a0 --- /dev/null +++ b/src/theory/bv/slice_manager.h @@ -0,0 +1,95 @@ +/* + * 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 + +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 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& lhsSlices, std::vector& rhsSlices); +}; + + +template +void SliceManager::addEquality(TNode lhs, TNode rhs, std::vector& lhsSlices, std::vector& rhsSlices) { + Debug("theory::bv::slicing") << "addEquality(" << lhs << "," << rhs << ")"; + lhsSlices.push_back(lhs); + rhsSlices.push_back(rhs); +} + +} // Namespace bv +} // Namespace theory +} // Namespace CVC4 diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c9e7c397e..cb8b95751 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -55,19 +55,36 @@ void TheoryBV::check(Effort e) { // 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 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 assertions; - d_eqEngine.getExplanation(equality[0], equality[1], assertions); - assertions.push_back(assertion); - d_out->conflict(mkAnd(assertions)); - return; + + // Slice the equality + std::vector 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 assertions; + d_eqEngine.getExplanation(lhsSlices[i], rhsSlices[i], assertions); + assertions.push_back(assertion); + d_out->conflict(mkAnd(assertions)); + return; + } } break; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index dfae3b965..14a526e36 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,7 +24,8 @@ #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 { @@ -45,10 +46,16 @@ public: } }; + typedef EqualityEngine BvEqualityEngine; + private: + /** Equality reasoning engine */ - EqualityEngine d_eqEngine; + BvEqualityEngine d_eqEngine; + + /** Slice manager */ + SliceManager d_sliceManager; /** Equality triggers indexed by ids from the equality manager */ std::vector d_triggers; @@ -62,7 +69,11 @@ private: 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); -- 2.30.2