summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-12-29 17:10:37 +0100
committerClifford Wolf <clifford@clifford.at>2014-12-29 17:10:37 +0100
commit29a555ec7eaa0e561f76c65258a50c54b6468546 (patch)
tree74d48ff9a1623b617338956ace2d373643f80139
parent7a4d5d1c0fb78d49163160bfabb8cd1f5d1a2899 (diff)
Added statehash to ezSAT
-rw-r--r--libs/ezsat/ezsat.cc49
-rw-r--r--libs/ezsat/ezsat.h3
-rw-r--r--passes/opt/share.cc8
3 files changed, 52 insertions, 8 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index b713c4c9..1224fd3a 100644
--- a/libs/ezsat/ezsat.cc
+++ b/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;
}
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 5c8c1ed0..a20713bc 100644
--- a/libs/ezsat/ezsat.h
+++ b/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; }
diff --git a/passes/opt/share.cc b/passes/opt/share.cc
index e2c31bec..7ab50991 100644
--- a/passes/opt/share.cc
+++ b/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());