diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
| commit | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (patch) | |
| tree | 6f1306e4476e3f7496d7a4e045e63d942802a392 /src/options | |
| parent | 1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 (diff) | |
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/options_handler.cpp | 2 | ||||
| -rw-r--r-- | src/options/quantifiers_modes.h | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d08f5f533..a2809bd67 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -576,8 +576,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, return theory::quantifiers::QCF_PROP_EQ; } else if(optarg == "partial") { return theory::quantifiers::QCF_PARTIAL; - } else if(optarg == "mc" ) { - return theory::quantifiers::QCF_MC; } else if(optarg == "help") { puts(s_qcfModeHelp.c_str()); exit(1); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a437cfc97..5749da972 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -83,8 +83,6 @@ enum QcfMode { QCF_PROP_EQ, /** use qcf for conflicts, propagations and heuristic instantiations */ QCF_PARTIAL, - /** use qcf for model checking */ - QCF_MC, }; enum UserPatMode { |