From 9bb9d1a5b17a6c2d5fb841ee890f67af75d7b569 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 27 Mar 2019 14:33:14 +0000 Subject: [PATCH 1/8] Rename prop_convt to decision_procedure_incrementalt decision_procedure_incrementalt will then be further split into support for assumptions and contexts. --- jbmc/src/jbmc/all_properties.cpp | 7 +- jbmc/src/jbmc/all_properties_class.h | 4 +- jbmc/src/jbmc/bmc.cpp | 21 ++-- jbmc/src/jbmc/bmc.h | 16 +-- src/goto-checker/bmc_util.cpp | 20 ++-- src/goto-checker/bmc_util.h | 11 +- .../counterexample_beautification.cpp | 11 +- .../counterexample_beautification.h | 4 +- .../goto_symex_fault_localizer.cpp | 4 +- src/goto-checker/goto_symex_fault_localizer.h | 6 +- .../goto_symex_property_decider.cpp | 17 +-- .../goto_symex_property_decider.h | 3 +- src/goto-checker/solver_factory.cpp | 67 +++++++----- src/goto-checker/solver_factory.h | 26 +++-- .../accelerate/scratch_program.h | 2 +- src/goto-symex/build_goto_trace.cpp | 101 +++++++++++------- src/goto-symex/build_goto_trace.h | 17 +-- src/goto-symex/symex_target_equation.cpp | 51 +++++---- src/goto-symex/symex_target_equation.h | 40 ++++--- src/solvers/Makefile | 2 +- src/solvers/flattening/functions.cpp | 2 +- src/solvers/flattening/functions.h | 11 +- src/solvers/prop/cover_goals.cpp | 13 +-- src/solvers/prop/cover_goals.h | 14 +-- ...cpp => decision_procedure_incremental.cpp} | 10 +- ...onv.h => decision_procedure_incremental.h} | 29 +++-- src/solvers/prop/prop_conv_solver.h | 10 +- src/solvers/prop/prop_minimize.cpp | 21 ++-- src/solvers/prop/prop_minimize.h | 6 +- src/solvers/smt2/smt2_conv.h | 4 +- 30 files changed, 308 insertions(+), 242 deletions(-) rename src/solvers/prop/{prop_conv.cpp => decision_procedure_incremental.cpp} (58%) rename src/solvers/prop/{prop_conv.h => decision_procedure_incremental.h} (65%) diff --git a/jbmc/src/jbmc/all_properties.cpp b/jbmc/src/jbmc/all_properties.cpp index 6b6ec88b441..2205d333450 100644 --- a/jbmc/src/jbmc/all_properties.cpp +++ b/jbmc/src/jbmc/all_properties.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include @@ -61,7 +61,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()() auto solver_start = std::chrono::steady_clock::now(); convert_symex_target_equation( - bmc.equation, bmc.prop_conv, get_message_handler()); + bmc.equation, bmc.decision_procedure, get_message_handler()); bmc.freeze_program_variables(); // Collect _all_ goals in `goal_map'. @@ -301,7 +301,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) safety_checkert::resultt bmct::all_properties(const goto_functionst &goto_functions) { - bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this); + bmc_all_propertiest bmc_all_properties( + goto_functions, decision_procedure, *this); bmc_all_properties.set_message_handler(get_message_handler()); return bmc_all_properties(); } diff --git a/jbmc/src/jbmc/all_properties_class.h b/jbmc/src/jbmc/all_properties_class.h index a5fc881ada4..e1b34d0e380 100644 --- a/jbmc/src/jbmc/all_properties_class.h +++ b/jbmc/src/jbmc/all_properties_class.h @@ -22,7 +22,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget public: bmc_all_propertiest( const goto_functionst &_goto_functions, - prop_convt &_solver, + decision_procedure_incrementalt &_solver, bmct &_bmc) : goto_functions(_goto_functions), solver(_solver), bmc(_bmc) { @@ -96,7 +96,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget protected: const goto_functionst &goto_functions; - prop_convt &solver; + decision_procedure_incrementalt &solver; bmct &bmc; virtual void report(const cover_goalst &cover_goals); diff --git a/jbmc/src/jbmc/bmc.cpp b/jbmc/src/jbmc/bmc.cpp index 7cb6f68f95b..f5a29ffe3c5 100644 --- a/jbmc/src/jbmc/bmc.cpp +++ b/jbmc/src/jbmc/bmc.cpp @@ -42,19 +42,20 @@ void bmct::freeze_program_variables() decision_proceduret::resultt bmct::run_decision_procedure() { - status() << "Passing problem to " << prop_conv.decision_procedure_text() - << eom; + status() << "Passing problem to " + << decision_procedure.decision_procedure_text() << eom; auto solver_start = std::chrono::steady_clock::now(); - convert_symex_target_equation(equation, prop_conv, get_message_handler()); + convert_symex_target_equation( + equation, decision_procedure, get_message_handler()); // hook for cegis to freeze synthesis program vars freeze_program_variables(); - status() << "Running " << prop_conv.decision_procedure_text() << eom; + status() << "Running " << decision_procedure.decision_procedure_text() << eom; - decision_proceduret::resultt dec_result = prop_conv(); + decision_proceduret::resultt dec_result = decision_procedure(); { auto solver_stop = std::chrono::steady_clock::now(); @@ -207,11 +208,11 @@ safety_checkert::resultt bmct::stop_on_fail() { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(prop_conv), equation); + dynamic_cast(decision_procedure), equation); } build_error_trace( - error_trace, ns, equation, prop_conv, ui_message_handler); + error_trace, ns, equation, decision_procedure, ui_message_handler); output_error_trace(error_trace, ns, trace_options(), ui_message_handler); output_graphml(error_trace, ns, options); } @@ -265,12 +266,11 @@ int bmct::do_language_agnostic_bmc( { std::unique_ptr cbmc_solver = solvers.get_solver(); - prop_convt &pc = cbmc_solver->prop_conv(); bmct bmc( opts, symbol_table, ui, - pc, + cbmc_solver->decision_procedure_incremental(), *worklist, callback_after_symex, guard_manager); @@ -314,13 +314,12 @@ int bmct::do_language_agnostic_bmc( { std::unique_ptr cbmc_solver = solvers.get_solver(); - prop_convt &pc = cbmc_solver->prop_conv(); path_storaget::patht &resume = worklist->peek(); path_explorert pe( opts, symbol_table, ui, - pc, + cbmc_solver->decision_procedure_incremental(), resume.equation, resume.state, *worklist, diff --git a/jbmc/src/jbmc/bmc.h b/jbmc/src/jbmc/bmc.h index 44c0754d3aa..21fa341b570 100644 --- a/jbmc/src/jbmc/bmc.h +++ b/jbmc/src/jbmc/bmc.h @@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include class cbmc_solverst; @@ -68,7 +68,7 @@ class bmct : public safety_checkert const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, - prop_convt &_prop_conv, + decision_procedure_incrementalt &_decision_procedure, path_storaget &_path_storage, std::function callback_after_symex, guard_managert &guard_manager) @@ -86,7 +86,7 @@ class bmct : public safety_checkert options, path_storage, guard_manager), - prop_conv(_prop_conv), + decision_procedure(_decision_procedure), ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) { @@ -141,7 +141,7 @@ class bmct : public safety_checkert const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, - prop_convt &_prop_conv, + decision_procedure_incrementalt &_decision_procedure, symex_target_equationt &_equation, path_storaget &_path_storage, std::function callback_after_symex, @@ -160,7 +160,7 @@ class bmct : public safety_checkert options, path_storage, guard_manager), - prop_conv(_prop_conv), + decision_procedure(_decision_procedure), ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) { @@ -180,7 +180,7 @@ class bmct : public safety_checkert guard_managert &guard_manager; path_storaget &path_storage; symex_bmct symex; - prop_convt &prop_conv; + decision_procedure_incrementalt &decision_procedure; std::unique_ptr memory_model; // use gui format ui_message_handlert &ui_message_handler; @@ -235,7 +235,7 @@ class path_explorert : public bmct const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, - prop_convt &_prop_conv, + decision_procedure_incrementalt &_decision_procedure, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, @@ -245,7 +245,7 @@ class path_explorert : public bmct _options, outer_symbol_table, _message_handler, - _prop_conv, + _decision_procedure, saved_equation, path_storage, callback_after_symex, diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index e39bbede197..82aa4eb4b3a 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -25,7 +25,7 @@ Author: Daniel Kroening, Peter Schrammel #include -#include +#include #include #include @@ -42,13 +42,13 @@ void build_error_trace( goto_tracet &goto_trace, const namespacet &ns, const symex_target_equationt &symex_target_equation, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, ui_message_handlert &ui_message_handler) { messaget log(ui_message_handler); message_building_error_trace(log); - build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace); + build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace); } ssa_step_predicatet @@ -56,9 +56,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id) { return [property_id]( symex_target_equationt::SSA_stepst::const_iterator step, - const prop_convt &prop_conv) { + const decision_proceduret &decision_procedure) { return step->is_assert() && step->get_property_id() == property_id && - prop_conv.l_get(step->cond_literal).is_false(); + decision_procedure.l_get(step->cond_literal).is_false(); }; } @@ -105,14 +105,14 @@ void output_error_trace( void freeze_guards( const symex_target_equationt &equation, - prop_convt &prop_conv) + decision_procedure_incrementalt &decision_procedure) { for(const auto &step : equation.SSA_steps) { if(!step.guard_literal.is_constant()) - prop_conv.set_frozen(step.guard_literal); + decision_procedure.set_frozen(step.guard_literal); if(step.is_assert() && !step.cond_literal.is_constant()) - prop_conv.set_frozen(step.cond_literal); + decision_procedure.set_frozen(step.cond_literal); } } @@ -162,14 +162,14 @@ void output_graphml( void convert_symex_target_equation( symex_target_equationt &equation, - prop_convt &prop_conv, + decision_proceduret &decision_procedure, message_handlert &message_handler) { messaget msg(message_handler); msg.status() << "converting SSA" << messaget::eom; // convert SSA - equation.convert(prop_conv); + equation.convert(decision_procedure); } std::unique_ptr diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 6c39c116ed0..5faf74fab80 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -28,7 +28,8 @@ class memory_model_baset; class message_handlert; class namespacet; class optionst; -class prop_convt; +class decision_proceduret; +class decision_procedure_incrementalt; class symex_bmct; class symex_target_equationt; struct trace_optionst; @@ -36,7 +37,7 @@ class ui_message_handlert; void convert_symex_target_equation( symex_target_equationt &, - prop_convt &, + decision_proceduret &, message_handlert &); /// Returns a function that checks whether an SSA step is an assertion @@ -51,7 +52,7 @@ void build_error_trace( goto_tracet &, const namespacet &, const symex_target_equationt &, - const prop_convt &, + const decision_proceduret &, ui_message_handlert &); void output_error_trace( @@ -60,7 +61,9 @@ void output_error_trace( const trace_optionst &, ui_message_handlert &); -void freeze_guards(const symex_target_equationt &, prop_convt &); +void freeze_guards( + const symex_target_equationt &, + decision_procedure_incrementalt &); void output_graphml(const goto_tracet &, const namespacet &, const optionst &); void output_graphml( diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp index 2f35b90bdea..d9696db8b4c 100644 --- a/src/goto-checker/counterexample_beautification.cpp +++ b/src/goto-checker/counterexample_beautification.cpp @@ -26,7 +26,7 @@ counterexample_beautificationt::counterexample_beautificationt( } void counterexample_beautificationt::get_minimization_list( - prop_convt &prop_conv, + decision_proceduret &decision_procedure, const symex_target_equationt &equation, minimization_listt &minimization_list) { @@ -41,7 +41,7 @@ void counterexample_beautificationt::get_minimization_list( it->is_assignment() && it->assignment_type == symex_targett::assignment_typet::STATE) { - if(!prop_conv.l_get(it->guard_literal).is_false()) + if(!decision_procedure.l_get(it->guard_literal).is_false()) { const typet &type = it->ssa_lhs.type(); @@ -69,7 +69,7 @@ void counterexample_beautificationt::get_minimization_list( symex_target_equationt::SSA_stepst::const_iterator counterexample_beautificationt::get_failed_property( - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const symex_target_equationt &equation) { // find failed property @@ -79,8 +79,9 @@ counterexample_beautificationt::get_failed_property( it != equation.SSA_steps.end(); it++) if( - it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() && - prop_conv.l_get(it->cond_literal).is_false()) + it->is_assert() && + decision_procedure.l_get(it->guard_literal).is_true() && + decision_procedure.l_get(it->cond_literal).is_false()) return it; UNREACHABLE; diff --git a/src/goto-checker/counterexample_beautification.h b/src/goto-checker/counterexample_beautification.h index e1c73ae439f..21d0db28c4c 100644 --- a/src/goto-checker/counterexample_beautification.h +++ b/src/goto-checker/counterexample_beautification.h @@ -28,14 +28,14 @@ class counterexample_beautificationt protected: void get_minimization_list( - prop_convt &prop_conv, + decision_proceduret &decision_procedure, const symex_target_equationt &equation, minimization_listt &minimization_list); void minimize(const exprt &expr, class prop_minimizet &prop_minimize); symex_target_equationt::SSA_stepst::const_iterator get_failed_property( - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const symex_target_equationt &equation); // the failed property diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp index 9f59452f306..2819ca62574 100644 --- a/src/goto-checker/goto_symex_fault_localizer.cpp +++ b/src/goto-checker/goto_symex_fault_localizer.cpp @@ -11,13 +11,11 @@ Author: Peter Schrammel #include "goto_symex_fault_localizer.h" -#include - goto_symex_fault_localizert::goto_symex_fault_localizert( const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, - prop_convt &solver) + decision_procedure_incrementalt &solver) : options(options), ui_message_handler(ui_message_handler), equation(equation), diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h index 4d96eb2e703..a59fe0327e3 100644 --- a/src/goto-checker/goto_symex_fault_localizer.h +++ b/src/goto-checker/goto_symex_fault_localizer.h @@ -18,6 +18,8 @@ Author: Peter Schrammel #include +#include + #include "fault_localization_provider.h" class goto_symex_fault_localizert @@ -27,7 +29,7 @@ class goto_symex_fault_localizert const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, - prop_convt &solver); + decision_procedure_incrementalt &solver); fault_location_infot operator()(const irep_idt &failed_property_id); @@ -35,7 +37,7 @@ class goto_symex_fault_localizert const optionst &options; ui_message_handlert &ui_message_handler; const symex_target_equationt &equation; - prop_convt &solver; + decision_procedure_incrementalt &solver; /// A localization point is a goto instruction that is potentially at fault typedef std::map diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index c474ad14bd5..3e6ad49abff 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -23,7 +23,9 @@ goto_symex_property_decidert::goto_symex_property_decidert( ns, ui_message_handler, ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI); + solver = solvers.get_solver(); + decision_procedure = &solver->decision_procedure_incremental(); } exprt goto_symex_property_decidert::goalt::as_expr() const @@ -69,7 +71,7 @@ void goto_symex_property_decidert::convert_goals() // Our goal is to falsify a property, i.e., we will // add the negation of the property as goal. goal_pair.second.condition = - !solver->prop_conv().convert(goal_pair.second.as_expr()); + !decision_procedure->convert(goal_pair.second.as_expr()); } } @@ -78,7 +80,7 @@ void goto_symex_property_decidert::freeze_goal_variables() for(const auto &goal_pair : goal_map) { if(!goal_pair.second.condition.is_constant()) - solver->prop_conv().set_frozen(goal_pair.second.condition); + decision_procedure->set_frozen(goal_pair.second.condition); } } @@ -98,17 +100,18 @@ void goto_symex_property_decidert::add_constraint_from_goals( } // this is 'false' if there are no disjuncts - solver->prop_conv().set_to_true(disjunction(disjuncts)); + decision_procedure->set_to_true(disjunction(disjuncts)); } decision_proceduret::resultt goto_symex_property_decidert::solve() { - return solver->prop_conv()(); + return (*decision_procedure)(); } -prop_convt &goto_symex_property_decidert::get_solver() const +decision_procedure_incrementalt & +goto_symex_property_decidert::get_solver() const { - return solver->prop_conv(); + return *decision_procedure; } symex_target_equationt &goto_symex_property_decidert::get_equation() const @@ -129,7 +132,7 @@ void goto_symex_property_decidert::update_properties_status_from_goals( { auto &status = properties.at(goal_pair.first).status; if( - solver->prop_conv().l_get(goal_pair.second.condition).is_true() && + decision_procedure->l_get(goal_pair.second.condition).is_true() && status != property_statust::FAIL) { status |= property_statust::FAIL; diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 6ff272fdce3..2bbbd9fe1ce 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -49,7 +49,7 @@ class goto_symex_property_decidert decision_proceduret::resultt solve(); /// Returns the solver instance - prop_convt &get_solver() const; + decision_procedure_incrementalt &get_solver() const; /// Return the equation associated with this instance symex_target_equationt &get_equation() const; @@ -72,6 +72,7 @@ class goto_symex_property_decidert ui_message_handlert &ui_message_handler; symex_target_equationt &equation; std::unique_ptr solver; + decision_procedure_incrementalt *decision_procedure = nullptr; struct goalt { diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 753cf92c450..9674200e3ce 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -25,8 +25,8 @@ Author: Daniel Kroening, Peter Schrammel #endif #include +#include #include -#include #include #include #include @@ -45,29 +45,39 @@ solver_factoryt::solver_factoryt( { } -solver_factoryt::solvert::solvert(std::unique_ptr p) - : prop_conv_ptr(std::move(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)), prop_conv_ptr(std::move(p1)) + : 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)), prop_conv_ptr(std::move(p1)) + : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1)) { } -prop_convt &solver_factoryt::solvert::prop_conv() const +decision_proceduret &solver_factoryt::solvert::decision_procedure() const { - PRECONDITION(prop_conv_ptr != nullptr); - return *prop_conv_ptr; + PRECONDITION(decision_procedure_ptr != nullptr); + return *decision_procedure_ptr; +} + +decision_procedure_incrementalt & +solver_factoryt::solvert::decision_procedure_incremental() const +{ + PRECONDITION(decision_procedure_ptr != nullptr); + decision_procedure_incrementalt *solver = + dynamic_cast(&*decision_procedure_ptr); + INVARIANT(solver != nullptr, "incremental decision procedure required"); + return *solver; } propt &solver_factoryt::solvert::prop() const @@ -76,7 +86,8 @@ propt &solver_factoryt::solvert::prop() const return *prop_ptr; } -void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv) +void solver_factoryt::set_decision_procedure_time_limit( + decision_proceduret &decision_procedure) { const int timeout_seconds = options.get_signed_int_option("solver-time-limit"); @@ -84,12 +95,13 @@ void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv) if(timeout_seconds > 0) { solver_resource_limitst *solver = - dynamic_cast(&prop_conv); + dynamic_cast(&decision_procedure); if(solver == nullptr) { messaget log(message_handler); log.warning() << "cannot set solver time limit on " - << prop_conv.decision_procedure_text() << messaget::eom; + << decision_procedure.decision_procedure_text() + << messaget::eom; return; } @@ -97,9 +109,10 @@ void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv) } } -void solver_factoryt::solvert::set_prop_conv(std::unique_ptr p) +void solver_factoryt::solvert::set_decision_procedure( + std::unique_ptr p) { - prop_conv_ptr = std::move(p); + decision_procedure_ptr = std::move(p); } void solver_factoryt::solvert::set_prop(std::unique_ptr p) @@ -179,8 +192,8 @@ std::unique_ptr solver_factoryt::get_default() else if(options.get_option("arrays-uf") == "always") bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL; - set_prop_conv_time_limit(*bv_pointers); - solver->set_prop_conv(std::move(bv_pointers)); + set_decision_procedure_time_limit(*bv_pointers); + solver->set_decision_procedure(std::move(bv_pointers)); return solver; } @@ -225,9 +238,10 @@ std::unique_ptr solver_factoryt::get_bv_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto prop_conv = util_make_unique(info); - set_prop_conv_time_limit(*prop_conv); - return util_make_unique(std::move(prop_conv), std::move(prop)); + auto decision_procedure = util_make_unique(info); + set_decision_procedure_time_limit(*decision_procedure); + return util_make_unique( + std::move(decision_procedure), std::move(prop)); } /// the string refinement adds to the bit vector refinement specifications for @@ -249,9 +263,10 @@ solver_factoryt::get_string_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto prop_conv = util_make_unique(info); - set_prop_conv_time_limit(*prop_conv); - return util_make_unique(std::move(prop_conv), std::move(prop)); + auto decision_procedure = util_make_unique(info); + set_decision_procedure_time_limit(*decision_procedure); + return util_make_unique( + std::move(decision_procedure), std::move(prop)); } std::unique_ptr @@ -284,7 +299,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_dec->set_message_handler(message_handler); - set_prop_conv_time_limit(*smt2_dec); + set_decision_procedure_time_limit(*smt2_dec); return util_make_unique(std::move(smt2_dec)); } else if(filename == "-") @@ -300,7 +315,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; - set_prop_conv_time_limit(*smt2_conv); + set_decision_procedure_time_limit(*smt2_conv); return util_make_unique(std::move(smt2_conv)); } else @@ -328,7 +343,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; - set_prop_conv_time_limit(*smt2_conv); + set_decision_procedure_time_limit(*smt2_conv); return util_make_unique(std::move(smt2_conv), std::move(out)); } } diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index b8b9c50a549..cd6954eff68 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -20,7 +20,7 @@ class message_handlert; class namespacet; class optionst; class propt; -class prop_convt; +class decision_proceduret; class solver_factoryt { @@ -38,21 +38,24 @@ class solver_factoryt { public: solvert() = default; - explicit solvert(std::unique_ptr p); - solvert(std::unique_ptr p1, std::unique_ptr p2); - solvert(std::unique_ptr p1, std::unique_ptr p2); - - prop_convt &prop_conv() const; + explicit solvert(std::unique_ptr p); + solvert(std::unique_ptr p1, std::unique_ptr p2); + solvert( + std::unique_ptr p1, + std::unique_ptr p2); + + decision_proceduret &decision_procedure() const; + decision_procedure_incrementalt &decision_procedure_incremental() const; propt &prop() const; - void set_prop_conv(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 prop_conv_ptr; + std::unique_ptr decision_procedure_ptr; }; /// Returns a solvert object @@ -74,10 +77,11 @@ class solver_factoryt smt2_dect::solvert get_smt2_solver_type() const; - /// Sets the timeout of \p prop_conv if the `solver-time-limit` option - /// has a positive value (in seconds). + /// Sets the timeout of \p decision_procedure if the `solver-time-limit` + /// option has a positive value (in seconds). /// \note Most solvers silently ignore the time limit at the moment. - void set_prop_conv_time_limit(prop_convt &prop_conv); + void + set_decision_procedure_time_limit(decision_proceduret &decision_procedure); // consistency checks during solver creation void no_beautification(); diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index 7a81b6f312f..f0ea4c8437c 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -90,7 +90,7 @@ class scratch_programt:public goto_programt std::unique_ptr satcheck; bv_pointerst satchecker; smt2_dect z3; - prop_convt *checker; + decision_proceduret *checker; static optionst get_default_options(); }; diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index e8b68012bcd..266245aa647 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -20,13 +20,12 @@ Author: Daniel Kroening #include -#include -#include +#include #include "partial_order_concurrency.h" static exprt build_full_lhs_rec( - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, const exprt &src_original, // original identifiers const exprt &src_ssa) // renamed identifiers @@ -39,17 +38,18 @@ static exprt build_full_lhs_rec( if(id==ID_index) { // get index value from src_ssa - exprt index_value=prop_conv.get(to_index_expr(src_ssa).index()); + exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index()); if(index_value.is_not_nil()) { simplify(index_value, ns); index_exprt tmp=to_index_expr(src_original); tmp.index()=index_value; - tmp.array()= - build_full_lhs_rec(prop_conv, ns, - to_index_expr(src_original).array(), - to_index_expr(src_ssa).array()); + tmp.array() = build_full_lhs_rec( + decision_procedure, + ns, + to_index_expr(src_original).array(), + to_index_expr(src_ssa).array()); return std::move(tmp); } @@ -58,8 +58,9 @@ static exprt build_full_lhs_rec( else if(id==ID_member) { member_exprt tmp=to_member_expr(src_original); - tmp.struct_op()=build_full_lhs_rec( - prop_conv, ns, + tmp.struct_op() = build_full_lhs_rec( + decision_procedure, + ns, to_member_expr(src_original).struct_op(), to_member_expr(src_ssa).struct_op()); } @@ -67,13 +68,19 @@ static exprt build_full_lhs_rec( { if_exprt tmp2=to_if_expr(src_original); - tmp2.false_case()=build_full_lhs_rec(prop_conv, ns, - tmp2.false_case(), to_if_expr(src_ssa).false_case()); + tmp2.false_case() = build_full_lhs_rec( + decision_procedure, + ns, + tmp2.false_case(), + to_if_expr(src_ssa).false_case()); - tmp2.true_case()=build_full_lhs_rec(prop_conv, ns, - tmp2.true_case(), to_if_expr(src_ssa).true_case()); + tmp2.true_case() = build_full_lhs_rec( + decision_procedure, + ns, + tmp2.true_case(), + to_if_expr(src_ssa).true_case()); - exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond()); + exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond()); if(tmp.is_true()) return tmp2.true_case(); @@ -85,8 +92,11 @@ static exprt build_full_lhs_rec( else if(id==ID_typecast) { typecast_exprt tmp=to_typecast_expr(src_original); - tmp.op()=build_full_lhs_rec(prop_conv, ns, - to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op()); + tmp.op() = build_full_lhs_rec( + decision_procedure, + ns, + to_typecast_expr(src_original).op(), + to_typecast_expr(src_ssa).op()); return std::move(tmp); } else if(id==ID_byte_extract_little_endian || @@ -94,7 +104,7 @@ static exprt build_full_lhs_rec( { byte_extract_exprt tmp = to_byte_extract_expr(src_original); tmp.op() = build_full_lhs_rec( - prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op()); + decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op()); // re-write into big case-split } @@ -169,7 +179,8 @@ static void update_internal_field( /// Replace nondet values that appear in \p type by their values as found by /// \p solver. -static void replace_nondet_in_type(typet &type, const prop_convt &solver) +static void +replace_nondet_in_type(typet &type, const decision_proceduret &solver) { if(type.id() == ID_array) { @@ -182,7 +193,8 @@ static void replace_nondet_in_type(typet &type, const prop_convt &solver) /// Replace nondet values that appear in the type of \p expr and its /// subexpressions type by their values as found by \p solver. -static void replace_nondet_in_type(exprt &expr, const prop_convt &solver) +static void +replace_nondet_in_type(exprt &expr, const decision_proceduret &solver) { replace_nondet_in_type(expr.type(), solver); for(auto &sub : expr.operands()) @@ -192,7 +204,7 @@ static void replace_nondet_in_type(exprt &expr, const prop_convt &solver) void build_goto_trace( const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) { @@ -218,14 +230,14 @@ void build_goto_trace( { if( last_step_to_keep == target.SSA_steps.end() && - is_last_step_to_keep(it, prop_conv)) + is_last_step_to_keep(it, decision_procedure)) { last_step_to_keep = it; } const SSA_stept &SSA_step = *it; - if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true)) + if(decision_procedure.l_get(SSA_step.guard_literal) != tvt(true)) continue; if(it->is_constraint() || @@ -250,7 +262,7 @@ void build_goto_trace( // these are just used to get the time stamp -- the clock type is // computed to be of the minimal necessary size, but we don't need to // know it to get the value so just use typeless - exprt clock_value = prop_conv.get( + exprt clock_value = decision_procedure.get( symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it))); const auto cv = numeric_cast(clock_value); @@ -342,7 +354,7 @@ void build_goto_trace( goto_trace_step.function_arguments = SSA_step.converted_function_arguments; for(auto &arg : goto_trace_step.function_arguments) - arg = prop_conv.get(arg); + arg = decision_procedure.get(arg); // update internal field for specific variables in the counterexample update_internal_field(SSA_step, goto_trace_step, ns); @@ -359,15 +371,20 @@ void build_goto_trace( if(SSA_step.original_full_lhs.is_not_nil()) { goto_trace_step.full_lhs = build_full_lhs_rec( - prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs); - replace_nondet_in_type(goto_trace_step.full_lhs, prop_conv); + decision_procedure, + ns, + SSA_step.original_full_lhs, + SSA_step.ssa_full_lhs); + replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure); } if(SSA_step.ssa_full_lhs.is_not_nil()) { - goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs); + goto_trace_step.full_lhs_value = + decision_procedure.get(SSA_step.ssa_full_lhs); simplify(goto_trace_step.full_lhs_value, ns); - replace_nondet_in_type(goto_trace_step.full_lhs_value, prop_conv); + replace_nondet_in_type( + goto_trace_step.full_lhs_value, decision_procedure); } for(const auto &j : SSA_step.converted_io_args) @@ -378,7 +395,7 @@ void build_goto_trace( } else { - exprt tmp = prop_conv.get(j); + exprt tmp = decision_procedure.get(j); goto_trace_step.io_args.push_back(tmp); } } @@ -388,7 +405,7 @@ void build_goto_trace( goto_trace_step.cond_expr = SSA_step.cond_expr; goto_trace_step.cond_value = - prop_conv.l_get(SSA_step.cond_literal).is_true(); + decision_procedure.l_get(SSA_step.cond_literal).is_true(); } if(ssa_step_it == last_step_to_keep) @@ -400,31 +417,33 @@ void build_goto_trace( void build_goto_trace( const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) { - const auto is_last_step_to_keep = [last_step_to_keep]( - symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) { - return last_step_to_keep == it; - }; + const auto is_last_step_to_keep = + [last_step_to_keep]( + symex_target_equationt::SSA_stepst::const_iterator it, + const decision_proceduret &) { return last_step_to_keep == it; }; return build_goto_trace( - target, is_last_step_to_keep, prop_conv, ns, goto_trace); + target, is_last_step_to_keep, decision_procedure, ns, goto_trace); } static bool is_failed_assertion_step( symex_target_equationt::SSA_stepst::const_iterator step, - const prop_convt &prop_conv) + const decision_proceduret &decision_procedure) { - return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false(); + return step->is_assert() && + decision_procedure.l_get(step->cond_literal).is_false(); } void build_goto_trace( const symex_target_equationt &target, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) { - build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace); + build_goto_trace( + target, is_failed_assertion_step, decision_procedure, ns, goto_trace); } diff --git a/src/goto-symex/build_goto_trace.h b/src/goto-symex/build_goto_trace.h index e1006b3b604..bac90da760e 100644 --- a/src/goto-symex/build_goto_trace.h +++ b/src/goto-symex/build_goto_trace.h @@ -20,12 +20,12 @@ Date: July 2005 /// Build a trace by going through the steps of \p target and stopping at the /// first failing assertion /// \param target: SSA form of the program -/// \param prop_conv: solver from which to get valuations +/// \param decision_procedure: solver from which to get valuations /// \param ns: namespace /// \param [out] goto_trace: trace to which the steps of the trace get appended void build_goto_trace( const symex_target_equationt &target, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace); @@ -33,18 +33,19 @@ void build_goto_trace( /// the given step /// \param target: SSA form of the program /// \param last_step_to_keep: iterator pointing to the last step to keep -/// \param prop_conv: solver from which to get valuations +/// \param decision_procedure: solver from which to get valuations /// \param ns: namespace /// \param [out] goto_trace: trace to which the steps of the trace get appended void build_goto_trace( const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace); -typedef std::function< - bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> +typedef std::function ssa_step_predicatet; /// Build a trace by going through the steps of \p target and stopping after @@ -52,13 +53,13 @@ typedef std::function< /// \param target: SSA form of the program /// \param stop_after_predicate: function with an SSA step iterator and solver /// as argument, which should return true for the last step to keep -/// \param prop_conv: solver from which to get valuations +/// \param decision_procedure: solver from which to get valuations /// \param ns: namespace /// \param [out] goto_trace: trace to which the steps of the trace get appended void build_goto_trace( const symex_target_equationt &target, ssa_step_predicatet stop_after_predicate, - const prop_convt &prop_conv, + const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace); diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 9eb7d711071..a98bd8a5d55 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -18,9 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include -#include #include "equation_conversion_exceptions.h" #include "goto_symex_state.h" @@ -329,20 +328,19 @@ void symex_target_equationt::constraint( merge_ireps(SSA_step); } -void symex_target_equationt::convert( - prop_convt &prop_conv) +void symex_target_equationt::convert(decision_proceduret &decision_procedure) { try { - convert_guards(prop_conv); - convert_assignments(prop_conv); - convert_decls(prop_conv); - convert_assumptions(prop_conv); - convert_assertions(prop_conv); - convert_goto_instructions(prop_conv); - convert_function_calls(prop_conv); - convert_io(prop_conv); - convert_constraints(prop_conv); + convert_guards(decision_procedure); + convert_assignments(decision_procedure); + convert_decls(decision_procedure); + convert_assumptions(decision_procedure); + convert_assertions(decision_procedure); + convert_goto_instructions(decision_procedure); + convert_function_calls(decision_procedure); + convert_io(decision_procedure); + convert_constraints(decision_procedure); } catch(const equation_conversion_exceptiont &conversion_exception) { @@ -370,7 +368,8 @@ void symex_target_equationt::convert_assignments( } } -void symex_target_equationt::convert_decls(prop_convt &prop_conv) +void symex_target_equationt::convert_decls( + decision_proceduret &decision_procedure) { for(auto &step : SSA_steps) { @@ -380,7 +379,7 @@ void symex_target_equationt::convert_decls(prop_convt &prop_conv) // the satisfiability of the formula. try { - prop_conv.convert(step.cond_expr); + decision_procedure.convert(step.cond_expr); step.converted = true; } catch(const bitvector_conversion_exceptiont &) @@ -394,7 +393,7 @@ void symex_target_equationt::convert_decls(prop_convt &prop_conv) } void symex_target_equationt::convert_guards( - prop_convt &prop_conv) + decision_proceduret &decision_procedure) { for(auto &step : SSA_steps) { @@ -409,7 +408,7 @@ void symex_target_equationt::convert_guards( try { - step.guard_literal = prop_conv.convert(step.guard); + step.guard_literal = decision_procedure.convert(step.guard); } catch(const bitvector_conversion_exceptiont &) { @@ -422,7 +421,7 @@ void symex_target_equationt::convert_guards( } void symex_target_equationt::convert_assumptions( - prop_convt &prop_conv) + decision_proceduret &decision_procedure) { for(auto &step : SSA_steps) { @@ -440,7 +439,7 @@ void symex_target_equationt::convert_assumptions( try { - step.cond_literal = prop_conv.convert(step.cond_expr); + step.cond_literal = decision_procedure.convert(step.cond_expr); } catch(const bitvector_conversion_exceptiont &) { @@ -454,7 +453,7 @@ void symex_target_equationt::convert_assumptions( } void symex_target_equationt::convert_goto_instructions( - prop_convt &prop_conv) + decision_proceduret &decision_procedure) { for(auto &step : SSA_steps) { @@ -472,7 +471,7 @@ void symex_target_equationt::convert_goto_instructions( try { - step.cond_literal = prop_conv.convert(step.cond_expr); + step.cond_literal = decision_procedure.convert(step.cond_expr); } catch(const bitvector_conversion_exceptiont &) { @@ -512,7 +511,7 @@ void symex_target_equationt::convert_constraints( } void symex_target_equationt::convert_assertions( - prop_convt &prop_conv) + decision_proceduret &decision_procedure) { // we find out if there is only _one_ assertion, // which allows for a simpler formula @@ -533,12 +532,12 @@ void symex_target_equationt::convert_assertions( if(step.is_assert() && !step.ignore && !step.converted) { step.converted = true; - prop_conv.set_to_false(step.cond_expr); + decision_procedure.set_to_false(step.cond_expr); step.cond_literal=const_literal(false); return; // prevent further assumptions! } else if(step.is_assume()) - prop_conv.set_to_true(step.cond_expr); + decision_procedure.set_to_true(step.cond_expr); } UNREACHABLE; // unreachable @@ -573,7 +572,7 @@ void symex_target_equationt::convert_assertions( // do the conversion try { - step.cond_literal = prop_conv.convert(implication); + step.cond_literal = decision_procedure.convert(implication); } catch(const bitvector_conversion_exceptiont &) { @@ -598,7 +597,7 @@ void symex_target_equationt::convert_assertions( } // the below is 'true' if there are no assertions - prop_conv.set_to_true(disjunction(disjuncts)); + decision_procedure.set_to_true(disjunction(disjuncts)); } void symex_target_equationt::convert_function_calls( diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 0776967602f..045fca809a3 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -32,7 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com class decision_proceduret; class namespacet; -class prop_convt; +class decision_proceduret; /// Inheriting the interface of symex_targett this class represents the SSA /// form of the input program as a list of \ref SSA_stept. It further extends @@ -176,51 +176,57 @@ class symex_target_equationt:public symex_targett /// Interface method to initiate the conversion into a decision procedure /// format. The method iterates over the equation, i.e. over the SSA steps and /// converts each type of step separately. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert(decision_proceduret &decision_procedure); /// Converts assignments: set the equality _lhs==rhs_ to _True_. /// \param decision_procedure: A handle to a particular decision procedure - /// interface + /// interface void convert_assignments(decision_proceduret &decision_procedure); /// Converts declarations: these are effectively ignored by the decision /// procedure. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert_decls(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_decls(decision_proceduret &decision_procedure); /// Converts assumptions: convert the expression the assumption represents. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert_assumptions(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_assumptions(decision_proceduret &decision_procedure); /// Converts assertions: build a disjunction of negated assertions. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert_assertions(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_assertions(decision_proceduret &decision_procedure); /// Converts constraints: set the represented condition to _True_. /// \param decision_procedure: A handle to a particular decision procedure - /// interface + /// interface void convert_constraints(decision_proceduret &decision_procedure); /// Converts goto instructions: convert the expression representing the /// condition of this goto. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert_goto_instructions(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_goto_instructions(decision_proceduret &decision_procedure); /// Converts guards: convert the expression the guard represents. - /// \param prop_conv: A handle to a particular decision procedure interface - void convert_guards(prop_convt &prop_conv); + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_guards(decision_proceduret &decision_procedure); /// Converts function calls: for each argument build an equality between its /// symbol and the argument itself. /// \param decision_procedure: A handle to a particular decision procedure - /// interface + /// interface void convert_function_calls(decision_proceduret &decision_procedure); /// Converts I/O: for each argument build an equality between its /// symbol and the argument itself. /// \param decision_procedure: A handle to a particular decision procedure - /// interface + /// interface void convert_io(decision_proceduret &decision_procedure); exprt make_expression() const; diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 81a435735cb..161afa4385f 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -145,10 +145,10 @@ SRC = $(BOOLEFORCE_SRC) \ prop/bdd_expr.cpp \ prop/cover_goals.cpp \ prop/decision_procedure.cpp \ + prop/decision_procedure_incremental.cpp \ prop/literal.cpp \ prop/prop_minimize.cpp \ prop/prop.cpp \ - prop/prop_conv.cpp \ prop/prop_conv_solver.cpp \ qbf/qbf_quantor.cpp \ qbf/qbf_qube.cpp \ diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp index 2588275b14f..92009bb6aad 100644 --- a/src/solvers/flattening/functions.cpp +++ b/src/solvers/flattening/functions.cpp @@ -66,7 +66,7 @@ void functionst::add_function_constraints(const function_infot &info) implies_exprt implication(arguments_equal_expr, equal_exprt(*it1, *it2)); - prop_conv.set_to_true(implication); + decision_procedure.set_to_true(implication); } } } diff --git a/src/solvers/flattening/functions.h b/src/solvers/flattening/functions.h index fe2018ef12e..abf9e66c960 100644 --- a/src/solvers/flattening/functions.h +++ b/src/solvers/flattening/functions.h @@ -12,17 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H #define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H +#include #include #include -#include +#include class functionst { public: - explicit functionst(prop_convt &_prop_conv): - prop_conv(_prop_conv) { } + explicit functionst(decision_proceduret &_decision_procedure) + : decision_procedure(_decision_procedure) + { + } virtual ~functionst() { @@ -37,7 +40,7 @@ class functionst } protected: - prop_convt &prop_conv; + decision_proceduret &decision_procedure; typedef std::set applicationst; diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 5099e81f80c..9e3b78dfcf5 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "decision_procedure_incremental.h" #include "literal_expr.h" -#include "prop_conv.h" cover_goalst::~cover_goalst() { @@ -28,8 +28,9 @@ void cover_goalst::mark() o->satisfying_assignment(); for(auto &g : goals) - if(g.status==goalt::statust::UNKNOWN && - prop_conv.l_get(g.condition).is_true()) + if( + g.status == goalt::statust::UNKNOWN && + decision_procedure.l_get(g.condition).is_true()) { g.status=goalt::statust::COVERED; _number_covered++; @@ -56,7 +57,7 @@ void cover_goalst::constraint() disjuncts.push_back(literal_exprt(g_it->condition)); // this is 'false' if there are no disjuncts - prop_conv.set_to_true(disjunction(disjuncts)); + decision_procedure.set_to_true(disjunction(disjuncts)); } /// Build clause @@ -67,7 +68,7 @@ void cover_goalst::freeze_goal_variables() g_it!=goals.end(); g_it++) if(!g_it->condition.is_constant()) - prop_conv.set_frozen(g_it->condition); + decision_procedure.set_frozen(g_it->condition); } /// Try to cover all goals @@ -88,7 +89,7 @@ operator()(message_handlert &message_handler) _iterations++; constraint(); - dec_result = prop_conv(); + dec_result = decision_procedure(); switch(dec_result) { diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index 8c4593313a2..62e197f7e07 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -14,21 +14,21 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "decision_procedure.h" +#include "decision_procedure_incremental.h" #include "literal.h" class message_handlert; -class prop_convt; +class decision_proceduret; /// Try to cover some given set of goals incrementally. This can be seen as a /// heuristic variant of SAT-based set-cover. No minimality guarantee. class cover_goalst { public: - explicit cover_goalst(prop_convt &_prop_conv): - _number_covered(0), - _iterations(0), - prop_conv(_prop_conv) + explicit cover_goalst(decision_procedure_incrementalt &_decision_procedure) + : _number_covered(0), + _iterations(0), + decision_procedure(_decision_procedure) { } @@ -95,7 +95,7 @@ class cover_goalst protected: std::size_t _number_covered; unsigned _iterations; - prop_convt &prop_conv; + decision_procedure_incrementalt &decision_procedure; typedef std::vector observerst; observerst observers; diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/decision_procedure_incremental.cpp similarity index 58% rename from src/solvers/prop/prop_conv.cpp rename to src/solvers/prop/decision_procedure_incremental.cpp index b371aa37e21..5f2f4c57b13 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/decision_procedure_incremental.cpp @@ -6,27 +6,27 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "prop_conv.h" +#include "decision_procedure_incremental.h" #include /// determine whether a variable is in the final conflict -bool prop_convt::is_in_conflict(literalt) const +bool decision_procedure_incrementalt::is_in_conflict(literalt) const { UNREACHABLE; return false; } -void prop_convt::set_assumptions(const bvt &) +void decision_procedure_incrementalt::set_assumptions(const bvt &) { UNREACHABLE; } -void prop_convt::set_frozen(const literalt) +void decision_procedure_incrementalt::set_frozen(const literalt) { UNREACHABLE; } -void prop_convt::set_frozen(const bvt &bv) +void decision_procedure_incrementalt::set_frozen(const bvt &bv) { for(const auto &bit : bv) if(!bit.is_constant()) diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/decision_procedure_incremental.h similarity index 65% rename from src/solvers/prop/prop_conv.h rename to src/solvers/prop/decision_procedure_incremental.h index f65ce436043..a500d7c3fc2 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/decision_procedure_incremental.h @@ -6,12 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H +#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H -#ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H -#define CPROVER_SOLVERS_PROP_PROP_CONV_H - -#include #include +#include #include #include @@ -25,10 +24,12 @@ Author: Daniel Kroening, kroening@kroening.com // API that provides a "handle" in the form of a literalt // for expressions. -class prop_convt:public decision_proceduret +class decision_procedure_incrementalt : public decision_proceduret { public: - virtual ~prop_convt() { } + virtual ~decision_procedure_incrementalt() + { + } using decision_proceduret::operator(); @@ -36,12 +37,20 @@ class prop_convt:public decision_proceduret virtual void set_frozen(literalt a); virtual void set_frozen(const bvt &); virtual void set_assumptions(const bvt &_assumptions); - virtual bool has_set_assumptions() const { return false; } - virtual void set_all_frozen() {} + virtual bool has_set_assumptions() const + { + return false; + } + virtual void set_all_frozen() + { + } // returns true if an assumption is in the final conflict virtual bool is_in_conflict(literalt l) const; - virtual bool has_is_in_conflict() const { return false; } + virtual bool has_is_in_conflict() const + { + return false; + } }; // @@ -49,4 +58,4 @@ class prop_convt:public decision_proceduret // propositional skeleton by passing it to a propt // -#endif // CPROVER_SOLVERS_PROP_PROP_CONV_H +#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index b0600ad1ded..c46a7f40c4a 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "decision_procedure.h" +#include "decision_procedure_incremental.h" #include "literal.h" #include "literal_expr.h" #include "prop.h" -#include "prop_conv.h" #include "solver_resource_limits.h" -class prop_conv_solvert : public prop_convt, public solver_resource_limitst +class prop_conv_solvert : public decision_procedure_incrementalt, + public solver_resource_limitst { public: prop_conv_solvert(propt &_prop, message_handlert &message_handler) @@ -43,8 +43,8 @@ class prop_conv_solvert : public prop_convt, public solver_resource_limitst } exprt get(const exprt &expr) const override; - // overloading from prop_convt - using prop_convt::set_frozen; + // overloading from decision_proceduret + using decision_procedure_incrementalt::set_frozen; tvt l_get(literalt a) const override { return prop.l_get(a); diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp index eb3bf9e6f9c..a40e4ce0446 100644 --- a/src/solvers/prop/prop_minimize.cpp +++ b/src/solvers/prop/prop_minimize.cpp @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "literal_expr.h" prop_minimizet::prop_minimizet( - prop_convt &_prop_conv, + decision_procedure_incrementalt &_decision_procedure, message_handlert &message_handler) - : prop_conv(_prop_conv), log(message_handler) + : decision_procedure(_decision_procedure), log(message_handler) { } @@ -47,11 +47,12 @@ void prop_minimizet::fix_objectives() o_it != entry.end(); ++o_it) { - if(!o_it->fixed && prop_conv.l_get(o_it->condition).is_false()) + if(!o_it->fixed && decision_procedure.l_get(o_it->condition).is_false()) { _number_satisfied++; _value += current->first; - prop_conv.set_to(literal_exprt(o_it->condition), false); // fix it + decision_procedure.set_to( + literal_exprt(o_it->condition), false); // fix it o_it->fixed = true; found = true; } @@ -88,7 +89,7 @@ literalt prop_minimizet::constraint() forall_literals(it, or_clause) disjuncts.push_back(literal_exprt(*it)); - return prop_conv.convert(disjunction(disjuncts)); + return decision_procedure.convert(disjunction(disjuncts)); } } @@ -96,7 +97,7 @@ literalt prop_minimizet::constraint() void prop_minimizet::operator()() { // we need to use assumptions - PRECONDITION(prop_conv.has_set_assumptions()); + PRECONDITION(decision_procedure.has_set_assumptions()); _iterations = 0; _number_satisfied = 0; @@ -122,8 +123,8 @@ void prop_minimizet::operator()() bvt assumptions; assumptions.push_back(c); - prop_conv.set_assumptions(assumptions); - dec_result = prop_conv(); + decision_procedure.set_assumptions(assumptions); + dec_result = decision_procedure(); switch(dec_result) { @@ -151,7 +152,7 @@ void prop_minimizet::operator()() // Run solver again to get one. bvt assumptions; // no assumptions - prop_conv.set_assumptions(assumptions); - (void)prop_conv(); + decision_procedure.set_assumptions(assumptions); + (void)decision_procedure(); } } diff --git a/src/solvers/prop/prop_minimize.h b/src/solvers/prop/prop_minimize.h index de3d730398f..5336d465174 100644 --- a/src/solvers/prop/prop_minimize.h +++ b/src/solvers/prop/prop_minimize.h @@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "prop_conv.h" +#include "decision_procedure_incremental.h" /// Computes a satisfying assignment of minimal cost according to a const /// function using incremental SAT class prop_minimizet { public: - prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler); + prop_minimizet(decision_procedure_incrementalt &, message_handlert &); void operator()(); @@ -71,7 +71,7 @@ class prop_minimizet std::size_t _number_satisfied = 0; std::size_t _number_objectives = 0; weightt _value = 0; - prop_convt &prop_conv; + decision_procedure_incrementalt &decision_procedure; messaget log; literalt constraint(); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 774df1f4adf..94dfc136388 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -20,9 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#include #include #include +#include #include "letify.h" @@ -31,7 +31,7 @@ class constant_exprt; class index_exprt; class member_exprt; -class smt2_convt:public prop_convt +class smt2_convt : public decision_procedure_incrementalt { public: enum class solvert From 8927b7dc032e9015ccb1889530d3f7022a91aa9b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 27 Mar 2019 17:43:23 +0000 Subject: [PATCH 2/8] Update decision procedure docs --- src/cbmc/README.md | 2 +- src/goto-symex/README.md | 2 +- src/solvers/README.md | 12 +++++++----- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/cbmc/README.md b/src/cbmc/README.md index c734456f9a1..72995dfbd6e 100644 --- a/src/cbmc/README.md +++ b/src/cbmc/README.md @@ -96,7 +96,7 @@ each assertion was violated. This is constructed using `build_goto_trace`, which queries the backend asking what value was chosen for each program variable on the path from the start of the program to the relevant assertion. For more details on how the trace is populated see the documentation for -`build_goto_trace` for `prop_convt::get`, the function used to query the +`build_goto_trace` for `decision_proceduret::get`, the function used to query the backend. ## Path-symex diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md index d9f63ec3a78..9511985995d 100644 --- a/src/goto-symex/README.md +++ b/src/goto-symex/README.md @@ -260,7 +260,7 @@ In the \ref goto-symex directory. **Key classes:** * \ref symex_target_equationt -* \ref prop_convt +* \ref decision_proceduret * \ref bmct * \ref counterexample_beautificationt diff --git a/src/solvers/README.md b/src/solvers/README.md index 1909f3e9c3b..4b9dc66513a 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -56,9 +56,11 @@ getting an over-view of the solvers currently supported. Many (but not all) decision procedures have a notion of logical expression and can provide information about logical expressions -within the solver. `prop_convt` expands on the interface of -`decision_proceduret` to add a data-type (`literalt`) and interfaces -for manipulating logical expressions within the solver. +within the solver. `decision_proceduret` also has functions to +get a handle (in the form of a `literalt`) on a particular +Boolean expression within the solver, which is useful the +retrieve to easily the truth value of that expression from +a satisfying assignment. Within decision procedures it is common to reduce the logical expressions to equivalent expressions in a simpler language. This is @@ -75,7 +77,7 @@ processors, creating a good SAT solver is a very specialised skill, so CPROVER uses third-party SAT solvers. By default this is MiniSAT, but others are supported (see the `sat/` directory). To do this it needs a software interface to a SAT solver : this is `propt`. It uses the -same `literalt` to refer to Boolean variables, just as `prop_convt` +same `literalt` to refer to Boolean variables, just as `decision_proceduret` uses them to refer to logical expressions. `land`, `lor`, `lxor` and so on allow gates to be constructed to express the formulae to be solved. If `cnf_handled_well` is true then you may also use `lcnf` to @@ -83,7 +85,7 @@ build formulae. Finally, `prop_solve` will run the decision procedure. As previously mentioned, many decision procedures reduce formulae to CNF and solve with a SAT solver. `prop_conv_solvert` contains the -foundations of this conversion. It implements the `prop_convt` by +foundations of this conversion. It implements the `decision_proceduret` by having an instance of `propt` (a SAT solver) and reducing the expressions that are input into CNF. The key entry point to this procedure is `prop_conv_solvert::convert` which then splits into From f62db13c94fd1bf735bb99d72152ccf3a22bc353 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 27 Mar 2019 22:37:44 +0000 Subject: [PATCH 3/8] Split out decision procedure with solving under assumptions Makes it explicit which algorithms actually require this feature. --- src/goto-checker/bmc_util.cpp | 12 ++-- .../goto_symex_fault_localizer.cpp | 2 +- src/goto-checker/goto_symex_fault_localizer.h | 6 +- .../goto_symex_property_decider.cpp | 7 ++- .../goto_symex_property_decider.h | 2 +- src/goto-checker/multi_path_symex_checker.cpp | 22 +++++-- .../single_path_symex_checker.cpp | 9 +-- src/goto-checker/solver_factory.cpp | 12 ++++ src/goto-checker/solver_factory.h | 7 ++- src/solvers/prop/cover_goals.cpp | 1 + .../prop/decision_procedure_assumptions.h | 29 +++++++++ .../prop/decision_procedure_incremental.cpp | 20 +------ .../prop/decision_procedure_incremental.h | 59 ++++++------------- src/solvers/prop/prop_conv_solver.h | 12 +--- src/solvers/prop/prop_minimize.cpp | 5 +- src/solvers/prop/prop_minimize.h | 6 +- src/solvers/smt2/smt2_conv.cpp | 18 ++++++ src/solvers/smt2/smt2_conv.h | 10 ++-- src/solvers/smt2/smt2_dec.h | 8 +-- 19 files changed, 133 insertions(+), 114 deletions(-) create mode 100644 src/solvers/prop/decision_procedure_assumptions.h diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 82aa4eb4b3a..f648c81ad09 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -368,13 +368,14 @@ std::chrono::duration prepare_property_decider( { auto solver_start = std::chrono::steady_clock::now(); + decision_proceduret &decision_procedure = + property_decider.get_solver().decision_procedure(); messaget log(ui_message_handler); log.status() << "Passing problem to " - << property_decider.get_solver().decision_procedure_text() - << messaget::eom; + << decision_procedure.decision_procedure_text() << messaget::eom; convert_symex_target_equation( - equation, property_decider.get_solver(), ui_message_handler); + equation, decision_procedure, ui_message_handler); property_decider.update_properties_goals_from_symex_target_equation( properties); property_decider.convert_goals(); @@ -394,9 +395,10 @@ void run_property_decider( { auto solver_start = std::chrono::steady_clock::now(); + const decision_proceduret &decision_procedure = + property_decider.get_solver().decision_procedure(); messaget log(ui_message_handler); - log.status() << "Running " - << property_decider.get_solver().decision_procedure_text() + log.status() << "Running " << decision_procedure.decision_procedure_text() << messaget::eom; property_decider.add_constraint_from_goals( diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp index 2819ca62574..fd69163e930 100644 --- a/src/goto-checker/goto_symex_fault_localizer.cpp +++ b/src/goto-checker/goto_symex_fault_localizer.cpp @@ -15,7 +15,7 @@ goto_symex_fault_localizert::goto_symex_fault_localizert( const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, - decision_procedure_incrementalt &solver) + decision_procedure_assumptionst &solver) : options(options), ui_message_handler(ui_message_handler), equation(equation), diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h index a59fe0327e3..9142e568b19 100644 --- a/src/goto-checker/goto_symex_fault_localizer.h +++ b/src/goto-checker/goto_symex_fault_localizer.h @@ -18,7 +18,7 @@ Author: Peter Schrammel #include -#include +#include #include "fault_localization_provider.h" @@ -29,7 +29,7 @@ class goto_symex_fault_localizert const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, - decision_procedure_incrementalt &solver); + decision_procedure_assumptionst &solver); fault_location_infot operator()(const irep_idt &failed_property_id); @@ -37,7 +37,7 @@ class goto_symex_fault_localizert const optionst &options; ui_message_handlert &ui_message_handler; const symex_target_equationt &equation; - decision_procedure_incrementalt &solver; + decision_procedure_assumptionst &solver; /// A localization point is a goto instruction that is potentially at fault typedef std::map diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index 3e6ad49abff..ea9da5218e1 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, Peter Schrammel #include "goto_symex_property_decider.h" +#include + goto_symex_property_decidert::goto_symex_property_decidert( const optionst &options, ui_message_handlert &ui_message_handler, @@ -108,10 +110,9 @@ decision_proceduret::resultt goto_symex_property_decidert::solve() return (*decision_procedure)(); } -decision_procedure_incrementalt & -goto_symex_property_decidert::get_solver() const +const solver_factoryt::solvert &goto_symex_property_decidert::get_solver() const { - return *decision_procedure; + return *solver; } symex_target_equationt &goto_symex_property_decidert::get_equation() const diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 2bbbd9fe1ce..7ae5176b5b3 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -49,7 +49,7 @@ class goto_symex_property_decidert decision_proceduret::resultt solve(); /// Returns the solver instance - decision_procedure_incrementalt &get_solver() const; + const solver_factoryt::solvert &get_solver() 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 8ec7a52adfd..c6eada2d968 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -73,7 +73,8 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties) properties, equation, property_decider, ui_message_handler); if(options.get_bool_option("localize-faults")) - freeze_guards(equation, property_decider.get_solver()); + freeze_guards( + equation, property_decider.get_solver().decision_procedure_incremental()); return solver_runtime; } @@ -93,7 +94,7 @@ goto_tracet multi_path_symex_checkert::build_full_trace() const build_goto_trace( equation, equation.SSA_steps.end(), - property_decider.get_solver(), + property_decider.get_solver().decision_procedure(), ns, goto_trace); @@ -106,11 +107,17 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(property_decider.get_solver()), equation); + dynamic_cast( + property_decider.get_solver().decision_procedure()), + equation); } goto_tracet goto_trace; - build_goto_trace(equation, property_decider.get_solver(), ns, goto_trace); + build_goto_trace( + equation, + property_decider.get_solver().decision_procedure(), + ns, + goto_trace); return goto_trace; } @@ -122,7 +129,7 @@ multi_path_symex_checkert::build_trace(const irep_idt &property_id) const build_goto_trace( equation, ssa_step_matches_failing_property(property_id), - property_decider.get_solver(), + property_decider.get_solver().decision_procedure(), ns, goto_trace); @@ -149,7 +156,10 @@ fault_location_infot multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const { goto_symex_fault_localizert fault_localizer( - options, ui_message_handler, equation, property_decider.get_solver()); + options, + ui_message_handler, + equation, + property_decider.get_solver().decision_procedure_assumptions()); return fault_localizer(property_id); } diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index aa97d1d2084..e0f79a0bfdf 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -122,7 +122,7 @@ goto_tracet single_path_symex_checkert::build_full_trace() const build_goto_trace( property_decider->get_equation(), property_decider->get_equation().SSA_steps.end(), - property_decider->get_solver(), + property_decider->get_solver().decision_procedure(), ns, goto_trace); @@ -135,14 +135,15 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const { // NOLINTNEXTLINE(whitespace/braces) counterexample_beautificationt{ui_message_handler}( - dynamic_cast(property_decider->get_solver()), + dynamic_cast( + property_decider->get_solver().decision_procedure()), property_decider->get_equation()); } goto_tracet goto_trace; build_goto_trace( property_decider->get_equation(), - property_decider->get_solver(), + property_decider->get_solver().decision_procedure(), ns, goto_trace); @@ -156,7 +157,7 @@ single_path_symex_checkert::build_trace(const irep_idt &property_id) const build_goto_trace( property_decider->get_equation(), ssa_step_matches_failing_property(property_id), - property_decider->get_solver(), + property_decider->get_solver().decision_procedure(), ns, goto_trace); diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 9674200e3ce..e681d0d34fc 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -80,6 +80,18 @@ solver_factoryt::solvert::decision_procedure_incremental() const return *solver; } +decision_procedure_assumptionst & +solver_factoryt::solvert::decision_procedure_assumptions() const +{ + PRECONDITION(decision_procedure_ptr != nullptr); + decision_procedure_assumptionst *solver = + dynamic_cast(&*decision_procedure_ptr); + INVARIANT( + solver != nullptr, + "incremental decision procedure with solving under assumptions required"); + return *solver; +} + propt &solver_factoryt::solvert::prop() const { PRECONDITION(prop_ptr != nullptr); diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index cd6954eff68..b7a1e645ec8 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -14,13 +14,15 @@ Author: Daniel Kroening, Peter Schrammel #include +#include +#include #include class message_handlert; class namespacet; class optionst; -class propt; -class decision_proceduret; +class decision_procedure_incrementalt; +class decision_procedure_assumptionst; class solver_factoryt { @@ -46,6 +48,7 @@ class solver_factoryt decision_proceduret &decision_procedure() const; decision_procedure_incrementalt &decision_procedure_incremental() const; + decision_procedure_assumptionst &decision_procedure_assumptions() const; propt &prop() const; void set_decision_procedure(std::unique_ptr p); diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 9e3b78dfcf5..f54ca46511b 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cover_goals.h" #include +#include #include "decision_procedure_incremental.h" #include "literal_expr.h" diff --git a/src/solvers/prop/decision_procedure_assumptions.h b/src/solvers/prop/decision_procedure_assumptions.h new file mode 100644 index 00000000000..4a29ec95d39 --- /dev/null +++ b/src/solvers/prop/decision_procedure_assumptions.h @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: Decision procedure with incremental solving under assumptions + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Decision procedure with incremental solving under assumptions + +#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H +#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H + +#include "decision_procedure_incremental.h" + +class decision_procedure_assumptionst : public decision_procedure_incrementalt +{ +public: + /// Set assumptions for the next call to operator() to solve the problem + virtual void set_assumptions(const bvt &) = 0; + + /// Returns true if an assumption is in the final conflict + virtual bool is_in_conflict(literalt l) const = 0; + + virtual ~decision_procedure_assumptionst() = default; +}; + +#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H diff --git a/src/solvers/prop/decision_procedure_incremental.cpp b/src/solvers/prop/decision_procedure_incremental.cpp index 5f2f4c57b13..0b8253b0504 100644 --- a/src/solvers/prop/decision_procedure_incremental.cpp +++ b/src/solvers/prop/decision_procedure_incremental.cpp @@ -1,30 +1,12 @@ /*******************************************************************\ -Module: +Module: Decision procedure with incremental solving Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "decision_procedure_incremental.h" -#include - -/// determine whether a variable is in the final conflict -bool decision_procedure_incrementalt::is_in_conflict(literalt) const -{ - UNREACHABLE; - return false; -} - -void decision_procedure_incrementalt::set_assumptions(const bvt &) -{ - UNREACHABLE; -} - -void decision_procedure_incrementalt::set_frozen(const literalt) -{ - UNREACHABLE; -} void decision_procedure_incrementalt::set_frozen(const bvt &bv) { diff --git a/src/solvers/prop/decision_procedure_incremental.h b/src/solvers/prop/decision_procedure_incremental.h index a500d7c3fc2..634ef5b4ad5 100644 --- a/src/solvers/prop/decision_procedure_incremental.h +++ b/src/solvers/prop/decision_procedure_incremental.h @@ -1,61 +1,36 @@ /*******************************************************************\ -Module: +Module: Decision procedure with incremental solving Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +/// \file +/// Decision procedure with incremental solving + #ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H #define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H -#include -#include - -#include -#include -#include - #include "decision_procedure.h" #include "literal.h" -#include "literal_expr.h" -#include "prop.h" - -// API that provides a "handle" in the form of a literalt -// for expressions. class decision_procedure_incrementalt : public decision_proceduret { public: - virtual ~decision_procedure_incrementalt() - { - } - - using decision_proceduret::operator(); - - // incremental solving - virtual void set_frozen(literalt a); - virtual void set_frozen(const bvt &); - virtual void set_assumptions(const bvt &_assumptions); - virtual bool has_set_assumptions() const - { - return false; - } - virtual void set_all_frozen() - { - } - - // returns true if an assumption is in the final conflict - virtual bool is_in_conflict(literalt l) const; - virtual bool has_is_in_conflict() const - { - return false; - } -}; + /// Prevent the solver-level variable associated with literal \p a from being + /// optimized away by the decision procedure + virtual void set_frozen(literalt a) = 0; + + /// Prevent the solver-level variables in the given bitvector \p bv from being + /// optimized away by the decision procedure + virtual void set_frozen(const bvt &bv); -// -// an instance of the above that converts the -// propositional skeleton by passing it to a propt -// + /// Prevent all solver-level variables encoding symbols occurring in the + /// expressions passed to the decision procedure from being optimized away + virtual void set_all_frozen() = 0; + + virtual ~decision_procedure_incrementalt() = default; +}; #endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index c46a7f40c4a..607674962a2 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -16,13 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "decision_procedure_incremental.h" +#include "decision_procedure_assumptions.h" #include "literal.h" #include "literal_expr.h" #include "prop.h" #include "solver_resource_limits.h" -class prop_conv_solvert : public decision_procedure_incrementalt, +class prop_conv_solvert : public decision_procedure_assumptionst, public solver_resource_limitst { public: @@ -57,10 +57,6 @@ class prop_conv_solvert : public decision_procedure_incrementalt, { prop.set_assumptions(_assumptions); } - bool has_set_assumptions() const override - { - return prop.has_set_assumptions(); - } void set_all_frozen() override { freeze_all = true; @@ -70,10 +66,6 @@ class prop_conv_solvert : public decision_procedure_incrementalt, { return prop.is_in_conflict(l); } - bool has_is_in_conflict() const override - { - return prop.has_is_in_conflict(); - } // get literal for expression, if available bool literal(const symbol_exprt &expr, literalt &literal) const; diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp index a40e4ce0446..90302be384a 100644 --- a/src/solvers/prop/prop_minimize.cpp +++ b/src/solvers/prop/prop_minimize.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "literal_expr.h" prop_minimizet::prop_minimizet( - decision_procedure_incrementalt &_decision_procedure, + decision_procedure_assumptionst &_decision_procedure, message_handlert &message_handler) : decision_procedure(_decision_procedure), log(message_handler) { @@ -96,9 +96,6 @@ literalt prop_minimizet::constraint() /// Try to cover all objectives void prop_minimizet::operator()() { - // we need to use assumptions - PRECONDITION(decision_procedure.has_set_assumptions()); - _iterations = 0; _number_satisfied = 0; _value = 0; diff --git a/src/solvers/prop/prop_minimize.h b/src/solvers/prop/prop_minimize.h index 5336d465174..36e3208090f 100644 --- a/src/solvers/prop/prop_minimize.h +++ b/src/solvers/prop/prop_minimize.h @@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "decision_procedure_incremental.h" +#include "decision_procedure_assumptions.h" /// Computes a satisfying assignment of minimal cost according to a const /// function using incremental SAT class prop_minimizet { public: - prop_minimizet(decision_procedure_incrementalt &, message_handlert &); + prop_minimizet(decision_procedure_assumptionst &, message_handlert &); void operator()(); @@ -71,7 +71,7 @@ class prop_minimizet std::size_t _number_satisfied = 0; std::size_t _number_objectives = 0; weightt _value = 0; - decision_procedure_incrementalt &decision_procedure; + decision_procedure_assumptionst &decision_procedure; messaget log; literalt constraint(); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2a085fc9891..b183f462606 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include // Mark different kinds of error conditions @@ -64,6 +65,23 @@ tvt smt2_convt::l_get(literalt l) const return tvt(boolean_assignment[l.var_no()]^l.sign()); } +void smt2_convt::set_frozen(literalt) +{ + // not needed +} + +void smt2_convt::set_all_frozen() +{ + // not needed +} + +bool smt2_convt::is_in_conflict(literalt l) const +{ + // we cannot do that + UNREACHABLE; + return false; +} + void smt2_convt::write_header() { out << "; SMT 2" << "\n"; diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 94dfc136388..36121ca4ff5 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "letify.h" @@ -31,7 +31,7 @@ class constant_exprt; class index_exprt; class member_exprt; -class smt2_convt : public decision_procedure_incrementalt +class smt2_convt : public decision_procedure_assumptionst { public: enum class solvert @@ -114,9 +114,9 @@ class smt2_convt : public decision_procedure_incrementalt bool emit_set_logic; literalt convert(const exprt &expr) override; - void set_frozen(literalt) override - { /* not needed */ - } + void set_frozen(literalt) override; + void set_all_frozen() override; + bool is_in_conflict(literalt l) const override; void set_to(const exprt &expr, bool value) override; exprt get(const exprt &expr) const override; std::string decision_procedure_text() const override diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index 4b77769cb47..355f9dfa622 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "smt2_conv.h" class smt2_stringstreamt @@ -40,12 +42,6 @@ class smt2_dect : protected smt2_stringstreamt, resultt dec_solve() override; std::string decision_procedure_text() const override; - // yes, we are incremental! - bool has_set_assumptions() const override - { - return true; - } - protected: resultt read_result(std::istream &in); }; From a17fb3696880178346e020a6dfa7104daff4e034 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 28 Mar 2019 17:28:46 +0000 Subject: [PATCH 4/8] Split out is_in_conflict solver capability This is only provided by the prop_conv_solvert-based hierarchy at the moment and is quite specific to MiniSAT-based solvers. The functionality itself is used out-of-tree only (2LS). --- .../prop/decision_procedure_assumptions.h | 3 -- src/solvers/prop/prop_conv_solver.h | 2 ++ src/solvers/prop/solver_conflicts.h | 28 +++++++++++++++++++ src/solvers/smt2/smt2_conv.cpp | 7 ----- src/solvers/smt2/smt2_conv.h | 1 - 5 files changed, 30 insertions(+), 11 deletions(-) create mode 100644 src/solvers/prop/solver_conflicts.h diff --git a/src/solvers/prop/decision_procedure_assumptions.h b/src/solvers/prop/decision_procedure_assumptions.h index 4a29ec95d39..7e644747ca9 100644 --- a/src/solvers/prop/decision_procedure_assumptions.h +++ b/src/solvers/prop/decision_procedure_assumptions.h @@ -20,9 +20,6 @@ class decision_procedure_assumptionst : public decision_procedure_incrementalt /// Set assumptions for the next call to operator() to solve the problem virtual void set_assumptions(const bvt &) = 0; - /// Returns true if an assumption is in the final conflict - virtual bool is_in_conflict(literalt l) const = 0; - virtual ~decision_procedure_assumptionst() = default; }; diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index 607674962a2..6be1b34ba2f 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -20,9 +20,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "literal.h" #include "literal_expr.h" #include "prop.h" +#include "solver_conflicts.h" #include "solver_resource_limits.h" class prop_conv_solvert : public decision_procedure_assumptionst, + public solver_conflictst, public solver_resource_limitst { public: diff --git a/src/solvers/prop/solver_conflicts.h b/src/solvers/prop/solver_conflicts.h new file mode 100644 index 00000000000..1cbbd64f714 --- /dev/null +++ b/src/solvers/prop/solver_conflicts.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Capability to return assumptions that are in a conflict + when solving under assumptions + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Capability to return assumptions that are in a conflict +// when solving under assumptions + +#ifndef CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H +#define CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H + +class literalt; + +class solver_conflictst +{ +public: + /// Returns true if an assumption is in the final conflict + virtual bool is_in_conflict(literalt) const = 0; + + virtual ~solver_conflictst() = default; +}; + +#endif // CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index b183f462606..7b8da582831 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -75,13 +75,6 @@ void smt2_convt::set_all_frozen() // not needed } -bool smt2_convt::is_in_conflict(literalt l) const -{ - // we cannot do that - UNREACHABLE; - return false; -} - void smt2_convt::write_header() { out << "; SMT 2" << "\n"; diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 36121ca4ff5..9d489c660eb 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -116,7 +116,6 @@ class smt2_convt : public decision_procedure_assumptionst literalt convert(const exprt &expr) override; void set_frozen(literalt) override; void set_all_frozen() override; - bool is_in_conflict(literalt l) const override; void set_to(const exprt &expr, bool value) override; exprt get(const exprt &expr) const override; std::string decision_procedure_text() const override From 30b635310ce8efb79965712699c671f3d4122421 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 28 Mar 2019 11:27:10 +0000 Subject: [PATCH 5/8] Decision procedure interface for incremental solving with contexts Provides push/pop interface --- .../prop/decision_procedure_contexts.h | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 src/solvers/prop/decision_procedure_contexts.h diff --git a/src/solvers/prop/decision_procedure_contexts.h b/src/solvers/prop/decision_procedure_contexts.h new file mode 100644 index 00000000000..32da3079dad --- /dev/null +++ b/src/solvers/prop/decision_procedure_contexts.h @@ -0,0 +1,30 @@ +/*******************************************************************\ + +Module: Decision procedure with incremental solving with contexts + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Decision procedure with incremental solving with contexts + +#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_CONTEXTS_H +#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_CONTEXTS_H + +#include "decision_procedure_assumptions.h" + +class decision_procedure_contextst : public decision_procedure_assumptionst +{ +public: + /// Push a new context on the stack + /// This context becomes a child context nested in the current context. + virtual void push_context() = 0; + + /// Pop the current context + virtual void pop_context() = 0; + + virtual ~decision_procedure_contextst() = default; +}; + +#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_CONTEXTS_H From bd5970ce642fea004acd15d1a5a421ecaa523efe Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 28 Mar 2019 22:40:25 +0000 Subject: [PATCH 6/8] Allow getting context-based incremental solver Puts the type check into a single place --- src/goto-checker/solver_factory.cpp | 13 +++++++++++++ src/goto-checker/solver_factory.h | 2 ++ 2 files changed, 15 insertions(+) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index e681d0d34fc..1f68e9c2673 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -25,6 +25,8 @@ Author: Daniel Kroening, Peter Schrammel #endif #include +#include +#include #include #include #include @@ -92,6 +94,17 @@ solver_factoryt::solvert::decision_procedure_assumptions() const return *solver; } +decision_procedure_contextst & +solver_factoryt::solvert::decision_procedure_contexts() const +{ + PRECONDITION(decision_procedure_ptr != nullptr); + decision_procedure_contextst *solver = + dynamic_cast(&*decision_procedure_ptr); + INVARIANT( + solver != nullptr, "incremental decision procedure with contexts required"); + return *solver; +} + propt &solver_factoryt::solvert::prop() const { PRECONDITION(prop_ptr != nullptr); diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index b7a1e645ec8..7e7f60068c7 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -21,6 +21,7 @@ Author: Daniel Kroening, Peter Schrammel class message_handlert; class namespacet; class optionst; +class decision_procedure_contextst; class decision_procedure_incrementalt; class decision_procedure_assumptionst; @@ -49,6 +50,7 @@ class solver_factoryt decision_proceduret &decision_procedure() const; decision_procedure_incrementalt &decision_procedure_incremental() const; decision_procedure_assumptionst &decision_procedure_assumptions() const; + decision_procedure_contextst &decision_procedure_contexts() const; propt &prop() const; void set_decision_procedure(std::unique_ptr p); From ac5813189caf20434062b18523e717adf5e909c5 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 28 Mar 2019 23:03:17 +0000 Subject: [PATCH 7/8] Implement context-based solver on top of prop_conv_solvert Also allows using raw assumptions within contexts (as required by minimization and refinement algorithms). --- src/solvers/prop/prop_conv_solver.cpp | 60 ++++++++++++++++++++++++--- src/solvers/prop/prop_conv_solver.h | 40 ++++++++++++++---- 2 files changed, 86 insertions(+), 14 deletions(-) diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 7b43be7a016..b1e41d5d38f 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -331,7 +331,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr) return true; } -void prop_conv_solvert::set_to(const exprt &expr, bool value) +void prop_conv_solvert::do_set_to(const exprt &expr, bool value) { PRECONDITION(expr.type().id() == ID_bool); @@ -346,7 +346,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value) { if(expr.operands().size() == 1) { - set_to(expr.op0(), !value); + do_set_to(expr.op0(), !value); return; } } @@ -359,7 +359,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value) if(expr.id() == ID_and) { forall_operands(it, expr) - set_to_true(*it); + do_set_to(*it, true); return; } @@ -403,14 +403,14 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value) { const implies_exprt &implies_expr = to_implies_expr(expr); - set_to_true(implies_expr.op0()); - set_to_false(implies_expr.op1()); + do_set_to(implies_expr.op0(), true); + do_set_to(implies_expr.op1(), false); return; } else if(expr.id() == ID_or) // !(a || b) == (!a && !b) { forall_operands(it, expr) - set_to_false(*it); + do_set_to(*it, false); return; } } @@ -493,3 +493,51 @@ std::size_t prop_conv_solvert::get_number_of_solver_calls() const { return prop.get_number_of_solver_calls(); } + +const char *prop_conv_solvert::context_prefix = "prop_conv::context$"; + +void prop_conv_solvert::set_to(const exprt &expr, bool value) +{ + if(context_literals.empty()) + { + // We are in the root context. + do_set_to(expr, value); + } + else + { + // We have a child context. We add context_literal ==> expr to the formula. + do_set_to(or_exprt(literal_exprt(!context_literals.back()), expr), value); + } +} + +void prop_conv_solvert::set_assumptions(const bvt &assumptions) +{ + bvt combined_assumptions; + combined_assumptions.reserve(context_literals.size() + assumptions.size()); + combined_assumptions.insert( + combined_assumptions.end(), + context_literals.begin(), + context_literals.end()); + combined_assumptions.insert( + combined_assumptions.end(), assumptions.begin(), assumptions.end()); + prop.set_assumptions(combined_assumptions); +} + +void prop_conv_solvert::push_context() +{ + // We create a new context literal. + literalt context_literal = prop_conv_solvert::convert(symbol_exprt( + context_prefix + std::to_string(context_literal_counter++), bool_typet())); + + context_literals.push_back(context_literal); + prop.set_assumptions(context_literals); +} + +void prop_conv_solvert::pop_context() +{ + PRECONDITION(!context_literals.empty()); + + // We remove the last context literal from the stack. + context_literals.pop_back(); + prop.set_assumptions(context_literals); +} diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index 6be1b34ba2f..f54e0944471 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "decision_procedure_assumptions.h" +#include "decision_procedure_contexts.h" #include "literal.h" #include "literal_expr.h" #include "prop.h" #include "solver_conflicts.h" #include "solver_resource_limits.h" -class prop_conv_solvert : public decision_procedure_assumptionst, +class prop_conv_solvert : public decision_procedure_contextst, public solver_conflictst, public solver_resource_limitst { @@ -36,7 +36,6 @@ class prop_conv_solvert : public decision_procedure_assumptionst, virtual ~prop_conv_solvert() = default; // overloading from decision_proceduret - void set_to(const exprt &expr, bool value) override; decision_proceduret::resultt dec_solve() override; void print_assignment(std::ostream &out) const override; std::string decision_procedure_text() const override @@ -55,10 +54,7 @@ class prop_conv_solvert : public decision_procedure_assumptionst, { prop.set_frozen(a); } - void set_assumptions(const bvt &_assumptions) override - { - prop.set_assumptions(_assumptions); - } + void set_all_frozen() override { freeze_all = true; @@ -69,6 +65,26 @@ class prop_conv_solvert : public decision_procedure_assumptionst, return prop.is_in_conflict(l); } + /// For a Boolean expression \p expr, add the constraint + /// 'current_context => expr' if \p value is `true`, + /// otherwise add 'current_context => not expr' + void set_to(const exprt &expr, bool value) override; + + /// Set \p assumptions within current context. + /// These assumptions can be removed by passing empty \p assumptions. + /// These assumptions will also be dropped in the course of any context + /// operation (`push_context` or `pop_context`). + void set_assumptions(const bvt &assumptions) override; + + /// Push a new context on the stack + /// This context becomes a child context nested in the current context. + void push_context() override; + + /// Pop the current context + void pop_context() override; + + static const char *context_prefix; + // get literal for expression, if available bool literal(const symbol_exprt &expr, literalt &literal) const; @@ -123,10 +139,18 @@ class prop_conv_solvert : public decision_procedure_assumptionst, virtual void ignoring(const exprt &expr); - // deliberately protected now to protect lower-level API + /// Actually adds the constraints to `prop` + void do_set_to(const exprt &expr, bool value); + propt ∝ messaget log; + + /// Context literals used as assumptions + bvt context_literals; + + /// Unique context literal names + std::size_t context_literal_counter = 0; }; #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H From 9e504659bbc76aa2b0903c0b4e89bb962b3b9953 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 29 Mar 2019 10:09:37 +0000 Subject: [PATCH 8/8] Make bv_refinementt compatible with contexts Must not bypass prop_conv_solvert::set_assumptions by calling prop directly. --- src/solvers/refinement/bv_refinement_loop.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 474b56b0f86..c955e2eb82c 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -101,9 +101,9 @@ decision_proceduret::resultt bv_refinementt::prop_solve() approximation.under_assumptions.end()); } - prop.set_assumptions(assumptions); + bv_pointerst::set_assumptions(assumptions); propt::resultt result=prop.prop_solve(); - prop.set_assumptions(parent_assumptions); + bv_pointerst::set_assumptions(parent_assumptions); switch(result) { @@ -136,5 +136,5 @@ void bv_refinementt::check_UNSAT() void bv_refinementt::set_assumptions(const bvt &_assumptions) { parent_assumptions=_assumptions; - prop.set_assumptions(_assumptions); + bv_pointerst::set_assumptions(_assumptions); }