First step towards replace_all operations

README.md

@@ -19,7 +19,7 @@ For a brief overview of the architecture, see [SMT-COMP'24 Z3-Noodler descriptio
 
 ### Dependencies
 
-1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.10`.
+1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.7.6`.
     ```shell
     git clone 'https://github.com/VeriFIT/mata.git'
     cd mata

src/smt/theory_str_noodler/formula.cpp

@@ -190,7 +190,7 @@ namespace smt::noodler {
     }
 
     std::set<BasicTerm> Predicate::get_side_vars(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         std::set<BasicTerm> vars;
         std::vector<BasicTerm> side_terms;
         switch (side) {
@@ -221,7 +221,7 @@ namespace smt::noodler {
     }
 
     bool Predicate::mult_occurr_var_side(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         const auto terms_begin{ get_side(side).cbegin() };
         const auto terms_end{ get_side(side).cend() };
         for (auto term_iter{ terms_begin }; term_iter < terms_end; ++term_iter) {
@@ -262,40 +262,39 @@ namespace smt::noodler {
     }
 
     std::string Predicate::to_string() const {
+
+        // joining BasicTerm in the given vector with str
+        auto join = [&](const std::vector<BasicTerm>& vec, const std::string& str) -> std::string {
+            if(vec.empty()) return "";
+            std::string ret = vec[0].to_string();
+            for(size_t i = 1; i < vec.size(); i++) {
+                ret += str + vec[i].to_string();
+            }
+            return ret;
+        };
+
         switch (type) {
             case PredicateType::Equation: {
-                std::string result{ "Equation:" };
-                for (const auto& item: get_left_side()) {
-                    result += " " + item.to_string();
-                }
-                result += " =";
-                for (const auto& item: get_right_side()) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Equation: " };
+                result += join(get_left_side(), " ") + " = " + join(get_right_side(), " ");
                 return result;
             }
 
             case PredicateType::Inequation: {
-                std::string result{ "Inequation:" };
-                for (const auto& item: get_left_side()) {
-                    result += " " + item.to_string();
-                }
-                result += " !=";
-                for (const auto& item: get_right_side()) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Inequation: " };
+                result += join(get_left_side(), " ") + " != " + join(get_right_side(), " ");
                 return result;
             }
 
             case PredicateType::NotContains: {
-                std::string result{ "Notcontains " };
-                for (const auto& item: params[0]) {
-                    result += " " + item.to_string();
-                }
-                result += " ,";
-                for (const auto& item: params[1]) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Notcontains: " };
+                result += join(params[0], " ") + " , " + join(params[1], " ");
+                return result;
+            }
+
+            case PredicateType::Transducer: {
+                std::string result{ "Transducer: " };
+                result += join(params[0], " ") + " , " + join(params[1], " ");
                 return result;
             }
         }
@@ -305,16 +304,40 @@ namespace smt::noodler {
 
     bool Predicate::equals(const Predicate &other) const {
         if (type == other.type) {
+            if(is_transducer()) {
+                if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
+                    return false;
+                }
+                // check if transducers are the same pointers
+                return transducer == other.transducer;
+            }
+            if (is_two_sided()) {
+                return params[0] == other.params[0] && params[1] == other.params[1];
+            }
+            return params == other.params;
+        }
+        return false;
+    }
+
+    bool Predicate::strong_equals(const Predicate& other) const {
+        if (type == other.type) {
+            if(is_transducer()) {
+                if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
+                    return false;
+                }
+                // check if transducers are the same pointers
+                return transducer->is_identical(*other.get_transducer());
+            }
             if (is_two_sided()) {
                 return params[0] == other.params[0] && params[1] == other.params[1];
             }
-            return true;
+            return params == other.params;
         }
         return false;
     }
 
     const std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         switch (side) {
             case EquationSideType::Left:
                 return params[0];
@@ -329,7 +352,7 @@ namespace smt::noodler {
     }
 
     std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         switch (side) {
             case EquationSideType::Left:
                 return params[0];

src/smt/theory_str_noodler/formula.h

@@ -24,6 +24,7 @@
 #include <map>
 #include <unordered_set>
 #include <iostream>
+#include <mata/nft/nft.hh>
 
 #include "util/zstring.h"
 #include "ast/ast.h"
@@ -35,6 +36,7 @@ namespace smt::noodler {
         Equation,
         Inequation,
         NotContains,
+        Transducer, 
     };
 
     [[nodiscard]] static std::string to_string(PredicateType predicate_type) {
@@ -45,6 +47,8 @@ namespace smt::noodler {
                 return "Inequation";
             case PredicateType::NotContains:
                 return "Notcontains";
+            case PredicateType::Transducer:
+                return "Transducer";
         }
 
         throw std::runtime_error("Unhandled predicate type passed to to_string().");
@@ -290,7 +294,7 @@ namespace smt::noodler {
         };
 
         Predicate() : type(PredicateType::Equation) {}
-        explicit Predicate(const PredicateType type): type(type) {
+        explicit Predicate(const PredicateType type): type(type), params(), transducer() {
             if (is_equation() || is_inequation()) {
                 params.resize(2);
                 params.emplace_back();
@@ -300,15 +304,25 @@ namespace smt::noodler {
 
         explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par):
             type(type),
-            params(par)
+            params(par),
+            transducer()
             { }
 
+        explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par, std::shared_ptr<mata::nft::Nft> trans) : 
+            type(type),
+            params(par),
+            transducer(trans) {
+            assert(type == PredicateType::Transducer);
+            assert(trans->num_of_levels == 2);
+        }
+
         [[nodiscard]] PredicateType get_type() const { return type; }
         [[nodiscard]] bool is_equation() const { return type == PredicateType::Equation; }
         [[nodiscard]] bool is_inequation() const { return type == PredicateType::Inequation; }
         [[nodiscard]] bool is_not_cont() const { return type == PredicateType::NotContains; }
         [[nodiscard]] bool is_eq_or_ineq() const { return is_equation() || is_inequation(); }
-        [[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont(); }
+        [[nodiscard]] bool is_transducer() const { return is(PredicateType::Transducer); }
+        [[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont() || is_transducer(); }
         [[nodiscard]] bool is_predicate() const { return !is_eq_or_ineq(); }
         [[nodiscard]] bool is(const PredicateType predicate_type) const { return predicate_type == this->type; }
 
@@ -364,15 +378,15 @@ namespace smt::noodler {
         }
 
         std::set<BasicTerm> get_left_set() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
             std::set<BasicTerm> ret;
             for(const BasicTerm& t : this->params[0])
                 ret.insert(t);
             return ret;
         }
 
         std::set<BasicTerm> get_right_set() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
             std::set<BasicTerm> ret;
             for(const BasicTerm& t : this->params[1])
                 ret.insert(t);
@@ -413,6 +427,7 @@ namespace smt::noodler {
                 return LenNode(LenFormulaType::PLUS, ops);
             };
 
+            assert(is_eq_or_ineq());
             LenNode left = plus_chain(this->params[0]);
             LenNode right = plus_chain(this->params[1]);
             LenNode eq = LenNode(LenFormulaType::EQ, {left, right});
@@ -429,7 +444,12 @@ namespace smt::noodler {
         [[nodiscard]] const std::vector<BasicTerm>& get_side(EquationSideType side) const;
 
         [[nodiscard]] Predicate get_switched_sides_predicate() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
+            // for transducers we need to invert tapes, i.e., T(x,y) iff T^{-1}(y,x)
+            if(is_transducer()) {
+                auto nft_inverse = std::make_shared<mata::nft::Nft>(mata::nft::invert_levels(*transducer));
+                return Predicate{ PredicateType::Transducer, { get_right_side(), get_left_side() }, nft_inverse };
+            }
             return Predicate{ type, { get_right_side(), get_left_side() } };
         }
 
@@ -479,6 +499,7 @@ namespace smt::noodler {
                 modif = modif || r;
             }
             res = Predicate(this->type, new_params);
+            res.transducer = this->transducer;
             return modif;
         }
 
@@ -530,29 +551,47 @@ namespace smt::noodler {
 
         [[nodiscard]] bool equals(const Predicate& other) const;
 
+        /**
+         * @brief Strong equality. For the case of transducer predicates the transducers
+         * are compared for identity (not just the indentity of pointers). It is 
+         * necessary for the inclusion graph handling where we require get_switched_side
+         * (get_swithch_side(x)) == x (which is not true for pointer comparison).
+         * 
+         * @param other Other predicate
+         * @return true Is strongly equal
+         */
+        bool strong_equals(const Predicate& other) const;
+
         [[nodiscard]] std::string to_string() const;
 
         struct HashFunction {
             size_t operator()(const Predicate& predicate) const {
                 size_t res{};
                 size_t row_hash = std::hash<PredicateType>()(predicate.type);
-                for (const auto& term: predicate.get_left_side()) {
-                    size_t col_hash = BasicTerm::HashFunction()(term) << 1;
-                    res ^= col_hash;
-                }
-                for (const auto& term: predicate.get_right_side()) {
-                    size_t col_hash = BasicTerm::HashFunction()(term) << 1;
-                    res ^= col_hash;
+                for(const auto& pr : predicate.get_params()) {
+                    for(const BasicTerm& term : pr) {
+                        size_t col_hash = BasicTerm::HashFunction()(term) << 1;
+                        res ^= col_hash;
+                    }
                 }
                 return row_hash ^ res;
             }
         };
 
-        // TODO: Additional operations.
+        /**
+         * @brief Get the transducer shared pointer (for the transducer predicates only).
+         * 
+         * @return std::shared_ptr<mata::nft::Nft> Transducer
+         */
+        const std::shared_ptr<mata::nft::Nft>& get_transducer() const {
+            assert(is_transducer());
+            return transducer;
+        }
 
     private:
         PredicateType type;
         std::vector<std::vector<BasicTerm>> params;
+        std::shared_ptr<mata::nft::Nft> transducer; // transducer for the case of PredicateType::Transducer
 
         // TODO: Add additional attributes such as cost, etc.
     }; // Class Predicate.
@@ -578,9 +617,14 @@ namespace smt::noodler {
         if (lhs.get_params() < rhs.get_params()) {
             return true;
         }
+        // For transducer predicates we compare pointers (assuming linear memory model)
+        if (lhs.is_transducer()) {
+            // compare pointers
+            return lhs.get_transducer() < rhs.get_transducer();
+        }
         return false;
     }
-    static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs); }
+    static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs) && lhs != rhs; }
 
     //----------------------------------------------------------------------------------------------------------------------------------
 

src/smt/theory_str_noodler/formula_preprocess.cpp

@@ -187,7 +187,7 @@ namespace smt::noodler {
     void FormulaVar::remove_predicate(size_t index) {
         std::set<BasicTerm> items = this->predicates[index].get_set();
 
-        const auto& filter = [&index](const VarNode& n) { return n.eq_index == index; };
+        const auto& filter = [&index](const VarNode& n) { return n.pred_index == index; };
         for(const BasicTerm& v : items) {
             std::set<VarNode>& occurr = this->varmap[v];
             remove_if(occurr, filter);
@@ -367,10 +367,10 @@ namespace smt::noodler {
             std::set<VarNode> occurrs = this->formula.get_var_occurr(left_var);
             if(occurrs.size() == 1) {
                 Predicate reg_pred;
-                if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->eq_index), reg_pred)) {
-                    worklist.emplace_back(occurrs.begin()->eq_index, reg_pred);
+                if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->pred_index), reg_pred)) {
+                    worklist.emplace_back(occurrs.begin()->pred_index, reg_pred);
                     // update dependency
-                    map_set_insert(this->dependency, occurrs.begin()->eq_index, pr.first);
+                    map_set_insert(this->dependency, occurrs.begin()->pred_index, pr.first);
                 }
             }
         }
@@ -625,7 +625,7 @@ namespace smt::noodler {
             // Get all occurrences of t
             std::set<VarNode> occurrs = this->formula.get_var_occurr(t);
             // Get predicate of a first equation containing t; and side containing t
-            Predicate act_pred = this->formula.get_predicate(occurrs.begin()->eq_index);
+            Predicate act_pred = this->formula.get_predicate(occurrs.begin()->pred_index);
             Concat side = occurrs.begin()->position > 0 ? act_pred.get_right_side() : act_pred.get_left_side();
 
             int start = std::abs(occurrs.begin()->position) - 1;
@@ -635,7 +635,7 @@ namespace smt::noodler {
                 for(const VarNode& vn : occurrs) {
                     vns.insert({
                         side[i],
-                        vn.eq_index,
+                        vn.pred_index,
                         FormulaVar::increment_side_index(vn.position, i-start)
                     });
                 }
@@ -728,7 +728,7 @@ namespace smt::noodler {
         for(const BasicTerm& t : eps_set) {
             std::set<VarNode> nds = get_formula().get_var_occurr(t);
             std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
-                [](const VarNode& n){ return n.eq_index ; });
+                [](const VarNode& n){ return n.pred_index ; });
         }
 
         while(!worklist.empty()) {
@@ -757,7 +757,7 @@ namespace smt::noodler {
                 eps_set.insert(t);
                 std::set<VarNode> nds = get_formula().get_var_occurr(t);
                 std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
-                    [](const VarNode& n){ return n.eq_index ; });
+                    [](const VarNode& n){ return n.pred_index ; });
             }
         }