Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

First step towards replace_all operations #209

Open
wants to merge 12 commits into
base: devel
Choose a base branch
from
Open

First step towards replace_all operations #209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
564678d
formula: basic transducer and replace_alls support
vhavlena Feb 9, 2025
3955d3b
formula: remove replace_alls; operations with transducer predicate
vhavlena Feb 11, 2025
ee2c3d0
inclusion graph: transducer constraints support
vhavlena Feb 13, 2025
17e2a18
preprocess: transducer constraint support
vhavlena Feb 13, 2025
6cacc38
integration: sketch of handling replace_all
vhavlena Feb 13, 2025
4f5d74c
replace_all: construct transducer constraint
vhavlena Feb 14, 2025
13c0fe1
replace_re_all: predicate handling
vhavlena Feb 16, 2025
58a5b2d
README: version of mata
vhavlena Feb 17, 2025
8bf9274
Update src/test/noodler/inclusion-graph-node.cc
vhavlena Feb 18, 2025
d4fab84
Update src/test/noodler/formula.cpp
vhavlena Feb 18, 2025
74d8ca3
rename get_word_formula_from_relevant to get_formula_from_relevant
vhavlena Feb 18, 2025
997b54d
update STRACE logging in string_theory_propagation
vhavlena Feb 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
64 changes: 35 additions & 29 deletions src/smt/theory_str_noodler/formula.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ namespace smt::noodler {
}

std::set<BasicTerm> Predicate::get_side_vars(const Predicate::EquationSideType side) const {
assert(is_eq_or_ineq());
assert(is_two_sided());
std::set<BasicTerm> vars;
std::vector<BasicTerm> side_terms;
switch (side) {
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -262,40 +262,39 @@ namespace smt::noodler {
}

std::string Predicate::to_string() const {

// joining BasicTerm in the given vector with str
auto join = [&](const std::vector<BasicTerm>& vec, const std::string& str) -> std::string {
if(vec.empty()) return "";
std::string ret = vec[0].to_string();
for(size_t i = 1; i < vec.size(); i++) {
ret += str + vec[i].to_string();
}
return ret;
};

switch (type) {
case PredicateType::Equation: {
std::string result{ "Equation:" };
for (const auto& item: get_left_side()) {
result += " " + item.to_string();
}
result += " =";
for (const auto& item: get_right_side()) {
result += " " + item.to_string();
}
std::string result{ "Equation: " };
result += join(get_left_side(), " ") + " = " + join(get_right_side(), " ");
return result;
}

case PredicateType::Inequation: {
std::string result{ "Inequation:" };
for (const auto& item: get_left_side()) {
result += " " + item.to_string();
}
result += " !=";
for (const auto& item: get_right_side()) {
result += " " + item.to_string();
}
std::string result{ "Inequation: " };
result += join(get_left_side(), " ") + " != " + join(get_right_side(), " ");
return result;
}

case PredicateType::NotContains: {
std::string result{ "Notcontains " };
for (const auto& item: params[0]) {
result += " " + item.to_string();
}
result += " ,";
for (const auto& item: params[1]) {
result += " " + item.to_string();
}
std::string result{ "Notcontains: " };
result += join(params[0], " ") + " , " + join(params[1], " ");
return result;
}

case PredicateType::Transducer: {
std::string result{ "Transducer: " };
result += join(params[0], " ") + " , " + join(params[1], " ");
return result;
}
}
Expand All @@ -305,16 +304,23 @@ 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);
Comment on lines +311 to +312
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This might be dangerous, we will forget that a cheap test is done here. Maybe some other function called cheap_equals?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, now that I think about it, it is equivalence of predicates and not the language equivalence, so checking if they are identical here makes sense. I would maybe go even step further and compare the pointers and not the transducers, I think equality is used for hashing, right?

}
if (is_two_sided()) {
return params[0] == other.params[0] && params[1] == other.params[1];
}
return true;
return params == other.params;
}
return false;
}

const std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) const {
assert(is_eq_or_ineq());
assert(is_two_sided());
switch (side) {
case EquationSideType::Left:
return params[0];
Expand All @@ -329,7 +335,7 @@ namespace smt::noodler {
}

std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) {
assert(is_eq_or_ineq());
assert(is_two_sided());
switch (side) {
case EquationSideType::Left:
return params[0];
Expand Down
67 changes: 52 additions & 15 deletions src/smt/theory_str_noodler/formula.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
#include <map>
#include <unordered_set>
#include <iostream>
#include <mata/nft/nft.hh>

#include "util/zstring.h"
#include "ast/ast.h"
Expand All @@ -35,6 +36,7 @@ namespace smt::noodler {
Equation,
Inequation,
NotContains,
Transducer,
};

[[nodiscard]] static std::string to_string(PredicateType predicate_type) {
Expand All @@ -45,6 +47,8 @@ namespace smt::noodler {
return "Inequation";
case PredicateType::NotContains:
return "Notcontains";
case PredicateType::Transducer:
return "Transducer";
}

throw std::runtime_error("Unhandled predicate type passed to to_string().");
Expand Down Expand Up @@ -290,7 +294,7 @@ namespace smt::noodler {
};

Predicate() : type(PredicateType::Equation) {}
explicit Predicate(const PredicateType type): type(type) {
explicit Predicate(const PredicateType type): type(type), params(), transducer() {
if (is_equation() || is_inequation()) {
params.resize(2);
params.emplace_back();
Expand All @@ -300,15 +304,25 @@ namespace smt::noodler {

explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par):
type(type),
params(par)
params(par),
transducer()
{ }

explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par, std::shared_ptr<mata::nft::Nft> trans) :
type(type),
params(par),
transducer(trans) {
assert(type == PredicateType::Transducer);
assert(trans->num_of_levels == 2);
}

[[nodiscard]] PredicateType get_type() const { return type; }
[[nodiscard]] bool is_equation() const { return type == PredicateType::Equation; }
[[nodiscard]] bool is_inequation() const { return type == PredicateType::Inequation; }
[[nodiscard]] bool is_not_cont() const { return type == PredicateType::NotContains; }
[[nodiscard]] bool is_eq_or_ineq() const { return is_equation() || is_inequation(); }
[[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont(); }
[[nodiscard]] bool is_transducer() const { return is(PredicateType::Transducer); }
[[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont() || is_transducer(); }
[[nodiscard]] bool is_predicate() const { return !is_eq_or_ineq(); }
[[nodiscard]] bool is(const PredicateType predicate_type) const { return predicate_type == this->type; }

Expand Down Expand Up @@ -364,15 +378,15 @@ namespace smt::noodler {
}

std::set<BasicTerm> get_left_set() const {
assert(is_eq_or_ineq());
assert(is_two_sided());
std::set<BasicTerm> ret;
for(const BasicTerm& t : this->params[0])
ret.insert(t);
return ret;
}

std::set<BasicTerm> get_right_set() const {
assert(is_eq_or_ineq());
assert(is_two_sided());
std::set<BasicTerm> ret;
for(const BasicTerm& t : this->params[1])
ret.insert(t);
Expand Down Expand Up @@ -413,6 +427,7 @@ namespace smt::noodler {
return LenNode(LenFormulaType::PLUS, ops);
};

assert(is_eq_or_ineq());
LenNode left = plus_chain(this->params[0]);
LenNode right = plus_chain(this->params[1]);
LenNode eq = LenNode(LenFormulaType::EQ, {left, right});
Expand All @@ -429,7 +444,12 @@ namespace smt::noodler {
[[nodiscard]] const std::vector<BasicTerm>& get_side(EquationSideType side) const;

[[nodiscard]] Predicate get_switched_sides_predicate() const {
assert(is_eq_or_ineq());
assert(is_two_sided());
// for transducers we need to invert tapes, i.e., T(x,y) iff T^{-1}(y,x)
if(is_transducer()) {
auto nft_inverse = std::make_shared<mata::nft::Nft>(mata::nft::invert_levels(*transducer));
return Predicate{ PredicateType::Transducer, { get_right_side(), get_left_side() }, nft_inverse };
}
return Predicate{ type, { get_right_side(), get_left_side() } };
}

Expand Down Expand Up @@ -479,6 +499,7 @@ namespace smt::noodler {
modif = modif || r;
}
res = Predicate(this->type, new_params);
res.transducer = this->transducer;
return modif;
}

Expand Down Expand Up @@ -536,23 +557,30 @@ namespace smt::noodler {
size_t operator()(const Predicate& predicate) const {
size_t res{};
size_t row_hash = std::hash<PredicateType>()(predicate.type);
for (const auto& term: predicate.get_left_side()) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
}
for (const auto& term: predicate.get_right_side()) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
for(const auto& pr : predicate.get_params()) {
for(const BasicTerm& term : pr) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
}
}
return row_hash ^ res;
}
};

// TODO: Additional operations.
/**
* @brief Get the transducer shared pointer (for the transducer predicates only).
*
* @return std::shared_ptr<mata::nft::Nft> Transducer
*/
const std::shared_ptr<mata::nft::Nft>& get_transducer() const {
assert(is_transducer());
return transducer;
}

private:
PredicateType type;
std::vector<std::vector<BasicTerm>> params;
std::shared_ptr<mata::nft::Nft> transducer; // transducer for the case of PredicateType::Transducer

// TODO: Add additional attributes such as cost, etc.
}; // Class Predicate.
Expand All @@ -578,9 +606,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();
Comment on lines +612 to +616
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly here, we should probably be checking only < of pointers, not that they are identical.

}
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; }

//----------------------------------------------------------------------------------------------------------------------------------

Expand Down
16 changes: 8 additions & 8 deletions src/smt/theory_str_noodler/formula_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ namespace smt::noodler {
void FormulaVar::remove_predicate(size_t index) {
std::set<BasicTerm> items = this->predicates[index].get_set();

const auto& filter = [&index](const VarNode& n) { return n.eq_index == index; };
const auto& filter = [&index](const VarNode& n) { return n.pred_index == index; };
for(const BasicTerm& v : items) {
std::set<VarNode>& occurr = this->varmap[v];
remove_if(occurr, filter);
Expand Down Expand Up @@ -367,10 +367,10 @@ namespace smt::noodler {
std::set<VarNode> occurrs = this->formula.get_var_occurr(left_var);
if(occurrs.size() == 1) {
Predicate reg_pred;
if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->eq_index), reg_pred)) {
worklist.emplace_back(occurrs.begin()->eq_index, reg_pred);
if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->pred_index), reg_pred)) {
worklist.emplace_back(occurrs.begin()->pred_index, reg_pred);
// update dependency
map_set_insert(this->dependency, occurrs.begin()->eq_index, pr.first);
map_set_insert(this->dependency, occurrs.begin()->pred_index, pr.first);
}
}
}
Expand Down Expand Up @@ -625,7 +625,7 @@ namespace smt::noodler {
// Get all occurrences of t
std::set<VarNode> occurrs = this->formula.get_var_occurr(t);
// Get predicate of a first equation containing t; and side containing t
Predicate act_pred = this->formula.get_predicate(occurrs.begin()->eq_index);
Predicate act_pred = this->formula.get_predicate(occurrs.begin()->pred_index);
Concat side = occurrs.begin()->position > 0 ? act_pred.get_right_side() : act_pred.get_left_side();

int start = std::abs(occurrs.begin()->position) - 1;
Expand All @@ -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)
});
}
Expand Down Expand Up @@ -728,7 +728,7 @@ namespace smt::noodler {
for(const BasicTerm& t : eps_set) {
std::set<VarNode> nds = get_formula().get_var_occurr(t);
std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
[](const VarNode& n){ return n.eq_index ; });
[](const VarNode& n){ return n.pred_index ; });
}

while(!worklist.empty()) {
Expand Down Expand Up @@ -757,7 +757,7 @@ namespace smt::noodler {
eps_set.insert(t);
std::set<VarNode> nds = get_formula().get_var_occurr(t);
std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
[](const VarNode& n){ return n.eq_index ; });
[](const VarNode& n){ return n.pred_index ; });
}
}

Expand Down
12 changes: 6 additions & 6 deletions src/smt/theory_str_noodler/formula_preprocess.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
Loading
Loading