summaryrefslogtreecommitdiff
path: root/src/options/options_handler.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r--src/options/options_handler.cpp1825
1 files changed, 27 insertions, 1798 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 35827d3b0..c99b0c7b5 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -29,23 +29,14 @@
#include "base/modal_exception.h"
#include "base/output.h"
#include "lib/strtok_r.h"
-#include "options/arith_heuristic_pivot_rule.h"
-#include "options/arith_propagation_mode.h"
-#include "options/arith_unate_lemma_mode.h"
#include "options/base_options.h"
-#include "options/bv_bitblast_mode.h"
#include "options/bv_options.h"
-#include "options/datatypes_modes.h"
-#include "options/decision_mode.h"
#include "options/decision_options.h"
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/option_exception.h"
-#include "options/printer_modes.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
-#include "options/theoryof_mode.h"
-#include "options/ufss_mode.h"
namespace CVC4 {
namespace options {
@@ -53,16 +44,16 @@ namespace options {
// helper functions
namespace {
-void throwLazyBBUnsupported(theory::bv::SatSolverMode m)
+void throwLazyBBUnsupported(options::SatSolverMode m)
{
std::string sat_solver;
- if (m == theory::bv::SAT_SOLVER_CADICAL)
+ if (m == options::SatSolverMode::CADICAL)
{
sat_solver = "CaDiCaL";
}
else
{
- Assert(m == theory::bv::SAT_SOLVER_CRYPTOMINISAT);
+ Assert(m == options::SatSolverMode::CRYPTOMINISAT);
sat_solver = "CryptoMiniSat";
}
std::string indent(25, ' ');
@@ -120,1130 +111,14 @@ void OptionsHandler::notifyPrintSuccess(std::string option) {
d_options->d_setPrintSuccessListeners.notify();
}
-// theory/arith/options_handlers.h
-const std::string OptionsHandler::s_arithUnateLemmasHelp = "\
-Unate lemmas are generated before SAT search begins using the relationship\n\
-of constant terms and polynomials.\n\
-Modes currently supported by the --unate-lemmas option:\n\
-+ none \n\
-+ ineqs \n\
- Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
-+ eqs \n\
- Outputs lemmas of the general forms\n\
- (= p c) implies (<= p d) for c < d, or\n\
- (= p c) implies (not (= p d)) for c != d.\n\
-+ all \n\
- A combination of inequalities and equalities.\n\
-";
-
-const std::string OptionsHandler::s_arithPropagationModeHelp = "\
-This decides on kind of propagation arithmetic attempts to do during the search.\n\
-+ none\n\
-+ unate\n\
- use constraints to do unate propagation\n\
-+ bi (Bounds Inference)\n\
- infers bounds on basic variables using the upper and lower bounds of the\n\
- non-basic variables in the tableau.\n\
-+both\n\
-";
-
-const std::string OptionsHandler::s_errorSelectionRulesHelp = "\
-This decides on the rule used by simplex during heuristic rounds\n\
-for deciding the next basic variable to select.\n\
-Heuristic pivot rules available:\n\
-+min\n\
- The minimum abs() value of the variable's violation of its bound. (default)\n\
-+max\n\
- The maximum violation the bound\n\
-+varord\n\
- The variable order\n\
-";
-
-ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(
- std::string option, std::string optarg)
-{
- if(optarg == "all") {
- return ALL_PRESOLVE_LEMMAS;
- } else if(optarg == "none") {
- return NO_PRESOLVE_LEMMAS;
- } else if(optarg == "ineqs") {
- return INEQUALITY_PRESOLVE_LEMMAS;
- } else if(optarg == "eqs") {
- return EQUALITY_PRESOLVE_LEMMAS;
- } else if(optarg == "help") {
- puts(s_arithUnateLemmasHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --unate-lemmas: `") +
- optarg + "'. Try --unate-lemmas help.");
- }
-}
-
-ArithPropagationMode OptionsHandler::stringToArithPropagationMode(
- std::string option, std::string optarg)
-{
- if(optarg == "none") {
- return NO_PROP;
- } else if(optarg == "unate") {
- return UNATE_PROP;
- } else if(optarg == "bi") {
- return BOUND_INFERENCE_PROP;
- } else if(optarg == "both") {
- return BOTH_PROP;
- } else if(optarg == "help") {
- puts(s_arithPropagationModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --arith-prop: `") +
- optarg + "'. Try --arith-prop help.");
- }
-}
-
-ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(
- std::string option, std::string optarg)
-{
- if(optarg == "min") {
- return MINIMUM_AMOUNT;
- } else if(optarg == "varord") {
- return VAR_ORDER;
- } else if(optarg == "max") {
- return MAXIMUM_AMOUNT;
- } else if(optarg == "help") {
- puts(s_errorSelectionRulesHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
- optarg + "'. Try --heuristic-pivot-rule help.");
- }
-}
// theory/quantifiers/options_handlers.h
-const std::string OptionsHandler::s_instWhenHelp = "\
-Instantiation modes currently supported by the --inst-when option:\n\
-\n\
-full-last-call (default)\n\
-+ Alternate running instantiation rounds at full effort and last\n\
- call. In other words, interleave instantiation and theory combination.\n\
-\n\
-full\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-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\
-\n\
-";
-
-const std::string OptionsHandler::s_literalMatchHelp = "\
-Literal match modes currently supported by the --literal-match option:\n\
-\n\
-none \n\
-+ Do not use literal matching.\n\
-\n\
-use (default)\n\
-+ Consider phase requirements of triggers conservatively. For example, the\n\
- trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
- terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
- terms in the equivalence class of false. Extends to equality.\n\
-\n\
-agg-predicate \n\
-+ Consider phase requirements aggressively for predicates. In the above example,\n\
- only match P( x ) with terms that are in the equivalence class of false.\n\
-\n\
-agg \n\
-+ Consider the phase requirements aggressively for all triggers.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_mbqiModeHelp =
- "\
-Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
-\n\
-default \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
- Modulo Theories.\n\
-\n\
-none \n\
-+ Disable model-based quantifier instantiation.\n\
-\n\
-trust \n\
-+ Do not instantiate quantified formulas (incomplete technique).\n\
-\n\
-";
-
-const std::string OptionsHandler::s_qcfWhenModeHelp = "\
-Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
-\n\
-default \n\
-+ Default, apply conflict finding at full effort.\n\
-\n\
-last-call \n\
-+ Apply conflict finding at last call, after theory combination and \n\
- and all theories report sat. \n\
-\n\
-std \n\
-+ Apply conflict finding at standard effort.\n\
-\n\
-std-h \n\
-+ Apply conflict finding at standard effort when heuristic says to. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_qcfModeHelp = "\
-Quantifier conflict find modes currently supported by the --quant-cf option:\n\
-\n\
-prop-eq \n\
-+ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\
-\n\
-conflict \n\
-+ Apply QCF algorithm to find conflicts only.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_userPatModeHelp = "\
-User pattern modes currently supported by the --user-pat option:\n\
-\n\
-trust \n\
-+ When provided, use only user-provided patterns for a quantified formula.\n\
-\n\
-use \n\
-+ Use both user-provided and auto-generated patterns when patterns\n\
- are provided for a quantified formula.\n\
-\n\
-resort \n\
-+ Use user-provided patterns only after auto-generated patterns saturate.\n\
-\n\
-ignore \n\
-+ Ignore user-provided patterns. \n\
-\n\
-interleave \n\
-+ Alternate between use/resort. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_triggerSelModeHelp = "\
-Trigger selection modes currently supported by the --trigger-sel option:\n\
-\n\
-min | default \n\
-+ Consider only minimal subterms that meet criteria for triggers.\n\
-\n\
-max \n\
-+ Consider only maximal subterms that meet criteria for triggers. \n\
-\n\
-all \n\
-+ Consider all subterms that meet criteria for triggers. \n\
-\n\
-min-s-max \n\
-+ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\
-\n\
-min-s-all \n\
-+ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
-\n\
-";
-const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\
-Trigger active selection modes currently supported by the \
---trigger-active-sel option:\n\
-\n\
-all \n\
-+ Make all triggers active. \n\
-\n\
-min \n\
-+ Activate triggers with minimal ground terms.\n\
-\n\
-max \n\
-+ Activate triggers with maximal ground terms. \n\
-\n\
-";
-const std::string OptionsHandler::s_prenexQuantModeHelp = "\
-Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
-\n\
-none \n\
-+ Do no prenex nested quantifiers. \n\
-\n\
-default | simple \n\
-+ Default, do simple prenexing of same sign quantifiers.\n\
-\n\
-dnorm \n\
-+ Prenex to disjunctive prenex normal form.\n\
-\n\
-norm \n\
-+ Prenex to prenex normal form.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_cegqiFairModeHelp = "\
-Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --sygus-fair:\n\
-\n\
-uf-dt-size \n\
-+ Enforce fairness using an uninterpreted function for datatypes size.\n\
-\n\
-direct \n\
-+ Enforce fairness using direct conflict lemmas.\n\
-\n\
-default | dt-size \n\
-+ Default, enforce fairness using size operator.\n\
-\n\
-dt-height-bound \n\
-+ Enforce fairness by height bound predicate.\n\
-\n\
-none \n\
-+ Do not enforce fairness. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_termDbModeHelp = "\
-Modes for terms included in the quantifiers term database, supported by\
---term-db-mode:\n\
-\n\
-all \n\
-+ Quantifiers module considers all ground terms.\n\
-\n\
-relevant \n\
-+ Quantifiers module considers only ground terms connected to current assertions. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_iteLiftQuantHelp = "\
-Modes for term database, supported by --ite-lift-quant:\n\
-\n\
-none \n\
-+ Do not lift if-then-else in quantified formulas.\n\
-\n\
-simple \n\
-+ Lift if-then-else in quantified formulas if results in smaller term size.\n\
-\n\
-all \n\
-+ Lift if-then-else in quantified formulas. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_cbqiBvIneqModeHelp =
- "\
-Modes for handling bit-vector inequalities in counterexample-guided\
-instantiation, supported by --cbqi-bv-ineq:\n\
-\n\
-eq-slack (default) \n\
-+ Solve for the inequality using the slack value in the model, e.g.,\
- t > s becomes t = s + ( t-s )^M.\n\
-\n\
-eq-boundary \n\
-+ Solve for the boundary point of the inequality, e.g.,\
- t > s becomes t = s+1.\n\
-\n\
-keep \n\
-+ Solve for the inequality directly using side conditions for invertibility.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
-Modes for single invocation techniques, supported by --cegqi-si:\n\
-\n\
-none \n\
-+ Do not use single invocation techniques.\n\
-\n\
-use (default) \n\
-+ Use single invocation techniques only if grammar is not restrictive.\n\
-\n\
-all-abort \n\
-+ Always use single invocation techniques, abort if solution reconstruction will likely fail,\
- for instance, when the grammar does not have ITE and solution requires it.\n\
-\n\
-all \n\
-+ Always use single invocation techniques. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_cegqiSingleInvRconsHelp =
- "\
-Modes for reconstruction solutions while using single invocation techniques,\
-supported by --cegqi-si-rcons:\n\
-\n\
-none \n\
-+ Do not try to reconstruct solutions in the original (user-provided) grammar\
- when using single invocation techniques. In this mode, solutions produced by\
- CVC4 may violate grammar restrictions.\n\
-\n\
-try \n\
-+ Try to reconstruct solutions in the original grammar when using single\
- invocation techniques in an incomplete (fail-fast) manner.\n\
-\n\
-all-limit \n\
-+ Try to reconstruct solutions in the original grammar, but termintate if a\
- maximum number of rounds for reconstruction is exceeded.\n\
-\n\
-all \n\
-+ Try to reconstruct solutions in the original grammar. In this mode,\
- we do not terminate until a solution is successfully reconstructed. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_cegisSampleHelp =
- "\
-Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\
-supported by --cegis-sample:\n\
-\n\
-none (default) \n\
-+ Do not use sampling with CEGIS.\n\
-\n\
-use \n\
-+ Use sampling to accelerate CEGIS. This will rule out solutions for a\
- conjecture when they are not satisfied by a sample point.\n\
-\n\
-trust \n\
-+ Trust that when a solution for a conjecture is always true under sampling,\
- then it is indeed a solution. Note this option may print out spurious\
- solutions for synthesis conjectures.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusQueryDumpFileHelp =
- "\
-Query file options supported by --sygus-query-gen-dump-files:\n\
-\n\
-none (default) \n\
-+ Do not dump query files when using --sygus-query-gen.\n\
-\n\
-all \n\
-+ Dump all query files.\n\
-\n\
-unsolved \n\
-+ Dump query files that the subsolver did not solve.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusFilterSolHelp =
- "\
-Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\
-\n\
-none (default) \n\
-+ Do not filter sygus solutions.\n\
-\n\
-strong \n\
-+ Filter solutions that are logically stronger than others.\n\
-\n\
-weak \n\
-+ Filter solutions that are logically weaker than others.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusInvTemplHelp = "\
-Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
-\n\
-none \n\
-+ Synthesize invariant directly.\n\
-\n\
-pre \n\
-+ Synthesize invariant based on weakening of precondition .\n\
-\n\
-post \n\
-+ Synthesize invariant based on strengthening of postcondition. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusActiveGenHelp =
- "\
-Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\
-\n\
-none \n\
-+ Do not use actively-generated sygus enumerators.\n\
-\n\
-basic \n\
-+ Use basic type enumerator for actively-generated sygus enumerators.\n\
-\n\
-enum \n\
-+ Use optimized enumerator for actively-generated sygus enumerators.\n\
-\n\
-var-agnostic \n\
-+ Use sygus solver to enumerate terms that are agnostic to variables. \n\
-\n\
-auto (default) \n\
-+ Internally decide the best policy for each enumerator. \n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusUnifPiHelp =
- "\
-Modes for piecewise-independent unification supported by --sygus-unif-pi:\n\
-\n\
-none \n\
-+ Do not use piecewise-independent unification.\n\
-\n\
-complete \n\
-+ Use complete approach for piecewise-independent unification (see Section 3\n\
-of Barbosa et al FMCAD 2019).\n\
-\n\
-cond-enum \n\
-+ Use unconstrained condition enumeration for piecewise-independent\n\
-unification (see Section 4 of Barbosa et al FMCAD 2019).\n\
-\n\
-cond-enum-igain \n\
-+ Same as cond-enum, but additionally uses an information gain heuristic\n\
-when doing decision tree learning.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_sygusGrammarConsHelp =
- "\
-Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\
-\n\
-simple (default) \n\
-+ Use simple grammar construction (no symbolic terms or constants).\n\
-\n\
-any-const \n\
-+ Use symoblic constant constructors.\n\
-\n\
-any-term \n\
-+ When applicable, use constructors corresponding to any symbolic term.\n\
-This option enables a sum-of-monomials grammar for arithmetic. For all\n\
-other types, it enables symbolic constant constructors.\n\
-\n\
-any-term-concise \n\
-+ When applicable, use constructors corresponding to any symbolic term,\n\
-favoring conciseness over generality. This option is equivalent to any-term\n\
-but enables a polynomial grammar for arithmetic when not in a combined\n\
-theory.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_macrosQuantHelp = "\
-Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
-\n\
-all \n\
-+ Infer definitions for functions, including those containing quantified formulas.\n\
-\n\
-ground (default) \n\
-+ Only infer ground definitions for functions.\n\
-\n\
-ground-uf \n\
-+ Only infer ground definitions for functions that result in triggers for all free variables.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_quantDSplitHelp = "\
-Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
-\n\
-none \n\
-+ Never split quantified formulas.\n\
-\n\
-default \n\
-+ Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\
-\n\
-agg \n\
-+ Aggressively split quantified formulas.\n\
-\n\
-";
-
-const std::string OptionsHandler::s_quantRepHelp = "\
-Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
-\n\
-ee \n\
-+ Let equality engine choose representatives.\n\
-\n\
-first (default) \n\
-+ Choose terms that appear first.\n\
-\n\
-depth \n\
-+ Choose terms that are of minimal depth.\n\
-\n\
-";
-
-theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(
- std::string option, std::string optarg)
-{
- if(optarg == "pre-full") {
- return theory::quantifiers::INST_WHEN_PRE_FULL;
- } else if(optarg == "full") {
- return theory::quantifiers::INST_WHEN_FULL;
- } else if(optarg == "full-delay") {
- return theory::quantifiers::INST_WHEN_FULL_DELAY;
- } else if(optarg == "full-last-call") {
- return theory::quantifiers::INST_WHEN_FULL_LAST_CALL;
- } else if(optarg == "full-delay-last-call") {
- return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL;
- } else if(optarg == "last-call") {
- return theory::quantifiers::INST_WHEN_LAST_CALL;
- } else if(optarg == "help") {
- puts(s_instWhenHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --inst-when: `") +
- optarg + "'. Try --inst-when help.");
- }
-}
-
-void OptionsHandler::checkInstWhenMode(std::string option,
- theory::quantifiers::InstWhenMode mode)
-{
- if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) {
- throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
- }
-}
-
-theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(
- std::string option, std::string optarg)
-{
- if(optarg == "none") {
- return theory::quantifiers::LITERAL_MATCH_NONE;
- } else if(optarg == "use") {
- return theory::quantifiers::LITERAL_MATCH_USE;
- } else if(optarg == "agg-predicate") {
- return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
- } else if(optarg == "agg") {
- return theory::quantifiers::LITERAL_MATCH_AGG;
- } else if(optarg == "help") {
- puts(s_literalMatchHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --literal-matching: `") +
- optarg + "'. Try --literal-matching help.");
- }
-}
-
-void OptionsHandler::checkLiteralMatchMode(
- std::string option, theory::quantifiers::LiteralMatchMode mode)
-{
-}
-
-theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
- std::string option, std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::MBQI_NONE;
- } else if(optarg == "default" || optarg == "fmc") {
- return theory::quantifiers::MBQI_FMC;
- } else if(optarg == "trust") {
- return theory::quantifiers::MBQI_TRUST;
- } else if(optarg == "help") {
- puts(s_mbqiModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --mbqi: `") +
- optarg + "'. Try --mbqi help.");
- }
-}
-
-void OptionsHandler::checkMbqiMode(std::string option,
- theory::quantifiers::MbqiMode mode)
-{
-}
-
-theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(
- std::string option, std::string optarg)
-{
- if(optarg == "default") {
- return theory::quantifiers::QCF_WHEN_MODE_DEFAULT;
- } else if(optarg == "last-call") {
- return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL;
- } else if(optarg == "std") {
- return theory::quantifiers::QCF_WHEN_MODE_STD;
- } else if(optarg == "std-h") {
- return theory::quantifiers::QCF_WHEN_MODE_STD_H;
- } else if(optarg == "help") {
- puts(s_qcfWhenModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --quant-cf-when: `") +
- optarg + "'. Try --quant-cf-when help.");
- }
-}
-
-theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
- std::string optarg)
-{
- if(optarg == "conflict") {
- return theory::quantifiers::QCF_CONFLICT_ONLY;
- } else if(optarg == "default" || optarg == "prop-eq") {
- return theory::quantifiers::QCF_PROP_EQ;
- } else if(optarg == "help") {
- puts(s_qcfModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
- optarg + "'. Try --quant-cf-mode help.");
- }
-}
-
-theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(
- std::string option, std::string optarg)
-{
- if(optarg == "use") {
- return theory::quantifiers::USER_PAT_MODE_USE;
- } else if(optarg == "default" || optarg == "trust") {
- return theory::quantifiers::USER_PAT_MODE_TRUST;
- } else if(optarg == "resort") {
- return theory::quantifiers::USER_PAT_MODE_RESORT;
- } else if(optarg == "ignore") {
- return theory::quantifiers::USER_PAT_MODE_IGNORE;
- } else if(optarg == "interleave") {
- return theory::quantifiers::USER_PAT_MODE_INTERLEAVE;
- } else if(optarg == "help") {
- puts(s_userPatModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --user-pat: `") +
- optarg + "'. Try --user-pat help.");
- }
-}
-
-theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(
- std::string option, std::string optarg)
-{
- if(optarg == "default" || optarg == "min") {
- return theory::quantifiers::TRIGGER_SEL_MIN;
- } else if(optarg == "max") {
- return theory::quantifiers::TRIGGER_SEL_MAX;
- } else if(optarg == "min-s-max") {
- return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX;
- } else if(optarg == "min-s-all") {
- return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL;
- } else if(optarg == "all") {
- return theory::quantifiers::TRIGGER_SEL_ALL;
- } else if(optarg == "help") {
- puts(s_triggerSelModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --trigger-sel: `") +
- optarg + "'. Try --trigger-sel help.");
- }
-}
-
-theory::quantifiers::TriggerActiveSelMode
-OptionsHandler::stringToTriggerActiveSelMode(std::string option,
- std::string optarg)
-{
- if(optarg == "default" || optarg == "all") {
- return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
- } else if(optarg == "min") {
- return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN;
- } else if(optarg == "max") {
- return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX;
- } else if(optarg == "help") {
- puts(s_triggerActiveSelModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
- optarg + "'. Try --trigger-active-sel help.");
- }
-}
-
-theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(
- std::string option, std::string optarg)
-{
- if(optarg== "default" || optarg== "simple" ) {
- return theory::quantifiers::PRENEX_QUANT_SIMPLE;
- } else if(optarg == "none") {
- return theory::quantifiers::PRENEX_QUANT_NONE;
- } else if(optarg == "dnorm") {
- return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL;
- } else if(optarg == "norm") {
- return theory::quantifiers::PRENEX_QUANT_NORMAL;
- } else if(optarg == "help") {
- puts(s_prenexQuantModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --prenex-quant: `") +
- optarg + "'. Try --prenex-quant help.");
- }
-}
-
-theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option,
- std::string optarg)
-{
- if(optarg == "direct") {
- return theory::SYGUS_FAIR_DIRECT;
- } else if(optarg == "default" || optarg == "dt-size") {
- return theory::SYGUS_FAIR_DT_SIZE;
- } else if(optarg == "dt-height-bound" ){
- return theory::SYGUS_FAIR_DT_HEIGHT_PRED;
- } else if(optarg == "dt-size-bound" ){
- return theory::SYGUS_FAIR_DT_SIZE_PRED;
- } else if(optarg == "none") {
- return theory::SYGUS_FAIR_NONE;
- } else if(optarg == "help") {
- puts(s_cegqiFairModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --cegqi-fair: `") +
- optarg + "'. Try --cegqi-fair help.");
- }
-}
-
-theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(
- std::string option, std::string optarg)
-{
- if(optarg == "all" ) {
- return theory::quantifiers::TERM_DB_ALL;
- } else if(optarg == "relevant") {
- return theory::quantifiers::TERM_DB_RELEVANT;
- } else if(optarg == "help") {
- puts(s_termDbModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --term-db-mode: `") +
- optarg + "'. Try --term-db-mode help.");
- }
-}
-
-theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(
- std::string option, std::string optarg)
-{
- if(optarg == "all" ) {
- return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL;
- } else if(optarg == "simple") {
- return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE;
- } else if(optarg == "none") {
- return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE;
- } else if(optarg == "help") {
- puts(s_iteLiftQuantHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
- optarg + "'. Try --ite-lift-quant help.");
- }
-}
-
-theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
- std::string option, std::string optarg)
-{
- if (optarg == "eq-slack")
- {
- return theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK;
- }
- else if (optarg == "eq-boundary")
- {
- return theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY;
- }
- else if (optarg == "keep")
- {
- return theory::quantifiers::CBQI_BV_INEQ_KEEP;
- }
- else if (optarg == "help")
- {
- puts(s_cbqiBvIneqModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --cbqi-bv-ineq: `")
- + optarg
- + "'. Try --cbqi-bv-ineq help.");
- }
-}
-
-theory::quantifiers::CegqiSingleInvMode
-OptionsHandler::stringToCegqiSingleInvMode(std::string option,
- std::string optarg)
-{
- if(optarg == "none" ) {
- return theory::quantifiers::CEGQI_SI_MODE_NONE;
- } else if(optarg == "use" || optarg == "default") {
- return theory::quantifiers::CEGQI_SI_MODE_USE;
- } else if(optarg == "all") {
- return theory::quantifiers::CEGQI_SI_MODE_ALL;
- } else if(optarg == "help") {
- puts(s_cegqiSingleInvHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --cegqi-si: `") +
- optarg + "'. Try --cegqi-si help.");
- }
-}
-
-theory::quantifiers::CegqiSingleInvRconsMode
-OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option,
- std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE;
- }
- else if (optarg == "try")
- {
- return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY;
- }
- else if (optarg == "all")
- {
- return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL;
- }
- else if (optarg == "all-limit")
- {
- return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT;
- }
- else if (optarg == "help")
- {
- puts(s_cegqiSingleInvRconsHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --cegqi-si-rcons: `")
- + optarg + "'. Try --cegqi-si-rcons help.");
- }
-}
-
-theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
- std::string option, std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::CEGIS_SAMPLE_NONE;
- }
- else if (optarg == "use")
- {
- return theory::quantifiers::CEGIS_SAMPLE_USE;
- }
- else if (optarg == "trust")
- {
- return theory::quantifiers::CEGIS_SAMPLE_TRUST;
- }
- else if (optarg == "help")
- {
- puts(s_cegisSampleHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --cegis-sample: `")
- + optarg
- + "'. Try --cegis-sample help.");
- }
-}
-
-theory::quantifiers::SygusQueryDumpFilesMode
-OptionsHandler::stringToSygusQueryDumpFilesMode(std::string option,
- std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::SYGUS_QUERY_DUMP_NONE;
- }
- else if (optarg == "all")
- {
- return theory::quantifiers::SYGUS_QUERY_DUMP_ALL;
- }
- else if (optarg == "unsolved")
- {
- return theory::quantifiers::SYGUS_QUERY_DUMP_UNSOLVED;
- }
- else if (optarg == "help")
- {
- puts(s_sygusQueryDumpFileHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(
- std::string("unknown option for --sygus-query-gen-dump-files: `")
- + optarg + "'. Try --sygus-query-gen-dump-files help.");
- }
-}
-theory::quantifiers::SygusFilterSolMode
-OptionsHandler::stringToSygusFilterSolMode(std::string option,
- std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::SYGUS_FILTER_SOL_NONE;
- }
- else if (optarg == "strong")
- {
- return theory::quantifiers::SYGUS_FILTER_SOL_STRONG;
- }
- else if (optarg == "weak")
- {
- return theory::quantifiers::SYGUS_FILTER_SOL_WEAK;
- }
- else if (optarg == "help")
- {
- puts(s_sygusFilterSolHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(
- std::string("unknown option for --sygus-filter-sol: `") + optarg
- + "'. Try --sygus-filter-sol help.");
- }
-}
-
-theory::quantifiers::SygusInvTemplMode
-OptionsHandler::stringToSygusInvTemplMode(std::string option,
- std::string optarg)
+void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
{
- if(optarg == "none" ) {
- return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
- } else if(optarg == "pre") {
- return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE;
- } else if(optarg == "post") {
- return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST;
- } else if(optarg == "help") {
- puts(s_sygusInvTemplHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
- optarg + "'. Try --sygus-inv-templ help.");
- }
-}
-
-theory::quantifiers::SygusActiveGenMode
-OptionsHandler::stringToSygusActiveGenMode(std::string option,
- std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE;
- }
- else if (optarg == "basic")
- {
- return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM_BASIC;
- }
- else if (optarg == "enum")
- {
- return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM;
- }
- else if (optarg == "var-agnostic")
- {
- return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
- }
- else if (optarg == "auto")
- {
- return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO;
- }
- else if (optarg == "help")
- {
- puts(s_sygusActiveGenHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --sygus-inv-templ: `")
- + optarg + "'. Try --sygus-inv-templ help.");
- }
-}
-theory::quantifiers::SygusGrammarConsMode
-OptionsHandler::stringToSygusGrammarConsMode(std::string option,
- std::string optarg)
-{
- if (optarg == "simple")
- {
- return theory::quantifiers::SYGUS_GCONS_SIMPLE;
- }
- else if (optarg == "any-const")
- {
- return theory::quantifiers::SYGUS_GCONS_ANY_CONST;
- }
- else if (optarg == "any-term")
+ if (mode == InstWhenMode::PRE_FULL)
{
- return theory::quantifiers::SYGUS_GCONS_ANY_TERM;
- }
- else if (optarg == "any-term-concise")
- {
- return theory::quantifiers::SYGUS_GCONS_ANY_TERM_CONCISE;
- }
- else if (optarg == "help")
- {
- puts(s_sygusGrammarConsHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(
- std::string("unknown option for --sygus-grammar-cons: `") + optarg
- + "'. Try --sygus-grammar-cons help.");
- }
-}
-
-theory::quantifiers::SygusUnifPiMode OptionsHandler::stringToSygusUnifPiMode(
- std::string option, std::string optarg)
-{
- if (optarg == "none")
- {
- return theory::quantifiers::SYGUS_UNIF_PI_NONE;
- }
- else if (optarg == "complete")
- {
- return theory::quantifiers::SYGUS_UNIF_PI_COMPLETE;
- }
- else if (optarg == "cond-enum")
- {
- return theory::quantifiers::SYGUS_UNIF_PI_CENUM;
- }
- else if (optarg == "cond-enum-igain")
- {
- return theory::quantifiers::SYGUS_UNIF_PI_CENUM_IGAIN;
- }
- else if (optarg == "help")
- {
- puts(s_sygusUnifPiHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --sygus-unif-pi: `")
- + optarg + "'. Try --sygus-unif-pi help.");
- }
-}
-
-theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
- std::string option, std::string optarg)
-{
- if(optarg == "all" ) {
- return theory::quantifiers::MACROS_QUANT_MODE_ALL;
- } else if(optarg == "ground") {
- return theory::quantifiers::MACROS_QUANT_MODE_GROUND;
- } else if(optarg == "ground-uf") {
- return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF;
- } else if(optarg == "help") {
- puts(s_macrosQuantHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
- optarg + "'. Try --macros-quant-mode help.");
- }
-}
-
-theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(
- std::string option, std::string optarg)
-{
- if(optarg == "none" ) {
- return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
- } else if(optarg == "default") {
- return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT;
- } else if(optarg == "agg") {
- return theory::quantifiers::QUANT_DSPLIT_MODE_AGG;
- } else if(optarg == "help") {
- puts(s_quantDSplitHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
- optarg + "'. Try --quant-dsplit-mode help.");
- }
-}
-
-theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(
- std::string option, std::string optarg)
-{
- if(optarg == "none" ) {
- return theory::quantifiers::QUANT_REP_MODE_EE;
- } else if(optarg == "first" || optarg == "default") {
- return theory::quantifiers::QUANT_REP_MODE_FIRST;
- } else if(optarg == "depth") {
- return theory::quantifiers::QUANT_REP_MODE_DEPTH;
- } else if(optarg == "help") {
- puts(s_quantRepHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
- optarg + "'. Try --quant-rep-mode help.");
+ throw OptionException(std::string("Mode pre-full for ") + option
+ + " is not supported in this release.");
}
}
@@ -1270,175 +145,25 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
#endif /* CVC4_USE_ABC */
}
-void OptionsHandler::satSolverEnabledBuild(std::string option, bool value)
-{
-#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
- if (value)
- {
- std::stringstream ss;
- ss << "option `" << option
- << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
- throw OptionException(ss.str());
- }
-#endif
-}
-
-void OptionsHandler::satSolverEnabledBuild(std::string option,
- std::string value)
-{
-#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
- if (!value.empty())
- {
- std::stringstream ss;
- ss << "option `" << option
- << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
- throw OptionException(ss.str());
- }
-#endif
-}
-
-const std::string OptionsHandler::s_bvSatSolverHelp = "\
-Sat solvers currently supported by the --bv-sat-solver option:\n\
-\n\
-minisat (default)\n\
-\n\
-cadical\n\
-\n\
-cryptominisat\n\
-";
-
-theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
- std::string optarg)
+void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
{
- if(optarg == "minisat") {
- return theory::bv::SAT_SOLVER_MINISAT;
- } else if(optarg == "cryptominisat") {
- if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
- options::bitblastMode.wasSetByUser()) {
- throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CRYPTOMINISAT);
- }
- if (!options::bitvectorToBool.wasSetByUser()) {
- options::bitvectorToBool.set(true);
- }
- return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
- }
- else if (optarg == "cadical")
+ if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL)
{
- if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
+ if (options::bitblastMode() == options::BitblastMode::LAZY
&& options::bitblastMode.wasSetByUser())
{
- throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CADICAL);
+ throwLazyBBUnsupported(m);
}
if (!options::bitvectorToBool.wasSetByUser())
{
options::bitvectorToBool.set(true);
}
- return theory::bv::SAT_SOLVER_CADICAL;
- } else if(optarg == "help") {
- puts(s_bvSatSolverHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
- optarg + "'. Try --bv-sat-solver=help.");
- }
-}
-
-const std::string OptionsHandler::s_bvProofFormatHelp =
- "\
-Proof formats currently supported by the --bv-proof-format option:\n\
-\n\
- lrat : DRAT with unit propagation hints to accelerate checking (default)\n\
-\n\
- drat : Deletion and Resolution Asymmetric Tautology Additions \n\
-\n\
- er : Extended Resolution, i.e. resolution with new variable definitions\n\
-\n\
-This option controls which underlying UNSAT proof format is used in BV proofs.\n\
-\n\
-Note: Currently this option does nothing. BV proofs are a work in progress!\
-";
-
-theory::bv::BvProofFormat OptionsHandler::stringToBvProofFormat(
- std::string option, std::string optarg)
-{
- if (optarg == "er")
- {
- return theory::bv::BITVECTOR_PROOF_ER;
- }
- else if (optarg == "lrat")
- {
- return theory::bv::BITVECTOR_PROOF_LRAT;
- }
- else if (optarg == "drat")
- {
- return theory::bv::BITVECTOR_PROOF_DRAT;
- }
- else if (optarg == "help")
- {
- puts(s_bvProofFormatHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --bv-proof-format: `")
- + optarg + "'. Try --bv-proof-format=help.");
}
}
-const std::string OptionsHandler::s_bvOptimizeSatProofHelp =
- "\
-Optimization levels currently supported by the --bv-optimize-sat-proof option:\n\
-\n\
- none : Do not optimize the SAT proof\n\
-\n\
- proof : Use drat-trim to shrink the SAT proof\n\
-\n\
- formula : Use drat-trim to shrink the SAT proof and formula (default)\
-";
-
-theory::bv::BvOptimizeSatProof OptionsHandler::stringToBvOptimizeSatProof(
- std::string option, std::string optarg)
+void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
{
- if (optarg == "none")
- {
- return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE;
- }
- else if (optarg == "proof")
- {
- return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF;
- }
- else if (optarg == "formula")
- {
- return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA;
- }
- else if (optarg == "help")
- {
- puts(s_bvOptimizeSatProofHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --bv-optimize-sat-proof: `")
- + optarg + "'. Try --bv-optimize-sat-proof=help.");
- }
-}
-
-
-const std::string OptionsHandler::s_bitblastingModeHelp = "\
-Bit-blasting modes currently supported by the --bitblast option:\n\
-\n\
-lazy (default)\n\
-+ Separate boolean structure and term reasoning between the core\n\
- SAT solver and the bv SAT solver\n\
-\n\
-eager\n\
-+ Bitblast eagerly to bv SAT solver\n\
-";
-
-theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
- std::string option, std::string optarg)
-{
- if (optarg == "lazy")
+ if (m == options::BitblastMode::LAZY)
{
if (!options::bitvectorPropagate.wasSetByUser())
{
@@ -1452,11 +177,11 @@ theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
{
if (options::incrementalSolving() || options::produceModels())
{
- options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF);
+ options::bitvectorEqualitySlicer.set(options::BvSlicerMode::OFF);
}
else
{
- options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO);
+ options::bitvectorEqualitySlicer.set(options::BvSlicerMode::AUTO);
}
}
@@ -1468,210 +193,17 @@ theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
{
options::bitvectorAlgebraicSolver.set(true);
}
- if (options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
+ if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
{
throwLazyBBUnsupported(options::bvSatSolver());
}
- return theory::bv::BITBLAST_MODE_LAZY;
}
- else if (optarg == "eager")
+ else if (m == BitblastMode::EAGER)
{
if (!options::bitvectorToBool.wasSetByUser())
{
options::bitvectorToBool.set(true);
}
- return theory::bv::BITBLAST_MODE_EAGER;
- }
- else if (optarg == "help")
- {
- puts(s_bitblastingModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --bitblast: `")
- + optarg + "'. Try --bitblast=help.");
- }
-}
-
-const std::string OptionsHandler::s_bvSlicerModeHelp = "\
-Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
-\n\
-auto (default)\n\
-+ Turn slicer on if input has only equalities over core symbols\n\
-\n\
-on\n\
-+ Turn slicer on\n\
-\n\
-off\n\
-+ Turn slicer off\n\
-";
-
-theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
- std::string option, std::string optarg)
-{
- if(optarg == "auto") {
- return theory::bv::BITVECTOR_SLICER_AUTO;
- } else if(optarg == "on") {
- return theory::bv::BITVECTOR_SLICER_ON;
- } else if(optarg == "off") {
- return theory::bv::BITVECTOR_SLICER_OFF;
- } else if(optarg == "help") {
- puts(s_bvSlicerModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
- optarg + "'. Try --bv-eq-slicer=help.");
- }
-}
-
-const std::string OptionsHandler::s_stringsProcessLoopModeHelp =
- "Loop processing modes supported by the --strings-process-loop-mode "
- "option:\n"
- "\n"
- "full (default)\n"
- "+ Perform full processing of looping word equations\n"
- "\n"
- "simple (default with --strings-fmf)\n"
- "+ Omit normal loop breaking\n"
- "\n"
- "simple-abort\n"
- "+ Abort when normal loop breaking is required\n"
- "\n"
- "none\n"
- "+ Omit loop processing\n"
- "\n"
- "abort\n"
- "+ Abort if looping word equations are encountered\n";
-
-theory::strings::ProcessLoopMode OptionsHandler::stringToStringsProcessLoopMode(
- std::string option, std::string optarg)
-{
- if (optarg == "full")
- {
- return theory::strings::ProcessLoopMode::FULL;
- }
- else if (optarg == "simple")
- {
- return theory::strings::ProcessLoopMode::SIMPLE;
- }
- else if (optarg == "simple-abort")
- {
- return theory::strings::ProcessLoopMode::SIMPLE_ABORT;
- }
- else if (optarg == "none")
- {
- return theory::strings::ProcessLoopMode::NONE;
- }
- else if (optarg == "abort")
- {
- return theory::strings::ProcessLoopMode::ABORT;
- }
- else if (optarg == "help")
- {
- puts(s_stringsProcessLoopModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(
- std::string("unknown option for --strings-process-loop-mode: `")
- + optarg + "'. Try --strings-process-loop-mode=help.");
- }
-}
-
-const std::string OptionsHandler::s_regExpInterModeHelp =
- "\
-Regular expression intersection modes supported by the --re-inter-mode option\
-\n\
-\n\
-all \n\
-+ Compute intersections for all regular expressions.\n\
-\n\
-constant (default)\n\
-+ Compute intersections only between regular expressions that do not contain\
-re.allchar or re.range\n\
-\n\
-one-constant\n\
-+ Compute intersections only between regular expressions such that at least one\
-side does not contain re.allchar or re.range\n\
-\n\
-none\n\
-+ Do not compute intersections for regular expressions\n\
-";
-
-theory::strings::RegExpInterMode OptionsHandler::stringToRegExpInterMode(
- std::string option, std::string optarg)
-{
- if (optarg == "all")
- {
- return theory::strings::RegExpInterMode::RE_INTER_ALL;
- }
- else if (optarg == "constant")
- {
- return theory::strings::RegExpInterMode::RE_INTER_CONSTANT;
- }
- else if (optarg == "one-constant")
- {
- return theory::strings::RegExpInterMode::RE_INTER_ONE_CONSTANT;
- }
- else if (optarg == "none")
- {
- return theory::strings::RegExpInterMode::RE_INTER_NONE;
- }
- else if (optarg == "help")
- {
- puts(s_regExpInterModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --re-inter-mode: `")
- + optarg + "'. Try --re-inter-mode=help.");
- }
-}
-
-const std::string OptionsHandler::s_boolToBVModeHelp =
- "\
-BoolToBV pass modes supported by the --bool-to-bv option:\n\
-\n\
-off (default)\n\
-+ Don't push any booleans to width one bit-vectors\n\
-\n\
-ite\n\
-+ Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\
- if not all sub-formulas can be turned to bit-vectors\n\
-\n\
-all\n\
-+ Force all booleans to be bit-vectors of width one except at the top level.\n\
- Most aggressive mode\n\
-";
-
-preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode(
- std::string option, std::string optarg)
-{
- if (optarg == "off")
- {
- return preprocessing::passes::BOOL_TO_BV_OFF;
- }
- else if (optarg == "ite")
- {
- return preprocessing::passes::BOOL_TO_BV_ITE;
- }
- else if (optarg == "all")
- {
- return preprocessing::passes::BOOL_TO_BV_ALL;
- }
- else if (optarg == "help")
- {
- puts(s_boolToBVModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --bool-to-bv: `")
- + optarg
- + "'. Try --bool-to-bv=help");
}
}
@@ -1679,11 +211,12 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg)
{
if(arg) {
if(options::bitblastMode.wasSetByUser()) {
- if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) {
+ if (options::bitblastMode() != options::BitblastMode::EAGER)
+ {
throw OptionException("bitblast-aig must be used with eager bitblaster");
}
} else {
- theory::bv::BitblastMode mode = stringToBitblastMode("", "eager");
+ options::BitblastMode mode = stringToBitblastMode("", "eager");
options::bitblastMode.set(mode);
}
if(!options::bitvectorAigSimplifications.wasSetByUser()) {
@@ -1692,68 +225,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg)
}
}
-// theory/uf/options_handlers.h
-const std::string OptionsHandler::s_ufssModeHelp = "\
-UF with cardinality options currently supported by the --uf-ss option when\n\
-combined with finite model finding:\n\
-\n\
-full \n\
-+ Default, use UF with cardinality to find minimal models for uninterpreted\n\
-sorts.\n\
-\n\
-no-minimal \n\
-+ Use UF with cardinality to shrink models, but do no enforce minimality.\n\
-\n\
-none \n\
-+ Do not use UF with cardinality to shrink model sizes. \n\
-\n\
-";
-
-theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option,
- std::string optarg)
-{
- if(optarg == "default" || optarg == "full" ) {
- return theory::uf::UF_SS_FULL;
- } else if(optarg == "no-minimal") {
- return theory::uf::UF_SS_NO_MINIMAL;
- } else if(optarg == "none") {
- return theory::uf::UF_SS_NONE;
- } else if(optarg == "help") {
- puts(s_ufssModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --uf-ss: `") +
- optarg + "'. Try --uf-ss help.");
- }
-}
-
-
-
-// theory/options_handlers.h
-const std::string OptionsHandler::s_theoryOfModeHelp = "\
-TheoryOf modes currently supported by the --theoryof-mode option:\n\
-\n\
-type (default) \n\
-+ type variables, constants and equalities by type\n\
-\n\
-term \n\
-+ type variables as uninterpreted, equalities by the parametric theory\n\
-";
-
-theory::TheoryOfMode OptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) {
- if(optarg == "type") {
- return theory::THEORY_OF_TYPE_BASED;
- } else if(optarg == "term") {
- return theory::THEORY_OF_TERM_BASED;
- } else if(optarg == "help") {
- puts(s_theoryOfModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --theoryof-mode: `") +
- optarg + "'. Try --theoryof-mode help.");
- }
-}
-
// theory/options_handlers.h
std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) {
std::string currentList = options::useTheoryList();
@@ -1768,19 +239,7 @@ void OptionsHandler::notifyUseTheoryList(std::string option) {
d_options->d_useTheoryListListeners.notify();
}
-
-
// printer/options_handlers.h
-const std::string OptionsHandler::s_modelFormatHelp = "\
-Model format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print model as expressions in the output language format.\n\
-\n\
-table\n\
-+ Print functional expressions over finite domains in a table format.\n\
-";
-
const std::string OptionsHandler::s_instFormatHelp = "\
Inst format modes currently supported by the --inst-format option:\n\
\n\
@@ -1791,29 +250,13 @@ szs\n\
+ Print instantiations as SZS compliant proof.\n\
";
-ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option,
- std::string optarg)
-{
- if(optarg == "default") {
- return MODEL_FORMAT_MODE_DEFAULT;
- } else if(optarg == "table") {
- return MODEL_FORMAT_MODE_TABLE;
- } else if(optarg == "help") {
- puts(s_modelFormatHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --model-format: `") +
- optarg + "'. Try --model-format help.");
- }
-}
-
InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
std::string optarg)
{
if(optarg == "default") {
- return INST_FORMAT_MODE_DEFAULT;
+ return InstFormatMode::DEFAULT;
} else if(optarg == "szs") {
- return INST_FORMAT_MODE_SZS;
+ return InstFormatMode::SZS;
} else if(optarg == "help") {
puts(s_instFormatHelp.c_str());
exit(1);
@@ -1823,224 +266,10 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
}
}
-
// decision/options_handlers.h
-const std::string OptionsHandler::s_decisionModeHelp = "\
-Decision modes currently supported by the --decision option:\n\
-\n\
-internal (default)\n\
-+ Use the internal decision heuristics of the SAT solver\n\
-\n\
-justification\n\
-+ An ATGP-inspired justification heuristic\n\
-\n\
-justification-stoponly\n\
-+ Use the justification heuristic only to stop early, not for decisions\n\
-";
-
-decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option,
- std::string optarg)
-{
- options::decisionStopOnly.set(false);
-
- if(optarg == "internal") {
- return decision::DECISION_STRATEGY_INTERNAL;
- } else if(optarg == "justification") {
- return decision::DECISION_STRATEGY_JUSTIFICATION;
- } else if(optarg == "justification-stoponly") {
- options::decisionStopOnly.set(true);
- return decision::DECISION_STRATEGY_JUSTIFICATION;
- } else if(optarg == "help") {
- puts(s_decisionModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --decision: `") +
- optarg + "'. Try --decision help.");
- }
-}
-
-decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(
- std::string option, std::string optarg)
-{
- if(optarg == "off")
- return decision::DECISION_WEIGHT_INTERNAL_OFF;
- else if(optarg == "max")
- return decision::DECISION_WEIGHT_INTERNAL_MAX;
- else if(optarg == "sum")
- return decision::DECISION_WEIGHT_INTERNAL_SUM;
- else if(optarg == "usr1")
- return decision::DECISION_WEIGHT_INTERNAL_USR1;
- else
- throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
-}
-
-
-// smt/options_handlers.h
-const std::string OptionsHandler::s_simplificationHelp = "\
-Simplification modes currently supported by the --simplification option:\n\
-\n\
-batch (default) \n\
-+ save up all ASSERTions; run nonclausal simplification and clausal\n\
- (MiniSat) propagation for all of them only after reaching a querying command\n\
- (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
-\n\
-none\n\
-+ do not perform nonclausal simplification\n\
-";
-
-SimplificationMode OptionsHandler::stringToSimplificationMode(
- std::string option, std::string optarg)
-{
- if(optarg == "batch") {
- return SIMPLIFICATION_MODE_BATCH;
- } else if(optarg == "none") {
- return SIMPLIFICATION_MODE_NONE;
- } else if(optarg == "help") {
- puts(s_simplificationHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --simplification: `") +
- optarg + "'. Try --simplification help.");
- }
-}
-
-const std::string OptionsHandler::s_modelCoresHelp =
- "\
-Model cores modes currently supported by the --model-cores option:\n\
-\n\
-none (default) \n\
-+ do not compute model cores\n\
-\n\
-simple\n\
-+ only include a subset of variables whose values are sufficient to show the\n\
-input formula is satisfied by the given model\n\
-\n\
-non-implied\n\
-+ only include a subset of variables whose values, in addition to the values\n\
-of variables whose values are implied, are sufficient to show the input\n\
-formula is satisfied by the given model\n\
-\n\
-";
-
-ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option,
- std::string optarg)
-{
- if (optarg == "none")
- {
- return MODEL_CORES_NONE;
- }
- else if (optarg == "simple")
- {
- return MODEL_CORES_SIMPLE;
- }
- else if (optarg == "non-implied")
- {
- return MODEL_CORES_NON_IMPLIED;
- }
- else if (optarg == "help")
- {
- puts(s_modelCoresHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --model-cores: `")
- + optarg + "'. Try --model-cores help.");
- }
-}
-
-const std::string OptionsHandler::s_blockModelsHelp =
- "\
-Blocking models modes are currently supported by the --block-models option:\n\
-\n\
-none (default) \n\
-+ do not block models\n\
-\n\
-literals\n\
-+ block models based on the SAT skeleton\n\
-\n\
-values\n\
-+ block models based on the concrete model values for the free variables.\n\
-\n\
-";
-
-BlockModelsMode OptionsHandler::stringToBlockModelsMode(std::string option,
- std::string optarg)
+void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
{
- if (optarg == "none")
- {
- return BLOCK_MODELS_NONE;
- }
- else if (optarg == "literals")
- {
- return BLOCK_MODELS_LITERALS;
- }
- else if (optarg == "values")
- {
- return BLOCK_MODELS_VALUES;
- ;
- }
- else if (optarg == "help")
- {
- puts(s_blockModelsHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --block-models: `")
- + optarg + "'. Try --block-models help.");
- }
-}
-
-const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
- "\
-Modes for sygus solution output, supported by --sygus-out:\n\
-\n\
-status \n\
-+ Print only status for check-synth calls.\n\
-\n\
-status-and-def (default) \n\
-+ Print status followed by definition corresponding to solution.\n\
-\n\
-status-or-def \n\
-+ Print status if infeasible, or definition corresponding to\n\
- solution if feasible.\n\
-\n\
-sygus-standard \n\
-+ Print based on SyGuS standard.\n\
-\n\
-";
-
-SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
- std::string option, std::string optarg)
-{
- if (optarg == "status")
- {
- return SYGUS_SOL_OUT_STATUS;
- }
- else if (optarg == "status-and-def")
- {
- return SYGUS_SOL_OUT_STATUS_AND_DEF;
- }
- else if (optarg == "status-or-def")
- {
- return SYGUS_SOL_OUT_STATUS_OR_DEF;
- }
- else if (optarg == "sygus-standard")
- {
- return SYGUS_SOL_OUT_STANDARD;
- }
- else if (optarg == "help")
- {
- puts(s_sygusSolutionOutModeHelp.c_str());
- exit(1);
- }
- else
- {
- throw OptionException(std::string("unknown option for --sygus-out: `")
- + optarg
- + "'. Try --sygus-out help.");
- }
+ options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
}
void OptionsHandler::setProduceAssertions(std::string option, bool value)
@@ -2052,9 +281,9 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value)
void OptionsHandler::proofEnabledBuild(std::string option, bool value)
{
#ifdef CVC4_PROOF
- if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
- && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT
- && options::bvSatSolver() != theory::bv::SAT_SOLVER_CRYPTOMINISAT)
+ if (value && options::bitblastMode() == options::BitblastMode::EAGER
+ && options::bvSatSolver() != options::SatSolverMode::MINISAT
+ && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT)
{
throw OptionException(
"Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback