diff options
Diffstat (limited to 'src/options')
44 files changed, 955 insertions, 4110 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 70af2f056..4fb331e50 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -1,21 +1,22 @@ +# Check if the toml Python module is installed. +execute_process( + COMMAND + ${PYTHON_EXECUTABLE} -c "import toml" + RESULT_VARIABLE + RET_TOML + ERROR_QUIET +) + +if(RET_TOML) + message(FATAL_ERROR + "Could not find Python module toml. Install via `pip install toml'.") +endif() + libcvc4_add_sources( argument_extender.h argument_extender_implementation.cpp argument_extender_implementation.h - arith_heuristic_pivot_rule.cpp - arith_heuristic_pivot_rule.h - arith_propagation_mode.cpp - arith_propagation_mode.h - arith_unate_lemma_mode.cpp - arith_unate_lemma_mode.h base_handlers.h - bool_to_bv_mode.cpp - bool_to_bv_mode.h - bv_bitblast_mode.cpp - bv_bitblast_mode.h - datatypes_modes.h - decision_mode.cpp - decision_mode.h decision_weight.h didyoumean.cpp didyoumean.h @@ -31,18 +32,8 @@ libcvc4_add_sources( options_public_functions.cpp printer_modes.cpp printer_modes.h - quantifiers_modes.cpp - quantifiers_modes.h set_language.cpp set_language.h - smt_modes.cpp - smt_modes.h - strings_modes.cpp - strings_modes.h - sygus_out_mode.h - theoryof_mode.cpp - theoryof_mode.h - ufss_mode.h ) set(options_toml_files diff --git a/src/options/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp deleted file mode 100644 index 6c1312dbf..000000000 --- a/src/options/arith_heuristic_pivot_rule.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/********************* */ -/*! \file arith_heuristic_pivot_rule.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/arith_heuristic_pivot_rule.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) { - switch(rule) { - case MINIMUM_AMOUNT: - out << "MINIMUM_AMOUNT"; - break; - case VAR_ORDER: - out << "VAR_ORDER"; - break; - case MAXIMUM_AMOUNT: - out << "MAXIMUM_AMOUNT"; - break; - default: - out << "ArithHeuristicPivotRule!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h deleted file mode 100644 index 2caa21043..000000000 --- a/src/options/arith_heuristic_pivot_rule.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_heuristic_pivot_rule.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H -#define CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H - -#include <iostream> - -namespace CVC4 { - -enum ErrorSelectionRule { - VAR_ORDER, - MINIMUM_AMOUNT, - MAXIMUM_AMOUNT, - SUM_METRIC -}; - -std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */ diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 80403ee0d..ab8164130 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -7,11 +7,21 @@ header = "options/arith_options.h" category = "regular" long = "unate-lemmas=MODE" type = "ArithUnateLemmaMode" - default = "ALL_PRESOLVE_LEMMAS" - handler = "stringToArithUnateLemmaMode" - includes = ["options/arith_unate_lemma_mode.h"] + default = "ALL" read_only = true help = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)" + help_mode = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials." +[[option.mode.ALL]] + name = "all" + help = "A combination of inequalities and equalities." +[[option.mode.EQUALITY]] + name = "eqs" + help = "Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d." +[[option.mode.INEQUALITY]] + name = "ineqs" + help = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d." +[[option.mode.NO]] + name = "none" [[option]] name = "arithPropagationMode" @@ -19,10 +29,22 @@ header = "options/arith_options.h" long = "arith-prop=MODE" type = "ArithPropagationMode" default = "BOTH_PROP" - handler = "stringToArithPropagationMode" - includes = ["options/arith_propagation_mode.h"] read_only = true help = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)" + help_mode = "This decides on kind of propagation arithmetic attempts to do during the search." +[[option.mode.NO_PROP]] + name = "none" +[[option.mode.UNATE_PROP]] + name = "unate" + help = "Use constraints to do unate propagation." +[[option.mode.BOUND_INFERENCE_PROP]] + name = "bi" + help = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau." +[[option.mode.BOTH_PROP]] + name = "both" + help = "Use bounds inference and unate." + + # The maximum number of difference pivots to do per invocation of simplex. # If this is negative, the number of pivots done is the number of variables. @@ -55,10 +77,20 @@ header = "options/arith_options.h" long = "error-selection-rule=RULE" type = "ErrorSelectionRule" default = "MINIMUM_AMOUNT" - handler = "stringToErrorSelectionRule" - includes = ["options/arith_heuristic_pivot_rule.h"] read_only = true help = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)" + help_mode = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select." +[[option.mode.MINIMUM_AMOUNT]] + name = "min" + help = "The minimum abs() value of the variable's violation of its bound." +[[option.mode.VAR_ORDER]] + name = "varord" + help = "The variable order." +[[option.mode.MAXIMUM_AMOUNT]] + name = "max" + help = "The maximum violation the bound." +[[option.mode.SUM_METRIC]] + name = "sum" # The number of pivots before simplex rechecks every basic variable for a conflict [[option]] diff --git a/src/options/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp deleted file mode 100644 index 895a01381..000000000 --- a/src/options/arith_propagation_mode.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file arith_propagation_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/arith_propagation_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) { - switch(mode) { - case NO_PROP: - out << "NO_PROP"; - break; - case UNATE_PROP: - out << "UNATE_PROP"; - break; - case BOUND_INFERENCE_PROP: - out << "BOUND_INFERENCE_PROP"; - break; - case BOTH_PROP: - out << "BOTH_PROP"; - break; - default: - out << "ArithPropagationMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/arith_propagation_mode.h b/src/options/arith_propagation_mode.h deleted file mode 100644 index b2c6b4c61..000000000 --- a/src/options/arith_propagation_mode.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_propagation_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H -#define CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H - -#include <iostream> - -namespace CVC4 { - -enum ArithPropagationMode { - NO_PROP, - UNATE_PROP, - BOUND_INFERENCE_PROP, - BOTH_PROP -}; - -std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */ diff --git a/src/options/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp deleted file mode 100644 index 34fbeb3b2..000000000 --- a/src/options/arith_unate_lemma_mode.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file arith_unate_lemma_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/arith_unate_lemma_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) { - switch(mode) { - case NO_PRESOLVE_LEMMAS: - out << "NO_PRESOLVE_LEMMAS"; - break; - case INEQUALITY_PRESOLVE_LEMMAS: - out << "INEQUALITY_PRESOLVE_LEMMAS"; - break; - case EQUALITY_PRESOLVE_LEMMAS: - out << "EQUALITY_PRESOLVE_LEMMAS"; - break; - case ALL_PRESOLVE_LEMMAS: - out << "ALL_PRESOLVE_LEMMAS"; - break; - default: - out << "ArithUnateLemmaMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h deleted file mode 100644 index a917b83fd..000000000 --- a/src/options/arith_unate_lemma_mode.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_unate_lemma_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H -#define CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H - -#include <iostream> - -namespace CVC4 { - -typedef enum { - NO_PRESOLVE_LEMMAS, - INEQUALITY_PRESOLVE_LEMMAS, - EQUALITY_PRESOLVE_LEMMAS, - ALL_PRESOLVE_LEMMAS -} ArithUnateLemmaMode; - -std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */ diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp deleted file mode 100644 index 12fd3c1f9..000000000 --- a/src/options/bool_to_bv_mode.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/********************* */ -/*! \file bool_to_bv_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ - -#include "options/bool_to_bv_mode.h" - -#include <iostream> - - -namespace CVC4 -{ - std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode) { - switch(mode) { - case preprocessing::passes::BOOL_TO_BV_OFF: - out << "BOOL_TO_BV_OFF"; - break; - case preprocessing::passes::BOOL_TO_BV_ITE: - out << "BOOL_TO_BV_ITE"; - break; - case preprocessing::passes::BOOL_TO_BV_ALL: - out << "BOOL_TO_BV_ALL"; - break; - default: - out << "BoolToBVMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; - } -} // namespace CVC4 diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h deleted file mode 100644 index 2dbd723c9..000000000 --- a/src/options/bool_to_bv_mode.h +++ /dev/null @@ -1,57 +0,0 @@ -/********************* */ -/*! \file bool_to_bv_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ - -#include "cvc4_private.h" - -#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H -#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H - -#include <iosfwd> - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -/** Enumeration of bool-to-bv modes */ -enum BoolToBVMode -{ - /** - * No bool-to-bv pass - */ - BOOL_TO_BV_OFF, - - /** - * Only lower bools in condition of ITEs - * Tries to give more info to bit-vector solver - * by using bit-vector-ITEs when possible - */ - BOOL_TO_BV_ITE, - - /** - * Lower every bool beneath the top layer to be a - * bit-vector - */ - BOOL_TO_BV_ALL -}; -} -} - -std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode); - -} - -#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp deleted file mode 100644 index d2425831a..000000000 --- a/src/options/bv_bitblast_mode.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/*! \file bv_bitblast_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Bitblast modes for bit-vector solver. - ** - ** Bitblast modes for bit-vector solver. - **/ - -#include "options/bv_bitblast_mode.h" - -#include <iostream> - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) { - switch(mode) { - case theory::bv::BITBLAST_MODE_LAZY: - out << "BITBLAST_MODE_LAZY"; - break; - case theory::bv::BITBLAST_MODE_EAGER: - out << "BITBLAST_MODE_EAGER"; - break; - default: - out << "BitblastMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { - switch(mode) { - case theory::bv::BITVECTOR_SLICER_ON: - out << "BITVECTOR_SLICER_ON"; - break; - case theory::bv::BITVECTOR_SLICER_OFF: - out << "BITVECTOR_SLICER_OFF"; - break; - case theory::bv::BITVECTOR_SLICER_AUTO: - out << "BITVECTOR_SLICER_AUTO"; - break; - default: - out << "BvSlicerMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) { - switch(solver) { - case theory::bv::SAT_SOLVER_MINISAT: - out << "SAT_SOLVER_MINISAT"; - break; - case theory::bv::SAT_SOLVER_CRYPTOMINISAT: - out << "SAT_SOLVER_CRYPTOMINISAT"; - break; - default: - out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format) -{ - switch (format) - { - case theory::bv::BITVECTOR_PROOF_ER: out << "BITVECTOR_PROOF_ER"; break; - case theory::bv::BITVECTOR_PROOF_DRAT: out << "BITVECTOR_PROOF_DRAT"; break; - case theory::bv::BITVECTOR_PROOF_LRAT: out << "BITVECTOR_PROOF_LRAT"; break; - default: out << "BvProofFormat:UNKNOWN![" << unsigned(format) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, - theory::bv::BvOptimizeSatProof level) -{ - switch (level) - { - case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE: - out << "BITVECTOR_OPTIMIZE_SAT_PROOF_NONE"; - break; - case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF: - out << "BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF"; - break; - case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA: - out << "BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA"; - break; - default: out << "BvOptimizeSatProof:UNKNOWN![" << unsigned(level) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h deleted file mode 100644 index 7243c38e1..000000000 --- a/src/options/bv_bitblast_mode.h +++ /dev/null @@ -1,123 +0,0 @@ -/********************* */ -/*! \file bv_bitblast_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Alex Ozdemir, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Bitblasting modes for bit-vector solver. - ** - ** Bitblasting modes for bit-vector solver. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__BV__BITBLAST_MODE_H -#define CVC4__THEORY__BV__BITBLAST_MODE_H - -#include <iosfwd> - -namespace CVC4 { -namespace theory { -namespace bv { - -/** Enumeration of bit-blasting modes */ -enum BitblastMode { - - /** - * Lazy bit-blasting that separates boolean reasoning - * from term reasoning. - */ - BITBLAST_MODE_LAZY, - - /** - * Bit-blast eagerly to the bit-vector SAT solver. - */ - BITBLAST_MODE_EAGER -};/* enum BitblastMode */ - -/** Enumeration of bit-vector equality slicer mode */ -enum BvSlicerMode { - - /** - * Force the slicer on. - */ - BITVECTOR_SLICER_ON, - - /** - * Slicer off. - */ - BITVECTOR_SLICER_OFF, - - /** - * Auto enable slicer if problem has only equalities. - */ - BITVECTOR_SLICER_AUTO - -};/* enum BvSlicerMode */ - -/** Enumeration of sat solvers that can be used. */ -enum SatSolverMode -{ - SAT_SOLVER_MINISAT, - SAT_SOLVER_CRYPTOMINISAT, - SAT_SOLVER_CADICAL, -}; /* enum SatSolver */ - -/** - * When the BV solver does eager bitblasting backed by CryptoMiniSat, proofs - * can be written in a variety of formats. - */ -enum BvProofFormat -{ - /** - * Write extended resolution proofs. - */ - BITVECTOR_PROOF_ER, - /** - * Write DRAT proofs. - */ - BITVECTOR_PROOF_DRAT, - /** - * Write LRAT proofs. - */ - BITVECTOR_PROOF_LRAT, -}; - -/** - * When the BV solver does eager bit-blasting backed by DRAT-producing SAT solvers, proofs - * can be written in a variety of formats. - */ -enum BvOptimizeSatProof -{ - /** - * Do not optimize the SAT proof. - */ - BITVECTOR_OPTIMIZE_SAT_PROOF_NONE = 0, - /** - * Optimize the SAT proof, but do not shrink the formula - */ - BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF = 1, - /** - * Optimize the SAT proof and shrink the formula - */ - BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA = 2, -}; - - -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode); -std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode); -std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode); -std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format); -std::ostream& operator<<(std::ostream& out, theory::bv::BvOptimizeSatProof level); - -}/* CVC4 namespace */ - -#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 9529b7500..00755d8a6 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -6,46 +6,72 @@ header = "options/bv_options.h" name = "bvProofFormat" category = "expert" long = "bv-proof-format=MODE" - type = "CVC4::theory::bv::BvProofFormat" - default = "CVC4::theory::bv::BITVECTOR_PROOF_ER" - handler = "stringToBvProofFormat" - predicates = ["satSolverEnabledBuild"] - includes = ["options/bv_bitblast_mode.h"] + type = "BvProofFormat" + default = "ER" + predicates = ["checkSatSolverEnabled<BvProofFormat>"] help = "choose which UNSAT proof format to use, see --bv-sat-solver=help" + help_mode = "Bit-vector proof formats." +[[option.mode.ER]] + name = "er" + help = "Extended Resolution, i.e. resolution with new variable definitions." +[[option.mode.DRAT]] + name = "drat" + help = "Deletion and Resolution Asymmetric Tautology Additions." +[[option.mode.LRAT]] + name = "lrat" + help = "DRAT with unit propagation hints to accelerate checking." [[option]] name = "bvOptimizeSatProof" category = "expert" long = "bv-optimize-sat-proof=MODE" - type = "CVC4::theory::bv::BvOptimizeSatProof" - default = "CVC4::theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA" - handler = "stringToBvOptimizeSatProof" - predicates = ["satSolverEnabledBuild"] - includes = ["options/bv_bitblast_mode.h"] + type = "BvOptimizeSatProof" + default = "FORMULA" + predicates = ["checkSatSolverEnabled<BvOptimizeSatProof>"] help = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help" + help_mode = "SAT proof optimization level." +[[option.mode.NONE]] + name = "none" + help = "Do not optimize the SAT proof." +[[option.mode.PROOF]] + name = "proof" + help = "Use drat-trim to shrink the SAT proof." +[[option.mode.FORMULA]] + name = "formula" + help = "Use drat-trim to shrink the SAT proof and formula." [[option]] name = "bvSatSolver" smt_name = "bv-sat-solver" category = "expert" long = "bv-sat-solver=MODE" - type = "CVC4::theory::bv::SatSolverMode" - default = "CVC4::theory::bv::SAT_SOLVER_MINISAT" - handler = "stringToSatSolver" - predicates = ["satSolverEnabledBuild"] - includes = ["options/bv_bitblast_mode.h"] + type = "SatSolverMode" + default = "MINISAT" + predicates = ["checkBvSatSolver"] help = "choose which sat solver to use, see --bv-sat-solver=help" + help_mode = "SAT solver for bit-blasting backend." +[[option.mode.MINISAT]] + name = "minisat" +[[option.mode.CRYPTOMINISAT]] + name = "cryptominisat" +[[option.mode.CADICAL]] + name = "cadical" [[option]] name = "bitblastMode" smt_name = "bitblast" category = "regular" long = "bitblast=MODE" - type = "CVC4::theory::bv::BitblastMode" - default = "CVC4::theory::bv::BITBLAST_MODE_LAZY" - handler = "stringToBitblastMode" - includes = ["options/bv_bitblast_mode.h"] + type = "BitblastMode" + default = "LAZY" help = "choose bitblasting mode, see --bitblast=help" + help_mode = "Bit-blasting modes." +[[option.mode.LAZY]] + name = "lazy" + help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver." +[[option.mode.EAGER]] + name = "eager" + help = "Bitblast eagerly to bit-vector SAT solver." [[option]] name = "bitvectorAig" @@ -85,12 +111,20 @@ header = "options/bv_options.h" name = "bitvectorEqualitySlicer" category = "regular" long = "bv-eq-slicer=MODE" - type = "CVC4::theory::bv::BvSlicerMode" - default = "CVC4::theory::bv::BITVECTOR_SLICER_OFF" - handler = "stringToBvSlicerMode" - includes = ["options/bv_bitblast_mode.h"] + type = "BvSlicerMode" + default = "OFF" links = ["--bv-eq-solver"] help = "turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)" + help_mode = "Bit-vector equality slicer modes." +[[option.mode.ON]] + name = "on" + help = "Turn slicer on." +[[option.mode.OFF]] + name = "off" + help = "Turn slicer off." +[[option.mode.AUTO]] + name = "auto" + help = "Turn slicer on if input has only equalities over core symbols." [[option]] name = "bitvectorInequalitySolver" @@ -130,11 +164,19 @@ header = "options/bv_options.h" smt_name = "bool-to-bv" category = "regular" long = "bool-to-bv=MODE" - type = "CVC4::preprocessing::passes::BoolToBVMode" - default = "CVC4::preprocessing::passes::BOOL_TO_BV_OFF" - handler = "stringToBoolToBVMode" - includes = ["options/bool_to_bv_mode.h"] + type = "BoolToBVMode" + default = "OFF" help = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help" + help_mode = "BoolToBV preprocessing pass modes." +[[option.mode.OFF]] + name = "off" + help = "Don't push any booleans to width one bit-vectors." +[[option.mode.ITE]] + name = "ite" + help = "Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if not all sub-formulas can be turned to bit-vectors." +[[option.mode.ALL]] + name = "all" + help = "Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode." [[option]] name = "bitwiseEq" diff --git a/src/options/datatypes_modes.h b/src/options/datatypes_modes.h deleted file mode 100644 index 8d7ced9e2..000000000 --- a/src/options/datatypes_modes.h +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file datatypes_modes.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__BASE__DATATYPES_MODES_H -#define CVC4__BASE__DATATYPES_MODES_H - -#include <iostream> - -namespace CVC4 { -namespace theory { - -enum SygusFairMode { - /** enforce fairness by direct conflict lemmas */ - SYGUS_FAIR_DIRECT, - /** enforce fairness by datatypes size */ - SYGUS_FAIR_DT_SIZE, - /** enforce fairness by datatypes height bound */ - SYGUS_FAIR_DT_HEIGHT_PRED, - /** enforce fairness by datatypes size bound */ - SYGUS_FAIR_DT_SIZE_PRED, - /** do not use fair strategy for CEGQI */ - SYGUS_FAIR_NONE, -}; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__BASE__DATATYPES_MODES_H */ diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 67829e033..7eb9d30c5 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -151,12 +151,26 @@ header = "options/datatypes_options.h" name = "sygusFair" category = "regular" long = "sygus-fair=MODE" - type = "CVC4::theory::SygusFairMode" - default = "CVC4::theory::SYGUS_FAIR_DT_SIZE" - handler = "stringToSygusFairMode" - includes = ["options/datatypes_modes.h"] + type = "SygusFairMode" + default = "DT_SIZE" read_only = true help = "if and how to apply fairness for sygus" + help_mode = "Modes for enforcing fairness for counterexample guided quantifier instantion." +[[option.mode.DIRECT]] + name = "direct" + help = "Enforce fairness using direct conflict lemmas." +[[option.mode.DT_SIZE]] + name = "dt-size" + help = "Enforce fairness using size operator." +[[option.mode.DT_HEIGHT_PRED]] + name = "dt-height-bound" + help = "Enforce fairness by height bound predicate." +[[option.mode.DT_SIZE_PRED]] + name = "dt-size-bound" + help = "Enforce fairness by size bound predicate." +[[option.mode.NONE]] + name = "none" + help = "Do not enforce fairness." [[option]] name = "sygusFairMax" diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp deleted file mode 100644 index f2c37f52a..000000000 --- a/src/options/decision_mode.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file decision_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/decision_mode.h" - -#include <iostream> - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) { - switch(mode) { - case decision::DECISION_STRATEGY_INTERNAL: - out << "DECISION_STRATEGY_INTERNAL"; - break; - case decision::DECISION_STRATEGY_JUSTIFICATION: - out << "DECISION_STRATEGY_JUSTIFICATION"; - break; - default: - out << "DecisionMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h deleted file mode 100644 index c90e0a6f0..000000000 --- a/src/options/decision_mode.h +++ /dev/null @@ -1,64 +0,0 @@ -/********************* */ -/*! \file decision_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__SMT__DECISION_MODE_H -#define CVC4__SMT__DECISION_MODE_H - -#include <iosfwd> - -namespace CVC4 { -namespace decision { - -/** Enumeration of decision strategies */ -enum DecisionMode { - - /** - * Decision engine doesn't do anything. Use sat solver's internal - * heuristics - */ - DECISION_STRATEGY_INTERNAL, - - /** - * Use the justification heuristic - */ - DECISION_STRATEGY_JUSTIFICATION, - - /** - * Use may-relevancy. - */ - DECISION_STRATEGY_RELEVANCY - -};/* enum DecisionMode */ - - -/** Enumeration of combining functions for computing internal weights */ -enum DecisionWeightInternal { - DECISION_WEIGHT_INTERNAL_OFF, - DECISION_WEIGHT_INTERNAL_MAX, - DECISION_WEIGHT_INTERNAL_SUM, - DECISION_WEIGHT_INTERNAL_USR1 -};/* enum DecisionInternalWeight */ - -}/* CVC4::decision namespace */ - -std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode); - -}/* CVC4 namespace */ - -#endif /* CVC4__SMT__DECISION_MODE_H */ diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 5826368c8..c614ab3db 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -7,11 +7,20 @@ header = "options/decision_options.h" smt_name = "decision-mode" category = "regular" long = "decision=MODE" - type = "decision::DecisionMode" - default = "decision::DECISION_STRATEGY_INTERNAL" - handler = "stringToDecisionMode" - includes = ["options/decision_mode.h"] + type = "DecisionMode" + default = "INTERNAL" + predicates = ["setDecisionModeStopOnly"] help = "choose decision mode, see --decision=help" + help_mode = "Decision modes." +[[option.mode.INTERNAL]] + name = "internal" + help = "Use the internal decision heuristics of the SAT solver." +[[option.mode.JUSTIFICATION]] + name = "justification" + help = "An ATGP-inspired justification heuristic." +[[option.mode.RELEVANCY]] + name = "justification-stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." [[option]] name = "decisionStopOnly" @@ -37,6 +46,7 @@ header = "options/decision_options.h" read_only = true help = "use the weight nodes (locally, by looking at children) to direct recursive search" + [[option]] name = "decisionRandomWeight" category = "expert" @@ -50,8 +60,16 @@ header = "options/decision_options.h" name = "decisionWeightInternal" category = "expert" long = "decision-weight-internal=HOW" - type = "decision::DecisionWeightInternal" - default = "decision::DECISION_WEIGHT_INTERNAL_OFF" - handler = "stringToDecisionWeightInternal" + type = "DecisionWeightInternal" + default = "OFF" read_only = true - help = "computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)" + help = "compute weights of internal nodes using children: off, max, sum, usr1" + help_mode = "Decision weight internal mode." +[[option.mode.OFF]] + name = "off" +[[option.mode.MAX]] + name = "max" +[[option.mode.SUM]] + name = "sum" +[[option.mode.USR1]] + name = "usr1" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 8f801466c..0dab2ed76 100755 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -46,16 +46,18 @@ import os import re import sys import textwrap +import toml ### Allowed attributes for module/option/alias MODULE_ATTR_REQ = ['id', 'name', 'header'] -MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['options', 'aliases'] +MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option', 'alias'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ - 'name', 'help', 'smt_name', 'short', 'long', 'default', 'includes', - 'handler', 'predicates', 'notifies', 'links', 'read_only', 'alternate' + 'name', 'help', 'help_mode', 'smt_name', 'short', 'long', 'default', + 'includes', 'handler', 'predicates', 'notifies', 'links', 'read_only', + 'alternate', 'mode' ] ALIAS_ATTR_REQ = ['category', 'long', 'links'] @@ -226,6 +228,64 @@ TPL_IMPL_OPTION_WAS_SET_BY_USER = \ return Options::current()->wasSetByUser(*this); }}""" +# Mode templates +TPL_DECL_MODE_ENUM = \ +""" +enum class {type} +{{ + {values} +}};""" + +TPL_DECL_MODE_FUNC = \ +""" +std::ostream& +operator<<(std::ostream& out, {type} mode) CVC4_PUBLIC;""" + +TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(" CVC4_PUBLIC;")] + \ +""" +{{ + out << "{type}::"; + switch(mode) {{{cases} + default: + Unreachable(); + }} + return out; +}} +""" + +TPL_IMPL_MODE_CASE = \ +""" + case {type}::{enum}: + out << "{enum}"; + break;""" + +TPL_DECL_MODE_HANDLER = \ +""" +{type} +stringTo{type}(const std::string& option, const std::string& optarg);""" + +TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \ +""" +{{ + {cases} + else if (optarg == "help") + {{ + puts({help}); + exit(1); + }} + else + {{ + throw OptionException(std::string("unknown option for --{long}: `") + + optarg + "'. Try --{long}=help."); + }} +}} +""" + +TPL_MODE_HANDLER_CASE = \ +"""if (optarg == "{name}") + {{ + return {type}::{enum}; + }}""" class Module(object): @@ -258,7 +318,6 @@ class Option(object): self.links = [] self.read_only = False self.alternate = True # add --no- alternative long option for bool - self.lineno = None self.filename = None for (attr, val) in d.items(): assert attr in self.__dict__ @@ -275,7 +334,6 @@ class Alias(object): def __init__(self, d): self.__dict__ = dict((k, None) for k in ALIAS_ATTR_ALL) self.links = [] - self.lineno = None self.filename = None self.alternate_for = None # replaces a --no- alternative for an option for (attr, val) in d.items(): @@ -288,8 +346,19 @@ def die(msg): sys.exit('[error] {}'.format(msg)) -def perr(filename, lineno, msg): - die('parse error in {}:{}: {}'.format(filename, lineno + 1, msg)) +def perr(filename, msg, option_or_alias = None): + msg_suffix = '' + if option_or_alias: + if isinstance(option_or_alias, Option): + msg_suffix = 'option ' + if option_or_alias.name: + msg_suffix = "{} '{}' ".format(msg_suffix, option_or_alias.name) + else: + msg_suffix = "{} '{}' ".format(msg_suffix, option_or_alias.long) + else: + assert isinstance(option_or_alias, Alias) + msg_suffix = "alias '{}' ".format(option_or_alias.long) + die('parse error in {}: {}{}'.format(filename, msg, msg_suffix)) def write_file(directory, name, content): @@ -437,6 +506,29 @@ def help_format(help_msg, opts): lines.extend([' ' * width_opt + l for l in text[1:]]) return ['"{}\\n"'.format(x) for x in lines] +def help_mode_format(option): + """ + Format help message for mode options. + """ + assert option.help_mode + assert option.mode + + wrapper = textwrap.TextWrapper(width=78, break_on_hyphens=False) + text = ['{}'.format(x) for x in wrapper.wrap(option.help_mode)] + text.append('Available modes for --{} are:'.format(option.long.split('=')[0])) + + for value, attrib in option.mode.items(): + assert len(attrib) == 1 + attrib = attrib[0] + if value == option.default and attrib['name'] != "default": + text.append('+ {} (default)'.format(attrib['name'])) + else: + text.append('+ {}'.format(attrib['name'])) + if 'help' in attrib: + text.extend(' {}'.format(x) for x in wrapper.wrap(attrib['help'])) + + return '\n '.join('"{}\\n"'.format(x) for x in text) + def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): """ @@ -450,6 +542,8 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): decls = [] specs = [] inls = [] + mode_decl = [] + mode_impl = [] # *_options_.cpp accs = [] @@ -512,6 +606,38 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Global definitions defs.append('struct {name}__option_t {name};'.format(name=option.name)) + if option.mode: + values = option.mode.keys() + mode_decl.append( + TPL_DECL_MODE_ENUM.format( + type=option.type, + values=',\n '.join(values))) + mode_decl.append(TPL_DECL_MODE_FUNC.format(type=option.type)) + cases = [TPL_IMPL_MODE_CASE.format( + type=option.type, enum=x) for x in values] + mode_impl.append( + TPL_IMPL_MODE_FUNC.format( + type=option.type, + cases=''.join(cases))) + + # Generate str-to-enum handler + cases = [] + for value, attrib in option.mode.items(): + assert len(attrib) == 1 + cases.append( + TPL_MODE_HANDLER_CASE.format( + name=attrib[0]['name'], + type=option.type, + enum=value)) + assert option.long + assert cases + mode_decl.append(TPL_DECL_MODE_HANDLER.format(type=option.type)) + mode_impl.append( + TPL_IMPL_MODE_HANDLER.format( + type=option.type, + cases='\n else '.join(cases), + help=help_mode_format(option), + long=option.long.split('=')[0])) filename = os.path.splitext(os.path.split(module.header)[1])[0] write_file(dst_dir, '{}.h'.format(filename), tpl_module_h.format( @@ -522,14 +648,14 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): holder_spec=' \\\n'.join(holder_specs), decls='\n'.join(decls), specs='\n'.join(specs), - inls='\n'.join(inls) - )) + inls='\n'.join(inls), + modes=''.join(mode_decl))) write_file(dst_dir, '{}.cpp'.format(filename), tpl_module_cpp.format( filename=filename, accs='\n'.join(accs), - defs='\n'.join(defs) - )) + defs='\n'.join(defs), + modes=''.join(mode_impl))) def docgen(category, name, smt_name, short_name, long_name, ctype, default, @@ -676,7 +802,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, '.TP\n.I "{} OPTIONS"'.format(module.name.upper())) man_others_int.append(man_others_smt[-1]) - for option in \ sorted(module.options, key=lambda x: x.long if x.long else x.name): assert option.type != 'void' or option.name is None @@ -696,6 +821,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, else: handler = \ 'handler->{}(option, optionarg)'.format(option.handler) + elif option.mode: + handler = 'stringTo{}(option, optionarg)'.format(option.type) elif option.type != 'bool': handler = \ 'handleOption<{}>(option, optionarg)'.format(option.type) @@ -907,6 +1034,9 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, # Default option values default = option.default if option.default else '' + # Prepend enum name + if option.mode and option.type not in default: + default = '{}::{}'.format(option.type, default) defaults.append('{}({})'.format(option.name, default)) defaults.append('{}__setByUser__(false)'.format(option.name)) @@ -1005,7 +1135,7 @@ def rstrip(suffix, s): return s[:-len(suffix)] if s.endswith(suffix) else s -def check_attribs(filename, lineno, req_attribs, valid_attribs, attribs, ctype): +def check_attribs(filename, req_attribs, valid_attribs, attribs, ctype): """ Check if for a given module/option/alias the defined attributes are valid and if all required attributes are defined. @@ -1013,30 +1143,32 @@ def check_attribs(filename, lineno, req_attribs, valid_attribs, attribs, ctype): msg_for = "" if 'name' in attribs: msg_for = " for '{}'".format(attribs['name']) + elif 'long' in attribs: + msg_for = " for '{}'".format(attribs['long']) for k in req_attribs: if k not in attribs: - perr(filename, lineno, + perr(filename, "required {} attribute '{}' not specified{}".format( ctype, k, msg_for)) for k in attribs: if k not in valid_attribs: - perr(filename, lineno, + perr(filename, "invalid {} attribute '{}' specified{}".format( ctype, k, msg_for)) -def check_unique(filename, lineno, value, cache): +def check_unique(filename, value, cache): """ Check if given name is unique in cache. """ if value in cache: - perr(filename, lineno, - "'{}' already defined in '{}' at line {}".format( - value, cache[value][0], cache[value][1])) - cache[value] = (filename, lineno + 1) + perr(filename, + "'{}' already defined in '{}'".format(value, cache[value])) + else: + cache[value] = filename -def check_long(filename, lineno, long_name, ctype=None): +def check_long(filename, option_or_alias, long_name, ctype=None): """ Check if given long option name is valid. """ @@ -1044,189 +1176,37 @@ def check_long(filename, lineno, long_name, ctype=None): if long_name is None: return if long_name.startswith('--'): - perr(filename, lineno, 'remove -- prefix from long option') + perr(filename, 'remove -- prefix from long', option_or_alias) r = r'^[0-9a-zA-Z\-=]+$' if not re.match(r, long_name): - perr(filename, lineno, - "long option '{}' does not match regex criteria '{}'".format( - long_name, r)) + perr(filename, + "long '{}' does not match regex criteria '{}'".format( + long_name, r), option_or_alias) name = long_get_option(long_name) - check_unique(filename, lineno, name, g_long_cache) + check_unique(filename, name, g_long_cache) if ctype == 'bool': - check_unique(filename, lineno, 'no-{}'.format(name), g_long_cache) - + check_unique(filename, 'no-{}'.format(name), g_long_cache) -def check_links(filename, lineno, links): +def check_links(filename, option_or_alias): """ Check if long options defined in links are valid and correctly used. """ global g_long_cache, g_long_arguments - for link in links: + for link in option_or_alias.links: long_name = lstrip('no-', lstrip('--', long_get_option(link))) if long_name not in g_long_cache: - perr(filename, lineno, - "invalid long option '{}' in links list".format(link)) + perr(filename, + "invalid long option '{}' in links list".format(link), + option_or_alias) # check if long option requires an argument if long_name in g_long_arguments and '=' not in link: - perr(filename, lineno, - "linked option '{}' requires an argument".format(link)) - - -def check_alias_attrib(filename, lineno, attrib, value): - """ - Check alias attribute values. All attribute checks that can be done while - parsing should be done here. - """ - if attrib not in ALIAS_ATTR_ALL: - perr(filename, lineno, "invalid alias attribute '{}'".format(attrib)) - if attrib == 'category': - if value not in CATEGORY_VALUES: - perr(filename, lineno, "invalid category value '{}'".format(value)) - elif attrib == 'long': - pass # Will be checked after parsing is done - elif attrib == 'links': - assert isinstance(value, list) - if not value: - perr(filename, lineno, 'links list must not be empty') - - -def check_option_attrib(filename, lineno, attrib, value): - """ - Check option attribute values. All attribute checks that can be done while - parsing should be done here. - """ - global g_smt_cache, g_name_cache, g_short_cache - - if attrib not in OPTION_ATTR_ALL: - perr(filename, lineno, "invalid option attribute '{}'".format(attrib)) - - if attrib == 'category': - if value not in CATEGORY_VALUES: - perr(filename, lineno, "invalid category value '{}'".format(value)) - elif attrib == 'type': - if not value: - perr(filename, lineno, 'type must not be empty') - elif attrib == 'long': - pass # Will be checked after parsing is done - elif attrib == 'name' and value: - r = r'^[a-zA-Z]+[0-9a-zA-Z_]*$' - if not re.match(r, value): - perr(filename, lineno, - "name '{}' does not match regex criteria '{}'".format( - value, r)) - check_unique(filename, lineno, value, g_name_cache) - elif attrib == 'smt_name' and value: - r = r'^[a-zA-Z]+[0-9a-zA-Z\-_]*$' - if not re.match(r, value): - perr(filename, lineno, - "smt_name '{}' does not match regex criteria '{}'".format( - value, r)) - check_unique(filename, lineno, value, g_smt_cache) - elif attrib == 'short' and value: - if value[0].startswith('-'): - perr(filename, lineno, 'remove - prefix from short option') - if len(value) != 1: - perr(filename, lineno, 'short option must be of length 1') - if not value.isalpha() and not value.isdigit(): - perr(filename, lineno, 'short option must be a character or a digit') - check_unique(filename, lineno, value, g_short_cache) - elif attrib == 'default': - pass - elif attrib == 'includes' and value: - if not isinstance(value, list): - perr(filename, lineno, 'expected list for includes attribute') - elif attrib == 'handler': - pass - elif attrib == 'predicates' and value: - if not isinstance(value, list): - perr(filename, lineno, 'expected list for predicates attribute') - elif attrib == 'notifies' and value: - if not isinstance(value, list): - perr(filename, lineno, 'expected list for notifies attribute') - elif attrib == 'links' and value: - if not isinstance(value, list): - perr(filename, lineno, 'expected list for links attribute') - elif attrib in ['read_only', 'alternate'] and value is not None: - if not isinstance(value, bool): - perr(filename, lineno, - "expected true/false instead of '{}' for {}".format( - value, attrib)) - - -def check_module_attrib(filename, lineno, attrib, value): - """ - Check module attribute values. All attribute checks that can be done while - parsing should be done here. - """ - global g_module_id_cache - if attrib not in MODULE_ATTR_ALL: - perr(filename, lineno, "invalid module attribute '{}'".format(attrib)) - if attrib == 'id': - if not value: - perr(filename, lineno, 'module id must not be empty') - if value in g_module_id_cache: - perr(filename, lineno, - "module id '{}' already defined in '{}' at line {}".format( - value, - g_module_id_cache[value][0], - g_module_id_cache[value][1])) - g_module_id_cache[value] = (filename, lineno) - r = r'^[A-Z]+[A-Z_]*$' - if not re.match(r, value): - perr(filename, lineno, - "module id '{}' does not match regex criteria '{}'".format( - value, r)) - elif attrib == 'name': - if not value: - perr(filename, lineno, 'module name must not be empty') - elif attrib == 'header': - if not value: - perr(filename, lineno, 'module header must not be empty') - header_name = \ - 'options/{}.h'.format(rstrip('.toml', os.path.basename(filename))) - if header_name != value: - perr(filename, lineno, - "expected module header '{}' instead of '{}'".format( - header_name, value)) - - -def parse_value(filename, lineno, attrib, val): - """ - Parse attribute values. - We only allow three types of values: - - bool (val either true/false or "true"/"false") - - string (val starting with ") - - lists (val starting with [) - """ - if val[0] == '"': - if val[-1] != '"': - perr(filename, lineno, 'missing closing " for string') - val = val.lstrip('"').rstrip('"').replace('\\"', '"') - - # for read_only/alternate we allow both true/false and "true"/"false" - if attrib in ['read_only', 'alternate']: - if val == 'true': - return True - elif val == 'false': - return False - return val if val else None - elif val[0] == '[': - try: - val_list = ast.literal_eval(val) - except SyntaxError as e: - perr(filename, lineno, 'parsing list: {}'.format(e.msg)) - return val_list - elif val == 'true': - return True - elif val == 'false': - return False - else: - perr(filename, lineno, "invalid value '{}'".format(val)) - return None + perr(filename, + "linked option '{}' requires an argument".format(link), + option_or_alias) -def parse_module(filename, file): +def parse_module(filename, module): """ Parse options module file. @@ -1235,122 +1215,51 @@ def parse_module(filename, file): toml format, we chose to implement our own parser to get better error messages. """ - module = dict() - options = [] - aliases = [] - lines = [[x.strip() for x in line.split('=', 1)] for line in file] - option = None - alias = None - option_lines = [] - alias_lines = [] - for i in range(len(lines)): - assert option is None or alias is None - line = lines[i] - # Skip comments - if line[0].startswith('#'): - continue - # Check if a new option/alias starts. - if len(line) == 1: - # Create a new option/alias object, save previously created - if line[0] in ['[[option]]', '[[alias]]']: - if option: - options.append(option) - option = None - if alias: - aliases.append(alias) - alias = None - # Create new option dict and save line number where option - # was defined. - if line[0] == '[[option]]': - assert alias is None - option = dict() - option_lines.append(i) - else: - # Create new alias dict and save line number where alias - # was defined. - assert line[0] == '[[alias]]' - assert option is None - alias = dict() - # Save line number where alias was defined - alias_lines.append(i) - elif line[0] != '': - perr(filename, i, "invalid attribute '{}'".format(line[0])) - # Parse module/option/alias attributes. - elif len(line) == 2: - attrib = line[0] - value = parse_value(filename, i, attrib, line[1]) - # All attributes we parse are part of the current option. - if option is not None: - check_option_attrib(filename, i, attrib, value) - if attrib in option: - perr(filename, i, - "duplicate option attribute '{}'".format(attrib)) - assert option is not None - option[attrib] = value - # All attributes we parse are part of the current alias. - elif alias is not None: - check_alias_attrib(filename, i, attrib, value) - if attrib in alias: - perr(filename, i, - "duplicate alias attribute '{}'".format(attrib)) - assert alias is not None - alias[attrib] = value - # All other attributes are part of the module. - else: - if attrib in module: - perr(filename, i, - "duplicate module attribute '{}'".format(attrib)) - check_module_attrib(filename, i, attrib, value) - module[attrib] = value - else: - perr(filename, i, "invalid attribute '{}'".format(line[0])) - - # Save previously parsed option/alias - if option: - options.append(option) - if alias: - aliases.append(alias) - # Check if parsed module attributes are valid and if all required # attributes are defined. - check_attribs(filename, 1, + check_attribs(filename, MODULE_ATTR_REQ, MODULE_ATTR_ALL, module, 'module') res = Module(module) - # Check parsed option/alias attributes and create option/alias objects and - # associate file name and line number with options/aliases (required for - # better error reporting). - assert len(option_lines) == len(options) - assert len(alias_lines) == len(aliases) - for i in range(len(options)): - attribs = options[i] - lineno = option_lines[i] - check_attribs(filename, lineno, - OPTION_ATTR_REQ, OPTION_ATTR_ALL, attribs, 'option') - option = Option(attribs) - if option.short and not option.long: - perr(filename, lineno, - "short option '{}' specified but no long option".format( - option.short)) - if option.type == 'bool' and option.handler: - perr(filename, lineno, - 'specifying handlers for options of type bool is not allowed') - if option.category != 'undocumented' and not option.help: - perr(filename, lineno, - 'help text is required for {} options'.format(option.category)) - option.lineno = lineno - option.filename = filename - res.options.append(option) - - for i in range(len(aliases)): - attribs = aliases[i] - lineno = alias_lines[i] - check_attribs(filename, lineno, - ALIAS_ATTR_REQ, ALIAS_ATTR_ALL, attribs, 'alias') - alias = Alias(attribs) - alias.lineno = lineno - alias.filename = filename - res.aliases.append(alias) + if 'option' in module: + for attribs in module['option']: + lineno = 0 + check_attribs(filename, + OPTION_ATTR_REQ, OPTION_ATTR_ALL, attribs, 'option') + option = Option(attribs) + if option.mode and not option.help_mode: + perr(filename, 'defines modes but no help_mode', option) + if option.mode and option.handler: + perr(filename, 'defines modes and a handler', option) + if option.mode and option.default and \ + option.default not in option.mode.keys(): + perr(filename, + "invalid default value '{}'".format(option.default), + option) + if option.short and not option.long: + perr(filename, + "short option '{}' specified but no long option".format( + option.short), + option) + if option.type == 'bool' and option.handler: + perr(filename, + 'defining handlers for bool options is not allowed', + option) + if option.category != 'undocumented' and not option.help: + perr(filename, + 'help text required for {} options'.format(option.category), + option) + option.filename = filename + res.options.append(option) + + if 'alias' in module: + for attribs in module['alias']: + lineno = 0 + check_attribs(filename, + ALIAS_ATTR_REQ, ALIAS_ATTR_ALL, attribs, 'alias') + alias = Alias(attribs) + alias.filename = filename + res.aliases.append(alias) return res @@ -1400,20 +1309,19 @@ def mkoptions_main(): # Parse files, check attributes and create module/option objects modules = [] for filename in filenames: - with open(filename, 'r') as file: - module = parse_module(filename, file) - # Check if long options are valid and unique. First populate - # g_long_cache with option.long and --no- alternatives if - # applicable. - for option in module.options: - check_long(option.filename, option.lineno, option.long, - option.type) - if option.long: - g_long_to_opt[long_get_option(option.long)] = option - # Add long option that requires an argument - if option.type not in ['bool', 'void']: - g_long_arguments.add(long_get_option(option.long)) - modules.append(module) + module = parse_module(filename, toml.load(filename)) + + # Check if long options are valid and unique. First populate + # g_long_cache with option.long and --no- alternatives if + # applicable. + for option in module.options: + check_long(filename, option, option.long, option.type) + if option.long: + g_long_to_opt[long_get_option(option.long)] = option + # Add long option that requires an argument + if option.type not in ['bool', 'void']: + g_long_arguments.add(long_get_option(option.long)) + modules.append(module) # Check if alias.long is unique and check if alias.long defines an alias # for an alternate (--no-<long>) option for existing option <long>. @@ -1428,7 +1336,7 @@ def mkoptions_main(): m[0].alternate = False alias.alternate_for = m[0] del g_long_cache[alias.long] - check_long(alias.filename, alias.lineno, alias.long) + check_long(alias.filename, alias, alias.long) # Add long option that requires an argument if '=' in alias.long: g_long_arguments.add(long_get_option(alias.long)) @@ -1437,9 +1345,9 @@ def mkoptions_main(): # long options are available). for module in modules: for option in module.options: - check_links(option.filename, option.lineno, option.links) + check_links(option.filename, option) for alias in module.aliases: - check_links(alias.filename, alias.lineno, alias.links) + check_links(alias.filename, alias) # Create *_options.{h,cpp} in destination directory for module in modules: diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index 46162845d..9ac94477c 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -16,6 +16,7 @@ **/ #include "options/options_holder.h" +#include "base/check.h" namespace CVC4 { @@ -26,6 +27,7 @@ namespace options { ${defs}$ +${modes}$ } // namespace options } // namespace CVC4 diff --git a/src/options/module_template.h b/src/options/module_template.h index 2ffe070d2..e3eb30fe1 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -32,8 +32,9 @@ namespace CVC4 { namespace options { -${decls}$ +${modes}$ +${decls}$ } // namespace options @@ -44,7 +45,6 @@ namespace options { ${inls}$ - } // namespace options } // namespace CVC4 diff --git a/src/options/options.h b/src/options/options.h index c321b3499..1493ceac9 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -195,7 +195,7 @@ public: // Get accessor functions. InputLanguage getInputLanguage() const; - InstFormatMode getInstFormatMode() const; + options::InstFormatMode getInstFormatMode() const; OutputLanguage getOutputLanguage() const; bool getUfHo() const; bool getCheckProofs() const; diff --git a/src/options/options.i b/src/options/options.i index 25eecaf2d..ba98c4fc4 100644 --- a/src/options/options.i +++ b/src/options/options.i @@ -2,9 +2,6 @@ #include "options/options.h" %} -%ignore CVC4::operator<<(std::ostream&, SimplificationMode); -%ignore CVC4::operator<<(std::ostream&, ArithPivotRule); - %apply char** STRING_ARRAY { char* argv[] } %include "options/options.h" %clear char* argv[]; 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"); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 2e372a00c..a395bb453 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -23,24 +23,14 @@ #include <string> #include "base/modal_exception.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" -#include "options/bool_to_bv_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/datatypes_modes.h" -#include "options/decision_mode.h" +#include "options/bv_options.h" +#include "options/decision_options.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" #include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/smt_modes.h" -#include "options/strings_modes.h" -#include "options/sygus_out_mode.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace options { @@ -70,117 +60,29 @@ public: options::less_equal(1.0)(option, value); } - // theory/arith/options_handlers.h - ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, - std::string optarg); - ArithPropagationMode stringToArithPropagationMode(std::string option, - std::string optarg); - ErrorSelectionRule stringToErrorSelectionRule(std::string option, - std::string optarg); - // theory/quantifiers/options_handlers.h - theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, - std::string optarg); - void checkInstWhenMode(std::string option, - theory::quantifiers::InstWhenMode mode); - theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode( - std::string option, std::string optarg); - void checkLiteralMatchMode(std::string option, - theory::quantifiers::LiteralMatchMode mode); - theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, - std::string optarg); - void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode); - theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, - std::string optarg); - theory::quantifiers::QcfMode stringToQcfMode(std::string option, - std::string optarg); - theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, - std::string optarg); - theory::quantifiers::TriggerSelMode stringToTriggerSelMode( - std::string option, std::string optarg); - theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode( - std::string option, std::string optarg); - theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode( - std::string option, std::string optarg); - theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, - std::string optarg); - theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode( - std::string option, std::string optarg); - theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode( - std::string option, std::string optarg); - theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( - std::string option, std::string optarg); - theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode( - std::string option, std::string optarg); - theory::quantifiers::CegisSampleMode stringToCegisSampleMode( - std::string option, std::string optarg); - theory::quantifiers::SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode( - std::string option, std::string optarg); - theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode( - std::string option, std::string optarg); - theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( - std::string option, std::string optarg); - theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( - std::string option, std::string optarg); - theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode( - std::string option, std::string optarg); - theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode( - std::string option, std::string optarg); - theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( - std::string option, std::string optarg); - theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode( - std::string option, std::string optarg); - theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, - std::string optarg); - theory::SygusFairMode stringToSygusFairMode(std::string option, - std::string optarg); + void checkInstWhenMode(std::string option, InstWhenMode mode); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value); void abcEnabledBuild(std::string option, std::string value); - void satSolverEnabledBuild(std::string option, bool value); - void satSolverEnabledBuild(std::string option, std::string optarg); - - theory::bv::BitblastMode stringToBitblastMode(std::string option, - std::string optarg); - theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, - std::string optarg); - preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option, - std::string optarg); - void setBitblastAig(std::string option, bool arg); - - theory::bv::SatSolverMode stringToSatSolver(std::string option, - std::string optarg); - theory::bv::BvProofFormat stringToBvProofFormat(std::string option, - std::string optarg); - theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option, - std::string optarg); + template<class T> void checkSatSolverEnabled(std::string option, T m); - theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( - std::string option, std::string optarg); - theory::strings::RegExpInterMode stringToRegExpInterMode(std::string option, - std::string optarg); + void checkBvSatSolver(std::string option, SatSolverMode m); + void checkBitblastMode(std::string option, BitblastMode m); - // theory/uf/options_handlers.h - theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); + void setBitblastAig(std::string option, bool arg); // theory/options_handlers.h - theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); void notifyUseTheoryList(std::string option); std::string handleUseTheoryList(std::string option, std::string optarg); - // printer/options_handlers.h - ModelFormatMode stringToModelFormatMode(std::string option, - std::string optarg); InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); // decision/options_handlers.h - decision::DecisionMode stringToDecisionMode(std::string option, - std::string optarg); - decision::DecisionWeightInternal stringToDecisionWeightInternal( - std::string option, std::string optarg); + void setDecisionModeStopOnly(std::string option, DecisionMode m); /** * Throws a ModalException if this option is being set after final @@ -188,13 +90,6 @@ public: */ void notifyBeforeSearch(const std::string& option); void notifyDumpMode(std::string option); - SimplificationMode stringToSimplificationMode(std::string option, - std::string optarg); - ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg); - BlockModelsMode stringToBlockModelsMode(std::string option, - std::string optarg); - SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option, - std::string optarg); void setProduceAssertions(std::string option, bool value); void proofEnabledBuild(std::string option, bool value); void LFSCEnabledBuild(std::string option, bool value); @@ -244,56 +139,20 @@ public: Options* d_options; /* Help strings */ - static const std::string s_bitblastingModeHelp; - static const std::string s_bvSatSolverHelp; - static const std::string s_bvProofFormatHelp; - static const std::string s_bvOptimizeSatProofHelp; - static const std::string s_booleanTermConversionModeHelp; - static const std::string s_bvSlicerModeHelp; - static const std::string s_stringsProcessLoopModeHelp; - static const std::string s_regExpInterModeHelp; - static const std::string s_boolToBVModeHelp; - static const std::string s_cegqiFairModeHelp; - static const std::string s_decisionModeHelp; - static const std::string s_instFormatHelp ; - static const std::string s_instWhenHelp; - static const std::string s_iteLiftQuantHelp; - static const std::string s_literalMatchHelp; - static const std::string s_macrosQuantHelp; - static const std::string s_quantDSplitHelp; - static const std::string s_quantRepHelp; - static const std::string s_mbqiModeHelp; - static const std::string s_modelFormatHelp; - static const std::string s_prenexQuantModeHelp; - static const std::string s_qcfModeHelp; - static const std::string s_qcfWhenModeHelp; - static const std::string s_simplificationHelp; - static const std::string s_modelCoresHelp; - static const std::string s_blockModelsHelp; - static const std::string s_sygusSolutionOutModeHelp; - static const std::string s_cbqiBvIneqModeHelp; - static const std::string s_cegqiSingleInvHelp; - static const std::string s_cegqiSingleInvRconsHelp; - static const std::string s_cegisSampleHelp; - static const std::string s_sygusQueryDumpFileHelp; - static const std::string s_sygusFilterSolHelp; - static const std::string s_sygusInvTemplHelp; - static const std::string s_sygusActiveGenHelp; - static const std::string s_sygusUnifPiHelp; - static const std::string s_sygusGrammarConsHelp; - static const std::string s_termDbModeHelp; - static const std::string s_theoryOfModeHelp; - static const std::string s_triggerSelModeHelp; - static const std::string s_triggerActiveSelModeHelp; - static const std::string s_ufssModeHelp; - static const std::string s_userPatModeHelp; - static const std::string s_fmfBoundMinModeModeHelp; - static const std::string s_errorSelectionRulesHelp; - static const std::string s_arithPropagationModeHelp; - static const std::string s_arithUnateLemmasHelp; + static const std::string s_instFormatHelp; }; /* class OptionHandler */ +template<class T> +void OptionsHandler::checkSatSolverEnabled(std::string option, T m) +{ +#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) + std::stringstream ss; + ss << "option `" << option + << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL"; + throw OptionException(ss.str()); +#endif +} }/* CVC4::options namespace */ }/* CVC4 namespace */ diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index d3906e24d..6548150aa 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -43,7 +43,8 @@ InputLanguage Options::getInputLanguage() const { return (*this)[options::inputLanguage]; } -InstFormatMode Options::getInstFormatMode() const { +options::InstFormatMode Options::getInstFormatMode() const +{ return (*this)[options::instFormatMode]; } diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp index b60dde467..db116dd05 100644 --- a/src/options/printer_modes.cpp +++ b/src/options/printer_modes.cpp @@ -19,33 +19,16 @@ namespace CVC4 { -std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) { - switch(mode) { - case MODEL_FORMAT_MODE_DEFAULT: - out << "MODEL_FORMAT_MODE_DEFAULT"; - break; - case MODEL_FORMAT_MODE_TABLE: - out << "MODEL_FORMAT_MODE_TABLE"; - break; - default: - out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, InstFormatMode mode) { - switch(mode) { - case INST_FORMAT_MODE_DEFAULT: - out << "INST_FORMAT_MODE_DEFAULT"; - break; - case INST_FORMAT_MODE_SZS: - out << "INST_FORMAT_MODE_SZS"; - break; - default: - out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]"; +std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode) +{ + out << "InstFormatMode::"; + switch (mode) + { + case options::InstFormatMode::DEFAULT: out << "DEFAULT"; break; + case options::InstFormatMode::SZS: out << "SZS"; break; + default: out << "UNKNOWN![" << unsigned(mode) << "]"; } return out; } -}/* CVC4 namespace */ +} // namespace CVC4 diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index 79c57828b..10f8a4eac 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -23,26 +23,23 @@ #include <iostream> namespace CVC4 { +namespace options { -/** Enumeration of model_format modes (how to print models from get-model command). */ -enum CVC4_PUBLIC ModelFormatMode { +/** Enumeration of inst_format modes (how to print models from get-model + * command). */ +enum class CVC4_PUBLIC InstFormatMode +{ /** default mode (print expressions in the output language format) */ - MODEL_FORMAT_MODE_DEFAULT, - /** print functional values in a table format */ - MODEL_FORMAT_MODE_TABLE, -}; - -/** Enumeration of inst_format modes (how to print models from get-model command). */ -enum CVC4_PUBLIC InstFormatMode { - /** default mode (print expressions in the output language format) */ - INST_FORMAT_MODE_DEFAULT, + DEFAULT, /** print as SZS proof */ - INST_FORMAT_MODE_SZS, + SZS, }; -std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC; +} // namespace options + +std::ostream& operator<<(std::ostream& out, + options::InstFormatMode mode) CVC4_PUBLIC; -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__PRINTER__MODEL_FORMAT_H */ diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index c1871259c..db2f3d6c9 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -7,20 +7,34 @@ header = "options/printer_options.h" category = "regular" long = "model-format=MODE" type = "ModelFormatMode" - default = "MODEL_FORMAT_MODE_DEFAULT" - handler = "stringToModelFormatMode" - includes = ["options/printer_modes.h"] + default = "DEFAULT" help = "print format mode for models, see --model-format=help" + help_mode = "Model format modes." +[[option.mode.DEFAULT]] + name = "default" + help = "Print model as expressions in the output language format." +[[option.mode.TABLE]] + name = "table" + help = "Print functional expressions over finite domains in a table format." [[option]] name = "instFormatMode" category = "regular" long = "inst-format=MODE" type = "InstFormatMode" - default = "INST_FORMAT_MODE_DEFAULT" + default = "InstFormatMode::DEFAULT" handler = "stringToInstFormatMode" includes = ["options/printer_modes.h"] help = "print format mode for instantiations, see --inst-format=help" +# InstFormatMode is currently exported as public so we can't auto genenerate +# the enum. +# help_mode = "Inst format modes." +#[[option.mode.DEFAULT]] +# name = "default" +# help = "Print instantiations as a list in the output language format." +#[[option.mode.SZS]] +# name = "szs" +# help = "Print instantiations as SZS compliant proof." [[option]] name = "flattenHOChains" diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp deleted file mode 100644 index a1d012aa5..000000000 --- a/src/options/quantifiers_modes.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \file quantifiers_modes.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ -#include "options/quantifiers_modes.h" - -#include <iostream> - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) { - switch(mode) { - case theory::quantifiers::INST_WHEN_PRE_FULL: - out << "INST_WHEN_PRE_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL: - out << "INST_WHEN_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: - out << "INST_WHEN_FULL_LAST_CALL"; - break; - case theory::quantifiers::INST_WHEN_LAST_CALL: - out << "INST_WHEN_LAST_CALL"; - break; - default: - out << "InstWhenMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { - switch(mode) { - case theory::quantifiers::LITERAL_MATCH_NONE: - out << "LITERAL_MATCH_NONE"; - break; - case theory::quantifiers::LITERAL_MATCH_USE: - out << "LITERAL_MATCH_USE"; - break; - case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE: - out << "LITERAL_MATCH_AGG_PREDICATE"; - break; - case theory::quantifiers::LITERAL_MATCH_AGG: - out << "LITERAL_MATCH_AGG"; - break; - default: - out << "LiteralMatchMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { - switch(mode) { - case theory::quantifiers::MBQI_NONE: - out << "MBQI_NONE"; - break; - case theory::quantifiers::MBQI_FMC: - out << "MBQI_FMC"; - break; - case theory::quantifiers::MBQI_TRUST: - out << "MBQI_TRUST"; - break; - default: - out << "MbqiMode!UNKNOWN"; - } - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h deleted file mode 100644 index 1a256b0bc..000000000 --- a/src/options/quantifiers_modes.h +++ /dev/null @@ -1,370 +0,0 @@ -/********************* */ -/*! \file quantifiers_modes.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__BASE__QUANTIFIERS_MODES_H -#define CVC4__BASE__QUANTIFIERS_MODES_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -enum InstWhenMode { - /** Apply instantiation round before full effort (possibly at standard effort) */ - INST_WHEN_PRE_FULL, - /** Apply instantiation round at full effort or above */ - INST_WHEN_FULL, - /** Apply instantiation round at full effort, after all other theories finish, or above */ - INST_WHEN_FULL_DELAY, - /** Apply instantiation round at full effort half the time, and last call always */ - INST_WHEN_FULL_LAST_CALL, - /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ - INST_WHEN_FULL_DELAY_LAST_CALL, - /** Apply instantiation round at last call only */ - INST_WHEN_LAST_CALL, -}; - -enum LiteralMatchMode { - /** Do not consider polarity of patterns */ - LITERAL_MATCH_NONE, - /** Conservatively consider polarity of patterns */ - LITERAL_MATCH_USE, - /** Aggressively consider polarity of Boolean predicates */ - LITERAL_MATCH_AGG_PREDICATE, - /** Aggressively consider polarity of all terms */ - LITERAL_MATCH_AGG, -}; - -enum MbqiMode { - /** no mbqi */ - MBQI_NONE, - /** default, mbqi from Section 5.4.2 of AJR thesis */ - MBQI_FMC, - /** mbqi trust (produce no instantiations) */ - MBQI_TRUST, -}; - -enum QcfWhenMode { - /** default, apply at full effort */ - QCF_WHEN_MODE_DEFAULT, - /** apply at last call */ - QCF_WHEN_MODE_LAST_CALL, - /** apply at standard effort */ - QCF_WHEN_MODE_STD, - /** apply based on heuristics */ - QCF_WHEN_MODE_STD_H, -}; - -enum QcfMode { - /** default, use qcf for conflicts only */ - QCF_CONFLICT_ONLY, - /** use qcf for conflicts and propagations */ - QCF_PROP_EQ, - /** use qcf for conflicts, propagations and heuristic instantiations */ - QCF_PARTIAL, -}; - -/** User pattern mode. -* -* These modes determine how user provided patterns (triggers) are -* used during E-matching. The modes vary on when instantiation based on -* user-provided triggers is combined with instantiation based on -* automatically selected triggers. -*/ -enum UserPatMode -{ - /** First instantiate based on user-provided triggers. If no instantiations - * are produced, use automatically selected triggers. - */ - USER_PAT_MODE_USE, - /** Default, if triggers are supplied for a quantifier, use only those. */ - USER_PAT_MODE_TRUST, - /** Resort to user triggers only when no instantiations are - * produced by automatically selected triggers - */ - USER_PAT_MODE_RESORT, - /** Ignore user patterns. */ - USER_PAT_MODE_IGNORE, - /** Interleave use/resort modes for quantified formulas with user patterns. */ - USER_PAT_MODE_INTERLEAVE, -}; - -/** Trigger selection mode. -* -* These modes are used for determining which terms to select -* as triggers for quantified formulas, when necessary, during E-matching. -* In the following, note the following terminology. A trigger is a set of terms, -* where a single trigger is a singleton set and a multi-trigger is a set of more -* than one term. -* -* TRIGGER_SEL_MIN selects single triggers of minimal term size. -* TRIGGER_SEL_MAX selects single triggers of maximal term size. -* -* For example, consider the quantified formula : -* forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y ) -* -* TRIGGER_SEL_MIN will select g( x, y ) and Q( f( x ), y ). -* TRIGGER_SEL_MAX will select P( f( g( x ) ) ) and Q( f( x ), y ). -* -* The remaining three trigger selections make a difference for multi-triggers -* only. For quantified formulas that require multi-triggers, we build a set of -* partial triggers that don't contain all variables, call this set S. Then, -* multi-triggers are built by taking a random subset of S that collectively -* contains all variables. -* -* Consider the quantified formula : -* forall xyz. P( h( x ), y ) V Q( y, z ) -* -* For TRIGGER_SEL_ALL and TRIGGER_SEL_MIN_SINGLE_ALL, -* S = { h( x ), P( h( x ), y ), Q( y, z ) }. -* For TRIGGER_SEL_MIN_SINGLE_MAX, -* S = { P( h( x ), y ), Q( y, z ) }. -* -* Furthermore, TRIGGER_SEL_MIN_SINGLE_ALL and TRIGGER_SEL_MIN_SINGLE_MAX, when -* selecting single triggers, only select terms of minimal size. -*/ -enum TriggerSelMode { - /** only consider minimal terms for triggers */ - TRIGGER_SEL_MIN, - /** only consider maximal terms for triggers */ - TRIGGER_SEL_MAX, - /** consider minimal terms for single triggers, maximal for non-single */ - TRIGGER_SEL_MIN_SINGLE_MAX, - /** consider minimal terms for single triggers, all for non-single */ - TRIGGER_SEL_MIN_SINGLE_ALL, - /** consider all terms for triggers */ - TRIGGER_SEL_ALL, -}; - -enum TriggerActiveSelMode { - /** always use all triggers */ - TRIGGER_ACTIVE_SEL_ALL, - /** only use triggers with minimal # of ground terms */ - TRIGGER_ACTIVE_SEL_MIN, - /** only use triggers with maximal # of ground terms */ - TRIGGER_ACTIVE_SEL_MAX, -}; - -enum CVC4_PUBLIC PrenexQuantMode { - /** do not prenex */ - PRENEX_QUANT_NONE, - /** prenex same sign quantifiers */ - PRENEX_QUANT_SIMPLE, - /** aggressive prenex, disjunctive prenex normal form */ - PRENEX_QUANT_DISJ_NORMAL, - /** prenex normal form */ - PRENEX_QUANT_NORMAL, -}; - -enum TermDbMode { - /** consider all terms in master equality engine */ - TERM_DB_ALL, - /** consider only relevant terms */ - TERM_DB_RELEVANT, -}; - -enum IteLiftQuantMode { - /** do not lift ITEs in quantified formulas */ - ITE_LIFT_QUANT_MODE_NONE, - /** only lift ITEs in quantified formulas if reduces the term size */ - ITE_LIFT_QUANT_MODE_SIMPLE, - /** lift ITEs */ - ITE_LIFT_QUANT_MODE_ALL, -}; - -enum CbqiBvIneqMode -{ - /** solve for inequalities using slack values in model */ - CBQI_BV_INEQ_EQ_SLACK, - /** solve for inequalities using boundary points */ - CBQI_BV_INEQ_EQ_BOUNDARY, - /** solve for inequalities directly, using side conditions */ - CBQI_BV_INEQ_KEEP, -}; - -enum CegqiSingleInvMode { - /** do not use single invocation techniques */ - CEGQI_SI_MODE_NONE, - /** use single invocation techniques */ - CEGQI_SI_MODE_USE, - /** always use single invocation techniques */ - CEGQI_SI_MODE_ALL, -}; - -/** Solution reconstruction modes for single invocation conjectures - * - * These modes indicate the policy when CVC4 solves a synthesis conjecture using - * single invocation techniques for a sygus problem with a user-specified - * grammar. - */ -enum CegqiSingleInvRconsMode -{ - /** - * Do not try to reconstruct solutions to single invocation conjectures. With - * this mode, solutions produced by CVC4 may violate grammar restrictions. - */ - CEGQI_SI_RCONS_MODE_NONE, - /** - * Try to reconstruct solution to single invocation conjectures in an - * incomplete (fail fast) way. - */ - CEGQI_SI_RCONS_MODE_TRY, - /** - * Reconstruct solutions to single invocation conjectures, but fail if we - * reach an upper limit on number of iterations in the enumeration - */ - CEGQI_SI_RCONS_MODE_ALL_LIMIT, - /** - * Reconstruct solutions to single invocation conjectures. This method - * relies on an expensive enumeration technique which only terminates when - * we succesfully reconstruct the solution, although it may not terminate. - */ - CEGQI_SI_RCONS_MODE_ALL, -}; - -enum CegisSampleMode -{ - /** do not use samples for CEGIS */ - CEGIS_SAMPLE_NONE, - /** use samples for CEGIS */ - CEGIS_SAMPLE_USE, - /** trust samples for CEGQI */ - CEGIS_SAMPLE_TRUST, -}; - -enum SygusInvTemplMode { - /** synthesize I( x ) */ - SYGUS_INV_TEMPL_MODE_NONE, - /** synthesize ( pre( x ) V I( x ) ) */ - SYGUS_INV_TEMPL_MODE_PRE, - /** synthesize ( post( x ) ^ I( x ) ) */ - SYGUS_INV_TEMPL_MODE_POST, -}; - -enum SygusActiveGenMode -{ - /** do not use actively-generated enumerators */ - SYGUS_ACTIVE_GEN_NONE, - /** use basic enumeration for actively-generated enumerators */ - SYGUS_ACTIVE_GEN_ENUM_BASIC, - /** use optimized enumeration actively-generated enumerators */ - SYGUS_ACTIVE_GEN_ENUM, - /** use variable-agnostic enumerators */ - SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, - /** internally decide the best policy for each enumerator */ - SYGUS_ACTIVE_GEN_AUTO, -}; - -enum SygusQueryDumpFilesMode -{ - /** do not dump query files */ - SYGUS_QUERY_DUMP_NONE, - /** dump all query files */ - SYGUS_QUERY_DUMP_ALL, - /** dump query files that were not solved by the subsolver */ - SYGUS_QUERY_DUMP_UNSOLVED, -}; - -enum SygusFilterSolMode -{ - /** do not filter solutions */ - SYGUS_FILTER_SOL_NONE, - /** filter logically stronger solutions */ - SYGUS_FILTER_SOL_STRONG, - /** filter logically weaker solutions */ - SYGUS_FILTER_SOL_WEAK, -}; - -enum SygusGrammarConsMode -{ - /** - * Use simple default SyGuS grammar construction (no symbolic terms or - * constants). - */ - SYGUS_GCONS_SIMPLE, - /** Use "any constant" constructors in default SyGuS grammar construction. */ - SYGUS_GCONS_ANY_CONST, - /** - * When applicable, use constructors that encode any term using "any constant" - * constructors. This construction uses sum-of-monomials for arithmetic - * grammars. - */ - SYGUS_GCONS_ANY_TERM, - /** - * When applicable, use constructors that encode any term using "any constant" - * constructors in a way that prefers conciseness over generality. This - * construction uses polynomials for arithmetic grammars. - */ - SYGUS_GCONS_ANY_TERM_CONCISE, -}; - -enum MacrosQuantMode { - /** infer all definitions */ - MACROS_QUANT_MODE_ALL, - /** infer ground definitions */ - MACROS_QUANT_MODE_GROUND, - /** infer ground uf definitions */ - MACROS_QUANT_MODE_GROUND_UF, -}; - -enum QuantDSplitMode { - /** never do quantifiers splitting */ - QUANT_DSPLIT_MODE_NONE, - /** default */ - QUANT_DSPLIT_MODE_DEFAULT, - /** do quantifiers splitting aggressively */ - QUANT_DSPLIT_MODE_AGG, -}; - -enum QuantRepMode { - /** let equality engine choose representatives */ - QUANT_REP_MODE_EE, - /** default, choose representatives that appear first */ - QUANT_REP_MODE_FIRST, - /** choose representatives that have minimal depth */ - QUANT_REP_MODE_DEPTH, -}; - -/** - * Modes for piecewise-independent unification for synthesis (see Barbosa et al - * FMCAD 2019). - */ -enum SygusUnifPiMode -{ - /** do not do piecewise-independent unification for synthesis */ - SYGUS_UNIF_PI_NONE, - /** use (finite-model) complete piecewise-independent unification */ - SYGUS_UNIF_PI_COMPLETE, - /** use approach based on condition enumeration for piecewise-independent - unification */ - SYGUS_UNIF_PI_CENUM, - /** use approach based on condition enumeration with information gain - heuristics for piecewise-independent unification */ - SYGUS_UNIF_PI_CENUM_IGAIN, -}; - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* CVC4__BASE__QUANTIFIERS_MODES_H */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d37c9db83..95ec636ca 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -36,11 +36,22 @@ header = "options/quantifiers_options.h" name = "prenexQuant" category = "regular" long = "prenex-quant=MODE" - type = "CVC4::theory::quantifiers::PrenexQuantMode" - default = "CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE" - handler = "stringToPrenexQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "PrenexQuantMode" + default = "SIMPLE" help = "prenex mode for quantified formulas" + help_mode = "Prenex quantifiers modes." +[[option.mode.NONE]] + name = "none" + help = "Do no prenex nested quantifiers." +[[option.mode.SIMPLE]] + name = "simple" + help = "Do simple prenexing of same sign quantifiers." +[[option.mode.DISJ_NORMAL]] + name = "dnorm" + help = "Prenex to disjunctive prenex normal form." +[[option.mode.NORMAL]] + name = "norm" + help = "Prenex to prenex normal form." [[option]] name = "prenexQuantUser" @@ -84,11 +95,19 @@ header = "options/quantifiers_options.h" name = "iteLiftQuant" category = "regular" long = "ite-lift-quant=MODE" - type = "CVC4::theory::quantifiers::IteLiftQuantMode" - default = "CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE" - handler = "stringToIteLiftQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "IteLiftQuantMode" + default = "SIMPLE" help = "ite lifting mode for quantified formulas" + help_mode = "ITE lifting modes for quantified formulas." +[[option.mode.NONE]] + name = "none" + help = "Do not lift if-then-else in quantified formulas." +[[option.mode.SIMPLE]] + name = "simple" + help = "Lift if-then-else in quantified formulas if results in smaller term size." +[[option.mode.ALL]] + name = "all" + help = "Lift if-then-else in quantified formulas." [[option]] name = "condVarSplitQuant" @@ -200,11 +219,16 @@ header = "options/quantifiers_options.h" name = "termDbMode" category = "regular" long = "term-db-mode=MODE" - type = "CVC4::theory::quantifiers::TermDbMode" - default = "CVC4::theory::quantifiers::TERM_DB_ALL" - handler = "stringToTermDbMode" - includes = ["options/quantifiers_modes.h"] + type = "TermDbMode" + default = "ALL" help = "which ground terms to consider for instantiation" + help_mode = "Modes for terms included in the quantifiers term database." +[[option.mode.ALL]] + name = "all" + help = "Quantifiers module considers all ground terms." +[[option.mode.RELEVANT]] + name = "relevant" + help = "Quantifiers module considers only ground terms connected to current assertions." [[option]] name = "registerQuantBodyTerms" @@ -310,35 +334,105 @@ header = "options/quantifiers_options.h" read_only = true help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms" +# Trigger selection mode. +# +# These modes are used for determining which terms to select +# as triggers for quantified formulas, when necessary, during E-matching. +# In the following, note the following terminology. A trigger is a set of terms, +# where a single trigger is a singleton set and a multi-trigger is a set of more +# than one term. +# +# MIN selects single triggers of minimal term size. +# MAX selects single triggers of maximal term size. +# +# For example, consider the quantified formula : +# forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y ) +# +# MIN will select g( x, y ) and Q( f( x ), y ). +# MAX will select P( f( g( x ) ) ) and Q( f( x ), y ). +# +# The remaining three trigger selections make a difference for multi-triggers +# only. For quantified formulas that require multi-triggers, we build a set of +# partial triggers that don't contain all variables, call this set S. Then, +# multi-triggers are built by taking a random subset of S that collectively +# contains all variables. +# +# Consider the quantified formula : +# forall xyz. P( h( x ), y ) V Q( y, z ) +# +# For ALL and MIN_SINGLE_ALL, +# S = { h( x ), P( h( x ), y ), Q( y, z ) }. +# For MIN_SINGLE_MAX, +# S = { P( h( x ), y ), Q( y, z ) }. +# +# Furthermore, MIN_SINGLE_ALL and MIN_SINGLE_MAX, when +# selecting single triggers, only select terms of minimal size. +# [[option]] name = "triggerSelMode" category = "regular" long = "trigger-sel=MODE" - type = "CVC4::theory::quantifiers::TriggerSelMode" - default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN" - handler = "stringToTriggerSelMode" - includes = ["options/quantifiers_modes.h"] + type = "TriggerSelMode" + default = "MIN" help = "selection mode for triggers" + help_mode = "Trigger selection modes." +[[option.mode.MIN]] + name = "min" + help = "Consider only minimal subterms that meet criteria for triggers." +[[option.mode.MAX]] + name = "max" + help = "Consider only maximal subterms that meet criteria for triggers." +[[option.mode.MIN_SINGLE_MAX]] + name = "min-s-max" + help = "Consider only minimal subterms that meet criteria for single triggers, maximal otherwise." +[[option.mode.MIN_SINGLE_ALL]] + name = "min-s-all" + help = "Consider only minimal subterms that meet criteria for single triggers, all otherwise." +[[option.mode.ALL]] + name = "all" + help = "Consider all subterms that meet criteria for triggers." [[option]] name = "triggerActiveSelMode" category = "regular" long = "trigger-active-sel=MODE" - type = "CVC4::theory::quantifiers::TriggerActiveSelMode" - default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL" - handler = "stringToTriggerActiveSelMode" - includes = ["options/quantifiers_modes.h"] + type = "TriggerActiveSelMode" + default = "ALL" help = "selection mode to activate triggers" + help_mode = "Trigger active selection modes." +[[option.mode.ALL]] + name = "all" + help = "Make all triggers active." +[[option.mode.MIN]] + name = "min" + help = "Activate triggers with minimal ground terms." +[[option.mode.MAX]] + name = "max" + help = "Activate triggers with maximal ground terms." [[option]] name = "userPatternsQuant" category = "regular" long = "user-pat=MODE" - type = "CVC4::theory::quantifiers::UserPatMode" - default = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST" - handler = "stringToUserPatMode" - includes = ["options/quantifiers_modes.h"] + type = "UserPatMode" + default = "TRUST" help = "policy for handling user-provided patterns for quantifier instantiation" + help_mode = "These modes determine how user provided patterns (triggers) are used during E-matching. The modes vary on when instantiation based on user-provided triggers is combined with instantiation based on automatically selected triggers." +[[option.mode.USE]] + name = "use" + help = "Use both user-provided and auto-generated patterns when patterns are provided for a quantified formula." +[[option.mode.TRUST]] + name = "trust" + help = "When provided, use only user-provided patterns for a quantified formula." +[[option.mode.RESORT]] + name = "resort" + help = "Use user-provided patterns only after auto-generated patterns saturate." +[[option.mode.IGNORE]] + name = "ignore" + help = "Ignore user-provided patterns." +[[option.mode.INTERLEAVE]] + name = "interleave" + help = "Alternate between use/resort." [[option]] name = "incrementTriggers" @@ -353,12 +447,29 @@ header = "options/quantifiers_options.h" name = "instWhenMode" category = "regular" long = "inst-when=MODE" - type = "CVC4::theory::quantifiers::InstWhenMode" - default = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL" - handler = "stringToInstWhenMode" + type = "InstWhenMode" + default = "FULL_LAST_CALL" predicates = ["checkInstWhenMode"] - includes = ["options/quantifiers_modes.h"] help = "when to apply instantiation" + help_mode = "Instantiation modes." +[[option.mode.PRE_FULL]] + name = "pre-full" + help = "Run instantiation round before full effort (possibly at standard effort)." +[[option.mode.FULL]] + name = "full" + help = "Run instantiation round at full effort, before theory combination." +[[option.mode.FULL_DELAY]] + name = "full-delay" + help = "Run instantiation round at full effort, before theory combination, after all other theories have finished." +[[option.mode.FULL_LAST_CALL]] + name = "full-last-call" + help = "Alternate running instantiation rounds at full effort and last call. In other words, interleave instantiation and theory combination." +[[option.mode.FULL_DELAY_LAST_CALL]] + name = "full-delay-last-call" + help = "Alternate running instantiation rounds at full effort after all other theories have finished, and last call." +[[option.mode.LAST_CALL]] + name = "last-call" + help = "Run instantiation at last call effort, after theory combination and and theories report sat." [[option]] name = "instWhenStrictInterleave" @@ -414,11 +525,19 @@ header = "options/quantifiers_options.h" name = "quantRepMode" category = "regular" long = "quant-rep-mode=MODE" - type = "CVC4::theory::quantifiers::QuantRepMode" - default = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST" - handler = "stringToQuantRepMode" - includes = ["options/quantifiers_modes.h"] + type = "QuantRepMode" + default = "FIRST" help = "selection mode for representatives in quantifiers engine" + help_mode = "Modes for quantifiers representative selection." +[[option.mode.EE]] + name = "ee" + help = "Let equality engine choose representatives." +[[option.mode.FIRST]] + name = "first" + help = "Choose terms that appear first." +[[option.mode.DEPTH]] + name = "depth" + help = "Choose terms that are of minimal depth." [[option]] name = "fullSaturateQuant" @@ -459,13 +578,23 @@ header = "options/quantifiers_options.h" name = "literalMatchMode" category = "regular" long = "literal-matching=MODE" - type = "CVC4::theory::quantifiers::LiteralMatchMode" - default = "CVC4::theory::quantifiers::LITERAL_MATCH_USE" - handler = "stringToLiteralMatchMode" - predicates = ["checkLiteralMatchMode"] - includes = ["options/quantifiers_modes.h"] + type = "LiteralMatchMode" + default = "USE" read_only = true help = "choose literal matching mode" + help_mode = "Literal match modes." +[[option.mode.NONE]] + name = "none" + help = "Do not use literal matching." +[[option.mode.USE]] + name = "use" + help = "Consider phase requirements of triggers conservatively. For example, the trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with terms in the equivalence class of true, and likewise Q( x ) will not be matched terms in the equivalence class of false. Extends to equality." +[[option.mode.AGG_PREDICATE]] + name = "agg-predicate" + help = "Consider phase requirements aggressively for predicates. In the above example, only match P( x ) with terms that are in the equivalence class of false." +[[option.mode.AGG]] + name = "agg" + help = "Consider the phase requirements aggressively for all triggers." ### Finite model finding options @@ -516,12 +645,19 @@ header = "options/quantifiers_options.h" name = "mbqiMode" category = "regular" long = "mbqi=MODE" - type = "CVC4::theory::quantifiers::MbqiMode" - default = "CVC4::theory::quantifiers::MBQI_FMC" - handler = "stringToMbqiMode" - predicates = ["checkMbqiMode"] - includes = ["options/quantifiers_modes.h"] + type = "MbqiMode" + default = "FMC" help = "choose mode for model-based quantifier instantiation" + help_mode = "Model-based quantifier instantiation modes." +[[option.mode.NONE]] + name = "none" + help = "Disable model-based quantifier instantiation." +[[option.mode.FMC]] + name = "fmc" + help = "Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability Modulo Theories." +[[option.mode.TRUST]] + name = "trust" + help = "Do not instantiate quantified formulas (incomplete technique)." [[option]] name = "fmfOneInstPerRound" @@ -638,23 +774,42 @@ header = "options/quantifiers_options.h" name = "qcfMode" category = "regular" long = "quant-cf-mode=MODE" - type = "CVC4::theory::quantifiers::QcfMode" - default = "CVC4::theory::quantifiers::QCF_PROP_EQ" - handler = "stringToQcfMode" - includes = ["options/quantifiers_modes.h"] + type = "QcfMode" + default = "PROP_EQ" read_only = true help = "what effort to apply conflict find mechanism" + help_mode = "Quantifier conflict find modes." +[[option.mode.CONFLICT_ONLY]] + name = "conflict" + help = "Apply QCF algorithm to find conflicts only." +[[option.mode.PROP_EQ]] + name = "prop-eq" + help = "Apply QCF algorithm to propagate equalities as well as conflicts." +[[option.mode.PARTIAL]] + name = "partial" + help = "Use QCF for conflicts, propagations and heuristic instantiations." [[option]] name = "qcfWhenMode" category = "regular" long = "quant-cf-when=MODE" - type = "CVC4::theory::quantifiers::QcfWhenMode" - default = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT" - handler = "stringToQcfWhenMode" - includes = ["options/quantifiers_modes.h"] + type = "QcfWhenMode" + default = "DEFAULT" read_only = true help = "when to invoke conflict find mechanism for quantifiers" + help_mode = "Quantifier conflict find modes." +[[option.mode.DEFAULT]] + name = "default" + help = "Default, apply conflict finding at full effort." +[[option.mode.LAST_CALL]] + name = "last-call" + help = "Apply conflict finding at last call, after theory combination and and all theories report sat." +[[option.mode.STD]] + name = "std" + help = "Apply conflict finding at standard effort." +[[option.mode.STD_H]] + name = "std-h" + help = "Apply conflict finding at standard effort when heuristic says to." [[option]] name = "qcfTConstraint" @@ -888,11 +1043,19 @@ header = "options/quantifiers_options.h" name = "cegqiSingleInvMode" category = "regular" long = "cegqi-si=MODE" - type = "CVC4::theory::quantifiers::CegqiSingleInvMode" - default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE" - handler = "stringToCegqiSingleInvMode" - includes = ["options/quantifiers_modes.h"] + type = "CegqiSingleInvMode" + default = "NONE" help = "mode for processing single invocation synthesis conjectures" + help_mode = "Modes for single invocation techniques." +[[option.mode.NONE]] + name = "none" + help = "Do not use single invocation techniques." +[[option.mode.USE]] + name = "use" + help = "Use single invocation techniques only if grammar is not restrictive." +[[option.mode.ALL]] + name = "all" + help = "Always use single invocation techniques." [[option]] name = "cegqiSingleInvPartial" @@ -903,15 +1066,32 @@ header = "options/quantifiers_options.h" read_only = true help = "combined techniques for synthesis conjectures that are partially single invocation" +# Solution reconstruction modes for single invocation conjectures +# +# These modes indicate the policy when CVC4 solves a synthesis conjecture using +# single invocation techniques for a sygus problem with a user-specified +# grammar. +# [[option]] name = "cegqiSingleInvReconstruct" category = "regular" long = "cegqi-si-rcons=MODE" - type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode" - default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT" - handler = "stringToCegqiSingleInvRconsMode" - includes = ["options/quantifiers_modes.h"] + type = "CegqiSingleInvRconsMode" + default = "ALL_LIMIT" help = "policy for reconstructing solutions for single invocation conjectures" + help_mode = "Modes for reconstruction solutions while using single invocation techniques." +[[option.mode.NONE]] + name = "none" + help = "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." +[[option.mode.TRY]] + name = "try" + help = "Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner." +[[option.mode.ALL_LIMIT]] + name = "all-limit" + help = "Try to reconstruct solutions in the original grammar, but termintate if a maximum number of rounds for reconstruction is exceeded." +[[option.mode.ALL]] + name = "all" + help = "Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed." [[option]] name = "cegqiSingleInvReconstructLimit" @@ -949,16 +1129,30 @@ header = "options/quantifiers_options.h" read_only = true help = "abort if constant repair techniques are not applicable" +# Modes for piecewise-independent unification for synthesis (see Barbosa et al +# FMCAD 2019). +# [[option]] name = "sygusUnifPi" category = "regular" long = "sygus-unif-pi=MODE" - type = "CVC4::theory::quantifiers::SygusUnifPiMode" - default = "CVC4::theory::quantifiers::SYGUS_UNIF_PI_NONE" - handler = "stringToSygusUnifPiMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusUnifPiMode" + default = "NONE" read_only = true help = "mode for synthesis via piecewise-indepedent unification" + help_mode = "Modes for piecewise-independent unification." +[[option.mode.NONE]] + name = "none" + help = "Do not use piecewise-independent unification." +[[option.mode.COMPLETE]] + name = "complete" + help = "Use complete approach for piecewise-independent unification (see Section 3 of Barbosa et al FMCAD 2019)" +[[option.mode.CENUM]] + name = "cond-enum" + help = "Use unconstrained condition enumeration for piecewise-independent unification (see Section 4 of Barbosa et al FMCAD 2019)." +[[option.mode.CENUM_IGAIN]] + name = "cond-enum-igain" + help = "Same as cond-enum, but additionally uses an information gain heuristic when doing decision tree learning." [[option]] name = "sygusUnifShuffleCond" @@ -1020,12 +1214,26 @@ header = "options/quantifiers_options.h" name = "sygusActiveGenMode" category = "regular" long = "sygus-active-gen=MODE" - type = "CVC4::theory::quantifiers::SygusActiveGenMode" - default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO" - handler = "stringToSygusActiveGenMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusActiveGenMode" + default = "AUTO" read_only = true help = "mode for actively-generated sygus enumerators" + help_mode = "Modes for actively-generated sygus enumerators." +[[option.mode.NONE]] + name = "none" + help = "Do not use actively-generated sygus enumerators." +[[option.mode.ENUM_BASIC]] + name = "basic" + help = "Use basic type enumerator for actively-generated sygus enumerators." +[[option.mode.ENUM]] + name = "enum" + help = "Use optimized enumerator for actively-generated sygus enumerators." +[[option.mode.VAR_AGNOSTIC]] + name = "var-agnostic" + help = "Use sygus solver to enumerate terms that are agnostic to variables." +[[option.mode.AUTO]] + name = "auto" + help = "Internally decide the best policy for each enumerator." [[option]] name = "sygusActiveGenEnumConsts" @@ -1075,21 +1283,40 @@ header = "options/quantifiers_options.h" name = "sygusGrammarConsMode" category = "regular" long = "sygus-grammar-cons=MODE" - type = "CVC4::theory::quantifiers::SygusGrammarConsMode" - default = "CVC4::theory::quantifiers::SYGUS_GCONS_SIMPLE" - handler = "stringToSygusGrammarConsMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusGrammarConsMode" + default = "SIMPLE" help = "mode for SyGuS grammar construction" + help_mode = "Modes for default SyGuS grammars." +[[option.mode.SIMPLE]] + name = "simple" + help = "Use simple grammar construction (no symbolic terms or constants)." +[[option.mode.ANY_CONST]] + name = "any-const" + help = "Use symoblic constant constructors." +[[option.mode.ANY_TERM]] + name = "any-term" + help = "When applicable, use constructors corresponding to any symbolic term. This option enables a sum-of-monomials grammar for arithmetic. For all other types, it enables symbolic constant constructors." +[[option.mode.ANY_TERM_CONCISE]] + name = "any-term-concise" + help = "When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to any-term but enables a polynomial grammar for arithmetic when not in a combined theory." [[option]] name = "sygusInvTemplMode" category = "regular" long = "sygus-inv-templ=MODE" - type = "CVC4::theory::quantifiers::SygusInvTemplMode" - default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" - handler = "stringToSygusInvTemplMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusInvTemplMode" + default = "POST" help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" + help_mode = "Template modes for sygus invariant synthesis." +[[option.mode.NONE]] + name = "none" + help = "Synthesize invariant directly." +[[option.mode.PRE]] + name = "pre" + help = "Synthesize invariant based on weakening of precondition." +[[option.mode.POST]] + name = "post" + help = "Synthesize invariant based on strengthening of postcondition." [[option]] name = "sygusInvTemplWhenSyntax" @@ -1188,11 +1415,19 @@ header = "options/quantifiers_options.h" name = "cegisSample" category = "regular" long = "cegis-sample=MODE" - type = "CVC4::theory::quantifiers::CegisSampleMode" - default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE" - handler = "stringToCegisSampleMode" - includes = ["options/quantifiers_modes.h"] + type = "CegisSampleMode" + default = "NONE" help = "mode for using samples in the counterexample-guided inductive synthesis loop" + help_mode = "Modes for sampling with counterexample-guided inductive synthesis (CEGIS)." +[[option.mode.NONE]] + name = "none" + help = "Do not use sampling with CEGIS." +[[option.mode.USE]] + name = "use" + help = "Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point." +[[option.mode.TRUST]] + name = "trust" + help = "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." [[option]] name = "minSynthSol" @@ -1409,21 +1644,37 @@ header = "options/quantifiers_options.h" name = "sygusQueryGenDumpFiles" category = "regular" long = "sygus-query-gen-dump-files=MODE" - type = "CVC4::theory::quantifiers::SygusQueryDumpFilesMode" - default = "CVC4::theory::quantifiers::SYGUS_QUERY_DUMP_NONE" - handler = "stringToSygusQueryDumpFilesMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusQueryDumpFilesMode" + default = "NONE" help = "mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen" + help_mode = "Query file options." +[[option.mode.NONE]] + name = "none" + help = "Do not dump query files when using --sygus-query-gen." +[[option.mode.ALL]] + name = "all" + help = "Dump all query files." +[[option.mode.UNSOLVED]] + name = "unsolved" + help = "Dump query files that the subsolver did not solve." [[option]] name = "sygusFilterSolMode" category = "regular" long = "sygus-filter-sol=MODE" - type = "CVC4::theory::quantifiers::SygusFilterSolMode" - default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" - handler = "stringToSygusFilterSolMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusFilterSolMode" + default = "NONE" help = "mode for filtering sygus solutions" + help_mode = "Modes for filtering sygus solutions." +[[option.mode.NONE]] + name = "none" + help = "Do not filter sygus solutions." +[[option.mode.STRONG]] + name = "strong" + help = "Filter solutions that are logically stronger than others." +[[option.mode.WEAK]] + name = "weak" + help = "Filter solutions that are logically weaker than others." [[option]] name = "sygusFilterSolRevSubsume" @@ -1627,11 +1878,19 @@ header = "options/quantifiers_options.h" name = "cbqiBvIneqMode" category = "regular" long = "cbqi-bv-ineq=MODE" - type = "CVC4::theory::quantifiers::CbqiBvIneqMode" - default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY" - handler = "stringToCbqiBvIneqMode" - includes = ["options/quantifiers_modes.h"] + type = "CbqiBvIneqMode" + default = "EQ_BOUNDARY" help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation" + help_mode = "Modes for handling bit-vector inequalities in counterexample-guided instantiation." +[[option.mode.EQ_SLACK]] + name = "eq-slack" + help = "Solve for the inequality using the slack value in the model, e.g., t > s becomes t = s + ( t-s )^M." +[[option.mode.EQ_BOUNDARY]] + name = "eq-boundary" + help = "Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1." +[[option.mode.KEEP]] + name = "keep" + help = "Solve for the inequality directly using side conditions for invertibility." [[option]] name = "cbqiBvRmExtract" @@ -1717,22 +1976,38 @@ header = "options/quantifiers_options.h" name = "macrosQuantMode" category = "regular" long = "macros-quant-mode=MODE" - type = "CVC4::theory::quantifiers::MacrosQuantMode" - default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF" - handler = "stringToMacrosQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "MacrosQuantMode" + default = "GROUND_UF" read_only = true help = "mode for quantifiers macro expansion" + help_mode = "Modes for quantifiers macro expansion." +[[option.mode.ALL]] + name = "all" + help = "Infer definitions for functions, including those containing quantified formulas." +[[option.mode.GROUND]] + name = "ground" + help = "Only infer ground definitions for functions." +[[option.mode.GROUND_UF]] + name = "ground-uf" + help = "Only infer ground definitions for functions that result in triggers for all free variables." [[option]] name = "quantDynamicSplit" category = "regular" long = "quant-dsplit-mode=MODE" - type = "CVC4::theory::quantifiers::QuantDSplitMode" - default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT" - handler = "stringToQuantDSplitMode" - includes = ["options/quantifiers_modes.h"] + type = "QuantDSplitMode" + default = "DEFAULT" help = "mode for dynamic quantifiers splitting" + help_mode = "Modes for quantifiers splitting." +[[option.mode.NONE]] + name = "none" + help = "Never split quantified formulas." +[[option.mode.DEFAULT]] + name = "default" + help = "Split quantified formulas over some finite datatypes when finite model finding is enabled." +[[option.mode.AGG]] + name = "agg" + help = "Aggressively split quantified formulas." [[option]] name = "quantAntiSkolem" diff --git a/src/options/smt_modes.cpp b/src/options/smt_modes.cpp deleted file mode 100644 index 3501da878..000000000 --- a/src/options/smt_modes.cpp +++ /dev/null @@ -1,36 +0,0 @@ -/********************* */ -/*! \file smt_modes.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/smt_modes.h" - -#include <iostream> - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) -{ - switch (mode) - { - case SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break; - case SIMPLIFICATION_MODE_NONE: out << "SIMPLIFICATION_MODE_NONE"; break; - default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -} // namespace CVC4 diff --git a/src/options/smt_modes.h b/src/options/smt_modes.h deleted file mode 100644 index d719dc243..000000000 --- a/src/options/smt_modes.h +++ /dev/null @@ -1,73 +0,0 @@ -/********************* */ -/*! \file smt_modes.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__SMT__MODES_H -#define CVC4__SMT__MODES_H - -#include <iosfwd> - -namespace CVC4 { - -/** Enumeration of simplification modes (when to simplify). */ -enum SimplificationMode -{ - /** Simplify the assertions all together once a check is requested */ - SIMPLIFICATION_MODE_BATCH, - /** Don't do simplification */ - SIMPLIFICATION_MODE_NONE -}; - -std::ostream& operator<<(std::ostream& out, - SimplificationMode mode) CVC4_PUBLIC; - -/** Enumeration of model core modes. */ -enum ModelCoresMode -{ - /** Do not compute model cores */ - MODEL_CORES_NONE, - /** - * Compute "simple" model cores that exclude variables that do not - * contribute to satisfying the input. - */ - MODEL_CORES_SIMPLE, - /** - * Compute model cores that also exclude variables whose variables are implied - * by others. - */ - MODEL_CORES_NON_IMPLIED -}; - -/** Block models modes. */ -enum BlockModelsMode -{ - /** Do not block models */ - BLOCK_MODELS_NONE, - /** - * block models based on literals truth values. - */ - BLOCK_MODELS_LITERALS, - /** - * block models based on concrete variable values in the model. - */ - BLOCK_MODELS_VALUES, -}; - -} // namespace CVC4 - -#endif /* CVC4__SMT__MODES_H */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 39d09c4ea..ba62a6455 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -36,10 +36,15 @@ header = "options/smt_options.h" category = "regular" long = "simplification=MODE" type = "SimplificationMode" - default = "SIMPLIFICATION_MODE_BATCH" - handler = "stringToSimplificationMode" - includes = ["options/smt_modes.h"] + default = "BATCH" help = "choose simplification mode, see --simplification=help" + help_mode = "Simplification modes." +[[option.mode.NONE]] + name = "none" + help = "Do not perform nonclausal simplification." +[[option.mode.BATCH]] + name = "batch" + help = "Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration)." [[alias]] category = "regular" @@ -101,21 +106,36 @@ header = "options/smt_options.h" category = "regular" long = "model-cores=MODE" type = "ModelCoresMode" - default = "MODEL_CORES_NONE" - handler = "stringToModelCoresMode" - includes = ["options/smt_modes.h"] + default = "NONE" help = "mode for producing model cores" - + help_mode = "Model cores modes." +[[option.mode.NONE]] + name = "none" + help = "Do not compute model cores." +[[option.mode.SIMPLE]] + name = "simple" + help = "Only include a subset of variables whose values are sufficient to show the input formula is satisfied by the given model." +[[option.mode.NON_IMPLIED]] + name = "non-implied" + help = "Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model." [[option]] name = "blockModelsMode" category = "regular" long = "block-models=MODE" type = "BlockModelsMode" - default = "BLOCK_MODELS_NONE" - handler = "stringToBlockModelsMode" - includes = ["options/smt_modes.h"] + default = "NONE" help = "mode for producing several models" + help_mode = "Blocking models modes." +[[option.mode.NONE]] + name = "none" + help = "Do not block models." +[[option.mode.LITERALS]] + name = "literals" + help = "Block models based on the SAT skeleton." +[[option.mode.VALUES]] + name = "valuels" + help = "Block models based on the concrete model values for the free variables." [[option]] name = "proof" @@ -163,10 +183,21 @@ header = "options/smt_options.h" category = "regular" long = "sygus-out=MODE" type = "SygusSolutionOutMode" - default = "SYGUS_SOL_OUT_STATUS_AND_DEF" - handler = "stringToSygusSolutionOutMode" - includes = ["options/sygus_out_mode.h"] + default = "STATUS_AND_DEF" help = "output mode for sygus" + help_mode = "Modes for sygus solution output." +[[option.mode.STATUS]] + name = "status" + help = "Print only status for check-synth calls." +[[option.mode.STATUS_AND_DEF]] + name = "status-and-def" + help = "Print status followed by definition corresponding to solution." +[[option.mode.STATUS_OR_DEF]] + name = "status-or-def" + help = "Print status if infeasible, or definition corresponding to solution if feasible." +[[option.mode.STANDARD]] + name = "sygus-standard" + help = "Print based on SyGuS standard." [[option]] name = "sygusPrintCallbacks" diff --git a/src/options/strings_modes.cpp b/src/options/strings_modes.cpp deleted file mode 100644 index c56c82716..000000000 --- a/src/options/strings_modes.cpp +++ /dev/null @@ -1,71 +0,0 @@ -/********************* */ -/*! \file strings_modes.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Modes for the string solver. - **/ - -#include "options/strings_modes.h" - -#include <cstdint> -#include <iostream> - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, - theory::strings::ProcessLoopMode mode) -{ - switch (mode) - { - case theory::strings::ProcessLoopMode::FULL: - out << "ProcessLoopMode::FULL"; - break; - case theory::strings::ProcessLoopMode::SIMPLE: - out << "ProcessLoopMode::SIMPLE"; - break; - case theory::strings::ProcessLoopMode::SIMPLE_ABORT: - out << "ProcessLoopMode::SIMPLE_ABORT"; - break; - case theory::strings::ProcessLoopMode::NONE: - out << "ProcessLoopMode::NONE"; - break; - case theory::strings::ProcessLoopMode::ABORT: - out << "ProcessLoopMode::ABORT"; - break; - default: - out << "ProcessLoopMode:UNKNOWN![" << static_cast<int64_t>(mode) << "]"; - } - return out; -} - -std::ostream& operator<<(std::ostream& out, - theory::strings::RegExpInterMode mode) -{ - switch (mode) - { - case theory::strings::RegExpInterMode::RE_INTER_ALL: - out << "RegExpInterMode::RE_INTER_ALL"; - break; - case theory::strings::RegExpInterMode::RE_INTER_CONSTANT: - out << "RegExpInterMode::RE_INTER_CONSTANT"; - break; - case theory::strings::RegExpInterMode::RE_INTER_ONE_CONSTANT: - out << "RegExpInterMode::RE_INTER_ONE_CONSTANT"; - break; - case theory::strings::RegExpInterMode::RE_INTER_NONE: - out << "RegExpInterMode::RE_INTER_NONE"; - break; - default: - out << "RegExpInterMode:UNKNOWN![" << static_cast<int64_t>(mode) << "]"; - } - return out; -} - -} // namespace CVC4 diff --git a/src/options/strings_modes.h b/src/options/strings_modes.h deleted file mode 100644 index 7823ea8c7..000000000 --- a/src/options/strings_modes.h +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \file strings_modes.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Modes for the string solver. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__STRINGS__STRINGS_MODES_H -#define CVC4__THEORY__STRINGS__STRINGS_MODES_H - -#include <iosfwd> - -namespace CVC4 { -namespace theory { -namespace strings { - -/** Enumeration of string processing loop modes */ -enum ProcessLoopMode -{ - /** Perform full loop processing. */ - FULL, - - /** Omit normal loop breaking. */ - SIMPLE, - - /** Abort if normal loop breaking is required. */ - SIMPLE_ABORT, - - /** Omit loop processing. */ - NONE, - - /** Abort if looping word equations are encountered. */ - ABORT -}; // enum ProcessLoopMode - -/** Enumeration of regular expression intersection modes */ -enum RegExpInterMode -{ - /** Compute intersections for all regular expressions. */ - RE_INTER_ALL, - - /** - * Compute intersections only for regular expressions without re.allchar - * and re.range. - */ - RE_INTER_CONSTANT, - - /** - * Compute intersections only between regular expressions where one side does - * not contain re.allchar and re.range. - */ - RE_INTER_ONE_CONSTANT, - - /** Do not compute intersections of regular expressions. */ - RE_INTER_NONE, -}; // enum RegExpInterMode - -} // namespace strings -} // namespace theory - -std::ostream& operator<<(std::ostream& out, - theory::strings::ProcessLoopMode mode); - -std::ostream& operator<<(std::ostream& out, - theory::strings::RegExpInterMode mode); - -} // namespace CVC4 - -#endif /* CVC4__THEORY__STRINGS__STRINGS_MODES_H */ diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 2d8411256..3916c68f3 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -132,11 +132,26 @@ header = "options/strings_options.h" name = "stringProcessLoopMode" category = "expert" long = "strings-process-loop-mode=MODE" - type = "CVC4::theory::strings::ProcessLoopMode" - default = "CVC4::theory::strings::ProcessLoopMode::FULL" - handler = "stringToStringsProcessLoopMode" - includes = ["options/strings_modes.h"] + type = "ProcessLoopMode" + default = "FULL" help = "determines how to process looping string equations" + help_mode = "Loop processing modes." +[[option.mode.FULL]] + name = "full" + help = "Perform full processing of looping word equations." +[[option.mode.SIMPLE]] + name = "simple" + help = "Omit normal loop breaking (default with --strings-fmf)." +[[option.mode.SIMPLE_ABORT]] + name = "simple-abort" + help = "Abort when normal loop breaking is required." +[[option.mode.NONE]] + name = "none" + help = "Omit loop processing." +[[option.mode.ABORT]] + name = "abort" + help = "Abort if looping word equations are encountered." + [[option]] name = "stringInferAsLemmas" @@ -221,8 +236,19 @@ header = "options/strings_options.h" name = "stringRegExpInterMode" category = "expert" long = "re-inter-mode=MODE" - type = "CVC4::theory::strings::RegExpInterMode" - default = "CVC4::theory::strings::RE_INTER_CONSTANT" - handler = "stringToRegExpInterMode" - includes = ["options/strings_modes.h"] + type = "RegExpInterMode" + default = "CONSTANT" help = "determines which regular expressions intersections to compute" + help_mode = "Regular expression intersection modes." +[[option.mode.ALL]] + name = "all" + help = "Compute intersections for all regular expressions." +[[option.mode.CONSTANT]] + name = "constant" + help = "Compute intersections only between regular expressions that do not contain re.allchar or re.range." +[[option.mode.ONE_CONSTANT]] + name = "one-constant" + help = "Compute intersections only between regular expressions such that at least one side does not contain re.allchar or re.range." +[[option.mode.NONE]] + name = "none" + help = "Do not compute intersections for regular expressions." diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h deleted file mode 100644 index 79480946a..000000000 --- a/src/options/sygus_out_mode.h +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file sygus_out_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Options for sygus solution output. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__SMT__SYGUS_OUT_MODE_H -#define CVC4__SMT__SYGUS_OUT_MODE_H - -#include <iosfwd> - -namespace CVC4 { - -/** Mode for printing sygus solutions. */ -enum SygusSolutionOutMode -{ - /** print status */ - SYGUS_SOL_OUT_STATUS, - /** (default) print status and solution */ - SYGUS_SOL_OUT_STATUS_AND_DEF, - /** print status if infeasible, or solution if feasible */ - SYGUS_SOL_OUT_STATUS_OR_DEF, - /** print output specified by sygus standard */ - SYGUS_SOL_OUT_STANDARD, -}; - -} /* CVC4 namespace */ - -#endif /* CVC4__SMT__SYGUS_OUT_MODE_H */ diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 3509f408d..13c3d5cfb 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -7,11 +7,16 @@ header = "options/theory_options.h" smt_name = "theoryof-mode" category = "expert" long = "theoryof-mode=MODE" - type = "CVC4::theory::TheoryOfMode" - default = "CVC4::theory::THEORY_OF_TYPE_BASED" - handler = "stringToTheoryOfMode" - includes = ["options/theoryof_mode.h"] + type = "TheoryOfMode" + default = "THEORY_OF_TYPE_BASED" help = "mode for Theory::theoryof()" + help_mode = "Defines how we associate theories with terms." +[[option.mode.THEORY_OF_TYPE_BASED]] + name = "type" + help = "Type variables, constants and equalities by type." +[[option.mode.THEORY_OF_TERM_BASED]] + name = "term" + help = "Type variables as uninterpreted, type constants by theory, equalities by the parametric theory." [[option]] name = "useTheoryList" diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp deleted file mode 100644 index 4d8d92e17..000000000 --- a/src/options/theoryof_mode.cpp +++ /dev/null @@ -1,36 +0,0 @@ -/********************* */ -/*! \file theoryof_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "options/theoryof_mode.h" - -#include <ostream> - -namespace CVC4 { -namespace theory { - -std::ostream& operator<<(std::ostream& out, TheoryOfMode m) -{ - switch(m) { - case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED"; - case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED"; - default: return out << "TheoryOfMode!UNKNOWN"; - } -} - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h deleted file mode 100644 index 900452fbc..000000000 --- a/src/options/theoryof_mode.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file theoryof_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Option selection for theoryOf() operation - ** - ** Option selection for theoryOf() operation. - **/ - -#include "cvc4_public.h" - -#pragma once - -#include <ostream> - -namespace CVC4 { -namespace theory { - -/** How do we associate theories with the terms */ -enum TheoryOfMode { - /** Equality, variables and constants are associated with the types */ - THEORY_OF_TYPE_BASED, - /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */ - THEORY_OF_TERM_BASED -};/* enum TheoryOfMode */ - -std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 8790e4ec3..6916598ce 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -51,12 +51,20 @@ header = "options/uf_options.h" name = "ufssMode" category = "regular" long = "uf-ss=MODE" - type = "CVC4::theory::uf::UfssMode" - default = "CVC4::theory::uf::UF_SS_FULL" - handler = "stringToUfssMode" - includes = ["options/ufss_mode.h"] + type = "UfssMode" + default = "FULL" read_only = true help = "mode of operation for uf with cardinality solver." + help_mode = "UF with cardinality options currently supported by the --uf-ss option when combined with finite model finding." +[[option.mode.FULL]] + name = "full" + help = "Default, use UF with cardinality to find minimal models for uninterpreted sorts." +[[option.mode.NO_MINIMAL]] + name = "no-minimal" + help = "Use UF with cardinality to shrink models, but do no enforce minimality." +[[option.mode.NONE]] + name = "none" + help = "Do not use UF with cardinality to shrink model sizes." [[option]] name = "ufssFairness" diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h deleted file mode 100644 index 452317b8f..000000000 --- a/src/options/ufss_mode.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \file ufss_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Custom handlers and predicates for TheoryUF options - ** - ** Custom handlers and predicates for TheoryUF options. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__BASE__UFSS_MODE_H -#define CVC4__BASE__UFSS_MODE_H - -namespace CVC4 { -namespace theory { -namespace uf { - -/** - * These modes determine the role of UF with cardinality when using finite model - * finding (--finite-model-find). - */ -enum UfssMode -{ - /** - * Default, use UF with cardinality to find minimal models for uninterpreted - * sorts. - */ - UF_SS_FULL, - /** - * Use UF with cardinality to shrink model sizes, but do no enforce - * minimality. - */ - UF_SS_NO_MINIMAL, - /** do not use UF with cardinality */ - UF_SS_NONE, -}; - -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__BASE__UFSS_MODE_H */ |