diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
| commit | a7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a (patch) | |
| tree | a62e3c29bb702a2e890b234504bbc121c4da2619 /src/theory/quantifiers/options_handlers.h | |
| parent | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (diff) | |
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
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 f27b98a3d..02a1a6cf2 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -40,6 +40,10 @@ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ +full-delay-last-call \n\ ++ Alternate running instantiation rounds at full effort after all other\n\ + theories have finished, and last call. \n\ +\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ @@ -235,6 +239,8 @@ inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, return INST_WHEN_FULL_DELAY; } else if(optarg == "full-last-call") { return INST_WHEN_FULL_LAST_CALL; + } else if(optarg == "full-delay-last-call") { + return INST_WHEN_FULL_DELAY_LAST_CALL; } else if(optarg == "last-call") { return INST_WHEN_LAST_CALL; } else if(optarg == "help") { |