diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 65d3697b7..a65d55859 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -71,6 +71,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -4283,6 +4284,13 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); + if (options::symmetryDetect()) + { + SymmetryDetect symd; + vector<vector<Node>> part; + symd.getPartition(part, d_assertions.ref()); + } + dumpAssertions("pre-static-learning", d_assertions); if(options::doStaticLearning()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl; |