Integrate learned rewrite preprocessing pass (#6840)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 6 Jul 2021 22:44:09 +0000 (17:44 -0500)
committerGitHub <noreply@github.com>
Tue, 6 Jul 2021 22:44:09 +0000 (17:44 -0500)
commit4ac6c5179265ef9895bc9e939be0e47b3754137e
treebf2cd175a534e5ca9a383a63cd6a086f1d5f45d0
parentb023494b8914be03d8f8ca26c1b1db332944f3fe
Integrate learned rewrite preprocessing pass (#6840)

This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.
src/CMakeLists.txt
src/options/smt_options.toml
src/preprocessing/passes/learned_rewrite.cpp
src/preprocessing/preprocessing_pass_registry.cpp
src/smt/process_assertions.cpp
src/smt/set_defaults.cpp