diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:21 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:36 -0600 |
| commit | eb5debabce433774a0dbfd46745efb8fcf38b8ab (patch) | |
| tree | 265975eab00a2919d53eb32c6bb993ed7490cbd4 /src/theory/quantifiers/options_handlers.h | |
| parent | 4c7f8d38445f067bb85f38cf3ea343cc92e41ef2 (diff) | |
Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
| -rw-r--r-- | src/theory/quantifiers/options_handlers.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 15d52cc96..eb2c05858 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -32,6 +32,10 @@ Modes currently supported by the --inst-when option:\n\ full (default)\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ +full-delay \n\ ++ Run instantiation round at full effort, before theory combination, after\n\ + all other theories have finished.\n\ +\n\ full-last-call\n\ + Alternate running instantiation rounds at full effort and last\n\ call. In other words, interleave instantiation and theory combination.\n\ @@ -147,6 +151,8 @@ inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, return INST_WHEN_PRE_FULL; } else if(optarg == "full") { return INST_WHEN_FULL; + } else if(optarg == "full-delay") { + return INST_WHEN_FULL_DELAY; } else if(optarg == "full-last-call") { return INST_WHEN_FULL_LAST_CALL; } else if(optarg == "last-call") { |