From d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 1 Mar 2014 21:00:34 +0100 Subject: Added ezSAT::eliminated API to help the SAT solver remember eliminated variables --- libs/ezsat/ezsat.cc | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'libs/ezsat/ezsat.cc') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index cc6301e4..4389c7a6 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -348,9 +348,13 @@ void ezSAT::freeze(int) { } -void ezSAT::assume(int id) +bool ezSAT::eliminated(int) { + return false; +} +void ezSAT::assume(int id) +{ if (id < 0) { assert(0 < -id && -id <= int(expressions.size())); @@ -486,7 +490,7 @@ int ezSAT::bind(int id) if (id >= 0) { assert(0 < id && id <= int(literals.size())); cnfLiteralVariables.resize(literals.size()); - if (cnfLiteralVariables[id-1] == 0) { + if (cnfLiteralVariables[id-1] == 0 || eliminated(cnfLiteralVariables[id-1])) { cnfLiteralVariables[id-1] = ++cnfVariableCount; if (id == TRUE) add_clause(+cnfLiteralVariables[id-1]); @@ -499,7 +503,7 @@ int ezSAT::bind(int id) assert(0 < -id && -id <= int(expressions.size())); cnfExpressionVariables.resize(expressions.size()); - if (cnfExpressionVariables[-id-1] == 0) + if (cnfExpressionVariables[-id-1] == 0 || eliminated(cnfExpressionVariables[-id-1])) { OpId op; std::vector args; -- cgit v1.2.3