Simplify incremental solver using CBMC's push and pop

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/domains/incremental_solver.cpp

@@ -29,22 +29,9 @@ void incremental_solvert::new_context()
 #endif
 
 #else
-
-  literalt activation_literal=
-    solver->convert(
-      symbol_exprt(
-        "goto_symex::\\act$"+
-        std::to_string(activation_literal_counter++), bool_typet()));
-
+  solver->push();
 #ifdef DEBUG_OUTPUT
-    debug() << "new context: " << activation_literal<< eom;
-#endif
-
-  activation_literals.push_back(activation_literal);
-  solver->set_assumptions(activation_literals);
-
-#if 0
-  return !activation_literals.back(); // not to be used anymore
+    debug() << "new context" <<  eom;
 #endif
 #endif
 }
@@ -62,45 +49,10 @@ void incremental_solvert::pop_context()
 
 #else
 
-  assert(!activation_literals.empty());
-  literalt activation_literal=activation_literals.back();
-  activation_literals.pop_back();
-#ifndef DEBUG_FORMULA
-  solver->set_to_false(literal_exprt(activation_literal));
-#else
-  formula.push_back(!activation_literal);
-#endif
-
+  solver->pop();
 #ifdef DEBUG_OUTPUT
-    debug() << "pop context: " << activation_literal << eom;
+    debug() << "pop context" << eom;
 #endif
-
-  solver->set_assumptions(activation_literals);
-#endif
-}
-
-void incremental_solvert::make_context_permanent()
-{
-#ifdef NON_INCREMENTAL
-  assert(contexts.size()>=2);
-  contextst::iterator c_it=contexts.end(); c_it--; c_it--;
-  c_it->insert(c_it->end(), contexts.back().begin(), contexts.back().end());
-  contexts.pop_back();
-#else
-  assert(!activation_literals.empty());
-  literalt activation_literal=activation_literals.back();
-  activation_literals.pop_back();
-#ifndef DEBUG_FORMULA
-  solver->set_to_true(literal_exprt(activation_literal));
-#else
-  formula.push_back(activation_literal);
-#endif
-
-#ifdef DEBUG_OUTPUT
-    debug() << "make context permanent: " << activation_literal<< eom;
-#endif
-
-  solver->set_assumptions(activation_literals);
 #endif
 }
 

src/domains/incremental_solver.h

@@ -126,15 +126,11 @@ class incremental_solvert:public messaget
 
   void new_context();
   void pop_context();
-  void make_context_permanent();
 
   // for debugging
   bvt formula;
   void debug_add_to_formula(const exprt &expr);
 
-  // context assumption literals
-  bvt activation_literals;
-
   // non-incremental solving
   contextst contexts;
 
@@ -192,11 +188,7 @@ static inline incremental_solvert &operator<<(
   dest.contexts.back().push_back(src);
 #else
 #ifndef DEBUG_FORMULA
-  if(!dest.activation_literals.empty())
-    *dest.solver <<
-      or_exprt(src, literal_exprt(!dest.activation_literals.back()));
-  else
-    *dest.solver << src;
+  *dest.solver << src;
 #else
   if(!dest.activation_literals.empty())
   {