Reworking independent and concretizing solvers

.github/workflows/build.yaml

@@ -2,9 +2,9 @@ name: CI
 
 on:
   pull_request:
-    branches: [main, utbot-main]
+    branches: [IndependentSolverReworkFinal, main, utbot-main]
   push:
-    branches: [main, utbot-main]
+    branches: [IndependentSolverReworkFinal, main, utbot-main]
 
 # Defaults for building KLEE
 env:

include/klee/ADT/DisjointSetUnion.h

@@ -0,0 +1,130 @@
+#ifndef KLEE_DISJOINEDSETUNION_H
+#define KLEE_DISJOINEDSETUNION_H
+#include "klee/ADT/Ref.h"
+
+#include <set>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace klee {
+
+template <typename ValueType, typename SetType, typename HashType>
+class DisjointSetUnion {
+protected:
+  std::unordered_map<ValueType, ValueType, HashType> parent;
+  std::unordered_set<ValueType, HashType> roots;
+  std::unordered_map<ValueType, size_t, HashType> rank;
+
+  std::unordered_set<ValueType, HashType> internalStorage;
+  std::unordered_map<ValueType, ref<const SetType>, HashType> disjointSets;
+
+  ValueType find(const ValueType &v) { // findparent
+    assert(parent.find(v) != parent.end());
+    if (v == parent[v])
+      return v;
+    return parent[v] = find(parent[v]);
+  }
+
+  ValueType constFind(const ValueType &v) const {
+    assert(parent.find(v) != parent.end());
+    ValueType v1 = parent.find(v)->second;
+    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[a] < rank[b]) {
+      std::swap(a, b);
+    }
+    parent[b] = a;
+    if (rank[a] == rank[b]) {
+      rank[a]++;
+    }
+
+    roots.erase(b);
+    disjointSets[a] = SetType::merge(disjointSets[a], disjointSets[b]);
+    disjointSets[b] = nullptr;
+  }
+
+  bool areJoined(const ValueType &i, const ValueType &j) const {
+    return constFind(i) == constFind(j);
+  }
+
+public:
+  using internalStorage_ty = std::unordered_set<ValueType, HashType>;
+  using disjointSets_ty =
+      std::unordered_map<ValueType, ref<const SetType>, HashType>;
+  using const_iterator = typename internalStorage_ty::const_iterator;
+
+  const_iterator begin() const { return internalStorage.begin(); }
+  const_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(const_iterator it) const {
+    return disjointSets.find(constFind(*it))->second;
+  }
+
+  void addValue(const ValueType value) {
+    if (internalStorage.find(value) != internalStorage.end()) {
+      return;
+    }
+    parent[value] = value;
+    roots.insert(value);
+    rank[value] = 0;
+    disjointSets[value] = new SetType(value);
+
+    internalStorage.insert(value);
+    std::vector<ValueType> oldRoots(roots.begin(), roots.end());
+    for (ValueType v : oldRoots) {
+      if (!areJoined(v, value) &&
+          SetType::intersects(disjointSets[find(v)],
+                              disjointSets[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) {
+    parent.insert(b.parent.begin(), b.parent.end());
+    roots.insert(b.roots.begin(), b.roots.end());
+    rank.insert(b.rank.begin(), b.rank.end());
+
+    internalStorage.insert(b.internalStorage.begin(), b.internalStorage.end());
+    disjointSets.insert(b.disjointSets.begin(), b.disjointSets.end());
+  }
+  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/OrderMaintenanceTrie.h

@@ -0,0 +1,243 @@
+#ifndef KLEE_ORDERMAINTENANCETRIE_H
+#define KLEE_ORDERMAINTENANCETRIE_H
+#include <bitset>
+#include <cassert>
+#include <cmath>
+#include <cstddef>
+#include <iterator>
+#include <memory>
+#include <vector>
+
+#define ITEMSIZE 64 // depth of tree
+#define ALPHA 1.4   // balancing constant
+
+namespace klee {
+
+class OrderMaintenanaceTrie {
+private:
+  struct Node {
+
+    size_t height = 0;
+    size_t weight = 0;
+    size_t tag = 0;
+
+    Node *parent = nullptr;
+    Node *left = nullptr;
+    Node *right = nullptr;
+
+    Node(size_t h = 0, Node *p = nullptr) {
+      parent = p;
+      height = h;
+    }
+
+    bool isFull() {
+      return std::pow(0.5, ITEMSIZE - height) * weight >
+             std::pow(1.0 / ALPHA, height);
+    }
+    ~Node() {
+      if (left)
+        delete left;
+      if (right)
+        delete right;
+      if (parent) {
+        if (this == parent->left)
+          parent->left = nullptr;
+        if (this == parent->right)
+          parent->right = nullptr;
+      }
+      Node *current = parent;
+      while (current) {
+        current->weight -= weight;
+        current = current->parent;
+      }
+    }
+  };
+
+private:
+  Node *root;
+
+private:
+  Node *insert(size_t x) const {
+    std::bitset<ITEMSIZE> xbin(x);
+    Node *current = root;
+    for (int i = ITEMSIZE - 1; i > -1; i--) {
+      current->weight++;
+      if (!xbin[i]) {
+        if (!current->left)
+          current->left = new Node(current->height + 1, current);
+        current = current->left;
+      } else {
+        if (!current->right)
+          current->right = new Node(current->height + 1, current);
+        current = current->right;
+      }
+    }
+    current->tag = x;
+    return current;
+  }
+
+  Node *find(size_t x) const {
+    std::bitset<ITEMSIZE> xbin(x);
+    Node *current = root;
+    for (int i = ITEMSIZE - 1; i > -1; i--) {
+      if (!xbin[i]) {
+        if (!current->left)
+          return nullptr;
+        current = current->left;
+      } else {
+        if (!current->right)
+          return nullptr;
+        current = current->right;
+      }
+    }
+    return current;
+  }
+
+  Node *getNext(Node *x) const {
+    Node *current = x;
+    assert(current && "No such item in trie");
+    while (current->parent &&
+           (current == current->parent->right || !current->parent->left ||
+            !current->parent->right)) {
+      current = current->parent;
+    }
+    if (!current->parent)
+      return nullptr;
+
+    current = current->parent->right;
+    while (current->height != ITEMSIZE) {
+      if (current->left)
+        current = current->left;
+      else if (current->right)
+        current = current->right;
+      else
+        assert(false);
+    }
+    return current;
+  }
+
+  Node *getNext(size_t x) const {
+    Node *current = find(x);
+    return getNext(current);
+  }
+
+  bool getNextItem(size_t x, size_t &result) const {
+    if (!getNext(x))
+      return false;
+    Node *next = getNext(x);
+    result = next->tag;
+    return true;
+  }
+
+  void findAllLeafs(Node *item, std::vector<Node *> &result) {
+    if (item->height == ITEMSIZE)
+      result.push_back(item);
+    if (item->left) {
+      findAllLeafs(item->left, result);
+    }
+    if (item->right) {
+      findAllLeafs(item->right, result);
+    }
+  }
+
+  void rebalance(Node *item) {
+    while (item->parent && item->parent->isFull()) {
+      item = item->parent;
+    }
+    assert(item->parent && "Wrong choice of constants");
+    std::vector<Node *> leafs;
+    findAllLeafs(item, leafs);
+    assert(leafs.size() > 0);
+    size_t min;
+    min = leafs[0]->tag;
+    min = min >> (ITEMSIZE - item->height) << (ITEMSIZE - item->height);
+    size_t diff = ((1 << (ITEMSIZE - item->height)) - 1) / leafs.size();
+
+    for (Node *i : leafs) {
+      i->parent->left = nullptr;
+      i->parent->right = nullptr;
+    }
+    delete item;
+    for (Node *i : leafs) {
+      Node *newItem = insert(min);
+      *i = *(newItem);
+      Node *parent = newItem->parent;
+      if (newItem == parent->left) {
+        delete newItem;
+        parent->left = i;
+      } else {
+        delete newItem;
+        parent->right = i;
+      }
+      min += diff;
+    }
+  }
+
+public:
+  struct Iterator {
+    using iterator_category = std::input_iterator_tag;
+    using difference_type = std::ptrdiff_t;
+    using value_type = size_t;
+    using pointer = size_t *;
+    using reference = size_t &;
+
+  private:
+    OrderMaintenanaceTrie::Node *leaf;
+    const OrderMaintenanaceTrie *owner;
+
+  public:
+    Iterator(OrderMaintenanaceTrie::Node *leaf = nullptr,
+             const OrderMaintenanaceTrie *owner = nullptr)
+        : leaf(leaf), owner(owner) {}
+
+    Iterator &operator++() {
+      if (!owner->getNext(leaf)) {
+        leaf = nullptr;
+        owner = nullptr;
+        return *this;
+      }
+      leaf = owner->getNext(leaf);
+      return *this;
+    }
+
+    bool operator==(const Iterator &other) const { return leaf == other.leaf; }
+
+    bool operator!=(const Iterator &other) const { return !(*this == other); }
+
+    size_t operator*() const {
+      assert(leaf);
+      return leaf->tag;
+    }
+  };
+
+public:
+  Iterator begin() { return Iterator(find(0), this); }
+  Iterator end() { return Iterator(nullptr, nullptr); }
+
+  OrderMaintenanaceTrie() {
+    root = new Node();
+    insert(0);
+  }
+
+  ~OrderMaintenanaceTrie() {
+    std::vector<Node *> leafs;
+    findAllLeafs(root, leafs);
+    delete root;
+  }
+
+  Iterator insertAfter(Iterator it) {
+    size_t next = 0;
+    size_t p = *it;
+    if (!getNextItem(p, next) || next != p + 1) {
+      return Iterator(insert(p + 1), this);
+    }
+    Node *found = find(p);
+    rebalance(found);
+    return Iterator(insert(found->tag + 1), this);
+  }
+};
+} // namespace klee
+
+#undef ITEMSIZE
+#undef ALPHA
+#endif