On 2/15/19, Rowan Worth <[email protected]> wrote:
> On Fri, 15 Feb 2019 at 16:13, Wout Mertens <[email protected]> wrote:
>
>> sqlite> create index b on t(b) where b is not null;
>> sqlite> explain query plan select b from t where b is not null;
>> QUERY PLAN
>> `--SCAN TABLE t USING COVERING INDEX b
>> sqlite> explain query plan select b from t where (b is not null)=1;
>> QUERY PLAN
>> `--SCAN TABLE t
>>
>> So basically, match the where of the index as part of an expression.
>>
>> I'm guessing the answer is no, but I thought I'd ask anyway
>>
>
> Hm, interesting. The docs have something to say about this -- from
> https://www.sqlite.org/expridx.html section 1:
>
> The SQLite query planner will consider using an index on an expression when
>> the expression that is indexed appears in the WHERE clause or in the ORDER
>> BY clause of a query, *exactly* as it is written in the CREATE INDEX
>> statement.

This is a slightly different situation, as (contra the Subject line)
the OPs question was about a "partial index", not an "index on an
expression".

A partial index is an index with a WHERE clause, that only indexes
rows of the main table for which the WHERE clause is true.

    CREATE INDEX ...(...) WHERE x;

If the query is of the form:

    SELECT .... WHERE y;

Then the partial index may only be used if y "implies" x, where
"implies" here is the logical operator often represented by an arrow
pointing to the right, and which is equivalent to "NOT y OR x".

When compiling a query, the SQLite query optimizer determines whether
or not it can use a partial index by looking at the two WHERE clauses
x and y and trying to prove that y implies x.  The "theorem prover"
that attempts this is pretty simple-minded.  The key observation is
that a false negative is merely a missed optimization, but a
false-positive is a bug in that it gives an incorrect answer.

In the specific question for this case, the theorem prover attempts to prove:

    ((b is not null)=1) IMPLIES (b is not null)

And it fails to come up with a proof, this preventing the partial
index from being used.  The OP is essentially asking that we make the
theorem prover smarter so that it is able to complete the proof and
answer "yes" above.

To answer the OP: such an enhancement "seems" simple enough, but
changes to the theorem prover are fraught with peril since if an error
results in a false positive, wrong answers can result.  Also, you can
grow a theorem prover without bound, but part of the goal of SQLite is
to remain small and compact.

-- 
D. Richard Hipp
[email protected]
_______________________________________________
sqlite-users mailing list
[email protected]
http://mailinglists.sqlite.org/cgi-bin/mailman/listinfo/sqlite-users

Reply via email to