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