adding simplification rules for neg (T|F)

IDNI · Nov 8, 2023 · cddb68e · cddb68e
1 parent a7a555f
commit cddb68e
Show file tree

Hide file tree

Showing 3 changed files with 160 additions and 3 deletions.
diff --git a/src/normalizer2.h b/src/normalizer2.h
@@ -32,10 +32,12 @@ RULE(BF_SIMPLIFY_ONE_0, "( T bf_or $X ) := T.")
 RULE(BF_SIMPLIFY_ONE_1, "( $X bf_or T ) := T.")
 RULE(BF_SIMPLIFY_ONE_2, "( T bf_and $X ) := $X.")
 RULE(BF_SIMPLIFY_ONE_3, "( $X bf_and T ) := $X.")
+RULE(BF_SIMPLIFY_ONE_4, "bf_neg T := F.")
 RULE(BF_SIMPLIFY_ZERO_0, "( F bf_and $X ) := F.")
 RULE(BF_SIMPLIFY_ZERO_1, "( $X bf_and F ) := F.")
 RULE(BF_SIMPLIFY_ZERO_2, "( F bf_or $X ) := $X.")
 RULE(BF_SIMPLIFY_ZERO_3, "( $X bf_or F ) := $X.")
+RULE(BF_SIMPLIFY_ZERO_4, "bf_neg F := T.")
 RULE(BF_SIMPLIFY_SELF_0, "( $X bf_and $X ) := $X.")
 RULE(BF_SIMPLIFY_SELF_1, "( $X bf_or $X ) := $X.")
 RULE(BF_SIMPLIFY_SELF_2, "( $X bf_and bf_neg $X ) := F.")
@@ -72,10 +74,12 @@ RULE(CBF_SIMPLIFY_ONE_0, "( T cbf_or $X ) := T.")
 RULE(CBF_SIMPLIFY_ONE_1, "( $X cbf_or T ) := T.")
 RULE(CBF_SIMPLIFY_ONE_2, "( T cbf_and $X ) := $X.")
 RULE(CBF_SIMPLIFY_ONE_3, "( $X cbf_and T ) := $X.")
+RULE(CBF_SIMPLIFY_ONE_4, "cbf_neg T := F.")
 RULE(CBF_SIMPLIFY_ZERO_0, "( F cbf_and $X ) := F.")
 RULE(CBF_SIMPLIFY_ZERO_1, "( $X cbf_and F ) := F.")
 RULE(CBF_SIMPLIFY_ZERO_2, "( F cbf_or $X ) := $X.")
 RULE(CBF_SIMPLIFY_ZERO_3, "( $X cbf_or F ) := $X.")
+RULE(CBF_SIMPLIFY_ZERO_4, "cbf_neg F := T.")
 RULE(CBF_SIMPLIFY_SELF_0, "( $X cbf_and $X ) := $X.")
 RULE(CBF_SIMPLIFY_SELF_1, "( $X cbf_or $X ) := $X.")
 RULE(CBF_SIMPLIFY_SELF_2, "( $X cbf_and cbf_neg $X ) := F.")
@@ -101,10 +105,12 @@ RULE(WFF_SIMPLIFY_ONE_0, "( T wff_or $X ) := T.")
 RULE(WFF_SIMPLIFY_ONE_1, "( $X wff_or T ) := T.")
 RULE(WFF_SIMPLIFY_ONE_2, "( T wff_and $X ) := $X.")
 RULE(WFF_SIMPLIFY_ONE_3, "( $X wff_and T ) := $X.")
+RULE(WFF_SIMPLIFY_ONE_4, " wff_neg T := F.")
 RULE(WFF_SIMPLIFY_ZERO_0, "( F wff_and $X ) := F.")
 RULE(WFF_SIMPLIFY_ZERO_1, "( $X wff_and F ) := F.")
 RULE(WFF_SIMPLIFY_ZERO_2, "( F wff_or $X ) := $X.")
 RULE(WFF_SIMPLIFY_ZERO_3, "( $X wff_or F ) := $X.")
+RULE(WFF_SIMPLIFY_ZERO_4, "wff_neg F := T.")
 RULE(WFF_SIMPLIFY_SELF_0, "( $X wff_and $X ) := $X.")
 RULE(WFF_SIMPLIFY_SELF_1, "( $X wff_or $X ) := $X.")
 RULE(WFF_SIMPLIFY_SELF_2, "( $X wff_and wff_neg $X ) := F.")
@@ -178,10 +184,12 @@ static auto simplify_bf = make_library<BAs...>(
 	+ BF_SIMPLIFY_ONE_1 
 	+ BF_SIMPLIFY_ONE_2 
 	+ BF_SIMPLIFY_ONE_3
+	+ BF_SIMPLIFY_ONE_4
 	+ BF_SIMPLIFY_ZERO_0 
 	+ BF_SIMPLIFY_ZERO_1 
 	+ BF_SIMPLIFY_ZERO_2 
 	+ BF_SIMPLIFY_ZERO_3
+	+ BF_SIMPLIFY_ZERO_4
 	+ BF_SIMPLIFY_SELF_0 
 	+ BF_SIMPLIFY_SELF_1 
 	+ BF_SIMPLIFY_SELF_2 
@@ -196,10 +204,12 @@ static auto simplify_wff = make_library<BAs...>(
 	+ WFF_SIMPLIFY_ONE_1 
 	+ WFF_SIMPLIFY_ONE_2 
 	+ WFF_SIMPLIFY_ONE_3
+	+ WFF_SIMPLIFY_ONE_4
 	+ WFF_SIMPLIFY_ZERO_0 
 	+ WFF_SIMPLIFY_ZERO_1 
 	+ WFF_SIMPLIFY_ZERO_2 
 	+ WFF_SIMPLIFY_ZERO_3
+	+ WFF_SIMPLIFY_ZERO_4
 	+ WFF_SIMPLIFY_SELF_0 
 	+ WFF_SIMPLIFY_SELF_1 
 	+ WFF_SIMPLIFY_SELF_2 
@@ -214,10 +224,12 @@ static auto simplify_cbf = make_library<BAs...>(
 	+ CBF_SIMPLIFY_ONE_1 
 	+ CBF_SIMPLIFY_ONE_2 
 	+ CBF_SIMPLIFY_ONE_3
+	+ CBF_SIMPLIFY_ONE_4
 	+ CBF_SIMPLIFY_ZERO_0 
 	+ CBF_SIMPLIFY_ZERO_1 
 	+ CBF_SIMPLIFY_ZERO_2 
 	+ CBF_SIMPLIFY_ZERO_3
+	+ CBF_SIMPLIFY_ZERO_4
 	+ CBF_SIMPLIFY_SELF_0 
 	+ CBF_SIMPLIFY_SELF_1 
 	+ CBF_SIMPLIFY_SELF_2 

diff --git a/tests/test_normalizer2.cpp b/tests/test_normalizer2.cpp
@@ -41,15 +41,15 @@ TEST_SUITE("steps parsing") {
 	}
 
 	TEST_CASE("simplify_bf") {
-		CHECK( simplify_bf<Bool>.size() == 14 );
+		CHECK( simplify_bf<Bool>.size() == 16 );
 	}
 
 	TEST_CASE("simplify_wff") {
-		CHECK( simplify_wff<Bool>.size() == 14 );
+		CHECK( simplify_wff<Bool>.size() == 16 );
 	}
 
 	TEST_CASE("simplify_cbf") {
-		CHECK( simplify_cbf<Bool>.size() == 14 );
+		CHECK( simplify_cbf<Bool>.size() == 16 );
 	}
 
 	TEST_CASE("apply_cb") {
@@ -110,3 +110,16 @@ TEST_SUITE("operator|"){
 // TODO (LOW) write tests to check build_wff_coimply
 // TODO (LOW) write tests to check build_wff_all
 // TODO (LOW) write tests to check build_wff_ex
+
+// TODO (MEDIUM) write test to check apply_defs
+// TODO (MEDIUM) write test to check elim_for_all
+// TODO (MEDIUM) write test to check to_dnf_wff
+// TODO (MEDIUM) write test to check to_dnf_cbf
+// TODO (MEDIUM) write test to check simplify_bf
+// TODO (MEDIUM) write test to check simplify_wff
+// TODO (MEDIUM) write test to check simplify_cbf
+// TODO (MEDIUM) write test to check apply_cb
+// TODO (MEDIUM) write test to check squeeze_positives
+// TODO (MEDIUM) write test to check further_process
+// TODO (MEDIUM) write test to check bf_elim_quantifiers
+// TODO (MEDIUM) write test to check trivialities
diff --git a/tests/test_rules.cpp b/tests/test_rules.cpp
@@ -71,6 +71,17 @@ TEST_SUITE("parsing bf rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("BF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(BF_SIMPLIFY_ONE_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::bf_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("BF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(BF_SIMPLIFY_ZERO_0);
 		auto tau_rule = make_statement(src_rule);
@@ -115,6 +126,17 @@ TEST_SUITE("parsing bf rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("BF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(BF_SIMPLIFY_ZERO_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::bf_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("BF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(BF_SIMPLIFY_SELF_0);
 		auto tau_rule = make_statement(src_rule);
@@ -459,6 +481,17 @@ TEST_SUITE("parsing cbf rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("CBF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(CBF_SIMPLIFY_ONE_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::cbf_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("CBF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(CBF_SIMPLIFY_ZERO_0);
 		auto tau_rule = make_statement(src_rule);
@@ -503,6 +536,17 @@ TEST_SUITE("parsing cbf rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("CBF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(CBF_SIMPLIFY_ZERO_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::cbf_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("CBF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(CBF_SIMPLIFY_SELF_0);
 		auto tau_rule = make_statement(src_rule);
@@ -737,6 +781,17 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("WFF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(WFF_SIMPLIFY_ONE_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::wff_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("WFF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(WFF_SIMPLIFY_ZERO_0);
 		auto tau_rule = make_statement(src_rule);
@@ -781,6 +836,17 @@ TEST_SUITE("parsing wff rules") {
 		CHECK( check.has_value() );
 	}
 
+	TEST_CASE("WFF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(WFF_SIMPLIFY_ZERO_4);
+		auto tau_rule = make_statement(src_rule);
+		auto check = tau_rule 
+			| tau_parser::library
+			| tau_parser::rules
+			| tau_parser::rule
+			| tau_parser::wff_rule;
+		CHECK( check.has_value() );
+	}
+
 	TEST_CASE("WFF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(WFF_SIMPLIFY_SELF_0);
 		auto tau_rule = make_statement(src_rule);
@@ -1004,6 +1070,17 @@ TEST_SUITE("executing bf rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("BF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(BF_SIMPLIFY_ONE_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body );
+		CHECK( result == body );
+	}
+
 	TEST_CASE("BF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(BF_SIMPLIFY_ZERO_0);
 		auto statement = make_statement(src_rule);
@@ -1048,6 +1125,17 @@ TEST_SUITE("executing bf rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("BF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(BF_SIMPLIFY_ZERO_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body );
+		CHECK( result == body );
+	}
+
 	TEST_CASE("BF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(BF_SIMPLIFY_SELF_0);
 		auto statement = make_statement(src_rule);
@@ -1482,6 +1570,17 @@ TEST_SUITE("executing cbf rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("CBF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(CBF_SIMPLIFY_ONE_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body );
+		CHECK( result == body );
+	}
+
 	TEST_CASE("CBF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(CBF_SIMPLIFY_ZERO_0);
 		auto statement = make_statement(src_rule);
@@ -1526,6 +1625,17 @@ TEST_SUITE("executing cbf rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("CBF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(CBF_SIMPLIFY_ZERO_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body );
+		CHECK( result == body );
+	}
+
 	TEST_CASE("CBF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(CBF_SIMPLIFY_SELF_0);
 		auto statement = make_statement(src_rule);
@@ -1760,6 +1870,17 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("WFF_SIMPLIFY_ONE_4") { 
+		auto src_rule = make_tau_source(WFF_SIMPLIFY_ONE_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body ); 
+		CHECK( result == body );
+	}
+
 	TEST_CASE("WFF_SIMPLIFY_ZERO_0") {
 		auto src_rule = make_tau_source(WFF_SIMPLIFY_ZERO_0);
 		auto statement = make_statement(src_rule);
@@ -1804,6 +1925,17 @@ TEST_SUITE("executing wff rules") {
 		CHECK( result == body );
 	}
 
+	TEST_CASE("WFF_SIMPLIFY_ZERO_4") {
+		auto src_rule = make_tau_source(WFF_SIMPLIFY_ZERO_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 = tau_apply(tau_rule, matcher);
+		CHECK( matcher != body );
+		CHECK( result == body );
+	}
+
 	TEST_CASE("WFF_SIMPLIFY_SELF_0") {
 		auto src_rule = make_tau_source(WFF_SIMPLIFY_SELF_0);
 		auto statement = make_statement(src_rule);