Merge pull request #7248 from diffblue/chc_verbose

CHC solver: redesigned verbose output

Author: kroening

src/cprover/axioms.cpp

@@ -74,8 +74,10 @@ void axiomst::evaluate_fc()
         operands_equal,
         equal_exprt(
           *a_it, typecast_exprt::conditional_cast(*b_it, a_it->type())));
+#if 0
       if(verbose)
         std::cout << "EVALUATE: " << format(implication) << '\n';
+#endif
       dest << replace(implication);
     }
   }
@@ -752,11 +754,13 @@ void axiomst::emit()
     constraint.visit_pre([this](const exprt &src) { node(src); });
 
     auto constraint_replaced = replace(constraint);
+#if 0
     if(verbose)
     {
       std::cout << "CONSTRAINT1: " << format(constraint) << "\n";
       std::cout << "CONSTRAINT2: " << format(constraint_replaced) << "\n";
     }
+#endif
     dest << constraint_replaced;
   }
 

src/cprover/counterexample_found.cpp

@@ -33,11 +33,13 @@ void show_assignment(const bv_pointers_widet &solver)
     if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not)
       continue;
     auto value = solver.l_get(entry.second);
+#  if 0
     std::cout << "|| " << format(expr) << " --> " << value << "\n";
+#  endif
   }
 #endif
 
-#if 1
+#if 0
   for(auto &entry : solver.get_map().get_mapping())
   {
     const auto &identifier = entry.first;
@@ -47,12 +49,14 @@ void show_assignment(const bv_pointers_widet &solver)
   }
 #endif
 
+#if 0
   for(auto &entry : solver.get_symbols())
   {
     const auto &identifier = entry.first;
     auto value = solver.l_get(entry.second);
     std::cout << "|| " << identifier << " --> " << value << "\n";
   }
