diff options
author | lianah <lianahady@gmail.com> | 2013-03-25 18:24:29 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-25 18:24:29 -0400 |
commit | 7f9b419adf3e45ce12ab9fb9b2d1afa076110e7d (patch) | |
tree | 025ca60adcbd33c2a2053fdc539217d398c438a5 /src/theory/bv/bv_inequality_graph.h | |
parent | 147f93cc140b1cf2a5957cbe95eccfc92e4d90b0 (diff) |
getEqualityStatus now also queries the inequality solver
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 112 |
1 files changed, 79 insertions, 33 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 1335eff93..b23ea7704 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -87,34 +87,37 @@ class InequalityGraph : public context::ContextNotifyObj{ value(val) {} }; + + typedef context::CDHashMap<TermId, ModelValue> Model; - struct PQueueElement { - TermId id; - BitVector lower_bound; - ModelValue model_value; - PQueueElement(TermId id, const BitVector& lb, const ModelValue& mv) - : id(id), - lower_bound(lb), - model_value(mv) + struct QueueComparator { + const Model* d_model; + QueueComparator(const Model* model) + : d_model(model) {} - - bool operator< (const PQueueElement& other) const { - return model_value.value > other.model_value.value; + bool operator() (TermId left, TermId right) const { + Assert (d_model->find(left) != d_model->end() && + d_model->find(right) != d_model->end()); + + return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; } - std::string toString() const; - }; - + }; + 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::priority_queue<PQueueElement> BFSQueue; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; - + + // to keep the explanation nodes alive + NodeSet d_reasonSet; std::vector<TNode> d_reasonNodes; ReasonToIdMap d_reasonToIdMap; @@ -125,7 +128,7 @@ class InequalityGraph : public context::ContextNotifyObj{ std::vector<TNode> d_conflict; bool d_signed; - context::CDHashMap<TermId, ModelValue> d_modelValues; + Model d_modelValues; void initializeModelValue(TNode node); void setModelValue(TermId term, const ModelValue& mv); ModelValue getModelValue(TermId term) const; @@ -163,23 +166,21 @@ class InequalityGraph : public context::ContextNotifyObj{ /** * If necessary update the value in the model of the current queue element. * - * @param el current queue element we are updating + * @param id 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, bool& changed); + bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed); /** * Update the current model starting with the start term. * * @param queue * @param start - * @param seen * * @return */ - bool computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& seen); + bool processQueue(BFSQueue& queue, TermId start); /** * Return the reasons why from <= to. If from is undefined we just * explain the current value of to. @@ -197,9 +198,10 @@ class InequalityGraph : public context::ContextNotifyObj{ /*** The currently asserted disequalities */ context::CDQueue<TNode> d_disequalities; - context::CDQueue<Node> d_lemmaQueue; - context::CDO<unsigned> d_lemmaIndex; - TNodeSet d_lemmasAdded; + context::CDQueue<TNode> d_disequalitiesToSplit; + context::CDO<unsigned> d_diseqToSplitIndex; + TNodeSet d_lemmasAdded; + TNodeSet d_disequalitiesAlreadySplit; /** Backtracking mechanisms **/ std::vector<std::pair<TermId, InequalityEdge> > d_undoStack; @@ -223,28 +225,72 @@ public: d_signed(s), d_modelValues(c), d_disequalities(c), - d_lemmaQueue(c), - d_lemmaIndex(c, 0), - d_lemmasAdded(), + d_disequalitiesToSplit(c), + d_diseqToSplitIndex(c, 0), + d_disequalitiesAlreadySplit(), d_undoStack(), d_undoStackIndex(c) {} /** - * + * Add a new inequality to the graph * * @param a * @param b - * @param diff + * @param strict * @param reason * * @return */ bool addInequality(TNode a, TNode b, bool strict, TNode reason); + /** + * Add a new disequality to the graph. This may lead in a lemma. + * + * @param a + * @param b + * @param reason + * + * @return + */ bool addDisequality(TNode a, TNode b, TNode reason); - bool areLessThan(TNode a, TNode b); void getConflict(std::vector<TNode>& conflict); virtual ~InequalityGraph() throw(AssertionException) {} - void getNewLemmas(std::vector<TNode>& new_lemmas); + /** + * Get any new lemmas (resulting from disequalities splits) that need + * to be added. + * + * @param new_lemmas + */ + void getNewLemmas(std::vector<Node>& new_lemmas); + /** + * Check that the currently asserted disequalities that have not been split on + * are still true in the current model. + */ + void checkDisequalities(); + /** + * Return true if a < b is entailed by the current set of assertions. + * + * @param a + * @param b + * + * @return + */ + bool isLessThan(TNode a, TNode b); + /** + * Returns true if the term has a value in the model (i.e. if we have seen it) + * + * @param a + * + * @return + */ + bool hasValueInModel(TNode a) const; + /** + * Return the value of a in the current model. + * + * @param a + * + * @return + */ + BitVector getValueInModel(TNode a) const; }; } |