`import "github.com/cockroachdb/cockroach/pkg/sql/opt/partialidx"`

❖

```
type Implicator struct {
// contains filtered or unexported fields
}
```

Implicator is used to 1) prove that query filters imply a partial index predicate expression and 2) reduce the original filters into a simplified set of filters that are equivalent to the original when applied on top of a partial index scan. The FiltersImplyPredicate function handles both of these tasks.

I. Proving Implication

Filters "imply" a predicate expression if truthful evaluation of the filters guarantees truthful evaluation of the predicate. As a simple example, the expression "a > 10" implies "a > 0" because all values that satisfy "a > 10" also satisfy "a > 0". Note that implication is not symmetrical; "a > 0" does not imply "a > 10".

We use the same logic as Postgres's predtest library to prove implication. Note that this "proof" is not mathematically formal or rigorous. For the sake of efficiency and reduced complexity this proof is a best-effort attempt and false-negatives are possible.

The logic is as follows, where "=>" means "implies" and an "atom" is any expression that is not a logical conjunction or disjunction.

atom A => atom B iff: B contains A atom A => AND-expr B iff: A => each of B's children atom A => OR-expr B iff: A => any of B's children AND-expr A => atom B iff: any of A's children => B AND-expr A => AND-expr B iff: A => each of B's children AND-expr A => OR-expr B iff: A => any of B's children OR any of A's children => B OR-expr A => atom B iff: each of A's children => B OR-expr A => AND-expr B iff: A => each of B's children OR-expr A => OR-expr B iff: each of A's children => any of B's children

II. Remaining Filters

The remaining filters that are returned upon a proof of implication are identical to the input filters except that unnecessary expressions are removed. When the remaining filters are applied on top of a scan of a partial index with the given predicate, the resulting expression is equivalent to the original expression.

Removing unnecessary filter expressions reduces the complexity of the filters and allows any columns that are referenced only in the filters to be pruned from the query plan.

We can safely remove an expression from the filters if all of the following are true:

1. The expression exactly matches an expression in the predicate. This prevents returning empty remaining filters for the implication below. The original filters must be applied on top of a partial index scan with the a > 0 predicate to filter out rows where a is between 0 and 10. a > 10 => a > 0 2. The expression does not reside within a disjunction in the predicate. This prevents the function from returning empty remaining filters for the implication below. The original filters must be applied on top of a partial index scan with the predicate to filter out rows where a > 0 but b != 'foo'. b = 'foo' => a > 0 OR b = 'foo' 3. The expression does not reside within a disjunction in the filters. This prevents the function from incorrectly reducing the filters for the implication below. The original filters must be applied in this case to filter out rows where a is false and c is true, but b is false. a OR (b AND c) => a OR c

An unfortunate side-effect of these three rules is that they prevent reducing the remaining filters in some cases in which it is theoretically possible to simplify the filters. For example, consider the implication below.

a OR b => b OR a

In this case, the remaining filters could be empty, but they are not, because of the asymmetry of the expressions. Individually a and b are exact matches in both the filters and the predicate, but rule #2 and rule #3 prevent this function from traversing the OR expressions and removing a and b from the remaining filters. It would be difficult to support this case without breaking the other cases prevented by each of the three rules.

A set of opt.Expr keeps track of exact matches encountered while exploring the filters and predicate expressions. If implication is proven, the filters expression is traversed and the expressions in the opt.Expr set are removed. While proving implication this set is not passed to recursive calls when a disjunction is encountered in the predicate (rule #2), and disjunctions in the filters are never traversed when searching for exact matches to remove (rule #3).

❖

func (im *Implicator) FiltersImplyPredicate( filters memo.FiltersExpr, pred memo.FiltersExpr, ) (remainingFilters memo.FiltersExpr, ok bool)

FiltersImplyPredicate attempts to prove that a partial index predicate is implied by the given filters. If implication is proven, the function returns the remaining filters (which when applied on top of a partial index scan, make a plan equivalent to the original) and true. If implication cannot be proven, nil and false are returned. See Implicator for more details on how implication is proven and how the remaining filters are determined.

❖

func (im *Implicator) Init(f *norm.Factory, md *opt.Metadata, evalCtx *tree.EvalContext)

Init initializes an Implicator with the given factory, metadata, and eval context.

Package partialidx imports 6 packages (graph) and is imported by 2 packages. Updated 2020-08-12. Refresh now. Tools for package owners.