Replaced semantic zero/one check with syntactic zero/one check in hoo…

…ks. Semantic reduction is instead done during normalization.

src/boolean_algebras/bdds/bdd_handle.h

@@ -76,6 +76,12 @@ hbdd<B, o> operator~(const hbdd<B, o>& x) { return ~(*x); }
 template<typename B, auto o = bdd_options<>::create()>
 hbdd<B, o> normalize (const hbdd<B, o>& x) {return x;}
 
+template<typename B, auto o = bdd_options<>::create()>
+bool is_syntactic_one (const hbdd<B, o>& x) {return x->is_one();}
+
+template<typename B, auto o = bdd_options<>::create()>
+bool is_syntactic_zero (const hbdd<B, o>& x) {return x->is_zero();}
+
 template<typename B, auto o = bdd_options<>::create()>
 hbdd<B, o> splitter (const hbdd<B, o>& x, splitter_type st) {
 	return x->splitter(st);

src/boolean_algebras/bool_ba.cpp

@@ -34,6 +34,14 @@ Bool normalize(const Bool &b) {
 	return b;
 }
 
+bool is_syntactic_one(const Bool& b) {
+	return b.is_one();
+}
+
+bool is_syntactic_zero(const Bool& b) {
+	return b.is_zero();
+}
+
 std::ostream& operator<<(std::ostream& os, const Bool& b) {
 	return os << (b.b ? 1 : 0);
 }

src/boolean_algebras/bool_ba.h

@@ -25,6 +25,9 @@ struct Bool {
 };
 
 Bool normalize (const Bool& b);
+bool is_syntactic_one (const Bool& b);
+bool is_syntactic_zero(const Bool& b);
+
 
 template<>
 struct std::hash<Bool> {

src/boolean_algebras/tau_ba.tmpl.h

@@ -119,10 +119,21 @@ bool operator!=(const bool& b, const tau_ba<BAs...>& other) {
 
 template<typename... BAs>
 auto normalize (const tau_ba<BAs...>& fm) {
-	auto res = normalizer<tau_ba<BAs...>, BAs...>(fm.nso_rr);
+	auto res = apply_rr_to_formula<tau_ba<BAs...>, BAs...>(fm.nso_rr);
+	res = simp_tau_unsat_valid(res);
 	return tau_ba<BAs...>(res);
 }
 
+template<typename... BAs>
+bool is_syntactic_one(const tau_ba<BAs...>& fm) {
+	return fm.nso_rr.main == _T<tau_ba<BAs...>, BAs...>;
+}
+
+template<typename... BAs>
+bool is_syntactic_zero(const tau_ba<BAs...>& fm) {
+	return fm.nso_rr.main == _F<tau_ba<BAs...>, BAs...>;
+}
+
 template<typename... BAs>
 auto splitter (const tau_ba<BAs...>& fm, splitter_type st) {
 	auto s = tau_splitter(normalizer(fm.nso_rr), st);
@@ -138,7 +149,7 @@ template<typename... BAs>
 bool is_closed (const tau_ba<BAs...>& fm) {
 	using p = tau_parser;
 	auto simp_fm = apply_rr_to_formula(fm.nso_rr);
-	if (!simp_fm) return false; // TODO (MEDIUM) check if this is correct
+	if (!simp_fm) return false;
 	if (find_top(simp_fm, is_non_terminal<tau_parser::ref, tau_ba<BAs...>, BAs...>))
 		return false;
 	auto vars = get_free_vars_from_nso(simp_fm);

src/boolean_algebras/variant_ba.h

@@ -72,6 +72,24 @@ std::variant<BAs...> normalize_ba(const std::variant<BAs...>& elem) {
 	), elem);
 }
 
+template <typename... BAs>
+bool is_syntactic_one(const std::variant<BAs...>& elem) {
+	return std::visit(overloaded(
+			[](const auto& el) {
+				return is_syntactic_one(el);
+			}
+		), elem);
+}
+
+template <typename... BAs>
+bool is_syntactic_zero(const std::variant<BAs...>& elem) {
+	return std::visit(overloaded(
+			[](const auto& el) {
+				return is_syntactic_zero(el);
+			}
+		), elem);
+}
+
 template<typename... BAs>
 std::variant<BAs...> splitter_ba(const std::variant<BAs...>& elem, splitter_type st) {
 	return std::visit(overloaded(
@@ -83,7 +101,7 @@ std::variant<BAs...> splitter_ba(const std::variant<BAs...>& elem, splitter_type
 
 template<typename... BAs>
 std::variant<BAs...> splitter_ba(const std::variant<BAs...>& elem) {
-	return splitter_ba(elem, splitter_type::middle);
+	return splitter_ba(elem, splitter_type::upper);
 }
 
 template<typename...BAs>

src/hooks.tmpl.h

@@ -335,6 +335,7 @@ tau<BAs...> make_node_hook_bf_xor(const rewriter::node<tau_sym<BAs...>>& n) {
 	return  build_bf_xor<BAs...>(first_argument_formula(n), second_argument_formula(n));
 }
 
+// Simplify constants being syntactically true or false
 template <typename...BAs>
 tau<BAs...> make_node_hook_cte(const rewriter::node<tau_sym<BAs...>>& n)
 {
@@ -343,13 +344,11 @@ tau<BAs...> make_node_hook_cte(const rewriter::node<tau_sym<BAs...>>& n)
 		| tau_parser::constant
 		| only_child_extractor<BAs...>
 		| ba_extractor<BAs...>;
-	//RULE(BF_CALLBACK_IS_ZERO, "{ $X } := bf_is_zero_cb { $X } 1.")
-	//RULE(BF_CALLBACK_IS_ONE, "{ $X } := bf_is_one_cb { $X } 1.")
 	if (l.has_value()) {
 		auto typed = n | tau_parser::bf_constant | tau_parser::type;
-		if (l.value() == false)
+		if (is_syntactic_zero(l.value()))
 			return typed.has_value() ? build_bf_f_type(typed.value()) : _0<BAs...>;
-		else if (l.value() == true)
+		else if (is_syntactic_one(l.value()))
 			return typed.has_value() ? build_bf_t_type(typed.value()) : _1<BAs...>;
 	}
 	return std::make_shared<rewriter::node<tau_sym<BAs...>>>(n);

src/normal_forms.h

@@ -862,7 +862,7 @@ bool assign_and_reduce(const tau<BAs...>& fm,
 		if (!is_wff) {
 			// fm is a Boolean function
 			// Normalize tau subformulas
-			fm_simp = fm | (tau_transform<BAs...>)normalize_ba<BAs...>;
+			fm_simp = normalize_ba<BAs...>(fm);
 			fm_simp = to_dnf2(fm_simp, false);
 			fm_simp = reduce2(fm_simp, tau_parser::bf);
 

src/satisfiability.h

@@ -1109,6 +1109,27 @@ bool are_tau_equivalent (const tau<BAs...>& f1, const tau<BAs...>& f2) {
 	return true;
 }
 
+template<typename... BAs>
+tau<BAs...> simp_tau_unsat_valid(const tau<BAs...>& fm, const int_t start_time = 0,
+			const bool output = false) {
+	BOOST_LOG_TRIVIAL(debug) << "(I) Start simp_tau_unsat_valid";
+	BOOST_LOG_TRIVIAL(debug) << "(F) " << fm;
+	// Check if formula is valid
+	if (is_tau_impl(_T<BAs...>, fm)) return _T<BAs...>;
+	auto normalized_fm = normalize_with_temp_simp(fm);
+	auto clauses = get_leaves(normalized_fm, tau_parser::wff_or,
+				  tau_parser::wff);
+
+	// Check satisfiability of each clause
+	for (auto& clause: clauses) {
+		if (transform_to_execution(clause, start_time, output) == _F<BAs...>)
+			clause = _F<BAs...>;
+	}
+
+	BOOST_LOG_TRIVIAL(debug) << "(I) End simp_tau_unsat_valid";
+	return build_wff_or<BAs...>(clauses);
+}
+
 /*
  *  Possible tests:
  *  (o1[t-1] = 0 -> o1[t] = 1) && (o1[t-1] = 1 -> o1[t] = 0) && o1[0] = 0, passing