Merge pull request #6551 from diffblue/rename_postprocessing

rename post_process to finish_eager_conversion

Author: kroening

src/solvers/flattening/arrays.h

@@ -38,10 +38,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();
   }
@@ -57,7 +57,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();
   }

src/solvers/flattening/boolbv.h

@@ -73,11 +73,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 };
@@ -267,7 +267,7 @@ class boolbvt:public arrayst
   typedef std::list<quantifiert> quantifier_listt;
   quantifier_listt quantifier_list;
 
-  void post_process_quantifiers();
+  void finish_eager_conversion_quantifiers();
 
   typedef std::vector<std::size_t> offset_mapt;
   offset_mapt build_offset_map(const struct_typet &src);

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;

src/solvers/flattening/bv_pointers.cpp

@@ -977,10 +977,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();

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
   {

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);
 };

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();
   }

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();

src/solvers/prop/prop_conv_solver.h

@@ -36,6 +36,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;
@@ -102,8 +105,6 @@ class prop_conv_solvert : public conflict_providert,
   }
 
 protected:
-  virtual void post_process();
-
   bool post_processing_done = false;
 
   /// Get a _boolean_ value from the model if the formula is satisfiable.

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;

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;
 

src/solvers/refinement/refine_arrays.cpp

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/sat/satcheck.h>
 
 /// 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