diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index a7ee9096269..2eb32f9b840 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -36,10 +36,10 @@ class arrayst:public equalityt message_handlert &message_handler, bool get_array_constraints = false); - void post_process() override + void finish_eager_conversion() override { - post_process_arrays(); - SUB::post_process(); + finish_eager_conversion_arrays(); + SUB::finish_eager_conversion(); if(get_array_constraints) display_array_constraint_count(); } @@ -55,7 +55,7 @@ class arrayst:public equalityt messaget log; message_handlert &message_handler; - virtual void post_process_arrays() + virtual void finish_eager_conversion_arrays() { add_array_constraints(); } diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 58b84da58ee..9a4bc6b3d33 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -72,11 +72,11 @@ class boolbvt:public arrayst bv_cache.clear(); } - void post_process() override + void finish_eager_conversion() override { - post_process_quantifiers(); - functions.post_process(); - SUB::post_process(); + finish_eager_conversion_quantifiers(); + functions.finish_eager_conversion(); + SUB::finish_eager_conversion(); } enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO }; @@ -266,7 +266,7 @@ class boolbvt:public arrayst typedef std::list quantifier_listt; quantifier_listt quantifier_list; - void post_process_quantifiers(); + void finish_eager_conversion_quantifiers(); typedef std::vector offset_mapt; offset_mapt build_offset_map(const struct_typet &src); diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 7283c86c208..fb5e201aa3e 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -271,7 +271,7 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src) return quantifier_list.back().l; } -void boolbvt::post_process_quantifiers() +void boolbvt::finish_eager_conversion_quantifiers() { if(quantifier_list.empty()) return; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index cd0235eba75..b45767f5bd2 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -976,10 +976,10 @@ void bv_pointerst::do_postponed( UNREACHABLE; } -void bv_pointerst::post_process() +void bv_pointerst::finish_eager_conversion() { // post-processing arrays may yield further objects, do this first - SUB::post_process(); + SUB::finish_eager_conversion(); for(postponed_listt::const_iterator it=postponed_list.begin(); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 2867340707f..6c389683e7b 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -24,7 +24,7 @@ class bv_pointerst:public boolbvt message_handlert &message_handler, bool get_array_constraints = false); - void post_process() override; + void finish_eager_conversion() override; std::size_t boolbv_width(const typet &type) const override { diff --git a/src/solvers/flattening/equality.h b/src/solvers/flattening/equality.h index 6d6b8d76f7e..d8f41158111 100644 --- a/src/solvers/flattening/equality.h +++ b/src/solvers/flattening/equality.h @@ -26,10 +26,12 @@ class equalityt:public prop_conv_solvert virtual literalt equality(const exprt &e1, const exprt &e2); - void post_process() override + using SUB = prop_conv_solvert; + + void finish_eager_conversion() override { add_equality_constraints(); - prop_conv_solvert::post_process(); + SUB::finish_eager_conversion(); typemap.clear(); // if called incrementally, don't do it twice } @@ -50,6 +52,8 @@ class equalityt:public prop_conv_solvert typemapt typemap; virtual literalt equality2(const exprt &e1, const exprt &e2); + + // an eager conversion of the transitivity constraints virtual void add_equality_constraints(); virtual void add_equality_constraints(const typestructt &typestruct); }; diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h index e8a77781e9b..1ee2e373767 100644 --- a/src/solvers/lowering/functions.h +++ b/src/solvers/lowering/functions.h @@ -33,7 +33,7 @@ class functionst void record(const function_application_exprt &function_application); - virtual void post_process() + virtual void finish_eager_conversion() { add_function_constraints(); } diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index f9bcb0bd4de..432140f8ad0 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -429,7 +429,7 @@ void prop_conv_solvert::ignoring(const exprt &expr) log.warning() << "warning: ignoring " << expr.pretty() << messaget::eom; } -void prop_conv_solvert::post_process() +void prop_conv_solvert::finish_eager_conversion() { } @@ -441,7 +441,7 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve() const auto post_process_start = std::chrono::steady_clock::now(); log.statistics() << "Post-processing" << messaget::eom; - post_process(); + finish_eager_conversion(); post_processing_done = true; const auto post_process_stop = std::chrono::steady_clock::now(); diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index 995ec6cdad7..e69756b2b98 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -35,6 +35,9 @@ class prop_conv_solvert : public conflict_providert, virtual ~prop_conv_solvert() = default; + // non-iterative eager conversion + virtual void finish_eager_conversion(); + // overloading from decision_proceduret decision_proceduret::resultt dec_solve() override; void print_assignment(std::ostream &out) const override; @@ -99,8 +102,6 @@ class prop_conv_solvert : public conflict_providert, void enable_hardness_collection() override; protected: - virtual void post_process(); - bool post_processing_done = false; /// Get a _boolean_ value from the model if the formula is satisfiable. diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 67ccd29e757..0f9b3506918 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -49,7 +49,7 @@ class bv_refinementt:public bv_pointerst protected: // Refine array - void post_process_arrays() override; + void finish_eager_conversion_arrays() override; // Refine arithmetic bvt convert_mult(const mult_exprt &expr) override; diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 21542ba26d5..6db58bf898b 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -25,7 +25,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve() { // do the usual post-processing log.status() << "BV-Refinement: post-processing" << messaget::eom; - post_process(); + finish_eager_conversion(); log.debug() << "Solving with " << prop.solver_text() << messaget::eom; diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 0f86c0e05b6..da4235f3c9f 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include /// generate array constraints -void bv_refinementt::post_process_arrays() +void bv_refinementt::finish_eager_conversion_arrays() { collect_indices(); // at this point all indices should in the index set