GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/options.cpp Lines: 2926 9150 32.0 %
Date: 2021-03-23 Branches: 3193 28919 11.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file options_template.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Andrew Reynolds
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 Contains code for handling command-line options.
13
 **
14
 ** Contains code for handling command-line options
15
 **/
16
17
#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
18
// force use of optreset; mingw32 croaks on argv-switching otherwise
19
#  include "cvc4autoconfig.h"
20
#  define _BSD_SOURCE
21
#  undef HAVE_DECL_OPTRESET
22
#  define HAVE_DECL_OPTRESET 1
23
#  define CVC4_IS_NOT_REALLY_BSD
24
#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
25
26
#ifdef __MINGW64__
27
extern int optreset;
28
#endif /* __MINGW64__ */
29
30
#include <getopt.h>
31
32
// clean up
33
#ifdef CVC4_IS_NOT_REALLY_BSD
34
#  undef _BSD_SOURCE
35
#endif /* CVC4_IS_NOT_REALLY_BSD */
36
37
#include <unistd.h>
38
#include <string.h>
39
#include <time.h>
40
41
#include <cstdio>
42
#include <cstdlib>
43
#include <cstring>
44
#include <iomanip>
45
#include <new>
46
#include <string>
47
#include <sstream>
48
#include <limits>
49
50
#include "base/check.h"
51
#include "base/exception.h"
52
#include "base/output.h"
53
#include "options/didyoumean.h"
54
#include "options/language.h"
55
#include "options/options_handler.h"
56
#include "options/options_listener.h"
57
58
#include "options/arith_options.h"
59
#include "options/arrays_options.h"
60
#include "options/base_options.h"
61
#include "options/booleans_options.h"
62
#include "options/builtin_options.h"
63
#include "options/bv_options.h"
64
#include "options/datatypes_options.h"
65
#include "options/decision_options.h"
66
#include "options/expr_options.h"
67
#include "options/fp_options.h"
68
#include "options/main_options.h"
69
#include "options/parser_options.h"
70
#include "options/printer_options.h"
71
#include "options/proof_options.h"
72
#include "options/prop_options.h"
73
#include "options/quantifiers_options.h"
74
#include "options/sep_options.h"
75
#include "options/sets_options.h"
76
#include "options/smt_options.h"
77
#include "options/strings_options.h"
78
#include "options/theory_options.h"
79
#include "options/uf_options.h"
80
81
82
#include "options/options_holder.h"
83
#include "cvc4autoconfig.h"
84
#include "options/base_handlers.h"
85
86
87
88
89
using namespace CVC4;
90
using namespace CVC4::options;
91
92
namespace CVC4 {
93
94
thread_local Options* Options::s_current = NULL;
95
96
/**
97
 * This is a default handler for options of built-in C++ type.  This
98
 * template is really just a helper for the handleOption() template,
99
 * below.  Variants of this template handle numeric and non-numeric,
100
 * integral and non-integral, signed and unsigned C++ types.
101
 * handleOption() makes sure to instantiate the right one.
102
 *
103
 * This implements default behavior when e.g. an option is
104
 * unsigned but the user specifies a negative argument; etc.
105
 */
106
template <class T, bool is_numeric, bool is_integer>
107
struct OptionHandler {
108
  static T handle(std::string option, std::string optionarg);
109
};/* struct OptionHandler<> */
110
111
/** Variant for integral C++ types */
112
template <class T>
113
struct OptionHandler<T, true, true> {
114
110
  static bool stringToInt(T& t, const std::string& str) {
115
220
    std::istringstream ss(str);
116
110
    ss >> t;
117
    char tmp;
118
220
    return !(ss.fail() || ss.get(tmp));
119
  }
120
121
79
  static bool containsMinus(const std::string& str) {
122
79
    return str.find('-') != std::string::npos;
123
  }
124
125
110
  static T handle(const std::string& option, const std::string& optionarg) {
126
    try {
127
      T i;
128
110
      bool success = stringToInt(i, optionarg);
129
130
110
      if(!success){
131
        throw OptionException(option + ": failed to parse "+ optionarg +
132
                              " as an integer of the appropriate type.");
133
      }
134
135
      // Depending in the platform unsigned numbers with '-' signs may parse.
136
      // Reject these by looking for any minus if it is not signed.
137
79
      if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
138
        // unsigned type but user gave negative argument
139
        throw OptionException(option + " requires a nonnegative argument");
140
110
      } else if(i < std::numeric_limits<T>::min()) {
141
        // negative overflow for type
142
        std::stringstream ss;
143
        ss << option << " requires an argument >= "
144
           << std::numeric_limits<T>::min();
145
        throw OptionException(ss.str());
146
110
      } else if(i > std::numeric_limits<T>::max()) {
147
        // positive overflow for type
148
        std::stringstream ss;
149
        ss << option << " requires an argument <= "
150
           << std::numeric_limits<T>::max();
151
        throw OptionException(ss.str());
152
      }
153
154
110
      return i;
155
156
      // if(std::numeric_limits<T>::is_signed) {
157
      //   return T(i.getLong());
158
      // } else {
159
      //   return T(i.getUnsignedLong());
160
      // }
161
    } catch(std::invalid_argument&) {
162
      // user gave something other than an integer
163
      throw OptionException(option + " requires an integer argument");
164
    }
165
  }
166
};/* struct OptionHandler<T, true, true> */
167
168
/** Variant for numeric but non-integral C++ types */
169
template <class T>
170
struct OptionHandler<T, true, false> {
171
  static T handle(std::string option, std::string optionarg) {
172
    std::stringstream in(optionarg);
173
    long double r;
174
    in >> r;
175
    if(! in.eof()) {
176
      // we didn't consume the whole string (junk at end)
177
      throw OptionException(option + " requires a numeric argument");
178
    }
179
180
    if(! std::numeric_limits<T>::is_signed && r < 0.0) {
181
      // unsigned type but user gave negative value
182
      throw OptionException(option + " requires a nonnegative argument");
183
    } else if(r < -std::numeric_limits<T>::max()) {
184
      // negative overflow for type
185
      std::stringstream ss;
186
      ss << option << " requires an argument >= "
187
         << -std::numeric_limits<T>::max();
188
      throw OptionException(ss.str());
189
    } else if(r > std::numeric_limits<T>::max()) {
190
      // positive overflow for type
191
      std::stringstream ss;
192
      ss << option << " requires an argument <= "
193
         << std::numeric_limits<T>::max();
194
      throw OptionException(ss.str());
195
    }
196
197
    return T(r);
198
  }
199
};/* struct OptionHandler<T, true, false> */
200
201
/** Variant for non-numeric C++ types */
202
template <class T>
203
struct OptionHandler<T, false, false> {
204
  static T handle(std::string option, std::string optionarg) {
205
    T::unsupported_handleOption_call___please_write_me;
206
    // The above line causes a compiler error if this version of the template
207
    // is ever instantiated (meaning that a specialization is missing).  So
208
    // don't worry about the segfault in the next line, the "return" is only
209
    // there to keep the compiler from giving additional, distracting errors
210
    // and warnings.
211
    return *(T*)0;
212
  }
213
};/* struct OptionHandler<T, false, false> */
214
215
/** Handle an option of type T in the default way. */
216
template <class T>
217
110
T handleOption(std::string option, std::string optionarg) {
218
110
  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
219
}
220
221
/** Handle an option of type std::string in the default way. */
222
template <>
223
12
std::string handleOption<std::string>(std::string option, std::string optionarg) {
224
12
  return optionarg;
225
}
226
227
/**
228
 * Run handler, and any user-given predicates, for option T.
229
 * If a user specifies a :handler or :predicates, it overrides this.
230
 */
231
template <class T>
232
typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) {
233
  // By default, parse the option argument in a way appropriate for its type.
234
  // E.g., for "unsigned int" options, ensure that the provided argument is
235
  // a nonnegative integer that fits in the unsigned int type.
236
237
  return handleOption<typename T::type>(option, optionarg);
238
}
239
240
template <class T>
241
14473
void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) {
242
  // By default, nothing to do for bool.  Users add things with
243
  // :predicate in options files to provide custom checking routines
244
  // that can throw exceptions.
245
14473
}
246
247
27323
Options::Options(OptionsListener* ol)
248
27323
    : d_holder(new options::OptionsHolder()),
249
27323
      d_handler(new options::OptionsHandler(this)),
250
54646
      d_olisten(ol)
251
27323
{}
252
253
49620
Options::~Options() {
254
24810
  delete d_handler;
255
24810
  delete d_holder;
256
24810
}
257
258
13713
void Options::copyValues(const Options& options){
259
13713
  if(this != &options) {
260
13713
    delete d_holder;
261
13713
    d_holder = new options::OptionsHolder(*options.d_holder);
262
  }
263
13713
}
264
265
std::string Options::formatThreadOptionException(const std::string& option) {
266
  std::stringstream ss;
267
  ss << "can't understand option `" << option
268
     << "': expected something like --threadN=\"--option1 --option2\","
269
     << " where N is a nonnegative integer";
270
  return ss.str();
271
}
272
273
9621
void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
274
275
template <> options::maxApproxDepth__option_t::type runHandlerAndPredicates(
276
    options::maxApproxDepth__option_t,
277
    std::string option,
278
    std::string optionarg,
279
    options::OptionsHandler* handler)
280
{
281
  options::maxApproxDepth__option_t::type retval = handleOption<int16_t>(option, optionarg);
282
283
  return retval;
284
}
285
template <> void Options::assign(
286
    options::maxApproxDepth__option_t,
287
    std::string option,
288
    std::string value)
289
{
290
  d_holder->maxApproxDepth =
291
    runHandlerAndPredicates(options::maxApproxDepth, option, value, d_handler);
292
  d_holder->maxApproxDepth__setByUser__ = true;
293
  Trace("options") << "user assigned option maxApproxDepth" << std::endl;
294
295
}
296
4
template <> void Options::assignBool(
297
    options::brabTest__option_t,
298
    std::string option,
299
    bool value)
300
{
301
4
  runBoolPredicates(options::brabTest, option, value, d_handler);
302
4
  d_holder->brabTest = value;
303
4
  d_holder->brabTest__setByUser__ = true;
304
4
  Trace("options") << "user assigned option brabTest" << std::endl;
305
306
4
}
307
3
template <> void Options::assignBool(
308
    options::arithNoPartialFun__option_t,
309
    std::string option,
310
    bool value)
311
{
312
3
  runBoolPredicates(options::arithNoPartialFun, option, value, d_handler);
313
3
  d_holder->arithNoPartialFun = value;
314
3
  d_holder->arithNoPartialFun__setByUser__ = true;
315
3
  Trace("options") << "user assigned option arithNoPartialFun" << std::endl;
316
317
3
}
318
template <> options::arithPropAsLemmaLength__option_t::type runHandlerAndPredicates(
319
    options::arithPropAsLemmaLength__option_t,
320
    std::string option,
321
    std::string optionarg,
322
    options::OptionsHandler* handler)
323
{
324
  options::arithPropAsLemmaLength__option_t::type retval = handleOption<uint16_t>(option, optionarg);
325
326
  return retval;
327
}
328
template <> void Options::assign(
329
    options::arithPropAsLemmaLength__option_t,
330
    std::string option,
331
    std::string value)
332
{
333
  d_holder->arithPropAsLemmaLength =
334
    runHandlerAndPredicates(options::arithPropAsLemmaLength, option, value, d_handler);
335
  d_holder->arithPropAsLemmaLength__setByUser__ = true;
336
  Trace("options") << "user assigned option arithPropAsLemmaLength" << std::endl;
337
338
}
339
template <> options::arithPropagationMode__option_t::type runHandlerAndPredicates(
340
    options::arithPropagationMode__option_t,
341
    std::string option,
342
    std::string optionarg,
343
    options::OptionsHandler* handler)
344
{
345
  options::arithPropagationMode__option_t::type retval = stringToArithPropagationMode(option, optionarg);
346
347
  return retval;
348
}
349
template <> void Options::assign(
350
    options::arithPropagationMode__option_t,
351
    std::string option,
352
    std::string value)
353
{
354
  d_holder->arithPropagationMode =
355
    runHandlerAndPredicates(options::arithPropagationMode, option, value, d_handler);
356
  d_holder->arithPropagationMode__setByUser__ = true;
357
  Trace("options") << "user assigned option arithPropagationMode" << std::endl;
358
359
}
360
6
template <> void Options::assignBool(
361
    options::arithRewriteEq__option_t,
362
    std::string option,
363
    bool value)
364
{
365
6
  runBoolPredicates(options::arithRewriteEq, option, value, d_handler);
366
6
  d_holder->arithRewriteEq = value;
367
6
  d_holder->arithRewriteEq__setByUser__ = true;
368
6
  Trace("options") << "user assigned option arithRewriteEq" << std::endl;
369
370
6
}
371
template <> void Options::assignBool(
372
    options::collectPivots__option_t,
373
    std::string option,
374
    bool value)
375
{
376
  runBoolPredicates(options::collectPivots, option, value, d_handler);
377
  d_holder->collectPivots = value;
378
  d_holder->collectPivots__setByUser__ = true;
379
  Trace("options") << "user assigned option collectPivots" << std::endl;
380
381
}
382
template <> void Options::assignBool(
383
    options::doCutAllBounded__option_t,
384
    std::string option,
385
    bool value)
386
{
387
  runBoolPredicates(options::doCutAllBounded, option, value, d_handler);
388
  d_holder->doCutAllBounded = value;
389
  d_holder->doCutAllBounded__setByUser__ = true;
390
  Trace("options") << "user assigned option doCutAllBounded" << std::endl;
391
392
}
393
template <> void Options::assignBool(
394
    options::exportDioDecompositions__option_t,
395
    std::string option,
396
    bool value)
397
{
398
  runBoolPredicates(options::exportDioDecompositions, option, value, d_handler);
399
  d_holder->exportDioDecompositions = value;
400
  d_holder->exportDioDecompositions__setByUser__ = true;
401
  Trace("options") << "user assigned option exportDioDecompositions" << std::endl;
402
403
}
404
template <> void Options::assignBool(
405
    options::dioRepeat__option_t,
406
    std::string option,
407
    bool value)
408
{
409
  runBoolPredicates(options::dioRepeat, option, value, d_handler);
410
  d_holder->dioRepeat = value;
411
  d_holder->dioRepeat__setByUser__ = true;
412
  Trace("options") << "user assigned option dioRepeat" << std::endl;
413
414
}
415
template <> void Options::assignBool(
416
    options::arithDioSolver__option_t,
417
    std::string option,
418
    bool value)
419
{
420
  runBoolPredicates(options::arithDioSolver, option, value, d_handler);
421
  d_holder->arithDioSolver = value;
422
  d_holder->arithDioSolver__setByUser__ = true;
423
  Trace("options") << "user assigned option arithDioSolver" << std::endl;
424
425
}
426
template <> options::dioSolverTurns__option_t::type runHandlerAndPredicates(
427
    options::dioSolverTurns__option_t,
428
    std::string option,
429
    std::string optionarg,
430
    options::OptionsHandler* handler)
431
{
432
  options::dioSolverTurns__option_t::type retval = handleOption<int>(option, optionarg);
433
434
  return retval;
435
}
436
template <> void Options::assign(
437
    options::dioSolverTurns__option_t,
438
    std::string option,
439
    std::string value)
440
{
441
  d_holder->dioSolverTurns =
442
    runHandlerAndPredicates(options::dioSolverTurns, option, value, d_handler);
443
  d_holder->dioSolverTurns__setByUser__ = true;
444
  Trace("options") << "user assigned option dioSolverTurns" << std::endl;
445
446
}
447
template <> options::arithErrorSelectionRule__option_t::type runHandlerAndPredicates(
448
    options::arithErrorSelectionRule__option_t,
449
    std::string option,
450
    std::string optionarg,
451
    options::OptionsHandler* handler)
452
{
453
  options::arithErrorSelectionRule__option_t::type retval = stringToErrorSelectionRule(option, optionarg);
454
455
  return retval;
456
}
457
template <> void Options::assign(
458
    options::arithErrorSelectionRule__option_t,
459
    std::string option,
460
    std::string value)
461
{
462
  d_holder->arithErrorSelectionRule =
463
    runHandlerAndPredicates(options::arithErrorSelectionRule, option, value, d_handler);
464
  d_holder->arithErrorSelectionRule__setByUser__ = true;
465
  Trace("options") << "user assigned option arithErrorSelectionRule" << std::endl;
466
467
}
468
template <> void Options::assignBool(
469
    options::havePenalties__option_t,
470
    std::string option,
471
    bool value)
472
{
473
  runBoolPredicates(options::havePenalties, option, value, d_handler);
474
  d_holder->havePenalties = value;
475
  d_holder->havePenalties__setByUser__ = true;
476
  Trace("options") << "user assigned option havePenalties" << std::endl;
477
478
}
479
template <> options::arithHeuristicPivots__option_t::type runHandlerAndPredicates(
480
    options::arithHeuristicPivots__option_t,
481
    std::string option,
482
    std::string optionarg,
483
    options::OptionsHandler* handler)
484
{
485
  options::arithHeuristicPivots__option_t::type retval = handleOption<int16_t>(option, optionarg);
486
487
  return retval;
488
}
489
template <> void Options::assign(
490
    options::arithHeuristicPivots__option_t,
491
    std::string option,
492
    std::string value)
493
{
494
  d_holder->arithHeuristicPivots =
495
    runHandlerAndPredicates(options::arithHeuristicPivots, option, value, d_handler);
496
  d_holder->arithHeuristicPivots__setByUser__ = true;
497
  Trace("options") << "user assigned option arithHeuristicPivots" << std::endl;
498
499
}
500
template <> void Options::assignBool(
501
    options::replayFailureLemma__option_t,
502
    std::string option,
503
    bool value)
504
{
505
  runBoolPredicates(options::replayFailureLemma, option, value, d_handler);
506
  d_holder->replayFailureLemma = value;
507
  d_holder->replayFailureLemma__setByUser__ = true;
508
  Trace("options") << "user assigned option replayFailureLemma" << std::endl;
509
510
}
511
template <> options::maxCutsInContext__option_t::type runHandlerAndPredicates(
512
    options::maxCutsInContext__option_t,
513
    std::string option,
514
    std::string optionarg,
515
    options::OptionsHandler* handler)
516
{
517
  options::maxCutsInContext__option_t::type retval = handleOption<unsigned>(option, optionarg);
518
519
  return retval;
520
}
521
template <> void Options::assign(
522
    options::maxCutsInContext__option_t,
523
    std::string option,
524
    std::string value)
525
{
526
  d_holder->maxCutsInContext =
527
    runHandlerAndPredicates(options::maxCutsInContext, option, value, d_handler);
528
  d_holder->maxCutsInContext__setByUser__ = true;
529
  Trace("options") << "user assigned option maxCutsInContext" << std::endl;
530
531
}
532
8
template <> void Options::assignBool(
533
    options::arithMLTrick__option_t,
534
    std::string option,
535
    bool value)
536
{
537
8
  runBoolPredicates(options::arithMLTrick, option, value, d_handler);
538
8
  d_holder->arithMLTrick = value;
539
8
  d_holder->arithMLTrick__setByUser__ = true;
540
8
  Trace("options") << "user assigned option arithMLTrick" << std::endl;
541
542
8
}
543
template <> options::arithMLTrickSubstitutions__option_t::type runHandlerAndPredicates(
544
    options::arithMLTrickSubstitutions__option_t,
545
    std::string option,
546
    std::string optionarg,
547
    options::OptionsHandler* handler)
548
{
549
  options::arithMLTrickSubstitutions__option_t::type retval = handleOption<unsigned>(option, optionarg);
550
551
  return retval;
552
}
553
template <> void Options::assign(
554
    options::arithMLTrickSubstitutions__option_t,
555
    std::string option,
556
    std::string value)
557
{
558
  d_holder->arithMLTrickSubstitutions =
559
    runHandlerAndPredicates(options::arithMLTrickSubstitutions, option, value, d_handler);
560
  d_holder->arithMLTrickSubstitutions__setByUser__ = true;
561
  Trace("options") << "user assigned option arithMLTrickSubstitutions" << std::endl;
562
563
}
564
8
template <> void Options::assignBool(
565
    options::newProp__option_t,
566
    std::string option,
567
    bool value)
568
{
569
8
  runBoolPredicates(options::newProp, option, value, d_handler);
570
8
  d_holder->newProp = value;
571
8
  d_holder->newProp__setByUser__ = true;
572
8
  Trace("options") << "user assigned option newProp" << std::endl;
573
574
8
}
575
template <> void Options::assignBool(
576
    options::nlCad__option_t,
577
    std::string option,
578
    bool value)
579
{
580
  runBoolPredicates(options::nlCad, option, value, d_handler);
581
  d_holder->nlCad = value;
582
  d_holder->nlCad__setByUser__ = true;
583
  Trace("options") << "user assigned option nlCad" << std::endl;
584
585
}
586
template <> void Options::assignBool(
587
    options::nlCadUseInitial__option_t,
588
    std::string option,
589
    bool value)
590
{
591
  runBoolPredicates(options::nlCadUseInitial, option, value, d_handler);
592
  d_holder->nlCadUseInitial = value;
593
  d_holder->nlCadUseInitial__setByUser__ = true;
594
  Trace("options") << "user assigned option nlCadUseInitial" << std::endl;
595
596
}
597
124
template <> void Options::assignBool(
598
    options::nlExt__option_t,
599
    std::string option,
600
    bool value)
601
{
602
124
  runBoolPredicates(options::nlExt, option, value, d_handler);
603
124
  d_holder->nlExt = value;
604
124
  d_holder->nlExt__setByUser__ = true;
605
124
  Trace("options") << "user assigned option nlExt" << std::endl;
606
607
124
}
608
template <> void Options::assignBool(
609
    options::nlExtEntailConflicts__option_t,
610
    std::string option,
611
    bool value)
612
{
613
  runBoolPredicates(options::nlExtEntailConflicts, option, value, d_handler);
614
  d_holder->nlExtEntailConflicts = value;
615
  d_holder->nlExtEntailConflicts__setByUser__ = true;
616
  Trace("options") << "user assigned option nlExtEntailConflicts" << std::endl;
617
618
}
619
template <> void Options::assignBool(
620
    options::nlExtFactor__option_t,
621
    std::string option,
622
    bool value)
623
{
624
  runBoolPredicates(options::nlExtFactor, option, value, d_handler);
625
  d_holder->nlExtFactor = value;
626
  d_holder->nlExtFactor__setByUser__ = true;
627
  Trace("options") << "user assigned option nlExtFactor" << std::endl;
628
629
}
630
2
template <> void Options::assignBool(
631
    options::nlExtIncPrecision__option_t,
632
    std::string option,
633
    bool value)
