mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-15 03:35:40 +00:00
Code Activity

ezsat add propagation budget api.

Browse source
This commit is contained in:
nella 2026-07-11 12:23:03 +02:00
parent b35b6706f8
commit b148993f7b
3 changed files with 37 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

19
libs/ezsat/ezminisat.cc
View file

@ -104,6 +104,8 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
preSolverCallback();
solverTimeoutStatus = false;
solverPropLimitStatus = false;
solverProps = 0;
if (0) {
contradiction:
@ -201,7 +203,21 @@ contradiction:
}
#endif
bool foundSolution = minisatSolver->solve(assumps);
uint64_t solverPropsBefore = minisatSolver->propagations;
bool foundSolution;
if (solverPropLimit > 0) {
minisatSolver->setPropBudget(solverPropLimit);
Minisat::lbool res = minisatSolver->solveLimited(assumps);
minisatSolver->budgetOff();
if (Minisat::toInt(res) == 2) // l_Undef: propagation budget exhausted
solverPropLimitStatus = true;
foundSolution = (Minisat::toInt(res) == 0); // l_True
} else {
foundSolution = minisatSolver->solve(assumps);
}
solverProps = minisatSolver->propagations - solverPropsBefore;
#if defined(HAS_ALARM)
if (solverTimeout > 0) {
@ -210,6 +226,7 @@ contradiction:
alarm(0);
sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout);
minisatSolver->clearInterrupt();
}
#endif

3
libs/ezsat/ezsat.cc
View file

@ -55,6 +55,9 @@ ezSAT::ezSAT()
solverTimeout = 0;
solverTimeoutStatus = false;
solverPropLimit = 0;
solverPropLimitStatus = false;
solverProps = 0;
literal("CONST_TRUE");
literal("CONST_FALSE");

16
libs/ezsat/ezsat.h
View file

@ -79,6 +79,9 @@ protected:
public:
int solverTimeout;
bool solverTimeoutStatus;
int64_t solverPropLimit;
bool solverPropLimitStatus;
int64_t solverProps;
ezSAT();
virtual ~ezSAT();
@ -157,6 +160,19 @@ public:
return solverTimeoutStatus;
}
void setSolverPropLimit(int64_t newPropLimit) {
solverPropLimit = newPropLimit;
}
bool getSolverPropLimitStatus() {
return solverPropLimitStatus;
}
// propagations spent by the most recent solve() call
int64_t getSolverProps() {
return solverProps;
}
// manage CNF (usually only accessed by SAT solvers)
virtual void clear();