diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/prop/sat.h | |
parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
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 |