1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
//! Whether a query's `WHERE` proves a partial index's predicate.
//!
//! Invariant: **an index is chosen only when every row the query wants is in
//! it.** A partial index holds the rows its predicate accepted and no others,
//! so reading one for a query whose rows it does not all hold answers the
//! question with rows missing - and the rows missing are exactly the ones the
//! predicate excludes, which is the hardest kind of wrong answer to notice.
//! Every rule here is therefore sound on its own rather than likely, and a
//! rule nobody could write is an index left unchosen.
//!
//! Here rather than in [`super`] because `plan.rs` is at its recorded size and
//! these two functions are one question its caller asks once.
use *;
/// Reports whether a query's `WHERE` implies a partial index's predicate.
///
/// **Two rules, both sound, and nothing that needs a theorem prover.**
///
/// The first is the predicate appearing, unchanged, as a conjunct of the
/// statement's `WHERE`. So an index declared `WHERE b > 5` answers
/// `WHERE b > 5 AND a = 1` and does not answer `WHERE b > 6`, even though the
/// second implies the first. Proving the general implication is a theorem
/// prover in the planner, and every case it got wrong would be a query
/// silently missing exactly the rows the predicate excludes.
///
/// The second is `IS NOT NULL`, and it was measured rather than reasoned about
/// (task-1913). This function's comment used to call the verbatim rule
/// "SQLite's rule"; the pinned 3.53.4 answers `SELECT n FROM t WHERE n = 1`
/// with `SEARCH t USING COVERING INDEX t_n (n=?)` over an index declared
/// `WHERE n IS NOT NULL`, and this engine scanned the table. That index is how
/// SQLite spells "unique among the rows that have one", so the shape is
/// common and the whole point of declaring it was to be searched.
///
/// The rule added is the narrowest one that answers it: a comparison is three
/// valued, so `n = 1` is *true* only when `n` is not NULL - and the same holds
/// for `<`, `<=`, `>`, `>=` and `<>`. A conjunct comparing the operand the
/// predicate asks about therefore proves the predicate. `IS` and `IS NOT` are
/// deliberately not comparisons here: `n IS NULL` is true precisely when `n`
/// is NULL, so reading it as proof of the opposite would choose an index that
/// holds none of the rows the query wants.
///
/// `false` when the index's own predicate could not be bound, which is what
/// leaves an index the planner cannot reason about unchosen rather than chosen
/// on a guess.
///
/// @param computed - the index's bound expressions, when it has them
/// @param terms - the statement's `WHERE` conjuncts
pub
/// Reports whether a conjunct is a comparison that one operand has to be
/// non-NULL to satisfy.
///
/// Only [`BoundExpr::Compare`], and only its six comparison operators. A
/// `Compare` holding an arithmetic operator is not a conjunct the binder
/// produces, and the match is written out rather than defaulted so that an
/// operator added later is a compilation error rather than a wrong answer.
///
/// @param term - one conjunct of the statement's `WHERE`
/// @param operand - the expression the index's predicate asks about
pub