diff options
| author | lianah <lianahady@gmail.com> | 2013-03-23 17:19:21 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-23 17:19:21 -0400 |
| commit | b9b17625957d2e718dc2d071dff505d04ccad879 (patch) | |
| tree | 879e6250604321afb94d95992be8ffdca2240501 /src/theory/bv/bv_inequality_graph.h | |
| parent | 8882aef2dd4f1f629b0de99fc3a7f390fab2f83e (diff) | |
non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
| -rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 18bd75726..6eb88ec79 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -101,6 +101,7 @@ class InequalityGraph { bool operator< (const PQueueElement& other) const { return value > other.value; } + std::string toString() const; }; typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; @@ -171,7 +172,7 @@ class InequalityGraph { * * @return */ - bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen); + bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen, bool& changed); /** * Update the current model starting with the start term. * |