Don't reencode expressions that are already encoded

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index e3d13050ab416d67fe06b1c69fe25969a02cbdb3..f2b8bd15fb34125f06ad4323ec515d4ad4178296 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -18,15 +18,17 @@ void naiveEncodingDecision(CSolver *This) {
        if (This->isUnSAT()) {
                return;
        }
+       HashsetBoolean *visited = new HashsetBoolean();
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge b = iterator->next();
-               naiveEncodingConstraint(This, b.getBoolean());
+               naiveEncodingConstraint(This, visited, b.getBoolean());
        }
        delete iterator;
+       delete visited;
 }
 
-void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
+void naiveEncodingConstraint(CSolver *csolver, HashsetBoolean *visited, Boolean *This) {
        switch (This->type) {
        case BOOLEANVAR: {
                return;
@@ -37,7 +39,7 @@ void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
                return;
        }
        case LOGICOP: {
-               naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
+               naiveEncodingLogicOp(csolver, visited, (BooleanLogic *) This);
                return;
        }
        case PREDICATEOP: {
@@ -49,9 +51,12 @@ void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
        }
 }
 
-void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, HashsetBoolean *visited, BooleanLogic *This) {
+       if (!visited->add(This))
+               return;
+
        for (uint i = 0; i < This->inputs.getSize(); i++) {
-               naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
+               naiveEncodingConstraint(csolver, visited, This->inputs.get(i).getBoolean());
        }
 }
 

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index fe84a2b64eb874b13fc6ba284e1dba3080feb5b6..b07fd2fb0470e7c356d8bcca64c321799242ce36 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -10,8 +10,8 @@
  */
 
 void naiveEncodingDecision(CSolver *csolver);
-void naiveEncodingConstraint(CSolver *csolver, Boolean *This);
-void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This);
+void naiveEncodingConstraint(CSolver *csolver, HashsetBoolean *visited, Boolean *This);
+void naiveEncodingLogicOp(CSolver *csolver, HashsetBoolean *visited, BooleanLogic *This);
 void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This);
 void naiveEncodingElement(CSolver *csolver, Element *This);
 #endif