src/smt/set_defaults.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of setting default options.
  14  */
  15
  16 #include "smt/set_defaults.h"
  17
  18 #include <sstream>
  19
  20 #include "base/output.h"
  21 #include "options/arith_options.h"
  22 #include "options/arrays_options.h"
  23 #include "options/base_options.h"
  24 #include "options/booleans_options.h"
  25 #include "options/bv_options.h"
  26 #include "options/datatypes_options.h"
  27 #include "options/decision_options.h"
  28 #include "options/language.h"
  29 #include "options/main_options.h"
  30 #include "options/option_exception.h"
  31 #include "options/printer_options.h"
  32 #include "options/proof_options.h"
  33 #include "options/prop_options.h"
  34 #include "options/quantifiers_options.h"
  35 #include "options/sep_options.h"
  36 #include "options/set_language.h"
  37 #include "options/smt_options.h"
  38 #include "options/strings_options.h"
  39 #include "options/theory_options.h"
  40 #include "options/uf_options.h"
  41 #include "smt/logic_exception.h"
  42 #include "theory/theory.h"
  43
  44 using namespace cvc5::theory;
  45
  46 namespace cvc5 {
  47 namespace smt {
  48
  49 SetDefaults::SetDefaults(bool isInternalSubsolver)
  50     : d_isInternalSubsolver(isInternalSubsolver)
  51 {
  52 }
  53
  54 void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
  55 {
  56   // initial changes that are independent of logic, and may impact the logic
  57   setDefaultsPre(opts);
  58   // now, finalize the logic
  59   finalizeLogic(logic, opts);
  60   // further changes to options based on the logic
  61   setDefaultsPost(logic, opts);
  62 }
  63
  64 void SetDefaults::setDefaultsPre(Options& opts)
  65 {
  66   // implied options
  67   if (opts.smt.debugCheckModels)
  68   {
  69     opts.smt.checkModels = true;
  70   }
  71   if (opts.smt.checkModels || opts.driver.dumpModels)
  72   {
  73     opts.smt.produceModels = true;
  74   }
  75   if (opts.smt.checkModels)
  76   {
  77     opts.smt.produceAssignments = true;
  78   }
  79   // unsat cores and proofs shenanigans
  80   if (opts.driver.dumpDifficulty)
  81   {
  82     opts.smt.produceDifficulty = true;
  83   }
  84   if (opts.smt.produceDifficulty)
  85   {
  86     if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
  87     {
  88       opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY;
  89     }
  90     opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
  91   }
  92   if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
  93       || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
  94       || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
  95   {
  96     opts.smt.unsatCores = true;
  97   }
  98   if (opts.smt.unsatCores
  99       && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
 100   {
 101     if (opts.smt.unsatCoresModeWasSetByUser)
 102     {
 103       Notice()
 104           << "Overriding OFF unsat-core mode since cores were requested.\n";
 105     }
 106     opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
 107   }
 108
 109   if (opts.smt.checkProofs || opts.driver.dumpProofs)
 110   {
 111     opts.smt.produceProofs = true;
 112   }
 113
 114   if (opts.smt.produceProofs
 115       && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF)
 116   {
 117     if (opts.smt.unsatCoresModeWasSetByUser)
 118     {
 119       Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
 120                   "were requested.\n";
 121     }
 122     // enable unsat cores, because they are available as a consequence of proofs
 123     opts.smt.unsatCores = true;
 124     opts.smt.unsatCoresMode = options::UnsatCoresMode::FULL_PROOF;
 125   }
 126
 127   // set proofs on if not yet set
 128   if (opts.smt.unsatCores && !opts.smt.produceProofs)
 129   {
 130     if (opts.smt.produceProofsWasSetByUser)
 131     {
 132       Notice()
 133           << "Forcing proof production since new unsat cores were requested.\n";
 134     }
 135     opts.smt.produceProofs = true;
 136   }
 137
 138   // if unsat cores are disabled, then unsat cores mode should be OFF
 139   Assert(opts.smt.unsatCores
 140          == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF));
 141
 142   // new unsat core specific restrictions for proofs
 143   if (opts.smt.unsatCores
 144       && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF)
 145   {
 146     // no fine-graininess
 147     if (!opts.proof.proofGranularityModeWasSetByUser)
 148     {
 149       opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
 150     }
 151   }
 152
 153   if (opts.bv.bitvectorAigSimplificationsWasSetByUser)
 154   {
 155     Notice() << "SolverEngine: setting bitvectorAig" << std::endl;
 156     opts.bv.bitvectorAig = true;
 157   }
 158   if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser)
 159   {
 160     Notice() << "SolverEngine: setting bitvectorAlgebraicSolver" << std::endl;
 161     opts.bv.bitvectorAlgebraicSolver = true;
 162   }
 163
 164   // if we requiring disabling proofs, disable them now
 165   if (opts.smt.produceProofs)
 166   {
 167     std::stringstream reasonNoProofs;
 168     if (incompatibleWithProofs(opts, reasonNoProofs))
 169     {
 170       opts.smt.unsatCores = false;
 171       opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
 172       Notice() << "SolverEngine: turning off produce-proofs due to "
 173                << reasonNoProofs.str() << "." << std::endl;
 174       opts.smt.produceProofs = false;
 175       opts.smt.checkProofs = false;
 176     }
 177   }
 178   if (d_isInternalSubsolver)
 179   {
 180     // these options must be disabled on internal subsolvers, as they are
 181     // used by the user to rephrase the input.
 182     opts.quantifiers.sygusInference = false;
 183     opts.quantifiers.sygusRewSynthInput = false;
 184   }
 185 }
 186
 187 void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 188 {
 189   if (opts.quantifiers.sygusInstWasSetByUser)
 190   {
 191     if (isSygus(opts))
 192     {
 193       throw OptionException(std::string(
 194           "SyGuS instantiation quantifiers module cannot be enabled "
 195           "for SyGuS inputs."));
 196     }
 197   }
 198   else if (!isSygus(opts) && logic.isQuantified()
 199            && (logic.isPure(THEORY_FP)
 200                || (logic.isPure(THEORY_ARITH) && !logic.isLinear())))
 201   {
 202     opts.quantifiers.sygusInst = true;
 203   }
 204
 205   if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
 206   {
 207     if (opts.smt.produceModels
 208         && (logic.isTheoryEnabled(THEORY_ARRAYS)
 209             || logic.isTheoryEnabled(THEORY_UF)))
 210     {
 211       if (opts.bv.bitblastModeWasSetByUser
 212           || opts.smt.produceModelsWasSetByUser)
 213       {
 214         throw OptionException(std::string(
 215             "Eager bit-blasting currently does not support model generation "
 216             "for the combination of bit-vectors with arrays or uinterpreted "
 217             "functions. Try --bitblast=lazy"));
 218       }
 219       Notice()
 220           << "SolverEngine: setting bit-blast mode to lazy to support model"
 221           << "generation" << std::endl;
 222       opts.bv.bitblastMode = options::BitblastMode::LAZY;
 223     }
 224     else if (!opts.base.incrementalSolving)
 225     {
 226       opts.smt.ackermann = true;
 227     }
 228   }
 229
 230   if (opts.smt.solveIntAsBV > 0)
 231   {
 232     // Int to BV currently always eliminates arithmetic completely (or otherwise
 233     // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
 234     // are required.
 235     logic = logic.getUnlockedCopy();
 236     logic.enableTheory(THEORY_BV);
 237     logic.disableTheory(THEORY_ARITH);
 238     logic.lock();
 239   }
 240
 241   if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
 242   {
 243     if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
 244     {
 245       throw OptionException(
 246           "solving bitvectors as integers is incompatible with --bool-to-bv.");
 247     }
 248     if (opts.smt.BVAndIntegerGranularity > 8)
 249     {
 250       /**
 251        * The granularity sets the size of the ITE in each element
 252        * of the sum that is generated for bitwise operators.
 253        * The size of the ITE is 2^{2*granularity}.
 254        * Since we don't want to introduce ITEs with unbounded size,
 255        * we bound the granularity.
 256        */
 257       throw OptionException("solve-bv-as-int accepts values from 0 to 8.");
 258     }
 259     if (logic.isTheoryEnabled(THEORY_BV))
 260     {
 261       logic = logic.getUnlockedCopy();
 262       logic.enableTheory(THEORY_ARITH);
 263       logic.arithNonLinear();
 264       logic.lock();
 265     }
 266   }
 267
 268   // set options about ackermannization
 269   if (opts.smt.ackermann && opts.smt.produceModels
 270       && (logic.isTheoryEnabled(THEORY_ARRAYS)
 271           || logic.isTheoryEnabled(THEORY_UF)))
 272   {
 273     if (opts.smt.produceModelsWasSetByUser)
 274     {
 275       throw OptionException(std::string(
 276           "Ackermannization currently does not support model generation."));
 277     }
 278     Notice() << "SolverEngine: turn off ackermannization to support model"
 279              << "generation" << std::endl;
 280     opts.smt.ackermann = false;
 281   }
 282
 283   if (opts.smt.ackermann)
 284   {
 285     if (logic.isTheoryEnabled(THEORY_UF))
 286     {
 287       logic = logic.getUnlockedCopy();
 288       logic.disableTheory(THEORY_UF);
 289       logic.lock();
 290     }
 291     if (logic.isTheoryEnabled(THEORY_ARRAYS))
 292     {
 293       logic = logic.getUnlockedCopy();
 294       logic.disableTheory(THEORY_ARRAYS);
 295       logic.lock();
 296     }
 297   }
 298
 299   // Set default options associated with strings-exp. We also set these options
 300   // if we are using eager string preprocessing, which may introduce quantified
 301   // formulas at preprocess time.
 302   //
 303   // We don't want to set this option when we are in logics that contain ALL.
 304   if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
 305   {
 306     // If the user explicitly set a logic that includes strings, but is not
 307     // the generic "ALL" logic, then enable stringsExp.
 308     opts.strings.stringExp = true;
 309     Trace("smt") << "Turning stringExp on since logic does not have everything "
 310                     "and string theory is enabled\n";
 311   }
 312   if (opts.strings.stringExp || !opts.strings.stringLazyPreproc)
 313   {
 314     // We require quantifiers since extended functions reduce using them.
 315     if (!logic.isQuantified())
 316     {
 317       logic = logic.getUnlockedCopy();
 318       logic.enableQuantifiers();
 319       logic.lock();
 320       Trace("smt") << "turning on quantifier logic, for strings-exp"
 321                    << std::endl;
 322     }
 323     // Note we allow E-matching by default to support combinations of sequences
 324     // and quantifiers. We also do not enable fmfBound here, which would
 325     // enable bounded integer instantiation for *all* quantifiers. Instead,
 326     // the bounded integers module will always process internally generated
 327     // quantifiers (those marked with InternalQuantAttribute).
 328   }
 329
 330   if (opts.arrays.arraysExp)
 331   {
 332     if (!logic.isQuantified())
 333     {
 334       logic = logic.getUnlockedCopy();
 335       logic.enableQuantifiers();
 336       logic.lock();
 337     }
 338   }
 339
 340   // We now know whether the input uses sygus. Update the logic to incorporate
 341   // the theories we need internally for handling sygus problems.
 342   if (usesSygus(opts))
 343   {
 344     logic = logic.getUnlockedCopy();
 345     logic.enableSygus();
 346     logic.lock();
 347   }
 348
 349   // widen the logic
 350   widenLogic(logic, opts);
 351
 352   // check if we have any options that are not supported with quantified logics
 353   if (logic.isQuantified())
 354   {
 355     std::stringstream reasonNoQuant;
 356     if (incompatibleWithQuantifiers(opts, reasonNoQuant))
 357     {
 358       std::stringstream ss;
 359       ss << reasonNoQuant.str() << " not supported in quantified logics.";
 360       throw OptionException(ss.str());
 361     }
 362   }
 363 }
 364
 365 void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 366 {
 367
 368   // sygus core connective requires unsat cores
 369   if (opts.quantifiers.sygusCoreConnective)
 370   {
 371     opts.smt.unsatCores = true;
 372     if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
 373     {
 374       opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
 375     }
 376   }
 377
 378   if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts
 379        || opts.smt.produceInterpols != options::ProduceInterpols::NONE
 380        || opts.smt.modelCoresMode != options::ModelCoresMode::NONE
 381        || opts.smt.blockModelsMode != options::BlockModelsMode::NONE
 382        || opts.smt.produceProofs)
 383       && !opts.smt.produceAssertions)
 384   {
 385     Notice() << "SolverEngine: turning on produce-assertions to support "
 386              << "option requiring assertions." << std::endl;
 387     opts.smt.produceAssertions = true;
 388   }
 389
 390   if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
 391   {
 392     /**
 393      * Operations on 1 bits are better handled as Boolean operations
 394      * than as integer operations.
 395      * Therefore, we enable bv-to-bool, which runs before
 396      * the translation to integers.
 397      */
 398     opts.bv.bitvectorToBool = true;
 399   }
 400
 401   // Disable options incompatible with incremental solving, or output an error
 402   // if enabled explicitly.
 403   if (opts.base.incrementalSolving)
 404   {
 405     std::stringstream reasonNoInc;
 406     std::stringstream suggestNoInc;
 407     if (incompatibleWithIncremental(logic, opts, reasonNoInc, suggestNoInc))
 408     {
 409       std::stringstream ss;
 410       ss << reasonNoInc.str() << " not supported with incremental solving. "
 411          << suggestNoInc.str();
 412       throw OptionException(ss.str());
 413     }
 414   }
 415
 416   // Disable options incompatible with unsat cores or output an error if enabled
 417   // explicitly
 418   if (safeUnsatCores(opts))
 419   {
 420     // check if the options are not compatible with unsat cores
 421     std::stringstream reasonNoUc;
 422     if (incompatibleWithUnsatCores(opts, reasonNoUc))
 423     {
 424       std::stringstream ss;
 425       ss << reasonNoUc.str() << " not supported with unsat cores";
 426       throw OptionException(ss.str());
 427     }
 428   }
 429   else
 430   {
 431     // Turn on unconstrained simplification for QF_AUFBV
 432     if (!opts.smt.unconstrainedSimpWasSetByUser
 433         && !opts.base.incrementalSolving)
 434     {
 435       // It is also currently incompatible with arithmetic, force the option
 436       // off.
 437       bool uncSimp = !opts.base.incrementalSolving && !logic.isQuantified()
 438                      && !opts.smt.produceModels && !opts.smt.produceAssignments
 439                      && !opts.smt.checkModels
 440                      && logic.isTheoryEnabled(THEORY_ARRAYS)
 441                      && logic.isTheoryEnabled(THEORY_BV)
 442                      && !logic.isTheoryEnabled(THEORY_ARITH);
 443       Trace("smt") << "setting unconstrained simplification to " << uncSimp
 444                    << std::endl;
 445       opts.smt.unconstrainedSimp = uncSimp;
 446     }
 447
 448     // by default, nonclausal simplification is off for QF_SAT
 449     if (!opts.smt.simplificationModeWasSetByUser)
 450     {
 451       bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
 452       Trace("smt") << "setting simplification mode to <"
 453                    << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
 454       // simplification=none works better for SMT LIB benchmarks with
 455       // quantifiers, not others opts.set(options::simplificationMode, qf_sat ||
 456       // quantifiers ? options::SimplificationMode::NONE :
 457       // options::SimplificationMode::BATCH);
 458       opts.smt.simplificationMode = qf_sat ? options::SimplificationMode::NONE
 459                                            : options::SimplificationMode::BATCH;
 460     }
 461   }
 462
 463   if (opts.quantifiers.cegqiBv && logic.isQuantified())
 464   {
 465     if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
 466     {
 467       if (opts.bv.boolToBitvectorWasSetByUser)
 468       {
 469         throw OptionException(
 470             "bool-to-bv != off not supported with CBQI BV for quantified "
 471             "logics");
 472       }
 473       Notice()
 474           << "SolverEngine: turning off bool-to-bitvector to support CBQI BV"
 475           << std::endl;
 476       opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
 477     }
 478   }
 479
 480   // cases where we need produce models
 481   if (!opts.smt.produceModels
 482       && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
 483           || usesSygus(opts)))
 484   {
 485     Notice() << "SolverEngine: turning on produce-models" << std::endl;
 486     opts.smt.produceModels = true;
 487   }
 488
 489   // --ite-simp is an experimental option designed for QF_LIA/nec. This
 490   // technique is experimental. This benchmark set also requires removing ITEs
 491   // during preprocessing, before repeating simplification. Hence, we enable
 492   // this by default.
 493   if (opts.smt.doITESimp)
 494   {
 495     if (!opts.smt.earlyIteRemovalWasSetByUser)
 496     {
 497       opts.smt.earlyIteRemoval = true;
 498     }
 499   }
 500
 501   // Set the options for the theoryOf
 502   if (!opts.theory.theoryOfModeWasSetByUser)
 503   {
 504     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
 505         && !logic.isTheoryEnabled(THEORY_STRINGS)
 506         && !logic.isTheoryEnabled(THEORY_SETS)
 507         && !logic.isTheoryEnabled(THEORY_BAGS)
 508         && !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
 509              && !logic.isQuantified()))
 510     {
 511       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
 512       opts.theory.theoryOfMode = options::TheoryOfMode::THEORY_OF_TERM_BASED;
 513     }
 514   }
 515
 516   // by default, symmetry breaker is on only for non-incremental QF_UF
 517   if (!opts.uf.ufSymmetryBreakerWasSetByUser)
 518   {
 519     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
 520                        && !opts.base.incrementalSolving
 521                        && !safeUnsatCores(opts);
 522     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
 523                  << std::endl;
 524     opts.uf.ufSymmetryBreaker = qf_uf_noinc;
 525   }
 526
 527   // If in arrays, set the UF handler to arrays
 528   if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder()
 529       && !opts.quantifiers.finiteModelFind
 530       && (!logic.isQuantified()
 531           || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
 532   {
 533     Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
 534   }
 535   else
 536   {
 537     Theory::setUninterpretedSortOwner(THEORY_UF);
 538   }
 539
 540   if (!opts.smt.simplifyWithCareEnabledWasSetByUser)
 541   {
 542     bool qf_aufbv =
 543         !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
 544         && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV);
 545
 546     bool withCare = qf_aufbv;
 547     Trace("smt") << "setting ite simplify with care to " << withCare
 548                  << std::endl;
 549     opts.smt.simplifyWithCareEnabled = withCare;
 550   }
 551   // Turn off array eager index splitting for QF_AUFLIA
 552   if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser)
 553   {
 554     if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
 555         && logic.isTheoryEnabled(THEORY_UF)
 556         && logic.isTheoryEnabled(THEORY_ARITH))
 557     {
 558       Trace("smt") << "setting array eager index splitting to false"
 559                    << std::endl;
 560       opts.arrays.arraysEagerIndexSplitting = false;
 561     }
 562   }
 563   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
 564   if (!opts.smt.repeatSimpWasSetByUser)
 565   {
 566     bool repeatSimp = !logic.isQuantified()
 567                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
 568                           && logic.isTheoryEnabled(THEORY_UF)
 569                           && logic.isTheoryEnabled(THEORY_BV))
 570                       && !safeUnsatCores(opts);
 571     Trace("smt") << "setting repeat simplification to " << repeatSimp
 572                  << std::endl;
 573     opts.smt.repeatSimp = repeatSimp;
 574   }
 575
 576   /* Disable bit-level propagation by default for the BITBLAST solver. */
 577   if (opts.bv.bvSolver == options::BVSolver::BITBLAST)
 578   {
 579     opts.bv.bitvectorPropagate = false;
 580   }
 581
 582   if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL
 583       && !logic.isTheoryEnabled(THEORY_BV))
 584   {
 585     if (opts.bv.boolToBitvectorWasSetByUser)
 586     {
 587       throw OptionException(
 588           "bool-to-bv=all not supported for non-bitvector logics.");
 589     }
 590     Notice() << "SolverEngine: turning off bool-to-bv for non-bv logic: "
 591              << logic.getLogicString() << std::endl;
 592     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
 593   }
 594
 595   if (!opts.bv.bvEagerExplanationsWasSetByUser
 596       && logic.isTheoryEnabled(THEORY_ARRAYS)
 597       && logic.isTheoryEnabled(THEORY_BV))
 598   {
 599     Trace("smt") << "enabling eager bit-vector explanations " << std::endl;
 600     opts.bv.bvEagerExplanations = true;
 601   }
 602
 603   // Turn on arith rewrite equalities only for pure arithmetic
 604   if (!opts.arith.arithRewriteEqWasSetByUser)
 605   {
 606     bool arithRewriteEq =
 607         logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
 608     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
 609                  << std::endl;
 610     opts.arith.arithRewriteEq = arithRewriteEq;
 611   }
 612   if (!opts.arith.arithHeuristicPivotsWasSetByUser)
 613   {
 614     int16_t heuristicPivots = 5;
 615     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
 616     {
 617       if (logic.isDifferenceLogic())
 618       {
 619         heuristicPivots = -1;
 620       }
 621       else if (!logic.areIntegersUsed())
 622       {
 623         heuristicPivots = 0;
 624       }
 625     }
 626     Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots
 627                  << std::endl;
 628     opts.arith.arithHeuristicPivots = heuristicPivots;
 629   }
 630   if (!opts.arith.arithPivotThresholdWasSetByUser)
 631   {
 632     uint16_t pivotThreshold = 2;
 633     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
 634     {
 635       if (logic.isDifferenceLogic())
 636       {
 637         pivotThreshold = 16;
 638       }
 639     }
 640     Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold
 641                  << std::endl;
 642     opts.arith.arithPivotThreshold = pivotThreshold;
 643   }
 644   if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser)
 645   {
 646     int16_t varOrderPivots = -1;
 647     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
 648     {
 649       varOrderPivots = 200;
 650     }
 651     Trace("smt") << "setting arithStandardCheckVarOrderPivots  "
 652                  << varOrderPivots << std::endl;
 653     opts.arith.arithStandardCheckVarOrderPivots = varOrderPivots;
 654   }
 655   if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
 656   {
 657     if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser)
 658     {
 659       Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
 660                    << std::endl;
 661       opts.arith.nlExtTangentPlanesInterleave = true;
 662     }
 663   }
 664   if (!opts.arith.nlRlvAssertBoundsWasSetByUser)
 665   {
 666     // use bound inference to determine when bounds are irrelevant only when
 667     // the logic is quantifier-free
 668     opts.arith.nlRlvAssertBounds = !logic.isQuantified();
 669   }
 670
 671   // set the default decision mode
 672   setDefaultDecisionMode(logic, opts);
 673
 674   // set up of central equality engine
 675   if (opts.theory.eeMode == options::EqEngineMode::CENTRAL)
 676   {
 677     if (!opts.arith.arithEqSolverWasSetByUser)
 678     {
 679       // use the arithmetic equality solver by default
 680       opts.arith.arithEqSolver = true;
 681     }
 682   }
 683   if (opts.arith.arithEqSolver)
 684   {
 685     if (!opts.arith.arithCongManWasSetByUser)
 686     {
 687       // if we are using the arithmetic equality solver, do not use the
 688       // arithmetic congruence manager by default
 689       opts.arith.arithCongMan = false;
 690     }
 691   }
 692
 693   if (logic.isHigherOrder())
 694   {
 695     if (!opts.theory.assignFunctionValues)
 696     {
 697       // must assign function values
 698       opts.theory.assignFunctionValues = true;
 699     }
 700   }
 701
 702   // set all defaults in the quantifiers theory, which includes sygus
 703   setDefaultsQuantifiers(logic, opts);
 704
 705   // shared selectors are generally not good to combine with standard
 706   // quantifier techniques e.g. E-matching
 707   if (!opts.datatypes.dtSharedSelectorsWasSetByUser)
 708   {
 709     if (logic.isQuantified() && !usesSygus(opts))
 710     {
 711       opts.datatypes.dtSharedSelectors = false;
 712     }
 713   }
 714
 715   // until bugs 371,431 are fixed
 716   if (!opts.prop.minisatUseElimWasSetByUser)
 717   {
 718     // cannot use minisat elimination for logics where a theory solver
 719     // introduces new literals into the search. This includes quantifiers
 720     // (quantifier instantiation), and the lemma schemas used in non-linear
 721     // and sets. We also can't use it if models are enabled.
 722     if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS)
 723         || logic.isQuantified() || opts.smt.produceModels
 724         || opts.smt.produceAssignments || opts.smt.checkModels
 725         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
 726     {
 727       opts.prop.minisatUseElim = false;
 728     }
 729   }
 730
 731   if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
 732       && opts.arith.nlRlvMode != options::NlRlvMode::NONE)
 733   {
 734     if (!opts.theory.relevanceFilter)
 735     {
 736       if (opts.theory.relevanceFilterWasSetByUser)
 737       {
 738         Warning() << "SolverEngine: turning on relevance filtering to support "
 739                      "--nl-ext-rlv="
 740                   << opts.arith.nlRlvMode << std::endl;
 741       }
 742       // must use relevance filtering techniques
 743       opts.theory.relevanceFilter = true;
 744     }
 745   }
 746
 747   // For now, these array theory optimizations do not support model-building
 748   if (opts.smt.produceModels || opts.smt.produceAssignments
 749       || opts.smt.checkModels)
 750   {
 751     opts.arrays.arraysOptimizeLinear = false;
 752   }
 753
 754   if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser)
 755   {
 756     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
 757                     "--strings-fmf enabled"
 758                  << std::endl;
 759     opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE;
 760   }
 761
 762   // !!! All options that require disabling models go here
 763   std::stringstream reasonNoModel;
 764   if (incompatibleWithModels(opts, reasonNoModel))
 765   {
 766     std::string sOptNoModel = reasonNoModel.str();
 767     if (opts.smt.produceModels)
 768     {
 769       if (opts.smt.produceModelsWasSetByUser)
 770       {
 771         std::stringstream ss;
 772         ss << "Cannot use " << sOptNoModel << " with model generation.";
 773         throw OptionException(ss.str());
 774       }
 775       Notice() << "SolverEngine: turning off produce-models to support "
 776                << sOptNoModel << std::endl;
 777       opts.smt.produceModels = false;
 778     }
 779     if (opts.smt.produceAssignments)
 780     {
 781       if (opts.smt.produceAssignmentsWasSetByUser)
 782       {
 783         std::stringstream ss;
 784         ss << "Cannot use " << sOptNoModel
 785            << " with model generation (produce-assignments).";
 786         throw OptionException(ss.str());
 787       }
 788       Notice() << "SolverEngine: turning off produce-assignments to support "
 789                << sOptNoModel << std::endl;
 790       opts.smt.produceAssignments = false;
 791     }
 792     if (opts.smt.checkModels)
 793     {
 794       if (opts.smt.checkModelsWasSetByUser)
 795       {
 796         std::stringstream ss;
 797         ss << "Cannot use " << sOptNoModel
 798            << " with model generation (check-models).";
 799         throw OptionException(ss.str());
 800       }
 801       Notice() << "SolverEngine: turning off check-models to support "
 802                << sOptNoModel << std::endl;
 803       opts.smt.checkModels = false;
 804     }
 805   }
 806
 807   if (opts.bv.bitblastMode == options::BitblastMode::EAGER
 808       && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
 809       && logic.getLogicString() != "QF_ABV")
 810   {
 811     throw OptionException(
 812         "Eager bit-blasting does not currently support theory combination. "
 813         "Note that in a QF_BV problem UF symbols can be introduced for "
 814         "division. "
 815         "Try --bv-div-zero-const to interpret division by zero as a constant.");
 816   }
 817
 818 #ifdef CVC5_USE_POLY
 819   if (logic == LogicInfo("QF_UFNRA"))
 820   {
 821     if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser)
 822     {
 823       opts.arith.nlCad = true;
 824       if (!opts.arith.nlExtWasSetByUser)
 825       {
 826         opts.arith.nlExt = options::NlExtMode::LIGHT;
 827       }
 828       if (!opts.arith.nlRlvModeWasSetByUser)
 829       {
 830         opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE;
 831       }
 832     }
 833   }
 834 #else
 835   if (opts.arith.nlCad)
 836   {
 837     if (opts.arith.nlCadWasSetByUser)
 838     {
 839       throw OptionException(
 840           "Cannot use --nl-cad without configuring with --poly.");
 841     }
 842     else
 843     {
 844       Notice() << "Cannot use --nl-cad without configuring with --poly."
 845                << std::endl;
 846       opts.arith.nlCad = false;
 847       opts.arith.nlExt = options::NlExtMode::FULL;
 848     }
 849   }
 850 #endif
 851 }
 852
 853 bool SetDefaults::isSygus(const Options& opts) const
 854 {
 855   if (language::isLangSygus(opts.base.inputLanguage))
 856   {
 857     return true;
 858   }
 859   if (!d_isInternalSubsolver)
 860   {
 861     if (opts.smt.produceAbducts
 862         || opts.smt.produceInterpols != options::ProduceInterpols::NONE
 863         || opts.quantifiers.sygusInference
 864         || opts.quantifiers.sygusRewSynthInput)
 865     {
 866       // since we are trying to recast as sygus, we assume the input is sygus
 867       return true;
 868     }
 869   }
 870   return false;
 871 }
 872
 873 bool SetDefaults::usesSygus(const Options& opts) const
 874 {
 875   if (isSygus(opts))
 876   {
 877     return true;
 878   }
 879   if (!d_isInternalSubsolver && opts.quantifiers.sygusInst)
 880   {
 881     // sygus instantiation uses sygus, but it is not a sygus problem
 882     return true;
 883   }
 884   return false;
 885 }
 886
 887 bool SetDefaults::incompatibleWithProofs(Options& opts,
 888                                          std::ostream& reason) const
 889 {
 890   if (opts.quantifiers.globalNegate)
 891   {
 892     // When global negate answers "unsat", it is not due to showing a set of
 893     // formulas is unsat. Thus, proofs do not apply.
 894     reason << "global-negate";
 895     return true;
 896   }
 897   if (isSygus(opts))
 898   {
 899     // When sygus answers "unsat", it is not due to showing a set of
 900     // formulas is unsat in the standard way. Thus, proofs do not apply.
 901     reason << "sygus";
 902     return true;
 903   }
 904   // options that are automatically set to support proofs
 905   if (opts.bv.bvAssertInput)
 906   {
 907     Notice()
 908         << "Disabling bv-assert-input since it is incompatible with proofs."
 909         << std::endl;
 910     opts.bv.bvAssertInput = false;
 911   }
 912   // If proofs are required and the user did not specify a specific BV solver,
 913   // we make sure to use the proof producing BITBLAST_INTERNAL solver.
 914   if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
 915       && !opts.bv.bvSolverWasSetByUser
 916       && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
 917   {
 918     Notice() << "Forcing internal bit-vector solver due to proof production."
 919              << std::endl;
 920     opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
 921   }
 922   return false;
 923 }
 924
 925 bool SetDefaults::incompatibleWithModels(const Options& opts,
 926                                          std::ostream& reason) const
 927 {
 928   if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
 929   {
 930     reason << "unconstrained-simp";
 931     return true;
 932   }
 933   else if (opts.smt.sortInference)
 934   {
 935     reason << "sort-inference";
 936     return true;
 937   }
 938   else if (opts.prop.minisatUseElim)
 939   {
 940     reason << "minisat-elimination";
 941     return true;
 942   }
 943   else if (opts.quantifiers.globalNegate)
 944   {
 945     reason << "global-negate";
 946     return true;
 947   }
 948   return false;
 949 }
 950
 951 bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
 952                                               Options& opts,
 953                                               std::ostream& reason,
 954                                               std::ostream& suggest) const
 955 {
 956   if (opts.smt.ackermann)
 957   {
 958     reason << "ackermann";
 959     return true;
 960   }
 961   if (opts.smt.unconstrainedSimp)
 962   {
 963     if (opts.smt.unconstrainedSimpWasSetByUser)
 964     {
 965       reason << "unconstrained simplification";
 966       return true;
 967     }
 968     Notice() << "SolverEngine: turning off unconstrained simplification to "
 969                 "support incremental solving"
 970              << std::endl;
 971     opts.smt.unconstrainedSimp = false;
 972   }
 973   if (opts.bv.bitblastMode == options::BitblastMode::EAGER
 974       && !logic.isPure(THEORY_BV))
 975   {
 976     reason << "eager bit-blasting in non-QF_BV logic";
 977     suggest << "Try --bitblast=lazy.";
 978     return true;
 979   }
 980   if (opts.quantifiers.sygusInference)
 981   {
 982     if (opts.quantifiers.sygusInferenceWasSetByUser)
 983     {
 984       reason << "sygus inference";
 985       return true;
 986     }
 987     Notice() << "SolverEngine: turning off sygus inference to support "
 988                 "incremental solving"
 989              << std::endl;
 990     opts.quantifiers.sygusInference = false;
 991   }
 992   if (opts.smt.solveIntAsBV > 0)
 993   {
 994     reason << "solveIntAsBV";
 995     return true;
 996   }
 997
 998   // disable modes not supported by incremental
 999   opts.smt.sortInference = false;
1000   opts.uf.ufssFairnessMonotone = false;
1001   opts.quantifiers.globalNegate = false;
1002   opts.quantifiers.cegqiNestedQE = false;
1003   opts.bv.bvAbstraction = false;
1004   opts.arith.arithMLTrick = false;
1005
1006   return false;
1007 }
1008
1009 bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
1010                                              std::ostream& reason) const
1011 {
1012   if (opts.smt.simplificationMode != options::SimplificationMode::NONE)
1013   {
1014     if (opts.smt.simplificationModeWasSetByUser)
1015     {
1016       reason << "simplification";
1017       return true;
1018     }
1019     Notice() << "SolverEngine: turning off simplification to support unsat "
1020                 "cores"
1021              << std::endl;
1022     opts.smt.simplificationMode = options::SimplificationMode::NONE;
1023   }
1024
1025   if (opts.smt.learnedRewrite)
1026   {
1027     if (opts.smt.learnedRewriteWasSetByUser)
1028     {
1029       reason << "learned rewrites";
1030       return true;
1031     }
1032     Notice() << "SolverEngine: turning off learned rewrites to support "
1033                 "unsat cores\n";
1034     opts.smt.learnedRewrite = false;
1035   }
1036
1037   if (opts.arith.pbRewrites)
1038   {
1039     if (opts.arith.pbRewritesWasSetByUser)
1040     {
1041       reason << "pseudoboolean rewrites";
1042       return true;
1043     }
1044     Notice() << "SolverEngine: turning off pseudoboolean rewrites to support "
1045                 "unsat cores\n";
1046     opts.arith.pbRewrites = false;
1047   }
1048
1049   if (opts.smt.sortInference)
1050   {
1051     if (opts.smt.sortInferenceWasSetByUser)
1052     {
1053       reason << "sort inference";
1054       return true;
1055     }
1056     Notice() << "SolverEngine: turning off sort inference to support unsat "
1057                 "cores\n";
1058     opts.smt.sortInference = false;
1059   }
1060
1061   if (opts.quantifiers.preSkolemQuant)
1062   {
1063     if (opts.quantifiers.preSkolemQuantWasSetByUser)
1064     {
1065       reason << "pre-skolemization";
1066       return true;
1067     }
1068     Notice() << "SolverEngine: turning off pre-skolemization to support "
1069                 "unsat cores\n";
1070     opts.quantifiers.preSkolemQuant = false;
1071   }
1072
1073   if (opts.bv.bitvectorToBool)
1074   {
1075     if (opts.bv.bitvectorToBoolWasSetByUser)
1076     {
1077       reason << "bv-to-bool";
1078       return true;
1079     }
1080     Notice() << "SolverEngine: turning off bitvector-to-bool to support "
1081                 "unsat cores\n";
1082     opts.bv.bitvectorToBool = false;
1083   }
1084
1085   if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
1086   {
1087     if (opts.bv.boolToBitvectorWasSetByUser)
1088     {
1089       reason << "bool-to-bv != off";
1090       return true;
1091     }
1092     Notice() << "SolverEngine: turning off bool-to-bv to support unsat cores\n";
1093     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
1094   }
1095
1096   if (opts.bv.bvIntroducePow2)
1097   {
1098     if (opts.bv.bvIntroducePow2WasSetByUser)
1099     {
1100       reason << "bv-intro-pow2";
1101       return true;
1102     }
1103     Notice()
1104         << "SolverEngine: turning off bv-intro-pow2 to support unsat cores";
1105     opts.bv.bvIntroducePow2 = false;
1106   }
1107
1108   if (opts.smt.repeatSimp)
1109   {
1110     if (opts.smt.repeatSimpWasSetByUser)
1111     {
1112       reason << "repeat-simp";
1113       return true;
1114     }
1115     Notice()
1116         << "SolverEngine: turning off repeat-simp to support unsat cores\n";
1117     opts.smt.repeatSimp = false;
1118   }
1119
1120   if (opts.quantifiers.globalNegate)
1121   {
1122     if (opts.quantifiers.globalNegateWasSetByUser)
1123     {
1124       reason << "global-negate";
1125       return true;
1126     }
1127     Notice() << "SolverEngine: turning off global-negate to support unsat "
1128                 "cores\n";
1129     opts.quantifiers.globalNegate = false;
1130   }
1131
1132   if (opts.bv.bitvectorAig)
1133   {
1134     reason << "bitblast-aig";
1135     return true;
1136   }
1137
1138   if (opts.smt.doITESimp)
1139   {
1140     reason << "ITE simp";
1141     return true;
1142   }
1143   if (opts.smt.unconstrainedSimp)
1144   {
1145     if (opts.smt.unconstrainedSimpWasSetByUser)
1146     {
1147       reason << "unconstrained simplification";
1148       return true;
1149     }
1150     Notice() << "SolverEngine: turning off unconstrained simplification to "
1151                 "support unsat cores"
1152              << std::endl;
1153     opts.smt.unconstrainedSimp = false;
1154   }
1155   return false;
1156 }
1157
1158 bool SetDefaults::safeUnsatCores(const Options& opts) const
1159 {
1160   // whether we want to force safe unsat cores, i.e., if we are in the default
1161   // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental
1162   return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS
1163          || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY;
1164 }
1165
1166 bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
1167                                               std::ostream& reason) const
1168 {
1169   if (opts.smt.ackermann)
1170   {
1171     reason << "ackermann";
1172     return true;
1173   }
1174   if (opts.arith.nlRlvMode != options::NlRlvMode::NONE)
1175   {
1176     // Theory relevance is incompatible with CEGQI and SyQI, since there is no
1177     // appropriate policy for the relevance of counterexample lemmas (when their
1178     // guard is entailed to be false, the entire lemma is relevant, not just the
1179     // guard). Hence, we throw an option exception if quantifiers are enabled.
1180     reason << "--nl-ext-rlv";
1181     return true;
1182   }
1183   return false;
1184 }
1185
1186 void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
1187 {
1188   bool needsUf = false;
1189   // strings require LIA, UF; widen the logic
1190   if (logic.isTheoryEnabled(THEORY_STRINGS))
1191   {
1192     LogicInfo log(logic.getUnlockedCopy());
1193     // Strings requires arith for length constraints, and also UF
1194     needsUf = true;
1195     if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
1196     {
1197       Notice()
1198           << "Enabling linear integer arithmetic because strings are enabled"
1199           << std::endl;
1200       log.enableTheory(THEORY_ARITH);
1201       log.enableIntegers();
1202       log.arithOnlyLinear();
1203     }
1204     else if (!logic.areIntegersUsed())
1205     {
1206       Notice() << "Enabling integer arithmetic because strings are enabled"
1207                << std::endl;
1208       log.enableIntegers();
1209     }
1210     logic = log;
1211     logic.lock();
1212   }
1213   if (opts.bv.bvAbstraction)
1214   {
1215     // bv abstraction may require UF
1216     Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
1217     needsUf = true;
1218   }
1219   else if (opts.quantifiers.preSkolemQuantNested
1220            && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
1221   {
1222     // if pre-skolem nested is explictly set, then we require UF. If it is
1223     // not explicitly set, it is disabled below if UF is not present.
1224     Notice() << "Enabling UF because preSkolemQuantNested requires it."
1225              << std::endl;
1226     needsUf = true;
1227   }
1228   if (needsUf
1229       // Arrays, datatypes and sets permit Boolean terms and thus require UF
1230       || logic.isTheoryEnabled(THEORY_ARRAYS)
1231       || logic.isTheoryEnabled(THEORY_DATATYPES)
1232       || logic.isTheoryEnabled(THEORY_SETS)
1233       || logic.isTheoryEnabled(THEORY_BAGS)
1234       // Non-linear arithmetic requires UF to deal with division/mod because
1235       // their expansion introduces UFs for the division/mod-by-zero case.
1236       // If we are eliminating non-linear arithmetic via solve-int-as-bv,
1237       // then this is not required, since non-linear arithmetic will be
1238       // eliminated altogether (or otherwise fail at preprocessing).
1239       || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
1240           && opts.smt.solveIntAsBV == 0)
1241       // FP requires UF since there are multiple operators that are partially
1242       // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more
1243       // details).
1244       || logic.isTheoryEnabled(THEORY_FP))
1245   {
1246     if (!logic.isTheoryEnabled(THEORY_UF))
1247     {
1248       LogicInfo log(logic.getUnlockedCopy());
1249       if (!needsUf)
1250       {
1251         Notice() << "Enabling UF because " << logic << " requires it."
1252                  << std::endl;
1253       }
1254       log.enableTheory(THEORY_UF);
1255       logic = log;
1256       logic.lock();
1257     }
1258   }
1259   if (opts.arith.arithMLTrick)
1260   {
1261     if (!logic.areIntegersUsed())
1262     {
1263       // enable integers
1264       LogicInfo log(logic.getUnlockedCopy());
1265       Notice() << "Enabling integers because arithMLTrick requires it."
1266                << std::endl;
1267       log.enableIntegers();
1268       logic = log;
1269       logic.lock();
1270     }
1271   }
1272 }
1273
1274 void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
1275                                          Options& opts) const
1276 {
1277   if (opts.arrays.arraysExp)
1278   {
1279     // Allows to answer sat more often by default.
1280     if (!opts.quantifiers.fmfBoundWasSetByUser)
1281     {
1282       opts.quantifiers.fmfBound = true;
1283       Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
1284     }
1285   }
1286   if (logic.hasCardinalityConstraints())
1287   {
1288     // must have finite model finding on
1289     opts.quantifiers.finiteModelFind = true;
1290   }
1291
1292   if (opts.quantifiers.instMaxLevel != -1)
1293   {
1294     Notice() << "SolverEngine: turning off cbqi to support instMaxLevel"
1295              << std::endl;
1296     opts.quantifiers.cegqi = false;
1297   }
1298
1299   if ((opts.quantifiers.fmfBoundLazyWasSetByUser
1300        && opts.quantifiers.fmfBoundLazy)
1301       || (opts.quantifiers.fmfBoundIntWasSetByUser
1302           && opts.quantifiers.fmfBoundInt))
1303   {
1304     opts.quantifiers.fmfBound = true;
1305     Trace("smt")
1306         << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n";
1307   }
1308   // now have determined whether fmfBound is on/off
1309   // apply fmfBound options
1310   if (opts.quantifiers.fmfBound)
1311   {
1312     if (!opts.quantifiers.mbqiModeWasSetByUser
1313         || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE
1314             && opts.quantifiers.mbqiMode != options::MbqiMode::FMC))
1315     {
1316       // if bounded integers are set, use no MBQI by default
1317       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
1318     }
1319     if (!opts.quantifiers.prenexQuantUserWasSetByUser)
1320     {
1321       opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
1322     }
1323   }
1324   if (logic.isHigherOrder())
1325   {
1326     // if higher-order, then current variants of model-based instantiation
1327     // cannot be used
1328     if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE)
1329     {
1330       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
1331     }
1332     if (!opts.quantifiers.hoElimStoreAxWasSetByUser)
1333     {
1334       // by default, use store axioms only if --ho-elim is set
1335       opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim;
1336     }
1337     // Cannot use macros, since lambda lifting and macro elimination are inverse
1338     // operations.
1339     if (opts.quantifiers.macrosQuant)
1340     {
1341       opts.quantifiers.macrosQuant = false;
1342     }
1343     // HOL is incompatible with fmfBound
1344     if (opts.quantifiers.fmfBound)
1345     {
1346       if (opts.quantifiers.fmfBoundWasSetByUser
1347           || opts.quantifiers.fmfBoundLazyWasSetByUser
1348           || opts.quantifiers.fmfBoundIntWasSetByUser)
1349       {
1350         Notice() << "Disabling bound finite-model finding since it is "
1351                     "incompatible with HOL.\n";
1352       }
1353
1354       opts.quantifiers.fmfBound = false;
1355       Trace("smt") << "turning off fmf-bound, since HOL\n";
1356     }
1357   }
1358   if (opts.quantifiers.fmfFunWellDefinedRelevant)
1359   {
1360     if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
1361     {
1362       opts.quantifiers.fmfFunWellDefined = true;
1363     }
1364   }
1365   if (opts.quantifiers.fmfFunWellDefined)
1366   {
1367     if (!opts.quantifiers.finiteModelFindWasSetByUser)
1368     {
1369       opts.quantifiers.finiteModelFind = true;
1370     }
1371   }
1372
1373   // now, have determined whether finite model find is on/off
1374   // apply finite model finding options
1375   if (opts.quantifiers.finiteModelFind)
1376   {
1377     // apply conservative quantifiers splitting
1378     if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
1379     {
1380       opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT;
1381     }
1382     if (!opts.quantifiers.eMatchingWasSetByUser)
1383     {
1384       opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
1385     }
1386     if (!opts.quantifiers.instWhenModeWasSetByUser)
1387     {
1388       // instantiate only on last call
1389       if (opts.quantifiers.eMatching)
1390       {
1391         opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
1392       }
1393     }
1394   }
1395
1396   // apply sygus options
1397   // if we are attempting to rewrite everything to SyGuS, use sygus()
1398   if (usesSygus(opts))
1399   {
1400     setDefaultsSygus(opts);
1401   }
1402   // counterexample-guided instantiation for non-sygus
1403   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1404   if ((logic.isQuantified()
1405        && (logic.isTheoryEnabled(THEORY_ARITH)
1406            || logic.isTheoryEnabled(THEORY_DATATYPES)
1407            || logic.isTheoryEnabled(THEORY_BV)
1408            || logic.isTheoryEnabled(THEORY_FP)))
1409       || opts.quantifiers.cegqiAll)
1410   {
1411     if (!opts.quantifiers.cegqiWasSetByUser)
1412     {
1413       opts.quantifiers.cegqi = true;
1414     }
1415     // check whether we should apply full cbqi
1416     if (logic.isPure(THEORY_BV))
1417     {
1418       if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
1419       {
1420         opts.quantifiers.cegqiFullEffort = true;
1421       }
1422     }
1423   }
1424   if (opts.quantifiers.cegqi)
1425   {
1426     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
1427     {
1428       if (!opts.quantifiers.quantConflictFindWasSetByUser)
1429       {
1430         opts.quantifiers.quantConflictFind = false;
1431       }
1432       if (!opts.quantifiers.instNoEntailWasSetByUser)
1433       {
1434         opts.quantifiers.instNoEntail = false;
1435       }
1436       if (!opts.quantifiers.instWhenModeWasSetByUser
1437           && opts.quantifiers.cegqiModel)
1438       {
1439         // only instantiation should happen at last call when model is avaiable
1440         opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
1441       }
1442     }
1443     else
1444     {
1445       // only supported in pure arithmetic or pure BV
1446       opts.quantifiers.cegqiNestedQE = false;
1447     }
1448     if (opts.quantifiers.globalNegate)
1449     {
1450       if (!opts.quantifiers.prenexQuantWasSetByUser)
1451       {
1452         opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
1453       }
1454     }
1455   }
1456   // implied options...
1457   if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
1458   {
1459     opts.quantifiers.quantConflictFind = true;
1460   }
1461   if (opts.quantifiers.cegqiNestedQE)
1462   {
1463     opts.quantifiers.prenexQuantUser = true;
1464     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
1465     {
1466       opts.quantifiers.preSkolemQuant = true;
1467     }
1468   }
1469   // for induction techniques
1470   if (opts.quantifiers.quantInduction)
1471   {
1472     if (!opts.quantifiers.dtStcInductionWasSetByUser)
1473     {
1474       opts.quantifiers.dtStcInduction = true;
1475     }
1476     if (!opts.quantifiers.intWfInductionWasSetByUser)
1477     {
1478       opts.quantifiers.intWfInduction = true;
1479     }
1480   }
1481   if (opts.quantifiers.dtStcInduction)
1482   {
1483     // try to remove ITEs from quantified formulas
1484     if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser)
1485     {
1486       opts.quantifiers.iteDtTesterSplitQuant = true;
1487     }
1488     if (!opts.quantifiers.iteLiftQuantWasSetByUser)
1489     {
1490       opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL;
1491     }
1492   }
1493   if (opts.quantifiers.intWfInduction)
1494   {
1495     if (!opts.quantifiers.purifyTriggersWasSetByUser)
1496     {
1497       opts.quantifiers.purifyTriggers = true;
1498     }
1499   }
1500   if (opts.quantifiers.conjectureNoFilter)
1501   {
1502     if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser)
1503     {
1504       opts.quantifiers.conjectureFilterActiveTerms = false;
1505     }
1506     if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser)
1507     {
1508       opts.quantifiers.conjectureFilterCanonical = false;
1509     }
1510     if (!opts.quantifiers.conjectureFilterModelWasSetByUser)
1511     {
1512       opts.quantifiers.conjectureFilterModel = false;
1513     }
1514   }
1515   if (opts.quantifiers.conjectureGenPerRoundWasSetByUser)
1516   {
1517     if (opts.quantifiers.conjectureGenPerRound > 0)
1518     {
1519       opts.quantifiers.conjectureGen = true;
1520     }
1521     else
1522     {
1523       opts.quantifiers.conjectureGen = false;
1524     }
1525   }
1526   // can't pre-skolemize nested quantifiers without UF theory
1527   if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant)
1528   {
1529     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
1530     {
1531       opts.quantifiers.preSkolemQuantNested = false;
1532     }
1533   }
1534   if (!logic.isTheoryEnabled(THEORY_DATATYPES))
1535   {
1536     opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE;
1537   }
1538 }
1539
1540 void SetDefaults::setDefaultsSygus(Options& opts) const
1541 {
1542   if (!opts.quantifiers.sygus)
1543   {
1544     Trace("smt") << "turning on sygus" << std::endl;
1545   }
1546   opts.quantifiers.sygus = true;
1547   // must use Ferrante/Rackoff for real arithmetic
1548   if (!opts.quantifiers.cegqiMidpointWasSetByUser)
1549   {
1550     opts.quantifiers.cegqiMidpoint = true;
1551   }
1552   // must disable cegqi-bv since it may introduce witness terms, which
1553   // cannot appear in synthesis solutions
1554   if (!opts.quantifiers.cegqiBvWasSetByUser)
1555   {
1556     opts.quantifiers.cegqiBv = false;
1557   }
1558   if (opts.quantifiers.sygusRepairConst)
1559   {
1560     if (!opts.quantifiers.cegqiWasSetByUser)
1561     {
1562       opts.quantifiers.cegqi = true;
1563     }
1564   }
1565   if (opts.quantifiers.sygusInference)
1566   {
1567     // optimization: apply preskolemization, makes it succeed more often
1568     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
1569     {
1570       opts.quantifiers.preSkolemQuant = true;
1571     }
1572     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
1573     {
1574       opts.quantifiers.preSkolemQuantNested = true;
1575     }
1576   }
1577   // counterexample-guided instantiation for sygus
1578   if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
1579   {
1580     opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
1581   }
1582   if (!opts.quantifiers.quantConflictFindWasSetByUser)
1583   {
1584     opts.quantifiers.quantConflictFind = false;
1585   }
1586   if (!opts.quantifiers.instNoEntailWasSetByUser)
1587   {
1588     opts.quantifiers.instNoEntail = false;
1589   }
1590   if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
1591   {
1592     // should use full effort cbqi for single invocation and repair const
1593     opts.quantifiers.cegqiFullEffort = true;
1594   }
1595   if (opts.quantifiers.sygusRew)
1596   {
1597     opts.quantifiers.sygusRewSynth = true;
1598     opts.quantifiers.sygusRewVerify = true;
1599   }
1600   if (opts.quantifiers.sygusRewSynthInput)
1601   {
1602     // If we are using synthesis rewrite rules from input, we use
1603     // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
1604     // details on this technique.
1605     opts.quantifiers.sygusRewSynth = true;
1606     // we should not use the extended rewriter, since we are interested
1607     // in rewrites that are not in the main rewriter
1608     if (!opts.quantifiers.sygusExtRewWasSetByUser)
1609     {
1610       opts.quantifiers.sygusExtRew = false;
1611     }
1612   }
1613   // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
1614   // is one that is specialized for returning a single solution. Non-basic
1615   // sygus algorithms currently include the PBE solver, UNIF+PI, static
1616   // template inference for invariant synthesis, and single invocation
1617   // techniques.
1618   bool reqBasicSygus = false;
1619   if (opts.smt.produceAbducts)
1620   {
1621     // if doing abduction, we should filter strong solutions
1622     if (!opts.quantifiers.sygusFilterSolModeWasSetByUser)
1623     {
1624       opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG;
1625     }
1626     // we must use basic sygus algorithms, since e.g. we require checking
1627     // a sygus side condition for consistency with axioms.
1628     reqBasicSygus = true;
1629   }
1630   if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify
1631       || opts.quantifiers.sygusQueryGen)
1632   {
1633     // rewrite rule synthesis implies that sygus stream must be true
1634     opts.quantifiers.sygusStream = true;
1635   }
1636   if (opts.quantifiers.sygusStream || opts.base.incrementalSolving)
1637   {
1638     // Streaming and incremental mode are incompatible with techniques that
1639     // focus the search towards finding a single solution.
1640     reqBasicSygus = true;
1641   }
1642   // Now, disable options for non-basic sygus algorithms, if necessary.
1643   if (reqBasicSygus)
1644   {
1645     if (!opts.quantifiers.sygusUnifPbeWasSetByUser)
1646     {
1647       opts.quantifiers.sygusUnifPbe = false;
1648     }
1649     if (opts.quantifiers.sygusUnifPiWasSetByUser)
1650     {
1651       opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE;
1652     }
1653     if (!opts.quantifiers.sygusInvTemplModeWasSetByUser)
1654     {
1655       opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE;
1656     }
1657     if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
1658     {
1659       opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
1660     }
1661   }
1662   // do not miniscope
1663   if (!opts.quantifiers.miniscopeQuantWasSetByUser)
1664   {
1665     opts.quantifiers.miniscopeQuant = false;
1666   }
1667   if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
1668   {
1669     opts.quantifiers.miniscopeQuantFreeVar = false;
1670   }
1671   if (!opts.quantifiers.quantSplitWasSetByUser)
1672   {
1673     opts.quantifiers.quantSplit = false;
1674   }
1675   // do not do macros
1676   if (!opts.quantifiers.macrosQuantWasSetByUser)
1677   {
1678     opts.quantifiers.macrosQuant = false;
1679   }
1680 }
1681 void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
1682                                          Options& opts) const
1683 {
1684   // Set decision mode based on logic (if not set by user)
1685   if (opts.decision.decisionModeWasSetByUser)
1686   {
1687     return;
1688   }
1689   options::DecisionMode decMode =
1690       // anything that uses sygus uses internal
1691       usesSygus(opts) ? options::DecisionMode::INTERNAL :
1692                       // ALL or its supersets
1693           logic.hasEverything()
1694               ? options::DecisionMode::JUSTIFICATION
1695               : (  // QF_BV
1696                     (not logic.isQuantified() && logic.isPure(THEORY_BV)) ||
1697                             // QF_AUFBV or QF_ABV or QF_UFBV
1698                             (not logic.isQuantified()
1699                              && (logic.isTheoryEnabled(THEORY_ARRAYS)
1700                                  || logic.isTheoryEnabled(THEORY_UF))
1701                              && logic.isTheoryEnabled(THEORY_BV))
1702                             ||
1703                             // QF_AUFLIA (and may be ends up enabling
1704                             // QF_AUFLRA?)
1705                             (not logic.isQuantified()
1706                              && logic.isTheoryEnabled(THEORY_ARRAYS)
1707                              && logic.isTheoryEnabled(THEORY_UF)
1708                              && logic.isTheoryEnabled(THEORY_ARITH))
1709                             ||
1710                             // QF_LRA
1711                             (not logic.isQuantified()
1712                              && logic.isPure(THEORY_ARITH) && logic.isLinear()
1713                              && !logic.isDifferenceLogic()
1714                              && !logic.areIntegersUsed())
1715                             ||
1716                             // Quantifiers
1717                             logic.isQuantified() ||
1718                             // Strings
1719                             logic.isTheoryEnabled(THEORY_STRINGS)
1720                         ? options::DecisionMode::JUSTIFICATION
1721                         : options::DecisionMode::INTERNAL);
1722
1723   bool stoponly =
1724       // ALL or its supersets
1725       logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
1726           ? false
1727           : (  // QF_AUFLIA
1728                 (not logic.isQuantified()
1729                  && logic.isTheoryEnabled(THEORY_ARRAYS)
1730                  && logic.isTheoryEnabled(THEORY_UF)
1731                  && logic.isTheoryEnabled(THEORY_ARITH))
1732                         ||
1733                         // QF_LRA
1734                         (not logic.isQuantified() && logic.isPure(THEORY_ARITH)
1735                          && logic.isLinear() && !logic.isDifferenceLogic()
1736                          && !logic.areIntegersUsed())
1737                     ? true
1738                     : false);
1739
1740   opts.decision.decisionMode = decMode;
1741   if (stoponly)
1742   {
1743     if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
1744     {
1745       opts.decision.decisionMode = options::DecisionMode::STOPONLY;
1746     }
1747     else
1748     {
1749       Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
1750     }
1751   }
1752   Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
1753                << std::endl;
1754 }
1755
1756 }  // namespace smt
1757 }  // namespace cvc5