diff options
author | lianah <lianahady@gmail.com> | 2013-03-20 21:10:10 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-20 21:10:10 -0400 |
commit | 27d848ac6b84a6b040baaf8a3f441692779e5bf6 (patch) | |
tree | 681597d55aed622b3960f43b2adf374d624a5ef5 /src/theory/bv/bv_inequality_graph.h | |
parent | 0a319e44fb2630d05207bba40eab290a805eab2b (diff) |
generalized bv inequality reasoning to handle both strict and non-strict inequalities
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 166 |
1 files changed, 117 insertions, 49 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 1a4b14ace..18bd75726 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -34,7 +34,8 @@ namespace bv { typedef unsigned TermId; typedef unsigned ReasonId; extern const TermId UndefinedTermId; -extern const ReasonId UndefinedReasonId; +extern const ReasonId UndefinedReasonId; +extern const ReasonId AxiomReasonId; class InequalityGraph { @@ -44,24 +45,25 @@ class InequalityGraph { struct InequalityEdge { TermId next; ReasonId reason; - InequalityEdge(TermId n, ReasonId r) - : next(n), - reason(r) + bool strict; + InequalityEdge(TermId n, bool s, ReasonId r) + : next(n), + reason(r), + strict(s) {} }; - + class InequalityNode { TermId d_id; unsigned d_bitwidth; bool d_isConstant; BitVector d_value; public: - InequalityNode(TermId id, unsigned bitwidth, bool isConst, BitVector val) + InequalityNode(TermId id, unsigned bitwidth, bool isConst, const BitVector val) : d_id(id), d_bitwidth(bitwidth), d_isConstant(isConst), - d_value(val) - {} + d_value(val) {} TermId getId() const { return d_id; } unsigned getBitwidth() const { return d_bitwidth; } bool isConstant() const { return d_isConstant; } @@ -69,17 +71,37 @@ class InequalityGraph { void setValue(const BitVector& val) { Assert (val.getSize() == d_bitwidth); d_value = val; } }; + struct Explanation { + TermId parent; + ReasonId reason; + + Explanation() + : parent(UndefinedTermId), + reason(UndefinedReasonId) + {} + + Explanation(TermId p, ReasonId r) + : parent(p), + reason(r) + {} + }; + struct PQueueElement { TermId id; - BitVector min_value; - PQueueElement(TermId id, BitVector min) - : id(id), - min_value(min) + BitVector value; + BitVector lower_bound; + Explanation explanation; + PQueueElement(TermId id, const BitVector v, const BitVector& lb, Explanation exp) + : id(id), + value(v), + lower_bound(lb), + explanation(exp) {} + bool operator< (const PQueueElement& other) const { - return min_value < other.min_value; + return value > other.value; } - }; + }; typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; @@ -87,64 +109,110 @@ class InequalityGraph { typedef std::vector<InequalityEdge> Edges; typedef __gnu_cxx::hash_set<TermId> TermIdSet; - typedef std::queue<TermId> TermIdQueue; - typedef std::priority_queue<PQueueElement> BFSQueue; - + typedef std::priority_queue<PQueueElement> BFSQueue; + typedef __gnu_cxx::hash_map<TermId, Explanation> TermIdToExplanationMap; 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; + ReasonToIdMap d_reasonToIdMap; + + std::vector<Node> d_termNodes; TermNodeToIdMap d_termNodeToIdMap; + TermIdToExplanationMap d_termToExplanation; + + context::CDO<bool> d_inConflict; + std::vector<TNode> d_conflict; + bool d_signed; + + + /** + * Registers the term by creating its corresponding InequalityNode + * and adding the min <= term <= max default edges. + * + * @param term + * + * @return + */ TermId registerTerm(TNode term); - ReasonId registerReason(TNode reason); - TNode getReason(ReasonId id) const; - TermId getReasonId(TermId a, TermId b); - TNode getTerm(TermId id) const; + TNode getTermNode(TermId id) const; + TermId getTermId(TNode node) 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]; } + ReasonId registerReason(TNode reason); + TNode getReasonNode(ReasonId id) const; + + bool hasExplanation(TermId id) const { return d_termToExplanation.find(id) != d_termToExplanation.end(); } + Explanation getExplanation(TermId id) const { Assert (hasExplanation(id)); return d_termToExplanation.find(id)->second; } + void setExplanation(TermId id, Explanation exp) { d_termToExplanation[id] = exp; } + + Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; } InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } - - const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); } unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); } + bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); } + BitVector maxValue(unsigned bitwidth); + BitVector minValue(unsigned bitwidth); + TermId getMaxValueId(unsigned bitwidth); + TermId getMinValueId(unsigned bitwidth); - bool hasValue(TermId id) const; - bool initializeValues(TNode a, TNode b, TermId reason_id); - TermId getMaxParent(TermId id); - bool hasParents(TermId id); - - bool canReach(TermId from, TermId to); - void bfs(TermIdSet& seen, TermIdQueue& queue); + const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); } + + void addEdge(TermId a, TermId b, bool strict, TermId reason); - void addEdge(TermId a, TermId b, TermId reason); - bool addInequalityInternal(TermId a, TermId b, ReasonId reason); - bool areLessThanInternal(TermId a, TermId b); - void getConflictInternal(std::vector<ReasonId>& conflict); - bool computeValuesBFS(BFSQueue& queue, TermIdSet& seen); + void setConflict(const std::vector<ReasonId>& conflict); + /** + * If necessary update the value in the model of the current queue element. + * + * @param el current queue element we are updating + * @param start node we started with, to detect cycles + * @param seen + * + * @return + */ + bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen); + /** + * Update the current model starting with the start term. + * + * @param queue + * @param start + * @param seen + * + * @return + */ + bool computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& seen); + /** + * Return the reasons why from <= to. If from is undefined we just + * explain the current value of to. + * + * @param from + * @param to + * @param explanation + */ void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); - context::CDO<bool> d_inConflict; - std::vector<TNode> d_conflict; - void setConflict(const std::vector<ReasonId>& conflict); - public: - InequalityGraph(context::Context* c) + InequalityGraph(context::Context* c, bool s = false) : d_context(c), d_ineqNodes(), d_ineqEdges(), - d_parentEdges(), d_inConflict(c, false), - d_conflict() + d_conflict(), + d_signed(s) {} - bool addInequality(TNode a, TNode b, TNode reason); + /** + * + * + * @param a + * @param b + * @param diff + * @param reason + * + * @return + */ + bool addInequality(TNode a, TNode b, bool strict, TNode reason); bool areLessThan(TNode a, TNode b); void getConflict(std::vector<TNode>& conflict); }; |