summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_builder.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r--src/theory/quantifiers/model_builder.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d9ed3f092..8e84f15e2 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -123,10 +123,6 @@ public:
QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilderIG() throw() {}
public:
- //whether to add inst-gen lemmas
- virtual bool optInstGen();
- //whether to only consider only quantifier per round of inst-gen
- virtual bool optOneQuantPerRoundInstGen();
/** statistics class */
class Statistics {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback