riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option

This commit is contained in:
Clifford Wolf 2014-02-22 11:34:31 +01:00
parent 1ec01d8c63
commit 357f3f6e93
2 changed files with 17 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libs/ezsat/ezminisat.cc
View File

@ -96,8 +96,12 @@ contradiction:
minisatSolver->verbosity = EZMINISAT_VERBOSITY; minisatSolver->verbosity = EZMINISAT_VERBOSITY;
} }
#if EZMINISAT_INCREMENTAL
std::vector<std::vector<int>> cnf; std::vector<std::vector<int>> cnf;
consumeCnf(cnf); consumeCnf(cnf);
#else
const std::vector<std::vector<int>> &cnf = this->cnf();
#endif
while (int(minisatVars.size()) < numCnfVariables()) while (int(minisatVars.size()) < numCnfVariables())
minisatVars.push_back(minisatSolver->newVar()); minisatVars.push_back(minisatSolver->newVar());
@ -145,8 +149,14 @@ contradiction:
alarm(old_alarm_timeout); alarm(old_alarm_timeout);
} }
if (!foundSolution) if (!foundSolution) {
#if !EZMINISAT_INCREMENTAL
delete minisatSolver;
minisatSolver = NULL;
minisatVars.clear();
#endif
return false; return false;
}
modelValues.clear(); modelValues.clear();
modelValues.resize(modelIdx.size()); modelValues.resize(modelIdx.size());
@ -164,6 +174,11 @@ contradiction:
modelValues[i] = (value == Minisat::lbool(refvalue)); modelValues[i] = (value == Minisat::lbool(refvalue));
} }
#if !EZMINISAT_INCREMENTAL
delete minisatSolver;
minisatSolver = NULL;
minisatVars.clear();
#endif
return true; return true;
} }

1
libs/ezsat/ezminisat.h
View File

@ -22,6 +22,7 @@
#define EZMINISAT_SOLVER Minisat::Solver #define EZMINISAT_SOLVER Minisat::Solver
#define EZMINISAT_VERBOSITY 0 #define EZMINISAT_VERBOSITY 0
#define EZMINISAT_INCREMENTAL 1
#include "ezsat.h" #include "ezsat.h"
#include <time.h> #include <time.h>