diff options
Diffstat (limited to 'libs/ezsat/ezsat.cc')
| -rw-r--r-- | libs/ezsat/ezsat.cc | 33 |
1 files changed, 27 insertions, 6 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 57762525..e6c005c6 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -29,18 +29,18 @@ const int ezSAT::FALSE = 2; ezSAT::ezSAT() { - literal("TRUE"); - literal("FALSE"); - - assert(literal("TRUE") == TRUE); - assert(literal("FALSE") == FALSE); - cnfConsumed = false; cnfVariableCount = 0; cnfClausesCount = 0; solverTimeout = 0; solverTimoutStatus = false; + + freeze(literal("TRUE")); + freeze(literal("FALSE")); + + assert(literal("TRUE") == TRUE); + assert(literal("FALSE") == FALSE); } ezSAT::~ezSAT() @@ -345,6 +345,10 @@ void ezSAT::clear() cnfAssumptions.clear(); } +void ezSAT::freeze(int) +{ +} + void ezSAT::assume(int id) { cnfAssumptions.insert(id); @@ -462,6 +466,23 @@ int ezSAT::bound(int id) const return 0; } +std::string ezSAT::cnfLiteralInfo(int idx) const +{ + for (size_t i = 0; i < cnfLiteralVariables.size(); i++) { + if (cnfLiteralVariables[i] == idx) + return to_string(i+1); + if (cnfLiteralVariables[i] == -idx) + return "NOT " + to_string(i+1); + } + for (size_t i = 0; i < cnfExpressionVariables.size(); i++) { + if (cnfExpressionVariables[i] == idx) + return to_string(-i-1); + if (cnfExpressionVariables[i] == -idx) + return "NOT " + to_string(-i-1); + } + return "<unnamed>"; +} + int ezSAT::bind(int id) { if (id >= 0) { |