diff options
Diffstat (limited to 'src/prop/sat.h')
| -rw-r--r-- | src/prop/sat.h | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index ee3978555..026193eae 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -114,6 +114,8 @@ public: virtual void unregisterVar(SatLiteral lit) = 0; /** Register the variable (of the literal) for solving */ virtual void renewVar(SatLiteral lit, int level = -1) = 0; + /** Interrupt the solver */ + virtual void interrupt() = 0; }; /** @@ -214,7 +216,7 @@ public: virtual ~SatSolver(); - bool solve(); + SatLiteralValue solve(unsigned long& resource); void addClause(SatClause& clause, bool removable); @@ -253,6 +255,8 @@ public: void renewVar(SatLiteral lit, int level = -1); + void interrupt(); + TNode getNode(SatLiteral lit); void notifyRestart(); @@ -261,6 +265,8 @@ public: void logDecision(SatLiteral lit); + void checkTime(); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ @@ -293,8 +299,20 @@ inline SatSolver::~SatSolver() { delete d_minisat; } -inline bool SatSolver::solve() { - return d_minisat->solve(); +inline SatLiteralValue SatSolver::solve(unsigned long& resource) { + Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + if(resource == 0) { + d_minisat->budgetOff(); + } else { + d_minisat->setConfBudget(resource); + } + Minisat::vec<SatLiteral> empty; + unsigned long conflictsBefore = d_minisat->conflicts; + SatLiteralValue result = d_minisat->solveLimited(empty); + d_minisat->clearInterrupt(); + resource = d_minisat->conflicts - conflictsBefore; + Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; + return result; } inline void SatSolver::addClause(SatClause& clause, bool removable) { @@ -333,6 +351,10 @@ inline void SatSolver::renewVar(SatLiteral lit, int level) { d_minisat->renewVar(lit, level); } +inline void SatSolver::interrupt() { + d_minisat->interrupt(); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t |