]> git.ipfire.org Git - thirdparty/postgresql.git/commitdiff
Refactor predicate_{implied,refuted}_by_simple_clause.
authorTom Lane <tgl@sss.pgh.pa.us>
Mon, 25 Mar 2024 21:45:15 +0000 (17:45 -0400)
committerTom Lane <tgl@sss.pgh.pa.us>
Mon, 25 Mar 2024 21:45:15 +0000 (17:45 -0400)
Put the node-type-dependent operations into switches on nodeTag.
This should ease addition of new proof rules for other expression
node types.  There is no functional change, although some tests
are made in a different order than before.

Also, add a couple of new cross-checks in test_predtest.c.

James Coleman (part of a larger patch series)

Discussion: https://postgr.es/m/CAAaqYe8Bo4bf_i6qKj8KBsmHMYXhe3Xt6vOe3OBQnOaf3_XBWg@mail.gmail.com

src/backend/optimizer/util/predtest.c
src/test/modules/test_predtest/test_predtest.c

index c37b416e24e8ed44bb617bba44b07355f579323a..6e3b376f3d35ae9d697a2101efc43dff6dd7f903 100644 (file)
@@ -1087,38 +1087,12 @@ arrayexpr_cleanup_fn(PredIterInfo info)
 }
 
 
-/*----------
+/*
  * predicate_implied_by_simple_clause
  *       Does the predicate implication test for a "simple clause" predicate
  *       and a "simple clause" restriction.
  *
  * We return true if able to prove the implication, false if not.
- *
- * We have several strategies for determining whether one simple clause
- * implies another:
- *
- * A simple and general way is to see if they are equal(); this works for any
- * kind of expression, and for either implication definition.  (Actually,
- * there is an implied assumption that the functions in the expression are
- * immutable --- but this was checked for the predicate by the caller.)
- *
- * Another way that always works is that for boolean x, "x = TRUE" is
- * equivalent to "x", likewise "x = FALSE" is equivalent to "NOT x".
- * These can be worth checking because, while we preferentially simplify
- * boolean comparisons down to "x" and "NOT x", the other form has to be
- * dealt with anyway in the context of index conditions.
- *
- * If the predicate is of the form "foo IS NOT NULL", and we are considering
- * strong implication, we can conclude that the predicate is implied if the
- * clause is strict for "foo", i.e., it must yield false or NULL when "foo"
- * is NULL.  In that case truth of the clause ensures that "foo" isn't NULL.
- * (Again, this is a safe conclusion because "foo" must be immutable.)
- * This doesn't work for weak implication, though.
- *
- * Finally, if both clauses are binary operator expressions, we may be able
- * to prove something using the system's knowledge about operators; those
- * proof rules are encapsulated in operator_predicate_proof().
- *----------
  */
 static bool
 predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
@@ -1127,97 +1101,125 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
        /* Allow interrupting long proof attempts */
        CHECK_FOR_INTERRUPTS();
 
-       /* First try the equal() test */
+       /*
+        * A simple and general rule is that a clause implies itself, hence we
+        * check if they are equal(); this works for any kind of expression, and
+        * for either implication definition.  (Actually, there is an implied
+        * assumption that the functions in the expression are immutable --- but
+        * this was checked for the predicate by the caller.)
+        */
        if (equal((Node *) predicate, clause))
                return true;
 
