/ Check-in [b3413197]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:A new implementation for the sqlite3ExprImpliesExpr() theorem prover that does a better job of answering TRUE to "(NOT A) OR B" when B is a NOT NULL expression.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256: b3413197f57711f04102d8cc6ff1e8ddbe0f5f2bcb6e1989cf314fa97f0ff7f1
User & Date: drh 2019-05-11 19:36:03
Context
2019-05-13
11:52
Fix an assert() failure in fts5 that could occur when processing a corrupt database. check-in: f158c048 user: dan tags: trunk
2019-05-11
19:36
A new implementation for the sqlite3ExprImpliesExpr() theorem prover that does a better job of answering TRUE to "(NOT A) OR B" when B is a NOT NULL expression. check-in: b3413197 user: drh tags: trunk
16:14
When considering partial indexes, do not assume that a "CASE x ..." expression implies "x IS NOT NULL". check-in: 1b243032 user: dan tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to src/expr.c.

  4903   4903   */
  4904   4904   int sqlite3ExprCompareSkip(Expr *pA, Expr *pB, int iTab){
  4905   4905     return sqlite3ExprCompare(0,
  4906   4906                sqlite3ExprSkipCollate(pA),
  4907   4907                sqlite3ExprSkipCollate(pB),
  4908   4908                iTab);
  4909   4909   }
         4910  +
         4911  +/*
         4912  +** Return non-zero if Expr p can only be true if pNN is not NULL.
         4913  +*/
         4914  +static int exprImpliesNotNull(
         4915  +  Parse *pParse,      /* Parsing context */
         4916  +  Expr *p,            /* The expression to be checked */
         4917  +  Expr *pNN,          /* The expression that is NOT NULL */
         4918  +  int iTab,           /* Table being evaluated */
         4919  +  int seenNot         /* True if p is an operand of NOT */
         4920  +){
         4921  +  assert( p );
         4922  +  assert( pNN );
         4923  +  if( sqlite3ExprCompare(pParse, p, pNN, iTab)==0 ) return 1;
         4924  +  switch( p->op ){
         4925  +    case TK_IN: {
         4926  +      if( seenNot && ExprHasProperty(p, EP_xIsSelect) ) return 0;
         4927  +      assert( ExprHasProperty(p,EP_xIsSelect)
         4928  +           || (p->x.pList!=0 && p->x.pList->nExpr>0) );
         4929  +      return exprImpliesNotNull(pParse, p->pLeft, pNN, iTab, seenNot);
         4930  +    }
         4931  +    case TK_BETWEEN: {
         4932  +      ExprList *pList = p->x.pList;
         4933  +      assert( pList!=0 );
         4934  +      assert( pList->nExpr==2 );
         4935  +      if( seenNot ) return 0;
         4936  +      if( exprImpliesNotNull(pParse, pList->a[0].pExpr, pNN, iTab, seenNot)
         4937  +       || exprImpliesNotNull(pParse, pList->a[1].pExpr, pNN, iTab, seenNot)
         4938  +      ){
         4939  +        return 1;
         4940  +      }
         4941  +      return exprImpliesNotNull(pParse, p->pLeft, pNN, iTab, seenNot);
         4942  +    }
         4943  +    case TK_EQ:
         4944  +    case TK_NE:
         4945  +    case TK_LT:
         4946  +    case TK_LE:
         4947  +    case TK_GT:
         4948  +    case TK_GE:
         4949  +    case TK_PLUS:
         4950  +    case TK_MINUS:
         4951  +    case TK_STAR:
         4952  +    case TK_REM:
         4953  +    case TK_BITAND:
         4954  +    case TK_BITOR:
         4955  +    case TK_SLASH:
         4956  +    case TK_LSHIFT:
         4957  +    case TK_RSHIFT: 
         4958  +    case TK_CONCAT: {
         4959  +      if( exprImpliesNotNull(pParse, p->pRight, pNN, iTab, seenNot) ) return 1;
         4960  +      /* Fall thru into the next case */
         4961  +    }
         4962  +    case TK_SPAN:
         4963  +    case TK_COLLATE:
         4964  +    case TK_BITNOT:
         4965  +    case TK_UPLUS:
         4966  +    case TK_UMINUS: {
         4967  +      return exprImpliesNotNull(pParse, p->pLeft, pNN, iTab, seenNot);
         4968  +    }
         4969  +    case TK_TRUTH: {
         4970  +      if( seenNot ) return 0;
         4971  +      if( p->op2!=TK_IS ) return 0;
         4972  +      return exprImpliesNotNull(pParse, p->pLeft, pNN, iTab, seenNot);
         4973  +    }
         4974  +    case TK_NOT: {
         4975  +      return exprImpliesNotNull(pParse, p->pLeft, pNN, iTab, 1);
         4976  +    }
         4977  +  }
         4978  +  return 0;
         4979  +}
  4910   4980   
  4911   4981   /*
  4912   4982   ** Return true if we can prove the pE2 will always be true if pE1 is
  4913   4983   ** true.  Return false if we cannot complete the proof or if pE2 might
  4914   4984   ** be false.  Examples:
  4915   4985   **
  4916   4986   **     pE1: x==5       pE2: x==5             Result: true
................................................................................
  4940   5010     if( pE2->op==TK_OR
  4941   5011      && (sqlite3ExprImpliesExpr(pParse, pE1, pE2->pLeft, iTab)
  4942   5012                || sqlite3ExprImpliesExpr(pParse, pE1, pE2->pRight, iTab) )
  4943   5013     ){
  4944   5014       return 1;
  4945   5015     }
  4946   5016     if( pE2->op==TK_NOTNULL
  4947         -   && pE1->op!=TK_ISNULL
  4948         -   && pE1->op!=TK_IS
  4949         -   && pE1->op!=TK_ISNOT
  4950         -   && pE1->op!=TK_OR
  4951         -   && pE1->op!=TK_CASE
         5017  +   && exprImpliesNotNull(pParse, pE1, pE2->pLeft, iTab, 0)
  4952   5018     ){
  4953         -    Expr *pX = sqlite3ExprSkipCollate(pE1->pLeft);
  4954         -    testcase( pX!=pE1->pLeft );
  4955         -    if( sqlite3ExprCompare(pParse, pX, pE2->pLeft, iTab)==0 ) return 1;
         5019  +    return 1;
  4956   5020     }
  4957   5021     return 0;
  4958   5022   }
  4959   5023   
  4960   5024   /*
  4961   5025   ** This is the Expr node callback for sqlite3ExprImpliesNotNullRow().
  4962   5026   ** If the expression node requires that the table at pWalker->iCur