634
{
635
2
  runBoolPredicates(options::nlExtIncPrecision, option, value, d_handler);
636
2
  d_holder->nlExtIncPrecision = value;
637
2
  d_holder->nlExtIncPrecision__setByUser__ = true;
638
2
  Trace("options") << "user assigned option nlExtIncPrecision" << std::endl;
639
640
2
}
641
5
template <> void Options::assignBool(
642
    options::nlExtPurify__option_t,
643
    std::string option,
644
    bool value)
645
{
646
5
  runBoolPredicates(options::nlExtPurify, option, value, d_handler);
647
5
  d_holder->nlExtPurify = value;
648
5
  d_holder->nlExtPurify__setByUser__ = true;
649
5
  Trace("options") << "user assigned option nlExtPurify" << std::endl;
650
651
5
}
652
template <> void Options::assignBool(
653
    options::nlExtResBound__option_t,
654
    std::string option,
655
    bool value)
656
{
657
  runBoolPredicates(options::nlExtResBound, option, value, d_handler);
658
  d_holder->nlExtResBound = value;
659
  d_holder->nlExtResBound__setByUser__ = true;
660
  Trace("options") << "user assigned option nlExtResBound" << std::endl;
661
662
}
663
template <> void Options::assignBool(
664
    options::nlExtRewrites__option_t,
665
    std::string option,
666
    bool value)
667
{
668
  runBoolPredicates(options::nlExtRewrites, option, value, d_handler);
669
  d_holder->nlExtRewrites = value;
670
  d_holder->nlExtRewrites__setByUser__ = true;
671
  Trace("options") << "user assigned option nlExtRewrites" << std::endl;
672
673
}
674
template <> void Options::assignBool(
675
    options::nlExtSplitZero__option_t,
676
    std::string option,
677
    bool value)
678
{
679
  runBoolPredicates(options::nlExtSplitZero, option, value, d_handler);
680
  d_holder->nlExtSplitZero = value;
681
  d_holder->nlExtSplitZero__setByUser__ = true;
682
  Trace("options") << "user assigned option nlExtSplitZero" << std::endl;
683
684
}
685
template <> options::nlExtTfTaylorDegree__option_t::type runHandlerAndPredicates(
686
    options::nlExtTfTaylorDegree__option_t,
687
    std::string option,
688
    std::string optionarg,
689
    options::OptionsHandler* handler)
690
{
691
  options::nlExtTfTaylorDegree__option_t::type retval = handleOption<int16_t>(option, optionarg);
692
693
  return retval;
694
}
695
template <> void Options::assign(
696
    options::nlExtTfTaylorDegree__option_t,
697
    std::string option,
698
    std::string value)
699
{
700
  d_holder->nlExtTfTaylorDegree =
701
    runHandlerAndPredicates(options::nlExtTfTaylorDegree, option, value, d_handler);
702
  d_holder->nlExtTfTaylorDegree__setByUser__ = true;
703
  Trace("options") << "user assigned option nlExtTfTaylorDegree" << std::endl;
704
705
}
706
43
template <> void Options::assignBool(
707
    options::nlExtTfTangentPlanes__option_t,
708
    std::string option,
709
    bool value)
710
{
711
43
  runBoolPredicates(options::nlExtTfTangentPlanes, option, value, d_handler);
712
43
  d_holder->nlExtTfTangentPlanes = value;
713
43
  d_holder->nlExtTfTangentPlanes__setByUser__ = true;
714
43
  Trace("options") << "user assigned option nlExtTfTangentPlanes" << std::endl;
715
716
43
}
717
41
template <> void Options::assignBool(
718
    options::nlExtTangentPlanes__option_t,
719
    std::string option,
720
    bool value)
721
{
722
41
  runBoolPredicates(options::nlExtTangentPlanes, option, value, d_handler);
723
41
  d_holder->nlExtTangentPlanes = value;
724
41
  d_holder->nlExtTangentPlanes__setByUser__ = true;
725
41
  Trace("options") << "user assigned option nlExtTangentPlanes" << std::endl;
726
727
41
}
728
template <> void Options::assignBool(
729
    options::nlExtTangentPlanesInterleave__option_t,
730
    std::string option,
731
    bool value)
732
{
733
  runBoolPredicates(options::nlExtTangentPlanesInterleave, option, value, d_handler);
734
  d_holder->nlExtTangentPlanesInterleave = value;
735
  d_holder->nlExtTangentPlanesInterleave__setByUser__ = true;
736
  Trace("options") << "user assigned option nlExtTangentPlanesInterleave" << std::endl;
737
738
}
739
template <> void Options::assignBool(
740
    options::nlICP__option_t,
741
    std::string option,
742
    bool value)
743
{
744
  runBoolPredicates(options::nlICP, option, value, d_handler);
745
  d_holder->nlICP = value;
746
  d_holder->nlICP__setByUser__ = true;
747
  Trace("options") << "user assigned option nlICP" << std::endl;
748
749
}
750
8
template <> options::nlRlvMode__option_t::type runHandlerAndPredicates(
751
    options::nlRlvMode__option_t,
752
    std::string option,
753
    std::string optionarg,
754
    options::OptionsHandler* handler)
755
{
756
8
  options::nlRlvMode__option_t::type retval = stringToNlRlvMode(option, optionarg);
757
758
8
  return retval;
759
}
760
8
template <> void Options::assign(
761
    options::nlRlvMode__option_t,
762
    std::string option,
763
    std::string value)
764
{
765
16
  d_holder->nlRlvMode =
766
24
    runHandlerAndPredicates(options::nlRlvMode, option, value, d_handler);
767
8
  d_holder->nlRlvMode__setByUser__ = true;
768
8
  Trace("options") << "user assigned option nlRlvMode" << std::endl;
769
770
8
}
771
2
template <> void Options::assignBool(
772
    options::pbRewrites__option_t,
773
    std::string option,
774
    bool value)
775
{
776
2
  runBoolPredicates(options::pbRewrites, option, value, d_handler);
777
2
  d_holder->pbRewrites = value;
778
2
  d_holder->pbRewrites__setByUser__ = true;
779
2
  Trace("options") << "user assigned option pbRewrites" << std::endl;
780
781
2
}
782
template <> options::arithPivotThreshold__option_t::type runHandlerAndPredicates(
783
    options::arithPivotThreshold__option_t,
784
    std::string option,
785
    std::string optionarg,
786
    options::OptionsHandler* handler)
787
{
788
  options::arithPivotThreshold__option_t::type retval = handleOption<uint16_t>(option, optionarg);
789
790
  return retval;
791
}
792
template <> void Options::assign(
793
    options::arithPivotThreshold__option_t,
794
    std::string option,
795
    std::string value)
796
{
797
  d_holder->arithPivotThreshold =
798
    runHandlerAndPredicates(options::arithPivotThreshold, option, value, d_handler);
799
  d_holder->arithPivotThreshold__setByUser__ = true;
800
  Trace("options") << "user assigned option arithPivotThreshold" << std::endl;
801
802
}
803
template <> options::ppAssertMaxSubSize__option_t::type runHandlerAndPredicates(
804
    options::ppAssertMaxSubSize__option_t,
805
    std::string option,
806
    std::string optionarg,
807
    options::OptionsHandler* handler)
808
{
809
  options::ppAssertMaxSubSize__option_t::type retval = handleOption<unsigned>(option, optionarg);
810
811
  return retval;
812
}
813
template <> void Options::assign(
814
    options::ppAssertMaxSubSize__option_t,
815
    std::string option,
816
    std::string value)
817
{
818
  d_holder->ppAssertMaxSubSize =
819
    runHandlerAndPredicates(options::ppAssertMaxSubSize, option, value, d_handler);
820
  d_holder->ppAssertMaxSubSize__setByUser__ = true;
821
  Trace("options") << "user assigned option ppAssertMaxSubSize" << std::endl;
822
823
}
824
template <> options::arithPropagateMaxLength__option_t::type runHandlerAndPredicates(
825
    options::arithPropagateMaxLength__option_t,
826
    std::string option,
827
    std::string optionarg,
828
    options::OptionsHandler* handler)
829
{
830
  options::arithPropagateMaxLength__option_t::type retval = handleOption<uint16_t>(option, optionarg);
831
832
  return retval;
833
}
834
template <> void Options::assign(
835
    options::arithPropagateMaxLength__option_t,
836
    std::string option,
837
    std::string value)
838
{
839
  d_holder->arithPropagateMaxLength =
840
    runHandlerAndPredicates(options::arithPropagateMaxLength, option, value, d_handler);
841
  d_holder->arithPropagateMaxLength__setByUser__ = true;
842
  Trace("options") << "user assigned option arithPropagateMaxLength" << std::endl;
843
844
}
845
template <> options::replayEarlyCloseDepths__option_t::type runHandlerAndPredicates(
846
    options::replayEarlyCloseDepths__option_t,
847
    std::string option,
848
    std::string optionarg,
849
    options::OptionsHandler* handler)
850
{
851
  options::replayEarlyCloseDepths__option_t::type retval = handleOption<int>(option, optionarg);
852
853
  return retval;
854
}
855
template <> void Options::assign(
856
    options::replayEarlyCloseDepths__option_t,
857
    std::string option,
858
    std::string value)
859
{
860
  d_holder->replayEarlyCloseDepths =
861
    runHandlerAndPredicates(options::replayEarlyCloseDepths, option, value, d_handler);
862
  d_holder->replayEarlyCloseDepths__setByUser__ = true;
863
  Trace("options") << "user assigned option replayEarlyCloseDepths" << std::endl;
864
865
}
866
template <> options::replayFailurePenalty__option_t::type runHandlerAndPredicates(
867
    options::replayFailurePenalty__option_t,
868
    std::string option,
869
    std::string optionarg,
870
    options::OptionsHandler* handler)
871
{
872
  options::replayFailurePenalty__option_t::type retval = handleOption<int>(option, optionarg);
873
874
  return retval;
875
}
876
template <> void Options::assign(
877
    options::replayFailurePenalty__option_t,
878
    std::string option,
879
    std::string value)
880
{
881
  d_holder->replayFailurePenalty =
882
    runHandlerAndPredicates(options::replayFailurePenalty, option, value, d_handler);
883
  d_holder->replayFailurePenalty__setByUser__ = true;
884
  Trace("options") << "user assigned option replayFailurePenalty" << std::endl;
885
886
}
887
template <> options::lemmaRejectCutSize__option_t::type runHandlerAndPredicates(
888
    options::lemmaRejectCutSize__option_t,
889
    std::string option,
890
    std::string optionarg,
891
    options::OptionsHandler* handler)
892
{
893
  options::lemmaRejectCutSize__option_t::type retval = handleOption<unsigned>(option, optionarg);
894
895
  return retval;
896
}
897
template <> void Options::assign(
898
    options::lemmaRejectCutSize__option_t,
899
    std::string option,
900
    std::string value)
901
{
902
  d_holder->lemmaRejectCutSize =
903
    runHandlerAndPredicates(options::lemmaRejectCutSize, option, value, d_handler);
904
  d_holder->lemmaRejectCutSize__setByUser__ = true;
905
  Trace("options") << "user assigned option lemmaRejectCutSize" << std::endl;
906
907
}
908
template <> options::replayNumericFailurePenalty__option_t::type runHandlerAndPredicates(
909
    options::replayNumericFailurePenalty__option_t,
910
    std::string option,
911
    std::string optionarg,
912
    options::OptionsHandler* handler)
913
{
914
  options::replayNumericFailurePenalty__option_t::type retval = handleOption<int>(option, optionarg);
915
916
  return retval;
917
}
918
template <> void Options::assign(
919
    options::replayNumericFailurePenalty__option_t,
920
    std::string option,
921
    std::string value)
922
{
923
  d_holder->replayNumericFailurePenalty =
924
    runHandlerAndPredicates(options::replayNumericFailurePenalty, option, value, d_handler);
925
  d_holder->replayNumericFailurePenalty__setByUser__ = true;
926
  Trace("options") << "user assigned option replayNumericFailurePenalty" << std::endl;
927
928
}
929
template <> options::replayRejectCutSize__option_t::type runHandlerAndPredicates(
930
    options::replayRejectCutSize__option_t,
931
    std::string option,
932
    std::string optionarg,
933
    options::OptionsHandler* handler)
934
{
935
  options::replayRejectCutSize__option_t::type retval = handleOption<unsigned>(option, optionarg);
936
937
  return retval;
938
}
939
template <> void Options::assign(
940
    options::replayRejectCutSize__option_t,
941
    std::string option,
942
    std::string value)
943
{
944
  d_holder->replayRejectCutSize =
945
    runHandlerAndPredicates(options::replayRejectCutSize, option, value, d_handler);
946
  d_holder->replayRejectCutSize__setByUser__ = true;
947
  Trace("options") << "user assigned option replayRejectCutSize" << std::endl;
948
949
}
950
template <> options::soiApproxMajorFailurePen__option_t::type runHandlerAndPredicates(
951
    options::soiApproxMajorFailurePen__option_t,
952
    std::string option,
953
    std::string optionarg,
954
    options::OptionsHandler* handler)
955
{
956
  options::soiApproxMajorFailurePen__option_t::type retval = handleOption<int>(option, optionarg);
957
958
  return retval;
959
}
960
template <> void Options::assign(
961
    options::soiApproxMajorFailurePen__option_t,
962
    std::string option,
963
    std::string value)
964
{
965
  d_holder->soiApproxMajorFailurePen =
966
    runHandlerAndPredicates(options::soiApproxMajorFailurePen, option, value, d_handler);
967
  d_holder->soiApproxMajorFailurePen__setByUser__ = true;
968
  Trace("options") << "user assigned option soiApproxMajorFailurePen" << std::endl;
969
970
}
971
template <> options::soiApproxMajorFailure__option_t::type runHandlerAndPredicates(
972
    options::soiApproxMajorFailure__option_t,
973
    std::string option,
974
    std::string optionarg,
975
    options::OptionsHandler* handler)
976
{
977
  options::soiApproxMajorFailure__option_t::type retval = handleOption<double>(option, optionarg);
978
979
  return retval;
980
}
981
template <> void Options::assign(
982
    options::soiApproxMajorFailure__option_t,
983
    std::string option,
984
    std::string value)
985
{
986
  d_holder->soiApproxMajorFailure =
987
    runHandlerAndPredicates(options::soiApproxMajorFailure, option, value, d_handler);
988
  d_holder->soiApproxMajorFailure__setByUser__ = true;
989
  Trace("options") << "user assigned option soiApproxMajorFailure" << std::endl;
990
991
}
992
template <> options::soiApproxMinorFailurePen__option_t::type runHandlerAndPredicates(
993
    options::soiApproxMinorFailurePen__option_t,
994
    std::string option,
995
    std::string optionarg,
996
    options::OptionsHandler* handler)
997
{
998
  options::soiApproxMinorFailurePen__option_t::type retval = handleOption<int>(option, optionarg);
999
1000
  return retval;
1001
}
1002
template <> void Options::assign(
1003
    options::soiApproxMinorFailurePen__option_t,
1004
    std::string option,
1005
    std::string value)
1006
{
1007
  d_holder->soiApproxMinorFailurePen =
1008
    runHandlerAndPredicates(options::soiApproxMinorFailurePen, option, value, d_handler);
1009
  d_holder->soiApproxMinorFailurePen__setByUser__ = true;
1010
  Trace("options") << "user assigned option soiApproxMinorFailurePen" << std::endl;
1011
1012
}
1013
template <> options::soiApproxMinorFailure__option_t::type runHandlerAndPredicates(
1014
    options::soiApproxMinorFailure__option_t,
1015
    std::string option,
1016
    std::string optionarg,
1017
    options::OptionsHandler* handler)
1018
{
1019
  options::soiApproxMinorFailure__option_t::type retval = handleOption<double>(option, optionarg);
1020
1021
  return retval;
1022
}
1023
template <> void Options::assign(
1024
    options::soiApproxMinorFailure__option_t,
1025
    std::string option,
1026
    std::string value)
1027
{
1028
  d_holder->soiApproxMinorFailure =
1029
    runHandlerAndPredicates(options::soiApproxMinorFailure, option, value, d_handler);
1030
  d_holder->soiApproxMinorFailure__setByUser__ = true;
1031
  Trace("options") << "user assigned option soiApproxMinorFailure" << std::endl;
1032
1033
}
1034
template <> void Options::assignBool(
1035
    options::restrictedPivots__option_t,
1036
    std::string option,
1037
    bool value)
1038
{
1039
  runBoolPredicates(options::restrictedPivots, option, value, d_handler);
1040
  d_holder->restrictedPivots = value;
1041
  d_holder->restrictedPivots__setByUser__ = true;
1042
  Trace("options") << "user assigned option restrictedPivots" << std::endl;
1043
1044
}
1045
template <> void Options::assignBool(
1046
    options::revertArithModels__option_t,
1047
    std::string option,
1048
    bool value)
1049
{
1050
  runBoolPredicates(options::revertArithModels, option, value, d_handler);
1051
  d_holder->revertArithModels = value;
1052
  d_holder->revertArithModels__setByUser__ = true;
1053
  Trace("options") << "user assigned option revertArithModels" << std::endl;
1054
1055
}
1056
template <> options::rrTurns__option_t::type runHandlerAndPredicates(
1057
    options::rrTurns__option_t,
1058
    std::string option,
1059
    std::string optionarg,
1060
    options::OptionsHandler* handler)
1061
{
1062
  options::rrTurns__option_t::type retval = handleOption<int>(option, optionarg);
1063
1064
  return retval;
1065
}
1066
template <> void Options::assign(
1067
    options::rrTurns__option_t,
1068
    std::string option,
1069
    std::string value)
1070
{
1071
  d_holder->rrTurns =
1072
    runHandlerAndPredicates(options::rrTurns, option, value, d_handler);
1073
  d_holder->rrTurns__setByUser__ = true;
1074
  Trace("options") << "user assigned option rrTurns" << std::endl;
1075
1076
}
1077
template <> void Options::assignBool(
1078
    options::trySolveIntStandardEffort__option_t,
1079
    std::string option,
1080
    bool value)
1081
{
1082
  runBoolPredicates(options::trySolveIntStandardEffort, option, value, d_handler);
1083
  d_holder->trySolveIntStandardEffort = value;
1084
  d_holder->trySolveIntStandardEffort__setByUser__ = true;
1085
  Trace("options") << "user assigned option trySolveIntStandardEffort" << std::endl;
1086
1087
}
1088
template <> options::arithSimplexCheckPeriod__option_t::type runHandlerAndPredicates(
1089
    options::arithSimplexCheckPeriod__option_t,
1090
    std::string option,
1091
    std::string optionarg,
1092
    options::OptionsHandler* handler)
1093
{
1094
  options::arithSimplexCheckPeriod__option_t::type retval = handleOption<uint16_t>(option, optionarg);
1095
1096
  return retval;
1097
}
1098
template <> void Options::assign(
1099
    options::arithSimplexCheckPeriod__option_t,
1100
    std::string option,
1101
    std::string value)
1102
{
1103
  d_holder->arithSimplexCheckPeriod =
1104
    runHandlerAndPredicates(options::arithSimplexCheckPeriod, option, value, d_handler);
1105
  d_holder->arithSimplexCheckPeriod__setByUser__ = true;
1106
  Trace("options") << "user assigned option arithSimplexCheckPeriod" << std::endl;
1107
1108
}
1109
template <> void Options::assignBool(
1110
    options::soiQuickExplain__option_t,
1111
    std::string option,
1112
    bool value)
1113
{
1114
  runBoolPredicates(options::soiQuickExplain, option, value, d_handler);
1115
  d_holder->soiQuickExplain = value;
1116
  d_holder->soiQuickExplain__setByUser__ = true;
1117
  Trace("options") << "user assigned option soiQuickExplain" << std::endl;
1118
1119
}
1120
template <> options::arithStandardCheckVarOrderPivots__option_t::type runHandlerAndPredicates(
1121
    options::arithStandardCheckVarOrderPivots__option_t,
1122
    std::string option,
1123
    std::string optionarg,
1124
    options::OptionsHandler* handler)
1125
{
1126
  options::arithStandardCheckVarOrderPivots__option_t::type retval = handleOption<int16_t>(option, optionarg);
1127
1128
  return retval;
1129
}
1130
template <> void Options::assign(
1131
    options::arithStandardCheckVarOrderPivots__option_t,
1132
    std::string option,
1133
    std::string value)
1134
{
1135
  d_holder->arithStandardCheckVarOrderPivots =
1136
    runHandlerAndPredicates(options::arithStandardCheckVarOrderPivots, option, value, d_handler);
1137
  d_holder->arithStandardCheckVarOrderPivots__setByUser__ = true;
1138
  Trace("options") << "user assigned option arithStandardCheckVarOrderPivots" << std::endl;
1139
1140
}
1141
template <> options::arithUnateLemmaMode__option_t::type runHandlerAndPredicates(
1142
    options::arithUnateLemmaMode__option_t,
1143
    std::string option,
1144
    std::string optionarg,
1145
    options::OptionsHandler* handler)
1146
{
1147
  options::arithUnateLemmaMode__option_t::type retval = stringToArithUnateLemmaMode(option, optionarg);
1148
1149
  return retval;
1150
}
1151
template <> void Options::assign(
1152
    options::arithUnateLemmaMode__option_t,
1153
    std::string option,
1154
    std::string value)
1155
{
1156
  d_holder->arithUnateLemmaMode =
1157
    runHandlerAndPredicates(options::arithUnateLemmaMode, option, value, d_handler);
1158
  d_holder->arithUnateLemmaMode__setByUser__ = true;
1159
  Trace("options") << "user assigned option arithUnateLemmaMode" << std::endl;
1160
1161
}
1162
template <> void Options::assignBool(
1163
    options::useApprox__option_t,
1164
    std::string option,
1165
    bool value)
1166
{
1167
  runBoolPredicates(options::useApprox, option, value, d_handler);
1168
  d_holder->useApprox = value;
1169
  d_holder->useApprox__setByUser__ = true;
1170
  Trace("options") << "user assigned option useApprox" << std::endl;
1171
1172
}
1173
template <> void Options::assignBool(
1174
    options::useFC__option_t,
1175
    std::string option,
1176
    bool value)
1177
{
1178
  runBoolPredicates(options::useFC, option, value, d_handler);
1179
  d_holder->useFC = value;
1180
  d_holder->useFC__setByUser__ = true;
1181
  Trace("options") << "user assigned option useFC" << std::endl;
1182
1183
}
1184
template <> void Options::assignBool(
1185
    options::useSOI__option_t,
1186
    std::string option,
1187
    bool value)
1188
{
1189
  runBoolPredicates(options::useSOI, option, value, d_handler);
1190
  d_holder->useSOI = value;
1191
  d_holder->useSOI__setByUser__ = true;
1192
  Trace("options") << "user assigned option useSOI" << std::endl;
1193
1194
}
1195
template <> options::arraysConfig__option_t::type runHandlerAndPredicates(
1196
    options::arraysConfig__option_t,
1197
    std::string option,
1198
    std::string optionarg,
1199
    options::OptionsHandler* handler)
1200
{
1201
  options::arraysConfig__option_t::type retval = handleOption<int>(option, optionarg);
1202
1203
  return retval;
1204
}
1205
template <> void Options::assign(
1206
    options::arraysConfig__option_t,
1207
    std::string option,
1208
    std::string value)
1209
{
1210
  d_holder->arraysConfig =
1211
    runHandlerAndPredicates(options::arraysConfig, option, value, d_handler);
1212
  d_holder->arraysConfig__setByUser__ = true;
1213
  Trace("options") << "user assigned option arraysConfig" << std::endl;
1214
1215
}
1216
template <> void Options::assignBool(
1217
    options::arraysEagerIndexSplitting__option_t,
1218
    std::string option,
1219
    bool value)
1220
{
1221
  runBoolPredicates(options::arraysEagerIndexSplitting, option, value, d_handler);
1222
  d_holder->arraysEagerIndexSplitting = value;
1223
  d_holder->arraysEagerIndexSplitting__setByUser__ = true;
1224
  Trace("options") << "user assigned option arraysEagerIndexSplitting" << std::endl;
1225
1226
}
1227
template <> void Options::assignBool(
1228
    options::arraysEagerLemmas__option_t,
1229
    std::string option,
1230
    bool value)
1231
{
1232
  runBoolPredicates(options::arraysEagerLemmas, option, value, d_handler);
1233
  d_holder->arraysEagerLemmas = value;
1234
  d_holder->arraysEagerLemmas__setByUser__ = true;
1235
  Trace("options") << "user assigned option arraysEagerLemmas" << std::endl;
1236
1237
}
1238
10
template <> void Options::assignBool(
1239
    options::arraysExp__option_t,
1240
    std::string option,
1241
    bool value)
1242
{
1243
10
  runBoolPredicates(options::arraysExp, option, value, d_handler);
1244
10
  d_holder->arraysExp = value;
1245
10
  d_holder->arraysExp__setByUser__ = true;
1246
10
  Trace("options") << "user assigned option arraysExp" << std::endl;
1247
1248
10
}
1249
template <> void Options::assignBool(
1250
    options::arraysModelBased__option_t,
1251
    std::string option,
1252
    bool value)
1253
{
1254
  runBoolPredicates(options::arraysModelBased, option, value, d_handler);
1255
  d_holder->arraysModelBased = value;
1256
  d_holder->arraysModelBased__setByUser__ = true;
1257
  Trace("options") << "user assigned option arraysModelBased" << std::endl;
1258
1259
}
1260
template <> void Options::assignBool(
1261
    options::arraysOptimizeLinear__option_t,
1262
    std::string option,
1263
    bool value)
1264
{
1265
  runBoolPredicates(options::arraysOptimizeLinear, option, value, d_handler);
1266
  d_holder->arraysOptimizeLinear = value;
1267
  d_holder->arraysOptimizeLinear__setByUser__ = true;
1268
  Trace("options") << "user assigned option arraysOptimizeLinear" << std::endl;
1269
1270
}
1271
template <> options::arraysPropagate__option_t::type runHandlerAndPredicates(
1272
    options::arraysPropagate__option_t,
1273
    std::string option,
1274
    std::string optionarg,
1275
    options::OptionsHandler* handler)
1276
{
1277
  options::arraysPropagate__option_t::type retval = handleOption<int>(option, optionarg);
1278
1279
  return retval;
1280
}
1281
template <> void Options::assign(
1282
    options::arraysPropagate__option_t,
1283
    std::string option,
1284
    std::string value)
1285
{
1286
  d_holder->arraysPropagate =
1287
    runHandlerAndPredicates(options::arraysPropagate, option, value, d_handler);
1288
  d_holder->arraysPropagate__setByUser__ = true;
1289
  Trace("options") << "user assigned option arraysPropagate" << std::endl;
1290
1291
}
1292
template <> void Options::assignBool(
1293
    options::arraysReduceSharing__option_t,
1294
    std::string option,
1295
    bool value)
1296
{
1297
  runBoolPredicates(options::arraysReduceSharing, option, value, d_handler);
1298
  d_holder->arraysReduceSharing = value;
1299
  d_holder->arraysReduceSharing__setByUser__ = true;
1300
  Trace("options") << "user assigned option arraysReduceSharing" << std::endl;
1301
1302
}
1303
template <> void Options::assignBool(
1304
    options::arraysWeakEquivalence__option_t,
1305
    std::string option,
1306
    bool value)
1307
{
1308
  runBoolPredicates(options::arraysWeakEquivalence, option, value, d_handler);
1309
  d_holder->arraysWeakEquivalence = value;
1310
  d_holder->arraysWeakEquivalence__setByUser__ = true;
1311
  Trace("options") << "user assigned option arraysWeakEquivalence" << std::endl;
1312
1313
}
1314
653
template <> options::inputLanguage__option_t::type runHandlerAndPredicates(
1315
    options::inputLanguage__option_t,
1316
    std::string option,
1317
    std::string optionarg,
1318
    options::OptionsHandler* handler)
1319
{
1320
653
  options::inputLanguage__option_t::type retval = handler->stringToInputLanguage(option, optionarg);
1321
1322
653
  return retval;
1323
}
1324
653
template <> void Options::assign(
1325
    options::inputLanguage__option_t,
1326
    std::string option,
1327
    std::string value)
1328
{
1329
1306
  d_holder->inputLanguage =
1330
1959
    runHandlerAndPredicates(options::inputLanguage, option, value, d_handler);
1331
653
  d_holder->inputLanguage__setByUser__ = true;
1332
653
  Trace("options") << "user assigned option inputLanguage" << std::endl;
1333
1334
653
}
1335
template <> void Options::assignBool(
1336
    options::languageHelp__option_t,
1337
    std::string option,
1338
    bool value)
1339
{
1340
  runBoolPredicates(options::languageHelp, option, value, d_handler);
1341
  d_holder->languageHelp = value;
1342
  d_holder->languageHelp__setByUser__ = true;
1343
  Trace("options") << "user assigned option languageHelp" << std::endl;
1344
1345
}
1346
86
template <> options::outputLanguage__option_t::type runHandlerAndPredicates(
1347
    options::outputLanguage__option_t,
1348
    std::string option,
1349
    std::string optionarg,
1350
    options::OptionsHandler* handler)
1351
{
1352
86
  options::outputLanguage__option_t::type retval = handler->stringToOutputLanguage(option, optionarg);
1353
1354
86
  return retval;
1355
}
1356
86
template <> void Options::assign(
1357
    options::outputLanguage__option_t,
1358
    std::string option,
1359
    std::string value)
1360
{
1361
172
  d_holder->outputLanguage =
1362
258
    runHandlerAndPredicates(options::outputLanguage, option, value, d_handler);
1363
86
  d_holder->outputLanguage__setByUser__ = true;
1364
86
  Trace("options") << "user assigned option outputLanguage" << std::endl;
1365
1366
86
}
1367
template <> void Options::assignBool(
1368
    options::parseOnly__option_t,
1369
    std::string option,
1370
    bool value)
1371
{
1372
  runBoolPredicates(options::parseOnly, option, value, d_handler);
1373
  d_holder->parseOnly = value;
1374
  d_holder->parseOnly__setByUser__ = true;
1375
  Trace("options") << "user assigned option parseOnly" << std::endl;
1376
1377
}
1378
3
template <> void Options::assignBool(
1379
    options::preprocessOnly__option_t,
1380
    std::string option,
1381
    bool value)
1382
{
1383
3
  runBoolPredicates(options::preprocessOnly, option, value, d_handler);
1384
3
  d_holder->preprocessOnly = value;
1385
3
  d_holder->preprocessOnly__setByUser__ = true;
1386
3
  Trace("options") << "user assigned option preprocessOnly" << std::endl;
1387
1388
3
}
1389
27
template <> void Options::assignBool(
1390
    options::printSuccess__option_t,
1391
    std::string option,
1392
    bool value)
1393
{
1394
27
  runBoolPredicates(options::printSuccess, option, value, d_handler);
1395
27
  d_holder->printSuccess = value;
1396
27
  d_holder->printSuccess__setByUser__ = true;
1397
27
  Trace("options") << "user assigned option printSuccess" << std::endl;
1398
1399
27
}
1400
template <> void runBoolPredicates(
1401
    options::statistics__option_t,
1402
    std::string option,
1403
    bool b,
1404
    options::OptionsHandler* handler)
1405
{
1406
  handler->statsEnabledBuild(option, b);
1407
}
1408
template <> void Options::assignBool(
1409
    options::statistics__option_t,
1410
    std::string option,
1411
    bool value)
1412
{
1413
  runBoolPredicates(options::statistics, option, value, d_handler);
1414
  d_holder->statistics = value;
1415
  d_holder->statistics__setByUser__ = true;
1416
  Trace("options") << "user assigned option statistics" << std::endl;
1417
1418
}
1419
template <> void Options::assignBool(
1420
    options::statsEveryQuery__option_t,
1421
    std::string option,
1422
    bool value)
1423
{
1424
  runBoolPredicates(options::statsEveryQuery, option, value, d_handler);
1425
  d_holder->statsEveryQuery = value;
1426
  d_holder->statsEveryQuery__setByUser__ = true;
1427
  Trace("options") << "user assigned option statsEveryQuery" << std::endl;
1428
1429
}
1430
template <> void Options::assignBool(
1431
    options::statsHideZeros__option_t,
1432
    std::string option,
1433
    bool value)
1434
{
1435
  runBoolPredicates(options::statsHideZeros, option, value, d_handler);
1436
  d_holder->statsHideZeros = value;
1437
  d_holder->statsHideZeros__setByUser__ = true;
1438
  Trace("options") << "user assigned option statsHideZeros" << std::endl;
1439
1440
}
1441
template <> void Options::assign(
1442
    options::verbosity__option_t,
1443
    std::string option,
1444
    std::string value)
1445
{
1446
  d_holder->verbosity =
1447
    runHandlerAndPredicates(options::verbosity, option, value, d_handler);
1448
  d_holder->verbosity__setByUser__ = true;
1449
  Trace("options") << "user assigned option verbosity" << std::endl;
1450
1451
}
1452
template <> void runBoolPredicates(
1453
    options::bitvectorAig__option_t,
1454
    std::string option,
1455
    bool b,
1456
    options::OptionsHandler* handler)
1457
{
1458
  handler->abcEnabledBuild(option, b);
1459
handler->setBitblastAig(option, b);
1460
}
1461
template <> void Options::assignBool(
1462
    options::bitvectorAig__option_t,
1463
    std::string option,
1464
    bool value)
1465
{
1466
  runBoolPredicates(options::bitvectorAig, option, value, d_handler);
1467
  d_holder->bitvectorAig = value;
1468
  d_holder->bitvectorAig__setByUser__ = true;
1469
  Trace("options") << "user assigned option bitvectorAig" << std::endl;
1470
1471
}
1472
32
template <> options::bitblastMode__option_t::type runHandlerAndPredicates(
1473
    options::bitblastMode__option_t,
1474
    std::string option,
1475
    std::string optionarg,
1476
    options::OptionsHandler* handler)
1477
{
1478
32
  options::bitblastMode__option_t::type retval = stringToBitblastMode(option, optionarg);
1479
1480
32
  return retval;
1481
}
1482
32
template <> void Options::assign(
1483
    options::bitblastMode__option_t,
1484
    std::string option,
1485
    std::string value)
1486
{
1487
64
  d_holder->bitblastMode =
1488
96
    runHandlerAndPredicates(options::bitblastMode, option, value, d_handler);
1489
32
  d_holder->bitblastMode__setByUser__ = true;
1490
32
  Trace("options") << "user assigned option bitblastMode" << std::endl;
1491
1492
32
}
1493
template <> void Options::assignBool(
1494
    options::bitwiseEq__option_t,
1495
    std::string option,
1496
    bool value)
1497
{
1498
  runBoolPredicates(options::bitwiseEq, option, value, d_handler);
1499
  d_holder->bitwiseEq = value;
1500
  d_holder->bitwiseEq__setByUser__ = true;
1501
  Trace("options") << "user assigned option bitwiseEq" << std::endl;
1502
1503
}
1504
12
template <> options::boolToBitvector__option_t::type runHandlerAndPredicates(
1505
    options::boolToBitvector__option_t,
1506
    std::string option,
1507
    std::string optionarg,
1508
    options::OptionsHandler* handler)
1509
{
1510
12
  options::boolToBitvector__option_t::type retval = stringToBoolToBVMode(option, optionarg);
1511
1512
12
  return retval;
1513
}
1514
12
template <> void Options::assign(
1515
    options::boolToBitvector__option_t,
1516
    std::string option,
1517
    std::string value)
1518
{
1519
24
  d_holder->boolToBitvector =
1520
36
    runHandlerAndPredicates(options::boolToBitvector, option, value, d_handler);
1521
12
  d_holder->boolToBitvector__setByUser__ = true;
1522
12
  Trace("options") << "user assigned option boolToBitvector" << std::endl;
1523
1524
12
}
1525
3
template <> void Options::assignBool(
1526
    options::bvAbstraction__option_t,
1527
    std::string option,
1528
    bool value)
1529
{
1530
3
  runBoolPredicates(options::bvAbstraction, option, value, d_handler);
1531
3
  d_holder->bvAbstraction = value;
1532
3
  d_holder->bvAbstraction__setByUser__ = true;
1533
3
  Trace("options") << "user assigned option bvAbstraction" << std::endl;
1534
1535
3
}
1536
template <> options::bitvectorAigSimplifications__option_t::type runHandlerAndPredicates(
1537
    options::bitvectorAigSimplifications__option_t,
1538
    std::string option,
1539
    std::string optionarg,
1540
    options::OptionsHandler* handler)
1541
{
1542
  options::bitvectorAigSimplifications__option_t::type retval = handleOption<std::string>(option, optionarg);
1543
  handler->abcEnabledBuild(option, retval);
1544
  return retval;
1545
}
1546
template <> void Options::assign(
1547
    options::bitvectorAigSimplifications__option_t,
1548
    std::string option,
1549
    std::string value)
1550
{
1551
  d_holder->bitvectorAigSimplifications =
1552
    runHandlerAndPredicates(options::bitvectorAigSimplifications, option, value, d_handler);
1553
  d_holder->bitvectorAigSimplifications__setByUser__ = true;
1554
  Trace("options") << "user assigned option bitvectorAigSimplifications" << std::endl;
1555
1556
}
1557
template <> void Options::assignBool(
1558
    options::bvAlgExtf__option_t,
1559
    std::string option,
1560
    bool value)
1561
{
1562
  runBoolPredicates(options::bvAlgExtf, option, value, d_handler);
1563
  d_holder->bvAlgExtf = value;
1564
  d_holder->bvAlgExtf__setByUser__ = true;
1565
  Trace("options") << "user assigned option bvAlgExtf" << std::endl;
1566
1567
}
1568
template <> options::bitvectorAlgebraicBudget__option_t::type runHandlerAndPredicates(
1569
    options::bitvectorAlgebraicBudget__option_t,
1570
    std::string option,
1571
    std::string optionarg,
1572
    options::OptionsHandler* handler)
1573
{
1574
  options::bitvectorAlgebraicBudget__option_t::type retval = handleOption<unsigned>(option, optionarg);
1575
1576
  return retval;
1577
}
1578
template <> void Options::assign(
1579
    options::bitvectorAlgebraicBudget__option_t,
1580
    std::string option,
1581
    std::string value)
1582
{
1583
  d_holder->bitvectorAlgebraicBudget =
1584
    runHandlerAndPredicates(options::bitvectorAlgebraicBudget, option, value, d_handler);
1585
  d_holder->bitvectorAlgebraicBudget__setByUser__ = true;
1586
  Trace("options") << "user assigned option bitvectorAlgebraicBudget" << std::endl;
1587
1588
}
1589
template <> void Options::assignBool(
1590
    options::bitvectorAlgebraicSolver__option_t,
1591
    std::string option,
1592
    bool value)
1593
{
1594
  runBoolPredicates(options::bitvectorAlgebraicSolver, option, value, d_handler);
1595
  d_holder->bitvectorAlgebraicSolver = value;
1596
  d_holder->bitvectorAlgebraicSolver__setByUser__ = true;
1597
  Trace("options") << "user assigned option bitvectorAlgebraicSolver" << std::endl;
1598
1599
}
1600
template <> void Options::assignBool(
1601
    options::bvEagerExplanations__option_t,
1602
    std::string option,
1603
    bool value)
1604
{
1605
  runBoolPredicates(options::bvEagerExplanations, option, value, d_handler);
1606
  d_holder->bvEagerExplanations = value;
1607
  d_holder->bvEagerExplanations__setByUser__ = true;
1608
  Trace("options") << "user assigned option bvEagerExplanations" << std::endl;
1609
1610
}
1611
2
template <> void Options::assignBool(
1612
    options::bitvectorEqualitySolver__option_t,
1613
    std::string option,
1614
    bool value)
1615
{
1616
2
  runBoolPredicates(options::bitvectorEqualitySolver, option, value, d_handler);
1617
2
  d_holder->bitvectorEqualitySolver = value;
1618
2
  d_holder->bitvectorEqualitySolver__setByUser__ = true;
1619
2
  Trace("options") << "user assigned option bitvectorEqualitySolver" << std::endl;
1620
1621
2
}
1622
template <> void Options::assignBool(
1623
    options::bvExtractArithRewrite__option_t,
1624
    std::string option,
1625
    bool value)
1626
{
1627
  runBoolPredicates(options::bvExtractArithRewrite, option, value, d_handler);
1628
  d_holder->bvExtractArithRewrite = value;
1629
  d_holder->bvExtractArithRewrite__setByUser__ = true;
1630
  Trace("options") << "user assigned option bvExtractArithRewrite" << std::endl;
1631
1632
}
1633
template <> void Options::assignBool(
1634
    options::bvGaussElim__option_t,
1635
    std::string option,
1636
    bool value)
1637
{
1638
  runBoolPredicates(options::bvGaussElim, option, value, d_handler);
1639
  d_holder->bvGaussElim = value;
1640
  d_holder->bvGaussElim__setByUser__ = true;
1641
  Trace("options") << "user assigned option bvGaussElim" << std::endl;
1642
1643
}
1644
template <> void Options::assignBool(
1645
    options::bitvectorInequalitySolver__option_t,
1646
    std::string option,
1647
    bool value)
1648
{
1649
  runBoolPredicates(options::bitvectorInequalitySolver, option, value, d_handler);
1650
  d_holder->bitvectorInequalitySolver = value;
1651
  d_holder->bitvectorInequalitySolver__setByUser__ = true;
1652
  Trace("options") << "user assigned option bitvectorInequalitySolver" << std::endl;
1653
1654
}
1655
2
template <> void Options::assignBool(
1656
    options::bvIntroducePow2__option_t,
1657
    std::string option,
1658
    bool value)
1659
{
1660
2
  runBoolPredicates(options::bvIntroducePow2, option, value, d_handler);
1661
2
  d_holder->bvIntroducePow2 = value;
1662
2
  d_holder->bvIntroducePow2__setByUser__ = true;
1663
2
  Trace("options") << "user assigned option bvIntroducePow2" << std::endl;
1664
1665
2
}
1666
template <> void Options::assignBool(
1667
    options::bvLazyReduceExtf__option_t,
1668
    std::string option,
1669
    bool value)
1670
{
1671
  runBoolPredicates(options::bvLazyReduceExtf, option, value, d_handler);
1672
  d_holder->bvLazyReduceExtf = value;
1673
  d_holder->bvLazyReduceExtf__setByUser__ = true;
1674
  Trace("options") << "user assigned option bvLazyReduceExtf" << std::endl;
1675
1676
}
1677
template <> void Options::assignBool(
1678
    options::bvLazyRewriteExtf__option_t,
1679
    std::string option,
1680
    bool value)
1681
{
1682
  runBoolPredicates(options::bvLazyRewriteExtf, option, value, d_handler);
1683
  d_holder->bvLazyRewriteExtf = value;
1684
  d_holder->bvLazyRewriteExtf__setByUser__ = true;
1685
  Trace("options") << "user assigned option bvLazyRewriteExtf" << std::endl;
1686
1687
}
1688
template <> options::bvNumFunc__option_t::type runHandlerAndPredicates(
1689
    options::bvNumFunc__option_t,
1690
    std::string option,
1691
    std::string optionarg,
1692
    options::OptionsHandler* handler)
1693
{
1694
  options::bvNumFunc__option_t::type retval = handleOption<unsigned>(option, optionarg);
1695
1696
  return retval;
1697
}
1698
template <> void Options::assign(
1699
    options::bvNumFunc__option_t,
1700
    std::string option,
1701
    std::string value)
1702
{
1703
  d_holder->bvNumFunc =
1704
    runHandlerAndPredicates(options::bvNumFunc, option, value, d_handler);
1705
  d_holder->bvNumFunc__setByUser__ = true;
1706
  Trace("options") << "user assigned option bvNumFunc" << std::endl;
1707
1708
}
1709
2
template <> void Options::assignBool(
1710
    options::bvPrintConstsAsIndexedSymbols__option_t,
1711
    std::string option,
1712
    bool value)
1713
{
1714
2
  runBoolPredicates(options::bvPrintConstsAsIndexedSymbols, option, value, d_handler);
1715
2
  d_holder->bvPrintConstsAsIndexedSymbols = value;
1716
2
  d_holder->bvPrintConstsAsIndexedSymbols__setByUser__ = true;
1717
2
  Trace("options") << "user assigned option bvPrintConstsAsIndexedSymbols" << std::endl;
1718
1719
2
}
1720
template <> void Options::assignBool(
1721
    options::bitvectorPropagate__option_t,
1722
    std::string option,
1723
    bool value)
1724
{
1725
  runBoolPredicates(options::bitvectorPropagate, option, value, d_handler);
1726
  d_holder->bitvectorPropagate = value;
1727
  d_holder->bitvectorPropagate__setByUser__ = true;
1728
  Trace("options") << "user assigned option bitvectorPropagate" << std::endl;
1729
1730
}
1731
template <> void Options::assignBool(
1732
    options::bitvectorQuickXplain__option_t,
1733
    std::string option,
1734
    bool value)
1735
{
1736
  runBoolPredicates(options::bitvectorQuickXplain, option, value, d_handler);
1737
  d_holder->bitvectorQuickXplain = value;
1738
  d_holder->bitvectorQuickXplain__setByUser__ = true;
1739
  Trace("options") << "user assigned option bitvectorQuickXplain" << std::endl;
1740
1741
}
1742
14
template <> options::bvSatSolver__option_t::type runHandlerAndPredicates(
1743
    options::bvSatSolver__option_t,
1744
    std::string option,
1745
    std::string optionarg,
1746
    options::OptionsHandler* handler)