-       /* Next see if clause is boolean equality to a constant */
-       if (is_opclause(clause) &&
-               ((OpExpr *) clause)->opno == BooleanEqualOperator)
+       /* Next we have some clause-type-specific strategies */
+       switch (nodeTag(clause))
        {
-               OpExpr     *op = (OpExpr *) clause;
-               Node       *rightop;
-
-               Assert(list_length(op->args) == 2);
-               rightop = lsecond(op->args);
-               /* We might never see a null Const here, but better check anyway */
-               if (rightop && IsA(rightop, Const) &&
-                       !((Const *) rightop)->constisnull)
-               {
-                       Node       *leftop = linitial(op->args);
-
-                       if (DatumGetBool(((Const *) rightop)->constvalue))
+               case T_OpExpr:
                        {
-                               /* X = true implies X */
-                               if (equal(predicate, leftop))
-                                       return true;
+                               OpExpr     *op = (OpExpr *) clause;
+
+                               /*----------
+                                * For boolean x, "x = TRUE" is equivalent to "x", likewise
+                                * "x = FALSE" is equivalent to "NOT x".  These can be worth
+                                * checking because, while we preferentially simplify boolean
+                                * comparisons down to "x" and "NOT x", the other form has to
+                                * be dealt with anyway in the context of index conditions.
+                                *
+                                * We could likewise check whether the predicate is boolean
+                                * equality to a constant; but there are no known use-cases
+                                * for that at the moment, assuming that the predicate has
+                                * been through constant-folding.
+                                *----------
+                                */
+                               if (op->opno == BooleanEqualOperator)
+                               {
+                                       Node       *rightop;
+
+                                       Assert(list_length(op->args) == 2);
+                                       rightop = lsecond(op->args);
+                                       /* We might never see null Consts here, but better check */
+                                       if (rightop && IsA(rightop, Const) &&
+                                               !((Const *) rightop)->constisnull)
+                                       {
+                                               Node       *leftop = linitial(op->args);
+
+                                               if (DatumGetBool(((Const *) rightop)->constvalue))
+                                               {
+                                                       /* X = true implies X */
+                                                       if (equal(predicate, leftop))
+                                                               return true;
+                                               }
+                                               else
+                                               {
+                                                       /* X = false implies NOT X */
+                                                       if (is_notclause(predicate) &&
+                                                               equal(get_notclausearg(predicate), leftop))
+                                                               return true;
+                                               }
+                                       }
+                               }
                        }
-                       else
+                       break;
+               default:
+                       break;
+       }
+
+       /* ... and some predicate-type-specific ones */
+       switch (nodeTag(predicate))
+       {
+               case T_NullTest:
                        {
-                               /* X = false implies NOT X */
-                               if (is_notclause(predicate) &&
-                                       equal(get_notclausearg(predicate), leftop))
-                                       return true;
+                               NullTest   *predntest = (NullTest *) predicate;
+
+                               switch (predntest->nulltesttype)
+                               {
+                                       case IS_NOT_NULL:
+
+                                               /*
+                                                * If the predicate is of the form "foo IS NOT NULL",
+                                                * and we are considering strong implication, we can
+                                                * conclude that the predicate is implied if the
+                                                * clause is strict for "foo", i.e., it must yield
+                                                * false or NULL when "foo" is NULL.  In that case
+                                                * truth of the clause ensures that "foo" isn't NULL.
+                                                * (Again, this is a safe conclusion because "foo"
+                                                * must be immutable.)  This doesn't work for weak
+                                                * implication, though.  Also, "row IS NOT NULL" does
+                                                * not act in the simple way we have in mind.
+                                                */
+                                               if (!weak &&
+                                                       !predntest->argisrow &&
+                                                       clause_is_strict_for(clause,
+                                                                                                (Node *) predntest->arg,
+                                                                                                true))
+                                                       return true;
+                                               break;
+                                       case IS_NULL:
+                                               break;
+                               }
                        }
-               }
+                       break;
+               default:
+                       break;
        }
 
        /*
-        * We could likewise check whether the predicate is boolean equality to a
-        * constant; but there are no known use-cases for that at the moment,
-        * assuming that the predicate has been through constant-folding.
+        * Finally, if both clauses are binary operator expressions, we may be
+        * able to prove something using the system's knowledge about operators;
+        * those proof rules are encapsulated in operator_predicate_proof().
         */
-
-       /* Next try the IS NOT NULL case */
-       if (!weak &&
-               predicate && IsA(predicate, NullTest))
-       {
-               NullTest   *ntest = (NullTest *) predicate;
-
-               /* row IS NOT NULL does not act in the simple way we have in mind */
-               if (ntest->nulltesttype == IS_NOT_NULL &&
-                       !ntest->argisrow)
-               {
-                       /* strictness of clause for foo implies foo IS NOT NULL */
-                       if (clause_is_strict_for(clause, (Node *) ntest->arg, true))
-                               return true;
-               }
-               return false;                   /* we can't succeed below... */
-       }
-
-       /* Else try operator-related knowledge */
        return operator_predicate_proof(predicate, clause, false, weak);
 }
 
-/*----------
+/*
  * predicate_refuted_by_simple_clause
  *       Does the predicate refutation test for a "simple clause" predicate
  *       and a "simple clause" restriction.
  *
  * We return true if able to prove the refutation, false if not.
  *
- * Unlike the implication case, checking for equal() clauses isn't helpful.
- * But relation_excluded_by_constraints() checks for self-contradictions in a
- * list of clauses, so that we may get here with predicate and clause being
- * actually pointer-equal, and that is worth eliminating quickly.
- *
- * When the predicate is of the form "foo IS NULL", we can conclude that
- * the predicate is refuted if the clause is strict for "foo" (see notes for
- * implication case), or is "foo IS NOT NULL".  That works for either strong
- * or weak refutation.
- *
- * A clause "foo IS NULL" refutes a predicate "foo IS NOT NULL" in all cases.
- * If we are considering weak refutation, it also refutes a predicate that
- * is strict for "foo", since then the predicate must yield false or NULL
- * (and since "foo" appears in the predicate, it's known immutable).
- *
- * (The main motivation for covering these IS [NOT] NULL cases is to support
- * using IS NULL/IS NOT NULL as partition-defining constraints.)
- *
- * Finally, if both clauses are binary operator expressions, we may be able
- * to prove something using the system's knowledge about operators; those
- * proof rules are encapsulated in operator_predicate_proof().
- *----------
+ * The main motivation for covering IS [NOT] NULL cases is to support using
+ * IS NULL/IS NOT NULL as partition-defining constraints.
  */
 static bool
 predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
@@ -1226,61 +1228,152 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
        /* Allow interrupting long proof attempts */
        CHECK_FOR_INTERRUPTS();
 
-       /* A simple clause can't refute itself */
-       /* Worth checking because of relation_excluded_by_constraints() */
+       /*
+        * A simple clause can't refute itself, so unlike the implication case,
+        * checking for equal() clauses isn't helpful.
+        *
+        * But relation_excluded_by_constraints() checks for self-contradictions
+        * in a list of clauses, so that we may get here with predicate and clause
+        * being actually pointer-equal, and that is worth eliminating quickly.
+        */
        if ((Node *) predicate == clause)
                return false;
 
-       /* Try the predicate-IS-NULL case */
-       if (predicate && IsA(predicate, NullTest) &&
-               ((NullTest *) predicate)->nulltesttype == IS_NULL)
+       /* Next we have some clause-type-specific strategies */
+       switch (nodeTag(clause))
        {
-               Expr       *isnullarg = ((NullTest *) predicate)->arg;
+               case T_NullTest:
+                       {
+                               NullTest   *clausentest = (NullTest *) clause;
 
-               /* row IS NULL does not act in the simple way we have in mind */
-               if (((NullTest *) predicate)->argisrow)
-                       return false;
+                               /* row IS NULL does not act in the simple way we have in mind */
+                               if (clausentest->argisrow)
+                                       return false;
 
-               /* strictness of clause for foo refutes foo IS NULL */
-               if (clause_is_strict_for(clause, (Node *) isnullarg, true))
-                       return true;
-
-               /* foo IS NOT NULL refutes foo IS NULL */
-               if (clause && IsA(clause, NullTest) &&
-                       ((NullTest *) clause)->nulltesttype == IS_NOT_NULL &&
-                       !((NullTest *) clause)->argisrow &&
-                       equal(((NullTest *) clause)->arg, isnullarg))
-                       return true;
+                               switch (clausentest->nulltesttype)
+                               {
+                                       case IS_NULL:
+                                               {
+                                                       switch (nodeTag(predicate))
+                                                       {
+                                                               case T_NullTest:
+                                                                       {
+                                                                               NullTest   *predntest = (NullTest *) predicate;
+
+                                                                               /*
+                                                                                * row IS NULL does not act in the
+                                                                                * simple way we have in mind
+                                                                                */
+                                                                               if (predntest->argisrow)
+                                                                                       return false;
+
+                                                                               /*
+                                                                                * foo IS NULL refutes foo IS NOT
+                                                                                * NULL, at least in the non-row case,
+                                                                                * for both strong and weak refutation
+                                                                                */
+                                                                               if (predntest->nulltesttype == IS_NOT_NULL &&
+                                                                                       equal(predntest->arg, clausentest->arg))
+                                                                                       return true;
+                                                                       }
+                                                                       break;
+                                                               default:
+                                                                       break;
+                                                       }
 
-               return false;                   /* we can't succeed below... */
+                                                       /*
+                                                        * foo IS NULL weakly refutes any predicate that
+                                                        * is strict for foo, since then the predicate
+                                                        * must yield false or NULL (and since foo appears
+                                                        * in the predicate, it's known immutable).
+                                                        */
+                                                       if (weak &&
+                                                               clause_is_strict_for((Node *) predicate,
+                                                                                                        (Node *) clausentest->arg,
+                                                                                                        true))
+                                                               return true;
+
+                                                       return false;   /* we can't succeed below... */
+                                               }
+                                               break;
+                                       case IS_NOT_NULL:
+                                               break;
+                               }
+                       }
+                       break;
+               default:
+                       break;
        }
 
-       /* Try the clause-IS-NULL case */
-       if (clause && IsA(clause, NullTest) &&
-               ((NullTest *) clause)->nulltesttype == IS_NULL)
+       /* ... and some predicate-type-specific ones */
+       switch (nodeTag(predicate))
        {
-               Expr       *isnullarg = ((NullTest *) clause)->arg;
+               case T_NullTest:
+                       {
+                               NullTest   *predntest = (NullTest *) predicate;
 
-               /* row IS NULL does not act in the simple way we have in mind */
-               if (((NullTest *) clause)->argisrow)
-                       return false;
+                               /* row IS NULL does not act in the simple way we have in mind */
+                               if (predntest->argisrow)
+                                       return false;
 
-               /* foo IS NULL refutes foo IS NOT NULL */
-               if (predicate && IsA(predicate, NullTest) &&
-                       ((NullTest *) predicate)->nulltesttype == IS_NOT_NULL &&
-                       !((NullTest *) predicate)->argisrow &&
-                       equal(((NullTest *) predicate)->arg, isnullarg))
-                       return true;
+                               switch (predntest->nulltesttype)
+                               {
+                                       case IS_NULL:
+                                               {
+                                                       switch (nodeTag(clause))
+                                                       {
+                                                               case T_NullTest:
+                                                                       {
+                                                                               NullTest   *clausentest = (NullTest *) clause;
+
+                                                                               /*
+                                                                                * row IS NULL does not act in the
+                                                                                * simple way we have in mind
+                                                                                */
+                                                                               if (clausentest->argisrow)
+                                                                                       return false;
+
+                                                                               /*
+                                                                                * foo IS NOT NULL refutes foo IS NULL
+                                                                                * for both strong and weak refutation
+                                                                                */
+                                                                               if (clausentest->nulltesttype == IS_NOT_NULL &&
+                                                                                       equal(clausentest->arg, predntest->arg))
+                                                                                       return true;
+                                                                       }
+                                                                       break;
+                                                               default:
+                                                                       break;
+                                                       }
 
-               /* foo IS NULL weakly refutes any predicate that is strict for foo */
-               if (weak &&
-                       clause_is_strict_for((Node *) predicate, (Node *) isnullarg, true))
-                       return true;
+                                                       /*
+                                                        * When the predicate is of the form "foo IS
+                                                        * NULL", we can conclude that the predicate is
+                                                        * refuted if the clause is strict for "foo" (see
+                                                        * notes for implication case).  That works for
+                                                        * either strong or weak refutation.
+                                                        */
+                                                       if (clause_is_strict_for(clause,
+                                                                                                        (Node *) predntest->arg,
+                                                                                                        true))
+                                                               return true;
+                                               }
+                                               break;
+                                       case IS_NOT_NULL:
+                                               break;
+                               }
 
-               return false;                   /* we can't succeed below... */
+                               return false;   /* we can't succeed below... */
+                       }
+                       break;
+               default:
+                       break;
        }
 
-       /* Else try operator-related knowledge */
+       /*
+        * Finally, if both clauses are binary operator expressions, we may be
+        * able to prove something using the system's knowledge about operators.
+        */
        return operator_predicate_proof(predicate, clause, true, weak);
 }
 
index 9e6a6471ccfe7b2479d8f5636a227be31194aecc..eaf006c64906bbb365fba034424240807be2add9 100644 (file)
@@ -118,6 +118,22 @@ test_predtest(PG_FUNCTION_ARGS)
                        w_r_holds = false;
        }
 
+       /*
+        * Strong refutation implies weak refutation, so we should never observe
+        * s_r_holds = true with w_r_holds = false.
+        *
+        * We can't make a comparable assertion for implication since moving from
+        * strong to weak implication expands the allowed values of "A" from true
+        * to either true or NULL.
+        *
+        * If this fails it constitutes a bug not with the proofs but with either
+        * this test module or a more core part of expression evaluation since we
+        * are validating the logical correctness of the observed result rather
+        * than the proof.
+        */
+       if (s_r_holds && !w_r_holds)
+               elog(WARNING, "s_r_holds was true; w_r_holds must not be false");
+
        /*
         * Now, dig the clause querytrees out of the plan, and see what predtest.c
         * does with them.
@@ -179,6 +195,19 @@ test_predtest(PG_FUNCTION_ARGS)
        if (weak_refuted_by && !w_r_holds)
                elog(WARNING, "weak_refuted_by result is incorrect");
 
+       /*
+        * As with our earlier check of the logical consistency of whether strong
+        * and weak refutation hold, we ought never prove strong refutation
+        * without also proving weak refutation.
+        *
+        * Also as earlier we cannot make the same guarantee about implication
+        * proofs.
+        *
+        * A warning here suggests a bug in the proof code.
+        */
+       if (strong_refuted_by && !weak_refuted_by)
+               elog(WARNING, "strong_refuted_by was proven; weak_refuted_by should also be proven");
+
        /*
         * Clean up and return a record of the results.
         */