diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-18 20:00:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-18 20:00:37 -0600 |
commit | 8ccb1ee50e16b2e19c1c12605c7c2163dc5af7cc (patch) | |
tree | fd93f7afa9bd49e81340903ee51278068c146536 /src/options | |
parent | 6f95e3c711d39b531eb0a8ac0e098c89a5737ce2 (diff) |
Ho instantiation (#1204)
* Higher-order instantiation.
* Add missing files.
* Document inst match generators, make collectHoVarApplyTerms iterative.
* More documentation.
* More documentation.
* More documentation.
* More documentation
* Refactoring, documentation.
* More documentation.
* Fix comment, reference issue.
* More documentation. Fix ho trigger for the changes from master.
* Minor
* More documentation.
* More documentation.
* More
* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.
* More
* Minor improvements to comments.
* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.
* Improve documentation for ho_trigger.
* Update ho trigger to not access now private member of TermDb.
* Address comments.
* Address
* Clang format
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/quantifiers_modes.h | 58 |
1 files changed, 52 insertions, 6 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a19555987..6274269ce 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -87,19 +87,65 @@ enum QcfMode { QCF_PARTIAL, }; -enum UserPatMode { - /** use but do not trust */ +/** User pattern mode. +* +* These modes determine how user provided patterns (triggers) are +* used during E-matching. The modes vary on when instantiation based on +* user-provided triggers is combined with instantiation based on +* automatically selected triggers. +*/ +enum UserPatMode +{ + /** First instantiate based on user-provided triggers. If no instantiations + * are produced, use automatically selected triggers. + */ USER_PAT_MODE_USE, - /** default, if patterns are supplied for a quantifier, use only those */ + /** Default, if triggers are supplied for a quantifier, use only those. */ USER_PAT_MODE_TRUST, - /** resort to user patterns only when necessary */ + /** Resort to user triggers only when no instantiations are + * produced by automatically selected triggers + */ USER_PAT_MODE_RESORT, - /** ignore user patterns */ + /** Ignore user patterns. */ USER_PAT_MODE_IGNORE, - /** interleave use/resort for user patterns */ + /** Interleave use/resort modes for quantified formulas with user patterns. */ USER_PAT_MODE_INTERLEAVE, }; +/** Trigger selection mode. +* +* These modes are used for determining which terms to select +* as triggers for quantified formulas, when necessary, during E-matching. +* In the following, note the following terminology. A trigger is a set of terms, +* where a single trigger is a singleton set and a multi-trigger is a set of more +* than one term. +* +* TRIGGER_SEL_MIN selects single triggers of minimal term size. +* TRIGGER_SEL_MAX selects single triggers of maximal term size. +* +* For example, consider the quantified formula : +* forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y ) +* +* TRIGGER_SEL_MIN will select g( x, y ) and Q( f( x ), y ). +* TRIGGER_SEL_MAX will select P( f( g( x ) ) ) and Q( f( x ), y ). +* +* The remaining three trigger selections make a difference for multi-triggers +* only. For quantified formulas that require multi-triggers, we build a set of +* partial triggers that don't contain all variables, call this set S. Then, +* multi-triggers are built by taking a random subset of S that collectively +* contains all variables. +* +* Consider the quantified formula : +* forall xyz. P( h( x ), y ) V Q( y, z ) +* +* For TRIGGER_SEL_ALL and TRIGGER_SEL_MIN_SINGLE_ALL, +* S = { h( x ), P( h( x ), y ), Q( y, z ) }. +* For TRIGGER_SEL_MIN_SINGLE_MAX, +* S = { P( h( x ), y ), Q( y, z ) }. +* +* Furthermore, TRIGGER_SEL_MIN_SINGLE_ALL and TRIGGER_SEL_MIN_SINGLE_MAX, when +* selecting single triggers, only select terms of minimal size. +*/ enum TriggerSelMode { /** only consider minimal terms for triggers */ TRIGGER_SEL_MIN, |