From 97a870f131138662d93299c76ef49865bbc6f546 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 11 May 2022 21:52:31 -0700 Subject: [PATCH] Make regular options access const (#8754) One of the loose ends of the options refactor is that internal code can write to options at will, even when the accessing it via Env::getOptions() which returns a const reference. There are technical reasons for this, C++ does not propagate the constness into reference members. This PR changes this behaviour by making the references members we use all over the place (options().smt.foo) const references and adding new functions writeSmt() which allow write access -- if you have a non-const handle to the options object. In order to do that, this PR also changes all places that legitimately change the options (options handlers, set defaults, solver engine and places where we spawn subsolvers) to use the new syntax. After that, only a single place remains: the solver engine attempts to write the filename (from Solver::setInfo("filename", "...");) into the original options (that are restored to the new solver object after a reset. As only the API solver has write access to this, it is moved to the Solver::setInfo() method. With this PR, all internal code is properly guarded against erroneous (and reckless) changing of options. Fixes cvc5/cvc5-projects#12. --- src/api/cpp/cvc5.cpp | 5 + src/options/README.md | 8 +- src/options/mkoptions.py | 22 +- src/options/options_handler.cpp | 22 +- src/options/options_template.cpp | 4 + src/smt/set_defaults.cpp | 298 +++++++++--------- src/smt/solver_engine.cpp | 25 +- src/smt/sygus_solver.cpp | 4 +- .../quantifiers/query_generator_unsat.cpp | 10 +- src/theory/quantifiers/sygus/synth_verify.cpp | 12 +- test/unit/node/node_black.cpp | 4 +- .../theory/theory_arith_coverings_white.cpp | 4 +- 12 files changed, 225 insertions(+), 193 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a69d1f641..e0999dbff 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7347,6 +7347,11 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const value) << "'sat', 'unsat' or 'unknown'"; //////// all checks before this line + if (keyword == "filename") + { + // only the Solver object has non-const access to the original options + d_originalOptions->writeDriver().filename = value; + } d_slv->setInfo(keyword, value); //////// CVC5_API_TRY_CATCH_END; diff --git a/src/options/README.md b/src/options/README.md index 2f89f04ee..9227cc35c 100644 --- a/src/options/README.md +++ b/src/options/README.md @@ -16,6 +16,8 @@ After parsing, a module is extended to have the following attributes: * `id`: lower-case version of the parsed `id` * `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class) +* `id_capitalized`: `id` with first letter upper-cased (used for the + `write{id_capitalized}()` method) * `filename`: base filename for generated files (`"{id}_options"`) * `header`: generated header name (`"options/{filename}.h"`) @@ -166,8 +168,10 @@ consists of the following components: The `Options` class is the central entry point for regular usage of options. It holds a `std::unique_ptr` to an "option holder" for every option module, that -can be accessed using references `{module}` (either as `const&` or `&`). These -holders hold the actual option data for the specific module. +can be accessed using references `const {module}&`. These holders hold the actual +option data for the specific module. For non-const accesses, there are methods +`write{module}()` which can only be used from a non-const handle to the `Options` +object. The holder types are forward declared and can thus only be accessed if one also includes the appropriate `{module}_options.h`, which contains the proper diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index e30f7093c..b4c1aeed9 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -157,6 +157,7 @@ class Module(object): self.options = [] self.id = self.id.lower() self.id_cap = self.id.upper() + self.id_capitalized = self.id.capitalize() self.filename = os.path.splitext(os.path.split(filename)[-1])[0] self.header = os.path.join('options', '{}.h'.format(self.filename)) @@ -220,7 +221,8 @@ def generate_holder_mem_decls(modules): def generate_holder_ref_decls(modules): """Render reference declarations for holder members of the Option class""" - return concat_format(' options::Holder{id_cap}& {id};', modules) + return concat_format(''' const options::Holder{id_cap}& {id}; + options::Holder{id_cap}& write{id_capitalized}();''', modules) ################################################################################ @@ -244,6 +246,15 @@ def generate_holder_ref_inits(modules): return concat_format(' {id}(*d_{id}),', modules) +def generate_write_functions(modules): + """Render write functions for holders within the Option class""" + return concat_format(''' options::Holder{id_cap}& Options::write{id_capitalized}() + {{ + return *d_{id}; + }} +''', modules) + + def generate_holder_mem_copy(modules): """Render copy operation of holder members of the Option class""" return concat_format(' *d_{id} = *options.d_{id};', modules) @@ -334,10 +345,10 @@ def generate_set_impl(modules): for pred in _set_predicates(option): res.append(' {}'.format(pred)) if option.name: - res.append(' opts.{module}.{name} = value;'.format( - module=module.id, name=option.name)) - res.append(' opts.{module}.{name}WasSetByUser = true;'.format( - module=module.id, name=option.name)) + res.append(' opts.write{module}().{name} = value;'.format( + module=module.id_capitalized, name=option.name)) + res.append(' opts.write{module}().{name}WasSetByUser = true;'.format( + module=module.id_capitalized, name=option.name)) return '\n '.join(res) @@ -873,6 +884,7 @@ def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls): 'headers_module': generate_module_headers(modules), 'holder_mem_inits': generate_holder_mem_inits(modules), 'holder_ref_inits': generate_holder_ref_inits(modules), + 'write_functions': generate_write_functions(modules), 'holder_mem_copy': generate_holder_mem_copy(modules), # options/options_public.cpp 'options_includes': generate_public_includes(modules), diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 839a848d6..fd4d5be06 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -177,13 +177,13 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value) void OptionsHandler::decreaseVerbosity(const std::string& flag, bool value) { - d_options->base.verbosity -= 1; + d_options->writeBase().verbosity -= 1; setVerbosity(flag, d_options->base.verbosity); } void OptionsHandler::increaseVerbosity(const std::string& flag, bool value) { - d_options->base.verbosity += 1; + d_options->writeBase().verbosity += 1; setVerbosity(flag, d_options->base.verbosity); } @@ -201,9 +201,9 @@ void OptionsHandler::setStats(const std::string& flag, bool value) #endif /* CVC5_STATISTICS_ON */ if (!value) { - d_options->base.statisticsAll = false; - d_options->base.statisticsEveryQuery = false; - d_options->base.statisticsInternal = false; + d_options->writeBase().statisticsAll = false; + d_options->writeBase().statisticsEveryQuery = false; + d_options->writeBase().statisticsInternal = false; } } @@ -221,7 +221,7 @@ void OptionsHandler::setStatsDetail(const std::string& flag, bool value) #endif /* CVC5_STATISTICS_ON */ if (value) { - d_options->base.statistics = true; + d_options->writeBase().statistics = true; } } @@ -237,7 +237,7 @@ void OptionsHandler::enableTraceTag(const std::string& flag, { if (optarg == "help") { - d_options->driver.showTraceTags = true; + d_options->writeDriver().showTraceTags = true; showTraceTags("", true); return; } @@ -268,7 +268,7 @@ void OptionsHandler::enableDebugTag(const std::string& flag, { if (optarg == "help") { - d_options->driver.showDebugTags = true; + d_options->writeDriver().showDebugTags = true; showDebugTags("", true); return; } @@ -288,7 +288,7 @@ void OptionsHandler::enableOutputTag(const std::string& flag, size_t tagid = static_cast(optarg); Assert(d_options->base.outputTagHolder.size() > tagid) << "Output tag is larger than the bitset that holds it."; - d_options->base.outputTagHolder.set(tagid); + d_options->writeBase().outputTagHolder.set(tagid); } void OptionsHandler::setPrintSuccess(const std::string& flag, bool value) @@ -301,7 +301,7 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value) void OptionsHandler::setResourceWeight(const std::string& flag, const std::string& optarg) { - d_options->base.resourceWeightHolder.emplace_back(optarg); + d_options->writeBase().resourceWeightHolder.emplace_back(optarg); } void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m) @@ -352,7 +352,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m) } if (!d_options->bv.bitvectorToBoolWasSetByUser) { - d_options->bv.bitvectorToBool = true; + d_options->writeBv().bitvectorToBool = true; } } } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 4783441fd..cea6a2139 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -40,6 +40,10 @@ ${holder_ref_inits}$ Options::~Options() {} +// clang-format off +${write_functions}$ +// clang-format on + void Options::copyValues(const Options& options) { if (this != &options) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4f54310e7..dc26303ad 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -71,26 +71,26 @@ void SetDefaults::setDefaultsPre(Options& opts) // implied options if (opts.smt.debugCheckModels) { - opts.smt.checkModels = true; + opts.writeSmt().checkModels = true; } if (opts.smt.checkModels || opts.driver.dumpModels) { - opts.smt.produceModels = true; + opts.writeSmt().produceModels = true; } if (opts.smt.checkModels) { - opts.smt.produceAssignments = true; + opts.writeSmt().produceAssignments = true; } // unsat cores and proofs shenanigans if (opts.driver.dumpDifficulty) { - opts.smt.produceDifficulty = true; + opts.writeSmt().produceDifficulty = true; } if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) { - opts.smt.unsatCores = true; + opts.writeSmt().unsatCores = true; } if (opts.smt.unsatCores && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) @@ -100,21 +100,21 @@ void SetDefaults::setDefaultsPre(Options& opts) notifyModifyOption( "unsatCoresMode", "assumptions", "enabling unsat cores"); } - opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; + opts.writeSmt().unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } // if check-proofs, dump-proofs, or proof-mode=full, then proofs being fully // enabled is implied if (opts.smt.checkProofs || opts.driver.dumpProofs || opts.smt.proofMode == options::ProofMode::FULL) { - opts.smt.produceProofs = true; + opts.writeSmt().produceProofs = true; } // this check assumes the user has requested *full* proofs if (opts.smt.produceProofs) { // if the user requested proofs, proof mode is full - opts.smt.proofMode = options::ProofMode::FULL; + opts.writeSmt().proofMode = options::ProofMode::FULL; // unsat cores are available due to proofs being enabled if (opts.smt.unsatCoresMode != options::UnsatCoresMode::SAT_PROOF) { @@ -122,8 +122,8 @@ void SetDefaults::setDefaultsPre(Options& opts) { notifyModifyOption("unsatCoresMode", "sat-proof", "enabling proofs"); } - opts.smt.unsatCores = true; - opts.smt.unsatCoresMode = options::UnsatCoresMode::SAT_PROOF; + opts.writeSmt().unsatCores = true; + opts.writeSmt().unsatCoresMode = options::UnsatCoresMode::SAT_PROOF; } } if (!opts.smt.produceProofs) @@ -132,32 +132,32 @@ void SetDefaults::setDefaultsPre(Options& opts) { // if (expert) user set proof mode to something other than off, enable // proofs - opts.smt.produceProofs = true; + opts.writeSmt().produceProofs = true; } // if proofs weren't enabled by user, and we are producing difficulty if (opts.smt.produceDifficulty) { - opts.smt.produceProofs = true; + opts.writeSmt().produceProofs = true; // ensure at least preprocessing proofs are enabled if (opts.smt.proofMode == options::ProofMode::OFF) { - opts.smt.proofMode = options::ProofMode::PP_ONLY; + opts.writeSmt().proofMode = options::ProofMode::PP_ONLY; } } // if proofs weren't enabled by user, and we are producing unsat cores if (opts.smt.unsatCores) { - opts.smt.produceProofs = true; + opts.writeSmt().produceProofs = true; if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF) { // if requested to be based on proofs, we produce (preprocessing +) SAT // proofs - opts.smt.proofMode = options::ProofMode::SAT; + opts.writeSmt().proofMode = options::ProofMode::SAT; } else if (opts.smt.proofMode == options::ProofMode::OFF) { // otherwise, we always produce preprocessing proofs - opts.smt.proofMode = options::ProofMode::PP_ONLY; + opts.writeSmt().proofMode = options::ProofMode::PP_ONLY; } } } @@ -184,10 +184,10 @@ void SetDefaults::setDefaultsPre(Options& opts) { // these options must be disabled on internal subsolvers, as they are // used by the user to rephrase the input. - opts.quantifiers.sygusInference = false; - opts.quantifiers.sygusRewSynthInput = false; + opts.writeQuantifiers().sygusInference = false; + opts.writeQuantifiers().sygusRewSynthInput = false; // deep restart does not work with internal subsolvers? - opts.smt.deepRestartMode = options::DeepRestartMode::NONE; + opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE; } } @@ -208,7 +208,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const && logic.areIntegersUsed())) && !opts.base.incrementalSolving) { - opts.quantifiers.sygusInst = true; + opts.writeQuantifiers().sygusInst = true; } if (opts.bv.bitblastMode == options::BitblastMode::EAGER) @@ -226,12 +226,12 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const "functions. Try --bitblast=lazy")); } notifyModifyOption("bitblastMode", "lazy", "model generation"); - opts.bv.bitblastMode = options::BitblastMode::LAZY; + opts.writeBv().bitblastMode = options::BitblastMode::LAZY; } else if (!opts.base.incrementalSolving) { // if not incremental, we rely on ackermann to eliminate other theories. - opts.smt.ackermann = true; + opts.writeSmt().ackermann = true; } else if (logic.isQuantified() || !logic.isPure(THEORY_BV)) { @@ -291,7 +291,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const "Ackermannization currently does not support model generation.")); } notifyModifyOption("ackermann", "false", "model generation"); - opts.smt.ackermann = false; + opts.writeSmt().ackermann = false; // we are not relying on ackermann to eliminate theories in this case Assert(opts.bv.bitblastMode != options::BitblastMode::EAGER); } @@ -325,7 +325,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. - opts.strings.stringExp = true; + opts.writeStrings().stringExp = true; Trace("smt") << "Turning stringExp on since logic does not have everything " "and string theory is enabled\n"; } @@ -399,7 +399,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.smt.produceAssertions) { verbose(1) << "SolverEngine: turning on produce-assertions." << std::endl; - opts.smt.produceAssertions = true; + opts.writeSmt().produceAssertions = true; } if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) @@ -410,7 +410,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const * Therefore, we enable bv-to-bool, which runs before * the translation to integers. */ - opts.bv.bitvectorToBool = true; + opts.writeBv().bitvectorToBool = true; } // Disable options incompatible with incremental solving, or output an error @@ -457,7 +457,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !logic.isTheoryEnabled(THEORY_ARITH); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; - opts.smt.unconstrainedSimp = uncSimp; + opts.writeSmt().unconstrainedSimp = uncSimp; } // by default, nonclausal simplification is off for QF_SAT @@ -470,8 +470,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // quantifiers, not others opts.set(options::simplificationMode, qf_sat || // quantifiers ? options::SimplificationMode::NONE : // options::SimplificationMode::BATCH); - opts.smt.simplificationMode = qf_sat ? options::SimplificationMode::NONE - : options::SimplificationMode::BATCH; + opts.writeSmt().simplificationMode = + qf_sat ? options::SimplificationMode::NONE + : options::SimplificationMode::BATCH; } } @@ -488,7 +489,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const verbose(1) << "SolverEngine: turning off bool-to-bitvector to support CBQI BV" << std::endl; - opts.bv.boolToBitvector = options::BoolToBVMode::OFF; + opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF; } } @@ -497,7 +498,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && (opts.smt.produceAssignments || usesSygus(opts))) { verbose(1) << "SolverEngine: turning on produce-models" << std::endl; - opts.smt.produceModels = true; + opts.writeSmt().produceModels = true; } // --ite-simp is an experimental option designed for QF_LIA/nec. This @@ -508,7 +509,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.smt.earlyIteRemovalWasSetByUser) { - opts.smt.earlyIteRemoval = true; + opts.writeSmt().earlyIteRemoval = true; } } @@ -523,7 +524,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !logic.isQuantified())) { Trace("smt") << "setting theoryof-mode to term-based" << std::endl; - opts.theory.theoryOfMode = options::TheoryOfMode::THEORY_OF_TERM_BASED; + opts.writeTheory().theoryOfMode = + options::TheoryOfMode::THEORY_OF_TERM_BASED; } } @@ -535,7 +537,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !safeUnsatCores(opts); Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << std::endl; - opts.uf.ufSymmetryBreaker = qf_uf_noinc; + opts.writeUf().ufSymmetryBreaker = qf_uf_noinc; } // If in arrays, set the UF handler to arrays @@ -560,7 +562,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const bool withCare = qf_aufbv; Trace("smt") << "setting ite simplify with care to " << withCare << std::endl; - opts.smt.simplifyWithCareEnabled = withCare; + opts.writeSmt().simplifyWithCareEnabled = withCare; } // Turn off array eager index splitting for QF_AUFLIA if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser) @@ -571,7 +573,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { Trace("smt") << "setting array eager index splitting to false" << std::endl; - opts.arrays.arraysEagerIndexSplitting = false; + opts.writeArrays().arraysEagerIndexSplitting = false; } } // Turn on multiple-pass non-clausal simplification for QF_AUFBV @@ -584,13 +586,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !safeUnsatCores(opts); Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; - opts.smt.repeatSimp = repeatSimp; + opts.writeSmt().repeatSimp = repeatSimp; } /* Disable bit-level propagation by default for the BITBLAST solver. */ if (opts.bv.bvSolver == options::BVSolver::BITBLAST) { - opts.bv.bitvectorPropagate = false; + opts.writeBv().bitvectorPropagate = false; } if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL @@ -603,7 +605,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } verbose(1) << "SolverEngine: turning off bool-to-bv for non-bv logic: " << logic.getLogicString() << std::endl; - opts.bv.boolToBitvector = options::BoolToBVMode::OFF; + opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF; } // Turn on arith rewrite equalities only for pure arithmetic @@ -613,7 +615,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; - opts.arith.arithRewriteEq = arithRewriteEq; + opts.writeArith().arithRewriteEq = arithRewriteEq; } if (!opts.arith.arithHeuristicPivotsWasSetByUser) { @@ -631,7 +633,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots << std::endl; - opts.arith.arithHeuristicPivots = heuristicPivots; + opts.writeArith().arithHeuristicPivots = heuristicPivots; } if (!opts.arith.arithPivotThresholdWasSetByUser) { @@ -645,7 +647,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold << std::endl; - opts.arith.arithPivotThreshold = pivotThreshold; + opts.writeArith().arithPivotThreshold = pivotThreshold; } if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) { @@ -656,7 +658,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots << std::endl; - opts.arith.arithStandardCheckVarOrderPivots = varOrderPivots; + opts.writeArith().arithStandardCheckVarOrderPivots = varOrderPivots; } if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed()) { @@ -664,14 +666,14 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << std::endl; - opts.arith.nlExtTangentPlanesInterleave = true; + opts.writeArith().nlExtTangentPlanesInterleave = true; } } if (!opts.arith.nlRlvAssertBoundsWasSetByUser) { // use bound inference to determine when bounds are irrelevant only when // the logic is quantifier-free - opts.arith.nlRlvAssertBounds = !logic.isQuantified(); + opts.writeArith().nlRlvAssertBounds = !logic.isQuantified(); } // set the default decision mode @@ -683,7 +685,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.arith.arithEqSolverWasSetByUser) { // use the arithmetic equality solver by default - opts.arith.arithEqSolver = true; + opts.writeArith().arithEqSolver = true; } } @@ -692,7 +694,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.theory.assignFunctionValues) { // must assign function values - opts.theory.assignFunctionValues = true; + opts.writeTheory().assignFunctionValues = true; } } @@ -708,7 +710,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const Trace("smt") << "Disabling shared selectors for quantified logic without SyGuS" << std::endl; - opts.datatypes.dtSharedSelectors = false; + opts.writeDatatypes().dtSharedSelectors = false; } } @@ -728,7 +730,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.checkModels || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { - opts.prop.minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM; + opts.writeProp().minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM; } } @@ -744,7 +746,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << opts.arith.nlRlvMode << std::endl; } // must use relevance filtering techniques - opts.theory.relevanceFilter = true; + opts.writeTheory().relevanceFilter = true; } } @@ -752,7 +754,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (opts.smt.produceModels || opts.smt.produceAssignments || opts.smt.checkModels) { - opts.arrays.arraysOptimizeLinear = false; + opts.writeArrays().arraysOptimizeLinear = false; } if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) @@ -760,7 +762,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const Trace("smt") << "settting stringProcessLoopMode to 'simple' since " "--strings-fmf enabled" << std::endl; - opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE; + opts.writeStrings().stringProcessLoopMode = + options::ProcessLoopMode::SIMPLE; } // !!! All options that require disabling models go here @@ -778,7 +781,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } verbose(1) << "SolverEngine: turning off produce-models to support " << sOptNoModel << std::endl; - opts.smt.produceModels = false; + opts.writeSmt().produceModels = false; } if (opts.smt.produceAssignments) { @@ -791,7 +794,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } verbose(1) << "SolverEngine: turning off produce-assignments to support " << sOptNoModel << std::endl; - opts.smt.produceAssignments = false; + opts.writeSmt().produceAssignments = false; } if (opts.smt.checkModels) { @@ -804,7 +807,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } verbose(1) << "SolverEngine: turning off check-models to support " << sOptNoModel << std::endl; - opts.smt.checkModels = false; + opts.writeSmt().checkModels = false; } } @@ -824,14 +827,14 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - opts.arith.nlCov = true; + opts.writeArith().nlCov = true; if (!opts.arith.nlExtWasSetByUser) { - opts.arith.nlExt = options::NlExtMode::LIGHT; + opts.writeArith().nlExt = options::NlExtMode::LIGHT; } if (!opts.arith.nlRlvModeWasSetByUser) { - opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE; + opts.writeArith().nlRlvMode = options::NlRlvMode::INTERLEAVE; } } } @@ -841,10 +844,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - opts.arith.nlCov = true; + opts.writeArith().nlCov = true; if (!opts.arith.nlExtWasSetByUser) { - opts.arith.nlExt = options::NlExtMode::LIGHT; + opts.writeArith().nlExt = options::NlExtMode::LIGHT; } } } @@ -860,8 +863,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { verbose(1) << "Cannot use --nl-cov without configuring with --poly." << std::endl; - opts.arith.nlCov = false; - opts.arith.nlExt = options::NlExtMode::FULL; + opts.writeArith().nlCov = false; + opts.writeArith().nlExt = options::NlExtMode::FULL; } } #endif @@ -869,7 +872,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.arith.nlExtWasSetByUser) { - opts.arith.nlExt = options::NlExtMode::FULL; + opts.writeArith().nlExt = options::NlExtMode::FULL; } } } @@ -953,7 +956,7 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, verbose(1) << "Disabling bv-assert-input since it is incompatible with proofs." << std::endl; - opts.bv.bvAssertInput = false; + opts.writeBv().bvAssertInput = false; } // If proofs are required and the user did not specify a specific BV solver, // we make sure to use the proof producing BITBLAST_INTERNAL solver. @@ -962,14 +965,14 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, { verbose(1) << "Forcing internal bit-vector solver due to proof production." << std::endl; - opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL; + opts.writeBv().bvSolver = options::BVSolver::BITBLAST_INTERNAL; } if (opts.arith.nlCovVarElim && !opts.arith.nlCovVarElimWasSetByUser) { verbose(1) << "Disabling nl-cov-var-elim since it is incompatible with proofs." << std::endl; - opts.arith.nlCovVarElim = false; + opts.writeArith().nlCovVarElim = false; } if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) { @@ -1033,7 +1036,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, return true; } notifyModifyOption("unconstrainedSimp", "false", "incremental solving"); - opts.smt.unconstrainedSimp = false; + opts.writeSmt().unconstrainedSimp = false; } if (opts.bv.bitblastMode == options::BitblastMode::EAGER && !logic.isPure(THEORY_BV)) @@ -1050,7 +1053,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, return true; } notifyModifyOption("sygusInference", "false", "incremental solving"); - opts.quantifiers.sygusInference = false; + opts.writeQuantifiers().sygusInference = false; } if (opts.quantifiers.sygusInst) { @@ -1060,7 +1063,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, return true; } notifyModifyOption("sygusInst", "false", "incremental solving"); - opts.quantifiers.sygusInst = false; + opts.writeQuantifiers().sygusInst = false; } if (opts.smt.solveIntAsBV > 0) { @@ -1080,13 +1083,13 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, // disable modes not supported by incremental notifyModifyOption("sortInference", "false", "incremental solving"); - opts.smt.sortInference = false; - opts.uf.ufssFairnessMonotone = false; + opts.writeSmt().sortInference = false; + opts.writeUf().ufssFairnessMonotone = false; notifyModifyOption("globalNegate", "false", "incremental solving"); - opts.quantifiers.globalNegate = false; + opts.writeQuantifiers().globalNegate = false; notifyModifyOption("cegqiNestedQE", "false", "incremental solving"); - opts.quantifiers.cegqiNestedQE = false; - opts.arith.arithMLTrick = false; + opts.writeQuantifiers().cegqiNestedQE = false; + opts.writeArith().arithMLTrick = false; return false; } @@ -1101,13 +1104,13 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("simplificationMode", "none", "unsat cores"); - opts.smt.simplificationMode = options::SimplificationMode::NONE; + opts.writeSmt().simplificationMode = options::SimplificationMode::NONE; if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) { verbose(1) << "SolverEngine: turning off deep restart to support unsat " "cores" << std::endl; - opts.smt.deepRestartMode = options::DeepRestartMode::NONE; + opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE; } } @@ -1119,7 +1122,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("learnedRewrite", "false", "unsat cores"); - opts.smt.learnedRewrite = false; + opts.writeSmt().learnedRewrite = false; } if (opts.arith.pbRewrites) @@ -1130,7 +1133,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("pbRewrites", "false", "unsat cores"); - opts.arith.pbRewrites = false; + opts.writeArith().pbRewrites = false; } if (opts.smt.sortInference) @@ -1141,7 +1144,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("sortInference", "false", "unsat cores"); - opts.smt.sortInference = false; + opts.writeSmt().sortInference = false; } if (opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF) @@ -1152,7 +1155,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("preSkolemQuant", "off", "unsat cores"); - opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::OFF; + opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::OFF; } if (opts.bv.bitvectorToBool) @@ -1163,7 +1166,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("bitvectorToBool", "false", "unsat cores"); - opts.bv.bitvectorToBool = false; + opts.writeBv().bitvectorToBool = false; } if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) @@ -1174,7 +1177,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("boolToBitvector", "off", "unsat cores"); - opts.bv.boolToBitvector = options::BoolToBVMode::OFF; + opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF; } if (opts.bv.bvIntroducePow2) @@ -1185,7 +1188,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("bvIntroducePow2", "false", "unsat cores"); - opts.bv.bvIntroducePow2 = false; + opts.writeBv().bvIntroducePow2 = false; } if (opts.smt.repeatSimp) @@ -1196,7 +1199,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("repeatSimp", "false", "unsat cores"); - opts.smt.repeatSimp = false; + opts.writeSmt().repeatSimp = false; } if (opts.quantifiers.globalNegate) @@ -1207,7 +1210,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("globalNegate", "false", "unsat cores"); - opts.quantifiers.globalNegate = false; + opts.writeQuantifiers().globalNegate = false; } if (opts.smt.doITESimp) @@ -1223,7 +1226,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, return true; } notifyModifyOption("unconstrainedSimp", "false", "unsat cores"); - opts.smt.unconstrainedSimp = false; + opts.writeSmt().unconstrainedSimp = false; } if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) { @@ -1280,7 +1283,7 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts, bool SetDefaults::incompatibleWithSeparationLogic(Options& opts, std::ostream& reason) const { - if (options().smt.simplificationBoolConstProp) + if (opts.smt.simplificationBoolConstProp) { // Spatial formulas in separation logic have a semantics that depends on // their position in the AST (e.g. their nesting beneath separation @@ -1288,7 +1291,7 @@ bool SetDefaults::incompatibleWithSeparationLogic(Options& opts, // predicates to the input formula. We disable this option altogether to // ensure this is the case notifyModifyOption("simplification-bcp", "false", "separation logic"); - options().smt.simplificationBoolConstProp = false; + opts.writeSmt().simplificationBoolConstProp = false; } return false; } @@ -1381,7 +1384,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (opts.quantifiers.fullSaturateQuant) { Trace("smt") << "enabling enum-inst for full-saturate-quant" << std::endl; - opts.quantifiers.enumInst = true; + opts.writeQuantifiers().enumInst = true; } if (opts.arrays.arraysExp) { @@ -1389,26 +1392,26 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (!opts.quantifiers.fmfBoundWasSetByUser) { notifyModifyOption("fmfBound", "true", "arrays-exp"); - opts.quantifiers.fmfBound = true; + opts.writeQuantifiers().fmfBound = true; } } if (logic.hasCardinalityConstraints()) { // must have finite model finding on - opts.quantifiers.finiteModelFind = true; + opts.writeQuantifiers().finiteModelFind = true; } if (opts.quantifiers.instMaxLevel != -1) { verbose(1) << "SolverEngine: turning off cbqi to support instMaxLevel" << std::endl; - opts.quantifiers.cegqi = false; + opts.writeQuantifiers().cegqi = false; } if (opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) { - opts.quantifiers.fmfBound = true; + opts.writeQuantifiers().fmfBound = true; Trace("smt") << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n"; } @@ -1421,11 +1424,11 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, && opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default - opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE; + opts.writeQuantifiers().fmfMbqiMode = options::FmfMbqiMode::NONE; } if (!opts.quantifiers.prenexQuantUserWasSetByUser) { - opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; + opts.writeQuantifiers().prenexQuant = options::PrenexQuantMode::NONE; } } if (logic.isHigherOrder()) @@ -1434,32 +1437,32 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // cannot be used if (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE) { - opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE; + opts.writeQuantifiers().fmfMbqiMode = options::FmfMbqiMode::NONE; } if (!opts.quantifiers.hoElimStoreAxWasSetByUser) { // by default, use store axioms only if --ho-elim is set - opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; + opts.writeQuantifiers().hoElimStoreAx = opts.quantifiers.hoElim; } // Cannot use macros, since lambda lifting and macro elimination are inverse // operations. if (opts.quantifiers.macrosQuant) { - opts.quantifiers.macrosQuant = false; + opts.writeQuantifiers().macrosQuant = false; } } if (opts.quantifiers.fmfFunWellDefinedRelevant) { if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) { - opts.quantifiers.fmfFunWellDefined = true; + opts.writeQuantifiers().fmfFunWellDefined = true; } } if (opts.quantifiers.fmfFunWellDefined) { if (!opts.quantifiers.finiteModelFindWasSetByUser) { - opts.quantifiers.finiteModelFind = true; + opts.writeQuantifiers().finiteModelFind = true; } } @@ -1470,20 +1473,21 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // apply conservative quantifiers splitting if (!opts.quantifiers.quantDynamicSplitWasSetByUser) { - opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT; + opts.writeQuantifiers().quantDynamicSplit = + options::QuantDSplitMode::DEFAULT; } if (!opts.quantifiers.eMatchingWasSetByUser) { // do not use E-matching by default. For E-matching + FMF, the user should // specify --finite-model-find --e-matching. - opts.quantifiers.eMatching = false; + opts.writeQuantifiers().eMatching = false; } if (!opts.quantifiers.instWhenModeWasSetByUser) { // instantiate only on last call if (opts.quantifiers.eMatching) { - opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; + opts.writeQuantifiers().instWhenMode = options::InstWhenMode::LAST_CALL; } } } @@ -1513,14 +1517,14 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { if (!opts.quantifiers.cegqiWasSetByUser) { - opts.quantifiers.cegqi = true; + opts.writeQuantifiers().cegqi = true; } // check whether we should apply full cbqi if (logic.isPure(THEORY_BV)) { if (!opts.quantifiers.cegqiFullEffortWasSetByUser) { - opts.quantifiers.cegqiFullEffort = true; + opts.writeQuantifiers().cegqiFullEffort = true; } } } @@ -1530,42 +1534,42 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { if (!opts.quantifiers.conflictBasedInstWasSetByUser) { - opts.quantifiers.conflictBasedInst = false; + opts.writeQuantifiers().conflictBasedInst = false; } if (!opts.quantifiers.instNoEntailWasSetByUser) { - opts.quantifiers.instNoEntail = false; + opts.writeQuantifiers().instNoEntail = false; } if (!opts.quantifiers.instWhenModeWasSetByUser) { // only instantiation should happen at last call when model is avaiable - opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; + opts.writeQuantifiers().instWhenMode = options::InstWhenMode::LAST_CALL; } } else { // only supported in pure arithmetic or pure BV - opts.quantifiers.cegqiNestedQE = false; + opts.writeQuantifiers().cegqiNestedQE = false; } if (opts.quantifiers.globalNegate) { if (!opts.quantifiers.prenexQuantWasSetByUser) { - opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; + opts.writeQuantifiers().prenexQuant = options::PrenexQuantMode::NONE; } } } // implied options... if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint) { - opts.quantifiers.conflictBasedInst = true; + opts.writeQuantifiers().conflictBasedInst = true; } if (opts.quantifiers.cegqiNestedQE) { - opts.quantifiers.prenexQuantUser = true; + opts.writeQuantifiers().prenexQuantUser = true; if (!opts.quantifiers.preSkolemQuantWasSetByUser) { - opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON; + opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::ON; } } // for induction techniques @@ -1573,11 +1577,11 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { if (!opts.quantifiers.dtStcInductionWasSetByUser) { - opts.quantifiers.dtStcInduction = true; + opts.writeQuantifiers().dtStcInduction = true; } if (!opts.quantifiers.intWfInductionWasSetByUser) { - opts.quantifiers.intWfInduction = true; + opts.writeQuantifiers().intWfInduction = true; } } if (opts.quantifiers.dtStcInduction) @@ -1585,29 +1589,29 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // try to remove ITEs from quantified formulas if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) { - opts.quantifiers.iteDtTesterSplitQuant = true; + opts.writeQuantifiers().iteDtTesterSplitQuant = true; } if (!opts.quantifiers.iteLiftQuantWasSetByUser) { - opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL; + opts.writeQuantifiers().iteLiftQuant = options::IteLiftQuantMode::ALL; } } if (opts.quantifiers.intWfInduction) { if (!opts.quantifiers.purifyTriggersWasSetByUser) { - opts.quantifiers.purifyTriggers = true; + opts.writeQuantifiers().purifyTriggers = true; } } if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { if (opts.quantifiers.conjectureGenPerRound > 0) { - opts.quantifiers.conjectureGen = true; + opts.writeQuantifiers().conjectureGen = true; } else { - opts.quantifiers.conjectureGen = false; + opts.writeQuantifiers().conjectureGen = false; } } // can't pre-skolemize nested quantifiers without UF theory @@ -1616,17 +1620,17 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { - opts.quantifiers.preSkolemQuantNested = false; + opts.writeQuantifiers().preSkolemQuantNested = false; } } if (!logic.isTheoryEnabled(THEORY_DATATYPES)) { - opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE; + opts.writeQuantifiers().quantDynamicSplit = options::QuantDSplitMode::NONE; } if (opts.quantifiers.globalNegate) { notifyModifyOption("deep-restart", "false", "global-negate"); - opts.smt.deepRestartMode = options::DeepRestartMode::NONE; + opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE; } } @@ -1635,24 +1639,24 @@ void SetDefaults::setDefaultsSygus(Options& opts) const if (!opts.quantifiers.sygus) { notifyModifyOption("sygus", "true", ""); - opts.quantifiers.sygus = true; + opts.writeQuantifiers().sygus = true; } // must use Ferrante/Rackoff for real arithmetic if (!opts.quantifiers.cegqiMidpointWasSetByUser) { - opts.quantifiers.cegqiMidpoint = true; + opts.writeQuantifiers().cegqiMidpoint = true; } // must disable cegqi-bv since it may introduce witness terms, which // cannot appear in synthesis solutions if (!opts.quantifiers.cegqiBvWasSetByUser) { - opts.quantifiers.cegqiBv = false; + opts.writeQuantifiers().cegqiBv = false; } if (opts.quantifiers.sygusRepairConst) { if (!opts.quantifiers.cegqiWasSetByUser) { - opts.quantifiers.cegqi = true; + opts.writeQuantifiers().cegqi = true; } } if (opts.quantifiers.sygusInference) @@ -1660,42 +1664,43 @@ void SetDefaults::setDefaultsSygus(Options& opts) const // optimization: apply preskolemization, makes it succeed more often if (!opts.quantifiers.preSkolemQuantWasSetByUser) { - opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON; + opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::ON; } if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { - opts.quantifiers.preSkolemQuantNested = true; + opts.writeQuantifiers().preSkolemQuantNested = true; } } // counterexample-guided instantiation for sygus if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; + opts.writeQuantifiers().cegqiSingleInvMode = + options::CegqiSingleInvMode::USE; } if (!opts.quantifiers.conflictBasedInstWasSetByUser) { - opts.quantifiers.conflictBasedInst = false; + opts.writeQuantifiers().conflictBasedInst = false; } if (!opts.quantifiers.instNoEntailWasSetByUser) { - opts.quantifiers.instNoEntail = false; + opts.writeQuantifiers().instNoEntail = false; } if (!opts.quantifiers.cegqiFullEffortWasSetByUser) { // should use full effort cbqi for single invocation and repair const - opts.quantifiers.cegqiFullEffort = true; + opts.writeQuantifiers().cegqiFullEffort = true; } if (opts.quantifiers.sygusRewSynthInput) { // If we are using synthesis rewrite rules from input, we use // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for // details on this technique. - opts.quantifiers.sygusRewSynth = true; + opts.writeQuantifiers().sygusRewSynth = true; // we should not use the extended rewriter, since we are interested // in rewrites that are not in the main rewriter if (!opts.datatypes.sygusRewriterWasSetByUser) { - opts.datatypes.sygusRewriter = options::SygusRewriterMode::BASIC; + opts.writeDatatypes().sygusRewriter = options::SygusRewriterMode::BASIC; } } // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm @@ -1709,7 +1714,8 @@ void SetDefaults::setDefaultsSygus(Options& opts) const // if doing abduction, we should filter strong solutions if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) { - opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; + opts.writeQuantifiers().sygusFilterSolMode = + options::SygusFilterSolMode::STRONG; } // we must use basic sygus algorithms, since e.g. we require checking // a sygus side condition for consistency with axioms. @@ -1719,7 +1725,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const || opts.quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE) { // rewrite rule synthesis implies that sygus stream must be true - opts.quantifiers.sygusStream = true; + opts.writeQuantifiers().sygusStream = true; } if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) { @@ -1732,30 +1738,32 @@ void SetDefaults::setDefaultsSygus(Options& opts) const { if (!opts.quantifiers.sygusUnifPbeWasSetByUser) { - opts.quantifiers.sygusUnifPbe = false; + opts.writeQuantifiers().sygusUnifPbe = false; } if (opts.quantifiers.sygusUnifPiWasSetByUser) { - opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; + opts.writeQuantifiers().sygusUnifPi = options::SygusUnifPiMode::NONE; } if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) { - opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; + opts.writeQuantifiers().sygusInvTemplMode = + options::SygusInvTemplMode::NONE; } if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; + opts.writeQuantifiers().cegqiSingleInvMode = + options::CegqiSingleInvMode::NONE; } } // do not miniscope if (!opts.quantifiers.miniscopeQuantWasSetByUser) { - opts.quantifiers.miniscopeQuant = options::MiniscopeQuantMode::OFF; + opts.writeQuantifiers().miniscopeQuant = options::MiniscopeQuantMode::OFF; } // do not do macros if (!opts.quantifiers.macrosQuantWasSetByUser) { - opts.quantifiers.macrosQuant = false; + opts.writeQuantifiers().macrosQuant = false; } } void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, @@ -1817,12 +1825,12 @@ void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, ? true : false); - opts.decision.decisionMode = decMode; + opts.writeDecision().decisionMode = decMode; if (stoponly) { if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION) { - opts.decision.decisionMode = options::DecisionMode::STOPONLY; + opts.writeDecision().decisionMode = options::DecisionMode::STOPONLY; } else { diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 2e11da69e..6c7b3d419 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -346,8 +346,7 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) if (key == "filename") { - d_env->d_options.driver.filename = value; - d_env->d_originalOptions->driver.filename = value; + d_env->d_options.writeDriver().filename = value; d_env->getStatisticsRegistry().registerValue( "driver::filename", value); } @@ -360,12 +359,12 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) << " unsupported, defaulting to language (and semantics of) " "SMT-LIB 2.6\n"; } - getOptions().base.inputLanguage = Language::LANG_SMTLIB_V2_6; + getOptions().writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6; // also update the output language if (!getOptions().base.outputLanguageWasSetByUser) { setOption("output-language", "smtlib2.6"); - getOptions().base.outputLanguageWasSetByUser = false; + getOptions().writeBase().outputLanguageWasSetByUser = false; } } else if (key == "status") @@ -1391,10 +1390,10 @@ std::vector SolverEngine::reduceUnsatCore(const std::vector& core) std::unique_ptr coreChecker; initializeSubsolver(coreChecker, *d_env.get()); coreChecker->setLogic(getLogicInfo()); - coreChecker->getOptions().smt.checkUnsatCores = false; + coreChecker->getOptions().writeSmt().checkUnsatCores = false; // disable all proof options - coreChecker->getOptions().smt.produceProofs = false; - coreChecker->getOptions().smt.checkProofs = false; + coreChecker->getOptions().writeSmt().produceProofs = false; + coreChecker->getOptions().writeSmt().checkProofs = false; for (const Node& ucAssertion : core) { @@ -1458,10 +1457,10 @@ void SolverEngine::checkUnsatCore() // initialize the core checker std::unique_ptr coreChecker; initializeSubsolver(coreChecker, *d_env.get()); - coreChecker->getOptions().smt.checkUnsatCores = false; + coreChecker->getOptions().writeSmt().checkUnsatCores = false; // disable all proof options - coreChecker->getOptions().smt.produceProofs = false; - coreChecker->getOptions().smt.checkProofs = false; + coreChecker->getOptions().writeSmt().produceProofs = false; + coreChecker->getOptions().writeSmt().checkProofs = false; // set up separation logic heap if necessary TypeNode sepLocType, sepDataType; @@ -1910,16 +1909,16 @@ void SolverEngine::setResourceLimit(uint64_t units, bool cumulative) { if (cumulative) { - d_env->d_options.base.cumulativeResourceLimit = units; + d_env->d_options.writeBase().cumulativeResourceLimit = units; } else { - d_env->d_options.base.perCallResourceLimit = units; + d_env->d_options.writeBase().perCallResourceLimit = units; } } void SolverEngine::setTimeLimit(uint64_t millis) { - d_env->d_options.base.perCallMillisecondLimit = millis; + d_env->d_options.writeBase().perCallMillisecondLimit = millis; } unsigned long SolverEngine::getResourceUsage() const diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2a5bf1b51..e14c6041b 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -376,8 +376,8 @@ void SygusSolver::checkSynthSolution(Assertions& as, // Start new SMT engine to check solutions std::unique_ptr solChecker; initializeSygusSubsolver(solChecker, as); - solChecker->getOptions().smt.checkSynthSol = false; - solChecker->getOptions().quantifiers.sygusRecFun = false; + solChecker->getOptions().writeSmt().checkSynthSol = false; + solChecker->getOptions().writeQuantifiers().sygusRecFun = false; Assert(conj.getKind() == FORALL); Node conjBody = conj[1]; // we must expand definitions here, since define-fun may contain the diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp index 67a3667c3..a8f248e05 100644 --- a/src/theory/quantifiers/query_generator_unsat.cpp +++ b/src/theory/quantifiers/query_generator_unsat.cpp @@ -32,11 +32,11 @@ QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env) : QueryGenerator(env) // determine the options to use for the verification subsolvers we spawn // we start with the provided options d_subOptions.copyValues(d_env.getOriginalOptions()); - d_subOptions.quantifiers.sygus = false; - d_subOptions.smt.produceProofs = true; - d_subOptions.smt.checkProofs = true; - d_subOptions.smt.produceModels = true; - d_subOptions.smt.checkModels = true; + d_subOptions.writeQuantifiers().sygus = false; + d_subOptions.writeSmt().produceProofs = true; + d_subOptions.writeSmt().checkProofs = true; + d_subOptions.writeSmt().produceModels = true; + d_subOptions.writeSmt().checkModels = true; } bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out) diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index a6b051275..a217fc7e8 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -40,24 +40,24 @@ SynthVerify::SynthVerify(Env& env, TermDbSygus* tds) // we start with the provided options d_subOptions.copyValues(options()); // limit the number of instantiation rounds on subcalls - d_subOptions.quantifiers.instMaxRounds = + d_subOptions.writeQuantifiers().instMaxRounds = d_subOptions.quantifiers.sygusVerifyInstMaxRounds; // Disable sygus on the subsolver. This is particularly important since it // ensures that recursive function definitions have the standard ownership // instead of being claimed by sygus in the subsolver. - d_subOptions.base.inputLanguage = Language::LANG_SMTLIB_V2_6; - d_subOptions.quantifiers.sygus = false; + d_subOptions.writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6; + d_subOptions.writeQuantifiers().sygus = false; // use tangent planes by default, since we want to put effort into // the verification step for sygus queries with non-linear arithmetic if (!d_subOptions.arith.nlExtTangentPlanesWasSetByUser) { - d_subOptions.arith.nlExtTangentPlanes = true; + d_subOptions.writeArith().nlExtTangentPlanes = true; } // we must use the same setting for datatype selectors, since shared selectors // can appear in solutions - d_subOptions.datatypes.dtSharedSelectors = + d_subOptions.writeDatatypes().dtSharedSelectors = options().datatypes.dtSharedSelectors; - d_subOptions.datatypes.dtSharedSelectorsWasSetByUser = true; + d_subOptions.writeDatatypes().dtSharedSelectorsWasSetByUser = true; } SynthVerify::~SynthVerify() {} diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index f0e8d0be8..95e5faf6b 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -68,8 +68,8 @@ class TestNodeBlackNode : public TestNode TestNode::SetUp(); // setup an SMT engine so that options are in scope Options opts; - opts.base.outputLanguage = Language::LANG_AST; - opts.base.outputLanguageWasSetByUser = true; + opts.writeBase().outputLanguage = Language::LANG_AST; + opts.writeBase().outputLanguageWasSetByUser = true; d_slvEngine.reset(new SolverEngine(d_nodeManager, &opts)); } diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index 912e21147..da828a0cb 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -383,8 +383,8 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) { Options opts; // enable proofs - opts.smt.proofMode = options::ProofMode::FULL; - opts.smt.produceProofs = true; + opts.writeSmt().proofMode = options::ProofMode::FULL; + opts.writeSmt().produceProofs = true; Env env(NodeManager::currentNM(), &opts); opts.handler().setDefaultDagThresh("--dag-thresh", 0); smt::PfManager pfm(env); -- 2.30.2