ebmc: transition_systemt does not need optional transt

The trans_expr in transition_systemt is always populated, and does not need
to be optional.

src/ebmc/ebmc_base.cpp

@@ -360,9 +360,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;
@@ -178,7 +176,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/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,19 +241,17 @@ int show_transt::show_trans()
   transition_system =
     get_transition_system(cmdline, message.get_message_handler());
 
-  PRECONDITION(transition_system.trans_expr.has_value());
-
   std::cout << "Initial state constraints:\n\n";
 
-  print_verilog_constraints(transition_system.trans_expr->init(), std::cout);
+  print_verilog_constraints(transition_system.trans_expr.init(), std::cout);
 
   std::cout << "State constraints:\n\n";
 
-  print_verilog_constraints(transition_system.trans_expr->invar(), std::cout);
+  print_verilog_constraints(transition_system.trans_expr.invar(), std::cout);
 
   std::cout << "Transition constraints:\n\n";
 
-  print_verilog_constraints(transition_system.trans_expr->trans(), std::cout);
+  print_verilog_constraints(transition_system.trans_expr.trans(), std::cout);
 
   return 0;
 }

src/ebmc/transition_system.cpp

@@ -252,8 +252,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
@@ -262,7 +261,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,19 @@ class message_handlert;
 class transition_systemt
 {
 public:
+  transition_systemt()
+    : trans_expr{
+        ID_trans,
+        conjunction({}),
+        conjunction({}),
+        conjunction({}),
+        typet()}
+  {
+  }
+
   symbol_tablet symbol_table;
   const symbolt *main_symbol;
-  optionalt<transt> trans_expr; // transition system expression
+  transt trans_expr; // transition system expression
 };
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);