1747
{
1748
14
  options::bvSatSolver__option_t::type retval = stringToSatSolverMode(option, optionarg);
1749
12
  handler->checkBvSatSolver(option, retval);
1750
12
  return retval;
1751
}
1752
14
template <> void Options::assign(
1753
    options::bvSatSolver__option_t,
1754
    std::string option,
1755
    std::string value)
1756
{
1757
26
  d_holder->bvSatSolver =
1758
42
    runHandlerAndPredicates(options::bvSatSolver, option, value, d_handler);
1759
12
  d_holder->bvSatSolver__setByUser__ = true;
1760
12
  Trace("options") << "user assigned option bvSatSolver" << std::endl;
1761
1762
12
}
1763
template <> void Options::assignBool(
1764
    options::skolemizeArguments__option_t,
1765
    std::string option,
1766
    bool value)
1767
{
1768
  runBoolPredicates(options::skolemizeArguments, option, value, d_handler);
1769
  d_holder->skolemizeArguments = value;
1770
  d_holder->skolemizeArguments__setByUser__ = true;
1771
  Trace("options") << "user assigned option skolemizeArguments" << std::endl;
1772
1773
}
1774
13
template <> options::bvSolver__option_t::type runHandlerAndPredicates(
1775
    options::bvSolver__option_t,
1776
    std::string option,
1777
    std::string optionarg,
1778
    options::OptionsHandler* handler)
1779
{
1780
13
  options::bvSolver__option_t::type retval = stringToBVSolver(option, optionarg);
1781
1782
13
  return retval;
1783
}
1784
13
template <> void Options::assign(
1785
    options::bvSolver__option_t,
1786
    std::string option,
1787
    std::string value)
1788
{
1789
26
  d_holder->bvSolver =
1790
39
    runHandlerAndPredicates(options::bvSolver, option, value, d_handler);
1791
13
  d_holder->bvSolver__setByUser__ = true;
1792
13
  Trace("options") << "user assigned option bvSolver" << std::endl;
1793
1794
13
}
1795
10
template <> void Options::assignBool(
1796
    options::bitvectorToBool__option_t,
1797
    std::string option,
1798
    bool value)
1799
{
1800
10
  runBoolPredicates(options::bitvectorToBool, option, value, d_handler);
1801
10
  d_holder->bitvectorToBool = value;
1802
10
  d_holder->bitvectorToBool__setByUser__ = true;
1803
10
  Trace("options") << "user assigned option bitvectorToBool" << std::endl;
1804
1805
10
}
1806
template <> void Options::assignBool(
1807
    options::cdtBisimilar__option_t,
1808
    std::string option,
1809
    bool value)
1810
{
1811
  runBoolPredicates(options::cdtBisimilar, option, value, d_handler);
1812
  d_holder->cdtBisimilar = value;
1813
  d_holder->cdtBisimilar__setByUser__ = true;
1814
  Trace("options") << "user assigned option cdtBisimilar" << std::endl;
1815
1816
}
1817
template <> void Options::assignBool(
1818
    options::dtBinarySplit__option_t,
1819
    std::string option,
1820
    bool value)
1821
{
1822
  runBoolPredicates(options::dtBinarySplit, option, value, d_handler);
1823
  d_holder->dtBinarySplit = value;
1824
  d_holder->dtBinarySplit__setByUser__ = true;
1825
  Trace("options") << "user assigned option dtBinarySplit" << std::endl;
1826
1827
}
1828
template <> void Options::assignBool(
1829
    options::dtBlastSplits__option_t,
1830
    std::string option,
1831
    bool value)
1832
{
1833
  runBoolPredicates(options::dtBlastSplits, option, value, d_handler);
1834
  d_holder->dtBlastSplits = value;
1835
  d_holder->dtBlastSplits__setByUser__ = true;
1836
  Trace("options") << "user assigned option dtBlastSplits" << std::endl;
1837
1838
}
1839
template <> void Options::assignBool(
1840
    options::dtCyclic__option_t,
1841
    std::string option,
1842
    bool value)
1843
{
1844
  runBoolPredicates(options::dtCyclic, option, value, d_handler);
1845
  d_holder->dtCyclic = value;
1846
  d_holder->dtCyclic__setByUser__ = true;
1847
  Trace("options") << "user assigned option dtCyclic" << std::endl;
1848
1849
}
1850
template <> void Options::assignBool(
1851
    options::dtForceAssignment__option_t,
1852
    std::string option,
1853
    bool value)
1854
{
1855
  runBoolPredicates(options::dtForceAssignment, option, value, d_handler);
1856
  d_holder->dtForceAssignment = value;
1857
  d_holder->dtForceAssignment__setByUser__ = true;
1858
  Trace("options") << "user assigned option dtForceAssignment" << std::endl;
1859
1860
}
1861
template <> void Options::assignBool(
1862
    options::dtInferAsLemmas__option_t,
1863
    std::string option,
1864
    bool value)
1865
{
1866
  runBoolPredicates(options::dtInferAsLemmas, option, value, d_handler);
1867
  d_holder->dtInferAsLemmas = value;
1868
  d_holder->dtInferAsLemmas__setByUser__ = true;
1869
  Trace("options") << "user assigned option dtInferAsLemmas" << std::endl;
1870
1871
}
1872
10
template <> void Options::assignBool(
1873
    options::dtNestedRec__option_t,
1874
    std::string option,
1875
    bool value)
1876
{
1877
10
  runBoolPredicates(options::dtNestedRec, option, value, d_handler);
1878
10
  d_holder->dtNestedRec = value;
1879
10
  d_holder->dtNestedRec__setByUser__ = true;
1880
10
  Trace("options") << "user assigned option dtNestedRec" << std::endl;
1881
1882
10
}
1883
template <> void Options::assignBool(
1884
    options::dtPoliteOptimize__option_t,
1885
    std::string option,
1886
    bool value)
1887
{
1888
  runBoolPredicates(options::dtPoliteOptimize, option, value, d_handler);
1889
  d_holder->dtPoliteOptimize = value;
1890
  d_holder->dtPoliteOptimize__setByUser__ = true;
1891
  Trace("options") << "user assigned option dtPoliteOptimize" << std::endl;
1892
1893
}
1894
5
template <> void Options::assignBool(
1895
    options::dtRewriteErrorSel__option_t,
1896
    std::string option,
1897
    bool value)
1898
{
1899
5
  runBoolPredicates(options::dtRewriteErrorSel, option, value, d_handler);
1900
5
  d_holder->dtRewriteErrorSel = value;
1901
5
  d_holder->dtRewriteErrorSel__setByUser__ = true;
1902
5
  Trace("options") << "user assigned option dtRewriteErrorSel" << std::endl;
1903
1904
5
}
1905
template <> void Options::assignBool(
1906
    options::dtSharedSelectors__option_t,
1907
    std::string option,
1908
    bool value)
1909
{
1910
  runBoolPredicates(options::dtSharedSelectors, option, value, d_handler);
1911
  d_holder->dtSharedSelectors = value;
1912
  d_holder->dtSharedSelectors__setByUser__ = true;
1913
  Trace("options") << "user assigned option dtSharedSelectors" << std::endl;
1914
1915
}
1916
16
template <> options::sygusAbortSize__option_t::type runHandlerAndPredicates(
1917
    options::sygusAbortSize__option_t,
1918
    std::string option,
1919
    std::string optionarg,
1920
    options::OptionsHandler* handler)
1921
{
1922
16
  options::sygusAbortSize__option_t::type retval = handleOption<int>(option, optionarg);
1923
1924
16
  return retval;
1925
}
1926
16
template <> void Options::assign(
1927
    options::sygusAbortSize__option_t,
1928
    std::string option,
1929
    std::string value)
1930
{
1931
32
  d_holder->sygusAbortSize =
1932
48
    runHandlerAndPredicates(options::sygusAbortSize, option, value, d_handler);
1933
16
  d_holder->sygusAbortSize__setByUser__ = true;
1934
16
  Trace("options") << "user assigned option sygusAbortSize" << std::endl;
1935
1936
16
}
1937
template <> void Options::assignBool(
1938
    options::sygusFairMax__option_t,
1939
    std::string option,
1940
    bool value)
1941
{
1942
  runBoolPredicates(options::sygusFairMax, option, value, d_handler);
1943
  d_holder->sygusFairMax = value;
1944
  d_holder->sygusFairMax__setByUser__ = true;
1945
  Trace("options") << "user assigned option sygusFairMax" << std::endl;
1946
1947
}
1948
4
template <> options::sygusFair__option_t::type runHandlerAndPredicates(
1949
    options::sygusFair__option_t,
1950
    std::string option,
1951
    std::string optionarg,
1952
    options::OptionsHandler* handler)
1953
{
1954
4
  options::sygusFair__option_t::type retval = stringToSygusFairMode(option, optionarg);
1955
1956
4
  return retval;
1957
}
1958
4
template <> void Options::assign(
1959
    options::sygusFair__option_t,
1960
    std::string option,
1961
    std::string value)
1962
{
1963
8
  d_holder->sygusFair =
1964
12
    runHandlerAndPredicates(options::sygusFair, option, value, d_handler);
1965
4
  d_holder->sygusFair__setByUser__ = true;
1966
4
  Trace("options") << "user assigned option sygusFair" << std::endl;
1967
1968
4
}
1969
8
template <> void Options::assignBool(
1970
    options::sygusSymBreak__option_t,
1971
    std::string option,
1972
    bool value)
1973
{
1974
8
  runBoolPredicates(options::sygusSymBreak, option, value, d_handler);
1975
8
  d_holder->sygusSymBreak = value;
1976
8
  d_holder->sygusSymBreak__setByUser__ = true;
1977
8
  Trace("options") << "user assigned option sygusSymBreak" << std::endl;
1978
1979
8
}
1980
template <> void Options::assignBool(
1981
    options::sygusSymBreakAgg__option_t,
1982
    std::string option,
1983
    bool value)
1984
{
1985
  runBoolPredicates(options::sygusSymBreakAgg, option, value, d_handler);
1986
  d_holder->sygusSymBreakAgg = value;
1987
  d_holder->sygusSymBreakAgg__setByUser__ = true;
1988
  Trace("options") << "user assigned option sygusSymBreakAgg" << std::endl;
1989
1990
}
1991
template <> void Options::assignBool(
1992
    options::sygusSymBreakDynamic__option_t,
1993
    std::string option,
1994
    bool value)
1995
{
1996
  runBoolPredicates(options::sygusSymBreakDynamic, option, value, d_handler);
1997
  d_holder->sygusSymBreakDynamic = value;
1998
  d_holder->sygusSymBreakDynamic__setByUser__ = true;
1999
  Trace("options") << "user assigned option sygusSymBreakDynamic" << std::endl;
2000
2001
}
2002
2
template <> void Options::assignBool(
2003
    options::sygusSymBreakLazy__option_t,
2004
    std::string option,
2005
    bool value)
2006
{
2007
2
  runBoolPredicates(options::sygusSymBreakLazy, option, value, d_handler);
2008
2
  d_holder->sygusSymBreakLazy = value;
2009
2
  d_holder->sygusSymBreakLazy__setByUser__ = true;
2010
2
  Trace("options") << "user assigned option sygusSymBreakLazy" << std::endl;
2011
2012
2
}
2013
template <> void Options::assignBool(
2014
    options::sygusSymBreakPbe__option_t,
2015
    std::string option,
2016
    bool value)
2017
{
2018
  runBoolPredicates(options::sygusSymBreakPbe, option, value, d_handler);
2019
  d_holder->sygusSymBreakPbe = value;
2020
  d_holder->sygusSymBreakPbe__setByUser__ = true;
2021
  Trace("options") << "user assigned option sygusSymBreakPbe" << std::endl;
2022
2023
}
2024
2
template <> void Options::assignBool(
2025
    options::sygusSymBreakRlv__option_t,
2026
    std::string option,
2027
    bool value)
2028
{
2029
2
  runBoolPredicates(options::sygusSymBreakRlv, option, value, d_handler);
2030
2
  d_holder->sygusSymBreakRlv = value;
2031
2
  d_holder->sygusSymBreakRlv__setByUser__ = true;
2032
2
  Trace("options") << "user assigned option sygusSymBreakRlv" << std::endl;
2033
2034
2
}
2035
template <> options::decisionRandomWeight__option_t::type runHandlerAndPredicates(
2036
    options::decisionRandomWeight__option_t,
2037
    std::string option,
2038
    std::string optionarg,
2039
    options::OptionsHandler* handler)
2040
{
2041
  options::decisionRandomWeight__option_t::type retval = handleOption<int>(option, optionarg);
2042
2043
  return retval;
2044
}
2045
template <> void Options::assign(
2046
    options::decisionRandomWeight__option_t,
2047
    std::string option,
2048
    std::string value)
2049
{
2050
  d_holder->decisionRandomWeight =
2051
    runHandlerAndPredicates(options::decisionRandomWeight, option, value, d_handler);
2052
  d_holder->decisionRandomWeight__setByUser__ = true;
2053
  Trace("options") << "user assigned option decisionRandomWeight" << std::endl;
2054
2055
}
2056
template <> options::decisionThreshold__option_t::type runHandlerAndPredicates(
2057
    options::decisionThreshold__option_t,
2058
    std::string option,
2059
    std::string optionarg,
2060
    options::OptionsHandler* handler)
2061
{
2062
  options::decisionThreshold__option_t::type retval = handleOption<decision::DecisionWeight>(option, optionarg);
2063
2064
  return retval;
2065
}
2066
template <> void Options::assign(
2067
    options::decisionThreshold__option_t,
2068
    std::string option,
2069
    std::string value)
2070
{
2071
  d_holder->decisionThreshold =
2072
    runHandlerAndPredicates(options::decisionThreshold, option, value, d_handler);
2073
  d_holder->decisionThreshold__setByUser__ = true;
2074
  Trace("options") << "user assigned option decisionThreshold" << std::endl;
2075
2076
}
2077
template <> void Options::assignBool(
2078
    options::decisionUseWeight__option_t,
2079
    std::string option,
2080
    bool value)
2081
{
2082
  runBoolPredicates(options::decisionUseWeight, option, value, d_handler);
2083
  d_holder->decisionUseWeight = value;
2084
  d_holder->decisionUseWeight__setByUser__ = true;
2085
  Trace("options") << "user assigned option decisionUseWeight" << std::endl;
2086
2087
}
2088
template <> options::decisionWeightInternal__option_t::type runHandlerAndPredicates(
2089
    options::decisionWeightInternal__option_t,
2090
    std::string option,
2091
    std::string optionarg,
2092
    options::OptionsHandler* handler)
2093
{
2094
  options::decisionWeightInternal__option_t::type retval = stringToDecisionWeightInternal(option, optionarg);
2095
2096
  return retval;
2097
}
2098
template <> void Options::assign(
2099
    options::decisionWeightInternal__option_t,
2100
    std::string option,
2101
    std::string value)
2102
{
2103
  d_holder->decisionWeightInternal =
2104
    runHandlerAndPredicates(options::decisionWeightInternal, option, value, d_handler);
2105
  d_holder->decisionWeightInternal__setByUser__ = true;
2106
  Trace("options") << "user assigned option decisionWeightInternal" << std::endl;
2107
2108
}
2109
77
template <> options::decisionMode__option_t::type runHandlerAndPredicates(
2110
    options::decisionMode__option_t,
2111
    std::string option,
2112
    std::string optionarg,
2113
    options::OptionsHandler* handler)
2114
{
2115
77
  options::decisionMode__option_t::type retval = stringToDecisionMode(option, optionarg);
2116
77
  handler->setDecisionModeStopOnly(option, retval);
2117
77
  return retval;
2118
}
2119
77
template <> void Options::assign(
2120
    options::decisionMode__option_t,
2121
    std::string option,
2122
    std::string value)
2123
{
2124
154
  d_holder->decisionMode =
2125
231
    runHandlerAndPredicates(options::decisionMode, option, value, d_handler);
2126
77
  d_holder->decisionMode__setByUser__ = true;
2127
77
  Trace("options") << "user assigned option decisionMode" << std::endl;
2128
2129
77
}
2130
template <> void Options::assignBool(
2131
    options::decisionStopOnly__option_t,
2132
    std::string option,
2133
    bool value)
2134
{
2135
  runBoolPredicates(options::decisionStopOnly, option, value, d_handler);
2136
  d_holder->decisionStopOnly = value;
2137
  d_holder->decisionStopOnly__setByUser__ = true;
2138
  Trace("options") << "user assigned option decisionStopOnly" << std::endl;
2139
2140
}
2141
1
template <> options::defaultDagThresh__option_t::type runHandlerAndPredicates(
2142
    options::defaultDagThresh__option_t,
2143
    std::string option,
2144
    std::string optionarg,
2145
    options::OptionsHandler* handler)
2146
{
2147
1
  options::defaultDagThresh__option_t::type retval = handleOption<int>(option, optionarg);
2148
1
  handler->setDefaultDagThreshPredicate(option, retval);
2149
1
  return retval;
2150
}
2151
1
template <> void Options::assign(
2152
    options::defaultDagThresh__option_t,
2153
    std::string option,
2154
    std::string value)
2155
{
2156
2
  d_holder->defaultDagThresh =
2157
3
    runHandlerAndPredicates(options::defaultDagThresh, option, value, d_handler);
2158
1
  d_holder->defaultDagThresh__setByUser__ = true;
2159
1
  Trace("options") << "user assigned option defaultDagThresh" << std::endl;
2160
2161
1
}
2162
template <> options::defaultExprDepth__option_t::type runHandlerAndPredicates(
2163
    options::defaultExprDepth__option_t,
2164
    std::string option,
2165
    std::string optionarg,
2166
    options::OptionsHandler* handler)
2167
{
2168
  options::defaultExprDepth__option_t::type retval = handleOption<int>(option, optionarg);
2169
  handler->setDefaultExprDepthPredicate(option, retval);
2170
  return retval;
2171
}
2172
template <> void Options::assign(
2173
    options::defaultExprDepth__option_t,
2174
    std::string option,
2175
    std::string value)
2176
{
2177
  d_holder->defaultExprDepth =
2178
    runHandlerAndPredicates(options::defaultExprDepth, option, value, d_handler);
2179
  d_holder->defaultExprDepth__setByUser__ = true;
2180
  Trace("options") << "user assigned option defaultExprDepth" << std::endl;
2181
2182
}
2183
template <> void Options::assignBool(
2184
    options::typeChecking__option_t,
2185
    std::string option,
2186
    bool value)
2187
{
2188
  runBoolPredicates(options::typeChecking, option, value, d_handler);
2189
  d_holder->typeChecking = value;
2190
  d_holder->typeChecking__setByUser__ = true;
2191
  Trace("options") << "user assigned option typeChecking" << std::endl;
2192
2193
}
2194
20
template <> void Options::assignBool(
2195
    options::fpExp__option_t,
2196
    std::string option,
2197
    bool value)
2198
{
2199
20
  runBoolPredicates(options::fpExp, option, value, d_handler);
2200
20
  d_holder->fpExp = value;
2201
20
  d_holder->fpExp__setByUser__ = true;
2202
20
  Trace("options") << "user assigned option fpExp" << std::endl;
2203
2204
20
}
2205
template <> void Options::assignBool(
2206
    options::earlyExit__option_t,
2207
    std::string option,
2208
    bool value)
2209
{
2210
  runBoolPredicates(options::earlyExit, option, value, d_handler);
2211
  d_holder->earlyExit = value;
2212
  d_holder->earlyExit__setByUser__ = true;
2213
  Trace("options") << "user assigned option earlyExit" << std::endl;
2214
2215
}
2216
template <> void Options::assignBool(
2217
    options::help__option_t,
2218
    std::string option,
2219
    bool value)
2220
{
2221
  runBoolPredicates(options::help, option, value, d_handler);
2222
  d_holder->help = value;
2223
  d_holder->help__setByUser__ = true;
2224
  Trace("options") << "user assigned option help" << std::endl;
2225
2226
}
2227
template <> void Options::assignBool(
2228
    options::interactive__option_t,
2229
    std::string option,
2230
    bool value)
2231
{
2232
  runBoolPredicates(options::interactive, option, value, d_handler);
2233
  d_holder->interactive = value;
2234
  d_holder->interactive__setByUser__ = true;
2235
  Trace("options") << "user assigned option interactive" << std::endl;
2236
2237
}
2238
template <> void Options::assignBool(
2239
    options::interactivePrompt__option_t,
2240
    std::string option,
2241
    bool value)
2242
{
2243
  runBoolPredicates(options::interactivePrompt, option, value, d_handler);
2244
  d_holder->interactivePrompt = value;
2245
  d_holder->interactivePrompt__setByUser__ = true;
2246
  Trace("options") << "user assigned option interactivePrompt" << std::endl;
2247
2248
}
2249
template <> options::seed__option_t::type runHandlerAndPredicates(
2250
    options::seed__option_t,
2251
    std::string option,
2252
    std::string optionarg,
2253
    options::OptionsHandler* handler)
2254
{
2255
  options::seed__option_t::type retval = handleOption<uint64_t>(option, optionarg);
2256
2257
  return retval;
2258
}
2259
template <> void Options::assign(
2260
    options::seed__option_t,
2261
    std::string option,
2262
    std::string value)
2263
{
2264
  d_holder->seed =
2265
    runHandlerAndPredicates(options::seed, option, value, d_handler);
2266
  d_holder->seed__setByUser__ = true;
2267
  Trace("options") << "user assigned option seed" << std::endl;
2268
2269
}
2270
template <> void Options::assignBool(
2271
    options::segvSpin__option_t,
2272
    std::string option,
2273
    bool value)
2274
{
2275
  runBoolPredicates(options::segvSpin, option, value, d_handler);
2276
  d_holder->segvSpin = value;
2277
  d_holder->segvSpin__setByUser__ = true;
2278
  Trace("options") << "user assigned option segvSpin" << std::endl;
2279
2280
}
2281
template <> options::tearDownIncremental__option_t::type runHandlerAndPredicates(
2282
    options::tearDownIncremental__option_t,
2283
    std::string option,
2284
    std::string optionarg,
2285
    options::OptionsHandler* handler)
2286
{
2287
  options::tearDownIncremental__option_t::type retval = handleOption<int>(option, optionarg);
2288
2289
  return retval;
2290
}
2291
template <> void Options::assign(
2292
    options::tearDownIncremental__option_t,
2293
    std::string option,
2294
    std::string value)
2295
{
2296
  d_holder->tearDownIncremental =
2297
    runHandlerAndPredicates(options::tearDownIncremental, option, value, d_handler);
2298
  d_holder->tearDownIncremental__setByUser__ = true;
2299
  Trace("options") << "user assigned option tearDownIncremental" << std::endl;
2300
2301
}
2302
template <> void Options::assignBool(
2303
    options::version__option_t,
2304
    std::string option,
2305
    bool value)
