diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8f645afe7..6de13ff3c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -111,7 +111,7 @@ private: /** list of all quantifiers seen */ std::vector< Node > d_quants; /** list of all lemmas produced */ - std::map< Node, bool > d_lemmas_produced; + //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; @@ -187,6 +187,8 @@ private: bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ void setInstantiationLevelAttr( Node n, uint64_t level ); + /** do substitution */ + Node doSubstitute( Node n, std::vector< Node >& terms ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -234,12 +236,8 @@ public: IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; IntStat d_instantiations; - IntStat d_max_instantiation_level; - IntStat d_splits; - IntStat d_total_inst_var; - IntStat d_total_inst_var_unspec; - IntStat d_inst_unspec; IntStat d_inst_duplicate; + IntStat d_inst_duplicate_eq; IntStat d_lit_phase_req; IntStat d_lit_phase_nreq; IntStat d_triggers; |