projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 841acca) | patch
Add support for fewer preprocessing holes
authorAndres Notzli <andres.noetzli@gmail.com>
Wed, 10 Aug 2016 02:24:28 +0000 (19:24 -0700)
committerAndres Notzli <andres.noetzli@gmail.com>
Fri, 12 Aug 2016 06:28:15 +0000 (23:28 -0700)
commit1dddbc74f01619928263b42bf4b4ef6a6ccb2f28
tree9fed432f9e9bcb81dd3b015326d7fa7f73c197f1tree
parent841acca266b026c9c1d20cb1adf0e73da15a0c10commit | diff
Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.
src/options/proof_options diff | blob | history
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history