diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
commit | 5ebe47d38892131b96521a729c915365a3369110 (patch) | |
tree | 59e8f2f3b9de3a9f81e178de7d18124ddc4f3c32 /src/theory/quantifiers_engine.h | |
parent | 304404e3709ff7e95156c87f65a3e2647d9f3441 (diff) |
efficient e-matching now specific to rewrite rules
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 18635a823..f9c016cb9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -66,6 +66,8 @@ namespace inst { class TriggerTrie; }/* CVC4::theory::inst */ +class EfficientEMatcher; + class QuantifiersEngine { friend class quantifiers::InstantiationEngine; friend class quantifiers::ModelEngine; @@ -86,6 +88,8 @@ private: QuantRelevance d_quant_rel; /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; + /** efficient e-matcher */ + EfficientEMatcher* d_eem; private: /** list of all quantifiers seen */ std::vector< Node > d_quants; @@ -131,6 +135,8 @@ public: QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); + /** get efficient e-matching utility */ + EfficientEMatcher* getEfficientEMatcher() { return d_eem; } public: /** check at level */ void check( Theory::Effort e ); |