Add optional debug information for dumping instantiations (#6950)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Aug 2021 19:19:51 +0000 (14:19 -0500)
committerGitHub <noreply@github.com>
Wed, 4 Aug 2021 19:19:51 +0000 (19:19 +0000)
commite29a86f380354371dee1e5032034a2fe5edfee16
tree0f076b97e4f150f3165275e733b4dc2c87253172
parent7f14a11349dae074b4f307488d0289e2fd7043e9
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))))
)
14 files changed:
src/main/command_executor.cpp
src/options/main_options.toml
src/printer/printer.cpp
src/smt/proof_post_processor.cpp
src/smt/proof_post_processor.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/unsat_core_manager.cpp
src/smt/unsat_core_manager.h
src/theory/inference_id.cpp
src/theory/inference_id.h
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/instantiation_list.cpp
src/theory/quantifiers/instantiation_list.h