Merge pull request #263 from diffblue/trans_expr_not_optional

ebmc: transition_systemt does not need optional transt

Author: kroening

src/ebmc/ebmc_base.cpp

@@ -341,9 +341,8 @@ int ebmc_baset::do_word_level_bmc(
 
       // convert the transition system
       const namespacet ns(transition_system.symbol_table);
-      CHECK_RETURN(transition_system.trans_expr.has_value());
       ::unwind(
-        *transition_system.trans_expr,
+        transition_system.trans_expr,
         message.get_message_handler(),
         solver,
         bound + 1,

src/ebmc/k_induction.cpp

@@ -122,15 +122,14 @@ Function: k_inductiont::induction_base
 
 int k_inductiont::induction_base()
 {
-  PRECONDITION(transition_system.trans_expr.has_value());
   message.status() << "Induction Base" << messaget::eom;
 
   auto solver_wrapper = solver_factory(ns, message.get_message_handler());
   auto &solver = solver_wrapper.stack_decision_procedure();
 
   // convert the transition system
   ::unwind(
-    *transition_system.trans_expr,
+    transition_system.trans_expr,
     message.get_message_handler(),
     solver,
     bound + 1,
@@ -162,7 +161,6 @@ Function: k_inductiont::induction_step
 
 int k_inductiont::induction_step()
 {
-  PRECONDITION(transition_system.trans_expr.has_value());
   message.status() << "Induction Step" << messaget::eom;
 
   unsigned no_timeframes=bound+1;
@@ -184,7 +182,7 @@ int k_inductiont::induction_step()
 
     // *no* initial state
     unwind(
-      *transition_system.trans_expr,
+      transition_system.trans_expr,
       message.get_message_handler(),
       solver,
       no_timeframes,

src/ebmc/liveness_to_safety.cpp

@@ -229,16 +229,16 @@ void liveness_to_safetyt::operator()()
   auto looped_invar = equal_exprt{
     this->looped_symbol(), and_exprt(saved_symbol(), state_is_loop())};
 
-  transition_system.trans_expr->init() =
-    conjunction({transition_system.trans_expr->init(), std::move(saved_init)});
+  transition_system.trans_expr.init() =
+    conjunction({transition_system.trans_expr.init(), std::move(saved_init)});
 
-  transition_system.trans_expr->invar() = conjunction(
-    {transition_system.trans_expr->invar(),
+  transition_system.trans_expr.invar() = conjunction(
+    {transition_system.trans_expr.invar(),
      std::move(save_invar),
      std::move(looped_invar)});
 
-  transition_system.trans_expr->trans() = conjunction(
-    {transition_system.trans_expr->trans(),
+  transition_system.trans_expr.trans() = conjunction(
+    {transition_system.trans_expr.trans(),
      std::move(saved_trans),
      std::move(loop_trans)});
 
@@ -284,8 +284,8 @@ void liveness_to_safetyt::translate_GFp(propertyt &property)
   // Initial-state constraint for 'live' variable.
   auto live_init = equal_exprt{live_symbol(property.name), false_exprt()};
 
-  transition_system.trans_expr->init() =
-    conjunction({transition_system.trans_expr->init(), std::move(live_init)});
+  transition_system.trans_expr.init() =
+    conjunction({transition_system.trans_expr.init(), std::move(live_init)});
 
   // Next-state constraint for 'live' variable.
   // The paper uses live' := live ∨ found, which is for F found,
@@ -295,8 +295,8 @@ void liveness_to_safetyt::translate_GFp(propertyt &property)
     or_exprt{
       and_exprt{live_symbol(property.name), not_exprt{save_symbol()}}, p}};
 
-  transition_system.trans_expr->trans() =
-    conjunction({transition_system.trans_expr->trans(), std::move(live_trans)});
+  transition_system.trans_expr.trans() =
+    conjunction({transition_system.trans_expr.trans(), std::move(live_trans)});
 
   // replace the liveness property
   property.expr = safety_replacement(property.name, property.expr);

src/ebmc/random_traces.cpp

@@ -449,15 +449,13 @@ void random_tracest::operator()(
 
   auto number_of_timeframes = number_of_trace_steps + 1;
 
-  PRECONDITION(transition_system.trans_expr.has_value());
-
   message.status() << "Passing transition system to solver" << messaget::eom;
 
   satcheckt satcheck{message.get_message_handler()};
   boolbvt solver(ns, satcheck, message.get_message_handler());
 
   ::unwind(
-    *transition_system.trans_expr,
+    transition_system.trans_expr,
     message.get_message_handler(),
     solver,
     number_of_timeframes,

src/ebmc/ranking_function.cpp

@@ -92,8 +92,6 @@ int do_ranking_function(
   transition_systemt transition_system =
     get_transition_system(cmdline, message_handler);
 
-  CHECK_RETURN(transition_system.trans_expr.has_value());
-
   // parse the ranking function
   if(!cmdline.isset("ranking-function"))
     throw ebmc_errort() << "no candidate ranking function given";
@@ -143,7 +141,7 @@ tvt is_ranking_function(
   auto &solver = solver_wrapper.stack_decision_procedure();
 
   // *no* initial state, two time frames
-  unwind(*transition_system.trans_expr, message_handler, solver, 2, ns, false);
+  unwind(transition_system.trans_expr, message_handler, solver, 2, ns, false);
 
   const auto p = [&property]() -> exprt
   {

src/ebmc/show_trans.cpp

@@ -241,8 +241,6 @@ int show_transt::show_trans()
   transition_system =
     get_transition_system(cmdline, message.get_message_handler());
 
-  PRECONDITION(transition_system.trans_expr.has_value());
-
   transition_system.output(std::cout);
 
   return 0;

src/ebmc/transition_system.cpp

@@ -60,15 +60,15 @@ void transition_systemt::output(std::ostream &out) const
 
   out << "Initial state constraints:\n\n";
 
-  ::output(trans_expr->init(), out, *language, ns);
+  ::output(trans_expr.init(), out, *language, ns);
 
   out << "State constraints:\n\n";
 
-  ::output(trans_expr->invar(), out, *language, ns);
+  ::output(trans_expr.invar(), out, *language, ns);
 
   out << "Transition constraints:\n\n";
 
-  ::output(trans_expr->trans(), out, *language, ns);
+  ::output(trans_expr.trans(), out, *language, ns);
 }
 
 int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
@@ -295,8 +295,7 @@ int get_transition_system(
       ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
 
     // true in initial state
-    CHECK_RETURN(transition_system.trans_expr.has_value());
-    transt new_trans_expr = *transition_system.trans_expr;
+    transt new_trans_expr = transition_system.trans_expr;
     new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
 
     // and not anymore afterwards
@@ -305,7 +304,7 @@ int get_transition_system(
 
     new_trans_expr.trans() =
       and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
-    *transition_system.trans_expr = new_trans_expr;
+    transition_system.trans_expr = new_trans_expr;
   }
 
   return -1; // done with the transition system

src/ebmc/transition_system.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_EBMC_TRANSITION_SYSTEM_H
 
 #include <util/mathematical_expr.h>
+#include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 class cmdlinet;
@@ -18,9 +19,14 @@ class message_handlert;
 class transition_systemt
 {
 public:
+  transition_systemt()
+    : trans_expr{ID_trans, true_exprt(), true_exprt(), true_exprt(), typet()}
+  {
+  }
+
   symbol_tablet symbol_table;
   const symbolt *main_symbol;
-  optionalt<transt> trans_expr; // transition system expression
+  transt trans_expr; // transition system expression
 
   void output(std::ostream &) const;
 };