From: bdemsky <bdemsky@uci.edu>
Date: Thu, 7 Nov 2019 23:21:32 +0000 (-0800)
Subject: Don't reencode expressions that are already encoded
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=b4cf68cef113d8e869586f2447a2e49ba91dbf3c

Don't reencode expressions that are already encoded
---

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index e3d1305..f2b8bd1 100644
--- 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 fe84a2b..b07fd2f 100644
--- 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