diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/quantifiers_engine.h | |
parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9743588a7..ffede2a5b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -59,6 +59,8 @@ namespace quantifiers { class TermEnumeration; class FirstOrderModel; class QuantAttributes; + class QuantEPR; + class QuantRelevance; class RelevantDomain; class BvInverter; class InstPropagator; @@ -116,7 +118,7 @@ private: /** equality inference class */ quantifiers::EqualityInference* d_eq_inference; /** for computing relevance of quantifiers */ - QuantRelevance * d_quant_rel; + quantifiers::QuantRelevance* d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; /** inversion utility for BV instantiation */ @@ -126,7 +128,7 @@ private: /** model builder */ quantifiers::QModelBuilder* d_builder; /** utility for effectively propositional logic */ - QuantEPR * d_qepr; + quantifiers::QuantEPR* d_qepr; /** term database */ quantifiers::TermDb* d_term_db; /** sygus term database */ @@ -253,12 +255,12 @@ public: /** get the BV inverter utility */ quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } /** get quantifier relevance */ - QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } /** get utility for EPR */ - QuantEPR* getQuantEPR() { return d_qepr; } -public: //modules + quantifiers::QuantEPR* getQuantEPR() { return d_qepr; } + public: // modules /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ |