Recurse weak and strong implication at the same time

This is particularly useful for implication as used in refutation proofs
with "NOT x" clauses. We don't plumb through external callers this way
since they are generally interested in one or the other.

Author: jcoleman

src/backend/optimizer/util/predtest.c

@@ -79,9 +79,12 @@ typedef struct PredIterInfoData
 		(info).cleanup_fn(&(info)); \
 	} while (0)
 
+typedef int ImplicationType;
+#define STRONG ((ImplicationType) 0x01)
+#define WEAK ((ImplicationType) 0x02)
 
 static bool predicate_implied_by_recurse(Node *clause, Node *predicate,
-										 bool weak);
+										 ImplicationType implication_mask);
 static bool predicate_refuted_by_recurse(Node *clause, Node *predicate,
 										 bool weak);
 static PredClass predicate_classify(Node *clause, PredIterInfo info);
@@ -96,11 +99,11 @@ static void arrayexpr_startup_fn(Node *clause, PredIterInfo info);
 static Node *arrayexpr_next_fn(PredIterInfo info);
 static void arrayexpr_cleanup_fn(PredIterInfo info);
 static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
-											   bool weak);
+											   ImplicationType implication_mask);
 static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 											   bool weak);
 static bool predicate_implied_not_null_by_clause(Expr *predicate, Node *clause,
-												 bool weak);
+												 ImplicationType implication_mask);
 static Node *extract_not_arg(Node *clause);
 static Node *extract_strong_not_arg(Node *clause);
 static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false);
@@ -178,7 +181,7 @@ predicate_implied_by(List *predicate_list, List *clause_list,
 		c = (Node *) clause_list;
 
 	/* And away we go ... */
-	return predicate_implied_by_recurse(c, p, weak);
+	return predicate_implied_by_recurse(c, p, weak ? WEAK : STRONG);
 }
 
 /*
@@ -295,7 +298,7 @@ predicate_refuted_by(List *predicate_list, List *clause_list,
  */
 static bool
 predicate_implied_by_recurse(Node *clause, Node *predicate,
-							 bool weak)
+							 ImplicationType implication_mask)
 {
 	PredIterInfoData clause_info;
 	PredIterInfoData pred_info;
@@ -323,7 +326,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_implied_by_recurse(clause, pitem,
-														  weak))
+														  implication_mask))
 						{
 							result = false;
 							break;
@@ -343,7 +346,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_implied_by_recurse(clause, pitem,
-														 weak))
+														 implication_mask))
 						{
 							result = true;
 							break;
@@ -361,7 +364,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_implied_by_recurse(citem, predicate,
-														 weak))
+														 implication_mask))
 						{
 							result = true;
 							break;
@@ -379,7 +382,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_implied_by_recurse(citem, predicate,
-														 weak))
+														 implication_mask))
 						{
 							result = true;
 							break;
@@ -407,7 +410,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 						iterate_begin(pitem, predicate, pred_info)
 						{
 							if (predicate_implied_by_recurse(citem, pitem,
-															 weak))
+															 implication_mask))
 							{
 								presult = true;
 								break;
@@ -435,7 +438,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (!predicate_implied_by_recurse(citem, predicate,
-														  weak))
+														  implication_mask))
 						{
 							result = false;
 							break;
@@ -458,7 +461,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_implied_by_recurse(clause, pitem,
-														  weak))
+														  implication_mask))
 						{
 							result = false;
 							break;
@@ -476,7 +479,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_implied_by_recurse(clause, pitem,
-														 weak))
+														 implication_mask))
 						{
 							result = true;
 							break;
@@ -493,7 +496,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					return
 						predicate_implied_by_simple_clause((Expr *) predicate,
 														   clause,
-														   weak);
+														   implication_mask);
 			}
 			break;
 	}
@@ -627,7 +630,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 false))
+													 STRONG))
 						return true;
 
 					/*
@@ -709,7 +712,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 false))
+													 STRONG))
 						return true;
 
 					/*
@@ -736,26 +739,24 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 			 * If A is a strong NOT-clause, A R=> B if B => A's arg
 			 *
 			 * Since A is strong, we may assume A's arg is false (not just
-			 * not-true).  If B weakly implies A's arg, then B can be neither
-			 * true nor null, so that strong refutation is proven.  If B
-			 * strongly implies A's arg, then B cannot be true, so that weak
-			 * refutation is proven.
+			 * not-true). If B strongly implies A's arg, then B cannot be true,
+			 * so that weak refutation is proven. If B weakly implies A's arg,
+			 * then B can be neither true nor null, so that strong refutation
+			 * are proven. In that case we can also prove weak refutation since
+			 * if B must be false, then surely it is not true.
 			 */
 			not_arg = extract_strong_not_arg(clause);
