Extracting new chcs after transformation

Author: Yakir Vizel

src/cprover/chc_large_step.h

@@ -20,6 +20,8 @@ class ResolutionVisitor : public wto_element_visitort
 public:
   ResolutionVisitor(chc_db & db) : m_db(db) {}
 
+  chc_db &giveme_new_db() { return m_new_db; }
+
   virtual void visit(const wto_singletont & s)
   {
     const symbol_exprt* symb = s.get();
@@ -39,23 +41,37 @@ class ResolutionVisitor : public wto_element_visitort
     resolve(head);
   }
 
-  std::vector<horn_clause> getClauses()
+  void populate_new_db()
   {
-    std::vector<horn_clause> all;
-    for (auto it = m_heads.begin(); it != m_heads.end(); it++)
+    std::vector<symbol_exprt> rels;
+    for (auto &clause : m_db)
+    {
+      if(clause.is_query())
+      {
+        clause.used_relations(m_db, std::back_inserter(rels));
+      }
+    }
+
+    std::set<std::size_t > preds_hash(m_heads.begin(), m_heads.end());
+    for (auto p : rels) {
+      preds_hash.insert(p.hash());
+    }
+
+    for (auto it : preds_hash)
     {
-      auto c = m_def.find(*it);
+      auto c = m_def.find(it);
       INVARIANT(c != m_def.end(), "No clauses");
-      all.insert(all.begin(), c->second.begin(), c->second.end());
+      for (auto clause : c->second)
+        m_new_db.add_clause(clause.get_chc());
     }
-    return all;
-  }
 
-  const std::vector<horn_clause>& getClauses(const symbol_exprt* symb)
-  {
-    auto it = m_def.find(symb->hash());
-    INVARIANT(it != m_def.end(), "No clauses");
-    return it->second;
+    for (auto &clause : m_db)
+    {
+      if(clause.is_query())
+      {
+        m_new_db.add_clause(clause.get_chc());
+      }
+    }
   }
 
 private:

src/cprover/state_encoding.cpp

@@ -1261,45 +1261,25 @@ void large_step_encoding(const container_encoding_targett & small_step_container
     {
       db.add_state_pred(s);
     }
-
   }
   chc_graph chc_g(db);
   chc_g.build_graph();
 
   chc_wtot wto(chc_g);
   wto.build_wto();
 
-  SimpleVisitor v;
-  for (auto it = wto.begin(); it != wto.end(); it++)
-  {
-    auto x = (*it);
-    x->accept(&v);
-  }
-
-  std::cout << "\n";
-
   ResolutionVisitor rv(db);
   for (auto it = wto.begin(); it != wto.end(); it++)
   {
     auto x = (*it);
     x->accept(&rv);
   }
 
-  std::vector<horn_clause> all = rv.getClauses();
-  for (auto &clause : db) {
-    if (clause.is_query()) {
-      std::vector<symbol_exprt> rels;
-      clause.used_relations(db, std::back_inserter(rels));
-      for (auto pred : rels)
-      {
-        all.insert(all.end(), rv.getClauses(&pred).begin(), rv.getClauses(&pred).end());
-      }
-      all.push_back(clause.get_chc());
-    }
-
-  }
+  rv.populate_new_db();
 
-  for (auto ce : all)
+  container_encoding_targett container2;
+  std::vector<horn_clause> all2;
+  for (auto & ce : rv.giveme_new_db())
   {
     large_step_container << ce.get_chc();
   }