diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 14:59:40 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-11 20:59:40 +0000 |
commit | 3d9daccc198844c24c8014f1fff31a64714b3dff (patch) | |
tree | d60ce10253aab175b004f7ae1576bd3b5a31c56a /src/theory/quantifiers_engine.cpp | |
parent | 42d5d8950d849aa4b855aa62834cd5fdee1a91a8 (diff) |
Introduce inference ids for quantifier instantiation (#6119)
This makes quantifiers use standard inference ids.
This eliminates the need to track ad-hoc statistics, per instantiation type.
This makes minor modifications to a few interfaces in quantifiers to enable this.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 35 |
1 files changed, 3 insertions, 32 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 401857206..24919fae0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -767,21 +767,12 @@ QuantifiersEngine::Statistics::Statistics() d_ematching_time("theory::QuantifiersEngine::time_ematching"), d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), + d_instantiation_rounds_lc( + "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), - d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), - d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), - d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0), - d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0), - d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0), - d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0), - d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0), - d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0) + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) { smtStatisticsRegistry()->registerStat(&d_time); smtStatisticsRegistry()->registerStat(&d_qcf_time); @@ -792,17 +783,7 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); - smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns); - smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen); - smtStatisticsRegistry()->registerStat(&d_instantiations_guess); - smtStatisticsRegistry()->registerStat(&d_instantiations_qcf); - smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop); - smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh); - smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi); - smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi); - smtStatisticsRegistry()->registerStat(&d_instantiations_rr); } QuantifiersEngine::Statistics::~Statistics(){ @@ -815,17 +796,7 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); - smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr); } Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ |