Added statehash to ezSAT

libs/ezsat/ezsat.cc

@@ -42,6 +42,8 @@ static std::string my_int_to_string(int i)
 
 ezSAT::ezSAT()
 {
+	statehash = 5381;
+
 	flag_keep_cnf = false;
 	flag_non_incremental = false;
 
@@ -65,6 +67,11 @@ ezSAT::~ezSAT()
 {
 }
 
+void ezSAT::addhash(unsigned int h)
+{
+	statehash = ((statehash << 5) + statehash) ^ h;
+}
+
 int ezSAT::value(bool val)
 {
 	return val ? CONST_TRUE : CONST_FALSE;
@@ -113,8 +120,14 @@ int ezSAT::expression(OpId op, const std::vector<int> &args)
 	myArgs.reserve(args.size());
 	bool xorRemovedOddTrues = false;
 
+	addhash(__LINE__);
+	addhash(op);
+
 	for (auto arg : args)
 	{
+		addhash(__LINE__);
+		addhash(arg);
+
 		if (arg == 0)
 			continue;
 		if (op == OpAnd && arg == CONST_TRUE)
@@ -200,7 +213,13 @@ int ezSAT::expression(OpId op, const std::vector<int> &args)
 		expressions.push_back(myExpr);
 	}
 
-	return xorRemovedOddTrues ? NOT(id) : id;
+	if (xorRemovedOddTrues)
+		id = NOT(id);
+
+	addhash(__LINE__);
+	addhash(id);
+
+	return id;
 }
 
 void ezSAT::lookup_literal(int id, std::string &name) const
@@ -387,6 +406,9 @@ bool ezSAT::eliminated(int)
 
 void ezSAT::assume(int id)
 {
+	addhash(__LINE__);
+	addhash(id);
+
 	if (id < 0)
 	{
 		assert(0 < -id && -id <= int(expressions.size()));
@@ -429,6 +451,10 @@ void ezSAT::assume(int id)
 
 void ezSAT::add_clause(const std::vector<int> &args)
 {
+	addhash(__LINE__);
+	for (auto arg : args)
+		addhash(arg);
+
 	cnfClauses.push_back(args);
 	cnfClausesCount++;
 }
@@ -519,6 +545,10 @@ std::string ezSAT::cnfLiteralInfo(int idx) const
 
 int ezSAT::bind(int id, bool auto_freeze)
 {
+	addhash(__LINE__);
+	addhash(id);
+	addhash(auto_freeze);
+
 	if (id >= 0) {
 		assert(0 < id && id <= int(literals.size()));
 		cnfLiteralVariables.resize(literals.size());
@@ -561,10 +591,13 @@ int ezSAT::bind(int id, bool auto_freeze)
 			while (args.size() > 1) {
 				std::vector<int> newArgs;
 				for (int i = 0; i < int(args.size()); i += 2)
-					if (i+1 == int(args.size()))
+					if (i+1 == int(args.size())) {
 						newArgs.push_back(args[i]);
-					else
-						newArgs.push_back(OR(AND(args[i], NOT(args[i+1])), AND(NOT(args[i]), args[i+1])));
+					} else {
+						int sub1 = AND(args[i], NOT(args[i+1]));
+						int sub2 = AND(NOT(args[i]), args[i+1]);
+						newArgs.push_back(OR(sub1, sub2));
+					}
 				args.swap(newArgs);
 			}
 			idx = bind(args.at(0), false);
@@ -575,12 +608,16 @@ int ezSAT::bind(int id, bool auto_freeze)
 			std::vector<int> invArgs;
 			for (auto arg : args)
 				invArgs.push_back(NOT(arg));
-			idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)), false);
+			int sub1 = expression(OpAnd, args);
+			int sub2 = expression(OpAnd, invArgs);
+			idx = bind(OR(sub1, sub2), false);
 			goto assign_idx;
 		}
 
 		if (op == OpITE) {
-			idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])), false);
+			int sub1 = AND(args[0], args[1]);
+			int sub2 = AND(NOT(args[0]), args[2]);
+			idx = bind(OR(sub1, sub2), false);
 			goto assign_idx;
 		}
 

libs/ezsat/ezsat.h

@@ -83,6 +83,9 @@ public:
 	ezSAT();
 	virtual ~ezSAT();
 
+	unsigned int statehash;
+	void addhash(unsigned int);
+
 	void keep_cnf() { flag_keep_cnf = true; }
 	void non_incremental() { flag_non_incremental = true; }
 

passes/opt/share.cc

@@ -1226,7 +1226,9 @@ struct ShareWorker
 				for (auto it : exclusive_ctrls)
 					if (satgen.importedSigBit(it.first) && satgen.importedSigBit(it.second)) {
 						log("      Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second));
-						ez.assume(ez.NOT(ez.AND(satgen.importSigBit(it.first), satgen.importSigBit(it.second))));
+						int sub1 = satgen.importSigBit(it.first);
+						int sub2 = satgen.importSigBit(it.second);
+						ez.assume(ez.NOT(ez.AND(sub1, sub2)));
 					}
 
 				if (!ez.solve(ez.expression(ez.OpOr, cell_active))) {
@@ -1248,7 +1250,9 @@ struct ShareWorker
 				std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
 				std::vector<bool> sat_model_values;
 
-				ez.assume(ez.AND(ez.expression(ez.OpOr, cell_active), ez.expression(ez.OpOr, other_cell_active)));
+				int sub1 = ez.expression(ez.OpOr, cell_active);
+				int sub2 = ez.expression(ez.OpOr, other_cell_active);
+				ez.assume(ez.AND(sub1, sub2));
 
 				log("      Size of SAT problem: %d cells, %d variables, %d clauses\n",
 						GetSize(sat_cells), ez.numCnfVariables(), ez.numCnfClauses());