From 1ed3d2c92dde0a64242fe3aa22f6db4da70aaf06 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Aug 2021 14:19:30 -0500 Subject: [PATCH] More refactoring of set defaults (#7043) A few minor changes to which options are enabled for sygus, otherwise no intended changes. --- src/smt/set_defaults.cpp | 988 +++++++++--------- src/smt/set_defaults.h | 26 +- src/theory/quantifiers/sygus/synth_verify.cpp | 7 + 3 files changed, 538 insertions(+), 483 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 12433d8ac..5532d599c 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -132,9 +132,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) opts.bv.bitvectorAlgebraicSolver = true; } - bool isSygus = language::isInputLangSygus(opts.base.inputLanguage); - bool usesSygus = isSygus; - if (opts.bv.bitblastMode == options::BitblastMode::EAGER) { if (opts.smt.produceModels @@ -301,14 +298,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) // the bounded integers module will always process internally generated // quantifiers (those marked with InternalQuantAttribute). } - // whether we must disable proofs - bool disableProofs = false; - if (opts.quantifiers.globalNegate) - { - // When global negate answers "unsat", it is not due to showing a set of - // formulas is unsat. Thus, proofs do not apply. - disableProofs = true; - } // new unsat core specific restrictions for proofs if (opts.smt.unsatCores @@ -337,42 +326,17 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) } } - // sygus inference may require datatypes - if (!d_isInternalSubsolver) - { - if (opts.smt.produceAbducts - || opts.smt.produceInterpols != options::ProduceInterpols::NONE - || opts.quantifiers.sygusInference - || opts.quantifiers.sygusRewSynthInput) - { - // since we are trying to recast as sygus, we assume the input is sygus - isSygus = true; - usesSygus = true; - } - else if (opts.quantifiers.sygusInst) - { - // sygus instantiation uses sygus, but it is not a sygus problem - usesSygus = true; - } - } - // We now know whether the input uses sygus. Update the logic to incorporate // the theories we need internally for handling sygus problems. - if (usesSygus) + if (usesSygus(opts)) { logic = logic.getUnlockedCopy(); logic.enableSygus(); logic.lock(); - if (isSygus) - { - // When sygus answers "unsat", it is not due to showing a set of - // formulas is unsat in the standard way. Thus, proofs do not apply. - disableProofs = true; - } } // if we requiring disabling proofs, disable them now - if (disableProofs && opts.smt.produceProofs) + if (mustDisableProofs(opts) && opts.smt.produceProofs) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; @@ -657,7 +621,7 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) // cases where we need produce models if (!opts.smt.produceModels && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck - || usesSygus)) + || usesSygus(opts))) { Notice() << "SmtEngine: turning on produce-models" << std::endl; opts.smt.produceModels = true; @@ -826,76 +790,8 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) } } - // Set decision mode based on logic (if not set by user) - if (!opts.decision.decisionModeWasSetByUser) - { - options::DecisionMode decMode = - // anything that uses sygus uses internal - usesSygus ? options::DecisionMode::INTERNAL : - // ALL or its supersets - 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 or its supersets - 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); - - opts.decision.decisionMode = decMode; - if (stoponly) - { - if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION) - { - opts.decision.decisionMode = options::DecisionMode::STOPONLY; - } - else - { - Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL); - } - } - Trace("smt") << "setting decision mode to " << opts.decision.decisionMode - << std::endl; - } + // set the default decision mode + setDefaultDecisionMode(logic, opts); // set up of central equality engine if (opts.theory.eeMode == options::EqEngineMode::CENTRAL) @@ -925,166 +821,479 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) opts.bv.bvAbstraction = false; opts.arith.arithMLTrick = false; } - if (logic.hasCardinalityConstraints()) - { - // must have finite model finding on - opts.quantifiers.finiteModelFind = true; - } - - if (opts.quantifiers.instMaxLevel != -1) - { - Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" - << std::endl; - opts.quantifiers.cegqi = false; - } - if ((opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) - || (opts.quantifiers.fmfBoundIntWasSetByUser && opts.quantifiers.fmfBoundInt)) - { - opts.quantifiers.fmfBound = true; - Trace("smt") - << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n"; - } - // now have determined whether fmfBound is on/off - // apply fmfBound options - if (opts.quantifiers.fmfBound) - { - if (!opts.quantifiers.mbqiModeWasSetByUser - || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE - && opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) - { - // if bounded integers are set, use no MBQI by default - opts.quantifiers.mbqiMode = options::MbqiMode::NONE; - } - if (!opts.quantifiers.prenexQuantUserWasSetByUser) - { - opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; - } - } if (logic.isHigherOrder()) { opts.uf.ufHo = true; - // if higher-order, then current variants of model-based instantiation - // cannot be used - if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) - { - opts.quantifiers.mbqiMode = options::MbqiMode::NONE; - } - if (!opts.quantifiers.hoElimStoreAxWasSetByUser) - { - // by default, use store axioms only if --ho-elim is set - opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; - } if (!opts.theory.assignFunctionValues) { // must assign function values opts.theory.assignFunctionValues = true; } - // Cannot use macros, since lambda lifting and macro elimination are inverse - // operations. - if (opts.quantifiers.macrosQuant) + } + + // set all defaults in the quantifiers theory, which includes sygus + setDefaultsQuantifiers(logic, opts); + + // until bugs 371,431 are fixed + if (!opts.prop.minisatUseElimWasSetByUser) + { + // 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.isTheoryEnabled(THEORY_BAGS) + || logic.isQuantified() || opts.smt.produceModels + || opts.smt.produceAssignments || opts.smt.checkModels + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { - opts.quantifiers.macrosQuant = false; + opts.prop.minisatUseElim = false; } - // HOL is incompatible with fmfBound - if (opts.quantifiers.fmfBound) + } + + if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && opts.arith.nlRlvMode != options::NlRlvMode::NONE) + { + if (!opts.theory.relevanceFilter) { - if (opts.quantifiers.fmfBoundWasSetByUser - || opts.quantifiers.fmfBoundLazyWasSetByUser - || opts.quantifiers.fmfBoundIntWasSetByUser) + if (opts.theory.relevanceFilterWasSetByUser) { - Notice() << "Disabling bound finite-model finding since it is " - "incompatible with HOL.\n"; + Warning() << "SmtEngine: turning on relevance filtering to support " + "--nl-ext-rlv=" + << opts.arith.nlRlvMode << std::endl; } - - opts.quantifiers.fmfBound = false; - Trace("smt") << "turning off fmf-bound, since HOL\n"; + // must use relevance filtering techniques + opts.theory.relevanceFilter = true; } } - if (opts.quantifiers.fmfFunWellDefinedRelevant) + + // For now, these array theory optimizations do not support model-building + if (opts.smt.produceModels || opts.smt.produceAssignments + || opts.smt.checkModels) { - if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) - { - opts.quantifiers.fmfFunWellDefined = true; - } + opts.arrays.arraysOptimizeLinear = false; } - if (opts.quantifiers.fmfFunWellDefined) + + if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) { - if (!opts.quantifiers.finiteModelFindWasSetByUser) - { - opts.quantifiers.finiteModelFind = true; - } + Trace("smt") << "settting stringProcessLoopMode to 'simple' since " + "--strings-fmf enabled" + << std::endl; + opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE; } - // now, have determined whether finite model find is on/off - // apply finite model finding options - if (opts.quantifiers.finiteModelFind) + // !!! All options that require disabling models go here + bool disableModels = false; + std::string sOptNoModel; + if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp) { - // apply conservative quantifiers splitting - if (!opts.quantifiers.quantDynamicSplitWasSetByUser) + disableModels = true; + sOptNoModel = "unconstrained-simp"; + } + else if (opts.smt.sortInference) + { + disableModels = true; + sOptNoModel = "sort-inference"; + } + else if (opts.prop.minisatUseElim) + { + disableModels = true; + sOptNoModel = "minisat-elimination"; + } + else if (opts.quantifiers.globalNegate) + { + disableModels = true; + sOptNoModel = "global-negate"; + } + if (disableModels) + { + if (opts.smt.produceModels) { - opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT; + if (opts.smt.produceModelsWasSetByUser) + { + 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; + opts.smt.produceModels = false; } - if (!opts.quantifiers.eMatchingWasSetByUser) + if (opts.smt.produceAssignments) { - opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine; + if (opts.smt.produceAssignmentsWasSetByUser) + { + 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; + opts.smt.produceAssignments = false; } - if (!opts.quantifiers.instWhenModeWasSetByUser) + if (opts.smt.checkModels) { - // instantiate only on last call - if (opts.quantifiers.eMatching) + if (opts.smt.checkModelsWasSetByUser) { - opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; + 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; + opts.smt.checkModels = false; } } - // apply sygus options - // if we are attempting to rewrite everything to SyGuS, use sygus() - if (usesSygus) + if (opts.bv.bitblastMode == options::BitblastMode::EAGER + && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" + && logic.getLogicString() != "QF_ABV") { - setDefaultsSygus(opts); + throw OptionException( + "Eager bit-blasting does not currently support theory combination. " + "Note that in a QF_BV problem UF symbols can be introduced for " + "division. " + "Try --bv-div-zero-const to interpret division by zero as a constant."); } - // 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))) - || opts.quantifiers.cegqiAll) + +#ifdef CVC5_USE_POLY + if (logic == LogicInfo("QF_UFNRA")) { - if (!opts.quantifiers.cegqiWasSetByUser) - { - opts.quantifiers.cegqi = true; - } - // check whether we should apply full cbqi - if (logic.isPure(THEORY_BV)) + if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { - if (!opts.quantifiers.cegqiFullEffortWasSetByUser) + opts.arith.nlCad = true; + if (!opts.arith.nlExtWasSetByUser) { - opts.quantifiers.cegqiFullEffort = true; + opts.arith.nlExt = options::NlExtMode::LIGHT; + } + if (!opts.arith.nlRlvModeWasSetByUser) + { + opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE; } } } - if (opts.quantifiers.cegqi) +#else + if (opts.arith.nlCad) { - if (opts.base.incrementalSolving) + if (opts.arith.nlCadWasSetByUser) { - // cannot do nested quantifier elimination in incremental mode - opts.quantifiers.cegqiNestedQE = false; + std::stringstream ss; + ss << "Cannot use " << options::arith::nlCad__name + << " without configuring with --poly."; + throw OptionException(ss.str()); } - if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) + else { - if (!opts.quantifiers.quantConflictFindWasSetByUser) - { - opts.quantifiers.quantConflictFind = false; - } - if (!opts.quantifiers.instNoEntailWasSetByUser) - { - opts.quantifiers.instNoEntail = false; + Notice() << "Cannot use --" << options::arith::nlCad__name + << " without configuring with --poly." << std::endl; + opts.arith.nlCad = false; + opts.arith.nlExt = options::NlExtMode::FULL; + } + } +#endif +} + +bool SetDefaults::isSygus(const Options& opts) const +{ + if (language::isInputLangSygus(opts.base.inputLanguage)) + { + return true; + } + if (!d_isInternalSubsolver) + { + if (opts.smt.produceAbducts + || opts.smt.produceInterpols != options::ProduceInterpols::NONE + || opts.quantifiers.sygusInference + || opts.quantifiers.sygusRewSynthInput) + { + // since we are trying to recast as sygus, we assume the input is sygus + return true; + } + } + return false; +} + +bool SetDefaults::usesSygus(const Options& opts) const +{ + if (isSygus(opts)) + { + return true; + } + if (!d_isInternalSubsolver && opts.quantifiers.sygusInst) + { + // sygus instantiation uses sygus, but it is not a sygus problem + return true; + } + return false; +} + +bool SetDefaults::mustDisableProofs(const Options& opts) const +{ + if (opts.quantifiers.globalNegate) + { + // When global negate answers "unsat", it is not due to showing a set of + // formulas is unsat. Thus, proofs do not apply. + return true; + } + if (isSygus(opts)) + { + // When sygus answers "unsat", it is not due to showing a set of + // formulas is unsat in the standard way. Thus, proofs do not apply. + return true; + } + return false; +} + +void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const +{ + bool needsUf = false; + // 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 + needsUf = true; + if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) + { + Notice() + << "Enabling linear integer arithmetic because strings are enabled" + << std::endl; + log.enableTheory(THEORY_ARITH); + log.enableIntegers(); + log.arithOnlyLinear(); + } + else if (!logic.areIntegersUsed()) + { + Notice() << "Enabling integer arithmetic because strings are enabled" + << std::endl; + log.enableIntegers(); + } + logic = log; + logic.lock(); + } + if (opts.bv.bvAbstraction) + { + // bv abstraction may require UF + Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; + needsUf = true; + } + else if (opts.quantifiers.preSkolemQuantNested + && opts.quantifiers.preSkolemQuantNestedWasSetByUser) + { + // if pre-skolem nested is explictly set, then we require UF. If it is + // not explicitly set, it is disabled below if UF is not present. + Notice() << "Enabling UF because preSkolemQuantNested requires it." + << std::endl; + needsUf = true; + } + if (needsUf + // Arrays, datatypes and sets permit Boolean terms and thus require UF + || logic.isTheoryEnabled(THEORY_ARRAYS) + || logic.isTheoryEnabled(THEORY_DATATYPES) + || logic.isTheoryEnabled(THEORY_SETS) + || logic.isTheoryEnabled(THEORY_BAGS) + // Non-linear arithmetic requires UF to deal with division/mod because + // their expansion introduces UFs for the division/mod-by-zero case. + // If we are eliminating non-linear arithmetic via solve-int-as-bv, + // then this is not required, since non-linear arithmetic will be + // eliminated altogether (or otherwise fail at preprocessing). + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && opts.smt.solveIntAsBV == 0) + // FP requires UF since there are multiple operators that are partially + // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more + // details). + || logic.isTheoryEnabled(THEORY_FP)) + { + if (!logic.isTheoryEnabled(THEORY_UF)) + { + LogicInfo log(logic.getUnlockedCopy()); + if (!needsUf) + { + Notice() << "Enabling UF because " << logic << " requires it." + << std::endl; + } + log.enableTheory(THEORY_UF); + logic = log; + logic.lock(); + } + } + if (opts.arith.arithMLTrick) + { + if (!logic.areIntegersUsed()) + { + // enable integers + LogicInfo log(logic.getUnlockedCopy()); + Notice() << "Enabling integers because arithMLTrick requires it." + << std::endl; + log.enableIntegers(); + logic = log; + logic.lock(); + } + } +} + +void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, + Options& opts) const +{ + if (logic.hasCardinalityConstraints()) + { + // must have finite model finding on + opts.quantifiers.finiteModelFind = true; + } + + if (opts.quantifiers.instMaxLevel != -1) + { + Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" + << std::endl; + opts.quantifiers.cegqi = false; + } + + if ((opts.quantifiers.fmfBoundLazyWasSetByUser + && opts.quantifiers.fmfBoundLazy) + || (opts.quantifiers.fmfBoundIntWasSetByUser + && opts.quantifiers.fmfBoundInt)) + { + opts.quantifiers.fmfBound = true; + Trace("smt") + << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n"; + } + // now have determined whether fmfBound is on/off + // apply fmfBound options + if (opts.quantifiers.fmfBound) + { + if (!opts.quantifiers.mbqiModeWasSetByUser + || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE + && opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) + { + // if bounded integers are set, use no MBQI by default + opts.quantifiers.mbqiMode = options::MbqiMode::NONE; + } + if (!opts.quantifiers.prenexQuantUserWasSetByUser) + { + opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; + } + } + if (logic.isHigherOrder()) + { + // if higher-order, then current variants of model-based instantiation + // cannot be used + if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) + { + opts.quantifiers.mbqiMode = options::MbqiMode::NONE; + } + if (!opts.quantifiers.hoElimStoreAxWasSetByUser) + { + // by default, use store axioms only if --ho-elim is set + opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; + } + // Cannot use macros, since lambda lifting and macro elimination are inverse + // operations. + if (opts.quantifiers.macrosQuant) + { + opts.quantifiers.macrosQuant = false; + } + // HOL is incompatible with fmfBound + if (opts.quantifiers.fmfBound) + { + if (opts.quantifiers.fmfBoundWasSetByUser + || opts.quantifiers.fmfBoundLazyWasSetByUser + || opts.quantifiers.fmfBoundIntWasSetByUser) + { + Notice() << "Disabling bound finite-model finding since it is " + "incompatible with HOL.\n"; + } + + opts.quantifiers.fmfBound = false; + Trace("smt") << "turning off fmf-bound, since HOL\n"; + } + } + if (opts.quantifiers.fmfFunWellDefinedRelevant) + { + if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) + { + opts.quantifiers.fmfFunWellDefined = true; + } + } + if (opts.quantifiers.fmfFunWellDefined) + { + if (!opts.quantifiers.finiteModelFindWasSetByUser) + { + opts.quantifiers.finiteModelFind = true; + } + } + + // now, have determined whether finite model find is on/off + // apply finite model finding options + if (opts.quantifiers.finiteModelFind) + { + // apply conservative quantifiers splitting + if (!opts.quantifiers.quantDynamicSplitWasSetByUser) + { + opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT; + } + if (!opts.quantifiers.eMatchingWasSetByUser) + { + opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine; + } + if (!opts.quantifiers.instWhenModeWasSetByUser) + { + // instantiate only on last call + if (opts.quantifiers.eMatching) + { + opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; + } + } + } + + // apply sygus options + // if we are attempting to rewrite everything to SyGuS, use sygus() + if (usesSygus(opts)) + { + setDefaultsSygus(opts); + } + // 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))) + || opts.quantifiers.cegqiAll) + { + if (!opts.quantifiers.cegqiWasSetByUser) + { + opts.quantifiers.cegqi = true; + } + // check whether we should apply full cbqi + if (logic.isPure(THEORY_BV)) + { + if (!opts.quantifiers.cegqiFullEffortWasSetByUser) + { + opts.quantifiers.cegqiFullEffort = true; + } + } + } + if (opts.quantifiers.cegqi) + { + if (opts.base.incrementalSolving) + { + // cannot do nested quantifier elimination in incremental mode + opts.quantifiers.cegqiNestedQE = false; + } + if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) + { + if (!opts.quantifiers.quantConflictFindWasSetByUser) + { + opts.quantifiers.quantConflictFind = false; + } + if (!opts.quantifiers.instNoEntailWasSetByUser) + { + opts.quantifiers.instNoEntail = false; } - if (!opts.quantifiers.instWhenModeWasSetByUser && opts.quantifiers.cegqiModel) + if (!opts.quantifiers.instWhenModeWasSetByUser + && opts.quantifiers.cegqiModel) { // only instantiation should happen at last call when model is avaiable opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; @@ -1185,256 +1394,9 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) { opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE; } - - // until bugs 371,431 are fixed - if (!opts.prop.minisatUseElimWasSetByUser) - { - // 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.isTheoryEnabled(THEORY_BAGS) - || logic.isQuantified() || opts.smt.produceModels - || opts.smt.produceAssignments || opts.smt.checkModels - || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) - { - opts.prop.minisatUseElim = false; - } - } - - if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && opts.arith.nlRlvMode != options::NlRlvMode::NONE) - { - if (!opts.theory.relevanceFilter) - { - if (opts.theory.relevanceFilterWasSetByUser) - { - Warning() << "SmtEngine: turning on relevance filtering to support " - "--nl-ext-rlv=" - << opts.arith.nlRlvMode << std::endl; - } - // must use relevance filtering techniques - opts.theory.relevanceFilter = true; - } - } - - // For now, these array theory optimizations do not support model-building - if (opts.smt.produceModels || opts.smt.produceAssignments - || opts.smt.checkModels) - { - opts.arrays.arraysOptimizeLinear = false; - } - - if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) - { - Trace("smt") << "settting stringProcessLoopMode to 'simple' since " - "--strings-fmf enabled" - << std::endl; - opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE; - } - - // !!! All options that require disabling models go here - bool disableModels = false; - std::string sOptNoModel; - if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp) - { - disableModels = true; - sOptNoModel = "unconstrained-simp"; - } - else if (opts.smt.sortInference) - { - disableModels = true; - sOptNoModel = "sort-inference"; - } - else if (opts.prop.minisatUseElim) - { - disableModels = true; - sOptNoModel = "minisat-elimination"; - } - else if (opts.quantifiers.globalNegate) - { - disableModels = true; - sOptNoModel = "global-negate"; - } - if (disableModels) - { - if (opts.smt.produceModels) - { - if (opts.smt.produceModelsWasSetByUser) - { - 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; - opts.smt.produceModels = false; - } - if (opts.smt.produceAssignments) - { - if (opts.smt.produceAssignmentsWasSetByUser) - { - 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; - opts.smt.produceAssignments = false; - } - if (opts.smt.checkModels) - { - if (opts.smt.checkModelsWasSetByUser) - { - 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; - opts.smt.checkModels = false; - } - } - - if (opts.bv.bitblastMode == options::BitblastMode::EAGER - && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" - && logic.getLogicString() != "QF_ABV") - { - throw OptionException( - "Eager bit-blasting does not currently support theory combination. " - "Note that in a QF_BV problem UF symbols can be introduced for " - "division. " - "Try --bv-div-zero-const to interpret division by zero as a constant."); - } - - if (logic == LogicInfo("QF_UFNRA")) - { -#ifdef CVC5_USE_POLY - if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) - { - opts.arith.nlCad = true; - if (!opts.arith.nlExtWasSetByUser) - { - opts.arith.nlExt = options::NlExtMode::LIGHT; - } - if (!opts.arith.nlRlvModeWasSetByUser) - { - opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE; - } - } -#endif - } -#ifndef CVC5_USE_POLY - if (opts.arith.nlCad) - { - if (opts.arith.nlCadWasSetByUser) - { - std::stringstream ss; - ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly."; - throw OptionException(ss.str()); - } - else - { - Notice() << "Cannot use --" << options::arith::nlCad__name - << " without configuring with --poly." << std::endl; - opts.arith.nlCad = false; - opts.arith.nlExt = options::NlExtMode::FULL; - } - } -#endif -} - -void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) -{ - bool needsUf = false; - // 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 - needsUf = true; - if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) - { - Notice() - << "Enabling linear integer arithmetic because strings are enabled" - << std::endl; - log.enableTheory(THEORY_ARITH); - log.enableIntegers(); - log.arithOnlyLinear(); - } - else if (!logic.areIntegersUsed()) - { - Notice() << "Enabling integer arithmetic because strings are enabled" - << std::endl; - log.enableIntegers(); - } - logic = log; - logic.lock(); - } - if (opts.bv.bvAbstraction) - { - // bv abstraction may require UF - Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; - needsUf = true; - } - else if (opts.quantifiers.preSkolemQuantNested - && opts.quantifiers.preSkolemQuantNestedWasSetByUser) - { - // if pre-skolem nested is explictly set, then we require UF. If it is - // not explicitly set, it is disabled below if UF is not present. - Notice() << "Enabling UF because preSkolemQuantNested requires it." - << std::endl; - needsUf = true; - } - if (needsUf - // Arrays, datatypes and sets permit Boolean terms and thus require UF - || logic.isTheoryEnabled(THEORY_ARRAYS) - || logic.isTheoryEnabled(THEORY_DATATYPES) - || logic.isTheoryEnabled(THEORY_SETS) - || logic.isTheoryEnabled(THEORY_BAGS) - // Non-linear arithmetic requires UF to deal with division/mod because - // their expansion introduces UFs for the division/mod-by-zero case. - // If we are eliminating non-linear arithmetic via solve-int-as-bv, - // then this is not required, since non-linear arithmetic will be - // eliminated altogether (or otherwise fail at preprocessing). - || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && opts.smt.solveIntAsBV == 0) - // FP requires UF since there are multiple operators that are partially - // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more - // details). - || logic.isTheoryEnabled(THEORY_FP)) - { - if (!logic.isTheoryEnabled(THEORY_UF)) - { - LogicInfo log(logic.getUnlockedCopy()); - if (!needsUf) - { - Notice() << "Enabling UF because " << logic << " requires it." - << std::endl; - } - log.enableTheory(THEORY_UF); - logic = log; - logic.lock(); - } - } - if (opts.arith.arithMLTrick) - { - if (!logic.areIntegersUsed()) - { - // enable integers - LogicInfo log(logic.getUnlockedCopy()); - Notice() << "Enabling integers because arithMLTrick requires it." - << std::endl; - log.enableIntegers(); - logic = log; - logic.lock(); - } - } } -void SetDefaults::setDefaultsSygus(Options& opts) +void SetDefaults::setDefaultsSygus(Options& opts) const { if (!opts.quantifiers.sygus) { @@ -1556,10 +1518,6 @@ void SetDefaults::setDefaultsSygus(Options& opts) opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; } } - if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) - { - opts.datatypes.dtRewriteErrorSel = true; - } // do not miniscope if (!opts.quantifiers.miniscopeQuantWasSetByUser) { @@ -1578,12 +1536,80 @@ void SetDefaults::setDefaultsSygus(Options& opts) { opts.quantifiers.macrosQuant = false; } - // use tangent planes by default, since we want to put effort into - // the verification step for sygus queries with non-linear arithmetic - if (!opts.arith.nlExtTangentPlanesWasSetByUser) - { - opts.arith.nlExtTangentPlanes = true; +} +void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, + Options& opts) const +{ + // Set decision mode based on logic (if not set by user) + if (opts.decision.decisionModeWasSetByUser) + { + return; + } + options::DecisionMode decMode = + // anything that uses sygus uses internal + usesSygus(opts) ? options::DecisionMode::INTERNAL : + // ALL or its supersets + 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 or its supersets + 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); + + opts.decision.decisionMode = decMode; + if (stoponly) + { + if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION) + { + opts.decision.decisionMode = options::DecisionMode::STOPONLY; + } + else + { + Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL); + } } + Trace("smt") << "setting decision mode to " << opts.decision.decisionMode + << std::endl; } } // namespace smt diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 99db64b4a..a1bf17a8f 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -46,16 +46,38 @@ class SetDefaults void setDefaults(LogicInfo& logic, Options& opts); private: + /** + * Determine whether we will be solving a SyGuS problem. + */ + bool isSygus(const Options& opts) const; + /** + * Determine whether we will be using SyGuS. + */ + bool usesSygus(const Options& opts) const; + /** + * Return true if proofs must be disabled. This is the case for any technique + * that answers "unsat" without showing a proof of unsatisfiabilty. + */ + bool mustDisableProofs(const Options& opts) const; /** * Widen logic to theories that are required, since some theories imply the * use of other theories to handle certain operators, e.g. UF to handle * partial functions. */ - void widenLogic(LogicInfo& logic, Options& opts); + void widenLogic(LogicInfo& logic, Options& opts) const; + /** + * Set defaults related to quantifiers, called when quantifiers are enabled. + * This method modifies opt.quantifiers only. + */ + void setDefaultsQuantifiers(const LogicInfo& logic, Options& opts) const; /** * Set defaults related to SyGuS, called when SyGuS is enabled. */ - void setDefaultsSygus(Options& opts); + void setDefaultsSygus(Options& opts) const; + /** + * Set default decision mode + */ + void setDefaultDecisionMode(const LogicInfo& logic, Options& opts) const; /** Are we an internal subsolver? */ bool d_isInternalSubsolver; }; diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 43131ac24..2d7255415 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/sygus/synth_verify.h" #include "expr/node_algorithm.h" +#include "options/arith_options.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "smt/smt_engine_scope.h" @@ -46,6 +47,12 @@ SynthVerify::SynthVerify(TermDbSygus* tds) : d_tds(tds) // instead of being claimed by sygus in the subsolver. d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; d_subOptions.quantifiers.sygus = false; + // use tangent planes by default, since we want to put effort into + // the verification step for sygus queries with non-linear arithmetic + if (!d_subOptions.arith.nlExtTangentPlanesWasSetByUser) + { + d_subOptions.arith.nlExtTangentPlanes = true; + } } SynthVerify::~SynthVerify() {} -- 2.30.2