From a932b4478e397d760d9457be7c6a80f9ba724391 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Jul 2020 15:10:51 -0500 Subject: [PATCH] Make use of options in setDefaults more consistent (#4729) The plan is to make setDefaults (the method to update the default options based on our internal heuristics) modify an explicit copy of options. This is the first step, which eliminates the dependence of this method on SmtEngine. This PR is furthermore required to eliminate options listeners. --- src/options/arith_options.toml | 1 - src/options/bv_options.toml | 1 - src/options/smt_options.toml | 1 - src/smt/set_defaults.cpp | 33 ++++++++++++++++----------------- src/smt/set_defaults.h | 19 +++++++++---------- src/smt/smt_engine.cpp | 2 +- 6 files changed, 26 insertions(+), 31 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index ce747b62d..a6c967dc9 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -425,7 +425,6 @@ header = "options/arith_options.h" long = "pb-rewrites" type = "bool" default = "false" - read_only = true help = "apply pseudo boolean rewrites" [[option]] diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 517d864d3..f7ec33f75 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -249,7 +249,6 @@ header = "options/bv_options.h" long = "bv-intro-pow2" type = "bool" default = "false" - read_only = true help = "introduce bitvector powers of two as a preprocessing pass" [[option]] diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 80183b71f..e4847716a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -395,7 +395,6 @@ header = "options/smt_options.h" long = "incremental" type = "bool" default = "true" - read_only = true help = "enable incremental solving" [[option]] diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 11751079e..8f6ab6c18 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -43,7 +43,7 @@ using namespace CVC4::theory; namespace CVC4 { namespace smt { -void setDefaults(SmtEngine& smte, LogicInfo& logic) +void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { // implied options if (options::debugCheckModels()) @@ -121,7 +121,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: setting bit-blast mode to lazy to support model" << "generation" << std::endl; - smte.setOption("bitblastMode", SExpr("lazy")); + options::bitblastMode.set(options::BitblastMode::LAZY); } else if (!options::incrementalSolving()) { @@ -289,7 +289,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } // sygus inference may require datatypes - if (!smte.isInternalSubsolver()) + if (!isInternalSubsolver) { if (options::produceAbducts() || options::produceInterpols() != options::ProduceInterpols::NONE @@ -325,7 +325,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { Notice() << "SmtEngine: turning on produce-assertions to support " << "option requiring assertions." << std::endl; - smte.setOption("produce-assertions", SExpr("true")); + options::produceAssertions.set(true); } // Disable options incompatible with incremental solving, unsat cores, and @@ -381,7 +381,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } } - if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { /** @@ -420,7 +419,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) Notice() << "SmtEngine: turning off pseudoboolean rewrites to support " "unsat cores/proofs" << std::endl; - smte.setOption("pb-rewrites", false); + options::pbRewrites.set(false); } if (options::sortInference()) @@ -473,7 +472,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) Notice() << "SmtEngine: turning off bool-to-bv to support unsat " "cores/proofs" << std::endl; - smte.setOption("boolToBitvector", SExpr("off")); + options::boolToBitvector.set(options::BoolToBVMode::OFF); } if (options::bvIntroducePow2()) @@ -486,7 +485,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) Notice() << "SmtEngine: turning off bv-intro-pow2 to support " "unsat-cores/proofs" << std::endl; - smte.setOption("bv-intro-pow2", false); + options::bvIntroducePow2.set(false); } if (options::repeatSimp()) @@ -499,7 +498,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) Notice() << "SmtEngine: turning off repeat-simp to support unsat " "cores/proofs" << std::endl; - smte.setOption("repeat-simp", false); + options::repeatSimp.set(false); } if (options::globalNegate()) @@ -512,7 +511,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) Notice() << "SmtEngine: turning off global-negate to support unsat " "cores/proofs" << std::endl; - smte.setOption("global-negate", false); + options::globalNegate.set(false); } if (options::bitvectorAig()) @@ -551,7 +550,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" << std::endl; - smte.setOption("boolToBitvector", SExpr("off")); + options::boolToBitvector.set(options::BoolToBVMode::OFF); } } @@ -561,7 +560,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << std::endl; - smte.setOption("produce-models", SExpr("true")); + options::produceModels.set(true); } ///////////////////////////////////////////////////////////////////////////// @@ -704,7 +703,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " << logic.getLogicString() << std::endl; - smte.setOption("boolToBitvector", SExpr("off")); + options::boolToBitvector.set(options::BoolToBVMode::OFF); } if (!options::bvEagerExplanations.wasSetByUser() @@ -1333,7 +1332,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) << "SmtEngine: turning off incremental solving mode (not yet " "supported with --proof, try --tear-down-incremental instead)" << std::endl; - smte.setOption("incremental", SExpr("false")); + options::incrementalSolving.set(false); } if (logic > LogicInfo("QF_AUFBVLRA")) { @@ -1433,7 +1432,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: turning off produce-models to support " << sOptNoModel << std::endl; - smte.setOption("produce-models", SExpr("false")); + options::produceModels.set(false); } if (options::produceAssignments()) { @@ -1446,7 +1445,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: turning off produce-assignments to support " << sOptNoModel << std::endl; - smte.setOption("produce-assignments", SExpr("false")); + options::produceAssignments.set(false); } if (options::checkModels()) { @@ -1459,7 +1458,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } Notice() << "SmtEngine: turning off check-models to support " << sOptNoModel << std::endl; - smte.setOption("check-models", SExpr("false")); + options::checkModels.set(false); } } diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index f3ec21c9b..606921b7c 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -15,7 +15,6 @@ #ifndef CVC4__SMT__SET_DEFAULTS_H #define CVC4__SMT__SET_DEFAULTS_H -#include "smt/smt_engine.h" #include "theory/logic_info.h" namespace CVC4 { @@ -23,18 +22,18 @@ namespace smt { /** * The purpose of this method is to set the default options and update the logic - * info for SMT engine smte. + * info for an SMT engine. * - * The argument logic is a reference to the logic of SmtEngine, which can be + * @param logic A reference to the logic of SmtEngine, which can be * updated by this method based on the current options and the logic itself. - * - * Note that currently, options are associated with the ExprManager. Thus, this - * call updates the options associated with the current ExprManager. - * If this designed is updated in the future so that SmtEngine has its own - * copy of options, this method should be updated accordingly so that it - * is responsible for updating this copy. + * @param isInternalSubsolver Whether we are setting the options for an + * internal subsolver (see SmtEngine::isInternalSubsolver). + * + * NOTE: we currently modify the current options in scope. This method + * can be further refactored to modify an options object provided as an + * explicit argument. */ -void setDefaults(SmtEngine& smte, LogicInfo& logic); +void setDefaults(LogicInfo& logic, bool isInternalSubsolver); } // namespace smt } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0d8189aa4..12e0f443e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -742,7 +742,7 @@ void SmtEngine::finishInit() Random::getRandom().setSeed(options::seed()); // ensure that our heuristics are properly set up - setDefaults(*this, d_logic); + setDefaults(d_logic, d_isInternalSubsolver); Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // We have mutual dependency here, so we add the prop engine to the theory -- 2.30.2