diff options
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") { |