(proof-new) Update add lazy step interface in LazyCDProof (#5299)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 20 Oct 2020 20:20:35 +0000 (15:20 -0500)
committerGitHub <noreply@github.com>
Tue, 20 Oct 2020 20:20:35 +0000 (15:20 -0500)
commit656004c54655ab15289d9e7666bda2e1c7bada1c
tree23d53585f8204a30fe42b35e91824901e6dc4e2c
parent417299119500eac6a910fcb6b2109f4c129b355c
(proof-new) Update add lazy step interface in LazyCDProof (#5299)

Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.

Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
15 files changed:
src/expr/lazy_proof.cpp
src/expr/lazy_proof.h
src/expr/term_conversion_proof_generator.cpp
src/expr/term_conversion_proof_generator.h
src/preprocessing/assertion_pipeline.cpp
src/prop/proof_cnf_stream.cpp
src/smt/proof_post_processor.cpp
src/smt/term_formula_removal.cpp
src/smt/witness_form.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/theory_engine.cpp
src/theory/theory_preprocessor.cpp
src/theory/trust_substitutions.cpp
src/theory/trust_substitutions.h
src/theory/uf/proof_equality_engine.cpp