2306
{
2307
  runBoolPredicates(options::version, option, value, d_handler);
2308
  d_holder->version = value;
2309
  d_holder->version__setByUser__ = true;
2310
  Trace("options") << "user assigned option version" << std::endl;
2311
2312
}
2313
template <> void Options::assignBool(
2314
    options::filesystemAccess__option_t,
2315
    std::string option,
2316
    bool value)
2317
{
2318
  runBoolPredicates(options::filesystemAccess, option, value, d_handler);
2319
  d_holder->filesystemAccess = value;
2320
  d_holder->filesystemAccess__setByUser__ = true;
2321
  Trace("options") << "user assigned option filesystemAccess" << std::endl;
2322
2323
}
2324
9
template <> options::forceLogicString__option_t::type runHandlerAndPredicates(
2325
    options::forceLogicString__option_t,
2326
    std::string option,
2327
    std::string optionarg,
2328
    options::OptionsHandler* handler)
2329
{
2330
9
  options::forceLogicString__option_t::type retval = handleOption<std::string>(option, optionarg);
2331
2332
9
  return retval;
2333
}
2334
9
template <> void Options::assign(
2335
    options::forceLogicString__option_t,
2336
    std::string option,
2337
    std::string value)
2338
{
2339
18
  d_holder->forceLogicString =
2340
27
    runHandlerAndPredicates(options::forceLogicString, option, value, d_handler);
2341
9
  d_holder->forceLogicString__setByUser__ = true;
2342
9
  Trace("options") << "user assigned option forceLogicString" << std::endl;
2343
2344
9
}
2345
16
template <> void Options::assignBool(
2346
    options::globalDeclarations__option_t,
2347
    std::string option,
2348
    bool value)
2349
{
2350
48
  runBoolPredicates(options::globalDeclarations, option, value, d_handler);
2351
16
  d_holder->globalDeclarations = value;
2352
16
  d_holder->globalDeclarations__setByUser__ = true;
2353
16
  Trace("options") << "user assigned option globalDeclarations" << std::endl;
2354
2355
16
}
2356
template <> void Options::assignBool(
2357
    options::memoryMap__option_t,
2358
    std::string option,
2359
    bool value)
2360
{
2361
  runBoolPredicates(options::memoryMap, option, value, d_handler);
2362
  d_holder->memoryMap = value;
2363
  d_holder->memoryMap__setByUser__ = true;
2364
  Trace("options") << "user assigned option memoryMap" << std::endl;
2365
2366
}
2367
template <> void Options::assignBool(
2368
    options::semanticChecks__option_t,
2369
    std::string option,
2370
    bool value)
2371
{
2372
  runBoolPredicates(options::semanticChecks, option, value, d_handler);
2373
  d_holder->semanticChecks = value;
2374
  d_holder->semanticChecks__setByUser__ = true;
2375
  Trace("options") << "user assigned option semanticChecks" << std::endl;
2376
2377
}
2378
10
template <> void Options::assignBool(
2379
    options::strictParsing__option_t,
2380
    std::string option,
2381
    bool value)
2382
{
2383
10
  runBoolPredicates(options::strictParsing, option, value, d_handler);
2384
10
  d_holder->strictParsing = value;
2385
10
  d_holder->strictParsing__setByUser__ = true;
2386
10
  Trace("options") << "user assigned option strictParsing" << std::endl;
2387
2388
10
}
2389
template <> void Options::assignBool(
2390
    options::flattenHOChains__option_t,
2391
    std::string option,
2392
    bool value)
2393
{
2394
  runBoolPredicates(options::flattenHOChains, option, value, d_handler);
2395
  d_holder->flattenHOChains = value;
2396
  d_holder->flattenHOChains__setByUser__ = true;
2397
  Trace("options") << "user assigned option flattenHOChains" << std::endl;
2398
2399
}
2400
template <> options::instFormatMode__option_t::type runHandlerAndPredicates(
2401
    options::instFormatMode__option_t,
2402
    std::string option,
2403
    std::string optionarg,
2404
    options::OptionsHandler* handler)
2405
{
2406
  options::instFormatMode__option_t::type retval = handler->stringToInstFormatMode(option, optionarg);
2407
2408
  return retval;
2409
}
2410
template <> void Options::assign(
2411
    options::instFormatMode__option_t,
2412
    std::string option,
2413
    std::string value)
2414
{
2415
  d_holder->instFormatMode =
2416
    runHandlerAndPredicates(options::instFormatMode, option, value, d_handler);
2417
  d_holder->instFormatMode__setByUser__ = true;
2418
  Trace("options") << "user assigned option instFormatMode" << std::endl;
2419
2420
}
2421
template <> options::modelFormatMode__option_t::type runHandlerAndPredicates(
2422
    options::modelFormatMode__option_t,
2423
    std::string option,
2424
    std::string optionarg,
2425
    options::OptionsHandler* handler)
2426
{
2427
  options::modelFormatMode__option_t::type retval = stringToModelFormatMode(option, optionarg);
2428
2429
  return retval;
2430
}
2431
template <> void Options::assign(
2432
    options::modelFormatMode__option_t,
2433
    std::string option,
2434
    std::string value)
2435
{
2436
  d_holder->modelFormatMode =
2437
    runHandlerAndPredicates(options::modelFormatMode, option, value, d_handler);
2438
  d_holder->modelFormatMode__setByUser__ = true;
2439
  Trace("options") << "user assigned option modelFormatMode" << std::endl;
2440
2441
}
2442
8
template <> void Options::assignBool(
2443
    options::printInstFull__option_t,
2444
    std::string option,
2445
    bool value)
2446
{
2447
8
  runBoolPredicates(options::printInstFull, option, value, d_handler);
2448
8
  d_holder->printInstFull = value;
2449
8
  d_holder->printInstFull__setByUser__ = true;
2450
8
  Trace("options") << "user assigned option printInstFull" << std::endl;
2451
2452
8
}
2453
3
template <> options::printInstMode__option_t::type runHandlerAndPredicates(
2454
    options::printInstMode__option_t,
2455
    std::string option,
2456
    std::string optionarg,
2457
    options::OptionsHandler* handler)
2458
{
2459
3
  options::printInstMode__option_t::type retval = stringToPrintInstMode(option, optionarg);
2460
2461
3
  return retval;
2462
}
2463
3
template <> void Options::assign(
2464
    options::printInstMode__option_t,
2465
    std::string option,
2466
    std::string value)
2467
{
2468
6
  d_holder->printInstMode =
2469
9
    runHandlerAndPredicates(options::printInstMode, option, value, d_handler);
2470
3
  d_holder->printInstMode__setByUser__ = true;
2471
3
  Trace("options") << "user assigned option printInstMode" << std::endl;
2472
2473
3
}
2474
2
template <> void Options::assignBool(
2475
    options::proofEagerChecking__option_t,
2476
    std::string option,
2477
    bool value)
2478
{
2479
2
  runBoolPredicates(options::proofEagerChecking, option, value, d_handler);
2480
2
  d_holder->proofEagerChecking = value;
2481
2
  d_holder->proofEagerChecking__setByUser__ = true;
2482
2
  Trace("options") << "user assigned option proofEagerChecking" << std::endl;
2483
2484
2
}
2485
template <> options::proofFormatMode__option_t::type runHandlerAndPredicates(
2486
    options::proofFormatMode__option_t,
2487
    std::string option,
2488
    std::string optionarg,
2489
    options::OptionsHandler* handler)
2490
{
2491
  options::proofFormatMode__option_t::type retval = stringToProofFormatMode(option, optionarg);
2492
2493
  return retval;
2494
}
2495
template <> void Options::assign(
2496
    options::proofFormatMode__option_t,
2497
    std::string option,
2498
    std::string value)
2499
{
2500
  d_holder->proofFormatMode =
2501
    runHandlerAndPredicates(options::proofFormatMode, option, value, d_handler);
2502
  d_holder->proofFormatMode__setByUser__ = true;
2503
  Trace("options") << "user assigned option proofFormatMode" << std::endl;
2504
2505
}
2506
template <> options::proofGranularityMode__option_t::type runHandlerAndPredicates(
2507
    options::proofGranularityMode__option_t,
2508
    std::string option,
2509
    std::string optionarg,
2510
    options::OptionsHandler* handler)
2511
{
2512
  options::proofGranularityMode__option_t::type retval = stringToProofGranularityMode(option, optionarg);
2513
2514
  return retval;
2515
}
2516
template <> void Options::assign(
2517
    options::proofGranularityMode__option_t,
2518
    std::string option,
2519
    std::string value)
2520
{
2521
  d_holder->proofGranularityMode =
2522
    runHandlerAndPredicates(options::proofGranularityMode, option, value, d_handler);
2523
  d_holder->proofGranularityMode__setByUser__ = true;
2524
  Trace("options") << "user assigned option proofGranularityMode" << std::endl;
2525
2526
}
2527
template <> options::proofPedantic__option_t::type runHandlerAndPredicates(
2528
    options::proofPedantic__option_t,
2529
    std::string option,
2530
    std::string optionarg,
2531
    options::OptionsHandler* handler)
2532
{
2533
  options::proofPedantic__option_t::type retval = handleOption<uint32_t>(option, optionarg);
2534
2535
  return retval;
2536
}
2537
template <> void Options::assign(
2538
    options::proofPedantic__option_t,
2539
    std::string option,
2540
    std::string value)
2541
{
2542
  d_holder->proofPedantic =
2543
    runHandlerAndPredicates(options::proofPedantic, option, value, d_handler);
2544
  d_holder->proofPedantic__setByUser__ = true;
2545
  Trace("options") << "user assigned option proofPedantic" << std::endl;
2546
2547
}
2548
template <> void Options::assignBool(
2549
    options::proofPrintConclusion__option_t,
2550
    std::string option,
2551
    bool value)
2552
{
2553
  runBoolPredicates(options::proofPrintConclusion, option, value, d_handler);
2554
  d_holder->proofPrintConclusion = value;
2555
  d_holder->proofPrintConclusion__setByUser__ = true;
2556
  Trace("options") << "user assigned option proofPrintConclusion" << std::endl;
2557
2558
}
2559
template <> void Options::assignBool(
2560
    options::minisatDumpDimacs__option_t,
2561
    std::string option,
2562
    bool value)
2563
{
2564
  runBoolPredicates(options::minisatDumpDimacs, option, value, d_handler);
2565
  d_holder->minisatDumpDimacs = value;
2566
  d_holder->minisatDumpDimacs__setByUser__ = true;
2567
  Trace("options") << "user assigned option minisatDumpDimacs" << std::endl;
2568
2569
}
2570
template <> void Options::assignBool(
2571
    options::minisatUseElim__option_t,
2572
    std::string option,
2573
    bool value)
2574
{
2575
  runBoolPredicates(options::minisatUseElim, option, value, d_handler);
2576
  d_holder->minisatUseElim = value;
2577
  d_holder->minisatUseElim__setByUser__ = true;
2578
  Trace("options") << "user assigned option minisatUseElim" << std::endl;
2579
2580
}
2581
template <> options::satRandomFreq__option_t::type runHandlerAndPredicates(
2582
    options::satRandomFreq__option_t,
2583
    std::string option,
2584
    std::string optionarg,
2585
    options::OptionsHandler* handler)
2586
{
2587
  options::satRandomFreq__option_t::type retval = handleOption<double>(option, optionarg);
2588
  handler->doubleGreaterOrEqual0(option, retval);
2589
handler->doubleLessOrEqual1(option, retval);
2590
  return retval;
2591
}
2592
template <> void Options::assign(
2593
    options::satRandomFreq__option_t,
2594
    std::string option,
2595
    std::string value)
2596
{
2597
  d_holder->satRandomFreq =
2598
    runHandlerAndPredicates(options::satRandomFreq, option, value, d_handler);
2599
  d_holder->satRandomFreq__setByUser__ = true;
2600
  Trace("options") << "user assigned option satRandomFreq" << std::endl;
2601
2602
}
2603
template <> options::satRandomSeed__option_t::type runHandlerAndPredicates(
2604
    options::satRandomSeed__option_t,
2605
    std::string option,
2606
    std::string optionarg,
2607
    options::OptionsHandler* handler)
2608
{
2609
  options::satRandomSeed__option_t::type retval = handleOption<uint32_t>(option, optionarg);
2610
2611
  return retval;
2612
}
2613
template <> void Options::assign(
2614
    options::satRandomSeed__option_t,
2615
    std::string option,
2616
    std::string value)
2617
{
2618
  d_holder->satRandomSeed =
2619
    runHandlerAndPredicates(options::satRandomSeed, option, value, d_handler);
2620
  d_holder->satRandomSeed__setByUser__ = true;
2621
  Trace("options") << "user assigned option satRandomSeed" << std::endl;
2622
2623
}
2624
template <> void Options::assignBool(
2625
    options::sat_refine_conflicts__option_t,
2626
    std::string option,
2627
    bool value)
2628
{
2629
  runBoolPredicates(options::sat_refine_conflicts, option, value, d_handler);
2630
  d_holder->sat_refine_conflicts = value;
2631
  d_holder->sat_refine_conflicts__setByUser__ = true;
2632
  Trace("options") << "user assigned option sat_refine_conflicts" << std::endl;
2633
2634
}
2635
template <> options::satRestartFirst__option_t::type runHandlerAndPredicates(
2636
    options::satRestartFirst__option_t,
2637
    std::string option,
2638
    std::string optionarg,
2639
    options::OptionsHandler* handler)
2640
{
2641
  options::satRestartFirst__option_t::type retval = handleOption<unsigned>(option, optionarg);
2642
2643
  return retval;
2644
}
2645
template <> void Options::assign(
2646
    options::satRestartFirst__option_t,
2647
    std::string option,
2648
    std::string value)
2649
{
2650
  d_holder->satRestartFirst =
2651
    runHandlerAndPredicates(options::satRestartFirst, option, value, d_handler);
2652
  d_holder->satRestartFirst__setByUser__ = true;
2653
  Trace("options") << "user assigned option satRestartFirst" << std::endl;
2654
2655
}
2656
template <> options::satRestartInc__option_t::type runHandlerAndPredicates(
2657
    options::satRestartInc__option_t,
2658
    std::string option,
2659
    std::string optionarg,
2660
    options::OptionsHandler* handler)
2661
{
2662
  options::satRestartInc__option_t::type retval = handleOption<double>(option, optionarg);
2663
  handler->doubleGreaterOrEqual0(option, retval);
2664
  return retval;
2665
}
2666
template <> void Options::assign(
2667
    options::satRestartInc__option_t,
2668
    std::string option,
2669
    std::string value)
2670
{
2671
  d_holder->satRestartInc =
2672
    runHandlerAndPredicates(options::satRestartInc, option, value, d_handler);
2673
  d_holder->satRestartInc__setByUser__ = true;
2674
  Trace("options") << "user assigned option satRestartInc" << std::endl;
2675
2676
}
2677
5
template <> void Options::assignBool(
2678
    options::aggressiveMiniscopeQuant__option_t,
2679
    std::string option,
2680
    bool value)
2681
{
2682
5
  runBoolPredicates(options::aggressiveMiniscopeQuant, option, value, d_handler);
2683
5
  d_holder->aggressiveMiniscopeQuant = value;
2684
5
  d_holder->aggressiveMiniscopeQuant__setByUser__ = true;
2685
5
  Trace("options") << "user assigned option aggressiveMiniscopeQuant" << std::endl;
2686
2687
5
}
2688
5
template <> options::cegisSample__option_t::type runHandlerAndPredicates(
2689
    options::cegisSample__option_t,
2690
    std::string option,
2691
    std::string optionarg,
2692
    options::OptionsHandler* handler)
2693
{
2694
5
  options::cegisSample__option_t::type retval = stringToCegisSampleMode(option, optionarg);
2695
2696
5
  return retval;
2697
}
2698
5
template <> void Options::assign(
2699
    options::cegisSample__option_t,
2700
    std::string option,
2701
    std::string value)
2702
{
2703
10
  d_holder->cegisSample =
2704
15
    runHandlerAndPredicates(options::cegisSample, option, value, d_handler);
2705
5
  d_holder->cegisSample__setByUser__ = true;
2706
5
  Trace("options") << "user assigned option cegisSample" << std::endl;
2707
2708
5
}
2709
18
template <> void Options::assignBool(
2710
    options::cegqi__option_t,
2711
    std::string option,
2712
    bool value)
2713
{
2714
18
  runBoolPredicates(options::cegqi, option, value, d_handler);
2715
18
  d_holder->cegqi = value;
2716
18
  d_holder->cegqi__setByUser__ = true;
2717
18
  Trace("options") << "user assigned option cegqi" << std::endl;
2718
2719
18
}
2720
15
template <> void Options::assignBool(
2721
    options::cegqiAll__option_t,
2722
    std::string option,
2723
    bool value)
2724
{
2725
15
  runBoolPredicates(options::cegqiAll, option, value, d_handler);
2726
15
  d_holder->cegqiAll = value;
2727
15
  d_holder->cegqiAll__setByUser__ = true;
2728
15
  Trace("options") << "user assigned option cegqiAll" << std::endl;
2729
2730
15
}
2731
107
template <> void Options::assignBool(
2732
    options::cegqiBv__option_t,
2733
    std::string option,
2734
    bool value)
2735
{
2736
107
  runBoolPredicates(options::cegqiBv, option, value, d_handler);
2737
107
  d_holder->cegqiBv = value;
2738
107
  d_holder->cegqiBv__setByUser__ = true;
2739
107
  Trace("options") << "user assigned option cegqiBv" << std::endl;
2740
2741
107
}
2742
template <> void Options::assignBool(
2743
    options::cegqiBvConcInv__option_t,
2744
    std::string option,
2745
    bool value)
2746
{
2747
  runBoolPredicates(options::cegqiBvConcInv, option, value, d_handler);
2748
  d_holder->cegqiBvConcInv = value;
2749
  d_holder->cegqiBvConcInv__setByUser__ = true;
2750
  Trace("options") << "user assigned option cegqiBvConcInv" << std::endl;
2751
2752
}
2753
82
template <> options::cegqiBvIneqMode__option_t::type runHandlerAndPredicates(
2754
    options::cegqiBvIneqMode__option_t,
2755
    std::string option,
2756
    std::string optionarg,
2757
    options::OptionsHandler* handler)
2758
{
2759
82
  options::cegqiBvIneqMode__option_t::type retval = stringToCegqiBvIneqMode(option, optionarg);
2760
2761
82
  return retval;
2762
}
2763
82
template <> void Options::assign(
2764
    options::cegqiBvIneqMode__option_t,
2765
    std::string option,
2766
    std::string value)
2767
{
2768
164
  d_holder->cegqiBvIneqMode =
2769
246
    runHandlerAndPredicates(options::cegqiBvIneqMode, option, value, d_handler);
2770
82
  d_holder->cegqiBvIneqMode__setByUser__ = true;
2771
82
  Trace("options") << "user assigned option cegqiBvIneqMode" << std::endl;
2772
2773
82
}
2774
template <> void Options::assignBool(
2775
    options::cegqiBvInterleaveValue__option_t,
2776
    std::string option,
2777
    bool value)
2778
{
2779
  runBoolPredicates(options::cegqiBvInterleaveValue, option, value, d_handler);
2780
  d_holder->cegqiBvInterleaveValue = value;
2781
  d_holder->cegqiBvInterleaveValue__setByUser__ = true;
2782
  Trace("options") << "user assigned option cegqiBvInterleaveValue" << std::endl;
2783
2784
}
2785
template <> void Options::assignBool(
2786
    options::cegqiBvLinearize__option_t,
2787
    std::string option,
2788
    bool value)
2789
{
2790
  runBoolPredicates(options::cegqiBvLinearize, option, value, d_handler);
2791
  d_holder->cegqiBvLinearize = value;
2792
  d_holder->cegqiBvLinearize__setByUser__ = true;
2793
  Trace("options") << "user assigned option cegqiBvLinearize" << std::endl;
2794
2795
}
2796
2
template <> void Options::assignBool(
2797
    options::cegqiBvRmExtract__option_t,
2798
    std::string option,
2799
    bool value)
2800
{
2801
2
  runBoolPredicates(options::cegqiBvRmExtract, option, value, d_handler);
2802
2
  d_holder->cegqiBvRmExtract = value;
2803
2
  d_holder->cegqiBvRmExtract__setByUser__ = true;
2804
2
  Trace("options") << "user assigned option cegqiBvRmExtract" << std::endl;
2805
2806
2
}
2807
template <> void Options::assignBool(
2808
    options::cegqiBvSolveNl__option_t,
2809
    std::string option,
2810
    bool value)
2811
{
2812
  runBoolPredicates(options::cegqiBvSolveNl, option, value, d_handler);
2813
  d_holder->cegqiBvSolveNl = value;
2814
  d_holder->cegqiBvSolveNl__setByUser__ = true;
2815
  Trace("options") << "user assigned option cegqiBvSolveNl" << std::endl;
2816
2817
}
2818
597
template <> void Options::assignBool(
2819
    options::cegqiFullEffort__option_t,
2820
    std::string option,
2821
    bool value)
2822
{
2823
597
  runBoolPredicates(options::cegqiFullEffort, option, value, d_handler);
2824
597
  d_holder->cegqiFullEffort = value;
2825
597
  d_holder->cegqiFullEffort__setByUser__ = true;
2826
597
  Trace("options") << "user assigned option cegqiFullEffort" << std::endl;
2827
2828
597
}
2829
template <> void Options::assignBool(
2830
    options::cegqiInnermost__option_t,
2831
    std::string option,
2832
    bool value)
2833
{
2834
  runBoolPredicates(options::cegqiInnermost, option, value, d_handler);
2835
  d_holder->cegqiInnermost = value;
2836
  d_holder->cegqiInnermost__setByUser__ = true;
2837
  Trace("options") << "user assigned option cegqiInnermost" << std::endl;
2838
2839
}
2840
template <> void Options::assignBool(
2841
    options::cegqiMidpoint__option_t,
2842
    std::string option,
2843
    bool value)
2844
{
2845
  runBoolPredicates(options::cegqiMidpoint, option, value, d_handler);
2846
  d_holder->cegqiMidpoint = value;
2847
  d_holder->cegqiMidpoint__setByUser__ = true;
2848
  Trace("options") << "user assigned option cegqiMidpoint" << std::endl;
2849
2850
}
2851
template <> void Options::assignBool(
2852
    options::cegqiMinBounds__option_t,
2853
    std::string option,
2854
    bool value)
2855
{
2856
  runBoolPredicates(options::cegqiMinBounds, option, value, d_handler);
2857
  d_holder->cegqiMinBounds = value;
2858
  d_holder->cegqiMinBounds__setByUser__ = true;
2859
  Trace("options") << "user assigned option cegqiMinBounds" << std::endl;
2860
2861
}
2862
template <> void Options::assignBool(
2863
    options::cegqiModel__option_t,
2864
    std::string option,
2865
    bool value)
