[eacsl] Add support of `remove_if` and `find_if` to the patricia trie

src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c

@@ -334,9 +334,16 @@ static pt_node_t *pt_get_leaf_node_from_leaf(const pt_struct_t *pt,
   return curr;
 }
 
-void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
-  pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
-  DASSERT(leaf_node_to_delete->leaf == leaf);
+/** Remove the given leaf node from the patricia trie.
+ *
+ * Internal function for `pt_remove()` and `pt_remove_if()`. The function will
+ * delete the given leaf node and copy its sibling if it exists to the parent
+ * node.
+ */
+static void pt_remove_leaf_node(pt_struct_t *pt,
+                                pt_node_t *leaf_node_to_delete) {
+  DASSERT(leaf_node_to_delete != NULL);
+  DASSERT(leaf_node_to_delete->is_leaf);
 
   if (leaf_node_to_delete->parent == NULL) {
     // the leaf is the root
@@ -367,9 +374,49 @@ void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
     }
     /* necessary ? -- end */
   }
+  pt->clean_leaf_fct(leaf_node_to_delete->leaf);
   private_free(leaf_node_to_delete);
 }
 
+void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
+  DASSERT(pt != NULL);
+  pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
+  DASSERT(leaf_node_to_delete->leaf == leaf);
+
+  pt_remove_leaf_node(pt, leaf_node_to_delete);
+}
+
+/** Starting at `node`, remove all leaves that satisfy the given predicate from
+ * the patricia trie. Return 1 if `node` is a leaf that is removed, 0
+ * otherwise.
+ * Internal function for `pt_remove_if()`. */
+int pt_remove_node_if(pt_struct_t *pt, pt_node_t *node,
+                      pt_predicate_t predicate) {
+  DASSERT(pt != NULL);
+  if (node != NULL) {
+    if (node->is_leaf) {
+      if (predicate(node->leaf)) {
+        pt_remove_leaf_node(pt, node);
+        return 1;
+      }
+    } else {
+      // If `node->left` is a leaf that is removed, then `node->right` is
+      // copied to node and we have `node->left == \old(node->right->left)`
+      // (see `pt_remove_leaf_node()̀).
+      // We need to call `pt_remove_node_if()` on `node->left` until it is not
+      // a removed leaf.
+      while (pt_remove_node_if(pt, node->left, predicate)) {}
+      pt_remove_node_if(pt, node->right, predicate);
+    }
+  }
+  return 0;
+}
+
+void pt_remove_if(pt_struct_t *pt, pt_predicate_t predicate) {
+  DASSERT(pt != NULL);
+  pt_remove_node_if(pt, pt->root, predicate);
+}
+
 pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
   DASSERT(pt != NULL);
   DASSERT(pt->root != NULL);
@@ -452,6 +499,29 @@ pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
   }
 }
 
+static pt_leaf_t pt_find_if_rec(pt_node_t *node, pt_predicate_t predicate) {
+  DASSERT(node != NULL);
+  if (node->is_leaf) {
+    return predicate(node->leaf) ? node->leaf : NULL;
+  } else {
+    pt_node_t *result = pt_find_if_rec(node->left, predicate);
+    if (result == NULL) {
+      result = pt_find_if_rec(node->right, predicate);
+    }
+    return result;
+  }
+}
+
+pt_leaf_t pt_find_if(const pt_struct_t *pt, pt_predicate_t predicate) {
+  DASSERT(pt != NULL);
+
+  if (pt->root == NULL) {
+    return NULL;
+  } else {
+    return pt_find_if_rec(pt->root, predicate);
+  }
+}
+
 static void pt_clean_rec(const pt_struct_t *pt, pt_node_t *ptr) {
   if (ptr == NULL) {
     return;

src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h

@@ -47,6 +47,9 @@ typedef int (*contains_ptr_fct_t)(pt_leaf_t, void *);
 typedef void (*clean_leaf_fct_t)(pt_leaf_t);
 /*! \brief Function pointer to a function that prints the content of a leaf. */
 typedef void (*print_leaf_fct_t)(pt_leaf_t);
+/*! \brief Function pointer to a predicate function that returns true (!= 0) or
+    false (== 0) for a given leaf. */
+typedef int (*pt_predicate_t)(pt_leaf_t leaf);
 
 /*! \brief Opaque structure of a patricia trie. */
 typedef struct pt_struct pt_struct_t;
@@ -92,6 +95,16 @@ void pt_insert(pt_struct_t *pt, pt_leaf_t leaf);
   @ assigns *pt \from *pt, leaf, indirect:__fc_heap_status; */
 void pt_remove(pt_struct_t *pt, pt_leaf_t leaf);
 
+/*! \brief Remove all leaves that satisfy the given predicate from the patricia
+    trie.
+    \param pt Patricia trie to update.
+    \param predicate Predicate to test the leaves of the trie. */
+/*@ requires \valid(pt);
+  @ requires \valid_function(pt_predicate_t predicate);
+  @ assigns __fc_heap_status \from __fc_heap_status;
+  @ assigns *pt \from *pt, indirect:predicate, indirect:__fc_heap_status; */
+void pt_remove_if(pt_struct_t *pt, pt_predicate_t predicate);
+
 /*! \brief Look for the leaf representing exactly the given pointer.
 
     Given the function `get_fct_ptr` provided at the trie creation and a leaf
@@ -119,6 +132,15 @@ pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr);
   @ assigns \result \from *pt, indirect:ptr; */
 pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr);
 
+/*! \brief Look for the first leaf that satisfies the given predicate.
+    \param pt Patricia trie where to look for.
+    \param predicate Predicate to test the leaves of the trie.
+    \return The first leaf satisfying the given predicate. */
+/*@ requires \valid_read(pt);
+  @ requires \valid_function(pt_predicate_t predicate);
+  @ assigns \result \from *pt, indirect:predicate; */
+pt_leaf_t pt_find_if(const pt_struct_t *pt, pt_predicate_t predicate);
+
 /*! \brief Clean the content of the given patricia trie.
 
     Contrary to `pt_destroy()`, this function removes all leaves of the trie but