GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/logic_info.cpp Lines: 390 431 90.5 %
Date: 2021-03-23 Branches: 412 712 57.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file logic_info.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 A class giving information about a logic (group a theory modules
13
 ** and configuration information)
14
 **
15
 ** A class giving information about a logic (group of theory modules and
16
 ** configuration information).
17
 **/
18
#include "theory/logic_info.h"
19
20
#include <cstring>
21
#include <iostream>
22
#include <sstream>
23
#include <string>
24
25
#include "base/check.h"
26
#include "base/configuration.h"
27
#include "expr/kind.h"
28
29
using namespace std;
30
using namespace CVC4::theory;
31
32
namespace CVC4 {
33
34
49487
LogicInfo::LogicInfo()
35
    : d_logicString(""),
36
      d_theories(THEORY_LAST, false),
37
      d_sharingTheories(0),
38
      d_integers(true),
39
      d_reals(true),
40
      d_transcendentals(true),
41
      d_linear(false),
42
      d_differenceLogic(false),
43
      d_cardinalityConstraints(false),
44
      d_higherOrder(true),
45
49487
      d_locked(false)
46
{
47
692818
  for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
48
  {
49
643331
    if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU())
50
    {
51
      continue;
52
    }
53
643331
    enableTheory(id);
54
  }
55
49487
}
56
57
10157
LogicInfo::LogicInfo(std::string logicString)
58
    : d_logicString(""),
59
      d_theories(THEORY_LAST, false),
60
      d_sharingTheories(0),
61
      d_integers(false),
62
      d_reals(false),
63
      d_transcendentals(false),
64
      d_linear(false),
65
      d_differenceLogic(false),
66
      d_cardinalityConstraints(false),
67
      d_higherOrder(false),
68
10159
      d_locked(false)
69
{
70
10159
  setLogicString(logicString);
71
10155
  lock();
72
10155
}
73
74
11447
LogicInfo::LogicInfo(const char* logicString)
75
    : d_logicString(""),
76
      d_theories(THEORY_LAST, false),
77
      d_sharingTheories(0),
78
      d_integers(false),
79
      d_reals(false),
80
      d_transcendentals(false),
81
      d_linear(false),
82
      d_differenceLogic(false),
83
      d_cardinalityConstraints(false),
84
      d_higherOrder(false),
85
11447
      d_locked(false)
