adding tests for collapsing positives tau rules

IDNI · Dec 26, 2023 · 3d53673 · 3d53673
1 parent 19bdc3e
commit 3d53673
Show file tree

Hide file tree

Showing 3 changed files with 251 additions and 13 deletions.
diff --git 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<typename... BAs>
 static auto to_dnf_tau = make_library<BAs...>(
@@ -109,7 +108,6 @@ static auto collapse_positives_tau = make_library<BAs...>(
 	+ 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
@@ -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
@@ -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() );
+	}
 }