Skip to content

Commit

Permalink
conparison of predicates; strong_equals
Browse files Browse the repository at this point in the history
  • Loading branch information
@vhavlena
vhavlena committed Feb 19, 2025
1 parent 997b54d commit c025e58
Show file tree
Hide file tree
Showing 6 changed files with 54 additions and 20 deletions.
21 changes: 19 additions & 2 deletions src/smt/theory_str_noodler/formula.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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];
Expand Down
15 changes: 13 additions & 2 deletions src/smt/theory_str_noodler/formula.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_str_noodler/inclusion_graph.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions src/smt/theory_str_noodler/inclusion_graph.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -152,7 +152,7 @@ namespace smt::noodler {
}

std::shared_ptr<GraphNode> get_node(const Predicate& predicate) {
auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr<GraphNode> &el){ return (el->get_predicate() == predicate);});
auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr<GraphNode> &el){ return (el->get_predicate().strong_equals(predicate));});
if (node == nodes.end()) { return nullptr; }
return *node;
}
Expand Down
20 changes: 12 additions & 8 deletions src/test/noodler/formula-preprocess.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<mata::nft::Nft>(nft);

Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) }) );
Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1, x1}), std::vector<BasicTerm>({x3, x2}) }) );
Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x2}) }) );
Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }) );
Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x1}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr );
Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x1}) }), nft_ptr );

SECTION("(In)equations") {
Formula conj;
Expand Down Expand Up @@ -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<mata::nft::Nft>(nft);

Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) }) );
Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) }) );
Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }) );
Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }) );
Predicate ieq2(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }) );
Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr );
Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr );
Formula conj;
conj.add_predicate(eq1);
conj.add_predicate(eq3);
Expand Down Expand Up @@ -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<mata::nft::Nft>(nft);

Predicate eq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4, b}), std::vector<BasicTerm>({x1, x1, x2}) }) );
Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x2, x1, x2}), std::vector<BasicTerm>({b, x3, x4, b}) }) );
Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, x1, x2}) }) );
Predicate eq4(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) }) );
Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) }), nft_ptr );


SECTION("basic") {
Expand Down Expand Up @@ -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>({
Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp0}), std::vector<BasicTerm>({x4, a, b}) })),
Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp1}), std::vector<BasicTerm>({tmp0}) }), std::make_shared<mata::nft::Nft>(nft) ),
Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp1}), std::vector<BasicTerm>({tmp0}) }), nft_ptr ),
Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp1 }), std::vector<BasicTerm>({x5, x1, x2, x3}) }) )
}));
}
Expand Down Expand Up @@ -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<mata::nft::Nft>(nft);

Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({eps}), std::vector<BasicTerm>({x1, x2}) }) );
Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x2, x1, x2}), std::vector<BasicTerm>({x3, x4}) }) );
Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x3, b, x4}), std::vector<BasicTerm>({x5, x1}) }) );
Predicate eq4(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({b, x1}), std::vector<BasicTerm>({eps}) }) );
Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({eps}) }) );
Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1}), std::vector<BasicTerm>({x2}) }), std::make_shared<mata::nft::Nft>(nft) );
Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1}), std::vector<BasicTerm>({x2}) }), nft_ptr );

SECTION("basic") {
Formula conj;
Expand Down Expand Up @@ -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>({
Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5}), std::vector<BasicTerm>() }), std::make_shared<mata::nft::Nft>(nft) ),
Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5}), std::vector<BasicTerm>() }), nft_ptr ),
}));
}
}
Expand Down
12 changes: 7 additions & 5 deletions src/test/noodler/formula.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) {

// result
Predicate switch_res { PredicateType::Transducer, { { y }, { x } }, std::make_shared<mata::nft::Nft>(nft_inv) };
CHECK(pred_trans_switch == switch_res);
CHECK(pred_trans_switch.strong_equals(switch_res));
}

SECTION("Comparison") {
Expand All @@ -46,11 +46,12 @@ TEST_CASE( "Transducer predicate", "[noodler]" ) {

Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft) };
Predicate p2 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft_other) };
Predicate p3 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(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));

Expand All @@ -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<mata::nft::Nft>(nft);


Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft) };
Predicate pres { PredicateType::Transducer, { { x }, { x } }, std::make_shared<mata::nft::Nft>(nft) };
Predicate p1 { PredicateType::Transducer, { { x }, { y } }, nft_ptr };
Predicate pres { PredicateType::Transducer, { { x }, { x } }, nft_ptr };

Formula f{};
f.add_predicate(p1);
Expand Down

0 comments on commit c025e58

Please sign in to comment.