projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d5de3d8) | patch
Simplify preprocessing (#5647)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Dec 2020 22:35:59 +0000 (16:35 -0600)
committerGitHub <noreply@github.com>
Wed, 16 Dec 2020 22:35:59 +0000 (16:35 -0600)
commitcd33db0a13ef195995885c4c42031386b2261ac4
treed3c03af37aa8c60741eb5c54e1122d9328374575tree
parentd5de3d822b978be11c98da5f026ab5f2ca9d0a83commit | diff
Simplify preprocessing (#5647)

This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).

This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.

@HanielB has done SMT-LIB performance runs, see below.
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/unconstrained_simplifier.cpp diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/process_assertions.h diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
test/regress/regress0/unconstrained/4481.smt2 diff | blob | history