diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-08 16:49:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-08 16:49:08 -0500 |
commit | d1ef66608567252526f1a5e1f675f08d342cc343 (patch) | |
tree | b9d539dd6ef13ad51d53869893d7024caa6b0559 /src/theory/quantifiers_engine.h | |
parent | a56575f413499d256e81f6ca1a64ffe1413ed3c7 (diff) |
Reorganize includes for quantifiers engine (#3169)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 110 |
1 files changed, 38 insertions, 72 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e0669c0d4..7e5fe9102 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,53 +17,33 @@ #ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H #define CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include <iostream> #include <map> -#include <memory> #include <unordered_map> #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "options/quantifiers_modes.h" -#include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" -#include "theory/quantifiers/conjecture_generator.h" -#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" -#include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/bounded_integers.h" -#include "theory/quantifiers/fmf/full_model_check.h" -#include "theory/quantifiers/fmf/model_engine.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/inst_propagator.h" -#include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_relevance.h" -#include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/theory.h" -#include "util/hash.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -72,6 +52,8 @@ class TheoryEngine; namespace theory { +class QuantifiersEnginePrivate; + // TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; @@ -97,16 +79,12 @@ public: const LogicInfo& getLogicInfo() const; //---------------------- end external interface //---------------------- utilities + /** get the master equality engine */ + eq::EqualityEngine* getMasterEqualityEngine() const; + /** get the active equality engine */ + eq::EqualityEngine* getActiveEqualityEngine() const; /** get equality query */ EqualityQuery* getEqualityQuery() const; - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() const; - /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() const; - /** get the BV inverter utility */ - quantifiers::BvInverter* getBvInverter() const; - /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() const; /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; /** get utility for EPR */ @@ -132,29 +110,49 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities - //---------------------- modules + //---------------------- utilities (TODO move these utilities #1163) + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() const; + /** get relevant domain */ + quantifiers::RelevantDomain* getRelevantDomain() const; + /** get the BV inverter utility */ + quantifiers::BvInverter* getBvInverter() const; + /** get quantifier relevance */ + quantifiers::QuantRelevance* getQuantifierRelevance() const; + //---------------------- end utilities + //---------------------- modules (TODO remove these #1163) /** get bounded integers utility */ quantifiers::BoundedIntegers* getBoundedIntegers() const; /** Conflict find mechanism for quantifiers */ quantifiers::QuantConflictFind* getConflictFind() const; - /** rewrite rules utility */ - quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ quantifiers::SynthEngine* getSynthEngine() const; - /** get full saturation */ - quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; //---------------------- end modules private: - /** owner of quantified formulas */ + /** + * Maps quantified formulas to the module that owns them, if any module has + * specifically taken ownership of it. + */ std::map< Node, QuantifiersModule * > d_owner; + /** + * The priority value associated with the ownership of quantified formulas + * in the domain of the above map, where higher values take higher + * precendence. + */ std::map< Node, int > d_owner_priority; public: /** get owner */ QuantifiersModule * getOwner( Node q ); - /** set owner */ + /** + * Set owner of quantified formula q to module m with given priority. If + * the quantified formula has previously been assigned an owner with + * lower priority, that owner is overwritten. + */ void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); + /** set owner of quantified formula q based on its attributes qa. */ + void setOwner(Node q, quantifiers::QAttributes& qa); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); /** is finite bound */ @@ -199,8 +197,6 @@ public: bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); - /** add EPR axiom */ - bool addEPRAxiom( TypeNode tn ); /** mark relevant quantified formula, this will indicate it should be checked before the others */ void markRelevant( Node q ); /** has added lemma */ @@ -225,10 +221,6 @@ public: void eqNotifyPreMerge(TNode t1, TNode t2); void eqNotifyPostMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine(); - /** get the active equality engine */ - eq::EqualityEngine* getActiveEqualityEngine(); /** use model equality engine */ bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ @@ -316,8 +308,6 @@ public: std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; /** equality inference class */ std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; - /** quantifiers instantiation propagtor */ - std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; /** all triggers will be stored in this trie */ std::unique_ptr<inst::TriggerTrie> d_tr_trie; /** extended model object */ @@ -349,34 +339,10 @@ public: /** term enumeration utility */ std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; //------------- end quantifiers utilities - //------------- quantifiers modules - /** alpha equivalence */ - std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; - /** instantiation engine */ - std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; - /** model engine */ - std::unique_ptr<quantifiers::ModelEngine> d_model_engine; - /** bounded integers utility */ - std::unique_ptr<quantifiers::BoundedIntegers> d_bint; - /** Conflict find mechanism for quantifiers */ - std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; - /** rewrite rules utility */ - std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; - /** subgoal generator */ - std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; - /** ceg instantiation */ - std::unique_ptr<quantifiers::SynthEngine> d_synth_e; - /** lte partial instantiation */ - std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; - /** full saturation */ - std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; - /** counterexample-based quantifier instantiation */ - std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi; - /** quantifiers splitting */ - std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; - /** quantifiers anti-skolemization */ - std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem; - //------------- end quantifiers modules + /** + * The private utility, which contains all of the quantifiers modules. + */ + std::unique_ptr<QuantifiersEnginePrivate> d_private; //------------- temporary information during check /** current effort level */ QuantifiersModule::QEffort d_curr_effort_level; |