2866
{
2867
  runBoolPredicates(options::cegqiModel, option, value, d_handler);
2868
  d_holder->cegqiModel = value;
2869
  d_holder->cegqiModel__setByUser__ = true;
2870
  Trace("options") << "user assigned option cegqiModel" << std::endl;
2871
2872
}
2873
3
template <> void Options::assignBool(
2874
    options::cegqiMultiInst__option_t,
2875
    std::string option,
2876
    bool value)
2877
{
2878
3
  runBoolPredicates(options::cegqiMultiInst, option, value, d_handler);
2879
3
  d_holder->cegqiMultiInst = value;
2880
3
  d_holder->cegqiMultiInst__setByUser__ = true;
2881
3
  Trace("options") << "user assigned option cegqiMultiInst" << std::endl;
2882
2883
3
}
2884
17
template <> void Options::assignBool(
2885
    options::cegqiNestedQE__option_t,
2886
    std::string option,
2887
    bool value)
2888
{
2889
17
  runBoolPredicates(options::cegqiNestedQE, option, value, d_handler);
2890
17
  d_holder->cegqiNestedQE = value;
2891
17
  d_holder->cegqiNestedQE__setByUser__ = true;
2892
17
  Trace("options") << "user assigned option cegqiNestedQE" << std::endl;
2893
2894
17
}
2895
template <> void Options::assignBool(
2896
    options::cegqiNopt__option_t,
2897
    std::string option,
2898
    bool value)
2899
{
2900
  runBoolPredicates(options::cegqiNopt, option, value, d_handler);
2901
  d_holder->cegqiNopt = value;
2902
  d_holder->cegqiNopt__setByUser__ = true;
2903
  Trace("options") << "user assigned option cegqiNopt" << std::endl;
2904
2905
}
2906
template <> void Options::assignBool(
2907
    options::cegqiRepeatLit__option_t,
2908
    std::string option,
2909
    bool value)
2910
{
2911
  runBoolPredicates(options::cegqiRepeatLit, option, value, d_handler);
2912
  d_holder->cegqiRepeatLit = value;
2913
  d_holder->cegqiRepeatLit__setByUser__ = true;
2914
  Trace("options") << "user assigned option cegqiRepeatLit" << std::endl;
2915
2916
}
2917
template <> void Options::assignBool(
2918
    options::cegqiRoundUpLowerLia__option_t,
2919
    std::string option,
2920
    bool value)
2921
{
2922
  runBoolPredicates(options::cegqiRoundUpLowerLia, option, value, d_handler);
2923
  d_holder->cegqiRoundUpLowerLia = value;
2924
  d_holder->cegqiRoundUpLowerLia__setByUser__ = true;
2925
  Trace("options") << "user assigned option cegqiRoundUpLowerLia" << std::endl;
2926
2927
}
2928
template <> void Options::assignBool(
2929
    options::cegqiSat__option_t,
2930
    std::string option,
2931
    bool value)
2932
{
2933
  runBoolPredicates(options::cegqiSat, option, value, d_handler);
2934
  d_holder->cegqiSat = value;
2935
  d_holder->cegqiSat__setByUser__ = true;
2936
  Trace("options") << "user assigned option cegqiSat" << std::endl;
2937
2938
}
2939
6
template <> void Options::assignBool(
2940
    options::cegqiUseInfInt__option_t,
2941
    std::string option,
2942
    bool value)
2943
{
2944
6
  runBoolPredicates(options::cegqiUseInfInt, option, value, d_handler);
2945
6
  d_holder->cegqiUseInfInt = value;
2946
6
  d_holder->cegqiUseInfInt__setByUser__ = true;
2947
6
  Trace("options") << "user assigned option cegqiUseInfInt" << std::endl;
2948
2949
6
}
2950
6
template <> void Options::assignBool(
2951
    options::cegqiUseInfReal__option_t,
2952
    std::string option,
2953
    bool value)
2954
{
2955
6
  runBoolPredicates(options::cegqiUseInfReal, option, value, d_handler);
2956
6
  d_holder->cegqiUseInfReal = value;
2957
6
  d_holder->cegqiUseInfReal__setByUser__ = true;
2958
6
  Trace("options") << "user assigned option cegqiUseInfReal" << std::endl;
2959
2960
6
}
2961
template <> void Options::assignBool(
2962
    options::condVarSplitQuantAgg__option_t,
2963
    std::string option,
2964
    bool value)
2965
{
2966
  runBoolPredicates(options::condVarSplitQuantAgg, option, value, d_handler);
2967
  d_holder->condVarSplitQuantAgg = value;
2968
  d_holder->condVarSplitQuantAgg__setByUser__ = true;
2969
  Trace("options") << "user assigned option condVarSplitQuantAgg" << std::endl;
2970
2971
}
2972
template <> void Options::assignBool(
2973
    options::condVarSplitQuant__option_t,
2974
    std::string option,
2975
    bool value)
2976
{
2977
  runBoolPredicates(options::condVarSplitQuant, option, value, d_handler);
2978
  d_holder->condVarSplitQuant = value;
2979
  d_holder->condVarSplitQuant__setByUser__ = true;
2980
  Trace("options") << "user assigned option condVarSplitQuant" << std::endl;
2981
2982
}
2983
template <> void Options::assignBool(
2984
    options::conjectureFilterActiveTerms__option_t,
2985
    std::string option,
2986
    bool value)
2987
{
2988
  runBoolPredicates(options::conjectureFilterActiveTerms, option, value, d_handler);
2989
  d_holder->conjectureFilterActiveTerms = value;
2990
  d_holder->conjectureFilterActiveTerms__setByUser__ = true;
2991
  Trace("options") << "user assigned option conjectureFilterActiveTerms" << std::endl;
2992
2993
}
2994
template <> void Options::assignBool(
2995
    options::conjectureFilterCanonical__option_t,
2996
    std::string option,
2997
    bool value)
2998
{
2999
  runBoolPredicates(options::conjectureFilterCanonical, option, value, d_handler);
3000
  d_holder->conjectureFilterCanonical = value;
3001
  d_holder->conjectureFilterCanonical__setByUser__ = true;
3002
  Trace("options") << "user assigned option conjectureFilterCanonical" << std::endl;
3003
3004
}
3005
2
template <> void Options::assignBool(
3006
    options::conjectureFilterModel__option_t,
3007
    std::string option,
3008
    bool value)
3009
{
3010
2
  runBoolPredicates(options::conjectureFilterModel, option, value, d_handler);
3011
2
  d_holder->conjectureFilterModel = value;
3012
2
  d_holder->conjectureFilterModel__setByUser__ = true;
3013
2
  Trace("options") << "user assigned option conjectureFilterModel" << std::endl;
3014
3015
2
}
3016
8
template <> void Options::assignBool(
3017
    options::conjectureGen__option_t,
3018
    std::string option,
3019
    bool value)
3020
{
3021
8
  runBoolPredicates(options::conjectureGen, option, value, d_handler);
3022
8
  d_holder->conjectureGen = value;
3023
8
  d_holder->conjectureGen__setByUser__ = true;
3024
8
  Trace("options") << "user assigned option conjectureGen" << std::endl;
3025
3026
8
}
3027
template <> options::conjectureGenGtEnum__option_t::type runHandlerAndPredicates(
3028
    options::conjectureGenGtEnum__option_t,
3029
    std::string option,
3030
    std::string optionarg,
3031
    options::OptionsHandler* handler)
3032
{
3033
  options::conjectureGenGtEnum__option_t::type retval = handleOption<int>(option, optionarg);
3034
3035
  return retval;
3036
}
3037
template <> void Options::assign(
3038
    options::conjectureGenGtEnum__option_t,
3039
    std::string option,
3040
    std::string value)
3041
{
3042
  d_holder->conjectureGenGtEnum =
3043
    runHandlerAndPredicates(options::conjectureGenGtEnum, option, value, d_handler);
3044
  d_holder->conjectureGenGtEnum__setByUser__ = true;
3045
  Trace("options") << "user assigned option conjectureGenGtEnum" << std::endl;
3046
3047
}
3048
template <> options::conjectureGenMaxDepth__option_t::type runHandlerAndPredicates(
3049
    options::conjectureGenMaxDepth__option_t,
3050
    std::string option,
3051
    std::string optionarg,
3052
    options::OptionsHandler* handler)
3053
{
3054
  options::conjectureGenMaxDepth__option_t::type retval = handleOption<int>(option, optionarg);
3055
3056
  return retval;
3057
}
3058
template <> void Options::assign(
3059
    options::conjectureGenMaxDepth__option_t,
3060
    std::string option,
3061
    std::string value)
3062
{
3063
  d_holder->conjectureGenMaxDepth =
3064
    runHandlerAndPredicates(options::conjectureGenMaxDepth, option, value, d_handler);
3065
  d_holder->conjectureGenMaxDepth__setByUser__ = true;
3066
  Trace("options") << "user assigned option conjectureGenMaxDepth" << std::endl;
3067
3068
}
3069
template <> options::conjectureGenPerRound__option_t::type runHandlerAndPredicates(
3070
    options::conjectureGenPerRound__option_t,
3071
    std::string option,
3072
    std::string optionarg,
3073
    options::OptionsHandler* handler)
3074
{
3075
  options::conjectureGenPerRound__option_t::type retval = handleOption<int>(option, optionarg);
3076
3077
  return retval;
3078
}
3079
template <> void Options::assign(
3080
    options::conjectureGenPerRound__option_t,
3081
    std::string option,
3082
    std::string value)
3083
{
3084
  d_holder->conjectureGenPerRound =
3085
    runHandlerAndPredicates(options::conjectureGenPerRound, option, value, d_handler);
3086
  d_holder->conjectureGenPerRound__setByUser__ = true;
3087
  Trace("options") << "user assigned option conjectureGenPerRound" << std::endl;
3088
3089
}
3090
template <> void Options::assignBool(
3091
    options::conjectureUeeIntro__option_t,
3092
    std::string option,
3093
    bool value)
3094
{
3095
  runBoolPredicates(options::conjectureUeeIntro, option, value, d_handler);
3096
  d_holder->conjectureUeeIntro = value;
3097
  d_holder->conjectureUeeIntro__setByUser__ = true;
3098
  Trace("options") << "user assigned option conjectureUeeIntro" << std::endl;
3099
3100
}
3101
2
template <> void Options::assignBool(
3102
    options::conjectureNoFilter__option_t,
3103
    std::string option,
3104
    bool value)
3105
{
3106
2
  runBoolPredicates(options::conjectureNoFilter, option, value, d_handler);
3107
2
  d_holder->conjectureNoFilter = value;
3108
2
  d_holder->conjectureNoFilter__setByUser__ = true;
3109
2
  Trace("options") << "user assigned option conjectureNoFilter" << std::endl;
3110
3111
2
}
3112
2
template <> void Options::assignBool(
3113
    options::debugInst__option_t,
3114
    std::string option,
3115
    bool value)
3116
{
3117
2
  runBoolPredicates(options::debugInst, option, value, d_handler);
3118
2
  d_holder->debugInst = value;
3119
2
  d_holder->debugInst__setByUser__ = true;
3120
2
  Trace("options") << "user assigned option debugInst" << std::endl;
3121
3122
2
}
3123
2
template <> void Options::assignBool(
3124
    options::debugSygus__option_t,
3125
    std::string option,
3126
    bool value)
3127
{
3128
2
  runBoolPredicates(options::debugSygus, option, value, d_handler);
3129
2
  d_holder->debugSygus = value;
3130
2
  d_holder->debugSygus__setByUser__ = true;
3131
2
  Trace("options") << "user assigned option debugSygus" << std::endl;
3132
3133
2
}
3134
template <> void Options::assignBool(
3135
    options::dtStcInduction__option_t,
3136
    std::string option,
3137
    bool value)
3138
{
3139
  runBoolPredicates(options::dtStcInduction, option, value, d_handler);
3140
  d_holder->dtStcInduction = value;
3141
  d_holder->dtStcInduction__setByUser__ = true;
3142
  Trace("options") << "user assigned option dtStcInduction" << std::endl;
3143
3144
}
3145
template <> void Options::assignBool(
3146
    options::dtVarExpandQuant__option_t,
3147
    std::string option,
3148
    bool value)
3149
{
3150
  runBoolPredicates(options::dtVarExpandQuant, option, value, d_handler);
3151
  d_holder->dtVarExpandQuant = value;
3152
  d_holder->dtVarExpandQuant__setByUser__ = true;
3153
  Trace("options") << "user assigned option dtVarExpandQuant" << std::endl;
3154
3155
}
3156
2
template <> void Options::assignBool(
3157
    options::eMatching__option_t,
3158
    std::string option,
3159
    bool value)
3160
{
3161
2
  runBoolPredicates(options::eMatching, option, value, d_handler);
3162
2
  d_holder->eMatching = value;
3163
2
  d_holder->eMatching__setByUser__ = true;
3164
2
  Trace("options") << "user assigned option eMatching" << std::endl;
3165
3166
2
}
3167
template <> void Options::assignBool(
3168
    options::elimTautQuant__option_t,
3169
    std::string option,
3170
    bool value)
3171
{
3172
  runBoolPredicates(options::elimTautQuant, option, value, d_handler);
3173
  d_holder->elimTautQuant = value;
3174
  d_holder->elimTautQuant__setByUser__ = true;
3175
  Trace("options") << "user assigned option elimTautQuant" << std::endl;
3176
3177
}
3178
11
template <> void Options::assignBool(
3179
    options::extRewriteQuant__option_t,
3180
    std::string option,
3181
    bool value)
3182
{
3183
11
  runBoolPredicates(options::extRewriteQuant, option, value, d_handler);
3184
11
  d_holder->extRewriteQuant = value;
3185
11
  d_holder->extRewriteQuant__setByUser__ = true;
3186
11
  Trace("options") << "user assigned option extRewriteQuant" << std::endl;
3187
3188
11
}
3189
156
template <> void Options::assignBool(
3190
    options::finiteModelFind__option_t,
3191
    std::string option,
3192
    bool value)
3193
{
3194
156
  runBoolPredicates(options::finiteModelFind, option, value, d_handler);
3195
156
  d_holder->finiteModelFind = value;
3196
156
  d_holder->finiteModelFind__setByUser__ = true;
3197
156
  Trace("options") << "user assigned option finiteModelFind" << std::endl;
3198
3199
156
}
3200
36
template <> void Options::assignBool(
3201
    options::fmfBound__option_t,
3202
    std::string option,
3203
    bool value)
3204
{
3205
36
  runBoolPredicates(options::fmfBound, option, value, d_handler);
3206
36
  d_holder->fmfBound = value;
3207
36
  d_holder->fmfBound__setByUser__ = true;
3208
36
  Trace("options") << "user assigned option fmfBound" << std::endl;
3209
3210
36
}
3211
11
template <> void Options::assignBool(
3212
    options::fmfBoundInt__option_t,
3213
    std::string option,
3214
    bool value)
3215
{
3216
11
  runBoolPredicates(options::fmfBoundInt, option, value, d_handler);
3217
11
  d_holder->fmfBoundInt = value;
3218
11
  d_holder->fmfBoundInt__setByUser__ = true;
3219
11
  Trace("options") << "user assigned option fmfBoundInt" << std::endl;
3220
3221
11
}
3222
3
template <> void Options::assignBool(
3223
    options::fmfBoundLazy__option_t,
3224
    std::string option,
3225
    bool value)
3226
{
3227
3
  runBoolPredicates(options::fmfBoundLazy, option, value, d_handler);
3228
3
  d_holder->fmfBoundLazy = value;
3229
3
  d_holder->fmfBoundLazy__setByUser__ = true;
3230
3
  Trace("options") << "user assigned option fmfBoundLazy" << std::endl;
3231
3232
3
}
3233
template <> void Options::assignBool(
3234
    options::fmfFmcSimple__option_t,
3235
    std::string option,
3236
    bool value)
3237
{
3238
  runBoolPredicates(options::fmfFmcSimple, option, value, d_handler);
3239
  d_holder->fmfFmcSimple = value;
3240
  d_holder->fmfFmcSimple__setByUser__ = true;
3241
  Trace("options") << "user assigned option fmfFmcSimple" << std::endl;
3242
3243
}
3244
template <> void Options::assignBool(
3245
    options::fmfFreshDistConst__option_t,
3246
    std::string option,
3247
    bool value)
3248
{
3249
  runBoolPredicates(options::fmfFreshDistConst, option, value, d_handler);
3250
  d_holder->fmfFreshDistConst = value;
3251
  d_holder->fmfFreshDistConst__setByUser__ = true;
3252
  Trace("options") << "user assigned option fmfFreshDistConst" << std::endl;
3253
3254
}
3255
40
template <> void Options::assignBool(
3256
    options::fmfFunWellDefined__option_t,
3257
    std::string option,
3258
    bool value)
3259
{
3260
40
  runBoolPredicates(options::fmfFunWellDefined, option, value, d_handler);
3261
40
  d_holder->fmfFunWellDefined = value;
3262
40
  d_holder->fmfFunWellDefined__setByUser__ = true;
3263
40
  Trace("options") << "user assigned option fmfFunWellDefined" << std::endl;
3264
3265
40
}
3266
10
template <> void Options::assignBool(
3267
    options::fmfFunWellDefinedRelevant__option_t,
3268
    std::string option,
3269
    bool value)
3270
{
3271
10
  runBoolPredicates(options::fmfFunWellDefinedRelevant, option, value, d_handler);
3272
10
  d_holder->fmfFunWellDefinedRelevant = value;
3273
10
  d_holder->fmfFunWellDefinedRelevant__setByUser__ = true;
3274
10
  Trace("options") << "user assigned option fmfFunWellDefinedRelevant" << std::endl;
3275
3276
10
}
3277
7
template <> void Options::assignBool(
3278
    options::fmfInstEngine__option_t,
3279
    std::string option,
3280
    bool value)
3281
{
3282
7
  runBoolPredicates(options::fmfInstEngine, option, value, d_handler);
3283
7
  d_holder->fmfInstEngine = value;
3284
7
  d_holder->fmfInstEngine__setByUser__ = true;
3285
7
  Trace("options") << "user assigned option fmfInstEngine" << std::endl;
3286
3287
7
}
3288
template <> options::fmfTypeCompletionThresh__option_t::type runHandlerAndPredicates(
3289
    options::fmfTypeCompletionThresh__option_t,
3290
    std::string option,
3291
    std::string optionarg,
3292
    options::OptionsHandler* handler)
3293
{
3294
  options::fmfTypeCompletionThresh__option_t::type retval = handleOption<int>(option, optionarg);
3295
3296
  return retval;
3297
}
3298
template <> void Options::assign(
3299
    options::fmfTypeCompletionThresh__option_t,
3300
    std::string option,
3301
    std::string value)
3302
{
3303
  d_holder->fmfTypeCompletionThresh =
3304
    runHandlerAndPredicates(options::fmfTypeCompletionThresh, option, value, d_handler);
3305
  d_holder->fmfTypeCompletionThresh__setByUser__ = true;
3306
  Trace("options") << "user assigned option fmfTypeCompletionThresh" << std::endl;
3307
3308
}
3309
template <> void Options::assignBool(
3310
    options::fullSaturateInterleave__option_t,
3311
    std::string option,
3312
    bool value)
3313
{
3314
  runBoolPredicates(options::fullSaturateInterleave, option, value, d_handler);
3315
  d_holder->fullSaturateInterleave = value;
3316
  d_holder->fullSaturateInterleave__setByUser__ = true;
3317
  Trace("options") << "user assigned option fullSaturateInterleave" << std::endl;
3318
3319
}
3320
3
template <> void Options::assignBool(
3321
    options::fullSaturateStratify__option_t,
3322
    std::string option,
3323
    bool value)
3324
{
3325
3
  runBoolPredicates(options::fullSaturateStratify, option, value, d_handler);
3326
3
  d_holder->fullSaturateStratify = value;
3327
3
  d_holder->fullSaturateStratify__setByUser__ = true;
3328
3
  Trace("options") << "user assigned option fullSaturateStratify" << std::endl;
3329
3330
3
}
3331
template <> void Options::assignBool(
3332
    options::fullSaturateSum__option_t,
3333
    std::string option,
3334
    bool value)
3335
{
3336
  runBoolPredicates(options::fullSaturateSum, option, value, d_handler);
3337
  d_holder->fullSaturateSum = value;
3338
  d_holder->fullSaturateSum__setByUser__ = true;
3339
  Trace("options") << "user assigned option fullSaturateSum" << std::endl;
3340
3341
}
3342
63
template <> void Options::assignBool(
3343
    options::fullSaturateQuant__option_t,
3344
    std::string option,
3345
    bool value)
3346
{
3347
63
  runBoolPredicates(options::fullSaturateQuant, option, value, d_handler);
3348
63
  d_holder->fullSaturateQuant = value;
3349
63
  d_holder->fullSaturateQuant__setByUser__ = true;
3350
63
  Trace("options") << "user assigned option fullSaturateQuant" << std::endl;
3351
3352
63
}
3353
3
template <> options::fullSaturateLimit__option_t::type runHandlerAndPredicates(
3354
    options::fullSaturateLimit__option_t,
3355
    std::string option,
3356
    std::string optionarg,
3357
    options::OptionsHandler* handler)
3358
{
3359
3
  options::fullSaturateLimit__option_t::type retval = handleOption<int>(option, optionarg);
3360
3361
3
  return retval;
3362
}
3363
3
template <> void Options::assign(
3364
    options::fullSaturateLimit__option_t,
3365
    std::string option,
3366
    std::string value)
3367
{
3368
6
  d_holder->fullSaturateLimit =
3369
9
    runHandlerAndPredicates(options::fullSaturateLimit, option, value, d_handler);
3370
3
  d_holder->fullSaturateLimit__setByUser__ = true;
3371
3
  Trace("options") << "user assigned option fullSaturateLimit" << std::endl;
3372
3373
3
}
3374
template <> void Options::assignBool(
3375
    options::fullSaturateQuantRd__option_t,
3376
    std::string option,
3377
    bool value)
3378
{
3379
  runBoolPredicates(options::fullSaturateQuantRd, option, value, d_handler);
3380
  d_holder->fullSaturateQuantRd = value;
3381
  d_holder->fullSaturateQuantRd__setByUser__ = true;
3382
  Trace("options") << "user assigned option fullSaturateQuantRd" << std::endl;
3383
3384
}
3385
5
template <> void Options::assignBool(
3386
    options::globalNegate__option_t,
3387
    std::string option,
3388
    bool value)
3389
{
3390
5
  runBoolPredicates(options::globalNegate, option, value, d_handler);
3391
5
  d_holder->globalNegate = value;
3392
5
  d_holder->globalNegate__setByUser__ = true;
3393
5
  Trace("options") << "user assigned option globalNegate" << std::endl;
3394
3395
5
}
3396
11
template <> void Options::assignBool(
3397
    options::hoElim__option_t,
3398
    std::string option,
3399
    bool value)
