Removing redundant include, and fixing function arguments

Author: Yakir Vizel

src/cprover/chc_db.cpp

@@ -7,6 +7,42 @@
 chc_dbt::chc_sett chc_dbt::m_empty_set;
 std::unordered_set<exprt, irep_hash> chc_grapht::m_expr_empty_set;
 
+void horn_clauset::used_relations(chc_dbt &db, std::vector<symbol_exprt> & out) const
+{
+  const exprt *body = this->body();
+  if (body == nullptr) return;
+  std::set<symbol_exprt> symbols = find_symbols(*body);
+
+  chc_dbt::is_state_pred filter(db);
+  for (auto & symb : symbols) {
+    if (filter(symb)) {
+      out.push_back(symb);
+    }
+  }
+}
+
+void horn_clauset::used_func_app(chc_dbt &db, std::vector<function_application_exprt> & out) const
+{
+  const exprt *body = this->body();
+  if (body == nullptr) return;
+
+  std::unordered_set<function_application_exprt, irep_hash> funcs;
+  body->visit_pre([&funcs](const exprt &expr) {
+                    if (can_cast_expr<function_application_exprt>(expr))
+                    {
+                      const function_application_exprt & f = to_function_application_expr(expr);
+                      funcs.insert(f);
+                    }
+                  });
+
+  chc_dbt::is_state_pred filter(db);
+  for (auto & f : funcs) {
+    if (filter(to_symbol_expr(f.function()))) {
+      out.push_back(f);
+    }
+  }
+}
+
 void chc_dbt::reset_indices()
 {
   m_body_idx.clear();
@@ -28,7 +64,7 @@ void chc_dbt::build_indices()
     m_head_idx[func].insert(i);
 
     std::vector<symbol_exprt> use;
-    r.used_relations(*this,std::back_inserter(use));
+    r.used_relations(*this, use);
     for (auto & symb : use)
     {
       m_body_idx[symb].insert(i);

src/cprover/chc_db.h

@@ -8,7 +8,6 @@
 #include <util/mathematical_expr.h>
 #include <util/std_expr.h>
 #include <util/find_symbols.h>
-#include <language_util.h>
 
 #include <vector>
 #include <map>
@@ -101,10 +100,8 @@ class horn_clauset
     return m_chc < other.m_chc;
   }
 
-  template <typename OutputIterator>
-  void used_relations(chc_dbt &db, OutputIterator out) const;
-  template <typename OutputIterator>
-  void used_func_app(chc_dbt &db, OutputIterator out) const;
+  void used_relations(chc_dbt &db, std::vector<symbol_exprt> & out) const;
+  void used_func_app(chc_dbt &db, std::vector<function_application_exprt> & out) const;
 };
 
 /*
@@ -192,44 +189,6 @@ class chc_dbt
   chcst::const_iterator end() const { return m_clauses.end(); }
 };
 
-template <typename OutputIterator>
-void horn_clauset::used_relations(chc_dbt &db, OutputIterator out) const
-{
-  const exprt *body = this->body();
-  if (body == nullptr) return;
-  std::set<symbol_exprt> symbols = find_symbols(*body);
-
-  chc_dbt::is_state_pred filter(db);
-  for (auto & symb : symbols) {
-    if (filter(symb)) {
-      *out = symb;
-    }
-  }
-}
-
-template <typename OutputIterator>
-void horn_clauset::used_func_app(chc_dbt &db, OutputIterator out) const
-{
-  const exprt *body = this->body();
-  if (body == nullptr) return;
-
-  std::unordered_set<function_application_exprt, irep_hash> funcs;
-  body->visit_pre([&funcs](const exprt &expr) {
-                     if (can_cast_expr<function_application_exprt>(expr))
-                     {
-                       const function_application_exprt & f = to_function_application_expr(expr);
-                       funcs.insert(f);
-                     }
-                   });
-
-  chc_dbt::is_state_pred filter(db);
-  for (auto & f : funcs) {
-    if (filter(to_symbol_expr(f.function()))) {
-      *out = f;
-    }
-  }
-}
-
 /*
  * The CHC dependency graph.
  * Uninterpreted relations are vertices, dependency is based on clauses:

src/cprover/chc_large_step.h

@@ -58,7 +58,7 @@ class resolution_visitort : public wto_element_visitort
     {
       if(clause.is_query())
       {
-        clause.used_relations(m_db, std::back_inserter(rels));
+        clause.used_relations(m_db, rels);
       }
     }
 
@@ -91,8 +91,7 @@ class resolution_visitort : public wto_element_visitort
     {
       auto & clause = m_db.get_clause(idx);
       std::vector<symbol_exprt> use;
-
-      clause.used_relations(m_db,std::back_inserter(use));
+      clause.used_relations(m_db, use);
       if (use.size() > 1) {
         throw incorrect_goto_program_exceptiont("Non-linear CHCs not supported yet");
       }
@@ -150,7 +149,7 @@ class resolution_visitort : public wto_element_visitort
     const exprt &head2 = *c2.head();
 
     std::vector<function_application_exprt> use2;
-    c2.used_func_app(m_db,std::back_inserter(use2));
+    c2.used_func_app(m_db,use2);
 
     INVARIANT(use2.size() == 1, "Only handling linear case");
     if (use2.size() != 1)