GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/set_defaults.cpp Lines: 558 694 80.4 %
Date: 2021-03-23 Branches: 1700 3556 47.8 %

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