3400
{
3401
11
  runBoolPredicates(options::hoElim, option, value, d_handler);
3402
11
  d_holder->hoElim = value;
3403
11
  d_holder->hoElim__setByUser__ = true;
3404
11
  Trace("options") << "user assigned option hoElim" << std::endl;
3405
3406
11
}
3407
1
template <> void Options::assignBool(
3408
    options::hoElimStoreAx__option_t,
3409
    std::string option,
3410
    bool value)
3411
{
3412
1
  runBoolPredicates(options::hoElimStoreAx, option, value, d_handler);
3413
1
  d_holder->hoElimStoreAx = value;
3414
1
  d_holder->hoElimStoreAx__setByUser__ = true;
3415
1
  Trace("options") << "user assigned option hoElimStoreAx" << std::endl;
3416
3417
1
}
3418
template <> void Options::assignBool(
3419
    options::hoMatching__option_t,
3420
    std::string option,
3421
    bool value)
3422
{
3423
  runBoolPredicates(options::hoMatching, option, value, d_handler);
3424
  d_holder->hoMatching = value;
3425
  d_holder->hoMatching__setByUser__ = true;
3426
  Trace("options") << "user assigned option hoMatching" << std::endl;
3427
3428
}
3429
template <> void Options::assignBool(
3430
    options::hoMatchingVarArgPriority__option_t,
3431
    std::string option,
3432
    bool value)
3433
{
3434
  runBoolPredicates(options::hoMatchingVarArgPriority, option, value, d_handler);
3435
  d_holder->hoMatchingVarArgPriority = value;
3436
  d_holder->hoMatchingVarArgPriority__setByUser__ = true;
3437
  Trace("options") << "user assigned option hoMatchingVarArgPriority" << std::endl;
3438
3439
}
3440
template <> void Options::assignBool(
3441
    options::hoMergeTermDb__option_t,
3442
    std::string option,
3443
    bool value)
3444
{
3445
  runBoolPredicates(options::hoMergeTermDb, option, value, d_handler);
3446
  d_holder->hoMergeTermDb = value;
3447
  d_holder->hoMergeTermDb__setByUser__ = true;
3448
  Trace("options") << "user assigned option hoMergeTermDb" << std::endl;
3449
3450
}
3451
template <> void Options::assignBool(
3452
    options::incrementTriggers__option_t,
3453
    std::string option,
3454
    bool value)
3455
{
3456
  runBoolPredicates(options::incrementTriggers, option, value, d_handler);
3457
  d_holder->incrementTriggers = value;
3458
  d_holder->incrementTriggers__setByUser__ = true;
3459
  Trace("options") << "user assigned option incrementTriggers" << std::endl;
3460
3461
}
3462
template <> void Options::assignBool(
3463
    options::instLevelInputOnly__option_t,
3464
    std::string option,
3465
    bool value)
3466
{
3467
  runBoolPredicates(options::instLevelInputOnly, option, value, d_handler);
3468
  d_holder->instLevelInputOnly = value;
3469
  d_holder->instLevelInputOnly__setByUser__ = true;
3470
  Trace("options") << "user assigned option instLevelInputOnly" << std::endl;
3471
3472
}
3473
3
template <> options::instMaxLevel__option_t::type runHandlerAndPredicates(
3474
    options::instMaxLevel__option_t,
3475
    std::string option,
3476
    std::string optionarg,
3477
    options::OptionsHandler* handler)
3478
{
3479
3
  options::instMaxLevel__option_t::type retval = handleOption<int>(option, optionarg);
3480
3481
3
  return retval;
3482
}
3483
3
template <> void Options::assign(
3484
    options::instMaxLevel__option_t,
3485
    std::string option,
3486
    std::string value)
3487
{
3488
6
  d_holder->instMaxLevel =
3489
9
    runHandlerAndPredicates(options::instMaxLevel, option, value, d_handler);
3490
3
  d_holder->instMaxLevel__setByUser__ = true;
3491
3
  Trace("options") << "user assigned option instMaxLevel" << std::endl;
3492
3493
3
}
3494
template <> void Options::assignBool(
3495
    options::instNoEntail__option_t,
3496
    std::string option,
3497
    bool value)
3498
{
3499
  runBoolPredicates(options::instNoEntail, option, value, d_handler);
3500
  d_holder->instNoEntail = value;
3501
  d_holder->instNoEntail__setByUser__ = true;
3502
  Trace("options") << "user assigned option instNoEntail" << std::endl;
3503
3504
}
3505
template <> options::instWhenPhase__option_t::type runHandlerAndPredicates(
3506
    options::instWhenPhase__option_t,
3507
    std::string option,
3508
    std::string optionarg,
3509
    options::OptionsHandler* handler)
3510
{
3511
  options::instWhenPhase__option_t::type retval = handleOption<int>(option, optionarg);
3512
3513
  return retval;
3514
}
3515
template <> void Options::assign(
3516
    options::instWhenPhase__option_t,
3517
    std::string option,
3518
    std::string value)
3519
{
3520
  d_holder->instWhenPhase =
3521
    runHandlerAndPredicates(options::instWhenPhase, option, value, d_handler);
3522
  d_holder->instWhenPhase__setByUser__ = true;
3523
  Trace("options") << "user assigned option instWhenPhase" << std::endl;
3524
3525
}
3526
template <> void Options::assignBool(
3527
    options::instWhenStrictInterleave__option_t,
3528
    std::string option,
3529
    bool value)
3530
{
3531
  runBoolPredicates(options::instWhenStrictInterleave, option, value, d_handler);
3532
  d_holder->instWhenStrictInterleave = value;
3533
  d_holder->instWhenStrictInterleave__setByUser__ = true;
3534
  Trace("options") << "user assigned option instWhenStrictInterleave" << std::endl;
3535
3536
}
3537
template <> void Options::assignBool(
3538
    options::instWhenTcFirst__option_t,
3539
    std::string option,
3540
    bool value)
3541
{
3542
  runBoolPredicates(options::instWhenTcFirst, option, value, d_handler);
3543
  d_holder->instWhenTcFirst = value;
3544
  d_holder->instWhenTcFirst__setByUser__ = true;
3545
  Trace("options") << "user assigned option instWhenTcFirst" << std::endl;
3546
3547
}
3548
3
template <> options::instWhenMode__option_t::type runHandlerAndPredicates(
3549
    options::instWhenMode__option_t,
3550
    std::string option,
3551
    std::string optionarg,
3552
    options::OptionsHandler* handler)
3553
{
3554
3
  options::instWhenMode__option_t::type retval = stringToInstWhenMode(option, optionarg);
3555
3
  handler->checkInstWhenMode(option, retval);
3556
3
  return retval;
3557
}
3558
3
template <> void Options::assign(
3559
    options::instWhenMode__option_t,
3560
    std::string option,
3561
    std::string value)
3562
{
3563
6
  d_holder->instWhenMode =
3564
9
    runHandlerAndPredicates(options::instWhenMode, option, value, d_handler);
3565
3
  d_holder->instWhenMode__setByUser__ = true;
3566
3
  Trace("options") << "user assigned option instWhenMode" << std::endl;
3567
3568
3
}
3569
6
template <> void Options::assignBool(
3570
    options::intWfInduction__option_t,
3571
    std::string option,
3572
    bool value)
3573
{
3574
6
  runBoolPredicates(options::intWfInduction, option, value, d_handler);
3575
6
  d_holder->intWfInduction = value;
3576
6
  d_holder->intWfInduction__setByUser__ = true;
3577
6
  Trace("options") << "user assigned option intWfInduction" << std::endl;
3578
3579
6
}
3580
template <> void Options::assignBool(
3581
    options::iteDtTesterSplitQuant__option_t,
3582
    std::string option,
3583
    bool value)
3584
{
3585
  runBoolPredicates(options::iteDtTesterSplitQuant, option, value, d_handler);
3586
  d_holder->iteDtTesterSplitQuant = value;
3587
  d_holder->iteDtTesterSplitQuant__setByUser__ = true;
3588
  Trace("options") << "user assigned option iteDtTesterSplitQuant" << std::endl;
3589
3590
}
3591
template <> options::iteLiftQuant__option_t::type runHandlerAndPredicates(
3592
    options::iteLiftQuant__option_t,
3593
    std::string option,
3594
    std::string optionarg,
3595
    options::OptionsHandler* handler)
3596
{
3597
  options::iteLiftQuant__option_t::type retval = stringToIteLiftQuantMode(option, optionarg);
3598
3599
  return retval;
3600
}
3601
template <> void Options::assign(
3602
    options::iteLiftQuant__option_t,
3603
    std::string option,
3604
    std::string value)
3605
{
3606
  d_holder->iteLiftQuant =
3607
    runHandlerAndPredicates(options::iteLiftQuant, option, value, d_handler);
3608
  d_holder->iteLiftQuant__setByUser__ = true;
3609
  Trace("options") << "user assigned option iteLiftQuant" << std::endl;
3610
3611
}
3612
template <> options::literalMatchMode__option_t::type runHandlerAndPredicates(
3613
    options::literalMatchMode__option_t,
3614
    std::string option,
3615
    std::string optionarg,
3616
    options::OptionsHandler* handler)
3617
{
3618
  options::literalMatchMode__option_t::type retval = stringToLiteralMatchMode(option, optionarg);
3619
3620
  return retval;
3621
}
3622
template <> void Options::assign(
3623
    options::literalMatchMode__option_t,
3624
    std::string option,
3625
    std::string value)
3626
{
3627
  d_holder->literalMatchMode =
3628
    runHandlerAndPredicates(options::literalMatchMode, option, value, d_handler);
3629
  d_holder->literalMatchMode__setByUser__ = true;
3630
  Trace("options") << "user assigned option literalMatchMode" << std::endl;
3631
3632
}
3633
13
template <> void Options::assignBool(
3634
    options::macrosQuant__option_t,
3635
    std::string option,
3636
    bool value)
3637
{
3638
13
  runBoolPredicates(options::macrosQuant, option, value, d_handler);
3639
13
  d_holder->macrosQuant = value;
3640
13
  d_holder->macrosQuant__setByUser__ = true;
3641
13
  Trace("options") << "user assigned option macrosQuant" << std::endl;
3642
3643
13
}
3644
2
template <> options::macrosQuantMode__option_t::type runHandlerAndPredicates(
3645
    options::macrosQuantMode__option_t,
3646
    std::string option,
3647
    std::string optionarg,
3648
    options::OptionsHandler* handler)
3649
{
3650
2
  options::macrosQuantMode__option_t::type retval = stringToMacrosQuantMode(option, optionarg);
3651
3652
2
  return retval;
3653
}
3654
2
template <> void Options::assign(
3655
    options::macrosQuantMode__option_t,
3656
    std::string option,
3657
    std::string value)
3658
{
3659
4
  d_holder->macrosQuantMode =
3660
6
    runHandlerAndPredicates(options::macrosQuantMode, option, value, d_handler);
3661
2
  d_holder->macrosQuantMode__setByUser__ = true;
3662
2
  Trace("options") << "user assigned option macrosQuantMode" << std::endl;
3663
3664
2
}
3665
template <> void Options::assignBool(
3666
    options::mbqiInterleave__option_t,
3667
    std::string option,
3668
    bool value)
3669
{
3670
  runBoolPredicates(options::mbqiInterleave, option, value, d_handler);
3671
  d_holder->mbqiInterleave = value;
3672
  d_holder->mbqiInterleave__setByUser__ = true;
3673
  Trace("options") << "user assigned option mbqiInterleave" << std::endl;
3674
3675
}
3676
template <> void Options::assignBool(
3677
    options::fmfOneInstPerRound__option_t,
3678
    std::string option,
3679
    bool value)
3680
{
3681
  runBoolPredicates(options::fmfOneInstPerRound, option, value, d_handler);
3682
  d_holder->fmfOneInstPerRound = value;
3683
  d_holder->fmfOneInstPerRound__setByUser__ = true;
3684
  Trace("options") << "user assigned option fmfOneInstPerRound" << std::endl;
3685
3686
}
3687
template <> options::mbqiMode__option_t::type runHandlerAndPredicates(
3688
    options::mbqiMode__option_t,
3689
    std::string option,
3690
    std::string optionarg,
3691
    options::OptionsHandler* handler)
3692
{
3693
  options::mbqiMode__option_t::type retval = stringToMbqiMode(option, optionarg);
3694
3695
  return retval;
3696
}
3697
template <> void Options::assign(
3698
    options::mbqiMode__option_t,
3699
    std::string option,
3700
    std::string value)
3701
{
3702
  d_holder->mbqiMode =
3703
    runHandlerAndPredicates(options::mbqiMode, option, value, d_handler);
3704
  d_holder->mbqiMode__setByUser__ = true;
3705
  Trace("options") << "user assigned option mbqiMode" << std::endl;
3706
3707
}
3708
240
template <> void Options::assignBool(
3709
    options::miniscopeQuant__option_t,
3710
    std::string option,
3711
    bool value)
3712
{
3713
240
  runBoolPredicates(options::miniscopeQuant, option, value, d_handler);
3714
240
  d_holder->miniscopeQuant = value;
3715
240
  d_holder->miniscopeQuant__setByUser__ = true;
3716
240
  Trace("options") << "user assigned option miniscopeQuant" << std::endl;
3717
3718
240
}
3719
237
template <> void Options::assignBool(
3720
    options::miniscopeQuantFreeVar__option_t,
3721
    std::string option,
3722
    bool value)
3723
{
3724
237
  runBoolPredicates(options::miniscopeQuantFreeVar, option, value, d_handler);
3725
237
  d_holder->miniscopeQuantFreeVar = value;
3726
237
  d_holder->miniscopeQuantFreeVar__setByUser__ = true;
3727
237
  Trace("options") << "user assigned option miniscopeQuantFreeVar" << std::endl;
3728
3729
237
}
3730
3
template <> void Options::assignBool(
3731
    options::multiTriggerCache__option_t,
3732
    std::string option,
3733
    bool value)
3734
{
3735
3
  runBoolPredicates(options::multiTriggerCache, option, value, d_handler);
3736
3
  d_holder->multiTriggerCache = value;
3737
3
  d_holder->multiTriggerCache__setByUser__ = true;
3738
3
  Trace("options") << "user assigned option multiTriggerCache" << std::endl;
3739
3740
3
}
3741
template <> void Options::assignBool(
3742
    options::multiTriggerLinear__option_t,
3743
    std::string option,
3744
    bool value)
3745
{
3746
  runBoolPredicates(options::multiTriggerLinear, option, value, d_handler);
3747
  d_holder->multiTriggerLinear = value;
3748
  d_holder->multiTriggerLinear__setByUser__ = true;
3749
  Trace("options") << "user assigned option multiTriggerLinear" << std::endl;
3750
3751
}
3752
template <> void Options::assignBool(
3753
    options::multiTriggerPriority__option_t,
3754
    std::string option,
3755
    bool value)
3756
{
3757
  runBoolPredicates(options::multiTriggerPriority, option, value, d_handler);
3758
  d_holder->multiTriggerPriority = value;
3759
  d_holder->multiTriggerPriority__setByUser__ = true;
3760
  Trace("options") << "user assigned option multiTriggerPriority" << std::endl;
3761
3762
}
3763
template <> void Options::assignBool(
3764
    options::multiTriggerWhenSingle__option_t,
3765
    std::string option,
3766
    bool value)
3767
{
3768
  runBoolPredicates(options::multiTriggerWhenSingle, option, value, d_handler);
3769
  d_holder->multiTriggerWhenSingle = value;
3770
  d_holder->multiTriggerWhenSingle__setByUser__ = true;
3771
  Trace("options") << "user assigned option multiTriggerWhenSingle" << std::endl;
3772
3773
}
3774
3
template <> void Options::assignBool(
3775
    options::partialTriggers__option_t,
3776
    std::string option,
3777
    bool value)
3778
{
3779
3
  runBoolPredicates(options::partialTriggers, option, value, d_handler);
3780
3
  d_holder->partialTriggers = value;
3781
3
  d_holder->partialTriggers__setByUser__ = true;
3782
3
  Trace("options") << "user assigned option partialTriggers" << std::endl;
3783
3784
3
}
3785
2
template <> void Options::assignBool(
3786
    options::preSkolemQuant__option_t,
3787
    std::string option,
3788
    bool value)
3789
{
3790
2
  runBoolPredicates(options::preSkolemQuant, option, value, d_handler);
3791
2
  d_holder->preSkolemQuant = value;
3792
2
  d_holder->preSkolemQuant__setByUser__ = true;
3793
2
  Trace("options") << "user assigned option preSkolemQuant" << std::endl;
3794
3795
2
}
3796
template <> void Options::assignBool(
3797
    options::preSkolemQuantAgg__option_t,
3798
    std::string option,
3799
    bool value)
3800
{
3801
  runBoolPredicates(options::preSkolemQuantAgg, option, value, d_handler);
3802
  d_holder->preSkolemQuantAgg = value;
3803
  d_holder->preSkolemQuantAgg__setByUser__ = true;
3804
  Trace("options") << "user assigned option preSkolemQuantAgg" << std::endl;
3805
3806
}
3807
template <> void Options::assignBool(
3808
    options::preSkolemQuantNested__option_t,
3809
    std::string option,
3810
    bool value)
3811
{
3812
  runBoolPredicates(options::preSkolemQuantNested, option, value, d_handler);
3813
  d_holder->preSkolemQuantNested = value;
3814
  d_holder->preSkolemQuantNested__setByUser__ = true;
3815
  Trace("options") << "user assigned option preSkolemQuantNested" << std::endl;
3816
3817
}
3818
template <> void Options::assignBool(
3819
    options::prenexQuantUser__option_t,
3820
    std::string option,
3821
    bool value)
3822
{
3823
  runBoolPredicates(options::prenexQuantUser, option, value, d_handler);
3824
  d_holder->prenexQuantUser = value;
3825
  d_holder->prenexQuantUser__setByUser__ = true;
3826
  Trace("options") << "user assigned option prenexQuantUser" << std::endl;
3827
3828
}
3829
template <> options::prenexQuant__option_t::type runHandlerAndPredicates(
3830
    options::prenexQuant__option_t,
3831
    std::string option,
3832
    std::string optionarg,
3833
    options::OptionsHandler* handler)
3834
{
3835
  options::prenexQuant__option_t::type retval = stringToPrenexQuantMode(option, optionarg);
3836
3837
  return retval;
3838
}
3839
template <> void Options::assign(
3840
    options::prenexQuant__option_t,
3841
    std::string option,
3842
    std::string value)
3843
{
3844
  d_holder->prenexQuant =
3845
    runHandlerAndPredicates(options::prenexQuant, option, value, d_handler);
3846
  d_holder->prenexQuant__setByUser__ = true;
3847
  Trace("options") << "user assigned option prenexQuant" << std::endl;
3848
3849
}
3850
3
template <> void Options::assignBool(
3851
    options::purifyTriggers__option_t,
3852
    std::string option,
3853
    bool value)
3854
{
3855
3
  runBoolPredicates(options::purifyTriggers, option, value, d_handler);
3856
3
  d_holder->purifyTriggers = value;
3857
3
  d_holder->purifyTriggers__setByUser__ = true;
3858
3
  Trace("options") << "user assigned option purifyTriggers" << std::endl;
3859
3860
3
}
3861
template <> void Options::assignBool(
3862
    options::qcfAllConflict__option_t,
3863
    std::string option,
3864
    bool value)
3865
{
3866
  runBoolPredicates(options::qcfAllConflict, option, value, d_handler);
3867
  d_holder->qcfAllConflict = value;
3868
  d_holder->qcfAllConflict__setByUser__ = true;
3869
  Trace("options") << "user assigned option qcfAllConflict" << std::endl;
3870
3871
}
3872
template <> void Options::assignBool(
3873
    options::qcfEagerCheckRd__option_t,
3874
    std::string option,
3875
    bool value)
3876
{
3877
  runBoolPredicates(options::qcfEagerCheckRd, option, value, d_handler);
3878
  d_holder->qcfEagerCheckRd = value;
3879
  d_holder->qcfEagerCheckRd__setByUser__ = true;
3880
  Trace("options") << "user assigned option qcfEagerCheckRd" << std::endl;
3881
3882
}
3883
template <> void Options::assignBool(
3884
    options::qcfEagerTest__option_t,
3885
    std::string option,
3886
    bool value)
3887
{
3888
  runBoolPredicates(options::qcfEagerTest, option, value, d_handler);
3889
  d_holder->qcfEagerTest = value;
3890
  d_holder->qcfEagerTest__setByUser__ = true;
3891
  Trace("options") << "user assigned option qcfEagerTest" << std::endl;
3892
3893
}
3894
template <> void Options::assignBool(
3895
    options::qcfNestedConflict__option_t,
3896
    std::string option,
3897
    bool value)
3898
{
3899
  runBoolPredicates(options::qcfNestedConflict, option, value, d_handler);
3900
  d_holder->qcfNestedConflict = value;
3901
  d_holder->qcfNestedConflict__setByUser__ = true;
3902
  Trace("options") << "user assigned option qcfNestedConflict" << std::endl;
3903
3904
}
3905
template <> void Options::assignBool(
3906
    options::qcfSkipRd__option_t,
3907
    std::string option,
3908
    bool value)
3909
{
3910
  runBoolPredicates(options::qcfSkipRd, option, value, d_handler);
3911
  d_holder->qcfSkipRd = value;
3912
  d_holder->qcfSkipRd__setByUser__ = true;
3913
  Trace("options") << "user assigned option qcfSkipRd" << std::endl;
3914
3915
}
3916
6
template <> void Options::assignBool(
3917
    options::qcfTConstraint__option_t,
3918
    std::string option,
3919
    bool value)
3920
{
3921
6
  runBoolPredicates(options::qcfTConstraint, option, value, d_handler);
3922
6
  d_holder->qcfTConstraint = value;
3923
6
  d_holder->qcfTConstraint__setByUser__ = true;
3924
6
  Trace("options") << "user assigned option qcfTConstraint" << std::endl;
3925
3926
6
}
3927
template <> void Options::assignBool(
3928
    options::qcfVoExp__option_t,
3929
    std::string option,
3930
    bool value)
3931
{
3932
  runBoolPredicates(options::qcfVoExp, option, value, d_handler);
3933
  d_holder->qcfVoExp = value;
3934
  d_holder->qcfVoExp__setByUser__ = true;
3935
  Trace("options") << "user assigned option qcfVoExp" << std::endl;
3936
3937
}
3938
template <> void Options::assignBool(
3939
    options::quantAlphaEquiv__option_t,
3940
    std::string option,
3941
    bool value)
