diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-24 19:08:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-24 19:08:41 -0600 |
commit | 3ab0db55341e7e752411bb003fb203fcd9ec9120 (patch) | |
tree | df79841a5e8244ea159ccc4a5e32c9e9d5fee2dc /src/theory/quantifiers_engine.h | |
parent | bb095659fb12e3733a73f1be31769ff5b5eb6055 (diff) |
(Refactor) Instantiate utility (#1387)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 105 |
1 files changed, 30 insertions, 75 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 37691488e..6c7820cef 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -40,18 +40,6 @@ namespace theory { class QuantifiersEngine; -class InstantiationNotify { -public: - InstantiationNotify(){} - virtual ~InstantiationNotify() {} - virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, - Node q, - Node lem, - std::vector<Node>& terms, - Node body) = 0; - virtual void filterInstantiations() = 0; -}; - namespace quantifiers { //TODO: organize this more/review this, github issue #1163 //TODO: include these instead of doing forward declarations? #1307 @@ -59,6 +47,7 @@ namespace quantifiers { class TermDb; class TermDbSygus; class TermUtil; + class Instantiate; class Skolemize; class TermEnumeration; class FirstOrderModel; @@ -97,6 +86,7 @@ namespace inst { class QuantifiersEngine { + // TODO: remove these github issue #1163 friend class quantifiers::InstantiationEngine; friend class quantifiers::InstStrategyCbqi; friend class quantifiers::InstStrategyCegqi; @@ -115,8 +105,6 @@ private: std::vector< QuantifiersUtil* > d_util; /** vector of modules for quantifiers */ std::vector< QuantifiersModule* > d_modules; - /** instantiation notify */ - std::vector< InstantiationNotify* > d_inst_notify; /** equality query class */ quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; /** equality inference class */ @@ -141,6 +129,8 @@ private: quantifiers::TermUtil* d_term_util; /** quantifiers attributes */ std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; + /** instantiate utility */ + std::unique_ptr<quantifiers::Instantiate> d_instantiate; /** skolemize utility */ std::unique_ptr<quantifiers::Skolemize> d_skolemize; /** term enumeration utility */ @@ -199,19 +189,10 @@ private: std::vector< Node > d_lemmas_waiting; /** phase requirements waiting */ std::map< Node, bool > d_phase_req_waiting; - /** list of all instantiations produced for each quantifier */ - std::map< Node, inst::InstMatchTrie > d_inst_match_trie; - std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; - /** recorded instantiations */ - std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** statistics for debugging */ - std::map< Node, int > d_total_inst_debug; - std::map< Node, int > d_temp_inst_debug; - int d_total_inst_count_debug; /** inst round counters TODO: make context-dependent? */ context::CDO< int > d_ierCounter_c; int d_ierCounter; @@ -319,37 +300,15 @@ public: private: /** reduceQuantifier, return true if reduced */ bool reduceQuantifier( Node q ); - /** compute term vector */ - void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); - /** record instantiation, return true if it was non-duplicate */ - bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true ); - /** remove instantiation */ - bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); - /** set instantiation level attr */ - static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ void flushLemmas(); public: - /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); - /** get instantiation */ - Node getInstantiation( Node q, InstMatch& m, bool doVts = false ); - /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false ); - /** do substitution */ - Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); /** remove pending lemma */ bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); - /** do instantiation specified by m */ - bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false ); - /** add instantiation */ - bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false ); - /** remove pending instantiation */ - bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ @@ -364,14 +323,14 @@ public: bool inConflict() { return d_conflict; } /** set conflict */ void setConflict(); + /** get current q effort */ + QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); /** get user pat mode */ quantifiers::UserPatMode getInstUserPatMode(); - /** set instantiation level attr */ - static void setInstantiationLevelAttr( Node n, uint64_t level ); public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; } @@ -385,6 +344,8 @@ public: quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr.get(); } + /** get instantiate utility */ + quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); } /** get skolemize utility */ quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } /** get term enumeration utility */ @@ -405,42 +366,41 @@ public: 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 */ void debugPrintEqualityEngine( const char * c ); /** get internal representative */ Node getInternalRepresentative( Node a, Node q, int index ); - /** get term for type - * - * This returns an arbitrary term for type tn. - * This term is chosen heuristically to be the best - * term for instantiation. Currently, this - * heuristic enumerates the first term of the - * type if the type is closed enumerable, otherwise - * an existing ground term from the term database if - * one exists, or otherwise a fresh variable. - */ - Node getTermForType(TypeNode tn); public: + //----------user interface for instantiations (see quantifiers/instantiate.h) /** print instantiations */ - void printInstantiations( std::ostream& out ); + void printInstantiations(std::ostream& out); /** print solution for synthesis conjectures */ - void printSynthSolution( std::ostream& out ); + void printSynthSolution(std::ostream& out); /** get list of quantified formulas that were instantiated */ - void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); + void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); /** get instantiations */ - void getInstantiations( Node q, std::vector< Node >& insts ); - void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + void getInstantiations(Node q, std::vector<Node>& insts); + void getInstantiations(std::map<Node, std::vector<Node> >& insts); /** get instantiation term vectors */ - void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); - void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); + void getInstantiationTermVectors(Node q, + std::vector<std::vector<Node> >& tvecs); + void getInstantiationTermVectors( + std::map<Node, std::vector<std::vector<Node> > >& insts); /** get instantiated conjunction */ - Node getInstantiatedConjunction( Node q ); + Node getInstantiatedConjunction(Node q); /** get unsat core lemmas */ - bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas ); - bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ); - /** get inst for lemmas */ - void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); + bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas); + bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas, + std::map<Node, Node>& weak_imp); + /** get explanation for instantiation lemmas */ + void getExplanationForInstLemmas(const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec); + //----------end user interface for instantiations + /** statistics class */ class Statistics { public: @@ -450,11 +410,6 @@ public: IntStat d_num_quant; IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; - IntStat d_instantiations; - IntStat d_inst_duplicate; - IntStat d_inst_duplicate_eq; - IntStat d_inst_duplicate_ent; - IntStat d_inst_duplicate_model_true; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; |