diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 00:51:17 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 00:51:17 -0400 |
commit | adad8844eeae9d5fc3b4de1941a64ad428998088 (patch) | |
tree | 7228c6a2223e357e685fe4b39c87405ebe147a2f /src/theory/bv/bv_inequality_graph.h | |
parent | b7054f0e092f54c9e385f4b55a81173602b74b42 (diff) |
implementing more inequality graph stuff; work in progress doesn't compile
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 83 |
1 files changed, 72 insertions, 11 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index c319ba5f4..2c7d3f8a3 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -33,14 +33,17 @@ namespace bv { typedef unsigned TermId; typedef unsigned ReasonId; + class InequalityGraph { - context::Context d_context; + + + context::Context* d_context; struct InequalityEdge { TermId next; ReasonId reason; InequalityEdge(TermId n, ReasonId r) - : next(n) + : next(n), reason(r) {} }; @@ -50,21 +53,79 @@ class InequalityGraph { unsigned d_bitwidth; bool d_isConstant; BitVector d_value; + public: + InequalityNode(TermId id, unsigned bitwidth, bool isConst = false) + : d_id(id), + d_bitwidth(bitwidth), + d_isConstant(isConst), + d_value(BitVector(bitwidth, 0u)) + {} + TermId getId() const { return d_id; } + unsigned getBitwidth() const { return d_bitwidth; } + bool isConstant() const { return d_isConstant; } + const BitVector& getValue() const { return d_value; } }; - std::vector<InequalityNode> d_nodes; - std::vector< std::vector<InequalityEdge> > d_nodeEdges; + + struct PQueueElement { + TermId id; + BitVector min_value; + PQueueElement(TermId id, BitVector min) + : id(id), + min_value(min) + {} + bool operator< (const PQueueElement& other) const { + return min_value < other.min_value; + } + }; + typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; + typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + + typedef std::vector<InequalityEdge> Edges; + typedef __gnu_cxx::hash_set<TermId> TermIdSet; + + typedef std::queue<PQueueElement> BFSQueue; + + + std::vector<InequalityNode> d_ineqNodes; + + std::vector< Edges > d_ineqEdges; + std::vector< Edges > d_parentEdges; + + std::vector<TNode> d_reasonNodes; + std::vector<TNode> d_termNodes; + ReasonToIdMap d_reasonToIdMap; + TermNodeToIdMap d_termNodeToIdMap; + + TermId registerTerm(TNode term); + ReasonId registerReason(TNode reason); + TNode getReason(ReasonId id) const; + TNode getTerm(TermId id) const; + + Edges& getOutEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; } + Edges& getInEdges(TermId id) { Assert (id < d_parentEdges.size()); return d_parentEdges[id]; } + InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } + const BitVector& getValue(TermId id) const { return getInequalityNode().getValue(); } + bool addInequalityInternal(TermId a, TermId b, ReasonId reason); + bool areLessThanInternal(TermId a, TermId b); + void getConflictInternal(std::vector<ReasonId>& conflict); + + context::CDO<bool> d_inConflict; + context::CDList<TNode> d_conflict; + void setConflict(const std::vector<ReasonId>& conflict); public: InequalityGraph(context::Context* c) - : d_context(c) + : d_context(c), + d_ineqNodes(), + d_ineqEdges(), + d_parentEdges(), + d_inConflict(c, false), + d_conflict(c) {} - bool addInequality(TermId a, TermId b, ReasonId reason); - bool propagate(); - bool areLessThan(TermId a, TermId b); - void getConflict(std::vector<ReasonId>& conflict); - TermId addTerm(unsigned bitwidth); - TermId addTerm(const BitVector& value); + bool addInequality(TNode a, TNode b, TNode reason); + bool areLessThan(TNode a, TNode b); + void getConflict(std::vector<TNode>& conflict); }; } |