3942
{
3943
  runBoolPredicates(options::quantAlphaEquiv, option, value, d_handler);
3944
  d_holder->quantAlphaEquiv = value;
3945
  d_holder->quantAlphaEquiv__setByUser__ = true;
3946
  Trace("options") << "user assigned option quantAlphaEquiv" << std::endl;
3947
3948
}
3949
template <> void Options::assignBool(
3950
    options::quantConflictFind__option_t,
3951
    std::string option,
3952
    bool value)
3953
{
3954
  runBoolPredicates(options::quantConflictFind, option, value, d_handler);
3955
  d_holder->quantConflictFind = value;
3956
  d_holder->quantConflictFind__setByUser__ = true;
3957
  Trace("options") << "user assigned option quantConflictFind" << std::endl;
3958
3959
}
3960
template <> options::qcfMode__option_t::type runHandlerAndPredicates(
3961
    options::qcfMode__option_t,
3962
    std::string option,
3963
    std::string optionarg,
3964
    options::OptionsHandler* handler)
3965
{
3966
  options::qcfMode__option_t::type retval = stringToQcfMode(option, optionarg);
3967
3968
  return retval;
3969
}
3970
template <> void Options::assign(
3971
    options::qcfMode__option_t,
3972
    std::string option,
3973
    std::string value)
3974
{
3975
  d_holder->qcfMode =
3976
    runHandlerAndPredicates(options::qcfMode, option, value, d_handler);
3977
  d_holder->qcfMode__setByUser__ = true;
3978
  Trace("options") << "user assigned option qcfMode" << std::endl;
3979
3980
}
3981
template <> options::qcfWhenMode__option_t::type runHandlerAndPredicates(
3982
    options::qcfWhenMode__option_t,
3983
    std::string option,
3984
    std::string optionarg,
3985
    options::OptionsHandler* handler)
3986
{
3987
  options::qcfWhenMode__option_t::type retval = stringToQcfWhenMode(option, optionarg);
3988
3989
  return retval;
3990
}
3991
template <> void Options::assign(
3992
    options::qcfWhenMode__option_t,
3993
    std::string option,
3994
    std::string value)
3995
{
3996
  d_holder->qcfWhenMode =
3997
    runHandlerAndPredicates(options::qcfWhenMode, option, value, d_handler);
3998
  d_holder->qcfWhenMode__setByUser__ = true;
3999
  Trace("options") << "user assigned option qcfWhenMode" << std::endl;
4000
4001
}
4002
template <> options::quantDynamicSplit__option_t::type runHandlerAndPredicates(
4003
    options::quantDynamicSplit__option_t,
4004
    std::string option,
4005
    std::string optionarg,
4006
    options::OptionsHandler* handler)
4007
{
4008
  options::quantDynamicSplit__option_t::type retval = stringToQuantDSplitMode(option, optionarg);
4009
4010
  return retval;
4011
}
4012
template <> void Options::assign(
4013
    options::quantDynamicSplit__option_t,
4014
    std::string option,
4015
    std::string value)
4016
{
4017
  d_holder->quantDynamicSplit =
4018
    runHandlerAndPredicates(options::quantDynamicSplit, option, value, d_handler);
4019
  d_holder->quantDynamicSplit__setByUser__ = true;
4020
  Trace("options") << "user assigned option quantDynamicSplit" << std::endl;
4021
4022
}
4023
template <> void Options::assignBool(
4024
    options::quantFunWellDefined__option_t,
4025
    std::string option,
4026
    bool value)
4027
{
4028
  runBoolPredicates(options::quantFunWellDefined, option, value, d_handler);
4029
  d_holder->quantFunWellDefined = value;
4030
  d_holder->quantFunWellDefined__setByUser__ = true;
4031
  Trace("options") << "user assigned option quantFunWellDefined" << std::endl;
4032
4033
}
4034
7
template <> void Options::assignBool(
4035
    options::quantInduction__option_t,
4036
    std::string option,
4037
    bool value)
4038
{
4039
7
  runBoolPredicates(options::quantInduction, option, value, d_handler);
4040
7
  d_holder->quantInduction = value;
4041
7
  d_holder->quantInduction__setByUser__ = true;
4042
7
  Trace("options") << "user assigned option quantInduction" << std::endl;
4043
4044
7
}
4045
template <> options::quantRepMode__option_t::type runHandlerAndPredicates(
4046
    options::quantRepMode__option_t,
4047
    std::string option,
4048
    std::string optionarg,
4049
    options::OptionsHandler* handler)
4050
{
4051
  options::quantRepMode__option_t::type retval = stringToQuantRepMode(option, optionarg);
4052
4053
  return retval;
4054
}
4055
template <> void Options::assign(
4056
    options::quantRepMode__option_t,
4057
    std::string option,
4058
    std::string value)
4059
{
4060
  d_holder->quantRepMode =
4061
    runHandlerAndPredicates(options::quantRepMode, option, value, d_handler);
4062
  d_holder->quantRepMode__setByUser__ = true;
4063
  Trace("options") << "user assigned option quantRepMode" << std::endl;
4064
4065
}
4066
237
template <> void Options::assignBool(
4067
    options::quantSplit__option_t,
4068
    std::string option,
4069
    bool value)
4070
{
4071
237
  runBoolPredicates(options::quantSplit, option, value, d_handler);
4072
237
  d_holder->quantSplit = value;
4073
237
  d_holder->quantSplit__setByUser__ = true;
4074
237
  Trace("options") << "user assigned option quantSplit" << std::endl;
4075
4076
237
}
4077
template <> void Options::assignBool(
4078
    options::registerQuantBodyTerms__option_t,
4079
    std::string option,
4080
    bool value)
4081
{
4082
  runBoolPredicates(options::registerQuantBodyTerms, option, value, d_handler);
4083
  d_holder->registerQuantBodyTerms = value;
4084
  d_holder->registerQuantBodyTerms__setByUser__ = true;
4085
  Trace("options") << "user assigned option registerQuantBodyTerms" << std::endl;
4086
4087
}
4088
15
template <> void Options::assignBool(
4089
    options::relationalTriggers__option_t,
4090
    std::string option,
4091
    bool value)
4092
{
4093
15
  runBoolPredicates(options::relationalTriggers, option, value, d_handler);
4094
15
  d_holder->relationalTriggers = value;
4095
15
  d_holder->relationalTriggers__setByUser__ = true;
4096
15
  Trace("options") << "user assigned option relationalTriggers" << std::endl;
4097
4098
15
}
4099
3
template <> void Options::assignBool(
4100
    options::relevantTriggers__option_t,
4101
    std::string option,
4102
    bool value)
4103
{
4104
3
  runBoolPredicates(options::relevantTriggers, option, value, d_handler);
4105
3
  d_holder->relevantTriggers = value;
4106
3
  d_holder->relevantTriggers__setByUser__ = true;
4107
3
  Trace("options") << "user assigned option relevantTriggers" << std::endl;
4108
4109
3
}
4110
template <> void Options::assignBool(
4111
    options::strictTriggers__option_t,
4112
    std::string option,
4113
    bool value)
4114
{
4115
  runBoolPredicates(options::strictTriggers, option, value, d_handler);
4116
  d_holder->strictTriggers = value;
4117
  d_holder->strictTriggers__setByUser__ = true;
4118
  Trace("options") << "user assigned option strictTriggers" << std::endl;
4119
4120
}
4121
template <> void Options::assignBool(
4122
    options::sygus__option_t,
4123
    std::string option,
4124
    bool value)
4125
{
4126
  runBoolPredicates(options::sygus, option, value, d_handler);
4127
  d_holder->sygus = value;
4128
  d_holder->sygus__setByUser__ = true;
4129
  Trace("options") << "user assigned option sygus" << std::endl;
4130
4131
}
4132
template <> options::sygusActiveGenEnumConsts__option_t::type runHandlerAndPredicates(
4133
    options::sygusActiveGenEnumConsts__option_t,
4134
    std::string option,
4135
    std::string optionarg,
4136
    options::OptionsHandler* handler)
4137
{
4138
  options::sygusActiveGenEnumConsts__option_t::type retval = handleOption<unsigned long>(option, optionarg);
4139
4140
  return retval;
4141
}
4142
template <> void Options::assign(
4143
    options::sygusActiveGenEnumConsts__option_t,
4144
    std::string option,
4145
    std::string value)
4146
{
4147
  d_holder->sygusActiveGenEnumConsts =
4148
    runHandlerAndPredicates(options::sygusActiveGenEnumConsts, option, value, d_handler);
4149
  d_holder->sygusActiveGenEnumConsts__setByUser__ = true;
4150
  Trace("options") << "user assigned option sygusActiveGenEnumConsts" << std::endl;
4151
4152
}
4153
20
template <> options::sygusActiveGenMode__option_t::type runHandlerAndPredicates(
4154
    options::sygusActiveGenMode__option_t,
4155
    std::string option,
4156
    std::string optionarg,
4157
    options::OptionsHandler* handler)
4158
{
4159
20
  options::sygusActiveGenMode__option_t::type retval = stringToSygusActiveGenMode(option, optionarg);
4160
4161
20
  return retval;
4162
}
4163
20
template <> void Options::assign(
4164
    options::sygusActiveGenMode__option_t,
4165
    std::string option,
4166
    std::string value)
4167
{
4168
40
  d_holder->sygusActiveGenMode =
4169
60
    runHandlerAndPredicates(options::sygusActiveGenMode, option, value, d_handler);
4170
20
  d_holder->sygusActiveGenMode__setByUser__ = true;
4171
20
  Trace("options") << "user assigned option sygusActiveGenMode" << std::endl;
4172
4173
20
}
4174
4
template <> void Options::assignBool(
4175
    options::sygusAddConstGrammar__option_t,
4176
    std::string option,
4177
    bool value)
4178
{
4179
4
  runBoolPredicates(options::sygusAddConstGrammar, option, value, d_handler);
4180
4
  d_holder->sygusAddConstGrammar = value;
4181
4
  d_holder->sygusAddConstGrammar__setByUser__ = true;
4182
4
  Trace("options") << "user assigned option sygusAddConstGrammar" << std::endl;
4183
4184
4
}
4185
6
template <> void Options::assignBool(
4186
    options::sygusArgRelevant__option_t,
4187
    std::string option,
4188
    bool value)
4189
{
4190
6
  runBoolPredicates(options::sygusArgRelevant, option, value, d_handler);
4191
6
  d_holder->sygusArgRelevant = value;
4192
6
  d_holder->sygusArgRelevant__setByUser__ = true;
4193
6
  Trace("options") << "user assigned option sygusArgRelevant" << std::endl;
4194
4195
6
}
4196
template <> void Options::assignBool(
4197
    options::sygusInvAutoUnfold__option_t,
4198
    std::string option,
4199
    bool value)
4200
{
4201
  runBoolPredicates(options::sygusInvAutoUnfold, option, value, d_handler);
4202
  d_holder->sygusInvAutoUnfold = value;
4203
  d_holder->sygusInvAutoUnfold__setByUser__ = true;
4204
  Trace("options") << "user assigned option sygusInvAutoUnfold" << std::endl;
4205
4206
}
4207
2
template <> void Options::assignBool(
4208
    options::sygusBoolIteReturnConst__option_t,
4209
    std::string option,
4210
    bool value)
4211
{
4212
2
  runBoolPredicates(options::sygusBoolIteReturnConst, option, value, d_handler);
4213
2
  d_holder->sygusBoolIteReturnConst = value;
4214
2
  d_holder->sygusBoolIteReturnConst__setByUser__ = true;
4215
2
  Trace("options") << "user assigned option sygusBoolIteReturnConst" << std::endl;
4216
4217
2
}
4218
10
template <> void Options::assignBool(
4219
    options::sygusCoreConnective__option_t,
4220
    std::string option,
4221
    bool value)
4222
{
4223
10
  runBoolPredicates(options::sygusCoreConnective, option, value, d_handler);
4224
10
  d_holder->sygusCoreConnective = value;
4225
10
  d_holder->sygusCoreConnective__setByUser__ = true;
4226
10
  Trace("options") << "user assigned option sygusCoreConnective" << std::endl;
4227
4228
10
}
4229
template <> void Options::assignBool(
4230
    options::sygusConstRepairAbort__option_t,
4231
    std::string option,
4232
    bool value)
4233
{
4234
  runBoolPredicates(options::sygusConstRepairAbort, option, value, d_handler);
4235
  d_holder->sygusConstRepairAbort = value;
4236
  d_holder->sygusConstRepairAbort__setByUser__ = true;
4237
  Trace("options") << "user assigned option sygusConstRepairAbort" << std::endl;
4238
4239
}
4240
template <> void Options::assignBool(
4241
    options::sygusEvalOpt__option_t,
4242
    std::string option,
4243
    bool value)
4244
{
4245
  runBoolPredicates(options::sygusEvalOpt, option, value, d_handler);
4246
  d_holder->sygusEvalOpt = value;
4247
  d_holder->sygusEvalOpt__setByUser__ = true;
4248
  Trace("options") << "user assigned option sygusEvalOpt" << std::endl;
4249
4250
}
4251
template <> void Options::assignBool(
4252
    options::sygusEvalUnfold__option_t,
4253
    std::string option,
4254
    bool value)
4255
{
4256
  runBoolPredicates(options::sygusEvalUnfold, option, value, d_handler);
4257
  d_holder->sygusEvalUnfold = value;
4258
  d_holder->sygusEvalUnfold__setByUser__ = true;
4259
  Trace("options") << "user assigned option sygusEvalUnfold" << std::endl;
4260
4261
}
4262
template <> void Options::assignBool(
4263
    options::sygusEvalUnfoldBool__option_t,
4264
    std::string option,
4265
    bool value)
4266
{
4267
  runBoolPredicates(options::sygusEvalUnfoldBool, option, value, d_handler);
4268
  d_holder->sygusEvalUnfoldBool = value;
4269
  d_holder->sygusEvalUnfoldBool__setByUser__ = true;
4270
  Trace("options") << "user assigned option sygusEvalUnfoldBool" << std::endl;
4271
4272
}
4273
template <> options::sygusExprMinerCheckTimeout__option_t::type runHandlerAndPredicates(
4274
    options::sygusExprMinerCheckTimeout__option_t,
4275
    std::string option,
4276
    std::string optionarg,
4277
    options::OptionsHandler* handler)
4278
{
4279
  options::sygusExprMinerCheckTimeout__option_t::type retval = handleOption<unsigned long>(option, optionarg);
4280
4281
  return retval;
4282
}
4283
template <> void Options::assign(
4284
    options::sygusExprMinerCheckTimeout__option_t,
4285
    std::string option,
4286
    std::string value)
4287
{
4288
  d_holder->sygusExprMinerCheckTimeout =
4289
    runHandlerAndPredicates(options::sygusExprMinerCheckTimeout, option, value, d_handler);
4290
  d_holder->sygusExprMinerCheckTimeout__setByUser__ = true;
4291
  Trace("options") << "user assigned option sygusExprMinerCheckTimeout" << std::endl;
4292
4293
}
4294
2
template <> void Options::assignBool(
4295
    options::sygusExtRew__option_t,
4296
    std::string option,
4297
    bool value)
4298
{
4299
2
  runBoolPredicates(options::sygusExtRew, option, value, d_handler);
4300
2
  d_holder->sygusExtRew = value;
4301
2
  d_holder->sygusExtRew__setByUser__ = true;
4302
2
  Trace("options") << "user assigned option sygusExtRew" << std::endl;
4303
4304
2
}
4305
template <> void Options::assignBool(
4306
    options::sygusFilterSolRevSubsume__option_t,
4307
    std::string option,
4308
    bool value)
4309
{
4310
  runBoolPredicates(options::sygusFilterSolRevSubsume, option, value, d_handler);
4311
  d_holder->sygusFilterSolRevSubsume = value;
4312
  d_holder->sygusFilterSolRevSubsume__setByUser__ = true;
4313
  Trace("options") << "user assigned option sygusFilterSolRevSubsume" << std::endl;
4314
4315
}
4316
template <> options::sygusFilterSolMode__option_t::type runHandlerAndPredicates(
4317
    options::sygusFilterSolMode__option_t,
4318
    std::string option,
4319
    std::string optionarg,
4320
    options::OptionsHandler* handler)
4321
{
4322
  options::sygusFilterSolMode__option_t::type retval = stringToSygusFilterSolMode(option, optionarg);
4323
4324
  return retval;
4325
}
4326
template <> void Options::assign(
4327
    options::sygusFilterSolMode__option_t,
4328
    std::string option,
4329
    std::string value)
4330
{
4331
  d_holder->sygusFilterSolMode =
4332
    runHandlerAndPredicates(options::sygusFilterSolMode, option, value, d_handler);
4333
  d_holder->sygusFilterSolMode__setByUser__ = true;
4334
  Trace("options") << "user assigned option sygusFilterSolMode" << std::endl;
4335
4336
}
4337
12
template <> options::sygusGrammarConsMode__option_t::type runHandlerAndPredicates(
4338
    options::sygusGrammarConsMode__option_t,
4339
    std::string option,
4340
    std::string optionarg,
4341
    options::OptionsHandler* handler)
4342
{
4343
12
  options::sygusGrammarConsMode__option_t::type retval = stringToSygusGrammarConsMode(option, optionarg);
4344
4345
12
  return retval;
4346
}
4347
12
template <> void Options::assign(
4348
    options::sygusGrammarConsMode__option_t,
4349
    std::string option,
4350
    std::string value)
4351
{
4352
24
  d_holder->sygusGrammarConsMode =
4353
36
    runHandlerAndPredicates(options::sygusGrammarConsMode, option, value, d_handler);
4354
12
  d_holder->sygusGrammarConsMode__setByUser__ = true;
4355
12
  Trace("options") << "user assigned option sygusGrammarConsMode" << std::endl;
4356
4357
12
}
4358
template <> void Options::assignBool(
4359
    options::sygusGrammarNorm__option_t,
4360
    std::string option,
4361
    bool value)
4362
{
4363
  runBoolPredicates(options::sygusGrammarNorm, option, value, d_handler);
4364
  d_holder->sygusGrammarNorm = value;
4365
  d_holder->sygusGrammarNorm__setByUser__ = true;
4366
  Trace("options") << "user assigned option sygusGrammarNorm" << std::endl;
4367
4368
}
4369
64
template <> void Options::assignBool(
4370
    options::sygusInference__option_t,
4371
    std::string option,
4372
    bool value)
4373
{
4374
64
  runBoolPredicates(options::sygusInference, option, value, d_handler);
4375
64
  d_holder->sygusInference = value;
4376
64
  d_holder->sygusInference__setByUser__ = true;
4377
64
  Trace("options") << "user assigned option sygusInference" << std::endl;
4378
4379
64
}
4380
17
template <> void Options::assignBool(
4381
    options::sygusInst__option_t,
4382
    std::string option,
4383
    bool value)
4384
{
4385
17
  runBoolPredicates(options::sygusInst, option, value, d_handler);
4386
17
  d_holder->sygusInst = value;
4387
17
  d_holder->sygusInst__setByUser__ = true;
4388
17
  Trace("options") << "user assigned option sygusInst" << std::endl;
4389
4390
17
}
4391
template <> options::sygusInstMode__option_t::type runHandlerAndPredicates(
4392
    options::sygusInstMode__option_t,
4393
    std::string option,
4394
    std::string optionarg,
4395
    options::OptionsHandler* handler)
4396
{
4397
  options::sygusInstMode__option_t::type retval = stringToSygusInstMode(option, optionarg);
4398
4399
  return retval;
4400
}
4401
template <> void Options::assign(
4402
    options::sygusInstMode__option_t,
4403
    std::string option,
4404
    std::string value)
4405
{
4406
  d_holder->sygusInstMode =
4407
    runHandlerAndPredicates(options::sygusInstMode, option, value, d_handler);
4408
  d_holder->sygusInstMode__setByUser__ = true;
4409
  Trace("options") << "user assigned option sygusInstMode" << std::endl;
4410
4411
}
4412
template <> options::sygusInstScope__option_t::type runHandlerAndPredicates(
4413
    options::sygusInstScope__option_t,
4414
    std::string option,
4415
    std::string optionarg,
4416
    options::OptionsHandler* handler)
4417
{
4418
  options::sygusInstScope__option_t::type retval = stringToSygusInstScope(option, optionarg);
4419
4420
  return retval;
4421
}
4422
template <> void Options::assign(
4423
    options::sygusInstScope__option_t,
4424
    std::string option,
4425
    std::string value)
4426
{
4427
  d_holder->sygusInstScope =
4428
    runHandlerAndPredicates(options::sygusInstScope, option, value, d_handler);
4429
  d_holder->sygusInstScope__setByUser__ = true;
4430
  Trace("options") << "user assigned option sygusInstScope" << std::endl;
4431
4432
}
4433
template <> options::sygusInstTermSel__option_t::type runHandlerAndPredicates(
4434
    options::sygusInstTermSel__option_t,
4435
    std::string option,
4436
    std::string optionarg,
4437
    options::OptionsHandler* handler)
4438
{
4439
  options::sygusInstTermSel__option_t::type retval = stringToSygusInstTermSelMode(option, optionarg);
4440
4441
  return retval;
4442
}
4443
template <> void Options::assign(
4444
    options::sygusInstTermSel__option_t,
4445
    std::string option,
4446
    std::string value)
4447
{
4448
  d_holder->sygusInstTermSel =
4449
    runHandlerAndPredicates(options::sygusInstTermSel, option, value, d_handler);
4450
  d_holder->sygusInstTermSel__setByUser__ = true;
4451
  Trace("options") << "user assigned option sygusInstTermSel" << std::endl;
4452
4453
}
4454
template <> void Options::assignBool(
4455
    options::sygusInvTemplWhenSyntax__option_t,
4456
    std::string option,
4457
    bool value)
4458
{
4459
  runBoolPredicates(options::sygusInvTemplWhenSyntax, option, value, d_handler);
4460
  d_holder->sygusInvTemplWhenSyntax = value;
4461
  d_holder->sygusInvTemplWhenSyntax__setByUser__ = true;
4462
  Trace("options") << "user assigned option sygusInvTemplWhenSyntax" << std::endl;
4463
4464
}
4465
6
template <> options::sygusInvTemplMode__option_t::type runHandlerAndPredicates(
4466
    options::sygusInvTemplMode__option_t,
4467
    std::string option,
4468
    std::string optionarg,
4469
    options::OptionsHandler* handler)
4470
{
4471
6
  options::sygusInvTemplMode__option_t::type retval = stringToSygusInvTemplMode(option, optionarg);
4472
4473
6
  return retval;
4474
}
4475
6
template <> void Options::assign(
4476
    options::sygusInvTemplMode__option_t,
4477
    std::string option,
4478
    std::string value)
4479
{
4480
12
  d_holder->sygusInvTemplMode =
4481
18
    runHandlerAndPredicates(options::sygusInvTemplMode, option, value, d_handler);
<