Remove experimental symmetry breaker (#4005)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Mar 2020 18:01:42 +0000 (13:01 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Mar 2020 18:01:42 +0000 (11:01 -0700)
commit8a56e62da0a8940f0ae1ee9575398e5f21660097
tree81a1610923265f0ece570f47edd964ac531776e6
parentac5ef49e14154daee4200783b57584febb726a4e
Remove experimental symmetry breaker (#4005)

This never impacted performance positively. Fixes #3997 and fixes #4015.

There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
20 files changed:
src/CMakeLists.txt
src/options/smt_options.toml
src/preprocessing/passes/symmetry_breaker.cpp [deleted file]
src/preprocessing/passes/symmetry_breaker.h [deleted file]
src/preprocessing/passes/symmetry_detect.cpp [deleted file]
src/preprocessing/passes/symmetry_detect.h [deleted file]
src/preprocessing/preprocessing_pass_registry.cpp
src/smt/smt_engine.cpp
test/regress/regress1/sym/q-constant.smt2
test/regress/regress1/sym/q-function.smt2
test/regress/regress1/sym/qf-function.smt2
test/regress/regress1/sym/sb-wrong.smt2
test/regress/regress1/sym/sym-setAB.smt2
test/regress/regress1/sym/sym1.smt2
test/regress/regress1/sym/sym2.smt2
test/regress/regress1/sym/sym3.smt2
test/regress/regress1/sym/sym4.smt2
test/regress/regress1/sym/sym5.smt2
test/regress/regress1/sym/sym6.smt2
test/regress/regress1/sym/sym7-uf.smt2