since I just got bitten by SATSolver::VarAssignment turning silently …

…into bool, let's prevent this for the future by making the SATSolver enums classes

FMB/FiniteModelBuilder.cpp

@@ -1626,7 +1626,7 @@ MainLoopResult FiniteModelBuilder::runImpl()
 #endif
     //TODO consider adding clauses directly to SAT solver in new interface?
     // pass clauses and assumption to SAT Solver
-    SATSolver::Status satResult = SATSolver::UNKNOWN;
+    SATSolver::Status satResult = SATSolver::Status::UNKNOWN;
     {
       if (_opt.randomTraversals()) {
         TIME_TRACE(TimeTrace::SHUFFLING);
@@ -1662,7 +1662,7 @@ MainLoopResult FiniteModelBuilder::runImpl()
     }
 
     // if the clauses are satisfiable then we have found a finite model
-    if(satResult == SATSolver::SATISFIABLE){
+    if(satResult == SATSolver::Status::SATISFIABLE){
 
       if (_xmass) { // for CONTOUR
         // before printing possibly retract _distinctSortSizes (and the corresponding _sortModelSizes) according to the set assumptions

Inferences/GlobalSubsumption.cpp

@@ -161,7 +161,7 @@ Clause* GlobalSubsumption::perform(Clause* cl, Stack<Unit*>& prems)
   // check for subsuming clause by looking for a proper subset of used assumptions
   SATSolver::Status res = solver.solveUnderAssumptions(assumps, _uprOnly, true /* only proper subsets */);
 
-  if (res == SATSolver::UNSATISFIABLE) {
+  if (res == SATSolver::Status::UNSATISFIABLE) {
     // it should always be UNSAT with full assumps,
     // but we may not get that far with limited solving power (_uprOnly)
 

Inferences/TheoryInstAndSimp.cpp

@@ -563,13 +563,13 @@ Option<Substitution> TheoryInstAndSimp::instantiateGeneralised(
     }
 
     DEBUG_CODE(auto res =) _solver->solveUnderAssumptions(theoryLits, 0, false);
-    ASS_EQ(res, SATSolver::UNSATISFIABLE)
+    ASS_EQ(res, SATSolver::Status::UNSATISFIABLE)
 
     Set<TermList> usedDefs;
     for (auto& x : _solver->failedAssumptions()) {
       definitionLiterals
         .tryGet(x)
-        .andThen([&](TermList t) 
+        .andThen([&](TermList t)
             { usedDefs.insert(t); });
     }
 
@@ -650,13 +650,13 @@ VirtualIterator<Solution> TheoryInstAndSimp::getSolutions(Stack<Literal*> const&
   // now we can call the solver
   SATSolver::Status status = _solver->solveUnderAssumptions(skolemized.lits, 0, false);
 
-  if(status == SATSolver::UNSATISFIABLE) {
+  if(status == SATSolver::Status::UNSATISFIABLE) {
     DEBUG("unsat")
     return pvi(getSingletonIterator(Solution::unsat()));
 
-  } else if(status == SATSolver::SATISFIABLE) {
+  } else if(status == SATSolver::Status::SATISFIABLE) {
     DEBUG("found model: ", _solver->getModel())
-    auto subst = _generalisation ? instantiateGeneralised(skolemized, freshVar) 
+    auto subst = _generalisation ? instantiateGeneralised(skolemized, freshVar)
                                  : instantiateWithModel(skolemized);
     if (subst.isSome()) {
       return pvi(getSingletonIterator(Solution(std::move(subst).unwrap())));
@@ -720,7 +720,7 @@ struct InstanceFn
         auto skolem = parent->skolemize(iterTraits(invertedLits.iterFifo() /* without guards !! */));
         auto status = parent->_solver->solveUnderAssumptions(skolem.lits, 0, false);
         // we have an unsat solution without guards
-        redundant = status == SATSolver::UNSATISFIABLE;
+        redundant = status == SATSolver::Status::UNSATISFIABLE;
       }
 
       if (redundant) {

SAT/BufferedSolver.cpp

@@ -22,7 +22,7 @@ namespace SAT
 {
 
 BufferedSolver::BufferedSolver(SATSolver* inner)
- : _inner(inner), _checkedIdx(0), _lastStatus(SATISFIABLE), _varCnt(0), _varCntInnerOld(0)
+ : _inner(inner), _checkedIdx(0), _lastStatus(Status::SATISFIABLE), _varCnt(0), _varCntInnerOld(0)
 {
 }
 /**
@@ -116,11 +116,11 @@ SATSolver::Status BufferedSolver::solve(unsigned conflictCountLimit)
   // it needs _inner to have either a model or to be provably unsat
   ASS_EQ(conflictCountLimit, UINT_MAX);
 
-  if (_lastStatus == UNSATISFIABLE) {
-    return UNSATISFIABLE;
+  if (_lastStatus == Status::UNSATISFIABLE) {
+    return Status::UNSATISFIABLE;
   }
 
-  ASS_EQ(_lastStatus,SATISFIABLE);
+  ASS_EQ(_lastStatus,Status::SATISFIABLE);
 
   // check if clauses are implied by current ground model and buffered literals
   size_t sz = _unadded.size();
@@ -134,7 +134,7 @@ SATSolver::Status BufferedSolver::solve(unsigned conflictCountLimit)
   }
 
   RSTAT_CTR_INC("solver_buffer_hit");
-  return SATSolver::SATISFIABLE;
+  return Status::SATISFIABLE;
 }
 
 /**
@@ -149,14 +149,14 @@ SATSolver::VarAssignment BufferedSolver::getAssignment(unsigned var)
 
   // check buffer
   if(!_literalBuffer.isEmpty() && _literalBuffer.find(var)) {
-    return _literalBuffer.get(var) ? SATSolver::TRUE : SATSolver::FALSE;
+    return _literalBuffer.get(var) ? VarAssignment::TRUE : VarAssignment::FALSE;
   }
 
   // refer to inner if variable not new
   if (var <= _varCntInnerOld) {
     return _inner->getAssignment(var); 
   } else {
-    return SATSolver::DONT_CARE; // If it is new and not yet assigned in buffer
+    return VarAssignment::DONT_CARE; // If it is new and not yet assigned in buffer
   }
 }
 

SAT/MinimizingSolver.cpp

@@ -77,17 +77,17 @@ SATSolver::VarAssignment MinimizingSolver::getAssignment(unsigned var)
   }
 
   if(admitsDontcare(var)) {
-    return SATSolver::DONT_CARE;
+    return VarAssignment::DONT_CARE;
   }
-  return _asgn[var] ? SATSolver::TRUE : SATSolver::FALSE;
+  return _asgn[var] ? VarAssignment::TRUE : VarAssignment::FALSE;
 }
 
 bool MinimizingSolver::isZeroImplied(unsigned var)
 {
   ASS_G(var,0); ASS_LE(var,_varCnt);
 
   bool res = _inner->isZeroImplied(var);
-  ASS(!res || getAssignment(var)!=DONT_CARE); //zero-implied variables will not become a don't care
+  ASS(!res || getAssignment(var)!=VarAssignment::DONT_CARE); //zero-implied variables will not become a don't care
   return res;
 }
 
@@ -184,18 +184,18 @@ void MinimizingSolver::processInnerAssignmentChanges()
     VarAssignment va = _inner->getAssignment(v);
     bool changed;
     switch(va) {
-    case DONT_CARE:
+    case VarAssignment::DONT_CARE:
       changed = false;
       break;
-    case TRUE:
+    case VarAssignment::TRUE:
       changed = !_asgn[v];
       _asgn[v] = true;
       break;
-    case FALSE:
+    case VarAssignment::FALSE:
       changed = _asgn[v];
       _asgn[v] = false;
       break;
-    case NOT_KNOWN:
+    case VarAssignment::NOT_KNOWN:
     default:
       ASSERTION_VIOLATION;
       break;

SAT/MinisatInterfacing.cpp

@@ -27,7 +27,7 @@ using namespace Lib;
 using namespace Minisat;
 
 MinisatInterfacing::MinisatInterfacing(const Shell::Options& opts, bool generateProofs):
-  _status(SATISFIABLE)
+  _status(Status::SATISFIABLE)
 {
   // TODO: consider tuning minisat's options to be set for _solver
   // (or even forwarding them to vampire's options)  
@@ -61,7 +61,7 @@ SATSolver::Status MinisatInterfacing::solveUnderAssumptions(const SATLiteralStac
 
   solveModuloAssumptionsAndSetStatus(conflictCountLimit);
 
-  if (_status == SATSolver::UNSATISFIABLE) {
+  if (_status == Status::UNSATISFIABLE) {
     // unload minisat's internal conflict clause to _failedAssumptionBuffer
     _failedAssumptionBuffer.reset();
     Minisat::LSet& conflict = _solver.conflict;
@@ -79,19 +79,19 @@ SATSolver::Status MinisatInterfacing::solveUnderAssumptions(const SATLiteralStac
  * Solve modulo assumptions and set status.
  * @b conflictCountLimit as with addAssumption.
  */
-void MinisatInterfacing::solveModuloAssumptionsAndSetStatus(unsigned conflictCountLimit) 
+void MinisatInterfacing::solveModuloAssumptionsAndSetStatus(unsigned conflictCountLimit)
 {
   // TODO: consider calling simplify(); or only from time to time?
-    
+
   _solver.setConfBudget(conflictCountLimit); // treating UINT_MAX as \infty
   lbool res = _solver.solveLimited(_assumptions);
-  
+
   if (res == l_True) {
-    _status = SATISFIABLE;
+    _status = Status::SATISFIABLE;
   } else if (res == l_False) {
-    _status = UNSATISFIABLE;    
+    _status = Status::UNSATISFIABLE;
   } else {
-    _status = UNKNOWN;
+    _status = Status::UNKNOWN;
   }
 }
 
@@ -129,29 +129,29 @@ SATSolver::Status MinisatInterfacing::solve(unsigned conflictCountLimit)
   return _status;
 }
 
-void MinisatInterfacing::addAssumption(SATLiteral lit) 
+void MinisatInterfacing::addAssumption(SATLiteral lit)
 {
   _assumptions.push(vampireLit2Minisat(lit));
 }
 
-SATSolver::VarAssignment MinisatInterfacing::getAssignment(unsigned var) 
+SATSolver::VarAssignment MinisatInterfacing::getAssignment(unsigned var)
 {
-	ASS_EQ(_status, SATISFIABLE);  
+	ASS_EQ(_status, Status::SATISFIABLE);
 	ASS_G(var,0); ASS_LE(var,(unsigned)_solver.nVars());
   lbool res;
-    
-  Minisat::Var mvar = vampireVar2Minisat(var);  
-  if (mvar < _solver.model.size()) {  
+
+  Minisat::Var mvar = vampireVar2Minisat(var);
+  if (mvar < _solver.model.size()) {
     if ((res = _solver.modelValue(mvar)) == l_True) {
-      return TRUE;
-    } else if (res == l_False) {    
-      return FALSE;
-    } else {              
+      return VarAssignment::TRUE;
+    } else if (res == l_False) {
+      return VarAssignment::FALSE;
+    } else {
       ASSERTION_VIOLATION;
-      return NOT_KNOWN;
+      return VarAssignment::NOT_KNOWN;
     }
   } else { // new vars have been added but the model didn't grow yet
-    return DONT_CARE;
+    return VarAssignment::DONT_CARE;
   }
 }
 

SAT/MinisatInterfacing.hpp

@@ -89,7 +89,7 @@ class MinisatInterfacing : public PrimitiveProofRecordingSATSolver
 
   virtual void retractAllAssumptions() override {
     _assumptions.clear();
-    _status = UNKNOWN;
+    _status = Status::UNKNOWN;
   };
 
   virtual bool hasAssumptions() const override {

SAT/MinisatInterfacingNewSimp.cpp

@@ -38,7 +38,7 @@ using namespace Minisat;
 const unsigned MinisatInterfacingNewSimp::VAR_MAX = std::numeric_limits<Minisat::Var>::max() / 2;
 
 MinisatInterfacingNewSimp::MinisatInterfacingNewSimp(const Shell::Options& opts, bool generateProofs):
-  _status(SATISFIABLE)
+  _status(Status::SATISFIABLE)
 {
   // TODO: consider tuning minisat's options to be set for _solver
   // (or even forwarding them to vampire's options)  
@@ -88,7 +88,7 @@ SATSolver::Status MinisatInterfacingNewSimp::solveUnderAssumptions(const SATLite
 
   solveModuloAssumptionsAndSetStatus(conflictCountLimit);
 
-  if (_status == SATSolver::UNSATISFIABLE) {
+  if (_status == Status::UNSATISFIABLE) {
     // unload minisat's internal conflict clause to _failedAssumptionBuffer
     _failedAssumptionBuffer.reset();
     Minisat::LSet& conflict = _solver.conflict;
@@ -120,11 +120,11 @@ void MinisatInterfacingNewSimp::solveModuloAssumptionsAndSetStatus(unsigned conf
     //cout << "After: vars " << bef - _solver.eliminated_vars << ", non-unit clauses " << _solver.nClauses() << endl;
 
     if (res == l_True) {
-      _status = SATISFIABLE;
+      _status = Status::SATISFIABLE;
     } else if (res == l_False) {
-      _status = UNSATISFIABLE;
+      _status = Status::UNSATISFIABLE;
     } else {
-      _status = UNKNOWN;
+      _status = Status::UNKNOWN;
     }
   }catch(Minisat::OutOfMemoryException&){
     reportMinisatOutOfMemory();
@@ -172,22 +172,22 @@ void MinisatInterfacingNewSimp::addAssumption(SATLiteral lit)
 
 SATSolver::VarAssignment MinisatInterfacingNewSimp::getAssignment(unsigned var) 
 {
-	ASS_EQ(_status, SATISFIABLE);  
+	ASS_EQ(_status, Status::SATISFIABLE);
 	ASS_G(var,0); ASS_LE(var,(unsigned)_solver.nVars());
   lbool res;
-    
-  Minisat::Var mvar = vampireVar2Minisat(var);  
-  if (mvar < _solver.model.size()) {  
+
+  Minisat::Var mvar = vampireVar2Minisat(var);
+  if (mvar < _solver.model.size()) {
     if ((res = _solver.modelValue(mvar)) == l_True) {
-      return TRUE;
-    } else if (res == l_False) {    
-      return FALSE;
-    } else {              
+      return VarAssignment::TRUE;
+    } else if (res == l_False) {
+      return VarAssignment::FALSE;
+    } else {
       ASSERTION_VIOLATION;
-      return NOT_KNOWN;
+      return VarAssignment::NOT_KNOWN;
     }
   } else { // new vars have been added but the model didn't grow yet
-    return DONT_CARE;
+    return VarAssignment::DONT_CARE;
   }
 }
 

SAT/MinisatInterfacingNewSimp.hpp

@@ -96,7 +96,7 @@ class MinisatInterfacingNewSimp : public SATSolverWithAssumptions
 
   virtual void retractAllAssumptions() override {
     _assumptions.clear();
-    _status = UNKNOWN;
+    _status = Status::UNKNOWN;
   };
 
   virtual bool hasAssumptions() const override {

SAT/SAT2FO.cpp

@@ -85,12 +85,12 @@ void SAT2FO::collectAssignment(SATSolver& solver, LiteralStack& res) const
   unsigned maxVar = maxSATVar();
   for (unsigned i = 1; i <= maxVar; i++) {
     SATSolver::VarAssignment asgn = solver.getAssignment(i);
-    if(asgn==SATSolver::DONT_CARE) {
+    if(asgn==SATSolver::VarAssignment::DONT_CARE) {
       //we don't add DONT_CARE literals into the assignment
       continue;
     }
-    ASS(asgn==SATSolver::TRUE || asgn==SATSolver::FALSE);
-    SATLiteral sl(i, asgn==SATSolver::TRUE);
+    ASS(asgn==SATSolver::VarAssignment::TRUE || asgn==SATSolver::VarAssignment::FALSE);
+    SATLiteral sl(i, asgn==SATSolver::VarAssignment::TRUE);
     ASS(solver.trueInAssignment(sl));
     Literal* lit = toFO(sl);
     if(!lit) {