diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index b69d953b5b9..0ab8671caab 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -114,18 +114,12 @@ decision_proceduret::resultt goto_symex_property_decidert::solve() return solver->decision_procedure()(); } -decision_proceduret & +stack_decision_proceduret & goto_symex_property_decidert::get_decision_procedure() const { return solver->decision_procedure(); } -stack_decision_proceduret & -goto_symex_property_decidert::get_stack_decision_procedure() const -{ - return solver->stack_decision_procedure(); -} - symex_target_equationt &goto_symex_property_decidert::get_equation() const { return equation; diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 715e9f9d154..62bfa3c1757 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -45,10 +45,7 @@ class goto_symex_property_decidert decision_proceduret::resultt solve(); /// Returns the solver instance - decision_proceduret &get_decision_procedure() const; - - /// Returns the solver instance - stack_decision_proceduret &get_stack_decision_procedure() const; + stack_decision_proceduret &get_decision_procedure() const; /// Return the equation associated with this instance symex_target_equationt &get_equation() const; diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 372c1de28af..b29c4ab50c8 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -113,7 +113,7 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(property_decider.get_stack_decision_procedure()), + dynamic_cast(property_decider.get_decision_procedure()), equation); } @@ -161,7 +161,7 @@ multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const options, ui_message_handler, equation, - property_decider.get_stack_decision_procedure()); + property_decider.get_decision_procedure()); return fault_localizer(property_id); } diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index ed3eedbe96c..551988655f2 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -44,7 +44,7 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( // Freeze all symbols if we are using a prop_conv_solvert prop_conv_solvert *prop_conv_solver = dynamic_cast( - &property_decider.get_stack_decision_procedure()); + &property_decider.get_decision_procedure()); if(prop_conv_solver != nullptr) prop_conv_solver->set_all_frozen(); } @@ -114,7 +114,7 @@ operator()(propertiest &properties) properties); // We convert the assertions in a new context. - property_decider.get_stack_decision_procedure().push(); + property_decider.get_decision_procedure().push(); equation.convert_assertions( property_decider.get_decision_procedure(), false); property_decider.convert_goals(); @@ -154,7 +154,7 @@ operator()(propertiest &properties) // Nothing else to do with the current set of assertions. // Let's pop them. - property_decider.get_stack_decision_procedure().pop(); + property_decider.get_decision_procedure().pop(); } // Now we are finally done. @@ -207,7 +207,7 @@ goto_tracet single_loop_incremental_symex_checkert::build_shortest_trace() const { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(property_decider.get_stack_decision_procedure()), + dynamic_cast(property_decider.get_decision_procedure()), equation); } diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 9d3d21c691b..4c9c8be312c 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -144,7 +144,7 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(property_decider->get_stack_decision_procedure()), + dynamic_cast(property_decider->get_decision_procedure()), property_decider->get_equation()); } diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 754542b8b79..8cb087f5fa0 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -46,41 +46,31 @@ solver_factoryt::solver_factoryt( { } -solver_factoryt::solvert::solvert(std::unique_ptr p) +solver_factoryt::solvert::solvert(std::unique_ptr p) : decision_procedure_ptr(std::move(p)) { } solver_factoryt::solvert::solvert( - std::unique_ptr p1, + std::unique_ptr p1, std::unique_ptr p2) : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1)) { } solver_factoryt::solvert::solvert( - std::unique_ptr p1, + std::unique_ptr p1, std::unique_ptr p2) : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1)) { } -decision_proceduret &solver_factoryt::solvert::decision_procedure() const +stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const { PRECONDITION(decision_procedure_ptr != nullptr); return *decision_procedure_ptr; } -stack_decision_proceduret & -solver_factoryt::solvert::stack_decision_procedure() const -{ - PRECONDITION(decision_procedure_ptr != nullptr); - stack_decision_proceduret *solver = - dynamic_cast(&*decision_procedure_ptr); - INVARIANT(solver != nullptr, "stack decision procedure required"); - return *solver; -} - void solver_factoryt::set_decision_procedure_time_limit( solver_resource_limitst &decision_procedure) { @@ -92,7 +82,7 @@ void solver_factoryt::set_decision_procedure_time_limit( } void solver_factoryt::solvert::set_decision_procedure( - std::unique_ptr p) + std::unique_ptr p) { decision_procedure_ptr = std::move(p); } diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index 8ebeb2a4638..f62d97ff5b8 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -22,7 +22,6 @@ class message_handlert; class namespacet; class optionst; class solver_resource_limitst; -class stack_decision_proceduret; class solver_factoryt final { @@ -39,23 +38,24 @@ class solver_factoryt final class solvert final { public: - explicit solvert(std::unique_ptr p); - solvert(std::unique_ptr p1, std::unique_ptr p2); + explicit solvert(std::unique_ptr p); solvert( - std::unique_ptr p1, + std::unique_ptr p1, + std::unique_ptr p2); + solvert( + std::unique_ptr p1, std::unique_ptr p2); - decision_proceduret &decision_procedure() const; - stack_decision_proceduret &stack_decision_procedure() const; + stack_decision_proceduret &decision_procedure() const; - void set_decision_procedure(std::unique_ptr p); + void set_decision_procedure(std::unique_ptr p); void set_prop(std::unique_ptr p); void set_ofstream(std::unique_ptr p); // the objects are deleted in the opposite order they appear below std::unique_ptr ofstream_ptr; std::unique_ptr prop_ptr; - std::unique_ptr decision_procedure_ptr; + std::unique_ptr decision_procedure_ptr; }; /// Returns a solvert object