summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_engine.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-10-13 12:11:09 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2014-10-13 12:11:15 +0200
commitc3992de261f0fa968f50349de1bdc3f9bef6ce6b (patch)
tree38308f6cdf2c502482bef56a9530e63f32376cb2 /src/theory/quantifiers/model_engine.h
parent41c09b51a7000fe5eb6b702d4ef9a1644129410b (diff)
Refactor model builder from model engine to quant engine. Work on fairness strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
-rw-r--r--src/theory/quantifiers/model_engine.h5
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 890af1643..6929188bc 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -29,9 +29,6 @@ class ModelEngine : public QuantifiersModule
{
friend class RepSetIterator;
private:
- /** builder class */
- QModelBuilder* d_builder;
-private:
//options
bool optOneQuantPerRound();
private:
@@ -49,8 +46,6 @@ private:
public:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
virtual ~ModelEngine();
- //get the builder
- QModelBuilder* getModelBuilder() { return d_builder; }
public:
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback