diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
commit | 51d642e075466bc6655cae9752350f6760b2bd0f (patch) | |
tree | 9c4e752e2d7ced10854c82555fa148b8e73e6d78 /src/theory/quantifiers_engine.h | |
parent | 4a8045f5f57c1e71dc4a2cdadc02ca09114c70af (diff) |
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index eb4470eec..78609914f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -89,6 +89,7 @@ namespace quantifiers { class QModelBuilder; class ConjectureGenerator; class CegInstantiation; + class LtePartialInst; }/* CVC4::theory::quantifiers */ namespace inst { @@ -135,7 +136,7 @@ private: /** ceg instantiation */ quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ - QuantLtePartialInst * d_lte_part_inst; + quantifiers::LtePartialInst * d_lte_part_inst; public: //effort levels enum { QEFFORT_CONFLICT, @@ -144,7 +145,7 @@ public: //effort levels }; private: /** list of all quantifiers seen */ - std::vector< Node > d_quants; + std::map< Node, bool > d_quants; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -217,6 +218,8 @@ public: //modules quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } /** ceg instantiation */ quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } + /** local theory ext partial inst */ + quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; @@ -233,7 +236,7 @@ public: /** check at level */ void check( Theory::Effort e ); /** register quantifier */ - void registerQuantifier( Node f ); + bool registerQuantifier( Node f ); /** register quantifier */ void registerPattern( std::vector<Node> & pattern); /** assert universal quantifier */ @@ -283,11 +286,6 @@ public: /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); public: - /** get number of quantifiers */ - int getNumQuantifiers() { return (int)d_quants.size(); } - /** get quantifier */ - Node getQuantifier( int i ) { return d_quants[i]; } -public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; } /** get term database */ |