diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 15:20:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 15:20:37 -0500 |
commit | 4b580ea3876055f701b13e67e0e4e78abbe47674 (patch) | |
tree | 35d1cd8f48077dfed5a5bae682f2efc90d80703f /src/theory/quantifiers_engine.h | |
parent | 13e452be03bef09e2f54f42e2bc42383505ffcea (diff) |
(Refactor) Split term util (#1303)
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index be0c4cd43..9743588a7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -50,10 +50,13 @@ public: namespace quantifiers { //TODO: organize this more/review this, github issue #1163 + //TODO: include these instead of doing forward declarations? #1307 //utilities class TermDb; class TermDbSygus; class TermUtil; + class Skolemize; + class TermEnumeration; class FirstOrderModel; class QuantAttributes; class RelevantDomain; @@ -132,6 +135,10 @@ private: quantifiers::TermUtil* d_term_util; /** quantifiers attributes */ std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; + /** skolemize utility */ + std::unique_ptr<quantifiers::Skolemize> d_skolemize; + /** term enumeration utility */ + std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; private: /** instantiation engine */ @@ -202,8 +209,6 @@ private: std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; /** recorded instantiations */ std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; - /** quantifiers that have been skolemized */ - BoolMap d_skolemized; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ @@ -385,6 +390,13 @@ public: quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr.get(); } + /** get skolemize utility */ + quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } + /** get term enumeration utility */ + quantifiers::TermEnumeration* getTermEnumeration() + { + return d_term_enum.get(); + } /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ @@ -402,7 +414,19 @@ public: void debugPrintEqualityEngine( const char * c ); /** get internal representative */ Node getInternalRepresentative( Node a, Node q, int index ); -public: + /** 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: /** print instantiations */ void printInstantiations( std::ostream& out ); /** print solution for synthesis conjectures */ |