diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
commit | f582b382a25463cead88bc1a46b93dd5c8099fad (patch) | |
tree | 15c54d5b5dc5b9b8a4da72a81c9ed0cf2ee6dc3d /src/theory/quantifiers/equality_infer.h | |
parent | 358e453bda62923fd0be94af5317b24a7281014b (diff) |
Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.
Diffstat (limited to 'src/theory/quantifiers/equality_infer.h')
-rw-r--r-- | src/theory/quantifiers/equality_infer.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4a6943119..70b05c351 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef EQUALITY_INFER_H -#define EQUALITY_INFER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #include <ext/hash_set> #include <iostream> @@ -60,14 +60,17 @@ private: /** use list */ NodeListMap d_uselist; void addToUseList( Node used, Node eqc ); + /** pending merges */ + NodeList d_pending_merges; public: EqualityInference(context::Context* c); virtual ~EqualityInference(); - /** notification when equality engine is updated */ + /** input : notification when equality engine is updated */ void eqNotifyNewClass(TNode t); void eqNotifyMerge(TNode t1, TNode t2); - - NodeList d_pending_merges; + /** output : inferred equalities */ + unsigned getNumPendingMerges() { return d_pending_merges.size(); } + Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; } }; } |