CHC solver: use hash set instead of linear search

This enables faster than linear lookup of conjuncts of the current invariant
hypothesis.

Author: kroening

src/cprover/solver.cpp

@@ -35,8 +35,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <set>
 
 bool is_subsumed(
-  const std::vector<exprt> &a1,
-  const std::vector<exprt> &a2,
+  const std::unordered_set<exprt, irep_hash> &a1,
+  const std::unordered_set<exprt, irep_hash> &a2,
   const exprt &b,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
@@ -45,13 +45,11 @@ bool is_subsumed(
   if(b.is_true())
     return true; // anything subsumes 'true'
 
-  for(auto &a_conjunct : a1)
-    if(a_conjunct.is_false())
-      return true; // 'false' subsumes anything
+  if(a1.find(false_exprt()) != a1.end())
+    return true; // 'false' subsumes anything
 
-  for(auto &a_conjunct : a1)
-    if(a_conjunct == b)
-      return true; // b is subsumed by a conjunct in a
+  if(a1.find(b) != a1.end())
+    return true; // b is subsumed by a conjunct in a
 
   cout_message_handlert message_handler;
 #if 0
@@ -183,8 +181,8 @@ void solver(
           std::cout << "trivial\n";
       }
       else if(is_subsumed(
-                f.invariants,
-                f.auxiliaries,
+                f.invariants_set,
+                f.auxiliaries_set,
                 invariant,
                 address_taken,
                 solver_options.verbose,

src/cprover/solver_types.cpp

@@ -26,7 +26,10 @@ void framet::add_invariant(exprt invariant)
       add_invariant(conjunct);
   }
   else
+  {
+    invariants_set.insert(invariant);
     invariants.push_back(std::move(invariant));
+  }
 }
 
 void framet::add_auxiliary(exprt invariant)
@@ -37,7 +40,10 @@ void framet::add_auxiliary(exprt invariant)
       add_auxiliary(conjunct);
   }
   else
+  {
+    auxiliaries_set.insert(invariant);
     auxiliaries.push_back(std::move(invariant));
+  }
 }
 
 frame_mapt build_frame_map(const std::vector<framet> &frames)

src/cprover/solver_types.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <chrono>
 #include <unordered_map>
+#include <unordered_set>
 
 class frame_reft
 {
@@ -53,9 +54,11 @@ class framet
 
   // our current hypothesis invariant
   std::vector<exprt> invariants;
+  std::unordered_set<exprt, irep_hash> invariants_set;
 
   // auxiliary facts
   std::vector<exprt> auxiliaries;
+  std::unordered_set<exprt, irep_hash> auxiliaries_set;
 
   // formulas where this frame is on the rhs of ⇒
   struct implicationt
@@ -84,7 +87,9 @@ class framet
   void reset()
   {
     invariants.clear();
+    invariants_set.clear();
     auxiliaries.clear();
+    auxiliaries_set.clear();
   }
 
   frame_reft ref;