86
{
87
11447
  setLogicString(logicString);
88
11447
  lock();
89
11447
}
90
91
/** Is sharing enabled for this logic? */
92
69503792
bool LogicInfo::isSharingEnabled() const {
93
69503792
  PrettyCheckArgument(d_locked, *this,
94
                      "This LogicInfo isn't locked yet, and cannot be queried");
95
69503792
  return d_sharingTheories > 1;
96
}
97
98
99
/** Is the given theory module active in this logic? */
100
81268413
bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const {
101
81268413
  PrettyCheckArgument(d_locked, *this,
102
                      "This LogicInfo isn't locked yet, and cannot be queried");
103
81268397
  return d_theories[theory];
104
}
105
106
/** Is this a quantified logic? */
107
199996
bool LogicInfo::isQuantified() const {
108
199996
  PrettyCheckArgument(d_locked, *this,
109
                      "This LogicInfo isn't locked yet, and cannot be queried");
110
199994
  return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
111
}
112
113
/** Is this a higher-order logic? */
114
2535
bool LogicInfo::isHigherOrder() const
115
{
116
2535
  PrettyCheckArgument(d_locked,
117
                      *this,
118
                      "This LogicInfo isn't locked yet, and cannot be queried");
119
2535
  return d_higherOrder;
120
}
121
122
/** Is this the all-inclusive logic? */
123
19413
bool LogicInfo::hasEverything() const {
124
19413
  PrettyCheckArgument(d_locked, *this,
125
                      "This LogicInfo isn't locked yet, and cannot be queried");
126
38826
  LogicInfo everything;
127
19413
  everything.lock();
128
38826
  return *this == everything;
129
}
130
131
/** Is this the all-exclusive logic?  (Here, that means propositional logic) */
132
52
bool LogicInfo::hasNothing() const {
133
52
  PrettyCheckArgument(d_locked, *this,
134
                      "This LogicInfo isn't locked yet, and cannot be queried");
135
104
  LogicInfo nothing("");
136
52
  nothing.lock();
137
104
  return *this == nothing;
138
}
139
140
86009
bool LogicInfo::isPure(theory::TheoryId theory) const {
141
86009
  PrettyCheckArgument(d_locked, *this,
142
                      "This LogicInfo isn't locked yet, and cannot be queried");
143
  // the third and fourth conjucts are really just to rule out the misleading
144
  // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
145
161533
  return isTheoryEnabled(theory) && !isSharingEnabled() &&
146
109610
      ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
147
94281
      ( isTrueTheory(theory) || d_sharingTheories == 0 );
148
}
149
150
14485
bool LogicInfo::areIntegersUsed() const {
151
14485
  PrettyCheckArgument(d_locked, *this,
152
                      "This LogicInfo isn't locked yet, and cannot be queried");
153
14483
  PrettyCheckArgument(
154
      isTheoryEnabled(theory::THEORY_ARITH), *this,
155
      "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
156
14479
  return d_integers;
157
}
158
159
8118
bool LogicInfo::areRealsUsed() const {
160
8118
  PrettyCheckArgument(d_locked, *this,
161
                      "This LogicInfo isn't locked yet, and cannot be queried");
162
8116
  PrettyCheckArgument(
163
      isTheoryEnabled(theory::THEORY_ARITH), *this,
164
      "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
165
8112
  return d_reals;
166
}
167
168
12110
bool LogicInfo::areTranscendentalsUsed() const
169
{
170
12110
  PrettyCheckArgument(d_locked,
171
                      *this,
172
                      "This LogicInfo isn't locked yet, and cannot be queried");
173
12110
  PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH),
174
                      *this,
175
                      "Arithmetic not used in this LogicInfo; cannot ask "
176
                      "whether transcendentals are used");
177
12106
  return d_transcendentals;
178
}
179
180
172296
bool LogicInfo::isLinear() const {
181
172296
  PrettyCheckArgument(d_locked, *this,
182
                      "This LogicInfo isn't locked yet, and cannot be queried");
183
172294
  PrettyCheckArgument(
184
      isTheoryEnabled(theory::THEORY_ARITH), *this,
185
      "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
186
172290
  return d_linear || d_differenceLogic;
187
}
188
189
6828
bool LogicInfo::isDifferenceLogic() const {
190
6828
  PrettyCheckArgument(d_locked, *this,
191
                      "This LogicInfo isn't locked yet, and cannot be queried");
192
6828
  PrettyCheckArgument(
193
      isTheoryEnabled(theory::THEORY_ARITH), *this,
194
      "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
195
6824
  return d_differenceLogic;
196
}
197
198
11616
bool LogicInfo::hasCardinalityConstraints() const {
199
11616
  PrettyCheckArgument(d_locked, *this,
200
                      "This LogicInfo isn't locked yet, and cannot be queried");
201
11616
  return d_cardinalityConstraints;
202
}
203
204
205
35603
bool LogicInfo::operator==(const LogicInfo& other) const {
206
35603
  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
207
                      "This LogicInfo isn't locked yet, and cannot be queried");
208
263721
  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
209
254583
    if(d_theories[id] != other.d_theories[id]) {
210
26465
      return false;
211
    }
212
  }
213
214
9138
  PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
215
                      "LogicInfo internal inconsistency");
216
18276
  bool res = d_cardinalityConstraints == other.d_cardinalityConstraints
217
9138
             && d_higherOrder == other.d_higherOrder;
218
9138
  if(isTheoryEnabled(theory::THEORY_ARITH)) {
219
17523
    return d_integers == other.d_integers && d_reals == other.d_reals
220
8411
           && d_transcendentals == other.d_transcendentals
221
8249
           && d_linear == other.d_linear
222
17043
           && d_differenceLogic == other.d_differenceLogic && res;
223
  } else {
224
122
    return res;
225
  }
226
}
227
228
7044
bool LogicInfo::operator<=(const LogicInfo& other) const {
229
7044
  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
230
                      "This LogicInfo isn't locked yet, and cannot be queried");
231
63594
  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
232
60672
    if(d_theories[id] && !other.d_theories[id]) {
233
4122
      return false;
234
    }
235
  }
236
2922
  PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
237
                      "LogicInfo internal inconsistency");
238
5868
  bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints)
