fixing some issues with solver

Author: castrod

src/solver.h

@@ -523,29 +523,60 @@ minterm_system<BAs...> add_minterm_to_disjoint(const minterm_system<BAs...>& dis
 		const minterm<BAs...>& m, const tau<BAs...>& splitter_one) {
 	minterm_system<BAs...> new_disjoint;
 	auto new_m = m;
-	auto new_m_cte = get_constant(new_m);
-	auto new_m_exp = get_exponent(new_m);
 
 	for (auto& d: disjoint) {
+		auto new_m_cte = get_constant(new_m);
+		auto new_m_exp = get_exponent(new_m);
+
+		#ifdef DEBUG
+		BOOST_LOG_TRIVIAL(trace)
+			<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/d: " << d << "\n"
+			<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/new_m: " << new_m << "\n"
+			<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/new_m_cte: " << new_m_cte << "\n"
+			<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/new_m_exp:\n";
+		for (const auto& e: new_m_exp)
+			BOOST_LOG_TRIVIAL(trace)
+				<< "solver.h:" << __LINE__ << "\t" << e;
+		#endif // DEBUG
+
 		// case 1
 		if (get_exponent(d) == new_m_exp) {
+
+			#ifdef DEBUG
+			BOOST_LOG_TRIVIAL(trace)
+				<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case1]/new_disjoint: " << d << "\n";
+			#endif // DEBUG
+
 			new_disjoint.insert(d);
 			continue;
 		}
 		if (auto d_cte = get_constant(d); (d_cte & new_m_cte) != false) {
 			// case 2
-			if ((d_cte & ~new_m_cte) != false)
+			if ((d_cte & ~new_m_cte) != false) {
 				new_disjoint.insert(~new_m_cte & d);
+
+				#ifdef DEBUG
+				BOOST_LOG_TRIVIAL(trace)
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case2]/new_disjoint: " << (~new_m_cte & d) << "\n";
+				#endif // DEBUG
+
 			// case 3
-			else if ((~d_cte & new_m_cte) != false) {
+			} else if ((~d_cte & new_m_cte) != false) {
 				new_disjoint.insert(d);
-				new_m = ~d_cte & new_m;
+				new_m = (~d_cte & new_m) | bf_reduce_canonical<BAs...>();
+
+				#ifdef DEBUG
+				BOOST_LOG_TRIVIAL(trace)
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case3]/new_disjoint: " << d << "\n"
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case3]/new_m: " << new_m << "\n";
+				#endif // DEBUG
+
 			// case 4
 			} else {
 
 				#ifdef DEBUG
 				BOOST_LOG_TRIVIAL(trace)
-					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/d_cte: " << d_cte << "\n";
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case4]/d_cte: " << d_cte << "\n";
 				#endif // DEBUG
 
 				auto s = d_cte == _1<BAs...>
@@ -558,14 +589,27 @@ minterm_system<BAs...> add_minterm_to_disjoint(const minterm_system<BAs...>& dis
 
 				#ifdef DEBUG
 				BOOST_LOG_TRIVIAL(trace)
-					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/s: " << s << "\n";
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case4]/s: " << s << "\n";
 				#endif // DEBUG
 
 				new_disjoint.insert(s & d);
-				new_m = ~s & new_m;
+				new_m = (~s & new_m) | bf_reduce_canonical<BAs...>();
+
+				#ifdef DEBUG
+				BOOST_LOG_TRIVIAL(trace)
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case4]/new_disjoint: " << (s & d) << "\n"
+					<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case4]/new_m: " << new_m << "\n";
+				#endif // DEBUG
 			}
 		// case 5
-		} else new_disjoint.insert(d);
+		} else {
+			new_disjoint.insert(d);
+
+			#ifdef DEBUG
+			BOOST_LOG_TRIVIAL(trace)
+				<< "solver.h:" << __LINE__ << " add_minterm_to_disjoint/[case5]/new_disjoint: " << d << "\n";
+			#endif // DEBUG
+		}
 	}
 	new_disjoint.insert(new_m);
 	return new_disjoint;
@@ -574,9 +618,27 @@ minterm_system<BAs...> add_minterm_to_disjoint(const minterm_system<BAs...>& dis
 template<typename...BAs>
 minterm_system<BAs...> make_minterm_system_disjoint(const minterm_system<BAs...>& sys,
 		const tau<BAs...>& splitter_one) {
+
+	#ifdef DEBUG
+	BOOST_LOG_TRIVIAL(trace)
+		<< "solver.h:" << __LINE__ << " make_minterm_system_disjoint/system: ";
+	for (const auto& minterm : sys)
+		BOOST_LOG_TRIVIAL(trace)
+			<< "solver.h:" << __LINE__ << "\t" << minterm;
+	#endif // DEBUG
+
 	minterm_system<BAs...> disjoints;
 	for (auto it = sys.begin(); it != sys.end(); ++it)
 		disjoints = add_minterm_to_disjoint<BAs...>(disjoints, *it, splitter_one);
+
+	#ifdef DEBUG
+	BOOST_LOG_TRIVIAL(trace)
+		<< "solver.h:" << __LINE__ << " make_minterm_system_disjoint/disjoints: ";
+	for (const auto& minterm : disjoints)
+		BOOST_LOG_TRIVIAL(trace)
+			<< "solver.h:" << __LINE__ << "\t" << minterm;
+	#endif // DEBUG
+
 	return disjoints;
 }
 

tests/integration/test_integration-solver.cpp

@@ -522,17 +522,17 @@ TEST_SUITE("solve_system") {
 		CHECK ( test_solve_system(equality, inequalities) );
 	}
 
-	/*TEST_CASE("two var: y < x && z < y && w < z.") {
-		const char* equality = "y & x' | z & y' | w & z' = 0.";
+	TEST_CASE("two var: y < x && z < y && w < z.") {
+		const char* equality = "x'y | y'z | wz' = 0.";
 		const std::vector<std::string> inequalities =
-			{ "y & x' | x & y' != 0.", "y & z' | z & y' != 0.", "w' & z | w & z' != 0." };
+			{ " w'z|wz' != 0.", "xy' != 0.", "yz' != 0." };
 		CHECK ( test_solve_system(equality, inequalities) );
-	}*/
+	}
 
 	/*TEST_CASE("two var: y < x && y = {a}:sbf && x' != 0.") {
 		const char* equality =  "y'{ a } : sbf|y{ a' } : sbf | yx'= 0.";
 		const std::vector<std::string> inequalities =
-			{ "y & x' | x & y' != 0.", "x' != 0." };
+			{ "y'x|yx' != 0.", "x' != 0." };
 		CHECK ( test_solve_system(equality, inequalities) );
 	}*/