This moves SmtEngine::setDefaults to its own file.
This design is not final. One could imagine this being a part of a "OptionsSetter" utility. I am leaving this as is until we refactor the relationship between SmtEngine and Options.
Regardless, the general file structure should be such that this method is separate from SmtEngine, since setting default options is a large task that should be addressed independently from the core of SmtEngine.
This is initial preparation towards converting the SmtEngine from Expr -> Node.
A few very minor changes were made to the code to make the separation possible.
smt/model_core_builder.h
smt/model_blocker.cpp
smt/model_blocker.h
+ smt/set_defaults.cpp
+ smt/set_defaults.h
smt/smt_engine.cpp
smt/smt_engine.h
smt/smt_engine_scope.cpp
--- /dev/null
+/********************* */
+/*! \file set_defaults.cpp
+ ** \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 Implementation of setting default options.
+ **/
+
+#include "smt/set_defaults.h"
+
+#include "base/output.h"
+#include "options/arith_options.h"
+#include "options/arrays_options.h"
+#include "options/base_options.h"
+#include "options/booleans_options.h"
+#include "options/bv_options.h"
+#include "options/datatypes_options.h"
+#include "options/decision_options.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/open_ostream.h"
+#include "options/option_exception.h"
+#include "options/printer_options.h"
+#include "options/proof_options.h"
+#include "options/prop_options.h"
+#include "options/quantifiers_options.h"
+#include "options/sep_options.h"
+#include "options/set_language.h"
+#include "options/smt_options.h"
+#include "options/strings_options.h"
+#include "options/theory_options.h"
+#include "options/uf_options.h"
+#include "theory/theory.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+void setDefaults(SmtEngine& smte, LogicInfo& logic)
+{
+ // Language-based defaults
+ if (!options::bitvectorDivByZeroConst.wasSetByUser())
+ {
+ // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
+ // set this option if the input format is SMT LIB 2.6. We also set this
+ // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
+ options::bitvectorDivByZeroConst.set(
+ language::isInputLang_smt2_6(options::inputLanguage())
+ || language::isInputLangSygus(options::inputLanguage()));
+ }
+ bool is_sygus = language::isInputLangSygus(options::inputLanguage());
+
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ if (options::produceModels()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_UF)))
+ {
+ if (options::bitblastMode.wasSetByUser()
+ || options::produceModels.wasSetByUser())
+ {
+ throw OptionException(std::string(
+ "Eager bit-blasting currently does not support model generation "
+ "for the combination of bit-vectors with arrays or uinterpreted "
+ "functions. Try --bitblast=lazy"));
+ }
+ Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
+ << "generation" << std::endl;
+ smte.setOption("bitblastMode", SExpr("lazy"));
+ }
+ else if (!options::incrementalSolving())
+ {
+ options::ackermann.set(true);
+ }
+
+ if (options::incrementalSolving() && !logic.isPure(THEORY_BV))
+ {
+ throw OptionException(
+ "Incremental eager bit-blasting is currently "
+ "only supported for QF_BV. Try --bitblast=lazy.");
+ }
+ }
+
+ if (options::solveIntAsBV() > 0)
+ {
+ logic = logic.getUnlockedCopy();
+ logic.enableTheory(THEORY_BV);
+ logic.lock();
+ }
+
+ if (options::solveBVAsInt() > 0)
+ {
+ if (logic.isTheoryEnabled(THEORY_BV))
+ {
+ logic = logic.getUnlockedCopy();
+ logic.enableTheory(THEORY_ARITH);
+ logic.arithNonLinear();
+ logic.lock();
+ }
+ }
+
+ // set options about ackermannization
+ if (options::ackermann() && options::produceModels()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_UF)))
+ {
+ if (options::produceModels.wasSetByUser())
+ {
+ throw OptionException(std::string(
+ "Ackermannization currently does not support model generation."));
+ }
+ Notice() << "SmtEngine: turn off ackermannization to support model"
+ << "generation" << std::endl;
+ options::ackermann.set(false);
+ }
+
+ if (options::ackermann())
+ {
+ if (options::incrementalSolving())
+ {
+ throw OptionException(
+ "Incremental Ackermannization is currently not supported.");
+ }
+
+ if (logic.isQuantified())
+ {
+ throw LogicException("Cannot use Ackermannization on quantified formula");
+ }
+
+ if (logic.isTheoryEnabled(THEORY_UF))
+ {
+ logic = logic.getUnlockedCopy();
+ logic.disableTheory(THEORY_UF);
+ logic.lock();
+ }
+ if (logic.isTheoryEnabled(THEORY_ARRAYS))
+ {
+ logic = logic.getUnlockedCopy();
+ logic.disableTheory(THEORY_ARRAYS);
+ logic.lock();
+ }
+ }
+
+ // Set default options associated with strings-exp. We also set these options
+ // if we are using eager string preprocessing, which may introduce quantified
+ // formulas at preprocess time.
+ if (options::stringExp() || !options::stringLazyPreproc())
+ {
+ // We require quantifiers since extended functions reduce using them.
+ if (!logic.isQuantified())
+ {
+ logic = logic.getUnlockedCopy();
+ logic.enableQuantifiers();
+ logic.lock();
+ Trace("smt") << "turning on quantifier logic, for strings-exp"
+ << std::endl;
+ }
+ // We require bounded quantifier handling.
+ if (!options::fmfBound.wasSetByUser())
+ {
+ options::fmfBound.set(true);
+ Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
+ }
+ // Turn off E-matching, since some bounded quantifiers introduced by strings
+ // (e.g. for replaceall) admit matching loops.
+ if (!options::eMatching.wasSetByUser())
+ {
+ options::eMatching.set(false);
+ Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
+ }
+ // Do not eliminate extended arithmetic symbols from quantified formulas,
+ // since some strategies, e.g. --re-elim-agg, introduce them.
+ if (!options::elimExtArithQuant.wasSetByUser())
+ {
+ options::elimExtArithQuant.set(false);
+ Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
+ << std::endl;
+ }
+ }
+
+ // sygus inference may require datatypes
+ if (!smte.isInternalSubsolver())
+ {
+ if (options::produceAbducts() || options::sygusInference()
+ || options::sygusRewSynthInput())
+ {
+ // since we are trying to recast as sygus, we assume the input is sygus
+ is_sygus = true;
+ }
+ }
+
+ // We now know whether the input is sygus. Update the logic to incorporate
+ // the theories we need internally for handling sygus problems.
+ if (is_sygus)
+ {
+ logic = logic.getUnlockedCopy();
+ logic.enableSygus();
+ logic.lock();
+ }
+
+ // sygus core connective requires unsat cores
+ if (options::sygusCoreConnective())
+ {
+ options::unsatCores.set(true);
+ }
+
+ if ((options::checkModels() || options::checkSynthSol()
+ || options::produceAbducts()
+ || options::modelCoresMode() != options::ModelCoresMode::NONE
+ || options::blockModelsMode() != options::BlockModelsMode::NONE)
+ && !options::produceAssertions())
+ {
+ Notice() << "SmtEngine: turning on produce-assertions to support "
+ << "option requiring assertions." << std::endl;
+ smte.setOption("produce-assertions", SExpr("true"));
+ }
+
+ // Disable options incompatible with incremental solving, unsat cores, and
+ // proofs or output an error if enabled explicitly
+ if (options::incrementalSolving() || options::unsatCores()
+ || options::proof())
+ {
+ if (options::unconstrainedSimp())
+ {
+ if (options::unconstrainedSimp.wasSetByUser())
+ {
+ throw OptionException(
+ "unconstrained simplification not supported with unsat "
+ "cores/proofs/incremental solving");
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to "
+ "support unsat cores/proofs/incremental solving"
+ << std::endl;
+ options::unconstrainedSimp.set(false);
+ }
+ }
+ else
+ {
+ // Turn on unconstrained simplification for QF_AUFBV
+ if (!options::unconstrainedSimp.wasSetByUser())
+ {
+ bool uncSimp = !logic.isQuantified() && !options::produceModels()
+ && !options::produceAssignments()
+ && !options::checkModels()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_BV));
+ Trace("smt") << "setting unconstrained simplification to " << uncSimp
+ << std::endl;
+ options::unconstrainedSimp.set(uncSimp);
+ }
+ }
+
+ if (options::incrementalSolving() || options::proof())
+ {
+ if (options::sygusInference())
+ {
+ if (options::sygusInference.wasSetByUser())
+ {
+ throw OptionException(
+ "sygus inference not supported with proofs/incremental solving");
+ }
+ Notice() << "SmtEngine: turning off sygus inference to support "
+ "proofs/incremental solving"
+ << std::endl;
+ options::sygusInference.set(false);
+ }
+ }
+
+ // Disable options incompatible with unsat cores and proofs or output an
+ // error if enabled explicitly
+ if (options::unsatCores() || options::proof())
+ {
+ if (options::simplificationMode() != options::SimplificationMode::NONE)
+ {
+ if (options::simplificationMode.wasSetByUser())
+ {
+ throw OptionException(
+ "simplification not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off simplification to support unsat "
+ "cores/proofs"
+ << std::endl;
+ options::simplificationMode.set(options::SimplificationMode::NONE);
+ }
+
+ if (options::pbRewrites())
+ {
+ if (options::pbRewrites.wasSetByUser())
+ {
+ throw OptionException(
+ "pseudoboolean rewrites not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+ "unsat cores/proofs"
+ << std::endl;
+ smte.setOption("pb-rewrites", false);
+ }
+
+ if (options::sortInference())
+ {
+ if (options::sortInference.wasSetByUser())
+ {
+ throw OptionException(
+ "sort inference not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off sort inference to support unsat "
+ "cores/proofs"
+ << std::endl;
+ options::sortInference.set(false);
+ }
+
+ if (options::preSkolemQuant())
+ {
+ if (options::preSkolemQuant.wasSetByUser())
+ {
+ throw OptionException(
+ "pre-skolemization not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
+ "cores/proofs"
+ << std::endl;
+ options::preSkolemQuant.set(false);
+ }
+
+ if (options::solveBVAsInt() > 0)
+ {
+ /**
+ * Operations on 1 bits are better handled as Boolean operations
+ * than as integer operations.
+ * Therefore, we enable bv-to-bool, which runs before
+ * the translation to integers.
+ */
+ options::bitvectorToBool.set(true);
+ }
+
+ if (options::bitvectorToBool())
+ {
+ if (options::bitvectorToBool.wasSetByUser())
+ {
+ throw OptionException(
+ "bv-to-bool not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
+ "cores/proofs"
+ << std::endl;
+ options::bitvectorToBool.set(false);
+ }
+
+ if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+ {
+ if (options::boolToBitvector.wasSetByUser())
+ {
+ throw OptionException(
+ "bool-to-bv != off not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
+ "cores/proofs"
+ << std::endl;
+ smte.setOption("boolToBitvector", SExpr("off"));
+ }
+
+ if (options::bvIntroducePow2())
+ {
+ if (options::bvIntroducePow2.wasSetByUser())
+ {
+ throw OptionException(
+ "bv-intro-pow2 not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
+ "unsat-cores/proofs"
+ << std::endl;
+ smte.setOption("bv-intro-pow2", false);
+ }
+
+ if (options::repeatSimp())
+ {
+ if (options::repeatSimp.wasSetByUser())
+ {
+ throw OptionException(
+ "repeat-simp not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off repeat-simp to support unsat "
+ "cores/proofs"
+ << std::endl;
+ smte.setOption("repeat-simp", false);
+ }
+
+ if (options::globalNegate())
+ {
+ if (options::globalNegate.wasSetByUser())
+ {
+ throw OptionException(
+ "global-negate not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off global-negate to support unsat "
+ "cores/proofs"
+ << std::endl;
+ smte.setOption("global-negate", false);
+ }
+
+ if (options::bitvectorAig())
+ {
+ throw OptionException(
+ "bitblast-aig not supported with unsat cores/proofs");
+ }
+ }
+ else
+ {
+ // by default, nonclausal simplification is off for QF_SAT
+ if (!options::simplificationMode.wasSetByUser())
+ {
+ bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
+ Trace("smt") << "setting simplification mode to <"
+ << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+ // simplification=none works better for SMT LIB benchmarks with
+ // quantifiers, not others options::simplificationMode.set(qf_sat ||
+ // quantifiers ? options::SimplificationMode::NONE :
+ // options::SimplificationMode::BATCH);
+ options::simplificationMode.set(qf_sat
+ ? options::SimplificationMode::NONE
+ : options::SimplificationMode::BATCH);
+ }
+ }
+
+ if (options::cbqiBv() && logic.isQuantified())
+ {
+ if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+ {
+ if (options::boolToBitvector.wasSetByUser())
+ {
+ throw OptionException(
+ "bool-to-bv != off not supported with CBQI BV for quantified "
+ "logics");
+ }
+ Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
+ << std::endl;
+ smte.setOption("boolToBitvector", SExpr("off"));
+ }
+ }
+
+ // cases where we need produce models
+ if (!options::produceModels()
+ && (options::produceAssignments() || options::sygusRewSynthCheck()
+ || is_sygus))
+ {
+ Notice() << "SmtEngine: turning on produce-models" << std::endl;
+ smte.setOption("produce-models", SExpr("true"));
+ }
+
+ // Set the options for the theoryOf
+ if (!options::theoryOfMode.wasSetByUser())
+ {
+ if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
+ && !logic.isTheoryEnabled(THEORY_STRINGS)
+ && !logic.isTheoryEnabled(THEORY_SETS))
+ {
+ Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
+ options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+ }
+ }
+
+ // strings require LIA, UF; widen the logic
+ if (logic.isTheoryEnabled(THEORY_STRINGS))
+ {
+ LogicInfo log(logic.getUnlockedCopy());
+ // Strings requires arith for length constraints, and also UF
+ if (!logic.isTheoryEnabled(THEORY_UF))
+ {
+ Trace("smt") << "because strings are enabled, also enabling UF"
+ << std::endl;
+ log.enableTheory(THEORY_UF);
+ }
+ if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()
+ || !logic.areIntegersUsed())
+ {
+ Trace("smt") << "because strings are enabled, also enabling linear "
+ "integer arithmetic"
+ << std::endl;
+ log.enableTheory(THEORY_ARITH);
+ log.enableIntegers();
+ log.arithOnlyLinear();
+ }
+ logic = log;
+ logic.lock();
+ }
+ if (logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_DATATYPES)
+ || logic.isTheoryEnabled(THEORY_SETS))
+ {
+ if (!logic.isTheoryEnabled(THEORY_UF))
+ {
+ LogicInfo log(logic.getUnlockedCopy());
+ Trace("smt") << "because a theory that permits Boolean terms is enabled, "
+ "also enabling UF"
+ << std::endl;
+ log.enableTheory(THEORY_UF);
+ logic = log;
+ logic.lock();
+ }
+ }
+
+ // by default, symmetry breaker is on only for non-incremental QF_UF
+ if (!options::ufSymmetryBreaker.wasSetByUser())
+ {
+ bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
+ && !options::incrementalSolving() && !options::proof()
+ && !options::unsatCores();
+ Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
+ << std::endl;
+ options::ufSymmetryBreaker.set(qf_uf_noinc);
+ }
+
+ // If in arrays, set the UF handler to arrays
+ if (logic.isTheoryEnabled(THEORY_ARRAYS)
+ && (!logic.isQuantified()
+ || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
+ {
+ Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
+ }
+ else
+ {
+ Theory::setUninterpretedSortOwner(THEORY_UF);
+ }
+
+ if (!options::simplifyWithCareEnabled.wasSetByUser())
+ {
+ bool qf_aufbv =
+ !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV);
+
+ bool withCare = qf_aufbv;
+ Trace("smt") << "setting ite simplify with care to " << withCare
+ << std::endl;
+ options::simplifyWithCareEnabled.set(withCare);
+ }
+ // Turn off array eager index splitting for QF_AUFLIA
+ if (!options::arraysEagerIndexSplitting.wasSetByUser())
+ {
+ if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_ARITH))
+ {
+ Trace("smt") << "setting array eager index splitting to false"
+ << std::endl;
+ options::arraysEagerIndexSplitting.set(false);
+ }
+ }
+ // Turn on multiple-pass non-clausal simplification for QF_AUFBV
+ if (!options::repeatSimp.wasSetByUser())
+ {
+ bool repeatSimp = !logic.isQuantified()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_BV))
+ && !options::unsatCores();
+ Trace("smt") << "setting repeat simplification to " << repeatSimp
+ << std::endl;
+ options::repeatSimp.set(repeatSimp);
+ }
+
+ if (options::boolToBitvector() == options::BoolToBVMode::ALL
+ && !logic.isTheoryEnabled(THEORY_BV))
+ {
+ if (options::boolToBitvector.wasSetByUser())
+ {
+ throw OptionException(
+ "bool-to-bv=all not supported for non-bitvector logics.");
+ }
+ Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
+ << logic.getLogicString() << std::endl;
+ smte.setOption("boolToBitvector", SExpr("off"));
+ }
+
+ if (!options::bvEagerExplanations.wasSetByUser()
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_BV))
+ {
+ Trace("smt") << "enabling eager bit-vector explanations " << std::endl;
+ options::bvEagerExplanations.set(true);
+ }
+
+ // Turn on arith rewrite equalities only for pure arithmetic
+ if (!options::arithRewriteEq.wasSetByUser())
+ {
+ bool arithRewriteEq =
+ logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
+ Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
+ << std::endl;
+ options::arithRewriteEq.set(arithRewriteEq);
+ }
+ if (!options::arithHeuristicPivots.wasSetByUser())
+ {
+ int16_t heuristicPivots = 5;
+ if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+ {
+ if (logic.isDifferenceLogic())
+ {
+ heuristicPivots = -1;
+ }
+ else if (!logic.areIntegersUsed())
+ {
+ heuristicPivots = 0;
+ }
+ }
+ Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
+ << std::endl;
+ options::arithHeuristicPivots.set(heuristicPivots);
+ }
+ if (!options::arithPivotThreshold.wasSetByUser())
+ {
+ uint16_t pivotThreshold = 2;
+ if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+ {
+ if (logic.isDifferenceLogic())
+ {
+ pivotThreshold = 16;
+ }
+ }
+ Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
+ << std::endl;
+ options::arithPivotThreshold.set(pivotThreshold);
+ }
+ if (!options::arithStandardCheckVarOrderPivots.wasSetByUser())
+ {
+ int16_t varOrderPivots = -1;
+ if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+ {
+ varOrderPivots = 200;
+ }
+ Trace("smt") << "setting arithStandardCheckVarOrderPivots "
+ << varOrderPivots << std::endl;
+ options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
+ }
+ if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
+ {
+ if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+ {
+ Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
+ << std::endl;
+ options::nlExtTangentPlanesInterleave.set(true);
+ }
+ }
+
+ // Set decision mode based on logic (if not set by user)
+ if (!options::decisionMode.wasSetByUser())
+ {
+ options::DecisionMode decMode =
+ // sygus uses internal
+ is_sygus ? options::DecisionMode::INTERNAL :
+ // ALL
+ logic.hasEverything()
+ ? options::DecisionMode::JUSTIFICATION
+ : ( // QF_BV
+ (not logic.isQuantified() && logic.isPure(THEORY_BV)) ||
+ // QF_AUFBV or QF_ABV or QF_UFBV
+ (not logic.isQuantified()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_UF))
+ && logic.isTheoryEnabled(THEORY_BV))
+ ||
+ // QF_AUFLIA (and may be ends up enabling
+ // QF_AUFLRA?)
+ (not logic.isQuantified()
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_ARITH))
+ ||
+ // QF_LRA
+ (not logic.isQuantified()
+ && logic.isPure(THEORY_ARITH) && logic.isLinear()
+ && !logic.isDifferenceLogic()
+ && !logic.areIntegersUsed())
+ ||
+ // Quantifiers
+ logic.isQuantified() ||
+ // Strings
+ logic.isTheoryEnabled(THEORY_STRINGS)
+ ? options::DecisionMode::JUSTIFICATION
+ : options::DecisionMode::INTERNAL);
+
+ bool stoponly =
+ // ALL
+ logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
+ ? false
+ : ( // QF_AUFLIA
+ (not logic.isQuantified()
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_ARITH))
+ ||
+ // QF_LRA
+ (not logic.isQuantified()
+ && logic.isPure(THEORY_ARITH) && logic.isLinear()
+ && !logic.isDifferenceLogic()
+ && !logic.areIntegersUsed())
+ ? true
+ : false);
+
+ Trace("smt") << "setting decision mode to " << decMode << std::endl;
+ options::decisionMode.set(decMode);
+ options::decisionStopOnly.set(stoponly);
+ }
+ if (options::incrementalSolving())
+ {
+ // disable modes not supported by incremental
+ options::sortInference.set(false);
+ options::ufssFairnessMonotone.set(false);
+ options::quantEpr.set(false);
+ options::globalNegate.set(false);
+ }
+ if (logic.hasCardinalityConstraints())
+ {
+ // must have finite model finding on
+ options::finiteModelFind.set(true);
+ }
+
+ // if it contains a theory with non-termination, do not strictly enforce that
+ // quantifiers and theory combination must be interleaved
+ if (logic.isTheoryEnabled(THEORY_STRINGS)
+ || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
+ {
+ if (!options::instWhenStrictInterleave.wasSetByUser())
+ {
+ options::instWhenStrictInterleave.set(false);
+ }
+ }
+
+ if (options::instMaxLevel() != -1)
+ {
+ Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
+ << std::endl;
+ options::cbqi.set(false);
+ }
+ // Do we need to track instantiations?
+ // Needed for sygus due to single invocation techniques.
+ if (options::cbqiNestedQE()
+ || (options::proof() && !options::trackInstLemmas.wasSetByUser())
+ || is_sygus)
+ {
+ options::trackInstLemmas.set(true);
+ }
+
+ if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy())
+ || (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt()))
+ {
+ options::fmfBound.set(true);
+ }
+ // now have determined whether fmfBoundInt is on/off
+ // apply fmfBoundInt options
+ if (options::fmfBound())
+ {
+ if (!options::mbqiMode.wasSetByUser()
+ || (options::mbqiMode() != options::MbqiMode::NONE
+ && options::mbqiMode() != options::MbqiMode::FMC))
+ {
+ // if bounded integers are set, use no MBQI by default
+ options::mbqiMode.set(options::MbqiMode::NONE);
+ }
+ if (!options::prenexQuant.wasSetByUser())
+ {
+ options::prenexQuant.set(options::PrenexQuantMode::NONE);
+ }
+ }
+ if (options::ufHo())
+ {
+ // if higher-order, then current variants of model-based instantiation
+ // cannot be used
+ if (options::mbqiMode() != options::MbqiMode::NONE)
+ {
+ options::mbqiMode.set(options::MbqiMode::NONE);
+ }
+ if (!options::hoElimStoreAx.wasSetByUser())
+ {
+ // by default, use store axioms only if --ho-elim is set
+ options::hoElimStoreAx.set(options::hoElim());
+ }
+ }
+ if (options::fmfFunWellDefinedRelevant())
+ {
+ if (!options::fmfFunWellDefined.wasSetByUser())
+ {
+ options::fmfFunWellDefined.set(true);
+ }
+ }
+ if (options::fmfFunWellDefined())
+ {
+ if (!options::finiteModelFind.wasSetByUser())
+ {
+ options::finiteModelFind.set(true);
+ }
+ }
+ // EPR
+ if (options::quantEpr())
+ {
+ if (!options::preSkolemQuant.wasSetByUser())
+ {
+ options::preSkolemQuant.set(true);
+ }
+ }
+
+ // now, have determined whether finite model find is on/off
+ // apply finite model finding options
+ if (options::finiteModelFind())
+ {
+ // apply conservative quantifiers splitting
+ if (!options::quantDynamicSplit.wasSetByUser())
+ {
+ options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
+ }
+ // do not eliminate extended arithmetic symbols from quantified formulas
+ if (!options::elimExtArithQuant.wasSetByUser())
+ {
+ options::elimExtArithQuant.set(false);
+ }
+ if (!options::eMatching.wasSetByUser())
+ {
+ options::eMatching.set(options::fmfInstEngine());
+ }
+ if (!options::instWhenMode.wasSetByUser())
+ {
+ // instantiate only on last call
+ if (options::eMatching())
+ {
+ options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+ }
+ }
+ }
+
+ // apply sygus options
+ // if we are attempting to rewrite everything to SyGuS, use sygus()
+ if (is_sygus)
+ {
+ if (!options::sygus())
+ {
+ Trace("smt") << "turning on sygus" << std::endl;
+ }
+ options::sygus.set(true);
+ // must use Ferrante/Rackoff for real arithmetic
+ if (!options::cbqiMidpoint.wasSetByUser())
+ {
+ options::cbqiMidpoint.set(true);
+ }
+ if (options::sygusRepairConst())
+ {
+ if (!options::cbqi.wasSetByUser())
+ {
+ options::cbqi.set(true);
+ }
+ }
+ if (options::sygusInference())
+ {
+ // optimization: apply preskolemization, makes it succeed more often
+ if (!options::preSkolemQuant.wasSetByUser())
+ {
+ options::preSkolemQuant.set(true);
+ }
+ if (!options::preSkolemQuantNested.wasSetByUser())
+ {
+ options::preSkolemQuantNested.set(true);
+ }
+ }
+ // counterexample-guided instantiation for sygus
+ if (!options::cegqiSingleInvMode.wasSetByUser())
+ {
+ options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
+ }
+ if (!options::quantConflictFind.wasSetByUser())
+ {
+ options::quantConflictFind.set(false);
+ }
+ if (!options::instNoEntail.wasSetByUser())
+ {
+ options::instNoEntail.set(false);
+ }
+ if (!options::cbqiFullEffort.wasSetByUser())
+ {
+ // should use full effort cbqi for single invocation and repair const
+ options::cbqiFullEffort.set(true);
+ }
+ if (options::sygusRew())
+ {
+ options::sygusRewSynth.set(true);
+ options::sygusRewVerify.set(true);
+ }
+ if (options::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.
+ options::sygusRewSynth.set(true);
+ // we should not use the extended rewriter, since we are interested
+ // in rewrites that are not in the main rewriter
+ if (!options::sygusExtRew.wasSetByUser())
+ {
+ options::sygusExtRew.set(false);
+ }
+ }
+ // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
+ // is one that is specialized for returning a single solution. Non-basic
+ // sygus algorithms currently include the PBE solver, UNIF+PI, static
+ // template inference for invariant synthesis, and single invocation
+ // techniques.
+ bool reqBasicSygus = false;
+ if (options::produceAbducts())
+ {
+ // if doing abduction, we should filter strong solutions
+ if (!options::sygusFilterSolMode.wasSetByUser())
+ {
+ options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
+ }
+ // we must use basic sygus algorithms, since e.g. we require checking
+ // a sygus side condition for consistency with axioms.
+ reqBasicSygus = true;
+ }
+ if (options::sygusRewSynth() || options::sygusRewVerify()
+ || options::sygusQueryGen())
+ {
+ // rewrite rule synthesis implies that sygus stream must be true
+ options::sygusStream.set(true);
+ }
+ if (options::sygusStream() || options::incrementalSolving())
+ {
+ // Streaming and incremental mode are incompatible with techniques that
+ // focus the search towards finding a single solution.
+ reqBasicSygus = true;
+ }
+ // Now, disable options for non-basic sygus algorithms, if necessary.
+ if (reqBasicSygus)
+ {
+ if (!options::sygusUnifPbe.wasSetByUser())
+ {
+ options::sygusUnifPbe.set(false);
+ }
+ if (options::sygusUnifPi.wasSetByUser())
+ {
+ options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
+ }
+ if (!options::sygusInvTemplMode.wasSetByUser())
+ {
+ options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
+ }
+ if (!options::cegqiSingleInvMode.wasSetByUser())
+ {
+ options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
+ }
+ }
+ // do not allow partial functions
+ if (!options::bitvectorDivByZeroConst())
+ {
+ if (options::bitvectorDivByZeroConst.wasSetByUser())
+ {
+ throw OptionException(
+ "--no-bv-div-zero-const is not supported with SyGuS");
+ }
+ Notice()
+ << "SmtEngine: setting bv-div-zero-const to true to support SyGuS"
+ << std::endl;
+ options::bitvectorDivByZeroConst.set(true);
+ }
+ if (!options::dtRewriteErrorSel.wasSetByUser())
+ {
+ options::dtRewriteErrorSel.set(true);
+ }
+ // do not miniscope
+ if (!options::miniscopeQuant.wasSetByUser())
+ {
+ options::miniscopeQuant.set(false);
+ }
+ if (!options::miniscopeQuantFreeVar.wasSetByUser())
+ {
+ options::miniscopeQuantFreeVar.set(false);
+ }
+ if (!options::quantSplit.wasSetByUser())
+ {
+ options::quantSplit.set(false);
+ }
+ // rewrite divk
+ if (!options::rewriteDivk.wasSetByUser())
+ {
+ options::rewriteDivk.set(true);
+ }
+ // do not do macros
+ if (!options::macrosQuant.wasSetByUser())
+ {
+ options::macrosQuant.set(false);
+ }
+ if (!options::cbqiPreRegInst.wasSetByUser())
+ {
+ options::cbqiPreRegInst.set(true);
+ }
+ }
+ // counterexample-guided instantiation for non-sygus
+ // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
+ if ((logic.isQuantified()
+ && (logic.isTheoryEnabled(THEORY_ARITH)
+ || logic.isTheoryEnabled(THEORY_DATATYPES)
+ || logic.isTheoryEnabled(THEORY_BV)
+ || logic.isTheoryEnabled(THEORY_FP)))
+ || options::cbqiAll())
+ {
+ if (!options::cbqi.wasSetByUser())
+ {
+ options::cbqi.set(true);
+ }
+ // check whether we should apply full cbqi
+ if (logic.isPure(THEORY_BV))
+ {
+ if (!options::cbqiFullEffort.wasSetByUser())
+ {
+ options::cbqiFullEffort.set(true);
+ }
+ }
+ }
+ if (options::cbqi())
+ {
+ // must rewrite divk
+ if (!options::rewriteDivk.wasSetByUser())
+ {
+ options::rewriteDivk.set(true);
+ }
+ if (options::incrementalSolving())
+ {
+ // cannot do nested quantifier elimination in incremental mode
+ options::cbqiNestedQE.set(false);
+ }
+ if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
+ {
+ if (!options::quantConflictFind.wasSetByUser())
+ {
+ options::quantConflictFind.set(false);
+ }
+ if (!options::instNoEntail.wasSetByUser())
+ {
+ options::instNoEntail.set(false);
+ }
+ if (!options::instWhenMode.wasSetByUser() && options::cbqiModel())
+ {
+ // only instantiation should happen at last call when model is avaiable
+ options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+ }
+ }
+ else
+ {
+ // only supported in pure arithmetic or pure BV
+ options::cbqiNestedQE.set(false);
+ }
+ // prenexing
+ if (options::cbqiNestedQE())
+ {
+ // only complete with prenex = disj_normal or normal
+ if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
+ {
+ options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL);
+ }
+ }
+ else if (options::globalNegate())
+ {
+ if (!options::prenexQuant.wasSetByUser())
+ {
+ options::prenexQuant.set(options::PrenexQuantMode::NONE);
+ }
+ }
+ }
+ // implied options...
+ if (options::strictTriggers())
+ {
+ if (!options::userPatternsQuant.wasSetByUser())
+ {
+ options::userPatternsQuant.set(options::UserPatMode::TRUST);
+ }
+ }
+ if (options::qcfMode.wasSetByUser() || options::qcfTConstraint())
+ {
+ options::quantConflictFind.set(true);
+ }
+ if (options::cbqiNestedQE())
+ {
+ options::prenexQuantUser.set(true);
+ if (!options::preSkolemQuant.wasSetByUser())
+ {
+ options::preSkolemQuant.set(true);
+ }
+ }
+ // for induction techniques
+ if (options::quantInduction())
+ {
+ if (!options::dtStcInduction.wasSetByUser())
+ {
+ options::dtStcInduction.set(true);
+ }
+ if (!options::intWfInduction.wasSetByUser())
+ {
+ options::intWfInduction.set(true);
+ }
+ }
+ if (options::dtStcInduction())
+ {
+ // try to remove ITEs from quantified formulas
+ if (!options::iteDtTesterSplitQuant.wasSetByUser())
+ {
+ options::iteDtTesterSplitQuant.set(true);
+ }
+ if (!options::iteLiftQuant.wasSetByUser())
+ {
+ options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
+ }
+ }
+ if (options::intWfInduction())
+ {
+ if (!options::purifyTriggers.wasSetByUser())
+ {
+ options::purifyTriggers.set(true);
+ }
+ }
+ if (options::conjectureNoFilter())
+ {
+ if (!options::conjectureFilterActiveTerms.wasSetByUser())
+ {
+ options::conjectureFilterActiveTerms.set(false);
+ }
+ if (!options::conjectureFilterCanonical.wasSetByUser())
+ {
+ options::conjectureFilterCanonical.set(false);
+ }
+ if (!options::conjectureFilterModel.wasSetByUser())
+ {
+ options::conjectureFilterModel.set(false);
+ }
+ }
+ if (options::conjectureGenPerRound.wasSetByUser())
+ {
+ if (options::conjectureGenPerRound() > 0)
+ {
+ options::conjectureGen.set(true);
+ }
+ else
+ {
+ options::conjectureGen.set(false);
+ }
+ }
+ // can't pre-skolemize nested quantifiers without UF theory
+ if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
+ {
+ if (!options::preSkolemQuantNested.wasSetByUser())
+ {
+ options::preSkolemQuantNested.set(false);
+ }
+ }
+ if (!logic.isTheoryEnabled(THEORY_DATATYPES))
+ {
+ options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
+ }
+
+ // until bugs 371,431 are fixed
+ if (!options::minisatUseElim.wasSetByUser())
+ {
+ // cannot use minisat elimination for logics where a theory solver
+ // introduces new literals into the search. This includes quantifiers
+ // (quantifier instantiation), and the lemma schemas used in non-linear
+ // and sets. We also can't use it if models are enabled.
+ if (logic.isTheoryEnabled(THEORY_SETS) || logic.isQuantified()
+ || options::produceModels() || options::produceAssignments()
+ || options::checkModels()
+ || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
+ {
+ options::minisatUseElim.set(false);
+ }
+ }
+
+ // For now, these array theory optimizations do not support model-building
+ if (options::produceModels() || options::produceAssignments()
+ || options::checkModels())
+ {
+ options::arraysOptimizeLinear.set(false);
+ options::arraysLazyRIntro1.set(false);
+ }
+
+ if (options::proof())
+ {
+ if (options::incrementalSolving())
+ {
+ if (options::incrementalSolving.wasSetByUser())
+ {
+ throw OptionException("--incremental is not supported with proofs");
+ }
+ Warning()
+ << "SmtEngine: turning off incremental solving mode (not yet "
+ "supported with --proof, try --tear-down-incremental instead)"
+ << std::endl;
+ smte.setOption("incremental", SExpr("false"));
+ }
+ if (logic > LogicInfo("QF_AUFBVLRA"))
+ {
+ throw OptionException(
+ "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
+ }
+ if (options::bitvectorAlgebraicSolver())
+ {
+ if (options::bitvectorAlgebraicSolver.wasSetByUser())
+ {
+ throw OptionException(
+ "--bv-algebraic-solver is not supported with proofs");
+ }
+ Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
+ << std::endl;
+ options::bitvectorAlgebraicSolver.set(false);
+ }
+ if (options::bitvectorEqualitySolver())
+ {
+ if (options::bitvectorEqualitySolver.wasSetByUser())
+ {
+ throw OptionException("--bv-eq-solver is not supported with proofs");
+ }
+ Notice() << "SmtEngine: turning off bv eq solver to support proofs"
+ << std::endl;
+ options::bitvectorEqualitySolver.set(false);
+ }
+ if (options::bitvectorInequalitySolver())
+ {
+ if (options::bitvectorInequalitySolver.wasSetByUser())
+ {
+ throw OptionException(
+ "--bv-inequality-solver is not supported with proofs");
+ }
+ Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
+ << std::endl;
+ options::bitvectorInequalitySolver.set(false);
+ }
+ }
+
+ if (!options::bitvectorEqualitySolver())
+ {
+ if (options::bvLazyRewriteExtf())
+ {
+ if (options::bvLazyRewriteExtf.wasSetByUser())
+ {
+ throw OptionException(
+ "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
+ }
+ }
+ Trace("smt")
+ << "disabling bvLazyRewriteExtf since equality solver is disabled"
+ << std::endl;
+ options::bvLazyRewriteExtf.set(false);
+ }
+
+ if (!options::sygusExprMinerCheckUseExport())
+ {
+ if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+ {
+ throw OptionException(
+ "--sygus-expr-miner-check-timeout=N requires "
+ "--sygus-expr-miner-check-use-export");
+ }
+ if (options::sygusRewSynthInput() || options::produceAbducts())
+ {
+ std::stringstream ss;
+ ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
+ : "--produce-abducts");
+ ss << "requires --sygus-expr-miner-check-use-export";
+ throw OptionException(ss.str());
+ }
+ }
+
+ if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
+ {
+ Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
+ "--strings-fmf enabled"
+ << std::endl;
+ options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
+ }
+
+ // !!! All options that require disabling models go here
+ bool disableModels = false;
+ std::string sOptNoModel;
+ if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
+ {
+ disableModels = true;
+ sOptNoModel = "unconstrained-simp";
+ }
+ else if (options::sortInference())
+ {
+ disableModels = true;
+ sOptNoModel = "sort-inference";
+ }
+ else if (options::minisatUseElim())
+ {
+ disableModels = true;
+ sOptNoModel = "minisat-elimination";
+ }
+ else if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+ && !options::nlExt())
+ {
+ disableModels = true;
+ sOptNoModel = "nonlinear arithmetic without nl-ext";
+ }
+ else if (options::globalNegate())
+ {
+ disableModels = true;
+ sOptNoModel = "global-negate";
+ }
+ if (disableModels)
+ {
+ if (options::produceModels())
+ {
+ if (options::produceModels.wasSetByUser())
+ {
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel << " with model generation.";
+ throw OptionException(ss.str());
+ }
+ Notice() << "SmtEngine: turning off produce-models to support "
+ << sOptNoModel << std::endl;
+ smte.setOption("produce-models", SExpr("false"));
+ }
+ if (options::produceAssignments())
+ {
+ if (options::produceAssignments.wasSetByUser())
+ {
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel
+ << " with model generation (produce-assignments).";
+ throw OptionException(ss.str());
+ }
+ Notice() << "SmtEngine: turning off produce-assignments to support "
+ << sOptNoModel << std::endl;
+ smte.setOption("produce-assignments", SExpr("false"));
+ }
+ if (options::checkModels())
+ {
+ if (options::checkModels.wasSetByUser())
+ {
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel
+ << " with model generation (check-models).";
+ throw OptionException(ss.str());
+ }
+ Notice() << "SmtEngine: turning off check-models to support "
+ << sOptNoModel << std::endl;
+ smte.setOption("check-models", SExpr("false"));
+ }
+ }
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file set_defaults.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 Method for setting the default options of an SMT engine.
+ **/
+
+#ifndef CVC4__SMT__SET_DEFAULTS_H
+#define CVC4__SMT__SET_DEFAULTS_H
+
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * The purpose of this method is to set the default options and update the logic
+ * info for SMT engine smte.
+ *
+ * The argument logic is 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.
+ */
+void setDefaults(SmtEngine& smte, LogicInfo& logic);
+
+} // namespace smt
+} // namespace CVC4
+
+#endif /* CVC4__SMT__SET_DEFAULTS_H */
#include "smt/managed_ostreams.h"
#include "smt/model_blocker.h"
#include "smt/model_core_builder.h"
+#include "smt/set_defaults.h"
#include "smt/smt_engine_scope.h"
#include "smt/term_formula_removal.h"
#include "smt/update_ostream.h"
d_fullyInited(false),
d_queryMade(false),
d_needPostsolve(false),
- d_earlyTheoryPP(true),
d_globalNegation(false),
d_status(),
d_expectedStatus(),
d_private->addUseTheoryListListener(getTheoryEngine());
+ // set the random seed
+ Random::getRandom().setSeed(options::seed());
+
// ensure that our heuristics are properly set up
- setDefaults();
+ setDefaults(*this, d_logic);
Trace("smt-debug") << "Making decision engine..." << std::endl;
d_logic.lock();
}
-void SmtEngine::setDefaults() {
- Random::getRandom().setSeed(options::seed());
- // Language-based defaults
- if (!options::bitvectorDivByZeroConst.wasSetByUser())
- {
- // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
- // set this option if the input format is SMT LIB 2.6. We also set this
- // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
- options::bitvectorDivByZeroConst.set(
- language::isInputLang_smt2_6(options::inputLanguage())
- || language::isInputLangSygus(options::inputLanguage()));
- }
- bool is_sygus = language::isInputLangSygus(options::inputLanguage());
-
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- if (options::produceModels()
- && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
- || d_logic.isTheoryEnabled(THEORY_UF)))
- {
- if (options::bitblastMode.wasSetByUser()
- || options::produceModels.wasSetByUser())
- {
- throw OptionException(std::string(
- "Eager bit-blasting currently does not support model generation "
- "for the combination of bit-vectors with arrays or uinterpreted "
- "functions. Try --bitblast=lazy"));
- }
- Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
- << "generation" << endl;
- setOption("bitblastMode", SExpr("lazy"));
- }
- else if (!options::incrementalSolving())
- {
- options::ackermann.set(true);
- }
-
- if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV))
- {
- throw OptionException(
- "Incremental eager bit-blasting is currently "
- "only supported for QF_BV. Try --bitblast=lazy.");
- }
- }
-
- if (options::solveIntAsBV() > 0)
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableTheory(THEORY_BV);
- d_logic.lock();
- }
-
- if (options::solveBVAsInt() > 0)
- {
- if (d_logic.isTheoryEnabled(THEORY_BV))
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableTheory(THEORY_ARITH);
- d_logic.arithNonLinear();
- d_logic.lock();
- }
- }
-
- // set options about ackermannization
- if (options::ackermann() && options::produceModels()
- && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
- || d_logic.isTheoryEnabled(THEORY_UF)))
- {
- if (options::produceModels.wasSetByUser())
- {
- throw OptionException(std::string(
- "Ackermannization currently does not support model generation."));
- }
- Notice() << "SmtEngine: turn off ackermannization to support model"
- << "generation" << endl;
- options::ackermann.set(false);
- }
-
- if (options::ackermann())
- {
- if (options::incrementalSolving())
- {
- throw OptionException(
- "Incremental Ackermannization is currently not supported.");
- }
-
- if (d_logic.isQuantified())
- {
- throw LogicException("Cannot use Ackermannization on quantified formula");
- }
-
- if (d_logic.isTheoryEnabled(THEORY_UF))
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.disableTheory(THEORY_UF);
- d_logic.lock();
- }
- if (d_logic.isTheoryEnabled(THEORY_ARRAYS))
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.disableTheory(THEORY_ARRAYS);
- d_logic.lock();
- }
- }
-
- // Set default options associated with strings-exp. We also set these options
- // if we are using eager string preprocessing, which may introduce quantified
- // formulas at preprocess time.
- if (options::stringExp() || !options::stringLazyPreproc())
- {
- // We require quantifiers since extended functions reduce using them.
- if (!d_logic.isQuantified())
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableQuantifiers();
- d_logic.lock();
- Trace("smt") << "turning on quantifier logic, for strings-exp"
- << std::endl;
- }
- // We require bounded quantifier handling.
- if (!options::fmfBound.wasSetByUser())
- {
- options::fmfBound.set( true );
- Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
- }
- // Turn off E-matching, since some bounded quantifiers introduced by strings
- // (e.g. for replaceall) admit matching loops.
- if (!options::eMatching.wasSetByUser())
- {
- options::eMatching.set(false);
- Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
- }
- // Do not eliminate extended arithmetic symbols from quantified formulas,
- // since some strategies, e.g. --re-elim-agg, introduce them.
- if (!options::elimExtArithQuant.wasSetByUser())
- {
- options::elimExtArithQuant.set(false);
- Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
- << std::endl;
- }
- }
-
- // sygus inference may require datatypes
- if (!d_isInternalSubsolver)
- {
- if (options::produceAbducts() || options::sygusInference()
- || options::sygusRewSynthInput())
- {
- // since we are trying to recast as sygus, we assume the input is sygus
- is_sygus = true;
- }
- }
-
- // We now know whether the input is sygus. Update the logic to incorporate
- // the theories we need internally for handling sygus problems.
- if (is_sygus)
- {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableSygus();
- d_logic.lock();
- }
-
- // sygus core connective requires unsat cores
- if (options::sygusCoreConnective())
- {
- options::unsatCores.set(true);
- }
-
- if ((options::checkModels() || options::checkSynthSol()
- || options::produceAbducts()
- || options::modelCoresMode() != options::ModelCoresMode::NONE
- || options::blockModelsMode() != options::BlockModelsMode::NONE)
- && !options::produceAssertions())
- {
- Notice() << "SmtEngine: turning on produce-assertions to support "
- << "option requiring assertions." << endl;
- setOption("produce-assertions", SExpr("true"));
- }
-
- // Disable options incompatible with incremental solving, unsat cores, and
- // proofs or output an error if enabled explicitly
- if (options::incrementalSolving() || options::unsatCores()
- || options::proof())
- {
- if (options::unconstrainedSimp())
- {
- if (options::unconstrainedSimp.wasSetByUser())
- {
- throw OptionException(
- "unconstrained simplification not supported with unsat "
- "cores/proofs/incremental solving");
- }
- Notice() << "SmtEngine: turning off unconstrained simplification to "
- "support unsat cores/proofs/incremental solving"
- << endl;
- options::unconstrainedSimp.set(false);
- }
- }
- else
- {
- // Turn on unconstrained simplification for QF_AUFBV
- if (!options::unconstrainedSimp.wasSetByUser())
- {
- // bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
- // !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
- // !options::incrementalSolving();
- bool uncSimp = !d_logic.isQuantified() && !options::produceModels()
- && !options::produceAssignments()
- && !options::checkModels()
- && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
- && d_logic.isTheoryEnabled(THEORY_BV));
- Trace("smt") << "setting unconstrained simplification to " << uncSimp
- << endl;
- options::unconstrainedSimp.set(uncSimp);
- }
- }
-
- if (options::incrementalSolving() || options::proof())
- {
- if (options::sygusInference())
- {
- if (options::sygusInference.wasSetByUser())
- {
- throw OptionException(
- "sygus inference not supported with proofs/incremental solving");
- }
- Notice() << "SmtEngine: turning off sygus inference to support "
- "proofs/incremental solving"
- << std::endl;
- options::sygusInference.set(false);
- }
- }
-
- // Disable options incompatible with unsat cores and proofs or output an
- // error if enabled explicitly
- if (options::unsatCores() || options::proof())
- {
- if (options::simplificationMode() != options::SimplificationMode::NONE)
- {
- if (options::simplificationMode.wasSetByUser())
- {
- throw OptionException(
- "simplification not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off simplification to support unsat "
- "cores/proofs"
- << endl;
- options::simplificationMode.set(options::SimplificationMode::NONE);
- }
-
- if (options::pbRewrites())
- {
- if (options::pbRewrites.wasSetByUser())
- {
- throw OptionException(
- "pseudoboolean rewrites not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
- "unsat cores/proofs"
- << endl;
- setOption("pb-rewrites", false);
- }
-
- if (options::sortInference())
- {
- if (options::sortInference.wasSetByUser())
- {
- throw OptionException(
- "sort inference not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off sort inference to support unsat "
- "cores/proofs"
- << endl;
- options::sortInference.set(false);
- }
-
- if (options::preSkolemQuant())
- {
- if (options::preSkolemQuant.wasSetByUser())
- {
- throw OptionException(
- "pre-skolemization not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
- "cores/proofs"
- << endl;
- options::preSkolemQuant.set(false);
- }
-
- if (options::solveBVAsInt() > 0)
- {
- /**
- * Operations on 1 bits are better handled as Boolean operations
- * than as integer operations.
- * Therefore, we enable bv-to-bool, which runs before
- * the translation to integers.
- */
- options::bitvectorToBool.set(true);
- }
-
- if (options::bitvectorToBool())
- {
- if (options::bitvectorToBool.wasSetByUser())
- {
- throw OptionException(
- "bv-to-bool not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
- "cores/proofs"
- << endl;
- options::bitvectorToBool.set(false);
- }
-
- if (options::boolToBitvector() != options::BoolToBVMode::OFF)
- {
- if (options::boolToBitvector.wasSetByUser())
- {
- throw OptionException(
- "bool-to-bv != off not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
- "cores/proofs"
- << endl;
- setOption("boolToBitvector", SExpr("off"));
- }
-
- if (options::bvIntroducePow2())
- {
- if (options::bvIntroducePow2.wasSetByUser())
- {
- throw OptionException(
- "bv-intro-pow2 not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
- "unsat-cores/proofs"
- << endl;
- setOption("bv-intro-pow2", false);
- }
-
- if (options::repeatSimp())
- {
- if (options::repeatSimp.wasSetByUser())
- {
- throw OptionException(
- "repeat-simp not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off repeat-simp to support unsat "
- "cores/proofs"
- << endl;
- setOption("repeat-simp", false);
- }
-
- if (options::globalNegate())
- {
- if (options::globalNegate.wasSetByUser())
- {
- throw OptionException(
- "global-negate not supported with unsat cores/proofs");
- }
- Notice() << "SmtEngine: turning off global-negate to support unsat "
- "cores/proofs"
- << endl;
- setOption("global-negate", false);
- }
-
- if (options::bitvectorAig())
- {
- throw OptionException(
- "bitblast-aig not supported with unsat cores/proofs");
- }
- }
- else
- {
- // by default, nonclausal simplification is off for QF_SAT
- if (!options::simplificationMode.wasSetByUser())
- {
- bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
- Trace("smt") << "setting simplification mode to <"
- << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
- // simplification=none works better for SMT LIB benchmarks with
- // quantifiers, not others options::simplificationMode.set(qf_sat ||
- // quantifiers ? options::SimplificationMode::NONE :
- // options::SimplificationMode::BATCH);
- options::simplificationMode.set(qf_sat
- ? options::SimplificationMode::NONE
- : options::SimplificationMode::BATCH);
- }
- }
-
- if (options::cbqiBv() && d_logic.isQuantified())
- {
- if (options::boolToBitvector() != options::BoolToBVMode::OFF)
- {
- if (options::boolToBitvector.wasSetByUser())
- {
- throw OptionException(
- "bool-to-bv != off not supported with CBQI BV for quantified "
- "logics");
- }
- Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
- << endl;
- setOption("boolToBitvector", SExpr("off"));
- }
- }
-
- // cases where we need produce models
- if (!options::produceModels()
- && (options::produceAssignments() || options::sygusRewSynthCheck()
- || is_sygus))
- {
- Notice() << "SmtEngine: turning on produce-models" << endl;
- setOption("produce-models", SExpr("true"));
- }
-
- // Set the options for the theoryOf
- if(!options::theoryOfMode.wasSetByUser()) {
- if(d_logic.isSharingEnabled() &&
- !d_logic.isTheoryEnabled(THEORY_BV) &&
- !d_logic.isTheoryEnabled(THEORY_STRINGS) &&
- !d_logic.isTheoryEnabled(THEORY_SETS) ) {
- Trace("smt") << "setting theoryof-mode to term-based" << endl;
- options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
- }
- }
-
- // strings require LIA, UF; widen the logic
- if(d_logic.isTheoryEnabled(THEORY_STRINGS)) {
- LogicInfo log(d_logic.getUnlockedCopy());
- // Strings requires arith for length constraints, and also UF
- if(!d_logic.isTheoryEnabled(THEORY_UF)) {
- Trace("smt") << "because strings are enabled, also enabling UF" << endl;
- log.enableTheory(THEORY_UF);
- }
- if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) {
- Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl;
- log.enableTheory(THEORY_ARITH);
- log.enableIntegers();
- log.arithOnlyLinear();
- }
- d_logic = log;
- d_logic.lock();
- }
- if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
- if(!d_logic.isTheoryEnabled(THEORY_UF)) {
- LogicInfo log(d_logic.getUnlockedCopy());
- Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
- log.enableTheory(THEORY_UF);
- d_logic = log;
- d_logic.lock();
- }
- }
-
- // by default, symmetry breaker is on only for non-incremental QF_UF
- if(! options::ufSymmetryBreaker.wasSetByUser()) {
- bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
- && !options::incrementalSolving() && !options::proof()
- && !options::unsatCores();
- Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl;
- options::ufSymmetryBreaker.set(qf_uf_noinc);
- }
-
- // If in arrays, set the UF handler to arrays
- if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
- (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
- Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
- } else {
- Theory::setUninterpretedSortOwner(THEORY_UF);
- }
-
- if(! options::simplifyWithCareEnabled.wasSetByUser() ){
- bool qf_aufbv = !d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_BV);
-
- bool withCare = qf_aufbv;
- Trace("smt") << "setting ite simplify with care to " << withCare << endl;
- options::simplifyWithCareEnabled.set(withCare);
- }
- // Turn off array eager index splitting for QF_AUFLIA
- if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
- if (not d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_ARITH)) {
- Trace("smt") << "setting array eager index splitting to false" << endl;
- options::arraysEagerIndexSplitting.set(false);
- }
- }
- // Turn on model-based arrays for QF_AX (unless models are enabled)
- // if(! options::arraysModelBased.wasSetByUser()) {
- // if (not d_logic.isQuantified() &&
- // d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- // d_logic.isPure(THEORY_ARRAYS) &&
- // !options::produceModels() &&
- // !options::checkModels()) {
- // Trace("smt") << "turning on model-based array solver" << endl;
- // options::arraysModelBased.set(true);
- // }
- // }
- // Turn on multiple-pass non-clausal simplification for QF_AUFBV
- if(! options::repeatSimp.wasSetByUser()) {
- bool repeatSimp = !d_logic.isQuantified() &&
- (d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_BV)) &&
- !options::unsatCores();
- Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
- options::repeatSimp.set(repeatSimp);
- }
-
- if (options::boolToBitvector() == options::BoolToBVMode::ALL
- && !d_logic.isTheoryEnabled(THEORY_BV))
- {
- if (options::boolToBitvector.wasSetByUser())
- {
- throw OptionException(
- "bool-to-bv=all not supported for non-bitvector logics.");
- }
- Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
- << d_logic.getLogicString() << std::endl;
- setOption("boolToBitvector", SExpr("off"));
- }
-
- if (! options::bvEagerExplanations.wasSetByUser() &&
- d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- d_logic.isTheoryEnabled(THEORY_BV)) {
- Trace("smt") << "enabling eager bit-vector explanations " << endl;
- options::bvEagerExplanations.set(true);
- }
-
- // Turn on arith rewrite equalities only for pure arithmetic
- if(! options::arithRewriteEq.wasSetByUser()) {
- bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified();
- Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl;
- options::arithRewriteEq.set(arithRewriteEq);
- }
- if(! options::arithHeuristicPivots.wasSetByUser()) {
- int16_t heuristicPivots = 5;
- if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()) {
- if(d_logic.isDifferenceLogic()) {
- heuristicPivots = -1;
- } else if(!d_logic.areIntegersUsed()) {
- heuristicPivots = 0;
- }
- }
- Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots << endl;
- options::arithHeuristicPivots.set(heuristicPivots);
- }
- if(! options::arithPivotThreshold.wasSetByUser()){
- uint16_t pivotThreshold = 2;
- if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
- if(d_logic.isDifferenceLogic()){
- pivotThreshold = 16;
- }
- }
- Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold << endl;
- options::arithPivotThreshold.set(pivotThreshold);
- }
- if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
- int16_t varOrderPivots = -1;
- if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
- varOrderPivots = 200;
- }
- Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots << endl;
- options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
- }
- // Turn off early theory preprocessing if arithRewriteEq is on
- if (options::arithRewriteEq()) {
- d_earlyTheoryPP = false;
- }
- if (d_logic.isPure(THEORY_ARITH) && !d_logic.areRealsUsed())
- {
- if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
- {
- Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl;
- options::nlExtTangentPlanesInterleave.set(true);
- }
- }
-
- // Set decision mode based on logic (if not set by user)
- if(!options::decisionMode.wasSetByUser()) {
- options::DecisionMode decMode =
- // sygus uses internal
- is_sygus ? options::DecisionMode::INTERNAL :
- // ALL
- d_logic.hasEverything()
- ? options::DecisionMode::JUSTIFICATION
- : ( // QF_BV
- (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV)) ||
- // QF_AUFBV or QF_ABV or QF_UFBV
- (not d_logic.isQuantified()
- && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
- || d_logic.isTheoryEnabled(THEORY_UF))
- && d_logic.isTheoryEnabled(THEORY_BV))
- ||
- // QF_AUFLIA (and may be ends up enabling
- // QF_AUFLRA?)
- (not d_logic.isQuantified()
- && d_logic.isTheoryEnabled(THEORY_ARRAYS)
- && d_logic.isTheoryEnabled(THEORY_UF)
- && d_logic.isTheoryEnabled(THEORY_ARITH))
- ||
- // QF_LRA
- (not d_logic.isQuantified()
- && d_logic.isPure(THEORY_ARITH)
- && d_logic.isLinear()
- && !d_logic.isDifferenceLogic()
- && !d_logic.areIntegersUsed())
- ||
- // Quantifiers
- d_logic.isQuantified() ||
- // Strings
- d_logic.isTheoryEnabled(THEORY_STRINGS)
- ? options::DecisionMode::JUSTIFICATION
- : options::DecisionMode::INTERNAL);
-
- bool stoponly =
- // ALL
- d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
- ( // QF_AUFLIA
- (not d_logic.isQuantified() &&
- d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
- d_logic.isTheoryEnabled(THEORY_UF) &&
- d_logic.isTheoryEnabled(THEORY_ARITH)
- ) ||
- // QF_LRA
- (not d_logic.isQuantified() &&
- d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
- )
- ? true : false
- );
-
- Trace("smt") << "setting decision mode to " << decMode << endl;
- options::decisionMode.set(decMode);
- options::decisionStopOnly.set(stoponly);
- }
- if( options::incrementalSolving() ){
- //disable modes not supported by incremental
- options::sortInference.set( false );
- options::ufssFairnessMonotone.set( false );
- options::quantEpr.set( false );
- options::globalNegate.set(false);
- }
- if( d_logic.hasCardinalityConstraints() ){
- //must have finite model finding on
- options::finiteModelFind.set( true );
- }
-
- //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
- if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
- if( !options::instWhenStrictInterleave.wasSetByUser() ){
- options::instWhenStrictInterleave.set( false );
- }
- }
-
- if( options::instMaxLevel()!=-1 ){
- Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
- options::cbqi.set(false);
- }
- // Do we need to track instantiations?
- // Needed for sygus due to single invocation techniques.
- if (options::cbqiNestedQE()
- || (options::proof() && !options::trackInstLemmas.wasSetByUser())
- || is_sygus)
- {
- options::trackInstLemmas.set( true );
- }
-
- if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) ||
- ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) {
- options::fmfBound.set( true );
- }
- //now have determined whether fmfBoundInt is on/off
- //apply fmfBoundInt options
- if( options::fmfBound() ){
- if (!options::mbqiMode.wasSetByUser()
- || (options::mbqiMode() != options::MbqiMode::NONE
- && options::mbqiMode() != options::MbqiMode::FMC))
- {
- //if bounded integers are set, use no MBQI by default
- options::mbqiMode.set(options::MbqiMode::NONE);
- }
- if( ! options::prenexQuant.wasSetByUser() ){
- options::prenexQuant.set(options::PrenexQuantMode::NONE);
- }
- }
- if( options::ufHo() ){
- //if higher-order, then current variants of model-based instantiation cannot be used
- if (options::mbqiMode() != options::MbqiMode::NONE)
- {
- options::mbqiMode.set(options::MbqiMode::NONE);
- }
- if (!options::hoElimStoreAx.wasSetByUser())
- {
- // by default, use store axioms only if --ho-elim is set
- options::hoElimStoreAx.set(options::hoElim());
- }
- }
- if( options::fmfFunWellDefinedRelevant() ){
- if( !options::fmfFunWellDefined.wasSetByUser() ){
- options::fmfFunWellDefined.set( true );
- }
- }
- if( options::fmfFunWellDefined() ){
- if( !options::finiteModelFind.wasSetByUser() ){
- options::finiteModelFind.set( true );
- }
- }
- //EPR
- if( options::quantEpr() ){
- if( !options::preSkolemQuant.wasSetByUser() ){
- options::preSkolemQuant.set( true );
- }
- }
-
- //now, have determined whether finite model find is on/off
- //apply finite model finding options
- if( options::finiteModelFind() ){
- //apply conservative quantifiers splitting
- if( !options::quantDynamicSplit.wasSetByUser() ){
- options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
- }
- //do not eliminate extended arithmetic symbols from quantified formulas
- if( !options::elimExtArithQuant.wasSetByUser() ){
- options::elimExtArithQuant.set( false );
- }
- if( !options::eMatching.wasSetByUser() ){
- options::eMatching.set( options::fmfInstEngine() );
- }
- if( !options::instWhenMode.wasSetByUser() ){
- //instantiate only on last call
- if( options::eMatching() ){
- options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
- }
- }
- }
-
- // apply sygus options
- // if we are attempting to rewrite everything to SyGuS, use sygus()
- if (is_sygus)
- {
- if (!options::sygus())
- {
- Trace("smt") << "turning on sygus" << std::endl;
- }
- options::sygus.set(true);
- // must use Ferrante/Rackoff for real arithmetic
- if (!options::cbqiMidpoint.wasSetByUser())
- {
- options::cbqiMidpoint.set(true);
- }
- if (options::sygusRepairConst())
- {
- if (!options::cbqi.wasSetByUser())
- {
- options::cbqi.set(true);
- }
- }
- if (options::sygusInference())
- {
- // optimization: apply preskolemization, makes it succeed more often
- if (!options::preSkolemQuant.wasSetByUser())
- {
- options::preSkolemQuant.set(true);
- }
- if (!options::preSkolemQuantNested.wasSetByUser())
- {
- options::preSkolemQuantNested.set(true);
- }
- }
- //counterexample-guided instantiation for sygus
- if( !options::cegqiSingleInvMode.wasSetByUser() ){
- options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
- }
- if( !options::quantConflictFind.wasSetByUser() ){
- options::quantConflictFind.set( false );
- }
- if( !options::instNoEntail.wasSetByUser() ){
- options::instNoEntail.set( false );
- }
- if (!options::cbqiFullEffort.wasSetByUser())
- {
- // should use full effort cbqi for single invocation and repair const
- options::cbqiFullEffort.set(true);
- }
- if (options::sygusRew())
- {
- options::sygusRewSynth.set(true);
- options::sygusRewVerify.set(true);
- }
- if (options::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.
- options::sygusRewSynth.set(true);
- // we should not use the extended rewriter, since we are interested
- // in rewrites that are not in the main rewriter
- if (!options::sygusExtRew.wasSetByUser())
- {
- options::sygusExtRew.set(false);
- }
- }
- // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
- // is one that is specialized for returning a single solution. Non-basic
- // sygus algorithms currently include the PBE solver, UNIF+PI, static
- // template inference for invariant synthesis, and single invocation
- // techniques.
- bool reqBasicSygus = false;
- if (options::produceAbducts())
- {
- // if doing abduction, we should filter strong solutions
- if (!options::sygusFilterSolMode.wasSetByUser())
- {
- options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
- }
- // we must use basic sygus algorithms, since e.g. we require checking
- // a sygus side condition for consistency with axioms.
- reqBasicSygus = true;
- }
- if (options::sygusRewSynth() || options::sygusRewVerify()
- || options::sygusQueryGen())
- {
- // rewrite rule synthesis implies that sygus stream must be true
- options::sygusStream.set(true);
- }
- if (options::sygusStream() || options::incrementalSolving())
- {
- // Streaming and incremental mode are incompatible with techniques that
- // focus the search towards finding a single solution.
- reqBasicSygus = true;
- }
- // Now, disable options for non-basic sygus algorithms, if necessary.
- if (reqBasicSygus)
- {
- if (!options::sygusUnifPbe.wasSetByUser())
- {
- options::sygusUnifPbe.set(false);
- }
- if (options::sygusUnifPi.wasSetByUser())
- {
- options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
- }
- if (!options::sygusInvTemplMode.wasSetByUser())
- {
- options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
- }
- if (!options::cegqiSingleInvMode.wasSetByUser())
- {
- options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
- }
- }
- //do not allow partial functions
- if (!options::bitvectorDivByZeroConst())
- {
- if (options::bitvectorDivByZeroConst.wasSetByUser())
- {
- throw OptionException(
- "--no-bv-div-zero-const is not supported with SyGuS");
- }
- Notice()
- << "SmtEngine: setting bv-div-zero-const to true to support SyGuS"
- << std::endl;
- options::bitvectorDivByZeroConst.set( true );
- }
- if( !options::dtRewriteErrorSel.wasSetByUser() ){
- options::dtRewriteErrorSel.set( true );
- }
- //do not miniscope
- if( !options::miniscopeQuant.wasSetByUser() ){
- options::miniscopeQuant.set( false );
- }
- if( !options::miniscopeQuantFreeVar.wasSetByUser() ){
- options::miniscopeQuantFreeVar.set( false );
- }
- if (!options::quantSplit.wasSetByUser())
- {
- options::quantSplit.set(false);
- }
- //rewrite divk
- if( !options::rewriteDivk.wasSetByUser()) {
- options::rewriteDivk.set( true );
- }
- //do not do macros
- if( !options::macrosQuant.wasSetByUser()) {
- options::macrosQuant.set( false );
- }
- if( !options::cbqiPreRegInst.wasSetByUser()) {
- options::cbqiPreRegInst.set( true );
- }
- }
- //counterexample-guided instantiation for non-sygus
- // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
- if ((d_logic.isQuantified()
- && (d_logic.isTheoryEnabled(THEORY_ARITH)
- || d_logic.isTheoryEnabled(THEORY_DATATYPES)
- || d_logic.isTheoryEnabled(THEORY_BV)
- || d_logic.isTheoryEnabled(THEORY_FP)))
- || options::cbqiAll())
- {
- if( !options::cbqi.wasSetByUser() ){
- options::cbqi.set( true );
- }
- // check whether we should apply full cbqi
- if (d_logic.isPure(THEORY_BV))
- {
- if (!options::cbqiFullEffort.wasSetByUser())
- {
- options::cbqiFullEffort.set(true);
- }
- }
- }
- if( options::cbqi() ){
- //must rewrite divk
- if( !options::rewriteDivk.wasSetByUser()) {
- options::rewriteDivk.set( true );
- }
- if (options::incrementalSolving())
- {
- // cannot do nested quantifier elimination in incremental mode
- options::cbqiNestedQE.set(false);
- }
- if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
- {
- if( !options::quantConflictFind.wasSetByUser() ){
- options::quantConflictFind.set( false );
- }
- if( !options::instNoEntail.wasSetByUser() ){
- options::instNoEntail.set( false );
- }
- if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
- //only instantiation should happen at last call when model is avaiable
- options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
- }
- }else{
- // only supported in pure arithmetic or pure BV
- options::cbqiNestedQE.set(false);
- }
- // prenexing
- if (options::cbqiNestedQE())
- {
- // only complete with prenex = disj_normal or normal
- if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
- {
- options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL);
- }
- }
- else if (options::globalNegate())
- {
- if (!options::prenexQuant.wasSetByUser())
- {
- options::prenexQuant.set(options::PrenexQuantMode::NONE);
- }
- }
- }
- //implied options...
- if( options::strictTriggers() ){
- if( !options::userPatternsQuant.wasSetByUser() ){
- options::userPatternsQuant.set(options::UserPatMode::TRUST);
- }
- }
- if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
- options::quantConflictFind.set( true );
- }
- if( options::cbqiNestedQE() ){
- options::prenexQuantUser.set( true );
- if( !options::preSkolemQuant.wasSetByUser() ){
- options::preSkolemQuant.set( true );
- }
- }
- //for induction techniques
- if( options::quantInduction() ){
- if( !options::dtStcInduction.wasSetByUser() ){
- options::dtStcInduction.set( true );
- }
- if( !options::intWfInduction.wasSetByUser() ){
- options::intWfInduction.set( true );
- }
- }
- if( options::dtStcInduction() ){
- //try to remove ITEs from quantified formulas
- if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
- options::iteDtTesterSplitQuant.set( true );
- }
- if( !options::iteLiftQuant.wasSetByUser() ){
- options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
- }
- }
- if( options::intWfInduction() ){
- if( !options::purifyTriggers.wasSetByUser() ){
- options::purifyTriggers.set( true );
- }
- }
- if( options::conjectureNoFilter() ){
- if( !options::conjectureFilterActiveTerms.wasSetByUser() ){
- options::conjectureFilterActiveTerms.set( false );
- }
- if( !options::conjectureFilterCanonical.wasSetByUser() ){
- options::conjectureFilterCanonical.set( false );
- }
- if( !options::conjectureFilterModel.wasSetByUser() ){
- options::conjectureFilterModel.set( false );
- }
- }
- if( options::conjectureGenPerRound.wasSetByUser() ){
- if( options::conjectureGenPerRound()>0 ){
- options::conjectureGen.set( true );
- }else{
- options::conjectureGen.set( false );
- }
- }
- //can't pre-skolemize nested quantifiers without UF theory
- if( !d_logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant() ){
- if( !options::preSkolemQuantNested.wasSetByUser() ){
- options::preSkolemQuantNested.set( false );
- }
- }
- if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
- options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
- }
-
- //until bugs 371,431 are fixed
- if( ! options::minisatUseElim.wasSetByUser()){
- // cannot use minisat elimination for logics where a theory solver
- // introduces new literals into the search. This includes quantifiers
- // (quantifier instantiation), and the lemma schemas used in non-linear
- // and sets. We also can't use it if models are enabled.
- if (d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified()
- || options::produceModels() || options::produceAssignments()
- || options::checkModels()
- || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()))
- {
- options::minisatUseElim.set( false );
- }
- }
-
- // For now, these array theory optimizations do not support model-building
- if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
- options::arraysOptimizeLinear.set(false);
- options::arraysLazyRIntro1.set(false);
- }
-
- if (options::proof())
- {
- if (options::incrementalSolving())
- {
- if (options::incrementalSolving.wasSetByUser())
- {
- throw OptionException("--incremental is not supported with proofs");
- }
- Warning()
- << "SmtEngine: turning off incremental solving mode (not yet "
- "supported with --proof, try --tear-down-incremental instead)"
- << endl;
- setOption("incremental", SExpr("false"));
- }
- if (d_logic > LogicInfo("QF_AUFBVLRA"))
- {
- throw OptionException(
- "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
- }
- if (options::bitvectorAlgebraicSolver())
- {
- if (options::bitvectorAlgebraicSolver.wasSetByUser())
- {
- throw OptionException(
- "--bv-algebraic-solver is not supported with proofs");
- }
- Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
- << std::endl;
- options::bitvectorAlgebraicSolver.set(false);
- }
- if (options::bitvectorEqualitySolver())
- {
- if (options::bitvectorEqualitySolver.wasSetByUser())
- {
- throw OptionException("--bv-eq-solver is not supported with proofs");
- }
- Notice() << "SmtEngine: turning off bv eq solver to support proofs"
- << std::endl;
- options::bitvectorEqualitySolver.set(false);
- }
- if (options::bitvectorInequalitySolver())
- {
- if (options::bitvectorInequalitySolver.wasSetByUser())
- {
- throw OptionException(
- "--bv-inequality-solver is not supported with proofs");
- }
- Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
- << std::endl;
- options::bitvectorInequalitySolver.set(false);
- }
- }
-
- if (!options::bitvectorEqualitySolver())
- {
- if (options::bvLazyRewriteExtf())
- {
- if (options::bvLazyRewriteExtf.wasSetByUser())
- {
- throw OptionException(
- "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
- }
- }
- Trace("smt")
- << "disabling bvLazyRewriteExtf since equality solver is disabled"
- << endl;
- options::bvLazyRewriteExtf.set(false);
- }
-
- if (!options::sygusExprMinerCheckUseExport())
- {
- if (options::sygusExprMinerCheckTimeout.wasSetByUser())
- {
- throw OptionException(
- "--sygus-expr-miner-check-timeout=N requires "
- "--sygus-expr-miner-check-use-export");
- }
- if (options::sygusRewSynthInput() || options::produceAbducts())
- {
- std::stringstream ss;
- ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
- : "--produce-abducts");
- ss << "requires --sygus-expr-miner-check-use-export";
- throw OptionException(ss.str());
- }
- }
-
- if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
- {
- Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
- "--strings-fmf enabled"
- << endl;
- options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
- }
-
- // !!! All options that require disabling models go here
- bool disableModels = false;
- std::string sOptNoModel;
- if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
- {
- disableModels = true;
- sOptNoModel = "unconstrained-simp";
- }
- else if (options::sortInference())
- {
- disableModels = true;
- sOptNoModel = "sort-inference";
- }
- else if (options::minisatUseElim())
- {
- disableModels = true;
- sOptNoModel = "minisat-elimination";
- }
- else if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()
- && !options::nlExt())
- {
- disableModels = true;
- sOptNoModel = "nonlinear arithmetic without nl-ext";
- }
- else if (options::globalNegate())
- {
- disableModels = true;
- sOptNoModel = "global-negate";
- }
- if (disableModels)
- {
- if (options::produceModels())
- {
- if (options::produceModels.wasSetByUser())
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel << " with model generation.";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off produce-models to support "
- << sOptNoModel << endl;
- setOption("produce-models", SExpr("false"));
- }
- if (options::produceAssignments())
- {
- if (options::produceAssignments.wasSetByUser())
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel
- << " with model generation (produce-assignments).";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off produce-assignments to support "
- << sOptNoModel << endl;
- setOption("produce-assignments", SExpr("false"));
- }
- if (options::checkModels())
- {
- if (options::checkModels.wasSetByUser())
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel
- << " with model generation (check-models).";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off check-models to support "
- << sOptNoModel << endl;
- setOption("check-models", SExpr("false"));
- }
- }
-}
-
void SmtEngine::setProblemExtended()
{
d_smtMode = SMT_MODE_ASSERT;
d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
// Theory preprocessing
- if (d_smt.d_earlyTheoryPP)
+ bool doEarlyTheoryPp = !options::arithRewriteEq();
+ if (doEarlyTheoryPp)
{
d_passes["theory-preprocess"]->apply(&d_assertions);
}
}
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
+
+bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
+
CVC4::SExpr SmtEngine::getOption(const std::string& key) const
{
NodeManagerScope nms(d_nodeManager);
* --sygus-abduct.
*/
void setIsInternalSubsolver();
+ /** Is this an internal subsolver? */
+ bool isInternalSubsolver() const;
/** set the input name */
void setFilename(std::string filename);
*/
void finalOptionsAreSet();
- /**
- * Apply heuristics settings and other defaults. Done once, at
- * finishInit() time.
- */
- void setDefaults();
-
/**
* Sets that the problem has been extended. This sets the smt mode of the
* solver to SMT_MODE_ASSERT, and clears the list of assumptions from the
projects / cvc5.git / commitdiff