-			if (not_arg &&
-				predicate_implied_by_recurse(predicate, not_arg,
-											 !weak))
-				return true;
+			if (not_arg)
+			{
+				int useful_implications = weak ? STRONG : WEAK;
 
-			/*
-			 * Because weak refutation expands the allowed outcomes for B
-			 * from "false" to "false or null", we can additionally prove
-			 * weak refutation in the case that strong refutation is proven.
-			 */
-			if (weak && not_arg &&
-				predicate_implied_by_recurse(predicate, not_arg,
-											 true))
-				return true;
+				if (weak)
+					useful_implications |= WEAK;
+
+				if (predicate_implied_by_recurse(predicate, not_arg,
+												 useful_implications))
+					return true;
+			}
 
 			switch (pclass)
 			{
@@ -805,7 +806,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 false))
+													 STRONG))
 						return true;
 
 					/*
@@ -1113,8 +1114,12 @@ arrayexpr_cleanup_fn(PredIterInfo info)
  */
 static bool
 predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
-								   bool weak)
+								   ImplicationType implication_mask)
 {
+	bool		weak = implication_mask & WEAK;
+	bool		strong = implication_mask & STRONG;
+
+
 	/* Allow interrupting long proof attempts */
 	CHECK_FOR_INTERRUPTS();
 
@@ -1302,7 +1307,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 						 * must be not null.
 						 */
 						if (predicate_implied_not_null_by_clause(predntest->arg,
-																 clause, weak))
+																 clause, implication_mask))
 							return true;
 						break;
 					case IS_NULL:
@@ -1332,7 +1337,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 						 * We can only prove strong implication here since
 						 * "null is true" is false rather than null.
 						 */
-						if (!weak && equal(clause, predbtest->arg))
+						if (strong && equal(clause, predbtest->arg))
 							return true;
 						break;
 					case IS_FALSE:
@@ -1342,7 +1347,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 						 * We can only prove strong implication here since "not
 						 * null" is null rather than true.
 						 */
-						if (!weak && is_notclause(clause) &&
+						if (strong && is_notclause(clause) &&
 							equal(get_notclausearg(clause), predbtest->arg))
 							return true;
 						break;
@@ -1401,7 +1406,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 						 *
 						 * For example: truth of x implies x is not unknown.
 						 */
-						if (predicate_implied_not_null_by_clause(predbtest->arg, clause, weak))
+						if (predicate_implied_not_null_by_clause(predbtest->arg, clause, implication_mask))
 							return true;
 						break;
 				}
@@ -1444,7 +1449,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
  * cycles on at this point.
  */
 static bool
-predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, bool weak)
+predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, ImplicationType implication_mask)
 {
 	switch (nodeTag(clause))
 	{
@@ -1517,7 +1522,7 @@ predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, bool weak)
 	 * work for weak implication, though, since the clause yielding the
 	 * non-false value NULL means the predicate will evaluate to false.
 	 */
-	if (!weak && clause_is_strict_for(clause, (Node *) predicate, true))
+	if (implication_mask & STRONG && clause_is_strict_for(clause, (Node *) predicate, true))
 		return true;
 
 	return false;
@@ -1578,7 +1583,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * = false" would mean both our clause and our
 							 * predicate would evaluate to "false".
 							 */
-							if (predicate_implied_not_null_by_clause(clausentest->arg, (Node *) predicate, true))
+							if (predicate_implied_not_null_by_clause(clausentest->arg, (Node *) predicate, WEAK))
 								return true;
 
 							/*
@@ -1588,7 +1593,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * in the predicate, it's known immutable).
 							 */
 							if (weak &&
-								clause_is_strict_for((Node *) predicate, (Node *) clausentest->arg, true))
+								clause_is_strict_for((Node *) predicate, (Node *) clausentest->arg, WEAK))
 								return true;
 
 							return false;	/* we can't succeed below... */
@@ -1665,7 +1670,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * = false" would mean both our clause and our
 							 * predicate would evaluate to "false".
 							 */
-							if (predicate_implied_not_null_by_clause(clausebtest->arg, (Node *) predicate, true))
+							if (predicate_implied_not_null_by_clause(clausebtest->arg, (Node *) predicate, WEAK))
 								return true;
 
 							/*
@@ -1728,7 +1733,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * refutation is a strict superset of weak
 							 * refutation.
 							 */
-							if (predicate_implied_not_null_by_clause(predntest->arg, clause, false))
+							if (predicate_implied_not_null_by_clause(predntest->arg, clause, STRONG))
 								return true;
 						}
 						break;
@@ -1759,7 +1764,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * refutation is a strict superset of weak
 							 * refutation.
 							 */
-							if (predicate_implied_not_null_by_clause(predbtest->arg, clause, false))
+							if (predicate_implied_not_null_by_clause(predbtest->arg, clause, STRONG))
 								return true;
 
 							return false;			/* we can't succeed below... */