Some comments and minor modifications

Author: Yakir Vizel

src/cprover/chc_large_step.h

@@ -9,9 +9,9 @@
 #include <util/substitute_symbols.h>
 #include <util/format_expr.h>
 
-/*
- * Traverses the clauses in order and resolving all predicates (symbols)
- * that are not a head (e.g. a head of a loop).
+/**
+ * Traverses the clauses in order (wto) and resolving all predicates (symbols)
+ * that are not a head of a component (e.g. a head of a loop).
  * This is similar to variable elimination in SAT.
  */
 class resolution_visitort : public wto_element_visitort
@@ -38,15 +38,19 @@ class resolution_visitort : public wto_element_visitort
   {
     const symbol_exprt* head = comp.head();
     m_heads.insert(head->hash());
-    std::string str = head->get_identifier().c_str();
-    std::cout << "Head: " << str << "\n";
+    if (m_verbose)
+    {
+      std::string str = head->get_identifier().c_str();
+      std::cout << "Head: " << str << "\n";
+    }
     for (auto it = comp.begin(); it != comp.end(); it++)
     {
       it->get()->accept(this);
     }
     eliminate(head);
   }
 
+  // Create the new CHC db after eliminating uninterpreted predicates.
   void populate_new_db()
   {
     std::vector<symbol_exprt> rels;
@@ -131,6 +135,13 @@ class resolution_visitort : public wto_element_visitort
     }
   }
 
+  /** Assuming the following shapes:
+   * c1 := Sxx(ς) ∧ ς(COND1) ⇒ Syy(ς[update1])
+   * c2 := Syy(ς) ∧ ς(COND2) ⇒ Szz(ς[update2])
+   * In this case, Syy(ς) is eliminated and we use substitution for c2 such
+   * that it "operates" over ς[update1]. This results in:
+   * Sxx(ς) ∧ ς(COND1) ∧ ς[update1](COND2) ⇒ Szz(ς[update1][update2])
+   */
   forall_exprt resolve_clauses(const horn_clauset & c1, const horn_clauset & c2)
   {
     const exprt &body1 = *c1.body();

src/cprover/chc_wto.h

@@ -17,6 +17,22 @@
 class wto_singletont;
 class wto_componentt;
 
+/**
+ * Bourdoncle Components over the cut-point graph of CHCs is a weak topological
+ * ordering (wto) on cut-points. This is mainly known from the work on
+ * widening operations in abstract interpretation. The most common intuition
+ * is an ordering of graph vertices with well-formed (aka well-matched)
+ * parentheses that mark components.
+ *
+ * For example, 1 (2 (3 4 5 6) 7) 8 is a wto with two components, where the
+ * inner componenet includes vertices 3-6, the outter component includes
+ * vertices 2 and 7. In this simple example, vertex 1 is the entry point, and
+ * vertex 8 is the exit point. Vertex 2 can be though of as the head of the
+ * outer loop, while vertex 3 is the head of the inner loop.
+ *
+ * The wto is used to guide the elimination step.
+ */
+
 class wto_element_visitort
 {
 public:
@@ -171,7 +187,6 @@ class chc_wtot
   }
 
   inf_numt visit(const symbol_exprt* v, std::deque<wto_element_ptr> &partition) {
-    std::string name = as_string(v->get_identifier());
     m_stack.push_back(v);
     m_dfn[v->hash()] = m_cur_dfn_num++;
     auto head = get_dfn(v);
@@ -276,6 +291,10 @@ class chc_wtot
   }
 };
 
+/**
+ * Simple Visitor prints the components of the WTO with well-formed
+ * parentheses.
+ */
 class simple_visitort : public wto_element_visitort
 {
   virtual void visit(const wto_singletont & s)

src/cprover/cutpoint_graph.h

@@ -14,11 +14,16 @@
  * 1. Entry node
  * 2. Exit node
  * 3. Every node that has a back-edge - namely, a loop head.
+ * This graph is used for large-step encoding of CHCs. Uninterpreted predicates
+ * are only needed where there are cut-points.
  */
 
 class cutpoint_grapht;
 class cutpointt;
 
+/**
+ * A class that represents an edge in the graph
+ */
 class cutpoint_edget
 {
   friend class cutpoint_grapht;
@@ -55,6 +60,9 @@ class cutpoint_edget
 
 typedef std::shared_ptr<cutpoint_edget> cutpoint_edge_ptr;
 
+/**
+ * A class that represents a cutpoint in the graph
+ */
 class cutpointt
 {
   const cutpoint_grapht &m_graph;
@@ -87,6 +95,9 @@ class cutpointt
   }
 };
 
+/**
+ * The graph
+ */
 class cutpoint_grapht
 {
   const goto_modelt & m_goto_model;