diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index c08f1d058..959642cb1 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/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, diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index c5922aa75..9e2db3117 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -122,7 +122,6 @@ 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()); @@ -130,7 +129,7 @@ int k_inductiont::induction_base() // 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, diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp index 52b80670a..70e7f3549 100644 --- a/src/ebmc/random_traces.cpp +++ b/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, diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp index 81c78aaec..f135071a5 100644 --- a/src/ebmc/ranking_function.cpp +++ b/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 { diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp index 41fd3a374..ffeb638b3 100644 --- a/src/ebmc/show_trans.cpp +++ b/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; } diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index f74be0b08..7d77776b8 100644 --- a/src/ebmc/transition_system.cpp +++ b/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 diff --git a/src/ebmc/transition_system.h b/src/ebmc/transition_system.h index 1f1cc73c6..19ef1b71f 100644 --- a/src/ebmc/transition_system.h +++ b/src/ebmc/transition_system.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_EBMC_TRANSITION_SYSTEM_H #include +#include #include 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 trans_expr; // transition system expression + transt trans_expr; // transition system expression }; transition_systemt get_transition_system(const cmdlinet &, message_handlert &);