Remove --apply-to-const preprocessing pass (#3919)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 6 Mar 2020 01:23:45 +0000 (17:23 -0800)
committerGitHub <noreply@github.com>
Fri, 6 Mar 2020 01:23:45 +0000 (17:23 -0800)
commitba6ade0fc3f4cd339885652bb9bf5c87113c498d
tree5823f632aca0903109d7ccabedffeae65ac6f637
parente1845f92742854a35c294541bd931b898b0211d2
Remove --apply-to-const preprocessing pass (#3919)

Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.
src/CMakeLists.txt
src/options/smt_options.toml
src/preprocessing/passes/apply_to_const.cpp [deleted file]
src/preprocessing/passes/apply_to_const.h [deleted file]
src/preprocessing/preprocessing_pass_registry.cpp
src/smt/smt_engine.cpp
test/regress/regress0/arith/apply2const-test.smt2 [deleted file]