projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 437c346) | patch
Refactoring initialization of proofs (#7834)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 17 Dec 2021 19:43:36 +0000 (13:43 -0600)
committerGitHub <noreply@github.com>
Fri, 17 Dec 2021 19:43:36 +0000 (19:43 +0000)
commitd7cb2cd925220e063a67c7eed6f829520b58ce53
tree2b654d54ea09d4ad0f9b9f82be88527b85951640tree
parent437c346559d920edcd19c28777747093ceba4e20commit | diff
Refactoring initialization of proofs (#7834)

Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.
16 files changed:
src/preprocessing/assertion_pipeline.cpp diff | blob | history
src/preprocessing/assertion_pipeline.h diff | blob | history
src/preprocessing/passes/non_clausal_simp.cpp diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/assertions.h diff | blob | history
src/smt/expand_definitions.cpp diff | blob | history
src/smt/expand_definitions.h diff | blob | history
src/smt/preprocess_proof_generator.cpp diff | blob | history
src/smt/preprocess_proof_generator.h diff | blob | history
src/smt/preprocessor.cpp diff | blob | history
src/smt/preprocessor.h diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
src/smt/solver_engine.h diff | blob | history
src/theory/booleans/circuit_propagator.cpp diff | blob | history
src/theory/booleans/circuit_propagator.h diff | blob | history