projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 119516a) | patch
Track instantiation reasons in proofs (#6935)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 27 Jul 2021 17:24:17 +0000 (12:24 -0500)
committerGitHub <noreply@github.com>
Tue, 27 Jul 2021 17:24:17 +0000 (17:24 +0000)
commit3a180a2f8ffe8ad5756119ce0cbe61ab4ab28127
tree228409a37f4cd24c752244a5f71bea4e8199490btree
parent119516a98c052e79ad55e126d13ce1ded38f90afcommit | diff
Track instantiation reasons in proofs (#6935)

This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.

Also simplifies an old argument modEq which was unused.

FYI @MikolasJanota
13 files changed:
src/proof/proof_rule.h diff | blob | history
src/smt/unsat_core_manager.cpp diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.h diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/model_builder.h diff | blob | history
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/proof_checker.cpp diff | blob | history