From b758cc1632b5725ba9fe7a59f46aaf46c7259bc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Klapka?= Date: Wed, 13 Dec 2023 13:54:02 +0100 Subject: [PATCH] rename BF_TRIVIALITY to BF_(N)EQ_SIMPLIFY --- src/normalizer2.h | 17 ++++++++--------- tests/unit/test_rules-wff_execution.cpp | 16 ++++++++-------- tests/unit/test_rules-wff_parsing.cpp | 16 ++++++++-------- 3 files changed, 24 insertions(+), 25 deletions(-) diff --git a/src/normalizer2.h b/src/normalizer2.h index ad5f6935..3e45e981 100644 --- 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( template static auto trivialities = make_library( - 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 diff --git a/tests/unit/test_rules-wff_execution.cpp b/tests/unit/test_rules-wff_execution.cpp index f0a86413..06e32362 100644 --- 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 index dacbc7e9..ff82f9f0 100644 --- 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