From 8a56e62da0a8940f0ae1ee9575398e5f21660097 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Mar 2020 13:01:42 -0500 Subject: 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. --- src/smt/smt_engine.cpp | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bfb126e9e..e4e582b6e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3454,12 +3454,6 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); - if (options::symmetryBreakerExp() && !options::incrementalSolving()) - { - // apply symmetry breaking if not in incremental mode - d_passes["sym-break"]->apply(&d_assertions); - } - if(options::doStaticLearning()) { d_passes["static-learning"]->apply(&d_assertions); } -- cgit v1.2.3