aboutsummaryrefslogtreecommitdiff
path: root/src/backend/optimizer/util/predtest.c
Commit message (Collapse)AuthorAge
* Rename nodes/relation.h to nodes/pathnodes.h.Tom Lane2019-01-29
| | | | | | | | | | | | | The old name of this file was never a very good indication of what it was for. Now that there's also access/relation.h, we have a potential confusion hazard as well, so let's rename it to something more apropos. Per discussion, "pathnodes.h" is reasonable, since a good fraction of the file is Path node definitions. While at it, tweak a couple of other headers that were gratuitously importing relation.h into modules that don't need it. Discussion: https://postgr.es/m/7719.1548688728@sss.pgh.pa.us
* Refactor planner's header files.Tom Lane2019-01-29
| | | | | | | | | | | | | | | | | | | | | | | | Create a new header optimizer/optimizer.h, which exposes just the planner functions that can be used "at arm's length", without need to access Paths or the other planner-internal data structures defined in nodes/relation.h. This is intended to provide the whole planner API seen by most of the rest of the system; although FDWs still need to use additional stuff, and more thought is also needed about just what selfuncs.c should rely on. The main point of doing this now is to limit the amount of new #include baggage that will be needed by "planner support functions", which I expect to introduce later, and which will be in relevant datatype modules rather than anywhere near the planner. This commit just moves relevant declarations into optimizer.h from other header files (a couple of which go away because everything got moved), and adjusts #include lists to match. There's further cleanup that could be done if we want to decide that some stuff being exposed by optimizer.h doesn't belong in the planner at all, but I'll leave that for another day. Discussion: https://postgr.es/m/11460.1548706639@sss.pgh.pa.us
* Make some small planner API cleanups.Tom Lane2019-01-29
| | | | | | | | | | | | | | | | | | | | | | Move a few very simple node-creation and node-type-testing functions from the planner's clauses.c to nodes/makefuncs and nodes/nodeFuncs. There's nothing planner-specific about them, as evidenced by the number of other places that were using them. While at it, rename and_clause() etc to is_andclause() etc, to clarify that they are node-type-testing functions not node-creation functions. And use "static inline" implementations for the shortest ones. Also, modify flatten_join_alias_vars() and some subsidiary functions to take a Query not a PlannerInfo to define the join structure that Vars should be translated according to. They were only using the "parse" field of the PlannerInfo anyway, so this just requires removing one level of indirection. The advantage is that now parse_agg.c can use flatten_join_alias_vars() without the horrid kluge of creating an incomplete PlannerInfo, which will allow that file to be decoupled from relation.h in a subsequent patch. Discussion: https://postgr.es/m/11460.1548706639@sss.pgh.pa.us
* Update copyright for 2019Bruce Momjian2019-01-02
| | | | Backpatch-through: certain files through 9.4
* Improve predtest.c's handling of cases with NULL-constant inputs.Tom Lane2018-03-21
| | | | | | | | | | | | | | | | | | | | Currently, if operator_predicate_proof() is given an operator clause like "something op NULL", it just throws up its hands and reports it can't prove anything. But we can often do better than that, if the operator is strict, because then we know that the clause returns NULL overall. Depending on whether we're trying to prove or refute something, and whether we need weak or strong semantics for NULL, this may be enough to prove the implication, especially when we rely on the standard rule that "false implies anything". In particular, this lets us do something useful with questions like "does X IN (1,3,5,NULL) imply X <= 5?" The null entry in the IN list can effectively be ignored for this purpose, but the proof rules were not previously smart enough to deduce that. This patch is by me, but it owes something to previous work by Amit Langote to try to solve problems of the form mentioned. Thanks also to Emre Hasegeli and Ashutosh Bapat for review. Discussion: https://postgr.es/m/3bad48fc-f257-c445-feeb-8a2b2fb622ba@lab.ntt.co.jp
* Improve predtest.c's internal docs, and enhance its functionality a bit.Tom Lane2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Commit b08df9cab left things rather poorly documented as far as the exact semantics of "clause_is_check" mode went. Also, that mode did not really work correctly for predicate_refuted_by; although given the lack of specification as to what it should do, as well as the lack of any actual use-case, that's perhaps not surprising. Rename "clause_is_check" to "weak" proof mode, and provide specifications for what it should do. I defined weak refutation as meaning "truth of A implies non-truth of B", which makes it possible to use the mode in the part of relation_excluded_by_constraints that checks for mutually contradictory WHERE clauses. Fix up several places that did things wrong for that definition. (As far as I can see, these errors would only lead to failure-to-prove, not incorrect claims of proof, making them not serious bugs even aside from the fact that v10 contains no use of this mode. So there seems no need for back-patching.) In addition, teach predicate_refuted_by_recurse that it can use predicate_implied_by_recurse after all when processing a strong NOT-clause, so long as it asks for the correct proof strength. This is an optimization that could have been included in commit b08df9cab, but wasn't. Also, simplify and generalize the logic that checks for whether nullness of the argument of IS [NOT] NULL would force overall nullness of the predicate or clause. (This results in a change in the partition_prune test's output, as it is now able to prune an all-nulls partition that it did not recognize before.) In passing, in PartConstraintImpliedByRelConstraint, remove bogus conversion of the constraint list to explicit-AND form and then right back again; that accomplished nothing except forcing a useless extra level of recursion inside predicate_implied_by. Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us
* Update copyright for 2018Bruce Momjian2018-01-02
| | | | Backpatch-through: certain files through 9.3
* Change TRUE/FALSE to true/falsePeter Eisentraut2017-11-08
| | | | | | | | | | | | | | The lower case spellings are C and C++ standard and are used in most parts of the PostgreSQL sources. The upper case spellings are only used in some files/modules. So standardize on the standard spellings. The APIs for ICU, Perl, and Windows define their own TRUE and FALSE, so those are left as is when using those APIs. In code comments, we use the lower-case spelling for the C concepts and keep the upper-case spelling for the SQL concepts. Reviewed-by: Michael Paquier <michael.paquier@gmail.com>
* Phase 2 of pgindent updates.Tom Lane2017-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Change pg_bsd_indent to follow upstream rules for placement of comments to the right of code, and remove pgindent hack that caused comments following #endif to not obey the general rule. Commit e3860ffa4dd0dad0dd9eea4be9cc1412373a8c89 wasn't actually using the published version of pg_bsd_indent, but a hacked-up version that tried to minimize the amount of movement of comments to the right of code. The situation of interest is where such a comment has to be moved to the right of its default placement at column 33 because there's code there. BSD indent has always moved right in units of tab stops in such cases --- but in the previous incarnation, indent was working in 8-space tab stops, while now it knows we use 4-space tabs. So the net result is that in about half the cases, such comments are placed one tab stop left of before. This is better all around: it leaves more room on the line for comment text, and it means that in such cases the comment uniformly starts at the next 4-space tab stop after the code, rather than sometimes one and sometimes two tabs after. Also, ensure that comments following #endif are indented the same as comments following other preprocessor commands such as #else. That inconsistency turns out to have been self-inflicted damage from a poorly-thought-through post-indent "fixup" in pgindent. This patch is much less interesting than the first round of indent changes, but also bulkier, so I thought it best to separate the effects. Discussion: https://postgr.es/m/E1dAmxK-0006EE-1r@gemulon.postgresql.org Discussion: https://postgr.es/m/30527.1495162840@sss.pgh.pa.us
* Initial pgindent run with pg_bsd_indent version 2.0.Tom Lane2017-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new indent version includes numerous fixes thanks to Piotr Stefaniak. The main changes visible in this commit are: * Nicer formatting of function-pointer declarations. * No longer unexpectedly removes spaces in expressions using casts, sizeof, or offsetof. * No longer wants to add a space in "struct structname *varname", as well as some similar cases for const- or volatile-qualified pointers. * Declarations using PG_USED_FOR_ASSERTS_ONLY are formatted more nicely. * Fixes bug where comments following declarations were sometimes placed with no space separating them from the code. * Fixes some odd decisions for comments following case labels. * Fixes some cases where comments following code were indented to less than the expected column 33. On the less good side, it now tends to put more whitespace around typedef names that are not listed in typedefs.list. This might encourage us to put more effort into typedef name collection; it's not really a bug in indent itself. There are more changes coming after this round, having to do with comment indentation and alignment of lines appearing within parentheses. I wanted to limit the size of the diffs to something that could be reviewed without one's eyes completely glazing over, so it seemed better to split up the changes as much as practical. Discussion: https://postgr.es/m/E1dAmxK-0006EE-1r@gemulon.postgresql.org Discussion: https://postgr.es/m/30527.1495162840@sss.pgh.pa.us
* Teach predtest.c about CHECK clauses to fix partitioning bugs.Robert Haas2017-06-14
| | | | | | | | | | | | | | | | | | In a CHECK clause, a null result means true, whereas in a WHERE clause it means false. predtest.c provided different functions depending on which set of semantics applied to the predicate being proved, but had no option to control what a null meant in the clauses provided as axioms. Add one. Use that in the partitioning code when figuring out whether the validation scan on a new partition can be skipped. Rip out the old logic that attempted (not very successfully) to compensate for the absence of the necessary support in predtest.c. Ashutosh Bapat and Robert Haas, reviewed by Amit Langote and incorporating feedback from Tom Lane. Discussion: http://postgr.es/m/CAFjFpReT_kq_uwU_B8aWDxR7jNGE=P0iELycdq5oupi=xSQTOw@mail.gmail.com
* Remove obsoleted code relating to targetlist SRF evaluation.Andres Freund2017-01-19
| | | | | | | | | | | | | Since 69f4b9c plain expression evaluation (and thus normal projection) can't return sets of tuples anymore. Thus remove code dealing with that possibility. This will require adjustments in external code using ExecEvalExpr()/ExecProject() - that should neither be hard nor very common. Author: Andres Freund and Tom Lane Discussion: https://postgr.es/m/20160822214023.aaxz5l4igypowyri@alap3.anarazel.de
* Update copyright via script for 2017Bruce Momjian2017-01-03
|
* Refactor to reduce code duplication for function property checking.Tom Lane2016-06-10
| | | | | | | | | | | | | | | | | | | | | | | As noted by Andres Freund, we'd accumulated quite a few similar functions in clauses.c that examine all functions in an expression tree to see if they satisfy some boolean test. Reduce the duplication by inventing a function check_functions_in_node() that applies a simple callback function to each SQL function OID appearing in a given expression node. This also fixes some arguable oversights; for example, contain_mutable_functions() did not check aggregate or window functions for mutability. I doubt that that represents a live bug at the moment, because we don't really consider mutability for aggregates; but it might someday be one. I chose to put check_functions_in_node() in nodeFuncs.c because it seemed like other modules might wish to use it in future. That in turn forced moving set_opfuncid() et al into nodeFuncs.c, as the alternative was for nodeFuncs.c to depend on optimizer/setrefs.c which didn't seem very clean. In passing, teach contain_leaked_vars_walker() about a few more expression node types it can safely look through, and improve the rather messy and undercommented code in has_parallel_hazard_walker(). Discussion: <20160527185853.ziol2os2zskahl7v@alap3.anarazel.de>
* Update copyright for 2016Bruce Momjian2016-01-02
| | | | Backpatch certain files through 9.1
* Teach predtest.c that "foo" implies "foo IS NOT NULL".Tom Lane2015-08-01
| | | | | | | | | | | Per complaint from Peter Holzer. It's useful to cover this special case, since for a boolean variable "foo", earlier parts of the planner will have reduced variants like "foo = true" to just "foo", and thus we may fail to recognize the applicability of a partial index with predicate "foo IS NOT NULL". Back-patch to 9.5, but not further; given the lack of previous complaints this doesn't seem like behavior to change in stable branches.
* Move strategy numbers to include/access/stratnum.hAlvaro Herrera2015-05-15
| | | | | | | | | | | | | | | | | | | | For upcoming BRIN opclasses, it's convenient to have strategy numbers defined in a single place. Since there's nothing appropriate, create it. The StrategyNumber typedef now lives there, as well as existing strategy numbers for B-trees (from skey.h) and R-tree-and-friends (from gist.h). skey.h is forced to include stratnum.h because of the StrategyNumber typedef, but gist.h is not; extensions that currently rely on gist.h for rtree strategy numbers might need to add a new A few .c files can stop including skey.h and/or gist.h, which is a nice side benefit. Per discussion: https://www.postgresql.org/message-id/20150514232132.GZ2523@alvh.no-ip.org Authored by Emre Hasegeli and Álvaro. (It's not clear to me why bootscanner.l has any #include lines at all.)
* Update copyright for 2015Bruce Momjian2015-01-06
| | | | Backpatch certain files through 9.0
* Improve hash_create's API for selecting simple-binary-key hash functions.Tom Lane2014-12-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, if you wanted anything besides C-string hash keys, you had to specify a custom hashing function to hash_create(). Nearly all such callers were specifying tag_hash or oid_hash; which is tedious, and rather error-prone, since a caller could easily miss the opportunity to optimize by using hash_uint32 when appropriate. Replace this with a design whereby callers using simple binary-data keys just specify HASH_BLOBS and don't need to mess with specific support functions. hash_create() itself will take care of optimizing when the key size is four bytes. This nets out saving a few hundred bytes of code space, and offers a measurable performance improvement in tidbitmap.c (which was not exploiting the opportunity to use hash_uint32 for its 4-byte keys). There might be some wins elsewhere too, I didn't analyze closely. In future we could look into offering a similar optimized hashing function for 8-byte keys. Under this design that could be done in a centralized and machine-independent fashion, whereas getting it right for keys of platform-dependent sizes would've been notationally painful before. For the moment, the old way still works fine, so as not to break source code compatibility for loadable modules. Eventually we might want to remove tag_hash and friends from the exported API altogether, since there's no real need for them to be explicitly referenced from outside dynahash.c. Teodor Sigaev and Tom Lane
* Improve predtest.c's ability to reason about operator expressions.Tom Lane2014-06-13
| | | | | | | | | | | | | | | | | | | | | We have for a long time been able to prove implications and refutations between clauses structured like "expr op const" with the same subexpression and btree-related operators; for example that "x < 4" implies "x <= 5". The implication machinery is needed to detect usability of partial indexes, and the refutation machinery is needed to implement constraint exclusion. This patch extends that machinery to make proofs for operator expressions involving the same two immutable-but-not-necessarily-just-Const input expressions, ie does "expr1 op1 expr2" prove or refute "expr1 op2 expr2" or "expr2 op2 expr1"? An important example is that we can now prove "x = y" given "y = x", which formerly the code could not deduce unless x or y was a constant. We can make use of the system's knowledge of operator commutator and negator pairs, and can also make use of btree opclass relationships, for example "x < y" implies "x <= y" and refutes "x > y" (notice that neither of these could be proven just from commutator or negator links). Inspired by a gripe from Brian Dunavant. This seems more like a new feature than a bug fix, though, so no back-patch.
* pgindent run for 9.4Bruce Momjian2014-05-06
| | | | | This includes removing tabs after periods in C comments, which was applied to back branches, so this change should not effect backpatching.
* Update copyright for 2014Bruce Momjian2014-01-07
| | | | | Update all files in head, and files COPYRIGHT and legal.sgml in all back branches.
* Update copyrights for 2013Bruce Momjian2013-01-01
| | | | | Fully update git head, and update back branches in ./COPYRIGHT and legal.sgml files.
* Run pgindent on 9.2 source tree in preparation for first 9.3Bruce Momjian2012-06-10
| | | | commit-fest.
* Update copyright notices for year 2012.Bruce Momjian2012-01-01
|
* Clean up the #include mess a little.Tom Lane2011-09-04
| | | | | | | | | | | | | | | | | walsender.h should depend on xlog.h, not vice versa. (Actually, the inclusion was circular until a couple hours ago, which was even sillier; but Bruce broke it in the expedient rather than logically correct direction.) Because of that poor decision, plus blind application of pgrminclude, we had a situation where half the system was depending on xlog.h to include such unrelated stuff as array.h and guc.h. Clean up the header inclusion, and manually revert a lot of what pgrminclude had done so things build again. This episode reinforces my feeling that pgrminclude should not be run without adult supervision. Inclusion changes in header files in particular need to be reviewed with great care. More generally, it'd be good if we had a clearer notion of module layering to dictate which headers can sanely include which others ... but that's a big task for another day.
* Remove unnecessary #include references, per pgrminclude script.Bruce Momjian2011-09-01
|
* Revise sinval code to remove no-longer-used tuple TID from inval messages.Tom Lane2011-08-16
| | | | | | | | | | This requires adjusting the API for syscache callback functions: they now get a hash value, not a TID, to identify the target tuple. Most of them weren't paying any attention to that argument anyway, but plancache did require a small amount of fixing. Also, improve performance a trifle by avoiding sending duplicate inval messages when a heap_update isn't changing the catcache lookup columns.
* Remove assumptions that not-equals operators cannot be in any opclass.Tom Lane2011-07-06
| | | | | | | | | | | | | | | get_op_btree_interpretation assumed this in order to save some duplication of code, but it's not true in general anymore because we added <> support to btree_gist. (We still assume it for btree opclasses, though.) Also, essentially the same logic was baked into predtest.c. Get rid of that duplication by generalizing get_op_btree_interpretation so that it can be used by predtest.c. Per bug report from Denis de Bernardy and investigation by Jeff Davis, though I didn't use Jeff's patch exactly as-is. Back-patch to 9.1; we do not support this usage before that.
* Move Trigger and TriggerDesc structs out of rel.h into a new reltrigger.hAlvaro Herrera2011-07-04
| | | | | This lets us stop including rel.h into execnodes.h, which is a widely used header.
* pgindent run before PG 9.1 beta 1.Bruce Momjian2011-04-10
|
* Clean up a few failures to set collation fields in expression nodes.Tom Lane2011-03-26
| | | | | | | | | I'm not sure these have any non-cosmetic implications, but I'm not sure they don't, either. In particular, ensure the CaseTestExpr generated by transformAssignmentIndirection to represent the base target column carries the correct collation, because parse_collate.c won't fix that. Tweak lsyscache.c API so that we can get the appropriate collation without an extra syscache lookup.
* Revise collation derivation method and expression-tree representation.Tom Lane2011-03-19
| | | | | | | | | | | | | | | | | | | All expression nodes now have an explicit output-collation field, unless they are known to only return a noncollatable data type (such as boolean or record). Also, nodes that can invoke collation-aware functions store a separate field that is the collation value to pass to the function. This avoids confusion that arises when a function has collatable inputs and noncollatable output type, or vice versa. Also, replace the parser's on-the-fly collation assignment method with a post-pass over the completed expression tree. This allows us to use a more complex (and hopefully more nearly spec-compliant) assignment rule without paying for it in extra storage in every expression node. Fix assorted bugs in the planner's handling of collations by making collation one of the defining properties of an EquivalenceClass and by converting CollateExprs into discardable RelabelType nodes during expression preprocessing.
* Per-column collation supportPeter Eisentraut2011-02-08
| | | | | | | | This adds collation support for columns and domains, a COLLATE clause to override it per expression, and B-tree index support. Peter Eisentraut reviewed by Pavel Stehule, Itagaki Takahiro, Robert Haas, Noah Misch
* Stamp copyrights for year 2011.Bruce Momjian2011-01-01
|
* Create the system catalog infrastructure needed for KNNGIST.Tom Lane2010-11-24
| | | | | | | | | | | | | | | | This commit adds columns amoppurpose and amopsortfamily to pg_amop, and column amcanorderbyop to pg_am. For the moment all the entries in amcanorderbyop are "false", since the underlying support isn't there yet. Also, extend the CREATE OPERATOR CLASS/ALTER OPERATOR FAMILY commands with [ FOR SEARCH | FOR ORDER BY sort_operator_family ] clauses to allow the new columns of pg_amop to be populated, and create pg_dump support for dumping that information. I also added some documentation, although it's perhaps a bit premature given that the feature doesn't do anything useful yet. Teodor Sigaev, Robert Haas, Tom Lane
* Remove cvs keywords from all files.Magnus Hagander2010-09-20
|
* pgindent run for 9.0Bruce Momjian2010-02-26
|
* Allow predicate_refuted_by() to deduce that NOT A refutes A.Tom Lane2010-02-25
| | | | | | | | | | | | | | | | | | | | | We had originally made the stronger assumption that NOT A refutes any B if B implies A, but this fails in three-valued logic, because we need to prove B is false not just that it's not true. However the logic does go through if B is equal to A. Recognizing this limited case is enough to handle examples that arise when we have simplified "bool_var = true" or "bool_var = false" to just "bool_var" or "NOT bool_var". If we had not done that simplification then the btree-operator proof logic would have been able to prove that the expressions were contradictory, but only for identical expressions being compared to the constants; so handling identical A and B covers all the same cases. The motivation for doing this is to avoid unexpected asymmetrical behavior when a partitioned table uses a boolean partitioning column, as in today's gripe from Dominik Sander. Back-patch to 8.2, which is as far back as predicate_refuted_by attempts to do anything at all with NOTs.
* Wrap calls to SearchSysCache and related functions using macros.Robert Haas2010-02-14
| | | | | | | | | | | | The purpose of this change is to eliminate the need for every caller of SearchSysCache, SearchSysCacheCopy, SearchSysCacheExists, GetSysCacheOid, and SearchSysCacheList to know the maximum number of allowable keys for a syscache entry (currently 4). This will make it far easier to increase the maximum number of keys in a future release should we choose to do so, and it makes the code shorter, too. Design and review by Tom Lane.
* Update copyright for the year 2010.Bruce Momjian2010-01-02
|
* Add an "argisrow" field to NullTest nodes, following a plan made way back inTom Lane2010-01-01
| | | | | | 8.2beta but never carried out. This avoids repetitive tests of whether the argument is of scalar or composite type. Also, be a bit more paranoid about composite arguments in some places where we previously weren't checking.
* Remove a couple of unnecessary calls of CreateCacheMemoryContext. TheseTom Lane2009-12-27
| | | | | | | probably got there via blind copy-and-paste from one of the legitimate callers, so rearrange and comment that code a bit to make it clearer that this isn't a necessary prerequisite to hash_create. Per observation from Robert Haas.
* 8.4 pgindent run, with new combined Linux/FreeBSD/MinGW typedef listBruce Momjian2009-06-11
| | | | provided by Andrew.
* Partially revert my patch of 2008-11-12 that installed a limit on the numberTom Lane2009-05-11
| | | | | | | | | | | of AND/OR clause branches that predtest.c would attempt to deal with. As noted in bug #4721, that change disabled proof attempts for sizes of problems that people are actually expecting it to work for. The original complaint it was trying to solve was O(N^2) behavior for long IN-lists, so let's try applying the limit to just ScalarArrayOpExprs rather than everything. Another case of "foolish consistency" I fear. Back-patch to 8.2, same as the previous patch was.
* Make a marginal performance improvement in predicate_implied_by andTom Lane2009-05-10
| | | | | | | | | | | | | predicate_refuted_by: if either top-level input is a single-element list, reduce it to its lone member before proceeding. This avoids a useless level of AND-recursion within the recursive proof routines. It's worth doing because, for example, if the clause is a 100-element list and the predicate is a 1-element list then we'd otherwise strip the predicate's list structure 100 times as we iterate through the clause. It's only needed at top level because there won't be any trivial ANDs below that --- this situation is an artifact of the decision to represent even single-item conditions as Lists in the "implicit AND" format, and that format is only used at the top level of any predicate or restriction condition.
* Arrange for function default arguments to be processed properly in expressionsTom Lane2009-01-09
| | | | | | | that are set up for execution with ExecPrepareExpr rather than going through the full planner process. By introducing an explicit notion of "expression planning", this patch also lays a bit of groundwork for maybe someday allowing sub-selects in standalone expressions.
* Update copyright for 2009.Bruce Momjian2009-01-01
|
* Arrange to cache the results of looking up a btree predicate proof comparisonTom Lane2008-11-13
| | | | | | | | | | | operator. The result depends only on the two input operators and the proof direction (imply or refute), so it's easy to cache. This provides a very large savings in cases such as Sergey Konoplev's long NOT-IN-list example, where predtest spends all its time repeatedly figuring out that the same pair of operators cannot be used to prove anything. (But of course the O(N^2) behavior still catches up with you eventually.) I'm not convinced it buys a whole lot when constraint_exclusion isn't turned on, but it's not a lot of added code so we might as well cache all the time.
* In predtest.c, install a limit on the number of branches we will process inTom Lane2008-11-12
| | | | | | | | | | | | | | | | | AND, OR, or equivalent clauses: if there are too many (more than 100) just exit without proving anything. This ensures that we don't spend O(N^2) time trying (and most likely failing) to prove anything about very long IN lists and similar cases. Also, install a couple of CHECK_FOR_INTERRUPTS calls to ensure that a long proof attempt can be interrupted. Per gripe from Sergey Konoplev. Back-patch the whole patch to 8.2 and just the CHECK_FOR_INTERRUPTS addition to 8.1. (The rest of the patch doesn't apply cleanly, and since 8.1 doesn't show the complained-of behavior anyway, it doesn't seem necessary to work hard on it.)