239
5820
             && (!d_higherOrder || other.d_higherOrder);
240
2922
  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
241
4128
    return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
242
1722
           && (!d_transcendentals || other.d_transcendentals)
243
1704
           && (d_linear || !other.d_linear)
244
4038
           && (d_differenceLogic || !other.d_differenceLogic) && res;
245
  } else {
246
288
    return res;
247
  }
248
}
249
250
6510
bool LogicInfo::operator>=(const LogicInfo& other) const {
251
6510
  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
252
                      "This LogicInfo isn't locked yet, and cannot be queried");
253
59092
  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
254
56338
    if(!d_theories[id] && other.d_theories[id]) {
255
3756
      return false;
256
    }
257
  }
258
2754
  PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
259
                      "LogicInfo internal inconsistency");
260
8232
  bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints)
261
5490
             && (d_higherOrder || !other.d_higherOrder);
262
2754
  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
263
3186
    return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
264
1594
           && (d_transcendentals || !other.d_transcendentals)
265
1582
           && (!d_linear || other.d_linear)
266
3800
           && (!d_differenceLogic || other.d_differenceLogic) && res;
267
    } else {
268
264
      return res;
269
  }
270
}
271
272
9889
std::string LogicInfo::getLogicString() const {
273
9889
  PrettyCheckArgument(
274
      d_locked, *this,
275
      "This LogicInfo isn't locked yet, and cannot be queried");
276
9887
  if(d_logicString == "") {
277
5776
    LogicInfo qf_all_supported;
278
2888
    qf_all_supported.disableQuantifiers();
279
2888
    qf_all_supported.lock();
280
2888
    if(hasEverything()) {
281
1511
      d_logicString = "ALL";
282
1377
    } else if(*this == qf_all_supported) {
283
      d_logicString = "QF_ALL";
284
    } else {
285
1377
      size_t seen = 0; // make sure we support all the active theories
286
287
2754
      stringstream ss;
288
1377
      if(!isQuantified()) {
289
96
        ss << "QF_";
290
      }
291
1377
      if (d_theories[THEORY_SEP])
292
      {
293
7
        ss << "SEP_";
294
7
        ++seen;
295
      }
296
1377
      if(d_theories[THEORY_ARRAYS]) {
297
47
        ss << (d_sharingTheories == 1 ? "AX" : "A");
298
47
        ++seen;
299
      }
300
1377
      if(d_theories[THEORY_UF]) {
301
1125
        ss << "UF";
302
1125
        ++seen;
303
      }
304
1377
      if( d_cardinalityConstraints ){
305
        ss << "C";
306
      }
307
1377
      if(d_theories[THEORY_BV]) {
308
357
        ss << "BV";
309
357
        ++seen;
310
      }
311
1377
      if(d_theories[THEORY_FP]) {
312
9
        ss << "FP";
313
9
        ++seen;
314
      }
315
1377
      if(d_theories[THEORY_DATATYPES]) {
316
1099
        ss << "DT";
317
1099
        ++seen;
318
      }
319
1377
      if(d_theories[THEORY_STRINGS]) {
320
220
        ss << "S";
321
220
        ++seen;
322
      }
323
1377
      if(d_theories[THEORY_ARITH]) {
324
1297
        if(isDifferenceLogic()) {
325
          ss << (areIntegersUsed() ? "I" : "");
326
          ss << (areRealsUsed() ? "R" : "");
327
          ss << "DL";
328
        } else {
329
1297
          ss << (isLinear() ? "L" : "N");
330
1297
          ss << (areIntegersUsed() ? "I" : "");
331
1297
          ss << (areRealsUsed() ? "R" : "");
332
1297
          ss << "A";
333
1297
          ss << (areTranscendentalsUsed() ? "T" : "");
334
        }
335
1297
        ++seen;
336
      }
337
1377
      if(d_theories[THEORY_SETS]) {
338
1
        ss << "FS";
339
1
        ++seen;
340
      }
341
1377
      if (d_theories[THEORY_BAGS])
342
      {
343
1
        ss << "FB";
344
1
        ++seen;
345
      }
346
1377
      if(seen != d_sharingTheories) {
347
        Unhandled()
348
            << "can't extract a logic string from LogicInfo; at least one "
349
               "active theory is unknown to LogicInfo::getLogicString() !";
350
      }
351
352
1377
      if(seen == 0) {
353
        ss << "SAT";
354
      }
355
356
1377
      d_logicString = ss.str();
357
    }
358
  }
359
9887
  return d_logicString;
360
}
361
362
21604
void LogicInfo::setLogicString(std::string logicString)
363
{
364
21604
  PrettyCheckArgument(!d_locked, *this,
365
                      "This LogicInfo is locked, and cannot be modified");
366
302456
  for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
367
280852
    d_theories[id] = false;// ensure it's cleared
368
  }
369
21604
  d_sharingTheories = 0;
370
371
  // Below, ONLY use enableTheory()/disableTheory() rather than
372
  // accessing d_theories[] directly.  This makes sure to set up
373
  // sharing properly.
374
375
21604
  enableTheory(THEORY_BUILTIN);
376
21604
  enableTheory(THEORY_BOOL);
377
378
21604
  const char* p = logicString.c_str();
379
21604
  if(*p == '\0') {
380
    // propositional logic only; we're done.
381
21550
  } else if(!strcmp(p, "QF_SAT")) {
382
    // propositional logic only; we're done.
383
18
    p += 6;
384
21532
  } else if(!strcmp(p, "SAT")) {
385
    // quantified Boolean formulas only; we're done.
386
12
    enableQuantifiers();
387
12
    p += 3;
388
21520
  } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
389
    // the "all theories included" logic, no quantifiers
390
287
    enableEverything();
391
287
    disableQuantifiers();
392
287
    arithNonLinear();
393
287
    p += 16;
394
21233
  } else if(!strcmp(p, "QF_ALL")) {
395
    // the "all theories included" logic, no quantifiers
396
68
    enableEverything();
397
68
    disableQuantifiers();
398
68
    arithNonLinear();
399
68
    p += 6;
400
21165
  } else if(!strcmp(p, "ALL_SUPPORTED")) {
401
    // the "all theories included" logic, with quantifiers
402
896
    enableEverything();
403
896
    enableQuantifiers();
404
896
    arithNonLinear();
405
896
    p += 13;
406
20269
  } else if(!strcmp(p, "ALL")) {
407
    // the "all theories included" logic, with quantifiers
408
1644
    enableEverything();
409
1644
    enableQuantifiers();
410
1644
    arithNonLinear();
411
1644
    p += 3;
412
  }
413
18625
  else if (!strcmp(p, "HORN"))
414
  {
415
    // the HORN logic
416
    enableEverything();
417
    enableQuantifiers();
418
    arithNonLinear();
419
    p += 4;
420
  } else {
421
18625
    if(!strncmp(p, "QF_", 3)) {
422
15791
      disableQuantifiers();
423
15791
      p += 3;
424
    } else {
425
2834
      enableQuantifiers();
426
    }
427
18625
    if (!strncmp(p, "SEP_", 4))
428
    {
429
8
      enableSeparationLogic();
430
8
      p += 4;
431
    }
432
18625
    if(!strncmp(p, "AX", 2)) {
433
50
      enableTheory(THEORY_ARRAYS);
434
50
      p += 2;
435
    } else {
436
18575
      if(*p == 'A') {
437
1888
        enableTheory(THEORY_ARRAYS);
438
1888
        ++p;
439
      }
440
18575
      if(!strncmp(p, "UF", 2)) {
441
12879
        enableTheory(THEORY_UF);
442
12879
        p += 2;
443
      }
444
18575
      if(!strncmp(p, "C", 1 )) {
445
54
        d_cardinalityConstraints = true;
446
54
        p += 1;
447
      }
448
      // allow BV or DT in either order
449
18575
      if(!strncmp(p, "BV", 2)) {
450
2597
        enableTheory(THEORY_BV);
451
2597
        p += 2;
452
      }
453
18575
      if(!strncmp(p, "FP", 2)) {
454
76
        enableTheory(THEORY_FP);
455
76
        p += 2;
456
      }
457
18575
      if(!strncmp(p, "DT", 2)) {
458
124
        enableTheory(THEORY_DATATYPES);
459
124
        p += 2;
460
      }
461
18575
      if(!d_theories[THEORY_BV] && !strncmp(p, "BV", 2)) {
462
        enableTheory(THEORY_BV);
463
        p += 2;
464
      }
465
18575
      if(*p == 'S') {
466
796
        enableTheory(THEORY_STRINGS);
467
796
        ++p;
468
      }
469
18575
      if(!strncmp(p, "IDL", 3)) {
470
227
        enableIntegers();
471
227
        disableReals();
472
227
        arithOnlyDifference();
473
227
        p += 3;
474
18348
      } else if(!strncmp(p, "RDL", 3)) {
475
118
        disableIntegers();
476
118
        enableReals();
477
118
        arithOnlyDifference();
478
118
        p += 3;
479
18230
      } else if(!strncmp(p, "IRDL", 4)) {
480
        // "IRDL" ?! --not very useful, but getLogicString() can produce
481
        // that string, so we really had better be able to read it back in.
482
        enableIntegers();
483
        enableReals();
484
        arithOnlyDifference();
485
        p += 4;
486
18230
      } else if(!strncmp(p, "LIA", 3)) {
487
2768
        enableIntegers();
488
2768
        disableReals();
489
2768
        arithOnlyLinear();
490
2768
        p += 3;
491
15462
      } else if(!strncmp(p, "LRA", 3)) {
492
924
        disableIntegers();
493
924
        enableReals();
494
924
        arithOnlyLinear();
495
924
        p += 3;
496
14538
      } else if(!strncmp(p, "LIRA", 4)) {
497
404
        enableIntegers();
498
404
        enableReals();
499
404
        arithOnlyLinear();
500
404
        p += 4;
501
14134
      } else if(!strncmp(p, "NIA", 3)) {
502
678
        enableIntegers();
503
678
        disableReals();
504
678
        arithNonLinear();
505
678
        p += 3;
506
13456
      } else if(!strncmp(p, "NRA", 3)) {
507
9641
        disableIntegers();
508
9641
        enableReals();
509
9641
        arithNonLinear();
510
9641
        p += 3;
511
9641
        if (*p == 'T')
512
        {
513
200
          arithTranscendentals();
514
200
          p += 1;
515
        }
516
3815
      } else if(!strncmp(p, "NIRA", 4)) {
517
280
        enableIntegers();
518
280
        enableReals();
519
280
        arithNonLinear();
520
280
        p += 4;
521
280
        if (*p == 'T')
522
        {
523
6
          arithTranscendentals();
524
6
          p += 1;
525
        }
526
      }
527
18575
      if(!strncmp(p, "FS", 2)) {
528
154
        enableTheory(THEORY_SETS);
529
154
        p += 2;
530
      }
531
    }
532
  }
533
534
21604
  if (d_theories[THEORY_FP])
535
  {
536
    // THEORY_BV is needed for bit-blasting.
537
    // We have to set this here rather than in expandDefinition as it
538
    // is possible to create variables without any theory specific
539
    // operations, so expandDefinition won't be called.
540
2971
    enableTheory(THEORY_BV);
541
  }
542
543
21604
  if(*p != '\0') {
544
4
    stringstream err;
545
2
    err << "LogicInfo::setLogicString(): ";
546
2
    if(p == logicString) {
547
      err << "cannot parse logic string: " << logicString;
548
    } else {
549
2
      err << "junk (\"" << p << "\") at end of logic string: " << logicString;
550
    }
551
2
    IllegalArgument(logicString, err.str().c_str());
552
  }
553
554
  // ensure a getLogic() returns the same thing as was set
555
21602
  d_logicString = logicString;
556
21602
}
557
558
2897
void LogicInfo::enableEverything() {
559
2897
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
560
2897
  *this = LogicInfo();
561
2897
}
562
563
2
void LogicInfo::disableEverything() {
564
2
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
565
2
  *this = LogicInfo("");
566
2
}
567
568
735991
void LogicInfo::enableTheory(theory::TheoryId theory) {
569
735991
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
570
735991
  if(!d_theories[theory]) {
571
725051
    if(isTrueTheory(theory)) {
572
530313
      ++d_sharingTheories;
573
    }
574
725051
    d_logicString = "";
575
725051
    d_theories[theory] = true;
576
  }
577
735991
}
578
579
29790
void LogicInfo::disableTheory(theory::TheoryId theory) {
580
29790
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
581
29780
  if(d_theories[theory]) {
582
3300
    if(isTrueTheory(theory)) {
583
55
      Assert(d_sharingTheories > 0);
584
55
      --d_sharingTheories;
585
    }
586
3300
    if(theory == THEORY_BUILTIN ||
587
       theory == THEORY_BOOL) {
588
      return;
589
    }
590
3300
    d_logicString = "";
591
3300
    d_theories[theory] = false;
592
  }
593
}
594
595
1351
void LogicInfo::enableSygus()
596
{
597
1351
  enableQuantifiers();
598
1351
  enableTheory(THEORY_UF);
599
1351
  enableTheory(THEORY_DATATYPES);
600
1351
  enableIntegers();
601
1351
  enableHigherOrder();
602
1351
}
603
604
8
void LogicInfo::enableSeparationLogic()
605
{
606
8
  enableTheory(THEORY_SEP);
607
8
  enableTheory(THEORY_UF);
608
8
  enableTheory(THEORY_SETS);
609
8
}
610
611
5838
void LogicInfo::enableIntegers() {
612
5838
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
613
5836
  d_logicString = "";
614
5836
  enableTheory(THEORY_ARITH);
615
5836
  d_integers = true;
616
5836
}
617
618
10687
void LogicInfo::disableIntegers() {
619
10687
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
620
10685
  d_logicString = "";
621
10685
  d_integers = false;
622
10685
  if(!d_reals) {
623
10683
    disableTheory(THEORY_ARITH);
624
  }
625
10685
}
626
627
11367
void LogicInfo::enableReals() {
628
11367
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
629
11367
  d_logicString = "";
630
11367
  enableTheory(THEORY_ARITH);
631
11367
  d_reals = true;
632
11367
}
633
634
3677
void LogicInfo::disableReals() {
635
3677
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
636
3675
  d_logicString = "";
637
3675
  d_reals = false;
638
3675
  if(!d_integers) {
639
    disableTheory(THEORY_ARITH);
640
  }
641
3675
}
642
643
206
void LogicInfo::arithTranscendentals()
644
{
645
206
  PrettyCheckArgument(
646
      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
647
206
  d_logicString = "";
648
206
  d_transcendentals = true;
649
206
  if (!d_reals)
650
  {
651
    enableReals();
652
  }
653
206
  if (d_linear)
654
  {
655
    arithNonLinear();
656
  }
657
206
}
658
659
345
void LogicInfo::arithOnlyDifference() {
660
345
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
661
345
  d_logicString = "";
662
345
  d_linear = true;
663
345
  d_differenceLogic = true;
664
345
  d_transcendentals = false;
665
345
}
666
667
4226
void LogicInfo::arithOnlyLinear() {
668
4226
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
669
4224
  d_logicString = "";
670
4224
  d_linear = true;
671
4224
  d_differenceLogic = false;
672
4224
  d_transcendentals = false;
673
4224
}
674
675
13615
void LogicInfo::arithNonLinear() {
676
13615
  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
677
13615
  d_logicString = "";
678
13615
  d_linear = false;
679
13615
  d_differenceLogic = false;
680
13615
}
681
682
void LogicInfo::enableCardinalityConstraints()
683
{
684
  PrettyCheckArgument(
685
      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
686
  d_logicString = "";
687
  d_cardinalityConstraints = true;
688
}
689
690
void LogicInfo::disableCardinalityConstraints()
691
{
692
  PrettyCheckArgument(
693
      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
694
  d_logicString = "";
695
  d_cardinalityConstraints = false;
696
}
697
698
1353
void LogicInfo::enableHigherOrder()
699
{
700
1353
  PrettyCheckArgument(
701
      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
702
1353
  d_logicString = "";
703
1353
  d_higherOrder = true;
704
1353
}
705
706
void LogicInfo::disableHigherOrder()
707
{
708
  PrettyCheckArgument(
709
      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
710
  d_logicString = "";
711
  d_higherOrder = false;
712
}
713
714
6387
LogicInfo LogicInfo::getUnlockedCopy() const {
715
6387
  if(d_locked) {
716
12774
    LogicInfo info = *this;
717
6387
    info.d_locked = false;
718
6387
    return info;
719
  } else {
720
    return *this;
721
  }
722
}
723
724
2352
std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) {
725
2352
  return out << logic.getLogicString();
726
}
727
728
26685
}/* CVC4 namespace */