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.h2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index a3d239d18..d9ed3f092 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -42,8 +42,6 @@ public:
virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
- //whether to construct model at fullModel = true
- virtual bool optBuildAtFullModel() { return false; }
/** number of lemmas generated while building model */
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback