Defining <, >, <=, == n' != in terms of =0 n' !=0

parser/tau.tgf

@@ -101,8 +101,7 @@ wff_rule		=> wff_matcher definition wff_body dot.
 # needed for rule CBF_DEF_IF
 wff_matcher	=> wff | wff_ref.
 wff_body	=> wff | bf_eq_cb | bf_neq_cb | wff_has_clashing_subformulas_cb
-				| wff_has_subformula_cb | wff_remove_existential
-				| bf_less_cb | bf_less_equal_cb | bf_greater_cb.
+				| wff_has_subformula_cb | wff_remove_existential.
 
 wff_ref			=> sym indexes wff_ref_args.
 wff_ref_args	=> open_parenthesis (variable)* close_parenthesis.
@@ -126,8 +125,10 @@ wff_ex			=> wff_ex_sym (variable|capture|ignore) ws_required wff.
 # they are named bf_* as they involve boolean functions,
 # but they are not boolean functions themselves, they return a T/F wff value
 # and hence, should be considered as wffs
-bf_eq 			=> open_parenthesis bf bf_equality_sym bf_f close_parenthesis.
-bf_neq 			=> open_parenthesis bf bf_nequality_sym bf_f close_parenthesis.
+bf_eq 			=> open_parenthesis bf bf_equality_sym bf close_parenthesis.
+bf_neq 			=> open_parenthesis bf bf_nequality_sym bf close_parenthesis.
+bf_eq 			=> open_parenthesis bf bf_equality_sym bf close_parenthesis.
+bf_neq 			=> open_parenthesis bf bf_nequality_sym bf close_parenthesis.
 bf_less			=> open_parenthesis bf bf_less_sym bf close_parenthesis.
 bf_less_equal	=> open_parenthesis bf bf_less_equal_sym bf close_parenthesis.
 bf_greater		=> open_parenthesis bf bf_greater_sym bf close_parenthesis.
@@ -220,9 +221,6 @@ bf_and_cb			=> bf_cb_arg bf_and_cb_sym bf_cb_arg.
 bf_or_cb			=> bf_cb_arg bf_or_cb_sym bf_cb_arg.
 bf_xor_cb			=> bf_cb_arg bf_xor_cb_sym bf_cb_arg.
 bf_neg_cb			=> bf_neg_cb_sym bf_cb_arg.
-bf_less_cb			=> bf_less_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-bf_less_equal_cb	=> bf_less_equal_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-bf_greater_cb		=> bf_greater_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
 bf_subs_cb			=> bf_subs_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
 bf_eq_cb			=> bf_eq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
 bf_neq_cb			=> bf_neq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
@@ -245,9 +243,6 @@ bf_and_cb_sym			=> ws "bf_and_cb" ws.
 bf_or_cb_sym			=> ws "bf_or_cb" ws.
 bf_xor_cb_sym			=> ws "bf_xor_cb" ws.
 bf_neg_cb_sym			=> ws "bf_neg_cb" ws.
-bf_less_cb_sym			=> ws "bf_less_cb" ws.
-bf_less_equal_cb_sym	=> ws "bf_less_equal_cb" ws.
-bf_greater_cb_sym		=> ws "bf_greater_cb" ws.
 bf_subs_cb_sym			=> ws "bf_subs_cb" ws.
 bf_eq_cb_sym			=> ws "bf_eq_cb" ws.
 bf_neq_cb_sym			=> ws "bf_neq_cb" ws.

src/formula.h

@@ -253,9 +253,6 @@ static const auto is_callback = [](const sp_tau_node<BAs...>& n) {
 		|| nt == tau_parser::bf_or_cb
 		|| nt == tau_parser::bf_xor_cb
 		|| nt == tau_parser::bf_neg_cb
-		|| nt == tau_parser::bf_less_cb
-		|| nt == tau_parser::bf_less_equal_cb
-		|| nt == tau_parser::bf_greater_cb
 		|| nt == tau_parser::bf_subs_cb
 		|| nt == tau_parser::bf_eq_cb
 		|| nt == tau_parser::bf_neq_cb
@@ -1156,9 +1153,6 @@ struct callback_applier {
 			case tau_parser::bf_neq_cb: return apply_equality_relation(_neq, n);
 			case tau_parser::bf_is_one_cb: return apply_constant_check(_is_one, n);
 			case tau_parser::bf_is_zero_cb: return apply_constant_check(_is_zero, n);
-			case tau_parser::bf_less_equal_cb: return apply_order_relation(_less_equal, n);
-			case tau_parser::bf_less_cb: return apply_order_relation(_less, n);
-			case tau_parser::bf_greater_cb: return apply_order_relation(_greater, n);
 			case tau_parser::bf_subs_cb: return apply_subs(n);
 			case tau_parser::bf_has_clashing_subformulas_cb: return apply_bf_clashing_subformulas_check(n);
 			case tau_parser::bf_has_subformula_cb: return apply_has_subformula_check(n, tau_parser::bf_cb_arg);
@@ -1180,16 +1174,31 @@ struct callback_applier {
 	static constexpr auto _equiv = [](const auto& l, const auto& r) { return _imply(l, r) & _imply(r, l); };
 	// unary operation
 	static constexpr auto _neg = [](const auto& l) { return ~l; };
-	// order operations
-	static constexpr auto _less_equal = [](const auto& l, const auto& r) -> bool { return (l & (~r)) == false; };
-	static constexpr auto _greater = [](const auto& l, const auto& r) -> bool { return !_less_equal(l, r); };
-	static constexpr auto _less = [](const auto& l, const auto& r) -> bool { return _less_equal(l,r) && ((l ^ r) != false); };
 	// ternary operators
 	static constexpr auto _eq = [](const auto& l) -> bool { return l == false; };
 	static constexpr auto _neq = [](const auto& l) -> bool { return !(l == false); };
 	static constexpr auto _is_one = [](const auto& l) -> bool { return l == true; };
 	static constexpr auto _is_zero = [](const auto& l) -> bool { return l == false; };
 
+	// TODO (LOW) move this code somewhere else so it could be use everywhere
+	#ifdef DEBUG
+	template<class... Ts>
+	struct overloaded : Ts... { using Ts::operator()...; };
+	template<class... Ts>
+	overloaded(Ts...) -> overloaded<Ts...>;
+
+	std::ostream& print_sp(std::ostream &os, sp_tau_node<BAs...> n) {
+		os << "{";
+		std::visit(overloaded{
+			[&os](tau_source_sym v) { if (v.nt()) os << v.n(); else os << v.t(); },
+			[&os](auto v) { os << "..."; }
+		}, n->value);
+		for (auto& d : n->child) print_sp(os, d);
+		os << "}";
+		return os;
+	}
+	#endif
+
 	void get_leaves(const sp_tau_node<BAs...>& n, tau_parser::nonterminal branch, tau_parser::nonterminal skip, std::vector<sp_tau_node<BAs...>>& leaves) {
 		if (auto check = n | branch; !check.has_value() && is_non_terminal(skip, n)) leaves.push_back(n);
 		else for (auto& c: n->child)
@@ -1226,14 +1235,17 @@ struct callback_applier {
 					gi_changes[var] = x_plus_fx;
 					auto ngi = replace<sp_tau_node<BAs...>>(g_i, gi_changes);
 					auto fex = build_bf_ex<BAs...>(var, ngi)| tau_parser::bf_ex | optional_value_extractor<sp_tau_node<BAs...>>;
-					wff_changes[neq] = build_wff_neq<BAs...>(fex) | tau_parser::bf_neq | optional_value_extractor<sp_tau_node<BAs...>>;
+					auto wff_neq = build_wff_neq<BAs...>(fex)| tau_parser::bf_neq | optional_value_extractor<sp_tau_node<BAs...>>;
+					wff_changes[neq] = wff_neq;
 				}
 			} else {
 				for (auto& neq: select_all(n, is_non_terminal<tau_parser::bf_neq, BAs...>)) {
 					auto g_i = neq | tau_parser::bf | only_child_extractor<BAs...>
 						| optional_value_extractor<sp_tau_node<BAs...>>;
 					auto fex = build_bf_ex<BAs...>(var, g_i)| tau_parser::bf_ex | optional_value_extractor<sp_tau_node<BAs...>>;
-					wff_changes[neq] = build_wff_neq<BAs...>(fex)| tau_parser::bf_neq | optional_value_extractor<sp_tau_node<BAs...>>;
+					auto wff_neq = build_wff_neq<BAs...>(fex)| tau_parser::bf_neq | optional_value_extractor<sp_tau_node<BAs...>>;
+					wff_changes[neq] = wff_neq;
+					// wff_changes[neq] = build_wff_neq<BAs...>(fex)| tau_parser::bf_neq | optional_value_extractor<sp_tau_node<BAs...>>;
 				}
 			}
 		}
@@ -1336,19 +1348,12 @@ struct callback_applier {
 		return std::visit(op, ba_element) ? args[1] : args[0];
 	}
 
-	sp_tau_node<BAs...> apply_order_relation(const auto& op, const sp_tau_node<BAs...>& n) {
-		auto bf_args = n || tau_parser::bf_cb_arg || tau_parser::bf || only_child_extractor<BAs...>;
-		auto wff_args = n || tau_parser::wff_cb_arg || only_child_extractor<BAs...>;
-		auto ba_first_element = bf_args[0] | ba_extractor<BAs...> | optional_value_extractor<std::variant<BAs...>>;;
-		auto ba_second_element = bf_args[1] | ba_extractor<BAs...> | optional_value_extractor<std::variant<BAs...>>;;
-		return std::visit(op, ba_first_element, ba_second_element) ? wff_args[0] : wff_args[1];
-	}
-
 	sp_tau_node<BAs...> apply_subs(const sp_tau_node<BAs...>& n) {
 		auto args = n || tau_parser::bf_cb_arg || only_child_extractor<BAs...>;
 		std::map<sp_tau_node<BAs...>, sp_tau_node<BAs...>> m;
-		m[args[0]] = args[1] | only_child_extractor<BAs...> | optional_value_extractor<sp_tau_node<BAs...>>;
-		return replace<sp_tau_node<BAs...>>(args[2], m);
+		m[args[0]] = args[1];
+		auto tmp = replace<sp_tau_node<BAs...>>(args[2], m)| only_child_extractor<BAs...> | optional_value_extractor<sp_tau_node<BAs...>>;
+		return tmp;
 	}
 };
 

src/normalizer2.h

@@ -28,12 +28,17 @@ namespace idni::tau {
 // IDEA (MEDIUM) add commutative rule and halve the number of rules if is performance friendly
 
 // bf rules
+RULE(BF_DISTRIBUTE_0, "(($X | $Y) & $Z) := (($X & $Z) | ($Y & $Z)).")
+RULE(BF_DISTRIBUTE_1, "($X & ($Y | $Z)) := (($X & $Y) | ($X & $Z)).")
+RULE(BF_PUSH_NEGATION_INWARDS_0, "~ ($X & $Y) := (~ $X | ~ $Y).")
+RULE(BF_PUSH_NEGATION_INWARDS_1, "~ ($X | $Y) := (~ $X & ~ $Y).")
+RULE(BF_ELIM_DOUBLE_NEGATION_0, "~ ~ $X :=  $X.")
 RULE(BF_SIMPLIFY_ONE_0, "( 1 | $X ) := 1.")
 RULE(BF_SIMPLIFY_ONE_1, "( $X | 1 ) := 1.")
 RULE(BF_SIMPLIFY_ONE_2, "( 1 & $X ) := $X.")
 RULE(BF_SIMPLIFY_ONE_3, "( $X & 1 ) := $X.")
 RULE(BF_SIMPLIFY_ONE_4, "~ 1 := 0.")
-RULE(BF_SIMPLIFY_ZERO_0, "( 0 & $X ) := 1.")
+RULE(BF_SIMPLIFY_ZERO_0, "( 0 & $X ) := 0.")
 RULE(BF_SIMPLIFY_ZERO_1, "( $X & 0 ) := 0.")
 RULE(BF_SIMPLIFY_ZERO_2, "( 0 | $X ) := $X.")
 RULE(BF_SIMPLIFY_ZERO_3, "( $X | 0 ) := $X.")
@@ -57,16 +62,9 @@ RULE(BF_CALLBACK_AND, "( { $X } & { $Y } ) := { $X bf_and_cb $Y }.")
 RULE(BF_CALLBACK_OR, "( { $X } | { $Y } ) := { $X bf_or_cb $Y }.")
 RULE(BF_CALLBACK_XOR, "( { $X } + { $Y } ) := { $X bf_xor_cb $Y }.")
 RULE(BF_CALLBACK_NEG, "~ { $X } := { bf_neg_cb $X }.")
-RULE(BF_CALLBACK_LESS, "( { $X } < { $Y } ) := bf_less_cb $X $Y T F.")
-RULE(BF_CALLBACK_LESS_EQUAL, "( { $X } <= { $Y } ) := bf_less_equal_cb $X $Y T F.")
-RULE(BF_CALLBACK_GREATER, "( { $X } > { $Y } ) := bf_greater_cb $X $Y T F.")
 RULE(BF_CALLBACK_IS_ZERO, "{ $X } := bf_is_zero_cb { $X } 0.") // (T|F) is bf_(t|f)
 RULE(BF_CALLBACK_IS_ONE, "{ $X } := bf_is_one_cb { $X } 1.") // (T|F) is bf_(t|f)
 
-// wff callbacks
-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)
-
 // speed up callbacks
 RULE(BF_CALLBACK_CLASHING_SUBFORMULAS_0, "( $X & $Y ) :=  bf_has_clashing_subformulas_cb ( $X & $Y ) 0.")
 RULE(BF_CALLBACK_HAS_SUBFORMULA_0, "( $X & $Y ) := bf_has_subformula_cb ( $X & $Y ) 0 0.")
@@ -105,6 +103,17 @@ RULE(WFF_DEF_CONDITIONAL, "( $X ? $Y : $Z) := (($X -> $Y) && (! $X -> $Z)).")
 RULE(WFF_DEF_IMPLY, "( $X -> $Y ) := ( ! $X || $Y).")
 RULE(WFF_DEF_EQUIV, "( $X <-> $Y ) := (( $X -> $Y ) && ( $Y -> $X )).")
 
+// additional wff dewfinitions (include wff formulas)
+RULE(BF_DEF_LESS_EQUAL, "( $X <= $Y ) := ( ($X & ~ $Y) = 0).")
+RULE(BF_DEF_LESS, "( $X < $Y ) := (( ($X & ~ $Y) = 0) && ( ($X + ~ $Y) != 0)).")
+RULE(BF_DEF_GREATER, "( $X > $Y ) := ((( $X & ~ $Y ) != 0) || (( $X + ~ $Y) = 0)).")
+RULE(BF_DEF_EQ, "( $X = $Y ) := (( $X + $Y ) = 0).")
+RULE(BF_DEF_NEQ, "( $X != $Y ) := (( $X + $Y ) != 0).")
+
+// wff callbacks
+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.")
@@ -122,7 +131,7 @@ RULE(WFF_REMOVE_EX_0, "ex $X $Y := wff_remove_existential_cb $X $Y.")
 
 // TODO (MEDIUM) delete trivial quantified formulas (i.e. ∀x. F = no_x..., ).
 
-// bf defs are just callbacks
+// bf
 template<typename... BAs>
 // TODO (LOW) rename library with rwsys or another name
 static auto apply_defs = make_library<BAs...>(
@@ -135,6 +144,16 @@ static auto apply_defs = make_library<BAs...>(
 	+ BF_DEF_XOR
 );
 
+template<typename... BAs>
+static auto apply_defs_once = make_library<BAs...>(
+	// wff defs
+	BF_DEF_LESS_EQUAL
+	+ BF_DEF_LESS
+	+ BF_DEF_GREATER
+	+ BF_DEF_EQ
+	+ BF_DEF_NEQ
+);
+
 template<typename... BAs>
 static auto elim_for_all = make_library<BAs...>(
 	WFF_ELIM_FORALL
@@ -151,6 +170,15 @@ static auto to_dnf_wff = make_library<BAs...>(
 	+ WFF_ELIM_DOUBLE_NEGATION_0
 );
 
+template<typename... BAs>
+static auto to_dnf_bf = make_library<BAs...>(
+	BF_DISTRIBUTE_0
+	+ BF_DISTRIBUTE_1
+	+ BF_PUSH_NEGATION_INWARDS_0
+	+ BF_PUSH_NEGATION_INWARDS_1
+	+ BF_ELIM_DOUBLE_NEGATION_0
+);
+
 template<typename... BAs>
 static auto simplify_bf = make_library<BAs...>(
 	BF_SIMPLIFY_ONE_0
@@ -197,9 +225,6 @@ static auto apply_cb = make_library<BAs...>(
 	+ BF_CALLBACK_OR
 	+ BF_CALLBACK_XOR
 	+ BF_CALLBACK_NEG
-	+ BF_CALLBACK_LESS
-	+ BF_CALLBACK_LESS_EQUAL
-	+ BF_CALLBACK_GREATER
 	+ BF_CALLBACK_EQ
  	+ BF_CALLBACK_NEQ
 );
@@ -389,14 +414,14 @@ steps<step<library<BAs...>, BAs...>, BAs...> operator|(const steps<step<library<
 	return ns;
 }
 
-template<typename step_t, typename... BAs>
-sp_tau_node<BAs...> operator|(const sp_tau_node<BAs...>& n, const steps<step_t, BAs...>& s) {
+template<typename... BAs>
+sp_tau_node<BAs...> operator|(const sp_tau_node<BAs...>& n, const library<BAs...>& l) {
+	auto s = step<BAs...>(l);
 	return s(n);
 }
 
-template<typename... BAs>
-sp_tau_node<BAs...> operator|(const sp_tau_node<BAs...>& n, const library<BAs...>& l) {
-	auto s = steps<library<BAs...>, BAs...>(l);
+template<typename step_t, typename... BAs>
+sp_tau_node<BAs...> operator|(const sp_tau_node<BAs...>& n, const steps<step_t, BAs...>& s) {
 	return s(n);
 }
 
@@ -440,9 +465,11 @@ formula<BAs...> normalizer_step(formula<BAs...>& form) {
 				| wff_remove_existential<BAs...>)
 			| repeat_all<step<BAs...>, BAs...>(
 				bf_elim_quantifiers<BAs...>
+				| to_dnf_bf<BAs...>
 				| simplify_bf<BAs...>
-				| apply_cb<BAs...>
-				| clause_simplify_bf<BAs...>
+				| apply_cb<BAs...>)
+			| repeat_all<step<BAs...>, BAs...>(
+				clause_simplify_bf<BAs...>
 				| trivialities<BAs...>
 				| to_dnf_wff<BAs...>
 				| simplify_wff<BAs...>
@@ -511,13 +538,27 @@ struct is_equivalent_predicate {
 
 template <typename... BAs>
 formula<BAs...> normalizer(formula<BAs...>& form) {
+	// IDEA extract this to an operator| overload
+	// apply defs to formula
+
+	#ifdef OUTPUT_APPLY_RULES
+	std::cout << "(I): -- Apply once definitions" << std::endl;
+	std::cout << "(F): " << form.main << std::endl;
+	#endif // OUTPUT_APPLY_RULES
+
+	auto nmain = tau_apply(apply_defs_once<BAs...>, form.main);
+	rules<BAs...> nrec_relations;
+	for (const auto& r : form.rec_relations) {
+		nrec_relations.emplace_back(r.first, tau_apply(apply_defs_once<BAs...>, r.second));
+	}
+	formula<BAs...> nform{ nrec_relations, nmain };
 
 	#ifdef OUTPUT_APPLY_RULES
 	std::cout << "(I): -- Begin normalizer" << std::endl;
 	#endif // OUTPUT_APPLY_RULES
 
 	std::vector<sp_tau_node<BAs...>> previous;
-	formula<BAs...> current = normalizer_step(form);
+	formula<BAs...> current = normalizer_step(nform);
 	auto is_equivalent = is_equivalent_predicate<BAs...>(current.main);
 	while (std::find_if(previous.rend(), previous.rbegin(),  is_equivalent) == previous.rend()) {
 		previous.push_back(current.main);

tests/test_builders.cpp

@@ -155,13 +155,12 @@ TEST_SUITE("builders execution") {
 	static constexpr char* sample =	" ( ?X = 0 ) .";
 	auto src = make_tau_source(sample);
 	auto frml = make_statement(src);
-	auto X = frml
+	auto bfs = frml
 		| tau_parser::formula | tau_parser::main | tau_parser::wff
-		| tau_parser::bf_eq | tau_parser::bf | tau_parser::variable
+		| tau_parser::bf_eq || tau_parser::bf;
+	auto X = bfs[0] | tau_parser::variable
 		| optional_value_extractor<sp_tau_node<Bool>>;
-	auto F = frml
-		| tau_parser::formula | tau_parser::main | tau_parser::wff
-		| tau_parser::bf_eq | tau_parser::bf_f
+	auto F = bfs[1] | tau_parser::bf_f
 		| optional_value_extractor<sp_tau_node<Bool>>;
 
 	TEST_CASE("BLDR_WFF_EQ") {