diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-04 14:19:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-04 19:19:51 +0000 |
| commit | e29a86f380354371dee1e5032034a2fe5edfee16 (patch) | |
| tree | 0f076b97e4f150f3165275e733b4dc2c87253172 /src/smt/proof_post_processor.h | |
| parent | 7f14a11349dae074b4f307488d0289e2fd7043e9 (diff) | |
Add optional debug information for dumping instantiations (#6950)
This complete the implementation of dump-instantiations-debug.
With this option, we can print the source of instantiations. For example:
$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)
Diffstat (limited to 'src/smt/proof_post_processor.h')
| -rw-r--r-- | src/smt/proof_post_processor.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index f9e93fa91..056f77695 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -24,6 +24,7 @@ #include "proof/proof_node_updater.h" #include "smt/witness_form.h" +#include "theory/inference_id.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -256,6 +257,11 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback private: /** Counts number of postprocessed proof nodes for each kind of proof rule */ HistogramStat<PfRule> d_ruleCount; + /** + * Counts number of postprocessed proof nodes of rule INSTANTIATE that were + * marked with the given inference id. + */ + HistogramStat<theory::InferenceId> d_instRuleIds; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ |