Independent solver rework

include/klee/ADT/DisjointSetUnion.h

@@ -0,0 +1,143 @@
+#ifndef KLEE_DISJOINEDSETUNION_H
+#define KLEE_DISJOINEDSETUNION_H
+#include "klee/ADT/PersistentMap.h"
+#include "klee/ADT/PersistentSet.h"
+#include "klee/ADT/Ref.h"
+#include <set>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace klee {
+
+template <typename ValueType, typename SetType,
+          typename CMP = std::less<ValueType>>
+class DisjointSetUnion {
+protected:
+  PersistentMap<ValueType, ValueType, CMP> parent;
+  PersistentSet<ValueType, CMP> roots;
+  PersistentMap<ValueType, size_t, CMP> rank;
+
+  PersistentSet<ValueType, CMP> internalStorage;
+  PersistentMap<ValueType, ref<const SetType>, CMP> disjointSets;
+
+  ValueType find(const ValueType &v) { // findparent
+    assert(parent.find(v) != parent.end());
+    if (v == parent.at(v))
+      return v;
+    parent.replace({v, find(parent.at(v))});
+    return parent.at(v);
+  }
+
+  ValueType constFind(const ValueType &v) const {
+    assert(parent.find(v) != parent.end());
+    ValueType v1 = parent.at(v);
+    if (v == v1)
+      return v;
+    return constFind(v1);
+  }
+
+  void merge(ValueType a, ValueType b) {
+    a = find(a);
+    b = find(b);
+    if (a == b) {
+      return;
+    }
+
+    if (rank.at(a) < rank.at(b)) {
+      std::swap(a, b);
+    }
+    parent.replace({b, a});
+    if (rank.at(a) == rank.at(b)) {
+      rank.replace({a, rank.at(a) + 1});
+    }
+
+    roots.remove(b);
+    disjointSets.replace(
+        {a, SetType::merge(disjointSets.at(a), disjointSets.at(b))});
+    disjointSets.replace({b, nullptr});
+  }
+
+  bool areJoined(const ValueType &i, const ValueType &j) const {
+    return constFind(i) == constFind(j);
+  }
+
+public:
+  using internalStorage_ty = PersistentSet<ValueType, CMP>;
+  using disjointSets_ty = ImmutableMap<ValueType, ref<const SetType>, CMP>;
+  using iterator = typename internalStorage_ty::iterator;
+
+  iterator begin() const { return internalStorage.begin(); }
+  iterator end() const { return internalStorage.end(); }
+
+  size_t numberOfValues() const noexcept { return internalStorage.size(); }
+
+  size_t numberOfGroups() const noexcept { return disjointSets.size(); }
+
+  bool empty() const noexcept { return numberOfValues() == 0; }
+
+  ref<const SetType> findGroup(const ValueType &i) const {
+    return disjointSets.find(constFind(i))->second;
+  }
+
+  ref<const SetType> findGroup(iterator it) const {
+    return disjointSets.find(constFind(*it))->second;
+  }
+
+  void addValue(const ValueType value) {
+    if (internalStorage.find(value) != internalStorage.end()) {
+      return;
+    }
+    parent.insert({value, value});
+    roots.insert(value);
+    rank.insert({value, 0});
+    disjointSets.insert({value, new SetType(value)});
+
+    internalStorage.insert(value);
+    internalStorage_ty oldRoots = roots;
+    for (ValueType v : oldRoots) {
+      if (!areJoined(v, value) &&
+          SetType::intersects(disjointSets.at(find(v)),
+                              disjointSets.at(find(value)))) {
+        merge(v, value);
+      }
+    }
+  }
+  void getAllIndependentSets(std::vector<ref<const SetType>> &result) const {
+    for (ValueType v : roots)
+      result.push_back(findGroup(v));
+  }
+
+  void add(const DisjointSetUnion &b) {
+    for (auto it : b.parent) {
+      parent.insert(it);
+    }
+    for (auto it : b.roots) {
+      roots.insert(it);
+    }
+    for (auto it : b.rank) {
+      rank.insert(it);
+    }
+    for (auto it : b.internalStorage) {
+      internalStorage.insert(it);
+    }
+    for (auto it : b.disjointSets) {
+      disjointSets.insert(it);
+    }
+  }
+
+  DisjointSetUnion() {}
+
+  DisjointSetUnion(const internalStorage_ty &is) {
+    for (ValueType v : is) {
+      addValue(v);
+    }
+  }
+
+public:
+  internalStorage_ty is() const { return internalStorage; }
+
+  disjointSets_ty ds() const { return disjointSets; }
+};
+} // namespace klee
+#endif

include/klee/ADT/ImmutableMap.h

@@ -44,6 +44,32 @@ template <class K, class D, class CMP = std::less<K>> class ImmutableMap {
     return *this;
   }
 
+  bool operator==(const ImmutableMap &b) const {
+    if (size() != b.size()) {
+      return false;
+    }
+    for (iterator it1 = begin(), it2 = b.begin();
+         it1 != end() && it2 != b.end(); ++it1, ++it2) {
+      if (*it1 != *it2)
+        return false;
+    }
+    return true;
+  }
+
+  bool operator<(const ImmutableMap &b) const {
+    if (size() != b.size()) {
+      return size() < b.size();
+    }
+    for (iterator it1 = begin(), it2 = b.begin();
+         it1 != end() && it2 != b.end(); ++it1, ++it2) {
+      if (*it1 < *it2)
+        return true;
+      if (*it1 > *it2)
+        return false;
+    }
+    return false;
+  }
+
   bool empty() const { return elts.empty(); }
   size_t count(const key_type &key) const { return elts.count(key); }
   const value_type *lookup(const key_type &key) const {
@@ -80,6 +106,7 @@ template <class K, class D, class CMP = std::less<K>> class ImmutableMap {
     return elts.upper_bound(key);
   }
 
+  const D &at(const key_type &key) const { return find(key)->second; }
   static size_t getAllocated() { return Tree::allocated; }
 };
 

include/klee/ADT/PersistentMap.h

@@ -37,6 +37,8 @@ template <class K, class D, class CMP = std::less<K>> class PersistentMap {
     elts = b.elts;
     return *this;
   }
+  bool operator==(const PersistentMap &b) const { return elts == b.elts; }
+  bool operator<(const PersistentMap &b) const { return elts < b.elts; }
 
   bool empty() const { return elts.empty(); }
   size_t count(const key_type &key) const { return elts.count(key); }
@@ -77,6 +79,8 @@ template <class K, class D, class CMP = std::less<K>> class PersistentMap {
       return *lookup(key);
     }
   }
+
+  const D &at(const key_type &key) const { return elts.at(key); }
 };
 } // namespace klee
 

include/klee/Expr/Assignment.h

@@ -10,6 +10,7 @@
 #ifndef KLEE_ASSIGNMENT_H
 #define KLEE_ASSIGNMENT_H
 
+#include "klee/ADT/PersistentMap.h"
 #include "klee/ADT/SparseStorage.h"
 #include "klee/Expr/ExprEvaluator.h"
 
