Extend the coverage of stopping the solver

src/api/MainSolver.cc

@@ -459,6 +459,11 @@ std::unique_ptr<SimpSMTSolver> MainSolver::createInnerSolver(SMTConfig & config,
     }
 }
 
+void MainSolver::notifyStop() {
+    smt_solver->notifyStop();
+    theory->getTSolverHandler().notifyStop();
+}
+
 void MainSolver::setTimeLimit(std::chrono::milliseconds limit, TimeLimitConf const & conf) {
     if (limit <= std::chrono::milliseconds::zero()) {
         throw std::invalid_argument{"MainSolver::setTimeLimit: The value must be positive."};

src/api/MainSolver.h

@@ -148,7 +148,7 @@ class MainSolver {
 
     // Notify this particular solver to stop the computation
     // For stopping at the global scope, refer to GlobalStop.h
-    void notifyStop() { smt_solver->notifyStop(); }
+    void notifyStop();
 
     // Set wall-clock time limit for the solver in miliseconds
     // When it expires, the solving is terminated gracefully and unknown is returned

src/proof/InterpolationContext.cc

@@ -557,7 +557,8 @@ PTRef SingleInterpolationComputationContext::produceSingleInterpolant() {
                 continue;
             }
 
-            assert(partial_interp != PTRef_Undef);
+            if (partial_interp == PTRef_Undef) { return PTRef_Undef; }
+
             setPartialInterpolant(*n, partial_interp);
             if (enabledPedInterpVerif()) { verifyPartialInterpolant(*n); }
         } else { // Inner node
@@ -666,6 +667,9 @@ PTRef SingleInterpolationComputationContext::computePartialInterpolantForOrigina
 }
 
 PTRef SingleInterpolationComputationContext::computePartialInterpolantForTheoryClause(ProofNode const & n) {
+    auto & tshandler = thandler->getSolverHandler();
+    if (tshandler.stopped()) { return PTRef_Undef; }
+
     backtrackTSolver();
     vec<Lit> newvec;
     std::vector<Lit> const & oldvec = n.getClause();
@@ -675,6 +679,10 @@ PTRef SingleInterpolationComputationContext::computePartialInterpolantForTheoryC
     bool satisfiable = this->assertLiteralsToTSolver(newvec);
     if (satisfiable) {
         TRes tres = thandler->check(true);
+        if (tres == TRes::UNKNOWN) {
+            assert(tshandler.stopped());
+            return PTRef_Undef;
+        }
         satisfiable = (tres != TRes::UNSAT);
     }
     if (satisfiable) {
@@ -850,11 +858,16 @@ void InterpolationContext::printProofDotty() {
     proof_graph->printProofGraph();
 }
 
-void InterpolationContext::getSingleInterpolant(vec<PTRef> & interpolants, ipartitions_t const & A_mask) {
+bool InterpolationContext::getSingleInterpolant(vec<PTRef> & interpolants, ipartitions_t const & A_mask) {
     assert(proof_graph);
     PTRef itp = SingleInterpolationComputationContext(config, theory, termMapper, pmanager, *proof_graph, A_mask)
                     .produceSingleInterpolant();
 
+    if (itp == PTRef_Undef) {
+        assert(theory.getTSolverHandler().stopped());
+        return false;
+    }
+
     if (enabledInterpVerif()) {
         bool sound = verifyInterpolant(itp, A_mask);
         assert(sound);
@@ -868,13 +881,15 @@ void InterpolationContext::getSingleInterpolant(vec<PTRef> & interpolants, ipart
 
     if (config.simplify_inter() > 0) { itp = simplifyInterpolant(itp); }
     interpolants.push(itp);
+    return true;
 }
 
-void InterpolationContext::getSingleInterpolant(std::vector<PTRef> & interpolants, ipartitions_t const & A_mask) {
+bool InterpolationContext::getSingleInterpolant(std::vector<PTRef> & interpolants, ipartitions_t const & A_mask) {
     vec<PTRef> itps;
-    getSingleInterpolant(itps, A_mask);
+    if (not getSingleInterpolant(itps, A_mask)) { return false; }
     for (int i = 0; i < itps.size(); i++)
         interpolants.push_back(itps[i]);
+    return true;
 }
 
 bool InterpolationContext::getPathInterpolants(vec<PTRef> & interpolants, std::vector<ipartitions_t> const & A_masks) {
@@ -886,7 +901,7 @@ bool InterpolationContext::getPathInterpolants(vec<PTRef> & interpolants, std::v
                .first == A_masks.end());
 
     for (unsigned i = 0; i < A_masks.size(); ++i) {
-        getSingleInterpolant(interpolants, A_masks[i]);
+        if (not getSingleInterpolant(interpolants, A_masks[i])) { return false; }
         if (i > 0 and enabledInterpVerif()) {
             PTRef previous_itp = interpolants[interpolants.size() - 2];
             PTRef next_itp = interpolants[interpolants.size() - 1];

src/proof/InterpolationContext.h

@@ -29,10 +29,11 @@ class InterpolationContext {
     // Create interpolants with each A consisting of the specified partitions
     void getInterpolants(std::vector<vec<int>> const & partitions, vec<PTRef> & interpolants);
 
-    void getSingleInterpolant(vec<PTRef> & interpolants, ipartitions_t const & A_mask);
-
-    void getSingleInterpolant(std::vector<PTRef> & interpolants, ipartitions_t const & A_mask);
+    // Returns true on success
+    bool getSingleInterpolant(vec<PTRef> & interpolants, ipartitions_t const & A_mask);
+    bool getSingleInterpolant(std::vector<PTRef> & interpolants, ipartitions_t const & A_mask);
 
+    // Returns true on success
     bool getPathInterpolants(vec<PTRef> & interpolants, std::vector<ipartitions_t> const & A_masks);
 
 private:

src/smtsolvers/CoreSMTSolver.cc

@@ -1517,6 +1517,7 @@ lbool CoreSMTSolver::search(int nof_conflicts)
                 default:
                     assert( false );
             }
+            if (not okContinue()) { break; }
 
             Lit next = lit_Undef;
             while (decisionLevel() < assumptions.size()) {
@@ -1570,6 +1571,7 @@ lbool CoreSMTSolver::search(int nof_conflicts)
                         return zeroLevelConflictHandler();
                     }
                     assert( res == TPropRes::Decide );
+                    if (not okContinue()) { break; }
 
                     // Otherwise we still have to make sure that
                     // splitting on demand did not add any new variable

src/tsolvers/ArrayTHandler.h

@@ -23,7 +23,7 @@ class ArrayTHandler : public TSolverHandler {
 
     Logic const & getLogic() const override { return logic; }
 
-    PTRef getInterpolant(const ipartitions_t & , ItpColorMap *, PartitionManager &) override { throw InternalException("Interpolation not supported yet"); };
+    PTRef getInterpolantImpl(const ipartitions_t & , ItpColorMap *, PartitionManager &) override { throw InternalException("Interpolation not supported yet"); };
 
 };
 

src/tsolvers/IDLTHandler.h

@@ -23,7 +23,7 @@ class IDLTHandler : public TSolverHandler
     virtual Logic& getLogic() override;
     virtual const Logic& getLogic() const override;
 //    virtual lbool getPolaritySuggestion(PTRef) const override;
-    virtual PTRef getInterpolant(const ipartitions_t&, ItpColorMap *, PartitionManager&) override {
+    virtual PTRef getInterpolantImpl(const ipartitions_t&, ItpColorMap *, PartitionManager&) override {
         throw std::logic_error("Not implemented yet");
     }
 

src/tsolvers/LATHandler.cc

@@ -18,7 +18,7 @@ LATHandler::LATHandler(SMTConfig & c, ArithLogic & l)
     setSolverSchedule({lasolver});
 }
 
-PTRef LATHandler::getInterpolant(ipartitions_t const & mask, ItpColorMap * labels, PartitionManager & pmanager) {
+PTRef LATHandler::getInterpolantImpl(ipartitions_t const & mask, ItpColorMap * labels, PartitionManager & pmanager) {
     if (logic.hasReals() and not logic.hasIntegers()) {
         return lasolver->getRealInterpolant(mask, labels, pmanager);
     } else if (logic.hasIntegers() and not logic.hasReals()) {

src/tsolvers/LATHandler.h

@@ -27,7 +27,7 @@ class LATHandler : public TSolverHandler
     virtual Logic const & getLogic() const override { return logic; }
     virtual lbool getPolaritySuggestion(PTRef p) const override { return lasolver->getPolaritySuggestion(p); }
 
-    virtual PTRef getInterpolant(ipartitions_t const & mask, ItpColorMap * labels, PartitionManager & pmanager) override;
+    virtual PTRef getInterpolantImpl(ipartitions_t const & mask, ItpColorMap * labels, PartitionManager & pmanager) override;
 };
 
 }

src/tsolvers/RDLTHandler.h

@@ -18,7 +18,7 @@ class RDLTHandler : public TSolverHandler
     virtual ~RDLTHandler() = default;
     Logic &getLogic() override;
     const Logic &getLogic() const override;
-    PTRef getInterpolant(const ipartitions_t &, ItpColorMap *, PartitionManager&) override {
+    PTRef getInterpolantImpl(const ipartitions_t &, ItpColorMap *, PartitionManager&) override {
         throw std::logic_error("Not implemented yet");
     }
 

src/tsolvers/THandler.cc

@@ -20,6 +20,11 @@ namespace opensmt {
 
 void THandler::backtrack(int lev)
 {
+    auto & tshandler = getSolverHandler();
+    //++ currently popBacktrackPoints may fail if stopped due to ending in an inconsistent state
+    // now we just return -> the solver state must be discarded and cannot be recovered
+    if (tshandler.stopped()) { return; }
+
     unsigned int backTrackPointsCounter = 0;
     // Undoes the state of theory atoms if needed
     while ( (int)stack.size( ) > (lev > 0 ? lev : 0) ) {
@@ -33,7 +38,7 @@ void THandler::backtrack(int lev)
         if (not isDeclared(var(PTRefToLit(e)))) continue;
         ++backTrackPointsCounter;
     }
-    for (auto solver : getSolverHandler().solverSchedule) {
+    for (auto solver : tshandler.solverSchedule) {
         solver->popBacktrackPoints(backTrackPointsCounter);
     }
 

src/tsolvers/TSolver.h

@@ -125,6 +125,8 @@ class TSolver
      */
     Map<PTRef,lbool,PTRefHash>  polarityMap;
 
+    bool stopFlag{false};
+
 protected:
     SolverId                    id;              // Solver unique identifier
     vec<PtAsgn>                 explanation;     // Stores the explanation
@@ -151,6 +153,8 @@ class TSolver
     vec<PTRef>                  splitondemand;
 
 public:
+    struct StopException {};
+
     // The states of the TSolver check query
 
 
@@ -190,6 +194,10 @@ class TSolver
     virtual bool isValid(PTRef tr) = 0;
     bool isInformed(PTRef tr) const { return informed_PTRefs.has(tr); }
 
+    virtual void notifyStop() { stopFlag = true; }
+
+    bool stopped() const { return stopFlag; }
+
     virtual void printStatistics(std::ostream & os);
 protected:
     void                        setInformed(PTRef tr) { informed_PTRefs.insert(tr, true); }

src/tsolvers/TSolverHandler.cc

@@ -12,14 +12,21 @@ TSolverHandler::~TSolverHandler()
     }
 }
 
+PTRef TSolverHandler::getInterpolant(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager& pmanager) {
+    if (stopped()) { return PTRef_Undef; }
+    return getInterpolantImpl(mask, labels, pmanager);
+}
+
 void TSolverHandler::computeModel()
 {
+    if (stopped()) { return; }
     for (auto solver : solverSchedule) {
         solver->computeModel();
     }
 }
 
 void TSolverHandler::fillTheoryFunctions(ModelBuilder & modelBuilder) const {
+    if (stopped()) { return; }
     for (auto solver : solverSchedule) {
         assert(solver);
         solver->fillTheoryFunctions(modelBuilder);
@@ -70,7 +77,9 @@ void TSolverHandler::informNewSplit(PTRef tr)
 }
 
 TRes TSolverHandler::check(bool complete)
-{
+try {
+    if (stopped()) { return TRes::UNKNOWN; }
+
     TRes res_final = TRes::SAT;
     for (auto solver : solverSchedule) {
         TRes res = solver->check(complete);
@@ -81,6 +90,10 @@ TRes TSolverHandler::check(bool complete)
     }
     return res_final;
 }
+catch (TSolver::StopException const &) {
+    assert(stopped());
+    return TRes::UNKNOWN;
+}
 
 vec<PTRef> TSolverHandler::getSplitClauses() {
     vec<PTRef> split_terms;
@@ -104,4 +117,11 @@ TSolver* TSolverHandler::getReasoningSolverFor(PTRef ptref) const {
     return nullptr;
 }
 
+void TSolverHandler::notifyStop() {
+    stopFlag = true;
+    for (auto solver : solverSchedule) {
+        solver->notifyStop();
+    }
+}
+
 }

src/tsolvers/TSolverHandler.h

@@ -60,7 +60,7 @@ class TSolverHandler {
 
     virtual       Logic& getLogic() = 0;
     virtual const Logic& getLogic() const = 0;
-    virtual PTRef getInterpolant(const ipartitions_t& mask, ItpColorMap *, PartitionManager& pmanager) = 0;
+    PTRef getInterpolant(const ipartitions_t& mask, ItpColorMap *, PartitionManager& pmanager);
 
     void    computeModel      ();                      // Computes a model in the solver if necessary
     bool    assertLit         (PtAsgn);                // Push the assignment to all theory solvers
@@ -70,9 +70,17 @@ class TSolverHandler {
     virtual TRes    check(bool);
     virtual vec<PTRef> getSplitClauses();
     virtual void fillTheoryFunctions(ModelBuilder & modelBuilder) const;
+
+    void notifyStop();
+
+    bool stopped() const { return stopFlag; }
 private:
+    virtual PTRef getInterpolantImpl(const ipartitions_t& mask, ItpColorMap *, PartitionManager& pmanager) = 0;
+
     // Helper method for computing reasons
     TSolver* getReasoningSolverFor(PTRef ptref) const;
+
+    bool stopFlag{false};
 };
 
 }

src/tsolvers/UFLATHandler.cc

@@ -22,7 +22,7 @@ UFLATHandler::UFLATHandler(SMTConfig & c, ArithLogic & l)
 
 }
 
-PTRef UFLATHandler::getInterpolant(const ipartitions_t&, ItpColorMap *, PartitionManager &)
+PTRef UFLATHandler::getInterpolantImpl(const ipartitions_t&, ItpColorMap *, PartitionManager &)
 {
     throw std::logic_error("Not implemented");
 }

src/tsolvers/UFLATHandler.h

@@ -53,7 +53,7 @@ class UFLATHandler : public TSolverHandler
     Logic & getLogic() override { return logic; }
     Logic const & getLogic() const override { return logic; }
 
-    PTRef getInterpolant(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager) override;
+    PTRef getInterpolantImpl(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager) override;
 
     lbool getPolaritySuggestion(PTRef pt) const override;
 

src/tsolvers/UFTHandler.cc

@@ -30,7 +30,7 @@ lbool UFTHandler::getPolaritySuggestion(PTRef p) const {
     return l_Undef;
 }
 
-PTRef UFTHandler::getInterpolant(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager)
+PTRef UFTHandler::getInterpolantImpl(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager)
 {
     InterpolatingEgraph* iegraph = dynamic_cast<InterpolatingEgraph*>(egraph);
     assert(iegraph);

src/tsolvers/UFTHandler.h

@@ -48,7 +48,7 @@ class UFTHandler : public TSolverHandler
     virtual const Logic& getLogic() const override;
     virtual lbool getPolaritySuggestion(PTRef) const override;
 
-    virtual PTRef getInterpolant(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager) override;
+    virtual PTRef getInterpolantImpl(const ipartitions_t& mask, ItpColorMap * labels, PartitionManager &pmanager) override;
 };
 
 }

src/tsolvers/lasolver/LASolver.cc

@@ -133,7 +133,12 @@ bool LASolver::check_simplex(bool complete) {
     if (status == INIT) {
         initSolver();
     }
-    storeExplanation(simplex.checkSimplex());
+
+    try { storeExplanation(simplex.checkSimplex()); }
+    catch (Simplex::StopException const &) {
+        assert(stopped());
+        throw StopException{};
+    }
 
     if (explanation.size() == 0)
         setStatus(SAT);
@@ -627,6 +632,11 @@ LASolver::~LASolver( )
 ArithLogic&  LASolver::getLogic()  { return logic; }
 
 
+void LASolver::notifyStop() {
+    TSolver::notifyStop();
+    simplex.notifyStop();
+}
+
 /**
  * Given an inequality v ~ c (with ~ is either < or <=), compute the correct bounds on the variable.
  * The correct values of the bounds are computed differently, based on whether the value of v must be Int or not.

src/tsolvers/lasolver/LASolver.h

@@ -78,6 +78,8 @@ class LASolver : public TSolver {
     ArithLogic & getLogic() override;
     bool isValid(PTRef tr) override;
 
+    void notifyStop() override;
+
 private:
     struct DecEl {
         PtAsgn asgn;