summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_builder.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-10-26 16:11:00 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2015-10-26 16:11:00 +0100
commitaf86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32 (patch)
treed86858d67279e940a225e7ca693172685532d6d7 /src/theory/quantifiers/model_builder.h
parentaaf1bbbdc6e42910e07db64441885ee3476d86df (diff)
Promote InstStrategyCbqi to quantifier module. Cleanup unused code.
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r--src/theory/quantifiers/model_builder.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 8e84f15e2..b45aa0ff0 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -184,6 +184,8 @@ protected:
int doInstGen( FirstOrderModel* fm, Node f );
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
+protected:
+ std::map< Node, QuantPhaseReq > d_phase_reqs;
public:
QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
~QModelBuilderDefault() throw() {}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback