Skip to content

Commit

Permalink
Merge pull request #209 from VeriFIT/transducers
Browse files Browse the repository at this point in the history 
First step towards `replace_all` operations
  • Loading branch information
@vhavlena
vhavlena authored Feb 20, 2025
2 parents 5227eea + d7add97 commit eb33649
Show file tree
Hide file tree
Showing 18 changed files with 683 additions and 110 deletions.
2 changes: 1 addition & 1 deletion README.md
View file
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
81 changes: 52 additions & 29 deletions src/smt/theory_str_noodler/formula.cpp
View file
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,40 @@ namespace smt::noodler {

bool Predicate::equals(const Predicate &other) const {
if (type == other.type) {
if(is_transducer()) {
if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
return false;
}
// check if transducers are the same pointers
return transducer == other.transducer;
}
if (is_two_sided()) {
return params[0] == other.params[0] && params[1] == other.params[1];
}
return params == other.params;
}
return false;
}

bool Predicate::strong_equals(const Predicate& other) const {
if (type == other.type) {
if(is_transducer()) {
if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
return false;
}
// check if transducers are the same pointers
return transducer->is_identical(*other.get_transducer());
}
if (is_two_sided()) {
return params[0] == other.params[0] && params[1] == other.params[1];
}
return true;
return params == other.params;
}
return false;
}

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

std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) {
assert(is_eq_or_ineq());
assert(is_two_sided());
switch (side) {
case EquationSideType::Left:
return params[0];
Expand Down
74 changes: 59 additions & 15 deletions src/smt/theory_str_noodler/formula.h
View file
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 @@ -530,29 +551,47 @@ namespace smt::noodler {

[[nodiscard]] bool equals(const Predicate& other) const;

/**
* @brief Strong equality. For the case of transducer predicates the transducers
* are compared for identity (not just the indentity of pointers). It is
* necessary for the inclusion graph handling where we require get_switched_side
* (get_swithch_side(x)) == x (which is not true for pointer comparison).
*
* @param other Other predicate
* @return true Is strongly equal
*/
bool strong_equals(const Predicate& other) const;

[[nodiscard]] std::string to_string() const;

struct HashFunction {
size_t operator()(const Predicate& predicate) const {
size_t res{};
size_t row_hash = std::hash<PredicateType>()(predicate.type);
for (const auto& term: predicate.get_left_side()) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
}
for (const auto& term: predicate.get_right_side()) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
for(const auto& pr : predicate.get_params()) {
for(const BasicTerm& term : pr) {
size_t col_hash = BasicTerm::HashFunction()(term) << 1;
res ^= col_hash;
}
}
return row_hash ^ res;
}
};

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

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

// TODO: Add additional attributes such as cost, etc.
}; // Class Predicate.
Expand All @@ -578,9 +617,14 @@ namespace smt::noodler {
if (lhs.get_params() < rhs.get_params()) {
return true;
}
// For transducer predicates we compare pointers (assuming linear memory model)
if (lhs.is_transducer()) {
// compare pointers
return lhs.get_transducer() < rhs.get_transducer();
}
return false;
}
static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs); }
static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs) && lhs != rhs; }

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

Expand Down
16 changes: 8 additions & 8 deletions src/smt/theory_str_noodler/formula_preprocess.cpp
View file
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
Loading

0 comments on commit eb33649

Please sign in to comment.