diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:23:51 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:24:02 -0600 |
commit | d0add0eb12cac4e9cbcf09fe60724d280889002d (patch) | |
tree | 217528663e877f15832a5cb00005e5a15a69f2ee /src/theory/quantifiers_engine.h | |
parent | 160572318e251a98a58b3f506c31fb233070d477 (diff) |
More optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ee7e6e6d8..9d341194f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -68,6 +68,7 @@ namespace quantifiers { class BoundedIntegers; class QuantConflictFind; class RewriteEngine; + class RelevantDomain; }/* CVC4::theory::quantifiers */ namespace inst { @@ -95,7 +96,9 @@ private: /** equality query class */ EqualityQueryQuantifiersEngine* d_eq_query; /** for computing relevance of quantifiers */ - QuantRelevance d_quant_rel; + QuantRelevance * d_quant_rel; + /** relevant domain */ + quantifiers::RelevantDomain* d_rel_dom; /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; /** efficient e-matcher */ @@ -121,7 +124,8 @@ private: /** has added lemma this round */ bool d_hasAddedLemma; /** list of all instantiations produced for each quantifier */ - std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie; + std::map< Node, inst::InstMatchTrie > d_inst_match_trie; + std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; /** term database */ quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ @@ -158,8 +162,10 @@ public: OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ Valuation& getValuation(); + /** get relevant domain */ + quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } /** get quantifier relevance */ - QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; } + QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } /** get phase requirement information */ QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ |