diff options
author | Clifford Wolf <clifford@clifford.at> | 2013-06-07 14:37:33 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2013-06-07 14:37:33 +0200 |
commit | 56b593b91cc693849e3b3b3de0666f6ec9a597f6 (patch) | |
tree | ccaa7c501a228f4056b887370682f054c81aea48 /libs/ezsat/ezsat.cc | |
parent | 46fbe9d26299a7b6197463b3056d778f525658fb (diff) |
Improved sat generator and sat_solve pass
Diffstat (limited to 'libs/ezsat/ezsat.cc')
-rw-r--r-- | libs/ezsat/ezsat.cc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index d6ebd678..cf9dd65b 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -34,6 +34,7 @@ ezSAT::ezSAT() cnfConsumed = false; cnfVariableCount = 0; + cnfClausesCount = 0; } ezSAT::~ezSAT() @@ -331,6 +332,7 @@ void ezSAT::clear() { cnfConsumed = false; cnfVariableCount = 0; + cnfClausesCount = 0; cnfLiteralVariables.clear(); cnfExpressionVariables.clear(); cnfClauses.clear(); @@ -342,11 +344,13 @@ void ezSAT::assume(int id) int idx = bind(id); cnfClauses.push_back(std::vector<int>(1, idx)); cnfAssumptions.insert(id); + cnfClausesCount++; } void ezSAT::add_clause(const std::vector<int> &args) { cnfClauses.push_back(args); + cnfClausesCount++; } void ezSAT::add_clause(const std::vector<int> &args, bool argsPolarity, int a, int b, int c) |