projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e4d9d23) | patch
(proof-new) Update preprocessing pass context for proofs (#5298)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 19 Oct 2020 16:06:16 +0000 (11:06 -0500)
committerGitHub <noreply@github.com>
Mon, 19 Oct 2020 16:06:16 +0000 (11:06 -0500)
commita8e839e29325f06ecd2d5dda7d8f64a44ddafb0c
tree1cae41ba9583546dfa08590469a93d8fd8c2bb7btree
parente4d9d23f37f40705961b6c58c59fefb6a443eba9commit | diff
(proof-new) Update preprocessing pass context for proofs (#5298)

This sets up the preprocessing pass context in preparation for proof production.

This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.

This PR also makes the "apply subst" preprocessing pass proof producing.
src/preprocessing/assertion_pipeline.cpp diff | blob | history
src/preprocessing/passes/apply_substs.cpp diff | blob | history
src/preprocessing/passes/miplib_trick.cpp diff | blob | history
src/preprocessing/passes/non_clausal_simp.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.h diff | blob | history
src/smt/preprocessor.cpp diff | blob | history
src/smt/preprocessor.h diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history