diff options
| -rw-r--r-- | libs/ezsat/ezsat.cc | 49 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.h | 3 | ||||
| -rw-r--r-- | passes/opt/share.cc | 8 |
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()); |