Change uit configuration to xml-specific Boolean choice

Author: tautschnig

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -152,8 +152,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=&sat_check;
-  const auto ui=ui_message_handlert::uit::PLAIN;
-  info.ui=ui;
+  info.output_xml = false;
   bv_refinementt solver(info);
   solver << expr;
   return solver();

src/cbmc/cbmc_solvers.cpp

@@ -118,7 +118,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=prop.get();
-  info.ui=ui;
+  info.output_xml = ui == ui_message_handlert::uit::XML_UI;
 
   // we allow setting some parameters
   if(options.get_bool_option("max-node-refinement"))
@@ -144,7 +144,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   prop->set_message_handler(get_message_handler());
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
-  info.ui=ui;
+  info.output_xml = ui == ui_message_handlert::uit::XML_UI;
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=
       options.get_unsigned_int_option("max-node-refinement");

src/solvers/refinement/bv_refinement.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 
-#include <util/ui_message.h>
-
 #include <solvers/flattening/bv_pointers.h>
 
 #define MAX_STATE 10000
@@ -23,7 +21,7 @@ class bv_refinementt:public bv_pointerst
 private:
   struct configt
   {
-    ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
+    bool output_xml = false;
     /// Max number of times we refine a formula node
     unsigned max_node_refinement=5;
     /// Enable array refinement

src/solvers/refinement/bv_refinement_loop.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "bv_refinement.h"
 
-#include <iostream>
-
 #include <util/xml.h>
 
 bv_refinementt::bv_refinementt(const infot &info):
@@ -41,7 +39,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
     status() << "BV-Refinement: iteration " << iteration << eom;
 
     // output the very same information in a structured fashion
-    if(config_.ui==ui_message_handlert::uit::XML_UI)
+    if(config_.output_xml)
     {
       xmlt xml("refinement-iteration");
       xml.data=std::to_string(iteration);

src/solvers/refinement/string_refinement_util.h

@@ -9,6 +9,8 @@
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
 
+#include <memory>
+
 #include "string_builtin_function.h"
 #include "string_constraint.h"
 #include "string_constraint_generator.h"