From a2d4f2cc2d546bd132e67f34301588d10dbd065b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Feb 2022 11:55:27 -0600 Subject: [PATCH] Standardizing notifications for setting options in set_defaults (#8057) --- src/smt/set_defaults.cpp | 89 ++++++++++++++++++---------------------- src/smt/set_defaults.h | 4 ++ 2 files changed, 44 insertions(+), 49 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 1fd2c3dc5..c3df86bf3 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -104,8 +104,8 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.unsatCoresModeWasSetByUser) { - verbose(1) - << "Overriding OFF unsat-core mode since cores were requested.\n"; + notifyModifyOption( + "unsatCoresMode", "assumptions", "enabling unsat cores"); } opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } @@ -120,8 +120,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.unsatCoresModeWasSetByUser) { - verbose(1) << "Forcing full-proof mode for unsat cores mode since proofs " - "were requested.\n"; + notifyModifyOption("unsatCoresMode", "full-proof", "enabling proofs"); } // enable unsat cores, because they are available as a consequence of proofs opts.smt.unsatCores = true; @@ -133,8 +132,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.produceProofsWasSetByUser) { - verbose(1) - << "Forcing proof production since new unsat cores were requested.\n"; + notifyModifyOption("produceProofs", "true", "enabling unsat cores"); } opts.smt.produceProofs = true; } @@ -151,8 +149,8 @@ void SetDefaults::setDefaultsPre(Options& opts) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - verbose(1) << "SolverEngine: turning off produce-proofs due to " - << reasonNoProofs.str() << "." << std::endl; + notifyModifyOption( + "produceProofs and unsatCores", "false", reasonNoProofs.str()); opts.smt.produceProofs = false; opts.smt.checkProofs = false; } @@ -200,9 +198,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const "for the combination of bit-vectors with arrays or uinterpreted " "functions. Try --bitblast=lazy")); } - verbose(1) - << "SolverEngine: setting bit-blast mode to lazy to support model" - << "generation" << std::endl; + notifyModifyOption("bitblastMode", "lazy", "model generation"); opts.bv.bitblastMode = options::BitblastMode::LAZY; } else if (!opts.base.incrementalSolving) @@ -259,8 +255,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(std::string( "Ackermannization currently does not support model generation.")); } - verbose(1) << "SolverEngine: turn off ackermannization to support model" - << "generation" << std::endl; + notifyModifyOption("ackermann", "false", "model generation"); opts.smt.ackermann = false; } @@ -950,9 +945,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "unconstrained simplification"; return true; } - verbose(1) << "SolverEngine: turning off unconstrained simplification to " - "support incremental solving" - << std::endl; + notifyModifyOption("unconstrainedSimp", "false", "incremental solving"); opts.smt.unconstrainedSimp = false; } if (opts.bv.bitblastMode == options::BitblastMode::EAGER @@ -969,9 +962,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inference"; return true; } - verbose(1) << "SolverEngine: turning off sygus inference to support " - "incremental solving" - << std::endl; + notifyModifyOption("sygusInference", "false", "incremental solving"); opts.quantifiers.sygusInference = false; } if (opts.quantifiers.sygusInst) @@ -981,9 +972,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inst"; return true; } - verbose(1) << "SolverEngine: turning off sygus inst to support " - "incremental solving" - << std::endl; + notifyModifyOption("sygusInst", "false", "incremental solving"); opts.quantifiers.sygusInst = false; } if (opts.smt.solveIntAsBV > 0) @@ -993,9 +982,12 @@ 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; + notifyModifyOption("globalNegate", "false", "incremental solving"); opts.quantifiers.globalNegate = false; + notifyModifyOption("cegqiNestedQE", "false", "incremental solving"); opts.quantifiers.cegqiNestedQE = false; opts.arith.arithMLTrick = false; @@ -1012,9 +1004,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "simplification"; return true; } - verbose(1) << "SolverEngine: turning off simplification to support unsat " - "cores" - << std::endl; + notifyModifyOption("simplificationMode", "none", "unsat cores"); opts.smt.simplificationMode = options::SimplificationMode::NONE; } @@ -1025,8 +1015,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "learned rewrites"; return true; } - verbose(1) << "SolverEngine: turning off learned rewrites to support " - "unsat cores\n"; + notifyModifyOption("learnedRewrite", "false", "unsat cores"); opts.smt.learnedRewrite = false; } @@ -1037,8 +1026,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pseudoboolean rewrites"; return true; } - verbose(1) << "SolverEngine: turning off pseudoboolean rewrites to support " - "unsat cores\n"; + notifyModifyOption("pbRewrites", "false", "unsat cores"); opts.arith.pbRewrites = false; } @@ -1049,8 +1037,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "sort inference"; return true; } - verbose(1) << "SolverEngine: turning off sort inference to support unsat " - "cores\n"; + notifyModifyOption("sortInference", "false", "unsat cores"); opts.smt.sortInference = false; } @@ -1061,8 +1048,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pre-skolemization"; return true; } - verbose(1) << "SolverEngine: turning off pre-skolemization to support " - "unsat cores\n"; + notifyModifyOption("preSkolemQuant", "false", "unsat cores"); opts.quantifiers.preSkolemQuant = false; } @@ -1073,8 +1059,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-to-bool"; return true; } - verbose(1) << "SolverEngine: turning off bitvector-to-bool to support " - "unsat cores\n"; + notifyModifyOption("bitvectorToBool", "false", "unsat cores"); opts.bv.bitvectorToBool = false; } @@ -1085,8 +1070,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bool-to-bv != off"; return true; } - verbose(1) - << "SolverEngine: turning off bool-to-bv to support unsat cores\n"; + notifyModifyOption("boolToBitvector", "off", "unsat cores"); opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } @@ -1097,8 +1081,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-intro-pow2"; return true; } - verbose(1) - << "SolverEngine: turning off bv-intro-pow2 to support unsat cores"; + notifyModifyOption("bvIntroducePow2", "false", "unsat cores"); opts.bv.bvIntroducePow2 = false; } @@ -1109,8 +1092,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "repeat-simp"; return true; } - verbose(1) - << "SolverEngine: turning off repeat-simp to support unsat cores\n"; + notifyModifyOption("repeatSimp", "false", "unsat cores"); opts.smt.repeatSimp = false; } @@ -1121,8 +1103,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "global-negate"; return true; } - verbose(1) << "SolverEngine: turning off global-negate to support unsat " - "cores\n"; + notifyModifyOption("globalNegate", "false", "unsat cores"); opts.quantifiers.globalNegate = false; } @@ -1138,9 +1119,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "unconstrained simplification"; return true; } - verbose(1) << "SolverEngine: turning off unconstrained simplification to " - "support unsat cores" - << std::endl; + notifyModifyOption("unconstrainedSimp", "false", "unsat cores"); opts.smt.unconstrainedSimp = false; } return false; @@ -1268,8 +1247,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // Allows to answer sat more often by default. if (!opts.quantifiers.fmfBoundWasSetByUser) { + notifyModifyOption("fmfBound", "true", "arrays-exp"); opts.quantifiers.fmfBound = true; - Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; } } if (logic.hasCardinalityConstraints()) @@ -1516,9 +1495,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const { if (!opts.quantifiers.sygus) { - Trace("smt") << "turning on sygus" << std::endl; + notifyModifyOption("sygus", "true", ""); + opts.quantifiers.sygus = true; } - opts.quantifiers.sygus = true; // must use Ferrante/Rackoff for real arithmetic if (!opts.quantifiers.cegqiMidpointWasSetByUser) { @@ -1728,5 +1707,17 @@ void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, << std::endl; } +void SetDefaults::notifyModifyOption(const std::string& x, + const std::string& val, + const std::string& reason) const +{ + verbose(1) << "SetDefaults: setting " << x << " to " << val; + if (!reason.empty()) + { + verbose(1) << " due to " << reason; + } + verbose(1) << std::endl; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 24b39e205..238e03b05 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -135,6 +135,10 @@ class SetDefaults : protected EnvObj * Set default decision mode */ void setDefaultDecisionMode(const LogicInfo& logic, Options& opts) const; + /** Notify that we are modifying option x to val due to reason. */ + void notifyModifyOption(const std::string& x, + const std::string& val, + const std::string& reason) const; /** Are we an internal subsolver? */ bool d_isInternalSubsolver; }; -- 2.30.2