Catch Minisat::OutOfMemoryException

src/solvers/sat/satcheck_minisat2.cpp

@@ -69,8 +69,18 @@ template<typename T>
 void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
 {
   assert(!a.is_constant());
-  add_variables();
-  solver->setPolarity(a.var_no(), value);
+
+  try
+  {
+    add_variables();
+    solver->setPolarity(a.var_no(), value);
+  }
+  catch(Minisat::OutOfMemoryException)
+  {
+    messaget::error() << "SAT checker ran out of memory" << eom;
+    status = statust::ERROR;
+    throw std::bad_alloc();
+  }
 }
 
 const std::string satcheck_minisat_no_simplifiert::solver_text()
@@ -93,26 +103,35 @@ void satcheck_minisat2_baset<T>::add_variables()
 template<typename T>
 void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 {
-  add_variables();
-
-  forall_literals(it, bv)
+  try
   {
-    if(it->is_true())
-      return;
-    else if(!it->is_false())
-      assert(it->var_no()<(unsigned)solver->nVars());
-  }
+    add_variables();
+
+    forall_literals(it, bv)
+    {
+      if(it->is_true())
+        return;
+      else if(!it->is_false())
+        assert(it->var_no() < (unsigned)solver->nVars());
+    }
 
-  Minisat::vec<Minisat::Lit> c;
+    Minisat::vec<Minisat::Lit> c;
 
-  convert(bv, c);
+    convert(bv, c);
 
-  // Note the underscore.
-  // Add a clause to the solver without making superflous internal copy.
+    // Note the underscore.
+    // Add a clause to the solver without making superflous internal copy.
 
-  solver->addClause_(c);
+    solver->addClause_(c);
 
-  clause_counter++;
+    clause_counter++;
+  }
+  catch(Minisat::OutOfMemoryException)
+  {
+    messaget::error() << "SAT checker ran out of memory" << eom;
+    status = statust::ERROR;
+    throw std::bad_alloc();
+  }
 }
 
 #ifndef _WIN32
@@ -243,13 +262,22 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
 {
   assert(!a.is_constant());
 
-  unsigned v=a.var_no();
-  bool sign=a.sign();
+  try
+  {
+    unsigned v = a.var_no();
+    bool sign = a.sign();
 
-  // MiniSat2 kills the model in case of UNSAT
-  solver->model.growTo(v+1);
-  value^=sign;
-  solver->model[v]=Minisat::lbool(value);
+    // MiniSat2 kills the model in case of UNSAT
+    solver->model.growTo(v + 1);
+    value ^= sign;
+    solver->model[v] = Minisat::lbool(value);
+  }
+  catch(Minisat::OutOfMemoryException)
+  {
+    messaget::error() << "SAT checker ran out of memory" << eom;
+    status = statust::ERROR;
+    throw std::bad_alloc();
+  }
 }
 
 template<typename T>
@@ -307,10 +335,19 @@ satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
 
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {
-  if(!a.is_constant())
+  try
   {
-    add_variables();
-    solver->setFrozen(a.var_no(), true);
+    if(!a.is_constant())
+    {
+      add_variables();
+      solver->setFrozen(a.var_no(), true);
+    }
+  }
+  catch(Minisat::OutOfMemoryException)
+  {
+    messaget::error() << "SAT checker ran out of memory" << eom;
+    status = statust::ERROR;
+    throw std::bad_alloc();
   }
 }