+#endif
 }
 
 static exprt evaluator_rec(

src/cprover/propagate.cpp

@@ -14,9 +14,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/format_expr.h>
 #include <util/simplify_expr.h>
 
+#include "console.h"
 #include "simplify_state_expr.h"
 #include "state.h"
 
+#include <iomanip>
 #include <iostream>
 
 void propagate(
@@ -28,16 +30,17 @@ void propagate(
   const std::function<void(const symbol_exprt &, exprt, const workt::patht &)>
     &propagator)
 {
+  auto &f = frames[work.frame.index];
+
   if(verbose)
   {
-    std::cout << "PROP";
-    for(const auto &p : work.path)
-      std::cout << ' ' << p.index;
-    std::cout << ": " << format(work.invariant) << '\n';
+    std::cout << '\n';
+    std::cout << consolet::faint;
+    std::cout << ' ' << std::setw(2) << work.frame.index << ' ';
+    std::cout << consolet::reset << consolet::cyan << format(work.invariant);
+    std::cout << consolet::reset << '\n';
   }
 
-  auto &f = frames[work.frame.index];
-
   for(const auto &implication : f.implications)
   {
     auto &next_state = implication.rhs.arguments().front();
@@ -52,6 +55,7 @@ void propagate(
       std::cout << "SIMPa: " << format(simplified1a) << "\n";
       abort();
     }
+
     auto simplified2 = simplify_expr(simplified1, ns);
 
     if(implication.lhs.id() == ID_function_application)
@@ -69,8 +73,9 @@ void propagate(
       auto &function_application =
         to_function_application_expr(to_and_expr(implication.lhs).op0());
       auto &state = to_symbol_expr(function_application.function());
-      auto cond = to_and_expr(implication.lhs).op1();
-      propagator(state, implies_exprt(cond, simplified2), work.path);
+      auto cond1 = to_and_expr(implication.lhs).op1();
+      auto cond2 = implies_exprt(cond1, simplified2);
+      propagator(state, cond2, work.path);
     }
   }
 }

src/cprover/solver.cpp

@@ -220,7 +220,11 @@ bool is_subsumed(
       return true; // b is subsumed by a conjunct in a
 
   cout_message_handlert message_handler;
+#if 0
   message_handler.set_verbosity(verbose ? 10 : 1);
+#else
+  message_handler.set_verbosity(1);
+#endif
   satcheckt satcheck(message_handler);
   bv_pointers_widet solver(ns, satcheck, message_handler);
   axiomst axioms(solver, address_taken, verbose, ns);
@@ -295,7 +299,7 @@ void solver(
   take_time_resourcet stop_time(property.stop);
 
   if(solver_options.verbose)
-    std::cout << "\nDoing " << format(property.condition) << '\n';
+    std::cout << "Doing " << format(property.condition) << '\n';
 
   for(auto &frame : frames)
     frame.reset();
@@ -325,31 +329,50 @@ void solver(
 
       if(solver_options.verbose)
       {
-        std::cout << "F: " << format(symbol) << " <- " << format(invariant)
-                  << '\n';
+        // print the current invariants in the frame
+        for(const auto &invariant : f.invariants)
+        {
+          std::cout << consolet::faint << consolet::blue;
+          std::cout << 'I' << std::setw(2) << frame_ref.index << ' ';
+          std::cout << format(invariant);
+          std::cout << consolet::reset << '\n';
+        }
+
+        std::cout << "\u2192" << consolet::faint << std::setw(2)
+                  << frame_ref.index << consolet::reset << ' ';
       }
 
-      // check if already subsumed
-      if(is_subsumed(
-           f.invariants,
-           f.auxiliaries,
-           invariant,
-           address_taken,
-           solver_options.verbose,
-           ns))
+      // trivially true?
+      if(invariant.is_true())
+      {
+        if(solver_options.verbose)
+          std::cout << "trivial\n";
+      }
+      else if(is_subsumed(
+                f.invariants,
+                f.auxiliaries,
+                invariant,
+                address_taken,
+                solver_options.verbose,
+                ns))
       {
         if(solver_options.verbose)
-          std::cout << "*** SUBSUMED\n";
+          std::cout << "subsumed " << format(invariant) << '\n';
       }
       else if(count_frame(path, frame_ref) > solver_options.loop_limit)
       {
         // loop limit exceeded, drop it
         if(solver_options.verbose)
-          std::cout << "*** DROPPED\n";
-        dropped.push_back(workt(frame_ref, invariant, path));
+          std::cout << consolet::red << "dropped" << consolet::reset << ' '
+                    << format(invariant) << '\n';
+        dropped.emplace_back(frame_ref, invariant, path);
       }
       else
       {
+        // propagate
+        if(solver_options.verbose)
+          std::cout << format(invariant) << '\n';
+
         auto new_path = path;
         new_path.push_back(frame_ref);
         queue.emplace_back(f.ref, std::move(invariant), std::move(new_path));
@@ -367,11 +390,13 @@ void solver(
 
     frames[work.frame.index].add_invariant(work.invariant);
 
+#if 0
     if(solver_options.verbose)
     {
       dump(frames, property, true, true);
       std::cout << '\n';
     }
+#endif
 
     auto counterexample_found = ::counterexample_found(
       frames, work, address_taken, solver_options.verbose, ns);
@@ -401,11 +426,13 @@ solver_resultt solver(
 {
   const auto address_taken = ::address_taken(constraints);
 
+#if 0
   if(solver_options.verbose)
   {
     for(auto &a : address_taken)
       std::cout << "address_taken: " << format(a) << '\n';
   }
+#endif
 
   auto frames = setup_frames(constraints);
 

src/cprover/solver_progress.cpp

@@ -19,6 +19,10 @@ void solver_progresst::operator()(size_t current)
 {
   if(verbose)
   {
+    if(current != 0)
+      std::cout << '\n';
+    std::cout << consolet::orange << "Processing property " << (current + 1)
+              << '/' << total << consolet::reset << '\n';
   }
   else
   {
@@ -44,6 +48,7 @@ void solver_progresst::finished()
 {
   if(verbose)
   {
+    std::cout << '\n';
   }
   else
   {

src/cprover/state_encoding.cpp

@@ -1245,11 +1245,13 @@ solver_resultt state_encoding_solver(
 
   equality_propagation(container.constraints);
 
+#if 0
   if(solver_options.verbose)
   {
     ascii_encoding_targett dest(std::cout);
     dest << container;
   }
+#endif
 
   return solver(container.constraints, solver_options, ns);
 }