From cc9398dd55c414592affc67305b35569c1a6c9d2 Mon Sep 17 00:00:00 2001 From: Pascal Kesseli Date: Wed, 17 Jan 2018 21:55:27 +0100 Subject: [PATCH] Expose MiniSAT's `interrupt()` Makes MiniSAT's `interrupt()` and `clearInterrupt()` available to direct users. This allows aborting a running SAT query, e.g. in the context of multiple queries on different threads. Once this feature is required with other solvers as well, it may be useful to create a `virtual` function in `cnf_solvert` or even `prop_convt`, but for now this feature is uniquely required for our experiments with MiniSAT. --- src/solvers/sat/satcheck_minisat2.cpp | 12 ++++++++++++ src/solvers/sat/satcheck_minisat2.h | 6 ++++++ 2 files changed, 18 insertions(+) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 3f50091bbb6..43e41ce163d 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -81,6 +81,18 @@ void satcheck_minisat2_baset::set_polarity(literalt a, bool value) } } +template +void satcheck_minisat2_baset::interrupt() +{ + solver->interrupt(); +} + +template +void satcheck_minisat2_baset::clear_interrupt() +{ + solver->clearInterrupt(); +} + const std::string satcheck_minisat_no_simplifiert::solver_text() { return "MiniSAT 2.2.1 without simplifier"; diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h index cda5ab21bac..9834cdb11f8 100644 --- a/src/solvers/sat/satcheck_minisat2.h +++ b/src/solvers/sat/satcheck_minisat2.h @@ -42,6 +42,12 @@ class satcheck_minisat2_baset:public cnf_solvert // extra MiniSat feature: default branching decision void set_polarity(literalt a, bool value); + // extra MiniSat feature: interrupt running SAT query + void interrupt(); + + // extra MiniSat feature: permit previously interrupted SAT query to continue + void clear_interrupt(); + virtual bool is_in_conflict(literalt a) const override; virtual bool has_set_assumptions() const final { return true; } virtual bool has_is_in_conflict() const final { return true; }