Merge pull request #3578 from peterschrammel/split-witness-output

Split witness output functions into proof and refutation [depends: 3565]

Author: peterschrammel

src/cbmc/bmc.cpp

@@ -152,7 +152,7 @@ safety_checkert::resultt bmct::execute(
       if(options.is_set("paths"))
         return safety_checkert::resultt::PAUSED;
       report_success(ui_message_handler);
-      output_graphml(resultt::SAFE, error_trace, equation, ns, options);
+      output_graphml(equation, ns, options);
       return safety_checkert::resultt::SAFE;
     }
 
@@ -219,7 +219,7 @@ safety_checkert::resultt bmct::stop_on_fail()
   {
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     report_success(ui_message_handler);
-    output_graphml(resultt::SAFE, error_trace, equation, ns, options);
+    output_graphml(equation, ns, options);
     return resultt::SAFE;
 
   case decision_proceduret::resultt::D_SATISFIABLE:
@@ -232,7 +232,7 @@ safety_checkert::resultt bmct::stop_on_fail()
       build_error_trace(
         error_trace, ns, equation, prop_conv, ui_message_handler);
       output_error_trace(error_trace, ns, trace_options(), ui_message_handler);
-      output_graphml(resultt::UNSAFE, error_trace, equation, ns, options);
+      output_graphml(error_trace, ns, options);
     }
 
     report_failure(ui_message_handler);

src/goto-checker/bmc_util.cpp

@@ -87,11 +87,9 @@ void output_error_trace(
   }
 }
 
-/// outputs witnesses in graphml format
+/// outputs an error witness in graphml format
 void output_graphml(
-  safety_checkert::resultt result,
   const goto_tracet &goto_trace,
-  const symex_target_equationt &symex_target_equation,
   const namespacet &ns,
   const optionst &options)
 {
@@ -100,13 +98,30 @@ void output_graphml(
     return;
 
   graphml_witnesst graphml_witness(ns);
-  if(result == safety_checkert::resultt::UNSAFE)
-    graphml_witness(goto_trace);
-  else if(result == safety_checkert::resultt::SAFE)
-    graphml_witness(symex_target_equation);
+  graphml_witness(goto_trace);
+
+  if(graphml == "-")
+    write_graphml(graphml_witness.graph(), std::cout);
   else
+  {
+    std::ofstream out(graphml);
+    write_graphml(graphml_witness.graph(), out);
+  }
+}
+
+/// outputs a proof in graphml format
+void output_graphml(
+  const symex_target_equationt &symex_target_equation,
+  const namespacet &ns,
+  const optionst &options)
+{
+  const std::string graphml = options.get_option("graphml-witness");
+  if(graphml.empty())
     return;
 
+  graphml_witnesst graphml_witness(ns);
+  graphml_witness(symex_target_equation);
+
   if(graphml == "-")
     write_graphml(graphml_witness.graph(), std::cout);
   else

src/goto-checker/bmc_util.h

@@ -48,9 +48,8 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
+void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(
-  safety_checkert::resultt,
-  const goto_tracet &,
   const symex_target_equationt &,
   const namespacet &,
   const optionst &);