Merge pull request #1594 from diffblue/use-output_filet-ebmc_solvert

use `output_filet` in `ebmc_solvert`

Author: tautschnig

src/ebmc/ebmc_solver_factory.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "ebmc_solver_factory.h"
 
-#include <util/unicode.h>
-
 #include <solvers/flattening/boolbv.h>
 #include <solvers/prop/prop.h>
 #include <solvers/sat/satcheck.h>
@@ -34,19 +32,17 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
 
       return [filename](const namespacet &ns, message_handlert &message_handler)
       {
-        std::unique_ptr<std::ofstream> outfile_ptr{
-          new std::ofstream(widen_if_needed(filename))};
-
-        if(!*outfile_ptr)
-          throw ebmc_errort() << "Failed to open `" << filename << "'";
+        std::unique_ptr<output_filet> output_file_ptr{
+          new output_filet{filename}};
 
         messaget message(message_handler);
-        message.status() << "Writing formula to `" << filename << "'"
-                         << messaget::eom;
+        message.status() << "Writing formula to `" << output_file_ptr->name()
+                         << "'" << messaget::eom;
 
-        auto dec = std::make_unique<show_formula_solvert>(*outfile_ptr);
+        auto dec =
+          std::make_unique<show_formula_solvert>(output_file_ptr->stream());
 
-        return ebmc_solvert{std::move(outfile_ptr), std::move(dec)};
+        return ebmc_solvert{std::move(output_file_ptr), std::move(dec)};
       };
     }
     else
@@ -79,25 +75,22 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
       return [filename, smt2_solver](
                const namespacet &ns, message_handlert &message_handler)
       {
-        std::unique_ptr<std::ofstream> outfile_ptr{
-          new std::ofstream(widen_if_needed(filename))};
-
-        if(!*outfile_ptr)
-          throw ebmc_errort() << "Failed to open `" << filename << "'";
+        std::unique_ptr<output_filet> output_file_ptr{
+          new output_filet{filename}};
 
         messaget message(message_handler);
-        message.status() << "Writing SMT2 formula to `" << filename << "'"
-                         << messaget::eom;
+        message.status() << "Writing SMT2 formula to `"
+                         << output_file_ptr->name() << "'" << messaget::eom;
 
         auto dec = std::make_unique<smt2_convt>(
           ns,
           "ebmc",
           std::string("Generated by EBMC ") + EBMC_VERSION,
           "QF_AUFBV",
           smt2_solver.value(),
-          *outfile_ptr);
+          output_file_ptr->stream());
 
-        return ebmc_solvert{std::move(outfile_ptr), std::move(dec)};
+        return ebmc_solvert{std::move(output_file_ptr), std::move(dec)};
       };
     }
     else

src/ebmc/ebmc_solver_factory.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
+#include "output_file.h"
+
 #include <fstream>
 #include <memory>
 
@@ -35,9 +37,9 @@ class ebmc_solvert final
   }
 
   ebmc_solvert(
-    std::unique_ptr<std::ofstream> p1,
+    std::unique_ptr<output_filet> p1,
     std::unique_ptr<decision_proceduret> p2)
-    : ofstream_ptr(std::move(p1)), decision_procedure_ptr(std::move(p2))
+    : output_file_ptr(std::move(p1)), decision_procedure_ptr(std::move(p2))
   {
   }
 
@@ -48,7 +50,7 @@ class ebmc_solvert final
   }
 
   // the objects are deleted in the opposite order they appear below
-  std::unique_ptr<std::ofstream> ofstream_ptr;
+  std::unique_ptr<output_filet> output_file_ptr;
   std::unique_ptr<propt> prop_ptr;
   std::unique_ptr<decision_proceduret> decision_procedure_ptr;
 };