From e50fc148b0ae2d74e3b7b7bb86cf8a038a3d9ca4 Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 13 Feb 2013 19:20:23 -0500 Subject: started working on incremental slicer - not compiling --- src/theory/bv/bv_subtheory_core.cpp | 1 + src/theory/bv/slicer.cpp | 35 +++++++++++++++++++++++- src/theory/bv/slicer.h | 54 +++++++++++++++++++++++++++++-------- 3 files changed, 78 insertions(+), 12 deletions(-) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index d678d7e31..3f2ede9e2 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -51,6 +51,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer) // 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); diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index f41612df3..3a6ca8a2f 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -216,6 +216,7 @@ void UnionFind::merge(TermId t1, TermId t2) { Assert (! hasChildren(t1) && ! hasChildren(t2)); setRepr(t1, t2); + recordOperation(UnionFind::MERGE, t1); d_representatives.erase(t1); d_statistics.d_numRepresentatives += -1; } @@ -224,7 +225,7 @@ TermId UnionFind::find(TermId id) { TermId repr = getRepr(id); if (repr != UndefinedId) { TermId find_id = find(repr); - setRepr(id, find_id); + // setRepr(id, find_id); return find_id; } return id; @@ -252,6 +253,7 @@ void UnionFind::split(TermId id, Index i) { 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); @@ -415,6 +417,37 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) { split(id, term.low); } +void UnionFind::backtrack() { + for (int i = d_undoStack.size() -1; i >= d_undoStackIndex; ++i) { + Operation op = d_undoStack.back(); + 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) { + Node& node = getNode(id); + Assert (getRepr(id) != id); + setRepr(id, id); +} + +void UnionFind::undoSplit(TermId id) { + Node& node = getNode(id); + Assert (hasChildren(node)); + setChildren(id, UndefindId, UndefinedId); +} + +void UnionFind::recordOperation(OperationKind op, TermId term) { + ++d_undoStackIndex; + d_undoStack.push_back(Operation(op, term)); + Assert (d_undoStack.size() == d_undoStackIndex); +} + /** * Slicer * diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 88254b983..731141262 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -29,6 +29,10 @@ #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 @@ -80,7 +84,7 @@ public: * UnionFind * */ -typedef __gnu_cxx::hash_set TermSet; +typedef context::CDHashSet CDTermSet; typedef std::vector Decomposition; struct ExtractTerm { @@ -121,7 +125,7 @@ struct NormalForm { }; -class UnionFind { +class UnionFind : public context::ContextNotifyObj { class Node { Index d_bitwidth; TermId d_ch1, d_ch0; @@ -157,7 +161,7 @@ class UnionFind { /// map from TermId to the nodes that represent them std::vector d_nodes; /// a term is in this set if it is its own representative - TermSet d_representatives; + CDTermSet d_representatives; void getDecomposition(const ExtractTerm& term, Decomposition& decomp); void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common); @@ -187,6 +191,28 @@ class UnionFind { 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 d_undoStack; + context::CDO d_undoStackIndex; + + void backtrack(); + void undoMerge(TermId id); + void undoSplit(TermId id); + void recordOperation(OperationKind op, TermId term); + class Statistics { public: IntStat d_numNodes; @@ -195,18 +221,18 @@ class UnionFind { IntStat d_numMerges; AverageStat d_avgFindDepth; ReferenceStat d_numAddedEqualities; - //IntStat d_numAddedEqualities; Statistics(); ~Statistics(); }; - Statistics d_statistics -; - + Statistics d_statistics; public: - UnionFind() + UnionFind(context::Context* ctx) : d_nodes(), - d_representatives() + d_representatives(ctx), + d_undoStack(), + d_undoStackIndex(ctx), + d_statistics() {} TermId addTerm(Index bitwidth); @@ -223,6 +249,11 @@ public: return d_nodes[id].getBitwidth(); } std::string debugPrint(TermId id); + + void contextNotifyPop() { + backtrack(); + } + friend class Slicer; }; @@ -233,16 +264,17 @@ class Slicer { UnionFind d_unionFind; ExtractTerm registerTerm(TNode node); public: - Slicer() + Slicer(context::Context* ctx) : d_idToNode(), d_nodeToId(), d_coreTermCache(), - d_unionFind() + d_unionFind(ctx) {} void getBaseDecomposition(TNode node, std::vector& decomp); void processEquality(TNode eq); bool isCoreTerm (TNode node); + static void splitEqualities(TNode node, std::vector& equalities); static unsigned d_numAddedEqualities; }; -- cgit v1.2.3