fixing some issues related to tau_ba and its testing

Author: castrod

src/tau.h

@@ -167,8 +167,8 @@ struct tau_ba {
 		auto vars = get_free_vars_from_nso(rr_nso.main);
 		auto wff = rr_nso.main;
 		for(auto& v: vars) wff = build_wff_all<BAs...>(v, wff);
-		auto rr_nso = rr<nso<tau_ba<BAs...>, BAs...>>(rr_nso.rec_relations, wff);
-		auto normalized = normalizer<tau_ba<BAs...>, BAs...>(rr_nso);
+		auto nrr_nso = rr<nso<tau_ba<BAs...>, BAs...>>(rr_nso.rec_relations, wff);
+		auto normalized = normalizer<tau_ba<BAs...>, BAs...>(nrr_nso);
 		auto check = normalized | tau_parser::wff_f;
 		return check.has_value();
 	}
@@ -178,8 +178,8 @@ struct tau_ba {
 		auto vars = get_free_vars_from_nso(rr_nso.main);
 		auto wff = build_wff_neg(rr_nso.main);
 		for(auto& v: vars) wff = build_wff_all<BAs...>(v, wff);
-		auto rr_nso = rr<nso<tau_ba<BAs...>, BAs...>>(rr_nso.rec_relations, wff);
-		auto normalized = normalizer<tau_ba<BAs...>, BAs...>(rr_nso);
+		auto nrr_nso = rr<nso<tau_ba<BAs...>, BAs...>>(rr_nso.rec_relations, wff);
+		auto normalized = normalizer<tau_ba<BAs...>, BAs...>(nrr_nso);
 		auto check = normalized | tau_parser::wff_f;
 		return check.has_value();
 	}

tests/integration/test_integration-tau_ba1.cpp

@@ -45,6 +45,9 @@ TEST_SUITE("operators: negation") {
 	}
 }
 
+// TODO (HIGH) add tests for is_zero
+// TODO (HIGH) add tests for is_one
+
 TEST_SUITE("operators: conjunction") {
 
 	TEST_CASE("(({ : T. } & { : T. }) = 0)") {

tests/integration/test_integration-tau_ba2.cpp

@@ -59,16 +59,36 @@ TEST_SUITE("complex tau_ba formulas") {
 		CHECK( check.has_value() );
 	}*/
 
-	TEST_CASE("tau_ba operators") {
-		auto T = get_tau_ba("( { : ({ : F.} = 0). } = 0 ).");
-		auto F = get_tau_ba("( { : ({ : T.} = 0). } = 0 ).");
-		auto TorF  = T | F;
-		auto TandF = T & F;
-		cout << "T: "     << T     << " \n\tnormal: " << normal(T)     << "\n";
-		cout << "F: "     << F     << " \n\tnormal: " << normal(F)     << "\n";
-		cout << "T | F: " << TorF  << " \n\tnormal: " << normal(TorF)  << "\n";
-		cout << "T & F: " << TandF << " \n\tnormal: " << normal(TandF) << "\n";
-
-		CHECK( true );
+	static auto T = get_tau_ba("( { : ({ : F.} = 0). } = 0 ).");
+	static auto F = get_tau_ba("( { : ({ : T.} = 0). } = 0 ).");
+
+	TEST_CASE("T") {
+		auto normalized = normalizer<tau_ba<bdd_test>, bdd_test>(T.rr_nso);
+		auto check = normalized | tau_parser::wff_t;
+		CHECK( check.has_value() );
+	}
+
+	TEST_CASE("F") {
+		auto normalized = normalizer<tau_ba<bdd_test>, bdd_test>(F.rr_nso);
+		auto check = normalized | tau_parser::wff_f;
+		CHECK( check.has_value() );
+	}
+
+	TEST_CASE("T | F") {
+		auto normalized = normalizer<tau_ba<bdd_test>, bdd_test>((T|F).rr_nso);
+		auto check = normalized | tau_parser::wff_t;
+		CHECK( check.has_value() );
+	}
+
+	TEST_CASE("T & F") {
+		auto normalized = normalizer<tau_ba<bdd_test>, bdd_test>((T&F).rr_nso);
+		auto check = normalized | tau_parser::wff_f;
+		CHECK( check.has_value() );
+	}
+
+	TEST_CASE("T & T") {
+		auto normalized = normalizer<tau_ba<bdd_test>, bdd_test>((T&T).rr_nso);
+		auto check = normalized | tau_parser::wff_t;
+		CHECK( check.has_value() );
 	}
 }