From 564678dae9b30b7c68979f486beea974fa116ec2 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 9 Feb 2025 21:18:59 +0100 Subject: [PATCH 01/15] formula: basic transducer and replace_alls support --- src/smt/theory_str_noodler/formula.cpp | 55 +++++++++++-------- src/smt/theory_str_noodler/formula.h | 41 ++++++++++---- src/smt/theory_str_noodler/inclusion_graph.cc | 1 + 3 files changed, 65 insertions(+), 32 deletions(-) diff --git a/src/smt/theory_str_noodler/formula.cpp b/src/smt/theory_str_noodler/formula.cpp index 9d7ae7030c6..9b0809ad25c 100644 --- a/src/smt/theory_str_noodler/formula.cpp +++ b/src/smt/theory_str_noodler/formula.cpp @@ -262,40 +262,51 @@ namespace smt::noodler { } std::string Predicate::to_string() const { + + // joining BasicTerm in the given vector with str + auto join = [&](const std::vector& 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(); - } + 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(); - } + 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(); - } + 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; + } + + case PredicateType::ReplaceAll: { + std::string result{ "ReplaceAll " }; + result += join(params[0], " ") + " = replace_all( " + join(params[1], " ") + ", " + join(params[2], " ") + ", " + join(params[3], " ") + ")"; + return result; + } + + case PredicateType::ReplaceREAll: { + std::string result{ "ReplaceREAll " }; + result += join(params[0], " ") + " = replace_re_all( " + join(params[1], " ") + ", " + join(params[2], " ") + ", " + join(params[3], " ") + ")"; return result; } } @@ -308,7 +319,7 @@ namespace smt::noodler { if (is_two_sided()) { return params[0] == other.params[0] && params[1] == other.params[1]; } - return true; + return params == other.params; } return false; } diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 4e196ce0cd8..0148dd75776 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -24,6 +24,7 @@ #include #include #include +#include #include "util/zstring.h" #include "ast/ast.h" @@ -35,6 +36,9 @@ namespace smt::noodler { Equation, Inequation, NotContains, + ReplaceAll, // params[0] = replace_all params[1] params[2] params[3] + ReplaceREAll, // params[0] = replace_re_all params[1] params[2] params[3] (params[2] is a basic term representing matching RE) + Transducer, }; [[nodiscard]] static std::string to_string(PredicateType predicate_type) { @@ -45,6 +49,12 @@ namespace smt::noodler { return "Inequation"; case PredicateType::NotContains: return "Notcontains"; + case PredicateType::ReplaceAll: + return "ReplaceAll"; + case PredicateType::ReplaceREAll: + return "ReplaceREAll"; + case PredicateType::Transducer: + return "Transducer"; } throw std::runtime_error("Unhandled predicate type passed to to_string()."); @@ -290,7 +300,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 +310,26 @@ namespace smt::noodler { explicit Predicate(const PredicateType type, std::vector> par): type(type), - params(par) + params(par), + transducer() { } + explicit Predicate(const PredicateType type, std::vector> par, std::shared_ptr trans) : + type(type), + params(par), + transducer(trans) { + assert(type == PredicateType::Transducer); + } + [[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_replace_all() const { return is(PredicateType::ReplaceAll); } + [[nodiscard]] bool is_replace_re_all() const { return is(PredicateType::ReplaceREAll); } + [[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; } @@ -413,6 +434,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}); @@ -536,13 +558,11 @@ namespace smt::noodler { size_t operator()(const Predicate& predicate) const { size_t res{}; size_t row_hash = std::hash()(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; } @@ -553,6 +573,7 @@ namespace smt::noodler { private: PredicateType type; std::vector> params; + std::shared_ptr transducer; // transducer for the case of PredicateType::Transducer // TODO: Add additional attributes such as cost, etc. }; // Class Predicate. diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc index ca6a3ea2999..93618e15651 100644 --- a/src/smt/theory_str_noodler/inclusion_graph.cc +++ b/src/smt/theory_str_noodler/inclusion_graph.cc @@ -29,6 +29,7 @@ namespace { case PredicateType::NotContains: { util::throw_error("Decision procedure can handle only equations and disequations"); } + // TODO: handle transducers case PredicateType::Equation: case PredicateType::Inequation: { std::string left_side{}; From 3955d3b6e1205f2f59a0c0b3088baa02848bda0c Mon Sep 17 00:00:00 2001 From: vhavlena Date: Tue, 11 Feb 2025 17:11:12 +0100 Subject: [PATCH 02/15] formula: remove replace_alls; operations with transducer predicate --- src/smt/theory_str_noodler/formula.cpp | 28 ++++++++------------------ src/smt/theory_str_noodler/formula.h | 20 +++++++++--------- 2 files changed, 17 insertions(+), 31 deletions(-) diff --git a/src/smt/theory_str_noodler/formula.cpp b/src/smt/theory_str_noodler/formula.cpp index 9b0809ad25c..96b654c5a98 100644 --- a/src/smt/theory_str_noodler/formula.cpp +++ b/src/smt/theory_str_noodler/formula.cpp @@ -190,7 +190,7 @@ namespace smt::noodler { } std::set Predicate::get_side_vars(const Predicate::EquationSideType side) const { - assert(is_eq_or_ineq()); + assert(is_two_sided()); std::set vars; std::vector 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) { @@ -275,40 +275,28 @@ namespace smt::noodler { switch (type) { case PredicateType::Equation: { - std::string result{ "Equation:" }; + std::string result{ "Equation: " }; result += join(get_left_side(), " ") + " = " + join(get_right_side(), " "); return result; } case PredicateType::Inequation: { - std::string result{ "Inequation:" }; + std::string result{ "Inequation: " }; result += join(get_left_side(), " ") + " != " + join(get_right_side(), " "); return result; } case PredicateType::NotContains: { - std::string result{ "Notcontains " }; + std::string result{ "Notcontains: " }; result += join(params[0], " ") + " , " + join(params[1], " "); return result; } case PredicateType::Transducer: { - std::string result{ "Transducer " }; + std::string result{ "Transducer: " }; result += join(params[0], " ") + " , " + join(params[1], " "); return result; } - - case PredicateType::ReplaceAll: { - std::string result{ "ReplaceAll " }; - result += join(params[0], " ") + " = replace_all( " + join(params[1], " ") + ", " + join(params[2], " ") + ", " + join(params[3], " ") + ")"; - return result; - } - - case PredicateType::ReplaceREAll: { - std::string result{ "ReplaceREAll " }; - result += join(params[0], " ") + " = replace_re_all( " + join(params[1], " ") + ", " + join(params[2], " ") + ", " + join(params[3], " ") + ")"; - return result; - } } throw std::runtime_error("Unhandled predicate type passed as 'this' to to_string()."); @@ -325,7 +313,7 @@ namespace smt::noodler { } const std::vector &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]; @@ -340,7 +328,7 @@ namespace smt::noodler { } std::vector &Predicate::get_side(const Predicate::EquationSideType side) { - assert(is_eq_or_ineq()); + assert(is_two_sided()); switch (side) { case EquationSideType::Left: return params[0]; diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 0148dd75776..6aeafeab991 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -36,8 +36,6 @@ namespace smt::noodler { Equation, Inequation, NotContains, - ReplaceAll, // params[0] = replace_all params[1] params[2] params[3] - ReplaceREAll, // params[0] = replace_re_all params[1] params[2] params[3] (params[2] is a basic term representing matching RE) Transducer, }; @@ -49,10 +47,6 @@ namespace smt::noodler { return "Inequation"; case PredicateType::NotContains: return "Notcontains"; - case PredicateType::ReplaceAll: - return "ReplaceAll"; - case PredicateType::ReplaceREAll: - return "ReplaceREAll"; case PredicateType::Transducer: return "Transducer"; } @@ -318,6 +312,7 @@ namespace smt::noodler { type(type), params(par), transducer(trans) { + // TODO: add check that we use only two-tape transducers assert(type == PredicateType::Transducer); } @@ -327,8 +322,6 @@ namespace smt::noodler { [[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_transducer() const { return is(PredicateType::Transducer); } - [[nodiscard]] bool is_replace_all() const { return is(PredicateType::ReplaceAll); } - [[nodiscard]] bool is_replace_re_all() const { return is(PredicateType::ReplaceREAll); } [[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; } @@ -385,7 +378,7 @@ namespace smt::noodler { } std::set get_left_set() const { - assert(is_eq_or_ineq()); + assert(is_two_sided()); std::set ret; for(const BasicTerm& t : this->params[0]) ret.insert(t); @@ -393,7 +386,7 @@ namespace smt::noodler { } std::set get_right_set() const { - assert(is_eq_or_ineq()); + assert(is_two_sided()); std::set ret; for(const BasicTerm& t : this->params[1]) ret.insert(t); @@ -451,7 +444,12 @@ namespace smt::noodler { [[nodiscard]] const std::vector& 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::invert_levels(*transducer)); + return Predicate{ PredicateType::Transducer, { get_right_side(), get_left_side() }, nft_inverse }; + } return Predicate{ type, { get_right_side(), get_left_side() } }; } From ee2c3d04203d20b8fbd8dd194beee4a6ad728c95 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 13 Feb 2025 12:19:10 +0100 Subject: [PATCH 03/15] inclusion graph: transducer constraints support --- src/smt/theory_str_noodler/formula.cpp | 7 ++ src/smt/theory_str_noodler/formula.h | 23 ++++- src/smt/theory_str_noodler/inclusion_graph.cc | 36 +++++--- src/test/noodler/CMakeLists.txt | 1 + src/test/noodler/formula.cpp | 71 +++++++++++++++ src/test/noodler/inclusion-graph-node.cc | 91 +++++++++++++++++++ 6 files changed, 212 insertions(+), 17 deletions(-) create mode 100644 src/test/noodler/formula.cpp diff --git a/src/smt/theory_str_noodler/formula.cpp b/src/smt/theory_str_noodler/formula.cpp index 96b654c5a98..db2922c59e1 100644 --- a/src/smt/theory_str_noodler/formula.cpp +++ b/src/smt/theory_str_noodler/formula.cpp @@ -304,6 +304,13 @@ 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 identical (cheaper than equivalence check, which might be too strong for this purpose) + return transducer->is_identical(*other.transducer); + } if (is_two_sided()) { return params[0] == other.params[0] && params[1] == other.params[1]; } diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 6aeafeab991..5ca7cfb69e3 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -312,8 +312,8 @@ namespace smt::noodler { type(type), params(par), transducer(trans) { - // TODO: add check that we use only two-tape transducers assert(type == PredicateType::Transducer); + assert(trans->num_of_levels == 2); } [[nodiscard]] PredicateType get_type() const { return type; } @@ -566,7 +566,15 @@ namespace smt::noodler { } }; - // TODO: Additional operations. + /** + * @brief Get the transducer shared pointer (for the transducer predicates only). + * + * @return std::shared_ptr Transducer + */ + const std::shared_ptr& get_transducer() const { + assert(is_transducer()); + return transducer; + } private: PredicateType type; @@ -597,9 +605,18 @@ 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()) { + // if we have the same object stored on two different places + if (lhs.get_transducer()->is_identical(*rhs.get_transducer())) { + return false; + } + // 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; } //---------------------------------------------------------------------------------------------------------------------------------- diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc index 93618e15651..822b93adb56 100644 --- a/src/smt/theory_str_noodler/inclusion_graph.cc +++ b/src/smt/theory_str_noodler/inclusion_graph.cc @@ -23,26 +23,34 @@ namespace { * @return String representation of @p node. */ std::string conv_node_to_string(const std::shared_ptr& node) { + // joining BasicTerm in the given vector with str + auto join = [&](const std::vector& 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; + }; + auto& predicate{ node->get_predicate() }; std::string result{}; switch (predicate.get_type()) { case PredicateType::NotContains: { util::throw_error("Decision procedure can handle only equations and disequations"); } - // TODO: handle transducers + + case PredicateType::Transducer: { + std::string left_side = join(predicate.get_left_side(), " "); + std::string right_side = join(predicate.get_right_side(), " "); + result = "T(" + left_side + ", " + right_side + ")"; + break; + } + case PredicateType::Equation: case PredicateType::Inequation: { - std::string left_side{}; - for (auto& item : predicate.get_left_side()) { - if (!left_side.empty()) { left_side += " "; } - left_side += item.to_string(); - } - - std::string right_side{}; - for (auto& item : predicate.get_right_side()) { - if (!right_side.empty()) { right_side += " "; } - right_side += item.to_string(); - } + std::string left_side = join(predicate.get_left_side(), " "); + std::string right_side = join(predicate.get_right_side(), " "); result = left_side; if (predicate.get_type() == PredicateType::Inequation) { result += " !"; @@ -159,7 +167,7 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form // Add all nodes which are not already present in direct and switched form. for (const auto& predicate: formula.get_predicates()) { // we skip trivial equations of the form x = x - if(predicate.get_left_side() == predicate.get_right_side()) { + if(!predicate.is_transducer() && predicate.get_left_side() == predicate.get_right_side()) { continue; } graph.add_node(predicate); @@ -184,7 +192,7 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form } else if (source_left_side == target_right_side) { // Have same var and sides are equal. - if (source_right_side == target_left_side) { // In the same equation. + if (source_predicate == target_predicate.get_switched_sides_predicate()) { // In the same reversed predicate. if (!source_predicate.mult_occurr_var_side(Predicate::EquationSideType::Left)) { // Does not have multiple occurrences of one var. Hence, cannot have an edge. continue; diff --git a/src/test/noodler/CMakeLists.txt b/src/test/noodler/CMakeLists.txt index a422e9d444d..3a2bd23cda7 100644 --- a/src/test/noodler/CMakeLists.txt +++ b/src/test/noodler/CMakeLists.txt @@ -20,6 +20,7 @@ if (Catch2_FOUND) decision-procedure.cpp parikh.cc util.cc + formula.cpp ) find_library(LIBMATA mata) diff --git a/src/test/noodler/formula.cpp b/src/test/noodler/formula.cpp new file mode 100644 index 00000000000..f21aea6d8eb --- /dev/null +++ b/src/test/noodler/formula.cpp @@ -0,0 +1,71 @@ +#include +#include + +#include +#include +#include + +#include "smt/theory_str_noodler/formula.h" + +using namespace smt::noodler; + + +TEST_CASE( "Transducer predicate", "[noodler]" ) { + + // two-tape transducer by default + mata::nft::Nft nft{2}; + nft.initial = {0}; + nft.final = {1}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + CHECK(nft.delta.num_of_states() == 3); + CHECK(nft.is_tuple_in_lang({ {'a'}, {'b'} })); + + BasicTerm x {BasicTermType::Variable, "x"}; + BasicTerm y {BasicTermType::Variable, "x"}; + + SECTION("Switched predicate") { + // transducer implementing inversion relation + mata::nft::Nft nft_inv = mata::nft::invert_levels(nft); + CHECK(nft_inv.is_tuple_in_lang({ {'b'}, {'a'} })); + CHECK(!nft_inv.is_tuple_in_lang({ {'a'}, {'b'} })); + + Predicate pred_trans { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; + Predicate pred_trans_switch = pred_trans.get_switched_sides_predicate(); + + // result + Predicate switch_res { PredicateType::Transducer, { { y }, { x } }, std::make_shared(nft_inv) }; + CHECK(pred_trans_switch == switch_res); + } + + SECTION("Comparison") { + mata::nft::Nft nft_other{2}; + nft_other.initial = {0}; + nft_other.final = {1}; + nft_other.insert_word_by_parts(0, { {'c'}, {'d'} } , 1); + + + Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; + Predicate p2 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft_other) }; + Predicate p3 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; + CHECK(p1 != p2); + CHECK(!(p1 < p1)); + CHECK(p1 == p1); + CHECK(p1 == p3); + CHECK(!(p1 < p3)); + CHECK(!(p3 < p1)); + + std::set st{}; + st.insert(p1); + st.insert(p2); + st.insert(p3); + CHECK(st.size() == 2); + + std::unordered_set st_un{}; + st_un.insert(p1); + st_un.insert(p2); + st_un.insert(p3); + CHECK(st_un.size() == 2); + } + + +} \ No newline at end of file diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc index 13e9573ca18..c656aa03116 100644 --- a/src/test/noodler/inclusion-graph-node.cc +++ b/src/test/noodler/inclusion-graph-node.cc @@ -2,6 +2,7 @@ #include #include +#include #include "smt/theory_str_noodler/inclusion_graph.h" @@ -360,3 +361,93 @@ TEST_CASE("print_to_dot()") { graph.print_to_dot(stream); CHECK(!stream.str().empty()); } + +TEST_CASE("Inclusion graph with transducers", "[noodler]") { + Graph graph; + Formula formula; + + BasicTerm u{ BasicTermType::Variable, "u" }; + BasicTerm v{ BasicTermType::Variable, "v" }; + BasicTerm x{ BasicTermType::Variable, "x" }; + BasicTerm y{ BasicTermType::Variable, "y" }; + BasicTerm z{ BasicTermType::Variable, "z" }; + + mata::nft::Nft nft1{2}; + nft1.initial = {0}; + nft1.final = {1}; + nft1.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + + mata::nft::Nft nft2{2}; + nft2.initial = {0}; + nft2.final = {1}; + nft2.insert_word_by_parts(0, { {'c'}, {'d'} } , 1); + + + SECTION("T(x,y) && S(zz,yu)") { + Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft1) }; + Predicate p2{ PredicateType::Transducer, { { z, z }, { y, u } }, std::make_shared(nft2) }; + + Formula formula; + formula.add_predicate(p1); + formula.add_predicate(p2); + graph = Graph::create_inclusion_graph(formula); + + CHECK(graph.get_nodes().size() == 2); + CHECK(graph.get_num_of_edges() == 1); + CHECK(!graph.is_cyclic()); + } + + SECTION("x=y && T(zz,yu)") { + Predicate p1{ PredicateType::Equation, { { x }, { y } } }; + Predicate p2{ PredicateType::Transducer, { { z, z }, { y, u } }, std::make_shared(nft2) }; + + Formula formula; + formula.add_predicate(p1); + formula.add_predicate(p2); + graph = Graph::create_inclusion_graph(formula); + + CHECK(graph.get_nodes().size() == 2); + CHECK(graph.get_num_of_edges() == 1); + CHECK(!graph.is_cyclic()); + } + + SECTION("T(x,x)") { + Predicate p1{ PredicateType::Transducer, { { x }, { x } }, std::make_shared(nft2) }; + + Formula formula; + formula.add_predicate(p1); + graph = Graph::create_inclusion_graph(formula); + + CHECK(graph.get_nodes().size() == 2); + CHECK(graph.get_num_of_edges() == 2); + CHECK(graph.is_cyclic()); + } + + SECTION("T(x,y) && x=y") { + Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft2) }; + Predicate p2{ PredicateType::Equation, { { x }, { y } } }; + + Formula formula; + formula.add_predicate(p1); + formula.add_predicate(p2); + graph = Graph::create_inclusion_graph(formula); + + CHECK(graph.get_nodes().size() == 4); + CHECK(graph.get_num_of_edges() == 8); + CHECK(graph.is_cyclic()); + } + + SECTION("T(x,y) && x=z") { + Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft2) }; + Predicate p2{ PredicateType::Equation, { { x }, { z } } }; + + Formula formula; + formula.add_predicate(p1); + formula.add_predicate(p2); + graph = Graph::create_inclusion_graph(formula); + + CHECK(graph.get_nodes().size() == 2); + CHECK(graph.get_num_of_edges() == 1); + CHECK(!graph.is_cyclic()); + } +} \ No newline at end of file From 17e2a185470593c3f3f65f39a6b394605acb71e3 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 13 Feb 2025 14:10:52 +0100 Subject: [PATCH 04/15] preprocess: transducer constraint support --- src/smt/theory_str_noodler/formula.h | 1 + .../theory_str_noodler/formula_preprocess.cpp | 16 +-- .../theory_str_noodler/formula_preprocess.h | 12 +- src/test/noodler/formula-preprocess.cpp | 132 +++++++++++++++--- src/test/noodler/formula.cpp | 19 ++- 5 files changed, 145 insertions(+), 35 deletions(-) diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 5ca7cfb69e3..847c43b54ab 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -499,6 +499,7 @@ namespace smt::noodler { modif = modif || r; } res = Predicate(this->type, new_params); + res.transducer = this->transducer; return modif; } diff --git a/src/smt/theory_str_noodler/formula_preprocess.cpp b/src/smt/theory_str_noodler/formula_preprocess.cpp index 18608f3724c..40f6ec4acc0 100644 --- a/src/smt/theory_str_noodler/formula_preprocess.cpp +++ b/src/smt/theory_str_noodler/formula_preprocess.cpp @@ -187,7 +187,7 @@ namespace smt::noodler { void FormulaVar::remove_predicate(size_t index) { std::set 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& occurr = this->varmap[v]; remove_if(occurr, filter); @@ -367,10 +367,10 @@ namespace smt::noodler { std::set 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 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 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 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 ; }); } } diff --git a/src/smt/theory_str_noodler/formula_preprocess.h b/src/smt/theory_str_noodler/formula_preprocess.h index 56fe0514691..a00db8a524b 100644 --- a/src/smt/theory_str_noodler/formula_preprocess.h +++ b/src/smt/theory_str_noodler/formula_preprocess.h @@ -196,33 +196,33 @@ namespace smt::noodler { */ struct VarNode { BasicTerm term; - size_t eq_index; + size_t pred_index; int position; - VarNode(BasicTerm term, const size_t eq_index, const int position): term{ std::move(term) }, eq_index{ eq_index }, position{ position } {} + VarNode(BasicTerm term, const size_t eq_index, const int position): term{ std::move(term) }, pred_index{ eq_index }, position{ position } {} VarNode(const VarNode& other) = default; VarNode(VarNode &&) = default; VarNode& operator=(const VarNode&) = default; bool operator==(const VarNode& other) const { - return term == other.term && eq_index == other.eq_index && position == other.position; + return term == other.term && pred_index == other.pred_index && position == other.position; } std::string to_string() const { std::string ret; - ret += "( " + term.to_string() + ";" + std::to_string(eq_index) + ";" + std::to_string(position) + ")"; + ret += "( " + term.to_string() + ";" + std::to_string(pred_index) + ";" + std::to_string(position) + ")"; return ret; }; }; inline bool operator<(const VarNode& lhs, const VarNode& rhs) { if(lhs.position == rhs.position) { - if(lhs.eq_index == rhs.eq_index) { + if(lhs.pred_index == rhs.pred_index) { if(lhs.term == rhs.term) return false; return lhs.term < rhs.term; } - return lhs.eq_index < rhs.eq_index; + return lhs.pred_index < rhs.pred_index; } return lhs.position < rhs.position; } diff --git a/src/test/noodler/formula-preprocess.cpp b/src/test/noodler/formula-preprocess.cpp index f72d63ace19..4d0d2b80727 100644 --- a/src/test/noodler/formula-preprocess.cpp +++ b/src/test/noodler/formula-preprocess.cpp @@ -5,6 +5,7 @@ #include #include #include +#include using namespace smt::noodler; @@ -273,33 +274,62 @@ TEST_CASE( "Propagate variables", "[noodler]" ) { {b, regex_to_nfa("b")}, }); + mata::nft::Nft nft{2}; + nft.initial = {0}; + nft.final = {1}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1, x1}), std::vector({x3, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x2}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); - Formula conj; - conj.add_predicate(eq1); - conj.add_predicate(ieq1); - conj.add_predicate(eq2); - conj.add_predicate(eq3); - FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); + Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); + Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x1}) }), std::make_shared(nft) ); - prep.propagate_variables(); - prep.clean_varmap(); - INFO(prep.to_string()); + SECTION("(In)equations") { + Formula conj; + conj.add_predicate(eq1); + conj.add_predicate(ieq1); + conj.add_predicate(eq2); + conj.add_predicate(eq3); + FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); - Formula res_conj; - res_conj.add_predicate(Predicate(PredicateType::Equation, std::vector>({ std::vector({a, x1, x4}), std::vector({b, x1, x1}) }))); - res_conj.add_predicate(Predicate(PredicateType::Inequation, std::vector>({ std::vector({x1, x1}), std::vector({x1, x1}) }))); - FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {}); + prep.propagate_variables(); + prep.clean_varmap(); + INFO(prep.to_string()); - AutAssignment ret = prep.get_aut_assignment(); - CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa(""))); - CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa("(a|b)*"))); - CHECK(mata::nfa::are_equivalent(*ret.at(x3), regex_to_nfa("(b|c)*"))); - CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap()); - CHECK(prep.get_formula().get_predicates_set() == prep_res.get_formula().get_predicates_set()); - CHECK(prep.get_dependency() == Dependency({{0, {2,3}}, {1, {2,3}}, {3, {2}}})); + Formula res_conj; + res_conj.add_predicate(Predicate(PredicateType::Equation, std::vector>({ std::vector({a, x1, x4}), std::vector({b, x1, x1}) }))); + res_conj.add_predicate(Predicate(PredicateType::Inequation, std::vector>({ std::vector({x1, x1}), std::vector({x1, x1}) }))); + FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {}); + + AutAssignment ret = prep.get_aut_assignment(); + CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa(""))); + CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa("(a|b)*"))); + CHECK(mata::nfa::are_equivalent(*ret.at(x3), regex_to_nfa("(b|c)*"))); + CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap()); + CHECK(prep.get_formula().get_predicates_set() == prep_res.get_formula().get_predicates_set()); + CHECK(prep.get_dependency() == Dependency({{0, {2,3}}, {1, {2,3}}, {3, {2}}})); + } + + SECTION("Transducers") { + Formula conj; + conj.add_predicate(tr1); + conj.add_predicate(eq3); + FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); + + prep.propagate_variables(); + prep.clean_varmap(); + INFO(prep.to_string()); + + Formula res_conj; + res_conj.add_predicate(tr2); + FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {}); + + CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap()); + CHECK(prep.get_modified_formula() == res_conj); + } + } TEST_CASE( "Remove duplicates", "[noodler]" ) { @@ -323,24 +353,33 @@ TEST_CASE( "Remove duplicates", "[noodler]" ) { {a, regex_to_nfa("a")}, {b, regex_to_nfa("b")}, }); + mata::nft::Nft nft{2}; + nft.initial = {0}; + nft.final = {1}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); Predicate ieq2(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); + Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); + Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); Formula conj; conj.add_predicate(eq1); conj.add_predicate(eq3); conj.add_predicate(ieq1); + conj.add_predicate(tr1); conj.add_predicate(eq2); conj.add_predicate(ieq2); + conj.add_predicate(tr2); FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); Formula res_conj; res_conj.add_predicate(eq1); res_conj.add_predicate(eq3); res_conj.add_predicate(ieq1); + res_conj.add_predicate(tr1); FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {}); INFO(prep.to_string()); @@ -374,6 +413,8 @@ TEST_CASE( "Sublists", "[noodler]" ) { Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4, b}), std::vector({x1, x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({b, x3, x4, b}), std::vector({x2, x1, x2}) }) ); + // transducer itself is not important for this case + Predicate tr2(PredicateType::Equation, std::vector>({ std::vector({b, x3, x4, b}), std::vector({x2, x1, x2}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, x1, x2}) }) ); Predicate eq4(PredicateType::Inequation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }) ); @@ -387,6 +428,16 @@ TEST_CASE( "Sublists", "[noodler]" ) { CHECK(res == std::map({ {std::vector({x3, x4, b}), 2} })); } + SECTION("sub1 with transducers") { + Formula conj; + conj.add_predicate(eq1); + conj.add_predicate(tr2); + FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); + std::map res; + prep.get_regular_sublists(res); + CHECK(res == std::map({ {std::vector({x3, x4, b}), 2} })); + } + SECTION("sub2") { Formula conj; std::map res; @@ -430,11 +481,16 @@ TEST_CASE( "Reduce regular", "[noodler]" ) { {b, regex_to_nfa("b")}, }); + mata::nft::Nft nft{2, {0}, {1}}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + Predicate eq1(PredicateType::Inequation, std::vector>({ std::vector({a, x3, x4, b}), std::vector({x1, x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x2, x1, x2}), std::vector({b, x3, x4, b}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, x1, x2}) }) ); Predicate eq4(PredicateType::Equation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }) ); + Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }), std::make_shared(nft) ); + SECTION("basic") { Formula conj; conj.add_predicate(eq1); @@ -491,6 +547,24 @@ TEST_CASE( "Reduce regular", "[noodler]" ) { CHECK(prep.get_dependency().empty()); CHECK(prep.get_flat_dependency().empty()); } + + SECTION("transducers") { + Formula conj; + conj.add_predicate(tr4); + FormulaPreprocessor prep(conj, aut_ass, {x2}, {}, {}); + prep.reduce_regular_sequence(1); + AutAssignment ret = prep.get_aut_assignment(); + + tmp0 = BasicTerm{BasicTermType::Variable, "regular_seq!n5"}; + tmp1 = BasicTerm{BasicTermType::Variable, "regular_seq!n6"}; + CHECK(mata::nfa::are_equivalent(*ret.at(tmp0), regex_to_nfa("b*ab"))); + CHECK(mata::nfa::are_equivalent(*ret.at(tmp1), regex_to_nfa("(a|b)*a*"))); + CHECK(prep.get_formula().get_predicates_set() == std::set({ + Predicate(PredicateType::Equation, std::vector>({ std::vector({tmp0}), std::vector({x4, a, b}) })), + Predicate(PredicateType::Transducer, std::vector>({ std::vector({tmp1}), std::vector({tmp0}) }), std::make_shared(nft) ), + Predicate(PredicateType::Equation, std::vector>({ std::vector({tmp1 }), std::vector({x5, x1, x2, x3}) }) ) + })); + } } TEST_CASE( "Propagate eps", "[noodler]" ) { @@ -515,11 +589,15 @@ TEST_CASE( "Propagate eps", "[noodler]" ) { {eps, regex_to_nfa("")}, }); + mata::nft::Nft nft{2, {0}, {1}}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({eps}), std::vector({x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x2, x1, x2}), std::vector({x3, x4}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x3, b, x4}), std::vector({x5, x1}) }) ); Predicate eq4(PredicateType::Equation, std::vector>({ std::vector({b, x1}), std::vector({eps}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({eps}) }) ); + Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1}), std::vector({x2}) }), std::make_shared(nft) ); SECTION("basic") { Formula conj; @@ -553,6 +631,20 @@ TEST_CASE( "Propagate eps", "[noodler]" ) { })); CHECK(prep.get_dependency() == Dependency({{0, {0}}})); } + + SECTION("transducer constraint") { + Formula conj; + conj.add_predicate(eq1); + conj.add_predicate(tr4); + FormulaPreprocessor prep(conj, aut_ass, {}, {}, {}); + prep.propagate_eps(); + AutAssignment ret = prep.get_aut_assignment(); + CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa(""))); + CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa(""))); + CHECK(prep.get_formula().get_predicates_set() == std::set({ + Predicate(PredicateType::Transducer, std::vector>({ std::vector({x5}), std::vector() }), std::make_shared(nft) ), + })); + } } TEST_CASE( "Separate eqs", "[noodler]" ) { diff --git a/src/test/noodler/formula.cpp b/src/test/noodler/formula.cpp index f21aea6d8eb..aa1e9fcb144 100644 --- a/src/test/noodler/formula.cpp +++ b/src/test/noodler/formula.cpp @@ -67,5 +67,22 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) { CHECK(st_un.size() == 2); } - + SECTION("Replace") { + mata::nft::Nft nft_other{2}; + nft_other.initial = {0}; + nft_other.final = {1}; + nft_other.insert_word_by_parts(0, { {'c'}, {'d'} } , 1); + + + Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; + Predicate pres { PredicateType::Transducer, { { x }, { x } }, std::make_shared(nft) }; + + Formula f{}; + f.add_predicate(p1); + f.replace({x}, {y}); + + Formula fres {}; + fres.add_predicate(pres); + CHECK(f == fres); + } } \ No newline at end of file From 6cacc38d10f2c05e79db997bf4847775577ff1d9 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 13 Feb 2025 16:20:41 +0100 Subject: [PATCH 05/15] integration: sketch of handling replace_all --- .../theory_str_noodler/theory_str_noodler.cpp | 27 +++++++++++- .../theory_str_noodler/theory_str_noodler.h | 3 ++ .../theory_str_noodler_final_check.cpp | 20 +++++++++ src/smt/theory_str_noodler/util.cc | 42 +++++++++++++++++++ src/smt/theory_str_noodler/util.h | 15 +++++++ 5 files changed, 106 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 25daa48520e..7c775a10961 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -399,7 +399,7 @@ namespace smt::noodler { } else if (m_util_s.str.is_replace(n)) { // str.replace handle_replace(n); } else if(m_util_s.str.is_replace_all(n)) { // str.replace_all - util::throw_error("str.replace_all is not supported"); + handle_replace_all(n); } else if(m_util_s.str.is_replace_re(n)) { // str.replace_re handle_replace_re(n); } else if(m_util_s.str.is_replace_re_all(n)) { // str.replace_re_all @@ -1502,6 +1502,31 @@ namespace smt::noodler { } } + /** + * @brief Handle replace_all. Just store the instance. It is solved using transducer + * constraints in the final_check. + * + * @param e replace_all + */ + void theory_str_noodler::handle_replace_all(expr *e) { + STRACE("str", tout << "handle-replace-all: " << mk_pp(e, m) << '\n';); + if (axiomatized_persist_terms.contains(e)) + return; + + axiomatized_persist_terms.insert(e); + + ast_manager &m = get_manager(); + expr *s = nullptr, *i = nullptr, *l = nullptr; + VERIFY(m_util_s.str.is_replace_all(e, s, i, l)); + + expr_ref v = mk_str_var_fresh("replace_all"); + // we need to store v into a storage. Since this->predicate_replace + // stores only pointers, the value v would cease to exist after end of + // handle_replace_all + this->trans_terms.push_back(v); + this->predicate_replace.insert(e, v.get()); + } + expr_ref theory_str_noodler::mk_concat(expr* e1, expr* e2) { return expr_ref(m_util_s.str.mk_concat(e1, e2), m); } diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index b8e9a6afbd0..e70c9b02b14 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -95,6 +95,8 @@ namespace smt::noodler { // mapping predicates and function to variables that they substitute to obj_map predicate_replace; + // mapping replace_all and replace_re_all to fresh variables + std::vector trans_terms; // TODO what are these? std::vector axiomatized_len_axioms; @@ -334,6 +336,7 @@ namespace smt::noodler { void handle_conversion(expr *e); void handle_lex_leq(expr *e); void handle_lex_lt(expr *e); + void handle_replace_all(expr *e); // methods for assigning boolean values to predicates void assign_not_contains(expr *e); diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index 149aadee571..56097b4b235 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -155,10 +155,15 @@ namespace smt::noodler { // Gather relevant word (dis)equations to noodler formula Formula instance = get_word_formula_from_relevant(); STRACE("str", + tout << std::endl; for(const auto& f : instance.get_predicates()) { tout << f.to_string() << std::endl; } ); + // decison procedure for transducer constraints is not implemented yet + if(instance.contains_pred_type(PredicateType::Transducer)) { + util::throw_error("transducer constraints are not supported"); + } // Gather symbols from relevant (dis)equations and from regular expressions of relevant memberships std::set symbols_in_formula = get_symbols_from_relevant(); @@ -478,14 +483,21 @@ namespace smt::noodler { Formula theory_str_noodler::get_word_formula_from_relevant() { Formula instance; + std::vector transducer_pred {}; for (const auto &we: this->m_word_eq_todo_rel) { Predicate inst = this->conv_eq_pred(ctx.mk_eq_atom(we.first, we.second)); + // gather transducer constraints occurring in the concatenation + util::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); instance.add_predicate(inst); } for (const auto& wd : this->m_word_diseq_todo_rel) { Predicate inst = this->conv_eq_pred(m.mk_not(ctx.mk_eq_atom(wd.first, wd.second))); + // gather transducer constraints occurring in the concatenation + util::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); instance.add_predicate(inst); } @@ -494,10 +506,18 @@ namespace smt::noodler { std::vector left, right; util::collect_terms(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, left); util::collect_terms(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, right); + // gather transducer constraints occurring in the concatenation + util::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); Predicate inst(PredicateType::NotContains, std::vector{left, right}); instance.add_predicate(inst); } + // add all transducer predicates + for(const auto& p : transducer_pred) { + instance.add_predicate(p); + } + return instance; } diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc index fe3a6d90242..cf6449a4373 100644 --- a/src/smt/theory_str_noodler/util.cc +++ b/src/smt/theory_str_noodler/util.cc @@ -82,6 +82,48 @@ namespace smt::noodler::util { return m_util_s.is_string(expression->get_sort()) && is_variable(expression); } + void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, std::vector& transducer_preds) { + if(m_util_s.str.is_string(ex) || is_variable(ex)) { // Handle string literals. + return; + } + + if(!m_util_s.str.is_concat(ex)) { + expr* rpl = pred_replace.find(ex); // dies if it is not found + // so-far we handle just replace_all + expr * a1 = nullptr, *a2 = nullptr, *a3 = nullptr; + if (m_util_s.str.is_replace_all(ex, a1, a2, a3)) { + if(!m_util_s.str.is_string(a2) || !m_util_s.str.is_string(a3)) { + util::throw_error("only replace_all with concrete find&replace is supported"); + } + + // recursively call on nested parameters + gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, transducer_preds); + // collect and replace replace_all argument with a concatenation of basic terms + std::vector side {}; + collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side); + + // result of the replace_all + std::string var = to_app(rpl)->get_decl()->get_name().str(); + BasicTerm bvar(BasicTermType::Variable, var); + + // TODO: add concrete transducer + mata::nft::Nft nft{2, {0}, {1}}; + nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + // TODO: switch sides? + Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared(nft)); + transducer_preds.push_back(rpl_all); + } + return; + } + + SASSERT(ex->get_num_args() == 2); + app *a_x = to_app(ex->get_arg(0)); + app *a_y = to_app(ex->get_arg(1)); + gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, transducer_preds); + gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, transducer_preds); + + } + void collect_terms(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, std::vector& terms) { diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h index 8b495a5d57e..26c23ccb504 100644 --- a/src/smt/theory_str_noodler/util.h +++ b/src/smt/theory_str_noodler/util.h @@ -11,6 +11,7 @@ #include #include #include +#include #include "smt/params/smt_params.h" #include "ast/arith_decl_plugin.h" @@ -90,6 +91,20 @@ namespace smt::noodler::util { */ void get_variable_names(expr* ex, const seq_util& m_util_s, const ast_manager& m, std::unordered_set& res); + /** + * @brief Gather transducer constraint (replace_all, replace_re_all) from a concatenation. Recursively applies also on + * nested calls of replace_all, replace_re_all. + * + * @param ex Concatenation of string terms. + * @param m AST manager + * @param m_util_s Seq util for AST. + * @param pred_replace Replacement of predicate and functions + * @param var_name Mapping of BasicTerm variables to z3 variables + * @param[out] transducer_preds Newly created transducer constraints + */ + void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, + std::map& var_name, std::vector& transducer_preds); + /** * Collect basic terms (vars, literals) from a concatenation @p ex. Append the basic terms to the output parameter * @p terms. From 4f5d74c882b7c472b18599ae5574536b41d5ccdb Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 14 Feb 2025 21:15:41 +0100 Subject: [PATCH 06/15] replace_all: construct transducer constraint --- .../theory_str_noodler/theory_str_noodler.cpp | 9 ++-- .../theory_str_noodler/theory_str_noodler.h | 21 ++++++-- .../theory_str_noodler_final_check.cpp | 48 +++++++++++++++---- src/smt/theory_str_noodler/util.cc | 26 ++++++---- src/smt/theory_str_noodler/util.h | 12 ++++- 5 files changed, 89 insertions(+), 27 deletions(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 7c775a10961..c8e055036ca 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -156,7 +156,7 @@ namespace smt::noodler { void theory_str_noodler::string_theory_propagation(expr *expr, bool init, bool neg, bool var_lengths) { STRACE("str", tout << __LINE__ << " enter " << __FUNCTION__ << std::endl;); - STRACE("str", tout << mk_pp(expr, get_manager()) << std::endl;); + // STRACE("str", tout << mk_pp(expr, get_manager()) << std::endl;); context &ctx = get_context(); @@ -1520,10 +1520,9 @@ namespace smt::noodler { VERIFY(m_util_s.str.is_replace_all(e, s, i, l)); expr_ref v = mk_str_var_fresh("replace_all"); - // we need to store v into a storage. Since this->predicate_replace - // stores only pointers, the value v would cease to exist after end of - // handle_replace_all - this->trans_terms.push_back(v); + // create equation for propagating length constraints + // tmp = replace_all(...) => |tmp| = |replace_all(...)| + add_axiom({mk_eq(v, e, false)}); this->predicate_replace.insert(e, v.get()); } diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index e70c9b02b14..ecb427d1712 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -95,8 +95,6 @@ namespace smt::noodler { // mapping predicates and function to variables that they substitute to obj_map predicate_replace; - // mapping replace_all and replace_re_all to fresh variables - std::vector trans_terms; // TODO what are these? std::vector axiomatized_len_axioms; @@ -400,10 +398,27 @@ namespace smt::noodler { @return Instance of predicate */ Predicate conv_eq_pred(app* expr); + + /** + * @brief Check if the given equation is a temporary equations that was added + * among axioms during axiomatization in handle_replace_all. These equalities + * are there due to length axioms inferring and proper handling of variable + * substitution. We want to discard them as they make the instances artificially harder: + * x = replace_all(...) || x = y --> we might get in final_check x = y && tmp = replace_all(...) + * in final_check we include only those transducer constraints that are present in remaining + * constraints (ignoring tmp = replace_all(...)). + * + * @param ex Equation + * @return true <-> is temporary transducer constraint + */ + bool is_tmp_transducer_eq(app* const ex); + /** * @brief Creates noodler formula containing relevant word equations and disequations + * + * @param alph Set of symbols of the current instance (for transducer constraints) */ - Formula get_word_formula_from_relevant(); + Formula get_word_formula_from_relevant(const std::set& alph); /** * @brief Get all symbols used in relevant word (dis)equations and memberships */ diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index 56097b4b235..ceddb22c6da 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -152,8 +152,11 @@ namespace smt::noodler { } } + // Gather symbols from relevant (dis)equations and from regular expressions of relevant memberships + std::set symbols_in_formula = get_symbols_from_relevant(); + // Gather relevant word (dis)equations to noodler formula - Formula instance = get_word_formula_from_relevant(); + Formula instance = get_word_formula_from_relevant(symbols_in_formula); STRACE("str", tout << std::endl; for(const auto& f : instance.get_predicates()) { @@ -165,8 +168,6 @@ namespace smt::noodler { util::throw_error("transducer constraints are not supported"); } - // Gather symbols from relevant (dis)equations and from regular expressions of relevant memberships - std::set symbols_in_formula = get_symbols_from_relevant(); // For the case that it is possible we have to_int/from_int, we keep digits (0-9) as explicit symbols, so that they are not represented by dummy_symbol and it is easier to handle to_int/from_int if (!m_conversion_todo.empty()) { for (mata::Symbol s = 48; s <= 57; ++s) { @@ -481,23 +482,45 @@ namespace smt::noodler { return Predicate(ptype, std::vector>{left, right}); } - Formula theory_str_noodler::get_word_formula_from_relevant() { + bool theory_str_noodler::is_tmp_transducer_eq(app* const ex) { + if (this->m_util_s.str.is_replace_all(ex->get_arg(0))) { + expr* rpl = this->predicate_replace.find(ex->get_arg(0)); + return rpl->hash() == ex->get_arg(1)->hash(); + } + if (this->m_util_s.str.is_replace_all(ex->get_arg(1))) { + expr* rpl = this->predicate_replace.find(ex->get_arg(1)); + return rpl->hash() == ex->get_arg(0)->hash(); + } + return false; + } + + Formula theory_str_noodler::get_word_formula_from_relevant(const std::set& alph) { Formula instance; std::vector transducer_pred {}; + // create mata alphabet for transducer constraints + mata::EnumAlphabet mata_alph{}; + for(const mata::Symbol& symb : alph) { + mata_alph.add_new_symbol(symb); + } for (const auto &we: this->m_word_eq_todo_rel) { + // ignore trivial equations obtained from axiomatization of + // transducer constraints, e.g., tmp = replace_all(...) + if(is_tmp_transducer_eq(ctx.mk_eq_atom(we.first, we.second))) { + continue; + } Predicate inst = this->conv_eq_pred(ctx.mk_eq_atom(we.first, we.second)); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); - util::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + util::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); instance.add_predicate(inst); } for (const auto& wd : this->m_word_diseq_todo_rel) { Predicate inst = this->conv_eq_pred(m.mk_not(ctx.mk_eq_atom(wd.first, wd.second))); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); - util::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + util::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); instance.add_predicate(inst); } @@ -507,8 +530,8 @@ namespace smt::noodler { util::collect_terms(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, left); util::collect_terms(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, right); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); - util::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, transducer_pred); + util::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + util::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); Predicate inst(PredicateType::NotContains, std::vector{left, right}); instance.add_predicate(inst); } @@ -526,6 +549,11 @@ namespace smt::noodler { std::set symbols_in_formula{util::get_dummy_symbol()}; for (const auto &word_equation: m_word_eq_todo_rel) { + // ignore trivial equations obtained from axiomatization of + // transducer constraints, e.g., tmp = replace_all(...) + if(is_tmp_transducer_eq(ctx.mk_eq_atom(word_equation.first, word_equation.second))) { + continue; + } regex::extract_symbols(word_equation.first, m_util_s, symbols_in_formula); regex::extract_symbols(word_equation.second, m_util_s, symbols_in_formula); } diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc index cf6449a4373..5644b7998a4 100644 --- a/src/smt/theory_str_noodler/util.cc +++ b/src/smt/theory_str_noodler/util.cc @@ -82,7 +82,7 @@ namespace smt::noodler::util { return m_util_s.is_string(expression->get_sort()) && is_variable(expression); } - void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, std::vector& transducer_preds) { + void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds) { if(m_util_s.str.is_string(ex) || is_variable(ex)) { // Handle string literals. return; } @@ -92,12 +92,13 @@ namespace smt::noodler::util { // so-far we handle just replace_all expr * a1 = nullptr, *a2 = nullptr, *a3 = nullptr; if (m_util_s.str.is_replace_all(ex, a1, a2, a3)) { - if(!m_util_s.str.is_string(a2) || !m_util_s.str.is_string(a3)) { + zstring find, replace; + if(!m_util_s.str.is_string(a2, find) || !m_util_s.str.is_string(a3, replace)) { util::throw_error("only replace_all with concrete find&replace is supported"); } // recursively call on nested parameters - gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, transducer_preds); + gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); // collect and replace replace_all argument with a concatenation of basic terms std::vector side {}; collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side); @@ -106,21 +107,22 @@ namespace smt::noodler::util { std::string var = to_app(rpl)->get_decl()->get_name().str(); BasicTerm bvar(BasicTermType::Variable, var); - // TODO: add concrete transducer - mata::nft::Nft nft{2, {0}, {1}}; - nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + // transducer corresponding to replace_all + mata::nft::Nft nft = mata::nft::strings::replace_reluctant_literal(get_mata_word_zstring(find), get_mata_word_zstring(replace), mata_alph); + // TODO: switch sides? Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared(nft)); transducer_preds.push_back(rpl_all); } + // TODO: handle replace_re_all return; } SASSERT(ex->get_num_args() == 2); app *a_x = to_app(ex->get_arg(0)); app *a_y = to_app(ex->get_arg(1)); - gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, transducer_preds); - gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, transducer_preds); + gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); + gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, mata_alph,transducer_preds); } @@ -310,6 +312,14 @@ namespace smt::noodler::util { return true; } + + mata::Word get_mata_word_zstring(const zstring& word) { + mata::Word ret{}; + for(size_t i = 0; i < word.length(); i++) { + ret.push_back(word[i]); + } + return ret; + } } template diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h index 26c23ccb504..ceef165810d 100644 --- a/src/smt/theory_str_noodler/util.h +++ b/src/smt/theory_str_noodler/util.h @@ -12,6 +12,7 @@ #include #include #include +#include #include "smt/params/smt_params.h" #include "ast/arith_decl_plugin.h" @@ -100,10 +101,11 @@ namespace smt::noodler::util { * @param m_util_s Seq util for AST. * @param pred_replace Replacement of predicate and functions * @param var_name Mapping of BasicTerm variables to z3 variables + * @param mata_alph Mata alphabet containing symbols from the current instance * @param[out] transducer_preds Newly created transducer constraints */ void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, - std::map& var_name, std::vector& transducer_preds); + std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds); /** * Collect basic terms (vars, literals) from a concatenation @p ex. Append the basic terms to the output parameter @@ -161,6 +163,14 @@ namespace smt::noodler::util { * @return boolean indicating whether we can split the @p word to @p automata (true if we can) */ bool split_word_to_automata(const zstring& word, const std::vector>& automata, std::vector& words); + + /** + * @brief Convert zstring to mata::Word + * + * @param word zstring + * @return mata::Word + */ + mata::Word get_mata_word_zstring(const zstring& word); } size_t bin_search_leftmost(const std::vector& haystack, mata::nfa::State needle); From 13c0fe1955484924c208e436bc75c78b01e0f581 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 16 Feb 2025 21:43:03 +0100 Subject: [PATCH 07/15] replace_re_all: predicate handling --- src/smt/theory_str_noodler/regex.cpp | 75 +++++++++++++++++++ src/smt/theory_str_noodler/regex.h | 16 ++++ .../theory_str_noodler/theory_str_noodler.cpp | 26 ++++++- .../theory_str_noodler/theory_str_noodler.h | 1 + .../theory_str_noodler_final_check.cpp | 16 ++-- src/smt/theory_str_noodler/util.cc | 44 ----------- src/smt/theory_str_noodler/util.h | 15 ---- 7 files changed, 125 insertions(+), 68 deletions(-) diff --git a/src/smt/theory_str_noodler/regex.cpp b/src/smt/theory_str_noodler/regex.cpp index 9a3758744cf..e465327f096 100644 --- a/src/smt/theory_str_noodler/regex.cpp +++ b/src/smt/theory_str_noodler/regex.cpp @@ -707,4 +707,79 @@ namespace smt::noodler::regex { throw regex_model_fail(); } } + + void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds) { + if(m_util_s.str.is_string(ex) || util::is_variable(ex)) { // Handle string literals. + return; + } + + if(!m_util_s.str.is_concat(ex)) { + expr* rpl = pred_replace.find(ex); // dies if it is not found + // so-far we handle just replace_all + expr * a1 = nullptr, *a2 = nullptr, *a3 = nullptr; + if (m_util_s.str.is_replace_all(ex, a1, a2, a3)) { + zstring find, replace; + if(!m_util_s.str.is_string(a2, find) || !m_util_s.str.is_string(a3, replace)) { + util::throw_error("only replace_all with concrete find&replace is supported"); + } + + // recursively call on nested parameters + gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); + // collect and replace replace_all argument with a concatenation of basic terms + std::vector side {}; + util::collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side); + + // result of the replace_all + std::string var = to_app(rpl)->get_decl()->get_name().str(); + BasicTerm bvar(BasicTermType::Variable, var); + + // transducer corresponding to replace_all + mata::nft::Nft nft = mata::nft::strings::replace_reluctant_literal(util::get_mata_word_zstring(find), util::get_mata_word_zstring(replace), mata_alph); + + // TODO: switch sides? + Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared(nft)); + transducer_preds.push_back(rpl_all); + + // replace_re_all + } else if (m_util_s.str.is_replace_re_all(ex, a1, a2, a3)) { + zstring replace; + if(!m_util_s.str.is_string(a3, replace)) { + util::throw_error("only replace_re_all with concrete find&replace is supported"); + } + + // construct NFA corresponding to the regex find + auto ov = mata_alph->get_alphabet_symbols(); + std::set syms(ov.begin(), ov.end()); + Alphabet alph(syms); + mata::nfa::Nfa find_nfa = conv_to_nfa(to_app(a2), m_util_s, m, alph); + + // recursively call on nested parameters + gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); + // collect and replace replace_all argument with a concatenation of basic terms + std::vector side {}; + util::collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side); + + // result of the replace_all + std::string var = to_app(rpl)->get_decl()->get_name().str(); + BasicTerm bvar(BasicTermType::Variable, var); + + // transducer corresponding to replace_all + mata::nft::Nft nft = mata::nft::strings::replace_reluctant_regex(find_nfa, util::get_mata_word_zstring(replace), mata_alph); + + // TODO: switch sides? + Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared(nft)); + transducer_preds.push_back(rpl_all); + } + // TODO: handle replace_re_all + return; + } + + SASSERT(ex->get_num_args() == 2); + app *a_x = to_app(ex->get_arg(0)); + app *a_y = to_app(ex->get_arg(1)); + gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); + gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, mata_alph,transducer_preds); + + } + } diff --git a/src/smt/theory_str_noodler/regex.h b/src/smt/theory_str_noodler/regex.h index f1c279d3903..5d8429508ab 100644 --- a/src/smt/theory_str_noodler/regex.h +++ b/src/smt/theory_str_noodler/regex.h @@ -156,6 +156,22 @@ namespace smt::noodler::regex { * @throws regex_model_fail if the model cannot be found (either regex represents empty language, or it contains intersection/complement/string variables, which this function currently cannot handle) */ zstring get_model_from_regex(const app *regex, const seq_util& m_util_s); + + /** + * @brief Gather transducer constraint (replace_all, replace_re_all) from a concatenation. Recursively applies also on + * nested calls of replace_all, replace_re_all. + * + * @param ex Concatenation of string terms. + * @param m AST manager + * @param m_util_s Seq util for AST. + * @param pred_replace Replacement of predicate and functions + * @param var_name Mapping of BasicTerm variables to z3 variables + * @param mata_alph Mata alphabet containing symbols from the current instance + * @param[out] transducer_preds Newly created transducer constraints + */ + void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, + std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds); + } #endif diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index c8e055036ca..4b73ad889bc 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -403,7 +403,7 @@ namespace smt::noodler { } else if(m_util_s.str.is_replace_re(n)) { // str.replace_re handle_replace_re(n); } else if(m_util_s.str.is_replace_re_all(n)) { // str.replace_re_all - util::throw_error("str.replace_re_all is not supported"); + handle_replace_re_all(n); } else if (m_util_s.str.is_is_digit(n)) { // str.is_digit handle_is_digit(n); } else if ( @@ -1526,6 +1526,30 @@ namespace smt::noodler { this->predicate_replace.insert(e, v.get()); } + /** + * @brief Handle replace_re_all. Just store the instance. It is solved using transducer + * constraints in the final_check. + * + * @param e replace_re_all + */ + void theory_str_noodler::handle_replace_re_all(expr *e) { + STRACE("str", tout << "handle-replace-re-all: " << mk_pp(e, m) << '\n';); + if (axiomatized_persist_terms.contains(e)) + return; + + axiomatized_persist_terms.insert(e); + + ast_manager &m = get_manager(); + expr *s = nullptr, *i = nullptr, *l = nullptr; + VERIFY(m_util_s.str.is_replace_re_all(e, s, i, l)); + + expr_ref v = mk_str_var_fresh("replace_all"); + // create equation for propagating length constraints + // tmp = replace_all(...) => |tmp| = |replace_all(...)| + add_axiom({mk_eq(v, e, false)}); + this->predicate_replace.insert(e, v.get()); + } + expr_ref theory_str_noodler::mk_concat(expr* e1, expr* e2) { return expr_ref(m_util_s.str.mk_concat(e1, e2), m); } diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index ecb427d1712..02dbcf9c7b3 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -335,6 +335,7 @@ namespace smt::noodler { void handle_lex_leq(expr *e); void handle_lex_lt(expr *e); void handle_replace_all(expr *e); + void handle_replace_re_all(expr *e); // methods for assigning boolean values to predicates void assign_not_contains(expr *e); diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index ceddb22c6da..ae3d1c94243 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -483,11 +483,11 @@ namespace smt::noodler { } bool theory_str_noodler::is_tmp_transducer_eq(app* const ex) { - if (this->m_util_s.str.is_replace_all(ex->get_arg(0))) { + if (this->m_util_s.str.is_replace_all(ex->get_arg(0)) || this->m_util_s.str.is_replace_re_all(ex->get_arg(0))) { expr* rpl = this->predicate_replace.find(ex->get_arg(0)); return rpl->hash() == ex->get_arg(1)->hash(); } - if (this->m_util_s.str.is_replace_all(ex->get_arg(1))) { + if (this->m_util_s.str.is_replace_all(ex->get_arg(1)) || this->m_util_s.str.is_replace_re_all(ex->get_arg(1))) { expr* rpl = this->predicate_replace.find(ex->get_arg(1)); return rpl->hash() == ex->get_arg(0)->hash(); } @@ -511,16 +511,16 @@ namespace smt::noodler { } Predicate inst = this->conv_eq_pred(ctx.mk_eq_atom(we.first, we.second)); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); - util::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); instance.add_predicate(inst); } for (const auto& wd : this->m_word_diseq_todo_rel) { Predicate inst = this->conv_eq_pred(m.mk_not(ctx.mk_eq_atom(wd.first, wd.second))); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); - util::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); instance.add_predicate(inst); } @@ -530,8 +530,8 @@ namespace smt::noodler { util::collect_terms(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, left); util::collect_terms(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, right); // gather transducer constraints occurring in the concatenation - util::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); - util::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); + regex::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred); Predicate inst(PredicateType::NotContains, std::vector{left, right}); instance.add_predicate(inst); } diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc index 5644b7998a4..35819ae5ae1 100644 --- a/src/smt/theory_str_noodler/util.cc +++ b/src/smt/theory_str_noodler/util.cc @@ -82,50 +82,6 @@ namespace smt::noodler::util { return m_util_s.is_string(expression->get_sort()) && is_variable(expression); } - void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds) { - if(m_util_s.str.is_string(ex) || is_variable(ex)) { // Handle string literals. - return; - } - - if(!m_util_s.str.is_concat(ex)) { - expr* rpl = pred_replace.find(ex); // dies if it is not found - // so-far we handle just replace_all - expr * a1 = nullptr, *a2 = nullptr, *a3 = nullptr; - if (m_util_s.str.is_replace_all(ex, a1, a2, a3)) { - zstring find, replace; - if(!m_util_s.str.is_string(a2, find) || !m_util_s.str.is_string(a3, replace)) { - util::throw_error("only replace_all with concrete find&replace is supported"); - } - - // recursively call on nested parameters - gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); - // collect and replace replace_all argument with a concatenation of basic terms - std::vector side {}; - collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side); - - // result of the replace_all - std::string var = to_app(rpl)->get_decl()->get_name().str(); - BasicTerm bvar(BasicTermType::Variable, var); - - // transducer corresponding to replace_all - mata::nft::Nft nft = mata::nft::strings::replace_reluctant_literal(get_mata_word_zstring(find), get_mata_word_zstring(replace), mata_alph); - - // TODO: switch sides? - Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared(nft)); - transducer_preds.push_back(rpl_all); - } - // TODO: handle replace_re_all - return; - } - - SASSERT(ex->get_num_args() == 2); - app *a_x = to_app(ex->get_arg(0)); - app *a_y = to_app(ex->get_arg(1)); - gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds); - gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, mata_alph,transducer_preds); - - } - void collect_terms(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, std::vector& terms) { diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h index ceef165810d..6310c271226 100644 --- a/src/smt/theory_str_noodler/util.h +++ b/src/smt/theory_str_noodler/util.h @@ -92,21 +92,6 @@ namespace smt::noodler::util { */ void get_variable_names(expr* ex, const seq_util& m_util_s, const ast_manager& m, std::unordered_set& res); - /** - * @brief Gather transducer constraint (replace_all, replace_re_all) from a concatenation. Recursively applies also on - * nested calls of replace_all, replace_re_all. - * - * @param ex Concatenation of string terms. - * @param m AST manager - * @param m_util_s Seq util for AST. - * @param pred_replace Replacement of predicate and functions - * @param var_name Mapping of BasicTerm variables to z3 variables - * @param mata_alph Mata alphabet containing symbols from the current instance - * @param[out] transducer_preds Newly created transducer constraints - */ - void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, - std::map& var_name, mata::Alphabet* mata_alph, std::vector& transducer_preds); - /** * Collect basic terms (vars, literals) from a concatenation @p ex. Append the basic terms to the output parameter * @p terms. From 58a5b2da7ffb87e3e928582b7c88c35afd1c138d Mon Sep 17 00:00:00 2001 From: vhavlena Date: Mon, 17 Feb 2025 07:26:41 +0100 Subject: [PATCH 08/15] README: version of mata --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3bea344273c..173cf298784 100644 --- a/README.md +++ b/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 From 8bf92745cd73191c3d2a4db6c9947ac6851679a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20Havlena?= Date: Tue, 18 Feb 2025 20:49:34 +0100 Subject: [PATCH 09/15] Update src/test/noodler/inclusion-graph-node.cc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Juraj Síč --- src/test/noodler/inclusion-graph-node.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc index c656aa03116..822a8234a7e 100644 --- a/src/test/noodler/inclusion-graph-node.cc +++ b/src/test/noodler/inclusion-graph-node.cc @@ -450,4 +450,4 @@ TEST_CASE("Inclusion graph with transducers", "[noodler]") { CHECK(graph.get_num_of_edges() == 1); CHECK(!graph.is_cyclic()); } -} \ No newline at end of file +} From d4fab8470a85cbb1670e51adc6cfc799fd89118c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20Havlena?= Date: Tue, 18 Feb 2025 20:49:48 +0100 Subject: [PATCH 10/15] Update src/test/noodler/formula.cpp MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Juraj Síč --- src/test/noodler/formula.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/noodler/formula.cpp b/src/test/noodler/formula.cpp index aa1e9fcb144..c50844fd705 100644 --- a/src/test/noodler/formula.cpp +++ b/src/test/noodler/formula.cpp @@ -85,4 +85,4 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) { fres.add_predicate(pres); CHECK(f == fres); } -} \ No newline at end of file +} From 74d8ca3cb6230e07b1aa14bbbbf55ac6469082db Mon Sep 17 00:00:00 2001 From: vhavlena Date: Tue, 18 Feb 2025 21:25:07 +0100 Subject: [PATCH 11/15] rename get_word_formula_from_relevant to get_formula_from_relevant --- src/smt/theory_str_noodler/theory_str_noodler.h | 2 +- src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index 02dbcf9c7b3..9b281ca1524 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -419,7 +419,7 @@ namespace smt::noodler { * * @param alph Set of symbols of the current instance (for transducer constraints) */ - Formula get_word_formula_from_relevant(const std::set& alph); + Formula get_formula_from_relevant(const std::set& alph); /** * @brief Get all symbols used in relevant word (dis)equations and memberships */ diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index ae3d1c94243..b6752544717 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -156,7 +156,7 @@ namespace smt::noodler { std::set symbols_in_formula = get_symbols_from_relevant(); // Gather relevant word (dis)equations to noodler formula - Formula instance = get_word_formula_from_relevant(symbols_in_formula); + Formula instance = get_formula_from_relevant(symbols_in_formula); STRACE("str", tout << std::endl; for(const auto& f : instance.get_predicates()) { @@ -494,7 +494,7 @@ namespace smt::noodler { return false; } - Formula theory_str_noodler::get_word_formula_from_relevant(const std::set& alph) { + Formula theory_str_noodler::get_formula_from_relevant(const std::set& alph) { Formula instance; std::vector transducer_pred {}; // create mata alphabet for transducer constraints From 997b54da12e2140db5bea67d7250904970ac0875 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Tue, 18 Feb 2025 21:27:22 +0100 Subject: [PATCH 12/15] update STRACE logging in string_theory_propagation --- src/smt/theory_str_noodler/theory_str_noodler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 4b73ad889bc..8d1e4351976 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -156,7 +156,7 @@ namespace smt::noodler { void theory_str_noodler::string_theory_propagation(expr *expr, bool init, bool neg, bool var_lengths) { STRACE("str", tout << __LINE__ << " enter " << __FUNCTION__ << std::endl;); - // STRACE("str", tout << mk_pp(expr, get_manager()) << std::endl;); + STRACE("str-propagation", tout << mk_pp(expr, get_manager()) << std::endl;); context &ctx = get_context(); From c025e588e29d829da73feddc469f17f2c650f8ef Mon Sep 17 00:00:00 2001 From: vhavlena Date: Wed, 19 Feb 2025 19:24:31 +0100 Subject: [PATCH 13/15] conparison of predicates; strong_equals --- src/smt/theory_str_noodler/formula.cpp | 21 +++++++++++++++++-- src/smt/theory_str_noodler/formula.h | 15 +++++++++++-- src/smt/theory_str_noodler/inclusion_graph.cc | 2 +- src/smt/theory_str_noodler/inclusion_graph.h | 4 ++-- src/test/noodler/formula-preprocess.cpp | 20 +++++++++++------- src/test/noodler/formula.cpp | 12 ++++++----- 6 files changed, 54 insertions(+), 20 deletions(-) diff --git a/src/smt/theory_str_noodler/formula.cpp b/src/smt/theory_str_noodler/formula.cpp index db2922c59e1..3e5f408ea76 100644 --- a/src/smt/theory_str_noodler/formula.cpp +++ b/src/smt/theory_str_noodler/formula.cpp @@ -308,8 +308,25 @@ namespace smt::noodler { if(!(params[0] == other.params[0] && params[1] == other.params[1])) { return false; } - // check if transducers are identical (cheaper than equivalence check, which might be too strong for this purpose) - return transducer->is_identical(*other.transducer); + // 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]; diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 847c43b54ab..9950fe50b34 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -551,6 +551,17 @@ 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 { @@ -608,8 +619,8 @@ namespace smt::noodler { } // For transducer predicates we compare pointers (assuming linear memory model) if (lhs.is_transducer()) { - // if we have the same object stored on two different places - if (lhs.get_transducer()->is_identical(*rhs.get_transducer())) { + // compare pointer for equality + if (lhs.get_transducer() == rhs.get_transducer()) { return false; } // compare pointers diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc index 822b93adb56..9fe73e8b2e6 100644 --- a/src/smt/theory_str_noodler/inclusion_graph.cc +++ b/src/smt/theory_str_noodler/inclusion_graph.cc @@ -192,7 +192,7 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form } else if (source_left_side == target_right_side) { // Have same var and sides are equal. - if (source_predicate == target_predicate.get_switched_sides_predicate()) { // In the same reversed predicate. + if (source_predicate.strong_equals(target_predicate.get_switched_sides_predicate())) { // In the same reversed predicate. if (!source_predicate.mult_occurr_var_side(Predicate::EquationSideType::Left)) { // Does not have multiple occurrences of one var. Hence, cannot have an edge. continue; diff --git a/src/smt/theory_str_noodler/inclusion_graph.h b/src/smt/theory_str_noodler/inclusion_graph.h index 195804305ab..e7f0c7dfd49 100644 --- a/src/smt/theory_str_noodler/inclusion_graph.h +++ b/src/smt/theory_str_noodler/inclusion_graph.h @@ -28,7 +28,7 @@ namespace smt::noodler { }; [[nodiscard]] bool equals(const GraphNode& other) const { - return this->node_predicate == other.node_predicate; + return this->node_predicate.strong_equals(other.node_predicate); } private: @@ -152,7 +152,7 @@ namespace smt::noodler { } std::shared_ptr get_node(const Predicate& predicate) { - auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr &el){ return (el->get_predicate() == predicate);}); + auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr &el){ return (el->get_predicate().strong_equals(predicate));}); if (node == nodes.end()) { return nullptr; } return *node; } diff --git a/src/test/noodler/formula-preprocess.cpp b/src/test/noodler/formula-preprocess.cpp index 4d0d2b80727..fd9991468f7 100644 --- a/src/test/noodler/formula-preprocess.cpp +++ b/src/test/noodler/formula-preprocess.cpp @@ -278,13 +278,14 @@ TEST_CASE( "Propagate variables", "[noodler]" ) { nft.initial = {0}; nft.final = {1}; nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + auto nft_ptr = std::make_shared(nft); Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1, x1}), std::vector({x3, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x2}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); - Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); - Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x1}) }), std::make_shared(nft) ); + Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), nft_ptr ); + Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x1}) }), nft_ptr ); SECTION("(In)equations") { Formula conj; @@ -357,14 +358,15 @@ TEST_CASE( "Remove duplicates", "[noodler]" ) { nft.initial = {0}; nft.final = {1}; nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + auto nft_ptr = std::make_shared(nft); Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({a, x3, x4}), std::vector({b, x1, x2}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); Predicate ieq2(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({x3}) }) ); - Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); - Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), std::make_shared(nft) ); + Predicate tr1(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), nft_ptr ); + Predicate tr2(PredicateType::Transducer, std::vector>({ std::vector({x1}), std::vector({x3}) }), nft_ptr ); Formula conj; conj.add_predicate(eq1); conj.add_predicate(eq3); @@ -483,12 +485,13 @@ TEST_CASE( "Reduce regular", "[noodler]" ) { mata::nft::Nft nft{2, {0}, {1}}; nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + auto nft_ptr = std::make_shared(nft); Predicate eq1(PredicateType::Inequation, std::vector>({ std::vector({a, x3, x4, b}), std::vector({x1, x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x2, x1, x2}), std::vector({b, x3, x4, b}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, x1, x2}) }) ); Predicate eq4(PredicateType::Equation, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }) ); - Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }), std::make_shared(nft) ); + Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1, x2, x3}), std::vector({x4, a, b}) }), nft_ptr ); SECTION("basic") { @@ -561,7 +564,7 @@ TEST_CASE( "Reduce regular", "[noodler]" ) { CHECK(mata::nfa::are_equivalent(*ret.at(tmp1), regex_to_nfa("(a|b)*a*"))); CHECK(prep.get_formula().get_predicates_set() == std::set({ Predicate(PredicateType::Equation, std::vector>({ std::vector({tmp0}), std::vector({x4, a, b}) })), - Predicate(PredicateType::Transducer, std::vector>({ std::vector({tmp1}), std::vector({tmp0}) }), std::make_shared(nft) ), + Predicate(PredicateType::Transducer, std::vector>({ std::vector({tmp1}), std::vector({tmp0}) }), nft_ptr ), Predicate(PredicateType::Equation, std::vector>({ std::vector({tmp1 }), std::vector({x5, x1, x2, x3}) }) ) })); } @@ -591,13 +594,14 @@ TEST_CASE( "Propagate eps", "[noodler]" ) { mata::nft::Nft nft{2, {0}, {1}}; nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1); + auto nft_ptr = std::make_shared(nft); Predicate eq1(PredicateType::Equation, std::vector>({ std::vector({eps}), std::vector({x1, x2}) }) ); Predicate eq2(PredicateType::Equation, std::vector>({ std::vector({x2, x1, x2}), std::vector({x3, x4}) }) ); Predicate eq3(PredicateType::Equation, std::vector>({ std::vector({x3, b, x4}), std::vector({x5, x1}) }) ); Predicate eq4(PredicateType::Equation, std::vector>({ std::vector({b, x1}), std::vector({eps}) }) ); Predicate ieq1(PredicateType::Inequation, std::vector>({ std::vector({x1}), std::vector({eps}) }) ); - Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1}), std::vector({x2}) }), std::make_shared(nft) ); + Predicate tr4(PredicateType::Transducer, std::vector>({ std::vector({x5, x1}), std::vector({x2}) }), nft_ptr ); SECTION("basic") { Formula conj; @@ -642,7 +646,7 @@ TEST_CASE( "Propagate eps", "[noodler]" ) { CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa(""))); CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa(""))); CHECK(prep.get_formula().get_predicates_set() == std::set({ - Predicate(PredicateType::Transducer, std::vector>({ std::vector({x5}), std::vector() }), std::make_shared(nft) ), + Predicate(PredicateType::Transducer, std::vector>({ std::vector({x5}), std::vector() }), nft_ptr ), })); } } diff --git a/src/test/noodler/formula.cpp b/src/test/noodler/formula.cpp index c50844fd705..9d236be21f4 100644 --- a/src/test/noodler/formula.cpp +++ b/src/test/noodler/formula.cpp @@ -34,7 +34,7 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) { // result Predicate switch_res { PredicateType::Transducer, { { y }, { x } }, std::make_shared(nft_inv) }; - CHECK(pred_trans_switch == switch_res); + CHECK(pred_trans_switch.strong_equals(switch_res)); } SECTION("Comparison") { @@ -46,11 +46,12 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) { Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; Predicate p2 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft_other) }; - Predicate p3 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; + Predicate p3 { PredicateType::Transducer, { { x }, { y } }, p1.get_transducer() }; CHECK(p1 != p2); CHECK(!(p1 < p1)); CHECK(p1 == p1); - CHECK(p1 == p3); + CHECK(p1.strong_equals(p1)); + CHECK(p1.strong_equals(p3)); CHECK(!(p1 < p3)); CHECK(!(p3 < p1)); @@ -72,10 +73,11 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) { nft_other.initial = {0}; nft_other.final = {1}; nft_other.insert_word_by_parts(0, { {'c'}, {'d'} } , 1); + auto nft_ptr = std::make_shared(nft); - Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared(nft) }; - Predicate pres { PredicateType::Transducer, { { x }, { x } }, std::make_shared(nft) }; + Predicate p1 { PredicateType::Transducer, { { x }, { y } }, nft_ptr }; + Predicate pres { PredicateType::Transducer, { { x }, { x } }, nft_ptr }; Formula f{}; f.add_predicate(p1); From 76f6c7ab3a3fca28e3ca94d2e9f3c0f9fb3b4b56 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Wed, 19 Feb 2025 19:55:44 +0100 Subject: [PATCH 14/15] inclusion graph: simplifying condition --- src/smt/theory_str_noodler/inclusion_graph.cc | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc index 9fe73e8b2e6..5ccf5d68e2d 100644 --- a/src/smt/theory_str_noodler/inclusion_graph.cc +++ b/src/smt/theory_str_noodler/inclusion_graph.cc @@ -189,16 +189,11 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form if (!have_same_var(source_left_side, target_right_side)) { continue; - } else if (source_left_side == target_right_side) { + } else if (source_predicate.strong_equals(target_predicate.get_switched_sides_predicate())) { // Have same var and sides are equal. - - if (source_predicate.strong_equals(target_predicate.get_switched_sides_predicate())) { // In the same reversed predicate. - if (!source_predicate.mult_occurr_var_side(Predicate::EquationSideType::Left)) { - // Does not have multiple occurrences of one var. Hence, cannot have an edge. - continue; - } - } else { - // In different equation. + if (!source_predicate.mult_occurr_var_side (Predicate::EquationSideType::Left)) { + // Does not have multiple occurrences of one var. Hence, cannot have an edge. + continue; } } else { // Have same var and sides are not equal, automatically add a new edge. From d7add978f5238ca1559b263dfdbd81907be18e41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20Havlena?= Date: Thu, 20 Feb 2025 08:56:31 +0100 Subject: [PATCH 15/15] Update src/smt/theory_str_noodler/formula.h MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Juraj Síč --- src/smt/theory_str_noodler/formula.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h index 9950fe50b34..d327472f2ed 100644 --- a/src/smt/theory_str_noodler/formula.h +++ b/src/smt/theory_str_noodler/formula.h @@ -619,10 +619,6 @@ namespace smt::noodler { } // For transducer predicates we compare pointers (assuming linear memory model) if (lhs.is_transducer()) { - // compare pointer for equality - if (lhs.get_transducer() == rhs.get_transducer()) { - return false; - } // compare pointers return lhs.get_transducer() < rhs.get_transducer(); }