summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-10-10 19:24:37 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-10-10 19:24:37 +0000
commit318e836ed5f6bd76d378dfce1c707b9908a1c5e1 (patch)
tree353e067a1cde3505595a5d0c6b410974f664c757 /src/theory/quantifiers/instantiation_engine.h
parent46864582756f3381cd5db3a0a977e8897fec66a7 (diff)
cleanup up some static data members in the quantifiers code
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r--src/theory/quantifiers/instantiation_engine.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 19dac736c..7721552c5 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -36,6 +36,8 @@ private:
std::map< Node, Node > d_ce_lit;
/** whether the instantiation engine should set incomplete if it cannot answer SAT */
bool d_setIncomplete;
+ /** inst round counter */
+ int d_ierCounter;
private:
bool hasAddedCbqiLemma( Node f );
void addCbqiLemma( Node f );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback