rename BF_TRIVIALITY to BF_(N)EQ_SIMPLIFY

IDNI · Dec 13, 2023 · b758cc1 · b758cc1
1 parent bcc05e0
commit b758cc1
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 25 deletions.
diff --git a/src/normalizer2.h b/src/normalizer2.h
@@ -121,11 +121,10 @@ RULE(BF_DEF_NEQ, "( $X != $Y ) := (( $X + $Y ) != 0).")
 RULE(BF_CALLBACK_EQ, "( { $X } = 0 ) := bf_eq_cb $X T F.") // (T|F) is wff_(t|f)
 RULE(BF_CALLBACK_NEQ, "( { $X } != 0 ) := bf_neq_cb $X T F.") // (T|F) is wff_(t|f)
 
-// TODO (LOW) rename to (N)EQ_SIMPLYFY
-RULE(BF_TRIVIALITY_0, "( 0 = 0 ) := T.")
-RULE(BF_TRIVIALITY_1, "( 1 = 0 ) :=  F.")
-RULE(BF_TRIVIALITY_2, "( 0 != 0 ) := F.")
-RULE(BF_TRIVIALITY_3, "( 1 != 0 ) := T.")
+RULE(BF_EQ_SIMPLIFY_0, "( 1 = 0 ) :=  F.")
+RULE(BF_EQ_SIMPLIFY_1, "( 0 = 0 ) := T.")
+RULE(BF_NEQ_SIMPLIFY_0, "( 0 != 0 ) := F.")
+RULE(BF_NEQ_SIMPLIFY_1, "( 1 != 0 ) := T.")
 
 RULE(BF_POSITIVE_LITERAL_UPWARDS_0, "(($X != 0) && (($Y = 0) && ($Z != 0))) := (($Y = 0) && (($X != 0) && ($Z != 0))).")
 RULE(BF_POSITIVE_LITERAL_UPWARDS_1, "(($X != 0) && (($Y != 0) && ($Z = 0))) := (($Z = 0) && (($X != 0) && ($Y != 0))).")
@@ -273,10 +272,10 @@ static auto bf_elim_quantifiers = make_library<BAs...>(
 
 template<typename... BAs>
 static auto trivialities = make_library<BAs...>(
-	BF_TRIVIALITY_0
-	+ BF_TRIVIALITY_1
-	+ BF_TRIVIALITY_2
-	+ BF_TRIVIALITY_3
+	BF_EQ_SIMPLIFY_0
+	+ BF_EQ_SIMPLIFY_1
+	+ BF_NEQ_SIMPLIFY_0
+	+ BF_NEQ_SIMPLIFY_1
 );
 
 template<typename... BAs>

diff --git a/tests/unit/test_rules-wff_execution.cpp b/tests/unit/test_rules-wff_execution.cpp
@@ -390,8 +390,8 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_0") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_0);
+	TEST_CASE("BF_EQ_SIMPLIFY_0") {
+		auto src_rule = make_tau_source(BF_EQ_SIMPLIFY_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());
@@ -401,8 +401,8 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_1") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_1);
+	TEST_CASE("BF_EQ_SIMPLIFY_1") {
+		auto src_rule = make_tau_source(BF_EQ_SIMPLIFY_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());
@@ -412,8 +412,8 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_2") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_2);
+	TEST_CASE("BF_NEQ_SIMPLIFY_0") {
+		auto src_rule = make_tau_source(BF_NEQ_SIMPLIFY_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());
@@ -423,8 +423,8 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_3") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_3);
+	TEST_CASE("BF_NEQ_SIMPLIFY_1") {
+		auto src_rule = make_tau_source(BF_NEQ_SIMPLIFY_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());

diff --git a/tests/unit/test_rules-wff_parsing.cpp b/tests/unit/test_rules-wff_parsing.cpp
@@ -386,8 +386,8 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_0") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_0);
+	TEST_CASE("BF_EQ_SIMPLIFY_0") {
+		auto src_rule = make_tau_source(BF_EQ_SIMPLIFY_0);
 		auto tau_rule = make_statement(src_rule);
 		auto check = tau_rule
 			| tau_parser::library
@@ -397,8 +397,8 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_1") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_1);
+	TEST_CASE("BF_EQ_SIMPLIFY_1") {
+		auto src_rule = make_tau_source(BF_EQ_SIMPLIFY_1);
 		auto tau_rule = make_statement(src_rule);
 		auto check = tau_rule
 			| tau_parser::library
@@ -408,8 +408,8 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_2") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_2);
+	TEST_CASE("BF_NEQ_SIMPLIFY_0") {
+		auto src_rule = make_tau_source(BF_NEQ_SIMPLIFY_0);
 		auto tau_rule = make_statement(src_rule);
 		auto check = tau_rule
 			| tau_parser::library
@@ -419,8 +419,8 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
-	TEST_CASE("BF_TRIVIALITY_3") {
-		auto src_rule = make_tau_source(BF_TRIVIALITY_3);
+	TEST_CASE("BF_NEQ_SIMPLIFY_1") {
+		auto src_rule = make_tau_source(BF_NEQ_SIMPLIFY_1);
 		auto tau_rule = make_statement(src_rule);
 		auto check = tau_rule
 			| tau_parser::library