@@ -27,24 +28,20 @@ using symcretes_ty = SymcreteOrderedSet;
 
 class Assignment {
 public:
-  typedef std::map<const Array *, SparseStorage<unsigned char>> bindings_ty;
+  using bindings_ty =
+      PersistentMap<const Array *, SparseStorage<unsigned char>>;
 
-  bool allowFreeValues;
   bindings_ty bindings;
 
   friend bool operator==(const Assignment &lhs, const Assignment &rhs) {
     return lhs.bindings == rhs.bindings;
   }
 
 public:
-  Assignment(bool _allowFreeValues = false)
-      : allowFreeValues(_allowFreeValues) {}
-  Assignment(const bindings_ty &_bindings, bool _allowFreeValues = false)
-      : allowFreeValues(_allowFreeValues), bindings(_bindings) {}
+  Assignment() {}
+  Assignment(const bindings_ty &_bindings) : bindings(_bindings) {}
   Assignment(const std::vector<const Array *> &objects,
-             const std::vector<SparseStorage<unsigned char>> &values,
-             bool _allowFreeValues = false)
-      : allowFreeValues(_allowFreeValues) {
+             const std::vector<SparseStorage<unsigned char>> &values) {
     assert(objects.size() == values.size());
     for (unsigned i = 0; i < values.size(); ++i) {
       const Array *os = objects.at(i);
@@ -53,19 +50,26 @@ class Assignment {
     }
   }
 
-  ref<Expr> evaluate(const Array *mo, unsigned index) const;
-  ref<Expr> evaluate(ref<Expr> e) const;
-  ConstraintSet createConstraintsFromAssignment() const;
+  void addIndependentAssignment(const Assignment &b);
+
+  ref<Expr> evaluate(const Array *mo, unsigned index,
+                     bool allowFreeValues = true) const;
+  ref<Expr> evaluate(ref<Expr> e, bool allowFreeValues = true) const;
+  constraints_ty createConstraintsFromAssignment() const;
 
   template <typename InputIterator>
-  bool satisfies(InputIterator begin, InputIterator end);
+  bool satisfies(InputIterator begin, InputIterator end,
+                 bool allowFreeValues = true);
+  template <typename InputIterator>
+  bool satisfiesNonBoolean(InputIterator begin, InputIterator end,
+                           bool allowFreeValues = true);
   void dump() const;
 
   Assignment diffWith(const Assignment &other) const;
   Assignment part(const SymcreteOrderedSet &symcretes) const;
 
-  bindings_ty::const_iterator begin() const { return bindings.begin(); }
-  bindings_ty::const_iterator end() const { return bindings.end(); }
+  bindings_ty::iterator begin() const { return bindings.begin(); }
+  bindings_ty::iterator end() const { return bindings.end(); }
   bool isEmpty() { return begin() == end(); }
 
   std::vector<const Array *> keys() const;
@@ -74,22 +78,24 @@ class Assignment {
 
 class AssignmentEvaluator : public ExprEvaluator {
   const Assignment &a;
+  bool allowFreeValues;
 
 protected:
   ref<Expr> getInitialValue(const Array &mo, unsigned index) {
-    return a.evaluate(&mo, index);
+    return a.evaluate(&mo, index, allowFreeValues);
   }
 
 public:
-  AssignmentEvaluator(const Assignment &_a) : a(_a) {}
+  AssignmentEvaluator(const Assignment &_a, bool _allowFreeValues)
+      : a(_a), allowFreeValues(_allowFreeValues) {}
 };
 
 /***/
 
-inline ref<Expr> Assignment::evaluate(const Array *array,
-                                      unsigned index) const {
+inline ref<Expr> Assignment::evaluate(const Array *array, unsigned index,
+                                      bool allowFreeValues) const {
   assert(array);
-  bindings_ty::const_iterator it = bindings.find(array);
+  bindings_ty::iterator it = bindings.find(array);
   if (it != bindings.end() && index < it->second.size()) {
     return ConstantExpr::alloc(it->second.load(index), array->getRange());
   } else {
@@ -102,17 +108,32 @@ inline ref<Expr> Assignment::evaluate(const Array *array,
   }
 }
 
-inline ref<Expr> Assignment::evaluate(ref<Expr> e) const {
-  AssignmentEvaluator v(*this);
+inline ref<Expr> Assignment::evaluate(ref<Expr> e, bool allowFreeValues) const {
+  AssignmentEvaluator v(*this, allowFreeValues);
   return v.visit(e);
 }
 
 template <typename InputIterator>
-inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
-  AssignmentEvaluator v(*this);
-  for (; begin != end; ++begin)
+inline bool Assignment::satisfies(InputIterator begin, InputIterator end,
+                                  bool allowFreeValues) {
+  AssignmentEvaluator v(*this, allowFreeValues);
+  for (; begin != end; ++begin) {
+    assert((*begin)->getWidth() == Expr::Bool && "constraints must be boolean");
     if (!v.visit(*begin)->isTrue())
       return false;
+  }
+  return true;
+}
+
+template <typename InputIterator>
+inline bool Assignment::satisfiesNonBoolean(InputIterator begin,
+                                            InputIterator end,
+                                            bool allowFreeValues) {
+  AssignmentEvaluator v(*this, allowFreeValues);
+  for (; begin != end; ++begin) {
+    if (!isa<ConstantExpr>(v.visit(*begin)))
+      return false;
+  }
   return true;
 }
 } // namespace klee

include/klee/Expr/Constraints.h

@@ -16,6 +16,8 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/IndependentConstraintSetUnion.h"
+#include "klee/Expr/IndependentSet.h"
 #include "klee/Expr/Path.h"
 #include "klee/Expr/Symcrete.h"
 
@@ -35,6 +37,8 @@ class ConstraintSet {
 public:
   ConstraintSet(constraints_ty cs, symcretes_ty symcretes,
                 Assignment concretization);
+  ConstraintSet(ref<const IndependentConstraintSet> ics);
+  ConstraintSet(const std::vector<ref<const IndependentConstraintSet>> &ics);
   ConstraintSet();
 
   void addConstraint(ref<Expr> e, const Assignment &delta);
@@ -55,7 +59,8 @@ class ConstraintSet {
     return _constraints < b._constraints ||
            (_constraints == b._constraints && _symcretes < b._symcretes);
   }
-
+  ConstraintSet getConcretizedVersion() const;
+  ConstraintSet getConcretizedVersion(const Assignment &c) const;
   void dump() const;
   void print(llvm::raw_ostream &os) const;
 
@@ -64,11 +69,21 @@ class ConstraintSet {
   const constraints_ty &cs() const;
   const symcretes_ty &symcretes() const;
   const Assignment &concretization() const;
+  const IndependentConstraintSetUnion &independentElements() const;
+
+  void getAllIndependentConstraintsSets(
+      ref<Expr> queryExpr,
+      std::vector<ref<const IndependentConstraintSet>> &result) const;
+
+  void getAllDependentConstraintsSets(
+      ref<Expr> queryExpr,
+      std::vector<ref<const IndependentConstraintSet>> &result) const;
 
 private:
   constraints_ty _constraints;
   symcretes_ty _symcretes;
   Assignment _concretization;
+  IndependentConstraintSetUnion _independentElements;
 };
 
 class PathConstraints {