diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-14 12:25:07 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-14 12:25:14 +0100 |
| commit | 83c0e6c14955e04b3dca56037508e4ceb6691f10 (patch) | |
| tree | 3e242ad90f0e34d03888e78267a4afe59e8a4ce3 /src/theory/quantifiers/options_handlers.h | |
| parent | f48855b3f7ebff4d6de916d6e433b3949afdbd1b (diff) | |
Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
| -rw-r--r-- | src/theory/quantifiers/options_handlers.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index f01e563df..e00879303 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -88,9 +88,6 @@ default \n\ none \n\ + Disable model-based quantifier instantiation.\n\ \n\ -instgen \n\ -+ Use instantiation algorithm that mimics Inst-Gen calculus. \n\ -\n\ gen-ev \n\ + Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ model finding paper based on generalizing evaluations.\n\ @@ -98,9 +95,6 @@ gen-ev \n\ fmc-interval \n\ + Same as default, but with intervals for models of integer functions.\n\ \n\ -interval \n\ -+ Use algorithm that abstracts domain elements as intervals. \n\ -\n\ abs \n\ + Use abstract MBQI algorithm (uses disjoint sets). \n\ \n\ |