3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-05-05 09:55:16 +00:00
This commit is contained in:
Gus Smith 2026-02-06 17:26:08 -08:00
parent 9ed56ac72c
commit f062a0c8d6
5 changed files with 9 additions and 9 deletions

View file

@ -67,7 +67,7 @@ bool ezCmdlineSAT::solver(const std::vector<int> &modelExpressions, std::vector<
modelValues.resize(modelIdx.size()); modelValues.resize(modelIdx.size());
if (!status_sat && !status_unsat) { if (!status_sat && !status_unsat) {
solverTimoutStatus = true; solverTimeoutStatus = true;
} }
if (!status_sat) { if (!status_sat) {
return false; return false;

View file

@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
{ {
preSolverCallback(); preSolverCallback();
solverTimoutStatus = false; solverTimeoutStatus = false;
if (0) { if (0) {
contradiction: contradiction:
@ -206,7 +206,7 @@ contradiction:
#if defined(HAS_ALARM) #if defined(HAS_ALARM)
if (solverTimeout > 0) { if (solverTimeout > 0) {
if (alarmHandlerTimeout == 0) if (alarmHandlerTimeout == 0)
solverTimoutStatus = true; solverTimeoutStatus = true;
alarm(0); alarm(0);
sigaction(SIGALRM, &old_sig_action, NULL); sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout); alarm(old_alarm_timeout);

View file

@ -54,7 +54,7 @@ ezSAT::ezSAT()
cnfClausesCount = 0; cnfClausesCount = 0;
solverTimeout = 0; solverTimeout = 0;
solverTimoutStatus = false; solverTimeoutStatus = false;
literal("CONST_TRUE"); literal("CONST_TRUE");
literal("CONST_FALSE"); literal("CONST_FALSE");

View file

@ -78,7 +78,7 @@ protected:
public: public:
int solverTimeout; int solverTimeout;
bool solverTimoutStatus; bool solverTimeoutStatus;
ezSAT(); ezSAT();
virtual ~ezSAT(); virtual ~ezSAT();
@ -153,8 +153,8 @@ public:
solverTimeout = newTimeoutSeconds; solverTimeout = newTimeoutSeconds;
} }
bool getSolverTimoutStatus() { bool getSolverTimeoutStatus() {
return solverTimoutStatus; return solverTimeoutStatus;
} }
// manage CNF (usually only accessed by SAT solvers) // manage CNF (usually only accessed by SAT solvers)

View file

@ -441,7 +441,7 @@ struct SatHelper
log_assert(gotTimeout == false); log_assert(gotTimeout == false);
ez->setSolverTimeout(timeout); ez->setSolverTimeout(timeout);
bool success = ez->solve(modelExpressions, modelValues, assumptions); bool success = ez->solve(modelExpressions, modelValues, assumptions);
if (ez->getSolverTimoutStatus()) if (ez->getSolverTimeoutStatus())
gotTimeout = true; gotTimeout = true;
return success; return success;
} }
@ -451,7 +451,7 @@ struct SatHelper
log_assert(gotTimeout == false); log_assert(gotTimeout == false);
ez->setSolverTimeout(timeout); ez->setSolverTimeout(timeout);
bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f); bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
if (ez->getSolverTimoutStatus()) if (ez->getSolverTimeoutStatus())
gotTimeout = true; gotTimeout = true;
return success; return success;
} }