From 3d536736ef95d055b229502a0bc66dc0af2913ab Mon Sep 17 00:00:00 2001 From: castrod Date: Tue, 26 Dec 2023 20:13:11 +0100 Subject: [PATCH] adding tests for collapsing positives tau rules --- src/tau.h | 24 +++-- tests/unit/test_rules-tau_execution.cpp | 119 +++++++++++++++++++++++ tests/unit/test_rules-tau_parsing.cpp | 121 ++++++++++++++++++++++++ 3 files changed, 251 insertions(+), 13 deletions(-) diff --git a/src/tau.h b/src/tau.h index bb4b3083..4293033b 100644 --- a/src/tau.h +++ b/src/tau.h @@ -54,18 +54,17 @@ RULE(TAU_SIMPLIFY_SELF_3, "( $X ||| % $X ) := T.") RULE(TAU_SIMPLIFY_SELF_4, "( % $X &&& $X ) := F.") RULE(TAU_SIMPLIFY_SELF_5, "( % $X ||| $X ) := T.") -RULE(TAU_COLLAPSE_POSITIVES_0, "($X &&& $Y) := tau_collapse_positives $X $Y.") -RULE(TAU_COLLAPSE_POSITIVES_1, "($X &&& ($Y &&& $Z)) := tau_collapse_positives $X $Y $Z.") -RULE(TAU_COLLAPSE_POSITIVES_2, "($X &&& ($Y &&& $Z)) := tau_collapse_positives $X $Z $Y.") -RULE(TAU_COLLAPSE_POSITIVES_3, "($X &&& ($Y &&& $Z)) := tau_collapse_positives $Y $Z $X.") -RULE(TAU_COLLAPSE_POSITIVES_4, "(($X &&& $Y) &&& $Z)) := tau_collapse_positives $Y $Z $X.") -RULE(TAU_COLLAPSE_POSITIVES_5, "(($X &&& $Y) &&& $Z)) := tau_collapse_positives $X $Z $Y.") -RULE(TAU_COLLAPSE_POSITIVES_6, "(($X &&& $Y) &&& $Z)) := tau_collapse_positives $X $Y $Z.") -RULE(TAU_PUSH_POSITIVES_UPWARDS_0, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Y ($Y &&& ($X &&& $Z).") -RULE(TAU_PUSH_POSITIVES_UPWARDS_1, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Z ($Z &&& ($X &&& $Y).") -RULE(TAU_PUSH_POSITIVES_UPWARDS_2, "(($X &&& $Y) &&& $Z) := tau_positives_upwards $X ($X &&& ($Y &&& $Z).") -RULE(TAU_PUSH_POSITIVES_UPWARDS_3, "(($X &&& $Y) &&& $Z) := tau_positives_upwards $Y ($Y &&& ($X &&& $Z).") -RULE(TAU_PUSH_POSITIVES_UPWARDS_4, "($X &&& $Y) := ($Y &&& $X).") +RULE(TAU_COLLAPSE_POSITIVES_0, "($X &&& $Y) := tau_collapse_positives_cb $X $Y.") +RULE(TAU_COLLAPSE_POSITIVES_1, "($X &&& ($Y &&& $Z)) := tau_collapse_positives_cb $X $Y $Z.") +RULE(TAU_COLLAPSE_POSITIVES_2, "($X &&& ($Y &&& $Z)) := tau_collapse_positives_cb $X $Z $Y.") +RULE(TAU_COLLAPSE_POSITIVES_3, "($X &&& ($Y &&& $Z)) := tau_collapse_positives_cb $Y $Z $X.") +RULE(TAU_COLLAPSE_POSITIVES_4, "(($X &&& $Y) &&& $Z) := tau_collapse_positives_cb $Y $Z $X.") +RULE(TAU_COLLAPSE_POSITIVES_5, "(($X &&& $Y) &&& $Z) := tau_collapse_positives_cb $X $Z $Y.") +RULE(TAU_COLLAPSE_POSITIVES_6, "(($X &&& $Y) &&& $Z) := tau_collapse_positives_cb $X $Y $Z.") +RULE(TAU_PUSH_POSITIVES_UPWARDS_0, "($X &&& ($Y &&& $Z)) := tau_positives_upwards_cb $Y ($Y &&& ($X &&& $Z)).") +RULE(TAU_PUSH_POSITIVES_UPWARDS_1, "($X &&& ($Y &&& $Z)) := tau_positives_upwards_cb $Z ($Z &&& ($X &&& $Y)).") +RULE(TAU_PUSH_POSITIVES_UPWARDS_2, "(($X &&& $Y) &&& $Z) := tau_positives_upwards_cb $X ($X &&& ($Y &&& $Z)).") +RULE(TAU_PUSH_POSITIVES_UPWARDS_3, "(($X &&& $Y) &&& $Z) := tau_positives_upwards_cb $Y ($Y &&& ($X &&& $Z)).") template static auto to_dnf_tau = make_library( @@ -109,7 +108,6 @@ static auto collapse_positives_tau = make_library( + TAU_PUSH_POSITIVES_UPWARDS_1 + TAU_PUSH_POSITIVES_UPWARDS_2 + TAU_PUSH_POSITIVES_UPWARDS_3 - + TAU_PUSH_POSITIVES_UPWARDS_4 ); // Check https://gcc.gnu.org/bugzilla/show_bug.cgi?id=102609 to follow up on diff --git a/tests/unit/test_rules-tau_execution.cpp b/tests/unit/test_rules-tau_execution.cpp index 42498046..d35ce871 100644 --- a/tests/unit/test_rules-tau_execution.cpp +++ b/tests/unit/test_rules-tau_execution.cpp @@ -260,5 +260,124 @@ TEST_SUITE("executing tau rules") { CHECK( result == body ); } + TEST_CASE("TAU_COLLAPSE_POSITIVES_0") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_0); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + TEST_CASE("TAU_COLLAPSE_POSITIVES_1") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_1); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_2") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_2); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_3") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_3); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_4") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_4); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_5") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_5); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_6") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_6); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_0") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_0); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_1") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_1); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_2") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_2); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_3") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_3); + auto statement = make_statement(src_rule); + auto rule = statement | tau_parser::library| tau_parser::rules | tau_parser::rule; + auto tau_rule = make_rule(rule.value()); + auto [matcher, body] = tau_rule; + auto result = formula_apply(tau_rule, matcher); + CHECK( matcher != body ); + CHECK( result == body ); + } } diff --git a/tests/unit/test_rules-tau_parsing.cpp b/tests/unit/test_rules-tau_parsing.cpp index efd2ff24..38851039 100644 --- a/tests/unit/test_rules-tau_parsing.cpp +++ b/tests/unit/test_rules-tau_parsing.cpp @@ -225,4 +225,125 @@ TEST_SUITE("parsing tau rules") { | tau_parser::tau_rule; CHECK( check.has_value() ); } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_0") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_0); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_1") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_1); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_2") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_2); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_3") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_3); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_4") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_4); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_5") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_5); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_COLLAPSE_POSITIVES_6") { + auto src_rule = make_tau_source(TAU_COLLAPSE_POSITIVES_6); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_0") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_0); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_1") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_1); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_2") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_2); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } + + TEST_CASE("TAU_PUSH_POSITIVES_UPWARDS_3") { + auto src_rule = make_tau_source(TAU_PUSH_POSITIVES_UPWARDS_3); + auto tau_rule = make_statement(src_rule); + auto check = tau_rule + | tau_parser::library + | tau_parser::rules + | tau_parser::rule + | tau_parser::tau_rule; + CHECK( check.has_value() ); + } }