diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:36 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:47 -0500 |
| commit | 576d50ac7c13233a589771401537b587eb36361e (patch) | |
| tree | 3f044ce37d5b3dc0f20db52339b3f1ae8cb59c8d /src/options/quantifiers_options | |
| parent | 0f69a8ba2286bd5d9b807c10ad350705952e93d6 (diff) | |
New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5f23a02e0..8ed4f24c0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -69,8 +69,8 @@ option inferArithTriggerEq --infer-arith-trigger-eq bool :default false option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false record explanations for inferArithTriggerEq -option smartTriggers --smart-triggers bool :default true - enable smart triggers +option strictTriggers --strict-triggers bool :default false + only instantiate quantifiers with user patterns based on triggers option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false @@ -89,7 +89,7 @@ option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true generate additional triggers as needed during search |