summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-05-06 17:04:52 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-05-06 17:04:52 -0500
commitdd84403eb19b769d80b4c57ae690ba14c02df041 (patch)
treeaa63f0f909ecd7063e38f7121c17cafb431abdf4 /src/theory/quantifiers_engine.h
parentc87ee73ad3d51c238700f236c18e425b80e8e7ac (diff)
Minor clean up, fixes related to sygus.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 60666c4a9..7522c633b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -158,8 +158,6 @@ private: //this information is reset during check
/** are we in conflict */
bool d_conflict;
context::CDO< bool > d_conflict_c;
- /** number of lemmas we actually added this round (for debugging) */
- unsigned d_num_added_lemmas_round;
/** has added lemma this round */
bool d_hasAddedLemma;
private:
@@ -332,8 +330,6 @@ public:
bool inConflict() { return d_conflict; }
/** get number of waiting lemmas */
unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
- /** get number of waiting lemmas */
- unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; }
/** get needs check */
bool getInstWhenNeedsCheck( Theory::Effort e );
/** get user pat mode */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback