diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 12:11:09 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 12:11:15 +0200 |
commit | c3992de261f0fa968f50349de1bdc3f9bef6ce6b (patch) | |
tree | 38308f6cdf2c502482bef56a9530e63f32376cb2 /src/theory/quantifiers_engine.h | |
parent | 41c09b51a7000fe5eb6b702d4ef9a1644129410b (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_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b5a02df60..ee905ad09 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -82,6 +82,7 @@ namespace quantifiers { class QuantConflictFind; class RewriteEngine; class RelevantDomain; + class QModelBuilder; class ConjectureGenerator; class CegInstantiation; }/* CVC4::theory::quantifiers */ @@ -111,6 +112,8 @@ private: QuantRelevance * d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; + /** model builder */ + quantifiers::QModelBuilder* d_builder; /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; /** instantiation engine */ @@ -184,6 +187,8 @@ public: quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } /** get quantifier relevance */ QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + /** get the model builder */ + quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } /** get phase requirement information */ QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ @@ -284,6 +289,8 @@ public: void addTermToDatabase( Node n, bool withinQuant = false ); /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; + /** debug print equality engine */ + void debugPrintEqualityEngine( const char * c ); public: /** print instantiations */ void printInstantiations( std::ostream& out ); |