Symmetry detection module (#1749)

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;