GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/api/cvc4cpp.h Lines: 13 18 72.2 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cvc4cpp.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
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 The CVC4 C++ API.
13
 **
14
 ** The CVC4 C++ API.
15
 **/
16
17
#include "cvc4_export.h"
18
19
#ifndef CVC4__API__CVC4CPP_H
20
#define CVC4__API__CVC4CPP_H
21
22
#include "api/cvc4cppkind.h"
23
24
#include <map>
25
#include <memory>
26
#include <set>
27
#include <sstream>
28
#include <string>
29
#include <unordered_map>
30
#include <unordered_set>
31
#include <vector>
32
33
namespace CVC4 {
34
35
template <bool ref_count>
36
class NodeTemplate;
37
typedef NodeTemplate<true> Node;
38
39
class AssertCommand;
40
class BlockModelValuesCommand;
41
class CheckSatCommand;
42
class CheckSatAssumingCommand;
43
class DatatypeDeclarationCommand;
44
class DeclareFunctionCommand;
45
class DeclareHeapCommand;
46
class DeclareSortCommand;
47
class DeclareSygusVarCommand;
48
class DefineFunctionCommand;
49
class DefineFunctionRecCommand;
50
class DefineSortCommand;
51
class DType;
52
class DTypeConstructor;
53
class DTypeSelector;
54
class GetAbductCommand;
55
class GetInterpolCommand;
56
class GetModelCommand;
57
class GetQuantifierEliminationCommand;
58
class GetUnsatCoreCommand;
59
class GetValueCommand;
60
class NodeManager;
61
class SetUserAttributeCommand;
62
class SimplifyCommand;
63
class SmtEngine;
64
class SygusConstraintCommand;
65
class SygusInvConstraintCommand;
66
class SynthFunCommand;
67
class TypeNode;
68
class Options;
69
class QueryCommand;
70
class Random;
71
class Result;
72
73
namespace api {
74
75
class Solver;
76
struct Statistics;
77
78
/* -------------------------------------------------------------------------- */
79
/* Exception                                                                  */
80
/* -------------------------------------------------------------------------- */
81
82
1318
class CVC4_EXPORT CVC4ApiException : public std::exception
83
{
84
 public:
85
1318
  CVC4ApiException(const std::string& str) : d_msg(str) {}
86
  CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {}
87
  std::string getMessage() const { return d_msg; }
88
59
  const char* what() const noexcept override { return d_msg.c_str(); }
89
90
 private:
91
  std::string d_msg;
92
};
93
94
53
class CVC4_EXPORT CVC4ApiRecoverableException : public CVC4ApiException
95
{
96
 public:
97
53
  CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {}
98
  CVC4ApiRecoverableException(const std::stringstream& stream)
99
      : CVC4ApiException(stream.str())
100
  {
101
  }
102
};
103
104
/* -------------------------------------------------------------------------- */
105
/* Result                                                                     */
106
/* -------------------------------------------------------------------------- */
107
108
/**
109
 * Encapsulation of a three-valued solver result, with explanations.
110
 */
111
371943
class CVC4_EXPORT Result
112
{
113
  friend class Solver;
114
115
 public:
116
  enum UnknownExplanation
117
  {
118
    REQUIRES_FULL_CHECK,
119
    INCOMPLETE,
120
    TIMEOUT,
121
    RESOURCEOUT,
122
    MEMOUT,
123
    INTERRUPTED,
124
    NO_STATUS,
125
    UNSUPPORTED,
126
    OTHER,
127
    UNKNOWN_REASON
128
  };
129
130
  /** Constructor. */
131
  Result();
132
133
  /**
134
   * Return true if Result is empty, i.e., a nullary Result, and not an actual
135
   * result returned from a checkSat() (and friends) query.
136
   */
137
  bool isNull() const;
138
139
  /**
140
   * Return true if query was a satisfiable checkSat() or checkSatAssuming()
141
   * query.
142
   */
143
  bool isSat() const;
144
145
  /**
146
   * Return true if query was an unsatisfiable checkSat() or
147
   * checkSatAssuming() query.
148
   */
149
  bool isUnsat() const;
150
151
  /**
152
   * Return true if query was a checkSat() or checkSatAssuming() query and
153
   * CVC4 was not able to determine (un)satisfiability.
154
   */
155
  bool isSatUnknown() const;
156
157
  /**
158
   * Return true if corresponding query was an entailed checkEntailed() query.
159
   */
160
  bool isEntailed() const;
161
162
  /**
163
   * Return true if corresponding query was a checkEntailed() query that is
164
   * not entailed.
165
   */
166
  bool isNotEntailed() const;
167
168
  /**
169
   * Return true if query was a checkEntailed() () query and CVC4 was not able
170
   * to determine if it is entailed.
171
   */
172
  bool isEntailmentUnknown() const;
173
174
  /**
175
   * Operator overloading for equality of two results.
176
   * @param r the result to compare to for equality
177
   * @return true if the results are equal
178
   */
179
  bool operator==(const Result& r) const;
180
181
  /**
182
   * Operator overloading for disequality of two results.
183
   * @param r the result to compare to for disequality
184
   * @return true if the results are disequal
185
   */
186
  bool operator!=(const Result& r) const;
187
188
  /**
189
   * @return an explanation for an unknown query result.
190
   */
191
  UnknownExplanation getUnknownExplanation() const;
192
193
  /**
194
   * @return a string representation of this result.
195
   */
196
  std::string toString() const;
197
198
 private:
199
  /**
200
   * Constructor.
201
   * @param r the internal result that is to be wrapped by this result
202
   * @return the Result
203
   */
204
  Result(const CVC4::Result& r);
205
206
  /**
207
   * The interal result wrapped by this result.
208
   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is
209
   *       not ref counted.
210
   */
211
  std::shared_ptr<CVC4::Result> d_result;
212
};
213
214
/**
215
 * Serialize a Result to given stream.
216
 * @param out the output stream
217
 * @param r the result to be serialized to the given output stream
218
 * @return the output stream
219
 */
220
std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT;
221
222
/**
223
 * Serialize an UnknownExplanation to given stream.
224
 * @param out the output stream
225
 * @param r the explanation to be serialized to the given output stream
226
 * @return the output stream
227
 */
228
std::ostream& operator<<(std::ostream& out,
229
                         enum Result::UnknownExplanation e) CVC4_EXPORT;
230
231
/* -------------------------------------------------------------------------- */
232
/* Sort                                                                       */
233
/* -------------------------------------------------------------------------- */
234
235
class Datatype;
236
237
/**
238
 * The sort of a CVC4 term.
239
 */
240
8633446
class CVC4_EXPORT Sort
241
{
242
  friend class CVC4::DatatypeDeclarationCommand;
243
  friend class CVC4::DeclareFunctionCommand;
244
  friend class CVC4::DeclareHeapCommand;
245
  friend class CVC4::DeclareSortCommand;
246
  friend class CVC4::DeclareSygusVarCommand;
247
  friend class CVC4::DefineSortCommand;
248
  friend class CVC4::GetAbductCommand;
249
  friend class CVC4::GetInterpolCommand;
250
  friend class CVC4::GetModelCommand;
251
  friend class CVC4::SynthFunCommand;
252
  friend class DatatypeConstructor;
253
  friend class DatatypeConstructorDecl;
254
  friend class DatatypeSelector;
255
  friend class DatatypeDecl;
256
  friend class Op;
257
  friend class Solver;
258
  friend class Grammar;
259
  friend struct SortHashFunction;
260
  friend class Term;
261
262
 public:
263
  /**
264
   * Constructor.
265
   */
266
  Sort();
267
268
  /**
269
   * Destructor.
270
   */
271
  ~Sort();
272
273
  /**
274
   * Comparison for structural equality.
275
   * @param s the sort to compare to
276
   * @return true if the sorts are equal
277
   */
278
  bool operator==(const Sort& s) const;
279
280
  /**
281
   * Comparison for structural disequality.
282
   * @param s the sort to compare to
283
   * @return true if the sorts are not equal
284
   */
285
  bool operator!=(const Sort& s) const;
286
287
  /**
288
   * Comparison for ordering on sorts.
289
   * @param s the sort to compare to
290
   * @return true if this sort is less than s
291
   */
292
  bool operator<(const Sort& s) const;
293
294
  /**
295
   * Comparison for ordering on sorts.
296
   * @param s the sort to compare to
297
   * @return true if this sort is greater than s
298
   */
299
  bool operator>(const Sort& s) const;
300
301
  /**
302
   * Comparison for ordering on sorts.
303
   * @param s the sort to compare to
304
   * @return true if this sort is less than or equal to s
305
   */
306
  bool operator<=(const Sort& s) const;
307
308
  /**
309
   * Comparison for ordering on sorts.
310
   * @param s the sort to compare to
311
   * @return true if this sort is greater than or equal to s
312
   */
313
  bool operator>=(const Sort& s) const;
314
315
  /**
316
   * @return true if this Sort is a null sort.
317
   */
318
  bool isNull() const;
319
320
  /**
321
   * Is this a Boolean sort?
322
   * @return true if the sort is a Boolean sort
323
   */
324
  bool isBoolean() const;
325
326
  /**
327
   * Is this a integer sort?
328
   * @return true if the sort is a integer sort
329
   */
330
  bool isInteger() const;
331
332
  /**
333
   * Is this a real sort?
334
   * @return true if the sort is a real sort
335
   */
336
  bool isReal() const;
337
338
  /**
339
   * Is this a string sort?
340
   * @return true if the sort is the string sort
341
   */
342
  bool isString() const;
343
344
  /**
345
   * Is this a regexp sort?
346
   * @return true if the sort is the regexp sort
347
   */
348
  bool isRegExp() const;
349
350
  /**
351
   * Is this a rounding mode sort?
352
   * @return true if the sort is the rounding mode sort
353
   */
354
  bool isRoundingMode() const;
355
356
  /**
357
   * Is this a bit-vector sort?
358
   * @return true if the sort is a bit-vector sort
359
   */
360
  bool isBitVector() const;
361
362
  /**
363
   * Is this a floating-point sort?
364
   * @return true if the sort is a floating-point sort
365
   */
366
  bool isFloatingPoint() const;
367
368
  /**
369
   * Is this a datatype sort?
370
   * @return true if the sort is a datatype sort
371
   */
372
  bool isDatatype() const;
373
374
  /**
375
   * Is this a parametric datatype sort?
376
   * @return true if the sort is a parametric datatype sort
377
   */
378
  bool isParametricDatatype() const;
379
380
  /**
381
   * Is this a constructor sort?
382
   * @return true if the sort is a constructor sort
383
   */
384
  bool isConstructor() const;
385
386
  /**
387
   * Is this a selector sort?
388
   * @return true if the sort is a selector sort
389
   */
390
  bool isSelector() const;
391
392
  /**
393
   * Is this a tester sort?
394
   * @return true if the sort is a tester sort
395
   */
396
  bool isTester() const;
397
  /**
398
   * Is this a function sort?
399
   * @return true if the sort is a function sort
400
   */
401
  bool isFunction() const;
402
403
  /**
404
   * Is this a predicate sort?
405
   * That is, is this a function sort mapping to Boolean? All predicate
406
   * sorts are also function sorts.
407
   * @return true if the sort is a predicate sort
408
   */
409
  bool isPredicate() const;
410
411
  /**
412
   * Is this a tuple sort?
413
   * @return true if the sort is a tuple sort
414
   */
415
  bool isTuple() const;
416
417
  /**
418
   * Is this a record sort?
419
   * @return true if the sort is a record sort
420
   */
421
  bool isRecord() const;
422
423
  /**
424
   * Is this an array sort?
425
   * @return true if the sort is a array sort
426
   */
427
  bool isArray() const;
428
429
  /**
430
   * Is this a Set sort?
431
   * @return true if the sort is a Set sort
432
   */
433
  bool isSet() const;
434
435
  /**
436
   * Is this a Bag sort?
437
   * @return true if the sort is a Bag sort
438
   */
439
  bool isBag() const;
440
441
  /**
442
   * Is this a Sequence sort?
443
   * @return true if the sort is a Sequence sort
444
   */
445
  bool isSequence() const;
446
447
  /**
448
   * Is this a sort kind?
449
   * @return true if this is a sort kind
450
   */
451
  bool isUninterpretedSort() const;
452
453
  /**
454
   * Is this a sort constructor kind?
455
   * @return true if this is a sort constructor kind
456
   */
457
  bool isSortConstructor() const;
458
459
  /**
460
   * Is this a first-class sort?
461
   * First-class sorts are sorts for which:
462
   * (1) we handle equalities between terms of that type, and
463
   * (2) they are allowed to be parameters of parametric sorts (e.g. index or
464
   *     element sorts of arrays).
465
   *
466
   * Examples of sorts that are not first-class include sort constructor sorts
467
   * and regular expression sorts.
468
   *
469
   * @return true if this is a first-class sort
470
   */
471
  bool isFirstClass() const;
472
473
  /**
474
   * Is this a function-LIKE sort?
475
   *
476
   * Anything function-like except arrays (e.g., datatype selectors) is
477
   * considered a function here. Function-like terms can not be the argument
478
   * or return value for any term that is function-like.
479
   * This is mainly to avoid higher order.
480
   *
481
   * Note that arrays are explicitly not considered function-like here.
482
   *
483
   * @return true if this is a function-like sort
484
   */
485
  bool isFunctionLike() const;
486
487
  /**
488
   * Is this sort a subsort of the given sort?
489
   * @return true if this sort is a subsort of s
490
   */
491
  bool isSubsortOf(const Sort& s) const;
492
493
  /**
494
   * Is this sort comparable to the given sort (i.e., do they share
495
   * a common ancestor in the subsort tree)?
496
   * @return true if this sort is comparable to s
497
   */
498
  bool isComparableTo(const Sort& s) const;
499
500
  /**
501
   * @return the underlying datatype of a datatype sort
502
   */
503
  Datatype getDatatype() const;
504
505
  /**
506
   * Instantiate a parameterized datatype/sort sort.
507
   * Create sorts parameter with Solver::mkParamSort().
508
   * @param params the list of sort parameters to instantiate with
509
   */
510
  Sort instantiate(const std::vector<Sort>& params) const;
511
512
  /**
513
   * Substitution of Sorts.
514
   * @param sort the subsort to be substituted within this sort.
515
   * @param replacement the sort replacing the substituted subsort.
516
   */
517
  Sort substitute(const Sort& sort, const Sort& replacement) const;
518
519
  /**
520
   * Simultaneous substitution of Sorts.
521
   * @param sorts the subsorts to be substituted within this sort.
522
   * @param replacements the sort replacing the substituted subsorts.
523
   */
524
  Sort substitute(const std::vector<Sort>& sorts,
525
                  const std::vector<Sort>& replacements) const;
526
527
  /**
528
   * Output a string representation of this sort to a given stream.
529
   * @param out the output stream
530
   */
531
  void toStream(std::ostream& out) const;
532
533
  /**
534
   * @return a string representation of this sort
535
   */
536
  std::string toString() const;
537
538
  /* Constructor sort ------------------------------------------------------- */
539
540
  /**
541
   * @return the arity of a constructor sort
542
   */
543
  size_t getConstructorArity() const;
544
545
  /**
546
   * @return the domain sorts of a constructor sort
547
   */
548
  std::vector<Sort> getConstructorDomainSorts() const;
549
550
  /**
551
   * @return the codomain sort of a constructor sort
552
   */
553
  Sort getConstructorCodomainSort() const;
554
555
  /* Selector sort ------------------------------------------------------- */
556
557
  /**
558
   * @return the domain sort of a selector sort
559
   */
560
  Sort getSelectorDomainSort() const;
561
562
  /**
563
   * @return the codomain sort of a selector sort
564
   */
565
  Sort getSelectorCodomainSort() const;
566
567
  /* Tester sort ------------------------------------------------------- */
568
569
  /**
570
   * @return the domain sort of a tester sort
571
   */
572
  Sort getTesterDomainSort() const;
573
574
  /**
575
   * @return the codomain sort of a tester sort, which is the Boolean sort
576
   */
577
  Sort getTesterCodomainSort() const;
578
579
  /* Function sort ------------------------------------------------------- */
580
581
  /**
582
   * @return the arity of a function sort
583
   */
584
  size_t getFunctionArity() const;
585
586
  /**
587
   * @return the domain sorts of a function sort
588
   */
589
  std::vector<Sort> getFunctionDomainSorts() const;
590
591
  /**
592
   * @return the codomain sort of a function sort
593
   */
594
  Sort getFunctionCodomainSort() const;
595
596
  /* Array sort ---------------------------------------------------------- */
597
598
  /**
599
   * @return the array index sort of an array sort
600
   */
601
  Sort getArrayIndexSort() const;
602
603
  /**
604
   * @return the array element sort of an array element sort
605
   */
606
  Sort getArrayElementSort() const;
607
608
  /* Set sort ------------------------------------------------------------ */
609
610
  /**
611
   * @return the element sort of a set sort
612
   */
613
  Sort getSetElementSort() const;
614
615
  /* Bag sort ------------------------------------------------------------ */
616
617
  /**
618
   * @return the element sort of a bag sort
619
   */
620
  Sort getBagElementSort() const;
621
622
  /* Sequence sort ------------------------------------------------------- */
623
624
  /**
625
   * @return the element sort of a sequence sort
626
   */
627
  Sort getSequenceElementSort() const;
628
629
  /* Uninterpreted sort -------------------------------------------------- */
630
631
  /**
632
   * @return the name of an uninterpreted sort
633
   */
634
  std::string getUninterpretedSortName() const;
635
636
  /**
637
   * @return true if an uninterpreted sort is parameterezied
638
   */
639
  bool isUninterpretedSortParameterized() const;
640
641
  /**
642
   * @return the parameter sorts of an uninterpreted sort
643
   */
644
  std::vector<Sort> getUninterpretedSortParamSorts() const;
645
646
  /* Sort constructor sort ----------------------------------------------- */
647
648
  /**
649
   * @return the name of a sort constructor sort
650
   */
651
  std::string getSortConstructorName() const;
652
653
  /**
654
   * @return the arity of a sort constructor sort
655
   */
656
  size_t getSortConstructorArity() const;
657
658
  /* Bit-vector sort ----------------------------------------------------- */
659
660
  /**
661
   * @return the bit-width of the bit-vector sort
662
   */
663
  uint32_t getBVSize() const;
664
665
  /* Floating-point sort ------------------------------------------------- */
666
667
  /**
668
   * @return the bit-width of the exponent of the floating-point sort
669
   */
670
  uint32_t getFPExponentSize() const;
671
672
  /**
673
   * @return the width of the significand of the floating-point sort
674
   */
675
  uint32_t getFPSignificandSize() const;
676
677
  /* Datatype sort ------------------------------------------------------- */
678
679
  /**
680
   * @return the parameter sorts of a datatype sort
681
   */
682
  std::vector<Sort> getDatatypeParamSorts() const;
683
684
  /**
685
   * @return the arity of a datatype sort
686
   */
687
  size_t getDatatypeArity() const;
688
689
  /* Tuple sort ---------------------------------------------------------- */
690
691
  /**
692
   * @return the length of a tuple sort
693
   */
694
  size_t getTupleLength() const;
695
696
  /**
697
   * @return the element sorts of a tuple sort
698
   */
699
  std::vector<Sort> getTupleSorts() const;
700
701
 private:
702
  /** @return the internal wrapped TypeNode of this sort. */
703
  const CVC4::TypeNode& getTypeNode(void) const;
704
705
  /** Helper to convert a set of Sorts to internal TypeNodes. */
706
  std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts);
707
  /** Helper to convert a vector of Sorts to internal TypeNodes. */
708
  std::vector<TypeNode> static sortVectorToTypeNodes(
709
      const std::vector<Sort>& sorts);
710
  /** Helper to convert a vector of internal TypeNodes to Sorts. */
711
  std::vector<Sort> static typeNodeVectorToSorts(
712
      const Solver* slv, const std::vector<TypeNode>& types);
713
714
  /**
715
   * Constructor.
716
   * @param slv the associated solver object
717
   * @param t the internal type that is to be wrapped by this sort
718
   * @return the Sort
719
   */
720
  Sort(const Solver* slv, const CVC4::TypeNode& t);
721
722
  /**
723
   * Helper for isNull checks. This prevents calling an API function with
724
   * CVC4_API_CHECK_NOT_NULL
725
   */
726
  bool isNullHelper() const;
727
728
  /**
729
   * The associated solver object.
730
   */
731
  const Solver* d_solver;
732
733
  /**
734
   * The interal type wrapped by this sort.
735
   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
736
   *       to memory allocation (CVC4::Type is already ref counted, so this
737
   *       could be a unique_ptr instead).
738
   */
739
  std::shared_ptr<CVC4::TypeNode> d_type;
740
};
741
742
/**
743
 * Serialize a sort to given stream.
744
 * @param out the output stream
745
 * @param s the sort to be serialized to the given output stream
746
 * @return the output stream
747
 */
748
std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_EXPORT;
749
750
/**
751
 * Hash function for Sorts.
752
 */
753
struct CVC4_EXPORT SortHashFunction
754
{
755
  size_t operator()(const Sort& s) const;
756
};
757
758
/* -------------------------------------------------------------------------- */
759
/* Op                                                                     */
760
/* -------------------------------------------------------------------------- */
761
762
/**
763
 * A CVC4 operator.
764
 * An operator is a term that represents certain operators, instantiated
765
 * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
766
 */
767
359955
class CVC4_EXPORT Op
768
{
769
  friend class Solver;
770
  friend class Term;
771
  friend struct OpHashFunction;
772
773
 public:
774
  /**
775
   * Constructor.
776
   */
777
  Op();
778
779
  /**
780
   * Destructor.
781
   */
782
  ~Op();
783
784
  /**
785
   * Syntactic equality operator.
786
   * Return true if both operators are syntactically identical.
787
   * Both operators must belong to the same solver object.
788
   * @param t the operator to compare to for equality
789
   * @return true if the operators are equal
790
   */
791
  bool operator==(const Op& t) const;
792
793
  /**
794
   * Syntactic disequality operator.
795
   * Return true if both operators differ syntactically.
796
   * Both terms must belong to the same solver object.
797
   * @param t the operator to compare to for disequality
798
   * @return true if operators are disequal
799
   */
800
  bool operator!=(const Op& t) const;
801
802
  /**
803
   * @return the kind of this operator
804
   */
805
  Kind getKind() const;
806
807
  /**
808
   * @return true if this operator is a null term
809
   */
810
  bool isNull() const;
811
812
  /**
813
   * @return true iff this operator is indexed
814
   */
815
  bool isIndexed() const;
816
817
  /**
818
   * Get the indices used to create this Op.
819
   * Supports the following template arguments:
820
   *   - string
821
   *   - Kind
822
   *   - uint32_t
823
   *   - pair<uint32_t, uint32_t>
824
   * Check the Op Kind with getKind() to determine which argument to use.
825
   * @return the indices used to create this Op
826
   */
827
  template <typename T>
828
  T getIndices() const;
829
830
  /**
831
   * @return a string representation of this operator
832
   */
833
  std::string toString() const;
834
835
 private:
836
  /**
837
   * Constructor for a single kind (non-indexed operator).
838
   * @param slv the associated solver object
839
   * @param k the kind of this Op
840
   */
841
  Op(const Solver* slv, const Kind k);
842
843
  /**
844
   * Constructor.
845
   * @param slv the associated solver object
846
   * @param k the kind of this Op
847
   * @param n the internal node that is to be wrapped by this term
848
   * @return the Term
849
   */
850
  Op(const Solver* slv, const Kind k, const CVC4::Node& n);
851
852
  /**
853
   * Helper for isNull checks. This prevents calling an API function with
854
   * CVC4_API_CHECK_NOT_NULL
855
   */
856
  bool isNullHelper() const;
857
858
  /**
859
   * Note: An indexed operator has a non-null internal node, d_node
860
   * Note 2: We use a helper method to avoid having API functions call
861
   *         other API functions (we need to call this internally)
862
   * @return true iff this Op is indexed
863
   */
864
  bool isIndexedHelper() const;
865
866
  /**
867
   * The associated solver object.
868
   */
869
  const Solver* d_solver;
870
871
  /** The kind of this operator. */
872
  Kind d_kind;
873
874
  /**
875
   * The internal node wrapped by this operator.
876
   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
877
   *       to memory allocation (CVC4::Node is already ref counted, so this
878
   *       could be a unique_ptr instead).
879
   */
880
  std::shared_ptr<CVC4::Node> d_node;
881
};
882
883
/* -------------------------------------------------------------------------- */
884
/* Term                                                                       */
885
/* -------------------------------------------------------------------------- */
886
887
/**
888
 * A CVC4 Term.
889
 */
890
49511478
class CVC4_EXPORT Term
891
{
892
  friend class CVC4::AssertCommand;
893
  friend class CVC4::BlockModelValuesCommand;
894
  friend class CVC4::CheckSatCommand;
895
  friend class CVC4::CheckSatAssumingCommand;
896
  friend class CVC4::DeclareSygusVarCommand;
897
  friend class CVC4::DefineFunctionCommand;
898
  friend class CVC4::DefineFunctionRecCommand;
899
  friend class CVC4::GetAbductCommand;
900
  friend class CVC4::GetInterpolCommand;
901
  friend class CVC4::GetModelCommand;
902
  friend class CVC4::GetQuantifierEliminationCommand;
903
  friend class CVC4::GetUnsatCoreCommand;
904
  friend class CVC4::GetValueCommand;
905
  friend class CVC4::SetUserAttributeCommand;
906
  friend class CVC4::SimplifyCommand;
907
  friend class CVC4::SygusConstraintCommand;
908
  friend class CVC4::SygusInvConstraintCommand;
909
  friend class CVC4::SynthFunCommand;
910
  friend class CVC4::QueryCommand;
911
  friend class Datatype;
912
  friend class DatatypeConstructor;
913
  friend class DatatypeSelector;
914
  friend class Solver;
915
  friend class Grammar;
916
  friend struct TermHashFunction;
917
918
 public:
919
  /**
920
   * Constructor.
921
   */
922
  Term();
923
924
  /**
925
   * Destructor.
926
   */
927
  ~Term();
928
929
  /**
930
   * Syntactic equality operator.
931
   * Return true if both terms are syntactically identical.
932
   * Both terms must belong to the same solver object.
933
   * @param t the term to compare to for equality
934
   * @return true if the terms are equal
935
   */
936
  bool operator==(const Term& t) const;
937
938
  /**
939
   * Syntactic disequality operator.
940
   * Return true if both terms differ syntactically.
941
   * Both terms must belong to the same solver object.
942
   * @param t the term to compare to for disequality
943
   * @return true if terms are disequal
944
   */
945
  bool operator!=(const Term& t) const;
946
947
  /**
948
   * Comparison for ordering on terms.
949
   * @param t the term to compare to
950
   * @return true if this term is less than t
951
   */
952
  bool operator<(const Term& t) const;
953
954
  /**
955
   * Comparison for ordering on terms.
956
   * @param t the term to compare to
957
   * @return true if this term is greater than t
958
   */
959
  bool operator>(const Term& t) const;
960
961
  /**
962
   * Comparison for ordering on terms.
963
   * @param t the term to compare to
964
   * @return true if this term is less than or equal to t
965
   */
966
  bool operator<=(const Term& t) const;
967
968
  /**
969
   * Comparison for ordering on terms.
970
   * @param t the term to compare to
971
   * @return true if this term is greater than or equal to t
972
   */
973
  bool operator>=(const Term& t) const;
974
975
  /** @return the number of children of this term  */
976
  size_t getNumChildren() const;
977
978
  /**
979
   * Get the child term at a given index.
980
   * @param index the index of the child term to return
981
   * @return the child term with the given index
982
   */
983
  Term operator[](size_t index) const;
984
985
  /**
986
   * @return the id of this term
987
   */
988
  uint64_t getId() const;
989
990
  /**
991
   * @return the kind of this term
992
   */
993
  Kind getKind() const;
994
995
  /**
996
   * @return the sort of this term
997
   */
998
  Sort getSort() const;
999
1000
  /**
1001
   * @return the result of replacing 'term' by 'replacement' in this term
1002
   */
1003
  Term substitute(const Term& term, const Term& replacement) const;
1004
1005
  /**
1006
   * @return the result of simulatenously replacing 'terms' by 'replacements'
1007
   * in this term
1008
   */
1009
  Term substitute(const std::vector<Term>& terms,
1010
                  const std::vector<Term>& replacements) const;
1011
1012
  /**
1013
   * @return true iff this term has an operator
1014
   */
1015
  bool hasOp() const;
1016
1017
  /**
1018
   * @return the Op used to create this term
1019
   * Note: This is safe to call when hasOp() returns true.
1020
   */
1021
  Op getOp() const;
1022
1023
  /**
1024
   * @return true if this Term is a null term
1025
   */
1026
  bool isNull() const;
1027
1028
  /**
1029
   *  Return the base (element stored at all indices) of a constant array
1030
   *  throws an exception if the kind is not CONST_ARRAY
1031
   *  @return the base value
1032
   */
1033
  Term getConstArrayBase() const;
1034
1035
  /**
1036
   *  Return the elements of a constant sequence
1037
   *  throws an exception if the kind is not CONST_SEQUENCE
1038
   *  @return the elements of the constant sequence.
1039
   */
1040
  std::vector<Term> getConstSequenceElements() const;
1041
1042
  /**
1043
   * Boolean negation.
1044
   * @return the Boolean negation of this term
1045
   */
1046
  Term notTerm() const;
1047
1048
  /**
1049
   * Boolean and.
1050
   * @param t a Boolean term
1051
   * @return the conjunction of this term and the given term
1052
   */
1053
  Term andTerm(const Term& t) const;
1054
1055
  /**
1056
   * Boolean or.
1057
   * @param t a Boolean term
1058
   * @return the disjunction of this term and the given term
1059
   */
1060
  Term orTerm(const Term& t) const;
1061
1062
  /**
1063
   * Boolean exclusive or.
1064
   * @param t a Boolean term
1065
   * @return the exclusive disjunction of this term and the given term
1066
   */
1067
  Term xorTerm(const Term& t) const;
1068
1069
  /**
1070
   * Equality.
1071
   * @param t a Boolean term
1072
   * @return the Boolean equivalence of this term and the given term
1073
   */
1074
  Term eqTerm(const Term& t) const;
1075
1076
  /**
1077
   * Boolean implication.
1078
   * @param t a Boolean term
1079
   * @return the implication of this term and the given term
1080
   */
1081
  Term impTerm(const Term& t) const;
1082
1083
  /**
1084
   * If-then-else with this term as the Boolean condition.
1085
   * @param then_t the 'then' term
1086
   * @param else_t the 'else' term
1087
   * @return the if-then-else term with this term as the Boolean condition
1088
   */
1089
  Term iteTerm(const Term& then_t, const Term& else_t) const;
1090
1091
  /**
1092
   * @return a string representation of this term
1093
   */
1094
  std::string toString() const;
1095
1096
  /**
1097
   * Iterator for the children of a Term.
1098
   * Note: This treats uninterpreted functions as Term just like any other term
1099
   *       for example, the term f(x, y) will have Kind APPLY_UF and three
1100
   *       children: f, x, and y
1101
   */
1102
468
  class const_iterator : public std::iterator<std::input_iterator_tag, Term>
1103
  {
1104
    friend class Term;
1105
1106
   public:
1107
    /**
1108
     * Null Constructor.
1109
     */
1110
    const_iterator();
1111
1112
    /**
1113
     * Constructor
1114
     * @param slv the associated solver object
1115
     * @param e a shared pointer to the node that we're iterating over
1116
     * @param p the position of the iterator (e.g. which child it's on)
1117
     */
1118
    const_iterator(const Solver* slv,
1119
                   const std::shared_ptr<CVC4::Node>& e,
1120
                   uint32_t p);
1121
1122
    /**
1123
     * Copy constructor.
1124
     */
1125
    const_iterator(const const_iterator& it);
1126
1127
    /**
1128
     * Assignment operator.
1129
     * @param it the iterator to assign to
1130
     * @return the reference to the iterator after assignment
1131
     */
1132
    const_iterator& operator=(const const_iterator& it);
1133
1134
    /**
1135
     * Equality operator.
1136
     * @param it the iterator to compare to for equality
1137
     * @return true if the iterators are equal
1138
     */
1139
    bool operator==(const const_iterator& it) const;
1140
1141
    /**
1142
     * Disequality operator.
1143
     * @param it the iterator to compare to for disequality
1144
     * @return true if the iterators are disequal
1145
     */
1146
    bool operator!=(const const_iterator& it) const;
1147
1148
    /**
1149
     * Increment operator (prefix).
1150
     * @return a reference to the iterator after incrementing by one
1151
     */
1152
    const_iterator& operator++();
1153
1154
    /**
1155
     * Increment operator (postfix).
1156
     * @return a reference to the iterator after incrementing by one
1157
     */
1158
    const_iterator operator++(int);
1159
1160
    /**
1161
     * Dereference operator.
1162
     * @return the term this iterator points to
1163
     */
1164
    Term operator*() const;
1165
1166
   private:
1167
    /**
1168
     * The associated solver object.
1169
     */
1170
    const Solver* d_solver;
1171
    /** The original node to be iterated over. */
1172
    std::shared_ptr<CVC4::Node> d_origNode;
1173
    /** Keeps track of the iteration position. */
1174
    uint32_t d_pos;
1175
  };
1176
1177
  /**
1178
   * @return an iterator to the first child of this Term
1179
   */
1180
  const_iterator begin() const;
1181
1182
  /**
1183
   * @return an iterator to one-off-the-last child of this Term
1184
   */
1185
  const_iterator end() const;
1186
1187
  /**
1188
   * @return true if the term is an integer that fits within std::int32_t.
1189
   */
1190
  bool isInt32() const;
1191
  /**
1192
   * @return the stored integer as a std::int32_t.
1193
   * Note: Asserts isInt32().
1194
   */
1195
  std::int32_t getInt32() const;
1196
  /**
1197
   * @return true if the term is an integer that fits within std::uint32_t.
1198
   */
1199
  bool isUInt32() const;
1200
  /**
1201
   * @return the stored integer as a std::uint32_t.
1202
   * Note: Asserts isUInt32().
1203
   */
1204
  std::uint32_t getUInt32() const;
1205
  /**
1206
   * @return true if the term is an integer that fits within std::int64_t.
1207
   */
1208
  bool isInt64() const;
1209
  /**
1210
   * @return the stored integer as a std::int64_t.
1211
   * Note: Asserts isInt64().
1212
   */
1213
  std::int64_t getInt64() const;
1214
  /**
1215
   * @return true if the term is an integer that fits within std::uint64_t.
1216
   */
1217
  bool isUInt64() const;
1218
  /**
1219
   * @return the stored integer as a std::uint64_t.
1220
   * Note: Asserts isUInt64().
1221
   */
1222
  std::uint64_t getUInt64() const;
1223
  /**
1224
   * @return true if the term is an integer.
1225
   */
1226
  bool isInteger() const;
1227
  /**
1228
   * @return the stored integer in (decimal) string representation.
1229
   * Note: Asserts isInteger().
1230
   */
1231
  std::string getInteger() const;
1232
1233
  /**
1234
   * @return true if the term is a string constant.
1235
   */
1236
  bool isString() const;
1237
  /**
1238
   * @return the stored string constant.
1239
   *
1240
   * Note: This method is not to be confused with toString() which returns the
1241
   *       term in some string representation, whatever data it may hold.
1242
   *       Asserts isString().
1243
   */
1244
  std::wstring getString() const;
1245
1246
 protected:
1247
  /**
1248
   * The associated solver object.
1249
   */
1250
  const Solver* d_solver;
1251
1252
 private:
1253
  /** Helper to convert a vector of Terms to internal Nodes. */
1254
  std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
1255
1256
  /**
1257
   * Constructor.
1258
   * @param slv the associated solver object
1259
   * @param n the internal node that is to be wrapped by this term
1260
   * @return the Term
1261
   */
1262
  Term(const Solver* slv, const CVC4::Node& n);
1263
1264
  /** @return the internal wrapped Node of this term. */
1265
  const CVC4::Node& getNode(void) const;
1266
1267
  /**
1268
   * Helper for isNull checks. This prevents calling an API function with
1269
   * CVC4_API_CHECK_NOT_NULL
1270
   */
1271
  bool isNullHelper() const;
1272
1273
  /**
1274
   * Helper function that returns the kind of the term, which takes into
1275
   * account special cases of the conversion for internal to external kinds.
1276
   * @return the kind of this term
1277
   */
1278
  Kind getKindHelper() const;
1279
1280
  /**
1281
   * @return true if the current term is a constant integer that is casted into
1282
   * real using the operator CAST_TO_REAL, and returns false otherwise
1283
   */
1284
  bool isCastedReal() const;
1285
  /**
1286
   * The internal node wrapped by this term.
1287
   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
1288
   *       to memory allocation (CVC4::Node is already ref counted, so this
1289
   *       could be a unique_ptr instead).
1290
   */
1291
  std::shared_ptr<CVC4::Node> d_node;
1292
};
1293
1294
/**
1295
 * Hash function for Terms.
1296
 */
1297
struct CVC4_EXPORT TermHashFunction
1298
{
1299
  size_t operator()(const Term& t) const;
1300
};
1301
1302
/**
1303
 * Serialize a term to given stream.
1304
 * @param out the output stream
1305
 * @param t the term to be serialized to the given output stream
1306
 * @return the output stream
1307
 */
1308
std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT;
1309
1310
/**
1311
 * Serialize a vector of terms to given stream.
1312
 * @param out the output stream
1313
 * @param vector the vector of terms to be serialized to the given stream
1314
 * @return the output stream
1315
 */
1316
std::ostream& operator<<(std::ostream& out,
1317
                         const std::vector<Term>& vector) CVC4_EXPORT;
1318
1319
/**
1320
 * Serialize a set of terms to the given stream.
1321
 * @param out the output stream
1322
 * @param set the set of terms to be serialized to the given stream
1323
 * @return the output stream
1324
 */
1325
std::ostream& operator<<(std::ostream& out,
1326
                         const std::set<Term>& set) CVC4_EXPORT;
1327
1328
/**
1329
 * Serialize an unordered_set of terms to the given stream.
1330
 *
1331
 * @param out the output stream
1332
 * @param unordered_set the set of terms to be serialized to the given stream
1333
 * @return the output stream
1334
 */
1335
std::ostream& operator<<(std::ostream& out,
1336
                         const std::unordered_set<Term, TermHashFunction>&
1337
                             unordered_set) CVC4_EXPORT;
1338
1339
/**
1340
 * Serialize a map of terms to the given stream.
1341
 *
1342
 * @param out the output stream
1343
 * @param map the map of terms to be serialized to the given stream
1344
 * @return the output stream
1345
 */
1346
template <typename V>
1347
std::ostream& operator<<(std::ostream& out,
1348
                         const std::map<Term, V>& map) CVC4_EXPORT;
1349
1350
/**
1351
 * Serialize an unordered_map of terms to the given stream.
1352
 *
1353
 * @param out the output stream
1354
 * @param unordered_map the map of terms to be serialized to the given stream
1355
 * @return the output stream
1356
 */
1357
template <typename V>
1358
std::ostream& operator<<(std::ostream& out,
1359
                         const std::unordered_map<Term, V, TermHashFunction>&
1360
                             unordered_map) CVC4_EXPORT;
1361
1362
/**
1363
 * Serialize an operator to given stream.
1364
 * @param out the output stream
1365
 * @param t the operator to be serialized to the given output stream
1366
 * @return the output stream
1367
 */
1368
std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_EXPORT;
1369
1370
/**
1371
 * Hash function for Ops.
1372
 */
1373
struct CVC4_EXPORT OpHashFunction
1374
{
1375
  size_t operator()(const Op& t) const;
1376
};
1377
1378
/* -------------------------------------------------------------------------- */
1379
/* Datatypes                                                                  */
1380
/* -------------------------------------------------------------------------- */
1381
1382
class DatatypeConstructorIterator;
1383
class DatatypeIterator;
1384
1385
/**
1386
 * A CVC4 datatype constructor declaration.
1387
 */
1388
20
class CVC4_EXPORT DatatypeConstructorDecl
1389
{
1390
  friend class DatatypeDecl;
1391
  friend class Solver;
1392
1393
 public:
1394
  /** Constructor.  */
1395
  DatatypeConstructorDecl();
1396
1397
  /**
1398
   * Destructor.
1399
   */
1400
  ~DatatypeConstructorDecl();
1401
1402
  /**
1403
   * Add datatype selector declaration.
1404
   * @param name the name of the datatype selector declaration to add
1405
   * @param sort the range sort of the datatype selector declaration to add
1406
   */
1407
  void addSelector(const std::string& name, const Sort& sort);
1408
  /**
1409
   * Add datatype selector declaration whose range type is the datatype itself.
1410
   * @param name the name of the datatype selector declaration to add
1411
   */
1412
  void addSelectorSelf(const std::string& name);
1413
1414
  /**
1415
   * @return true if this DatatypeConstructorDecl is a null declaration.
1416
   */
1417
  bool isNull() const;
1418
1419
  /**
1420
   * @return a string representation of this datatype constructor declaration
1421
   */
1422
  std::string toString() const;
1423
1424
 private:
1425
  /**
1426
   * Constructor.
1427
   * @param slv the associated solver object
1428
   * @param name the name of the datatype constructor
1429
   * @return the DatatypeConstructorDecl
1430
   */
1431
  DatatypeConstructorDecl(const Solver* slv, const std::string& name);
1432
1433
  /**
1434
   * Helper for isNull checks. This prevents calling an API function with
1435
   * CVC4_API_CHECK_NOT_NULL
1436
   */
1437
  bool isNullHelper() const;
1438
1439
  /**
1440
   * The associated solver object.
1441
   */
1442
  const Solver* d_solver;
1443
1444
  /**
1445
   * The internal (intermediate) datatype constructor wrapped by this
1446
   * datatype constructor declaration.
1447
   * Note: This is a shared_ptr rather than a unique_ptr since
1448
   *       CVC4::DTypeConstructor is not ref counted.
1449
   */
1450
  std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
1451
};
1452
1453
class Solver;
1454
1455
/**
1456
 * A CVC4 datatype declaration.
1457
 */
1458
1563
class CVC4_EXPORT DatatypeDecl
1459
{
1460
  friend class DatatypeConstructorArg;
1461
  friend class Solver;
1462
  friend class Grammar;
1463
1464
 public:
1465
  /** Constructor.  */
1466
  DatatypeDecl();
1467
1468
  /**
1469
   * Destructor.
1470
   */
1471
  ~DatatypeDecl();
1472
1473
  /**
1474
   * Add datatype constructor declaration.
1475
   * @param ctor the datatype constructor declaration to add
1476
   */
1477
  void addConstructor(const DatatypeConstructorDecl& ctor);
1478
1479
  /** Get the number of constructors (so far) for this Datatype declaration. */
1480
  size_t getNumConstructors() const;
1481
1482
  /** Is this Datatype declaration parametric? */
1483
  bool isParametric() const;
1484
1485
  /**
1486
   * @return true if this DatatypeDecl is a null object
1487
   */
1488
  bool isNull() const;
1489
1490
  /**
1491
   * @return a string representation of this datatype declaration
1492
   */
1493
  std::string toString() const;
1494
1495
  /** @return the name of this datatype declaration. */
1496
  std::string getName() const;
1497
1498
 private:
1499
  /**
1500
   * Constructor.
1501
   * @param slv the associated solver object
1502
   * @param name the name of the datatype
1503
   * @param isCoDatatype true if a codatatype is to be constructed
1504
   * @return the DatatypeDecl
1505
   */
1506
  DatatypeDecl(const Solver* slv,
1507
               const std::string& name,
1508
               bool isCoDatatype = false);
1509
1510
  /**
1511
   * Constructor for parameterized datatype declaration.
1512
   * Create sorts parameter with Solver::mkParamSort().
1513
   * @param slv the associated solver object
1514
   * @param name the name of the datatype
1515
   * @param param the sort parameter
1516
   * @param isCoDatatype true if a codatatype is to be constructed
1517
   */
1518
  DatatypeDecl(const Solver* slv,
1519
               const std::string& name,
1520
               const Sort& param,
1521
               bool isCoDatatype = false);
1522
1523
  /**
1524
   * Constructor for parameterized datatype declaration.
1525
   * Create sorts parameter with Solver::mkParamSort().
1526
   * @param slv the associated solver object
1527
   * @param name the name of the datatype
1528
   * @param params a list of sort parameters
1529
   * @param isCoDatatype true if a codatatype is to be constructed
1530
   */
1531
  DatatypeDecl(const Solver* slv,
1532
               const std::string& name,
1533
               const std::vector<Sort>& params,
1534
               bool isCoDatatype = false);
1535
1536
  /** @return the internal wrapped Dtype of this datatype declaration. */
1537
  CVC4::DType& getDatatype(void) const;
1538
1539
  /**
1540
   * Helper for isNull checks. This prevents calling an API function with
1541
   * CVC4_API_CHECK_NOT_NULL
1542
   */
1543
  bool isNullHelper() const;
1544
1545
  /**
1546
   * The associated solver object.
1547
   */
1548
  const Solver* d_solver;
1549
1550
  /**
1551
   * The internal (intermediate) datatype wrapped by this datatype
1552
   * declaration.
1553
   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1554
   *       not ref counted.
1555
   */
1556
  std::shared_ptr<CVC4::DType> d_dtype;
1557
};
1558
1559
/**
1560
 * A CVC4 datatype selector.
1561
 */
1562
class CVC4_EXPORT DatatypeSelector
1563
{
1564
  friend class DatatypeConstructor;
1565
  friend class Solver;
1566
1567
 public:
1568
  /**
1569
   * Constructor.
1570
   */
1571
  DatatypeSelector();
1572
1573
  /**
1574
   * Destructor.
1575
   */
1576
  ~DatatypeSelector();
1577
1578
  /** @return the name of this Datatype selector. */
1579
  std::string getName() const;
1580
1581
  /**
1582
   * Get the selector operator of this datatype selector.
1583
   * @return the selector term
1584
   */
1585
  Term getSelectorTerm() const;
1586
1587
  /** @return the range sort of this argument. */
1588
  Sort getRangeSort() const;
1589
1590
  /**
1591
   * @return true if this DatatypeSelector is a null object
1592
   */
1593
  bool isNull() const;
1594
1595
  /**
1596
   * @return a string representation of this datatype selector
1597
   */
1598
  std::string toString() const;
1599
1600
 private:
1601
  /**
1602
   * Constructor.
1603
   * @param slv the associated solver object
1604
   * @param stor the internal datatype selector to be wrapped
1605
   * @return the DatatypeSelector
1606
   */
1607
  DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor);
1608
1609
  /**
1610
   * Helper for isNull checks. This prevents calling an API function with
1611
   * CVC4_API_CHECK_NOT_NULL
1612
   */
1613
  bool isNullHelper() const;
1614
1615
  /**
1616
   * The associated solver object.
1617
   */
1618
  const Solver* d_solver;
1619
1620
  /**
1621
   * The internal datatype selector wrapped by this datatype selector.
1622
   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1623
   *       not ref counted.
1624
   */
1625
  std::shared_ptr<CVC4::DTypeSelector> d_stor;
1626
};
1627
1628
/**
1629
 * A CVC4 datatype constructor.
1630
 */
1631
class CVC4_EXPORT DatatypeConstructor
1632
{
1633
  friend class Datatype;
1634
  friend class Solver;
1635
1636
 public:
1637
  /**
1638
   * Constructor.
1639
   */
1640
  DatatypeConstructor();
1641
1642
  /**
1643
   * Destructor.
1644
   */
1645
  ~DatatypeConstructor();
1646
1647
  /** @return the name of this Datatype constructor. */
1648
  std::string getName() const;
1649
1650
  /**
1651
   * Get the constructor operator of this datatype constructor.
1652
   * @return the constructor term
1653
   */
1654
  Term getConstructorTerm() const;
1655
1656
  /**
1657
   * Get the constructor operator of this datatype constructor whose return
1658
   * type is retSort. This method is intended to be used on constructors of
1659
   * parametric datatypes and can be seen as returning the constructor
1660
   * term that has been explicitly cast to the given sort.
1661
   *
1662
   * This method is required for constructors of parametric datatypes whose
1663
   * return type cannot be determined by type inference. For example, given:
1664
   *   (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
1665
   * The type of nil terms need to be provided by the user. In SMT version 2.6,
1666
   * this is done via the syntax for qualified identifiers:
1667
   *   (as nil (List Int))
1668
   * This method is equivalent of applying the above, where this
1669
   * DatatypeConstructor is the one corresponding to nil, and retSort is
1670
   * (List Int).
1671
   *
1672
   * Furthermore note that the returned constructor term t is an operator,
1673
   * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
1674
   * (nullary) application of nil.
1675
   *
1676
   * @param retSort the desired return sort of the constructor
1677
   * @return the constructor term
1678
   */
1679
  Term getSpecializedConstructorTerm(const Sort& retSort) const;
1680
1681
  /**
1682
   * Get the tester operator of this datatype constructor.
1683
   * @return the tester operator
1684
   */
1685
  Term getTesterTerm() const;
1686
1687
  /**
1688
   * @return the number of selectors (so far) of this Datatype constructor.
1689
   */
1690
  size_t getNumSelectors() const;
1691
1692
  /** @return the i^th DatatypeSelector. */
1693
  DatatypeSelector operator[](size_t index) const;
1694
  /**
1695
   * Get the datatype selector with the given name.
1696
   * This is a linear search through the selectors, so in case of
1697
   * multiple, similarly-named selectors, the first is returned.
1698
   * @param name the name of the datatype selector
1699
   * @return the first datatype selector with the given name
1700
   */
1701
  DatatypeSelector operator[](const std::string& name) const;
1702
  DatatypeSelector getSelector(const std::string& name) const;
1703
1704
  /**
1705
   * Get the term representation of the datatype selector with the given name.
1706
   * This is a linear search through the arguments, so in case of multiple,
1707
   * similarly-named arguments, the selector for the first is returned.
1708
   * @param name the name of the datatype selector
1709
   * @return a term representing the datatype selector with the given name
1710
   */
1711
  Term getSelectorTerm(const std::string& name) const;
1712
1713
  /**
1714
   * @return true if this DatatypeConstructor is a null object
1715
   */
1716
  bool isNull() const;
1717
1718
  /**
1719
   * @return a string representation of this datatype constructor
1720
   */
1721
  std::string toString() const;
1722
1723
  /**
1724
   * Iterator for the selectors of a datatype constructor.
1725
   */
1726
  class const_iterator
1727
      : public std::iterator<std::input_iterator_tag, DatatypeConstructor>
1728
  {
1729
    friend class DatatypeConstructor;  // to access constructor
1730
1731
   public:
1732
    /** Nullary constructor (required for Cython). */
1733
    const_iterator();
1734
1735
    /**
1736
     * Assignment operator.
1737
     * @param it the iterator to assign to
1738
     * @return the reference to the iterator after assignment
1739
     */
1740
    const_iterator& operator=(const const_iterator& it);
1741
1742
    /**
1743
     * Equality operator.
1744
     * @param it the iterator to compare to for equality
1745
     * @return true if the iterators are equal
1746
     */
1747
    bool operator==(const const_iterator& it) const;
1748
1749
    /**
1750
     * Disequality operator.
1751
     * @param it the iterator to compare to for disequality
1752
     * @return true if the iterators are disequal
1753
     */
1754
    bool operator!=(const const_iterator& it) const;
1755
1756
    /**
1757
     * Increment operator (prefix).
1758
     * @return a reference to the iterator after incrementing by one
1759
     */
1760
    const_iterator& operator++();
1761
1762
    /**
1763
     * Increment operator (postfix).
1764
     * @return a reference to the iterator after incrementing by one
1765
     */
1766
    const_iterator operator++(int);
1767
1768
    /**
1769
     * Dereference operator.
1770
     * @return a reference to the selector this iterator points to
1771
     */
1772
    const DatatypeSelector& operator*() const;
1773
1774
    /**
1775
     * Dereference operator.
1776
     * @return a pointer to the selector this iterator points to
1777
     */
1778
    const DatatypeSelector* operator->() const;
1779
1780
   private:
1781
    /**
1782
     * Constructor.
1783
     * @param slv the associated Solver object
1784
     * @param ctor the internal datatype constructor to iterate over
1785
     * @param true if this is a begin() iterator
1786
     */
1787
    const_iterator(const Solver* slv,
1788
                   const CVC4::DTypeConstructor& ctor,
1789
                   bool begin);
1790
1791
    /**
1792
     * The associated solver object.
1793
     */
1794
    const Solver* d_solver;
1795
1796
    /**
1797
     * A pointer to the list of selectors of the internal datatype
1798
     * constructor to iterate over.
1799
     * This pointer is maintained for operators == and != only.
1800
     */
1801
    const void* d_int_stors;
1802
1803
    /** The list of datatype selector (wrappers) to iterate over. */
1804
    std::vector<DatatypeSelector> d_stors;
1805
1806
    /** The current index of the iterator. */
1807
    size_t d_idx;
1808
  };
1809
1810
  /**
1811
   * @return an iterator to the first selector of this constructor
1812
   */
1813
  const_iterator begin() const;
1814
1815
  /**
1816
   * @return an iterator to one-off-the-last selector of this constructor
1817
   */
1818
  const_iterator end() const;
1819
1820
 private:
1821
  /**
1822
   * Constructor.
1823
   * @param ctor the internal datatype constructor to be wrapped
1824
   * @return the DatatypeConstructor
1825
   */
1826
  DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor);
1827
1828
  /**
1829
   * Return selector for name.
1830
   * @param name The name of selector to find
1831
   * @return the selector object for the name
1832
   */
1833
  DatatypeSelector getSelectorForName(const std::string& name) const;
1834
1835
  /**
1836
   * Helper for isNull checks. This prevents calling an API function with
1837
   * CVC4_API_CHECK_NOT_NULL
1838
   */
1839
  bool isNullHelper() const;
1840
1841
  /**
1842
   * The associated solver object.
1843
   */
1844
  const Solver* d_solver;
1845
1846
  /**
1847
   * The internal datatype constructor wrapped by this datatype constructor.
1848
   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1849
   *       not ref counted.
1850
   */
1851
  std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
1852
};
1853
1854
/*
1855
 * A CVC4 datatype.
1856
 */
1857
class CVC4_EXPORT Datatype
1858
{
1859
  friend class Solver;
1860
  friend class Sort;
1861
1862
 public:
1863
  /** Constructor. */
1864
  Datatype();
1865
1866
  /**
1867
   * Destructor.
1868
   */
1869
  ~Datatype();
1870
1871
  /**
1872
   * Get the datatype constructor at a given index.
1873
   * @param idx the index of the datatype constructor to return
1874
   * @return the datatype constructor with the given index
1875
   */
1876
  DatatypeConstructor operator[](size_t idx) const;
1877
1878
  /**
1879
   * Get the datatype constructor with the given name.
1880
   * This is a linear search through the constructors, so in case of multiple,
1881
   * similarly-named constructors, the first is returned.
1882
   * @param name the name of the datatype constructor
1883
   * @return the datatype constructor with the given name
1884
   */
1885
  DatatypeConstructor operator[](const std::string& name) const;
1886
  DatatypeConstructor getConstructor(const std::string& name) const;
1887
1888
  /**
1889
   * Get a term representing the datatype constructor with the given name.
1890
   * This is a linear search through the constructors, so in case of multiple,
1891
   * similarly-named constructors, the
1892
   * first is returned.
1893
   */
1894
  Term getConstructorTerm(const std::string& name) const;
1895
1896
  /** @return the name of this Datatype. */
1897
  std::string getName() const;
1898
1899
  /** @return the number of constructors for this Datatype. */
1900
  size_t getNumConstructors() const;
1901
1902
  /** @return true if this datatype is parametric */
1903
  bool isParametric() const;
1904
1905
  /** @return true if this datatype corresponds to a co-datatype */
1906
  bool isCodatatype() const;
1907
1908
  /** @return true if this datatype corresponds to a tuple */
1909
  bool isTuple() const;
1910
1911
  /** @return true if this datatype corresponds to a record */
1912
  bool isRecord() const;
1913
1914
  /** @return true if this datatype is finite */
1915
  bool isFinite() const;
1916
1917
  /**
1918
   * Is this datatype well-founded? If this datatype is not a codatatype,
1919
   * this returns false if there are no values of this datatype that are of
1920
   * finite size.
1921
   *
1922
   * @return true if this datatype is well-founded
1923
   */
1924
  bool isWellFounded() const;
1925
1926
  /**
1927
   * Does this datatype have nested recursion? This method returns false if a
1928
   * value of this datatype includes a subterm of its type that is nested
1929
   * beneath a non-datatype type constructor. For example, a datatype
1930
   * T containing a constructor having a selector with range type (Set T) has
1931
   * nested recursion.
1932
   *
1933
   * @return true if this datatype has nested recursion
1934
   */
1935
  bool hasNestedRecursion() const;
1936
1937
  /**
1938
   * @return true if this Datatype is a null object
1939
   */
1940
  bool isNull() const;
1941
1942
  /**
1943
   * @return a string representation of this datatype
1944
   */
1945
  std::string toString() const;
1946
1947
  /**
1948
   * Iterator for the constructors of a datatype.
1949
   */
1950
  class const_iterator : public std::iterator<std::input_iterator_tag, Datatype>
1951
  {
1952
    friend class Datatype;  // to access constructor
1953
1954
   public:
1955
    /** Nullary constructor (required for Cython). */
1956
    const_iterator();
1957
1958
    /**
1959
     * Assignment operator.
1960
     * @param it the iterator to assign to
1961
     * @return the reference to the iterator after assignment
1962
     */
1963
    const_iterator& operator=(const const_iterator& it);
1964
1965
    /**
1966
     * Equality operator.
1967
     * @param it the iterator to compare to for equality
1968
     * @return true if the iterators are equal
1969
     */
1970
    bool operator==(const const_iterator& it) const;
1971
1972
    /**
1973
     * Disequality operator.
1974
     * @param it the iterator to compare to for disequality
1975
     * @return true if the iterators are disequal
1976
     */
1977
    bool operator!=(const const_iterator& it) const;
1978
1979
    /**
1980
     * Increment operator (prefix).
1981
     * @return a reference to the iterator after incrementing by one
1982
     */
1983
    const_iterator& operator++();
1984
1985
    /**
1986
     * Increment operator (postfix).
1987
     * @return a reference to the iterator after incrementing by one
1988
     */
1989
    const_iterator operator++(int);
1990
1991
    /**
1992
     * Dereference operator.
1993
     * @return a reference to the constructor this iterator points to
1994
     */
1995
    const DatatypeConstructor& operator*() const;
1996
1997
    /**
1998
     * Dereference operator.
1999
     * @return a pointer to the constructor this iterator points to
2000
     */
2001
    const DatatypeConstructor* operator->() const;
2002
2003
   private:
2004
    /**
2005
     * Constructor.
2006
     * @param slv the associated Solver object
2007
     * @param dtype the internal datatype to iterate over
2008
     * @param true if this is a begin() iterator
2009
     */
2010
    const_iterator(const Solver* slv, const CVC4::DType& dtype, bool begin);
2011
2012
    /**
2013
     * The associated solver object.
2014
     */
2015
    const Solver* d_solver;
2016
2017
    /**
2018
     * A pointer to the list of constructors of the internal datatype
2019
     * to iterate over.
2020
     * This pointer is maintained for operators == and != only.
2021
     */
2022
    const void* d_int_ctors;
2023
2024
    /** The list of datatype constructor (wrappers) to iterate over. */
2025
    std::vector<DatatypeConstructor> d_ctors;
2026
2027
    /** The current index of the iterator. */
2028
    size_t d_idx;
2029
  };
2030
2031
  /**
2032
   * @return an iterator to the first constructor of this datatype
2033
   */
2034
  const_iterator begin() const;
2035
2036
  /**
2037
   * @return an iterator to one-off-the-last constructor of this datatype
2038
   */
2039
  const_iterator end() const;
2040
2041
 private:
2042
  /**
2043
   * Constructor.
2044
   * @param dtype the internal datatype to be wrapped
2045
   * @return the Datatype
2046
   */
2047
  Datatype(const Solver* slv, const CVC4::DType& dtype);
2048
2049
  /**
2050
   * Return constructor for name.
2051
   * @param name The name of constructor to find
2052
   * @return the constructor object for the name
2053
   */
2054
  DatatypeConstructor getConstructorForName(const std::string& name) const;
2055
2056
  /**
2057
   * Helper for isNull checks. This prevents calling an API function with
2058
   * CVC4_API_CHECK_NOT_NULL
2059
   */
2060
  bool isNullHelper() const;
2061
2062
  /**
2063
   * The associated solver object.
2064
   */
2065
  const Solver* d_solver;
2066
2067
  /**
2068
   * The internal datatype wrapped by this datatype.
2069
   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
2070
   *       not ref counted.
2071
   */
2072
  std::shared_ptr<CVC4::DType> d_dtype;
2073
};
2074
2075
/**
2076
 * Serialize a datatype declaration to given stream.
2077
 * @param out the output stream
2078
 * @param dtdecl the datatype declaration to be serialized to the given stream
2079
 * @return the output stream
2080
 */
2081
std::ostream& operator<<(std::ostream& out,
2082
                         const DatatypeDecl& dtdecl) CVC4_EXPORT;
2083
2084
/**
2085
 * Serialize a datatype constructor declaration to given stream.
2086
 * @param out the output stream
2087
 * @param ctordecl the datatype constructor declaration to be serialized
2088
 * @return the output stream
2089
 */
2090
std::ostream& operator<<(std::ostream& out,
2091
                         const DatatypeConstructorDecl& ctordecl) CVC4_EXPORT;
2092
2093
/**
2094
 * Serialize a vector of datatype constructor declarations to given stream.
2095
 * @param out the output stream
2096
 * @param vector the vector of datatype constructor declarations to be
2097
 * serialized to the given stream
2098
 * @return the output stream
2099
 */
2100
std::ostream& operator<<(std::ostream& out,
2101
                         const std::vector<DatatypeConstructorDecl>& vector);
2102
2103
/**
2104
 * Serialize a datatype to given stream.
2105
 * @param out the output stream
2106
 * @param dtdecl the datatype to be serialized to given stream
2107
 * @return the output stream
2108
 */
2109
std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT;
2110
2111
/**
2112
 * Serialize a datatype constructor to given stream.
2113
 * @param out the output stream
2114
 * @param ctor the datatype constructor to be serialized to given stream
2115
 * @return the output stream
2116
 */
2117
std::ostream& operator<<(std::ostream& out,
2118
                         const DatatypeConstructor& ctor) CVC4_EXPORT;
2119
2120
/**
2121
 * Serialize a datatype selector to given stream.
2122
 * @param out the output stream
2123
 * @param ctor the datatype selector to be serialized to given stream
2124
 * @return the output stream
2125
 */
2126
std::ostream& operator<<(std::ostream& out,
2127
                         const DatatypeSelector& stor) CVC4_EXPORT;
2128
2129
/* -------------------------------------------------------------------------- */
2130
/* Grammar                                                                    */
2131
/* -------------------------------------------------------------------------- */
2132
2133
/**
2134
 * A Sygus Grammar.
2135
 */
2136
303
class CVC4_EXPORT Grammar
2137
{
2138
  friend class CVC4::GetAbductCommand;
2139
  friend class CVC4::GetInterpolCommand;
2140
  friend class CVC4::SynthFunCommand;
2141
  friend class Solver;
2142
2143
 public:
2144
  /**
2145
   * Add <rule> to the set of rules corresponding to <ntSymbol>.
2146
   * @param ntSymbol the non-terminal to which the rule is added
2147
   * @param rule the rule to add
2148
   */
2149
  void addRule(const Term& ntSymbol, const Term& rule);
2150
2151
  /**
2152
   * Add <rules> to the set of rules corresponding to <ntSymbol>.
2153
   * @param ntSymbol the non-terminal to which the rules are added
2154
   * @param rule the rules to add
2155
   */
2156
  void addRules(const Term& ntSymbol, const std::vector<Term>& rules);
2157
2158
  /**
2159
   * Allow <ntSymbol> to be an arbitrary constant.
2160
   * @param ntSymbol the non-terminal allowed to be any constant
2161
   */
2162
  void addAnyConstant(const Term& ntSymbol);
2163
2164
  /**
2165
   * Allow <ntSymbol> to be any input variable to corresponding
2166
   * synth-fun/synth-inv with the same sort as <ntSymbol>.
2167
   * @param ntSymbol the non-terminal allowed to be any input constant
2168
   */
2169
  void addAnyVariable(const Term& ntSymbol);
2170
2171
  /**
2172
   * @return a string representation of this grammar.
2173
   */
2174
  std::string toString() const;
2175
2176
  /**
2177
   * Nullary constructor. Needed for the Cython API.
2178
   */
2179
  Grammar();
2180
2181
 private:
2182
  /**
2183
   * Constructor.
2184
   * @param slv the solver that created this grammar
2185
   * @param sygusVars the input variables to synth-fun/synth-var
2186
   * @param ntSymbols the non-terminals of this grammar
2187
   */
2188
  Grammar(const Solver* slv,
2189
          const std::vector<Term>& sygusVars,
2190
          const std::vector<Term>& ntSymbols);
2191
2192
  /**
2193
   * @return the resolved datatype of the Start symbol of the grammar
2194
   */
2195
  Sort resolve();
2196
2197
  /**
2198
   * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
2199
   *
2200
   * <ntsToUnres> contains a mapping from non-terminal symbols to the
2201
   * unresolved sorts they correspond to. This map indicates how the argument
2202
   * <term> should be interpreted (instances of symbols from the domain of
2203
   * <ntsToUnres> correspond to constructor arguments).
2204
   *
2205
   * The sygus operator that is actually added to <dt> corresponds to replacing
2206
   * each occurrence of non-terminal symbols from the domain of <ntsToUnres>
2207
   * with bound variables via purifySygusGTerm, and binding these variables
2208
   * via a lambda.
2209
   *
2210
   * @param dt the non-terminal's datatype to which a constructor is added
2211
   * @param term the sygus operator of the constructor
2212
   * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2213
   */
2214
  void addSygusConstructorTerm(
2215
      DatatypeDecl& dt,
2216
      const Term& term,
2217
      const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const;
2218
2219
  /**
2220
   * Purify SyGuS grammar term.
2221
   *
2222
   * This returns a term where all occurrences of non-terminal symbols (those
2223
   * in the domain of <ntsToUnres>) are replaced by fresh variables. For
2224
   * each variable replaced in this way, we add the fresh variable it is
2225
   * replaced with to <args>, and the unresolved sorts corresponding to the
2226
   * non-terminal symbol to <cargs> (constructor args). In other words, <args>
2227
   * contains the free variables in the term returned by this method (which
2228
   * should be bound by a lambda), and <cargs> contains the sorts of the
2229
   * arguments of the sygus constructor.
2230
   *
2231
   * @param term the term to purify
2232
   * @param args the free variables in the term returned by this method
2233
   * @param cargs the sorts of the arguments of the sygus constructor
2234
   * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2235
   * @return the purfied term
2236
   */
2237
  Term purifySygusGTerm(
2238
      const Term& term,
2239
      std::vector<Term>& args,
2240
      std::vector<Sort>& cargs,
2241
      const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const;
2242
2243
  /**
2244
   * This adds constructors to <dt> for sygus variables in <d_sygusVars> whose
2245
   * sort is argument <sort>. This method should be called when the sygus
2246
   * grammar term (Variable sort) is encountered.
2247
   *
2248
   * @param dt the non-terminal's datatype to which the constructors are added
2249
   * @param sort the sort of the sygus variables to add
2250
   */
2251
  void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const;
2252
2253
  /** The solver that created this grammar. */
2254
  const Solver* d_solver;
2255
  /** Input variables to the corresponding function/invariant to synthesize.*/
2256
  std::vector<Term> d_sygusVars;
2257
  /** The non-terminal symbols of this grammar. */
2258
  std::vector<Term> d_ntSyms;
2259
  /** The mapping from non-terminal symbols to their production terms. */
2260
  std::unordered_map<Term, std::vector<Term>, TermHashFunction> d_ntsToTerms;
2261
  /** The set of non-terminals that can be arbitrary constants. */
2262
  std::unordered_set<Term, TermHashFunction> d_allowConst;
2263
  /** The set of non-terminals that can be sygus variables. */
2264
  std::unordered_set<Term, TermHashFunction> d_allowVars;
2265
  /** Did we call resolve() before? */
2266
  bool d_isResolved;
2267
};
2268
2269
/**
2270
 * Serialize a grammar to given stream.
2271
 * @param out the output stream
2272
 * @param g the grammar to be serialized to the given output stream
2273
 * @return the output stream
2274
 */
2275
std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT;
2276
2277
/* -------------------------------------------------------------------------- */
2278
/* Rounding Mode for Floating Points                                          */
2279
/* -------------------------------------------------------------------------- */
2280
2281
/**
2282
 * A CVC4 floating point rounding mode.
2283
 */
2284
enum CVC4_EXPORT RoundingMode
2285
{
2286
  ROUND_NEAREST_TIES_TO_EVEN,
2287
  ROUND_TOWARD_POSITIVE,
2288
  ROUND_TOWARD_NEGATIVE,
2289
  ROUND_TOWARD_ZERO,
2290
  ROUND_NEAREST_TIES_TO_AWAY,
2291
};
2292
2293
/**
2294
 * Hash function for RoundingModes.
2295
 */
2296
struct CVC4_EXPORT RoundingModeHashFunction
2297
{
2298
  inline size_t operator()(const RoundingMode& rm) const;
2299
};
2300
2301
/* -------------------------------------------------------------------------- */
2302
/* Solver                                                                     */
2303
/* -------------------------------------------------------------------------- */
2304
2305
/*
2306
 * A CVC4 solver.
2307
 */
2308
class CVC4_EXPORT Solver
2309
{
2310
  friend class Datatype;
2311
  friend class DatatypeDecl;
2312
  friend class DatatypeConstructor;
2313
  friend class DatatypeConstructorDecl;
2314
  friend class DatatypeSelector;
2315
  friend class Grammar;
2316
  friend class Op;
2317
  friend class Sort;
2318
  friend class Term;
2319
2320
 public:
2321
  /* .................................................................... */
2322
  /* Constructors/Destructors                                             */
2323
  /* .................................................................... */
2324
2325
  /**
2326
   * Constructor.
2327
   * @param opts an optional pointer to a solver options object
2328
   * @return the Solver
2329
   */
2330
  Solver(Options* opts = nullptr);
2331
2332
  /**
2333
   * Destructor.
2334
   */
2335
  ~Solver();
2336
2337
  /**
2338
   * Disallow copy/assignment.
2339
   */
2340
  Solver(const Solver&) = delete;
2341
  Solver& operator=(const Solver&) = delete;
2342
2343
  /* .................................................................... */
2344
  /* Solver Configuration                                                 */
2345
  /* .................................................................... */
2346
2347
  bool supportsFloatingPoint() const;
2348
2349
  /* .................................................................... */
2350
  /* Sorts Handling                                                       */
2351
  /* .................................................................... */
2352
2353
  /**
2354
   * @return sort null
2355
   */
2356
  Sort getNullSort() const;
2357
2358
  /**
2359
   * @return sort Boolean
2360
   */
2361
  Sort getBooleanSort() const;
2362
2363
  /**
2364
   * @return sort Integer (in CVC4, Integer is a subtype of Real)
2365
   */
2366
  Sort getIntegerSort() const;
2367
2368
  /**
2369
   * @return sort Real
2370
   */
2371
  Sort getRealSort() const;
2372
2373
  /**
2374
   * @return sort RegExp
2375
   */
2376
  Sort getRegExpSort() const;
2377
2378
  /**
2379
   * @return sort RoundingMode
2380
   */
2381
  Sort getRoundingModeSort() const;
2382
2383
  /**
2384
   * @return sort String
2385
   */
2386
  Sort getStringSort() const;
2387
2388
  /**
2389
   * Create an array sort.
2390
   * @param indexSort the array index sort
2391
   * @param elemSort the array element sort
2392
   * @return the array sort
2393
   */
2394
  Sort mkArraySort(const Sort& indexSort, const Sort& elemSort) const;
2395
2396
  /**
2397
   * Create a bit-vector sort.
2398
   * @param size the bit-width of the bit-vector sort
2399
   * @return the bit-vector sort
2400
   */
2401
  Sort mkBitVectorSort(uint32_t size) const;
2402
2403
  /**
2404
   * Create a floating-point sort.
2405
   * @param exp the bit-width of the exponent of the floating-point sort.
2406
   * @param sig the bit-width of the significand of the floating-point sort.
2407
   */
2408
  Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const;
2409
2410
  /**
2411
   * Create a datatype sort.
2412
   * @param dtypedecl the datatype declaration from which the sort is created
2413
   * @return the datatype sort
2414
   */
2415
  Sort mkDatatypeSort(const DatatypeDecl& dtypedecl) const;
2416
2417
  /**
2418
   * Create a vector of datatype sorts. The names of the datatype declarations
2419
   * must be distinct.
2420
   *
2421
   * @param dtypedecls the datatype declarations from which the sort is created
2422
   * @return the datatype sorts
2423
   */
2424
  std::vector<Sort> mkDatatypeSorts(
2425
      const std::vector<DatatypeDecl>& dtypedecls) const;
2426
2427
  /**
2428
   * Create a vector of datatype sorts using unresolved sorts. The names of
2429
   * the datatype declarations in dtypedecls must be distinct.
2430
   *
2431
   * This method is called when the DatatypeDecl objects dtypedecls have been
2432
   * built using "unresolved" sorts.
2433
   *
2434
   * We associate each sort in unresolvedSorts with exacly one datatype from
2435
   * dtypedecls. In particular, it must have the same name as exactly one
2436
   * datatype declaration in dtypedecls.
2437
   *
2438
   * When constructing datatypes, unresolved sorts are replaced by the datatype
2439
   * sort constructed for the datatype declaration it is associated with.
2440
   *
2441
   * @param dtypedecls the datatype declarations from which the sort is created
2442
   * @param unresolvedSorts the list of unresolved sorts
2443
   * @return the datatype sorts
2444
   */
2445
  std::vector<Sort> mkDatatypeSorts(
2446
      const std::vector<DatatypeDecl>& dtypedecls,
2447
      const std::set<Sort>& unresolvedSorts) const;
2448
2449
  /**
2450
   * Create function sort.
2451
   * @param domain the sort of the fuction argument
2452
   * @param codomain the sort of the function return value
2453
   * @return the function sort
2454
   */
2455
  Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const;
2456
2457
  /**
2458
   * Create function sort.
2459
   * @param sorts the sort of the function arguments
2460
   * @param codomain the sort of the function return value
2461
   * @return the function sort
2462
   */
2463
  Sort mkFunctionSort(const std::vector<Sort>& sorts,
2464
                      const Sort& codomain) const;
2465
2466
  /**
2467
   * Create a sort parameter.
2468
   * @param symbol the name of the sort
2469
   * @return the sort parameter
2470
   */
2471
  Sort mkParamSort(const std::string& symbol) const;
2472
2473
  /**
2474
   * Create a predicate sort.
2475
   * @param sorts the list of sorts of the predicate
2476
   * @return the predicate sort
2477
   */
2478
  Sort mkPredicateSort(const std::vector<Sort>& sorts) const;
2479
2480
  /**
2481
   * Create a record sort
2482
   * @param fields the list of fields of the record
2483
   * @return the record sort
2484
   */
2485
  Sort mkRecordSort(
2486
      const std::vector<std::pair<std::string, Sort>>& fields) const;
2487
2488
  /**
2489
   * Create a set sort.
2490
   * @param elemSort the sort of the set elements
2491
   * @return the set sort
2492
   */
2493
  Sort mkSetSort(const Sort& elemSort) const;
2494
2495
  /**
2496
   * Create a bag sort.
2497
   * @param elemSort the sort of the bag elements
2498
   * @return the bag sort
2499
   */
2500
  Sort mkBagSort(const Sort& elemSort) const;
2501
2502
  /**
2503
   * Create a sequence sort.
2504
   * @param elemSort the sort of the sequence elements
2505
   * @return the sequence sort
2506
   */
2507
  Sort mkSequenceSort(const Sort& elemSort) const;
2508
2509
  /**
2510
   * Create an uninterpreted sort.
2511
   * @param symbol the name of the sort
2512
   * @return the uninterpreted sort
2513
   */
2514
  Sort mkUninterpretedSort(const std::string& symbol) const;
2515
2516
  /**
2517
   * Create a sort constructor sort.
2518
   * @param symbol the symbol of the sort
2519
   * @param arity the arity of the sort
2520
   * @return the sort constructor sort
2521
   */
2522
  Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const;
2523
2524
  /**
2525
   * Create a tuple sort.
2526
   * @param sorts of the elements of the tuple
2527
   * @return the tuple sort
2528
   */
2529
  Sort mkTupleSort(const std::vector<Sort>& sorts) const;
2530
2531
  /* .................................................................... */
2532
  /* Create Terms                                                         */
2533
  /* .................................................................... */
2534
2535
  /**
2536
   * Create 0-ary term of given kind.
2537
   * @param kind the kind of the term
2538
   * @return the Term
2539
   */
2540
  Term mkTerm(Kind kind) const;
2541
2542
  /**
2543
   * Create a unary term of given kind.
2544
   * @param kind the kind of the term
2545
   * @param child the child of the term
2546
   * @return the Term
2547
   */
2548
  Term mkTerm(Kind kind, const Term& child) const;
2549
2550
  /**
2551
   * Create binary term of given kind.
2552
   * @param kind the kind of the term
2553
   * @param child1 the first child of the term
2554
   * @param child2 the second child of the term
2555
   * @return the Term
2556
   */
2557
  Term mkTerm(Kind kind, const Term& child1, const Term& child2) const;
2558
2559
  /**
2560
   * Create ternary term of given kind.
2561
   * @param kind the kind of the term
2562
   * @param child1 the first child of the term
2563
   * @param child2 the second child of the term
2564
   * @param child3 the third child of the term
2565
   * @return the Term
2566
   */
2567
  Term mkTerm(Kind kind,
2568
              const Term& child1,
2569
              const Term& child2,
2570
              const Term& child3) const;
2571
2572
  /**
2573
   * Create n-ary term of given kind.
2574
   * @param kind the kind of the term
2575
   * @param children the children of the term
2576
   * @return the Term
2577
   */
2578
  Term mkTerm(Kind kind, const std::vector<Term>& children) const;
2579
2580
  /**
2581
   * Create nullary term of given kind from a given operator.
2582
   * Create operators with mkOp().
2583
   * @param the operator
2584
   * @return the Term
2585
   */
2586
  Term mkTerm(const Op& op) const;
2587
2588
  /**
2589
   * Create unary term of given kind from a given operator.
2590
   * Create operators with mkOp().
2591
   * @param the operator
2592
   * @child the child of the term
2593
   * @return the Term
2594
   */
2595
  Term mkTerm(const Op& op, const Term& child) const;
2596
2597
  /**
2598
   * Create binary term of given kind from a given operator.
2599
   * Create operators with mkOp().
2600
   * @param the operator
2601
   * @child1 the first child of the term
2602
   * @child2 the second child of the term
2603
   * @return the Term
2604
   */
2605
  Term mkTerm(const Op& op, const Term& child1, const Term& child2) const;
2606
2607
  /**
2608
   * Create ternary term of given kind from a given operator.
2609
   * Create operators with mkOp().
2610
   * @param the operator
2611
   * @child1 the first child of the term
2612
   * @child2 the second child of the term
2613
   * @child3 the third child of the term
2614
   * @return the Term
2615
   */
2616
  Term mkTerm(const Op& op,
2617
              const Term& child1,
2618
              const Term& child2,
2619
              const Term& child3) const;
2620
2621
  /**
2622
   * Create n-ary term of given kind from a given operator.
2623
   * Create operators with mkOp().
2624
   * @param op the operator
2625
   * @children the children of the term
2626
   * @return the Term
2627
   */
2628
  Term mkTerm(const Op& op, const std::vector<Term>& children) const;
2629
2630
  /**
2631
   * Create a tuple term. Terms are automatically converted if sorts are
2632
   * compatible.
2633
   * @param sorts The sorts of the elements in the tuple
2634
   * @param terms The elements in the tuple
2635
   * @return the tuple Term
2636
   */
2637
  Term mkTuple(const std::vector<Sort>& sorts,
2638
               const std::vector<Term>& terms) const;
2639
2640
  /* .................................................................... */
2641
  /* Create Operators                                                     */
2642
  /* .................................................................... */
2643
2644
  /**
2645
   * Create an operator for a builtin Kind
2646
   * The Kind may not be the Kind for an indexed operator
2647
   *   (e.g. BITVECTOR_EXTRACT)
2648
   * Note: in this case, the Op simply wraps the Kind.
2649
   * The Kind can be used in mkTerm directly without
2650
   *   creating an op first.
2651
   * @param kind the kind to wrap
2652
   */
2653
  Op mkOp(Kind kind) const;
2654
2655
  /**
2656
   * Create operator of kind:
2657
   *   - RECORD_UPDATE
2658
   *   - DIVISIBLE (to support arbitrary precision integers)
2659
   * See enum Kind for a description of the parameters.
2660
   * @param kind the kind of the operator
2661
   * @param arg the string argument to this operator
2662
   */
2663
  Op mkOp(Kind kind, const std::string& arg) const;
2664
2665
  /**
2666
   * Create operator of kind:
2667
   *   - DIVISIBLE
2668
   *   - BITVECTOR_REPEAT
2669
   *   - BITVECTOR_ZERO_EXTEND
2670
   *   - BITVECTOR_SIGN_EXTEND
2671
   *   - BITVECTOR_ROTATE_LEFT
2672
   *   - BITVECTOR_ROTATE_RIGHT
2673
   *   - INT_TO_BITVECTOR
2674
   *   - FLOATINGPOINT_TO_UBV
2675
   *   - FLOATINGPOINT_TO_UBV_TOTAL
2676
   *   - FLOATINGPOINT_TO_SBV
2677
   *   - FLOATINGPOINT_TO_SBV_TOTAL
2678
   *   - TUPLE_UPDATE
2679
   * See enum Kind for a description of the parameters.
2680
   * @param kind the kind of the operator
2681
   * @param arg the uint32_t argument to this operator
2682
   */
2683
  Op mkOp(Kind kind, uint32_t arg) const;
2684
2685
  /**
2686
   * Create operator of Kind:
2687
   *   - BITVECTOR_EXTRACT
2688
   *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
2689
   *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT
2690
   *   - FLOATINGPOINT_TO_FP_REAL
2691
   *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
2692
   *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
2693
   *   - FLOATINGPOINT_TO_FP_GENERIC
2694
   * See enum Kind for a description of the parameters.
2695
   * @param kind the kind of the operator
2696
   * @param arg1 the first uint32_t argument to this operator
2697
   * @param arg2 the second uint32_t argument to this operator
2698
   */
2699
  Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
2700
2701
  /**
2702
   * Create operator of Kind:
2703
   *   - TUPLE_PROJECT
2704
   * See enum Kind for a description of the parameters.
2705
   * @param kind the kind of the operator
2706
   */
2707
  Op mkOp(Kind kind, const std::vector<uint32_t>& args) const;
2708
2709
  /* .................................................................... */
2710
  /* Create Constants                                                     */
2711
  /* .................................................................... */
2712
2713
  /**
2714
   * Create a Boolean true constant.
2715
   * @return the true constant
2716
   */
2717
  Term mkTrue() const;
2718
2719
  /**
2720
   * Create a Boolean false constant.
2721
   * @return the false constant
2722
   */
2723
  Term mkFalse() const;
2724
2725
  /**
2726
   * Create a Boolean constant.
2727
   * @return the Boolean constant
2728
   * @param val the value of the constant
2729
   */
2730
  Term mkBoolean(bool val) const;
2731
2732
  /**
2733
   * Create a constant representing the number Pi.
2734
   * @return a constant representing Pi
2735
   */
2736
  Term mkPi() const;
2737
  /**
2738
   * Create an integer constant from a string.
2739
   * @param s the string representation of the constant, may represent an
2740
   *          integer (e.g., "123").
2741
   * @return a constant of sort Integer assuming 's' represents an integer)
2742
   */
2743
  Term mkInteger(const std::string& s) const;
2744
2745
  /**
2746
   * Create an integer constant from a c++ int.
2747
   * @param val the value of the constant
2748
   * @return a constant of sort Integer
2749
   */
2750
  Term mkInteger(int64_t val) const;
2751
2752
  /**
2753
   * Create a real constant from a string.
2754
   * @param s the string representation of the constant, may represent an
2755
   *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
2756
   * @return a constant of sort Real
2757
   */
2758
  Term mkReal(const std::string& s) const;
2759
2760
  /**
2761
   * Create a real constant from an integer.
2762
   * @param val the value of the constant
2763
   * @return a constant of sort Integer
2764
   */
2765
  Term mkReal(int64_t val) const;
2766
2767
  /**
2768
   * Create a real constant from a rational.
2769
   * @param num the value of the numerator
2770
   * @param den the value of the denominator
2771
   * @return a constant of sort Real
2772
   */
2773
  Term mkReal(int64_t num, int64_t den) const;
2774
2775
  /**
2776
   * Create a regular expression empty term.
2777
   * @return the empty term
2778
   */
2779
  Term mkRegexpEmpty() const;
2780
2781
  /**
2782
   * Create a regular expression sigma term.
2783
   * @return the sigma term
2784
   */
2785
  Term mkRegexpSigma() const;
2786
2787
  /**
2788
   * Create a constant representing an empty set of the given sort.
2789
   * @param sort the sort of the set elements.
2790
   * @return the empty set constant
2791
   */
2792
  Term mkEmptySet(const Sort& sort) const;
2793
2794
  /**
2795
   * Create a constant representing an empty bag of the given sort.
2796
   * @param sort the sort of the bag elements.
2797
   * @return the empty bag constant
2798
   */
2799
  Term mkEmptyBag(const Sort& sort) const;
2800
2801
  /**
2802
   * Create a separation logic nil term.
2803
   * @param sort the sort of the nil term
2804
   * @return the separation logic nil term
2805
   */
2806
  Term mkSepNil(const Sort& sort) const;
2807
2808
  /**
2809
   * Create a String constant.
2810
   * @param s the string this constant represents
2811
   * @param useEscSequences determines whether escape sequences in \p s should
2812
   * be converted to the corresponding character
2813
   * @return the String constant
2814
   */
2815
  Term mkString(const std::string& s, bool useEscSequences = false) const;
2816
2817
  /**
2818
   * Create a String constant.
2819
   * @param c the character this constant represents
2820
   * @return the String constant
2821
   */
2822
  Term mkString(const unsigned char c) const;
2823
2824
  /**
2825
   * Create a String constant.
2826
   * @param s a list of unsigned (unicode) values this constant represents as
2827
   * string
2828
   * @return the String constant
2829
   */
2830
  Term mkString(const std::vector<uint32_t>& s) const;
2831
2832
  /**
2833
   * Create a character constant from a given string.
2834
   * @param s the string denoting the code point of the character (in base 16)
2835
   * @return the character constant
2836
   */
2837
  Term mkChar(const std::string& s) const;
2838
2839
  /**
2840
   * Create an empty sequence of the given element sort.
2841
   * @param sort The element sort of the sequence.
2842
   * @return the empty sequence with given element sort.
2843
   */
2844
  Term mkEmptySequence(const Sort& sort) const;
2845
2846
  /**
2847
   * Create a universe set of the given sort.
2848
   * @param sort the sort of the set elements
2849
   * @return the universe set constant
2850
   */
2851
  Term mkUniverseSet(const Sort& sort) const;
2852
2853
  /**
2854
   * Create a bit-vector constant of given size and value.
2855
   * @param size the bit-width of the bit-vector sort
2856
   * @param val the value of the constant
2857
   * @return the bit-vector constant
2858
   */
2859
  Term mkBitVector(uint32_t size, uint64_t val = 0) const;
2860
2861
  /**
2862
   * Create a bit-vector constant from a given string of base 2, 10 or 16.
2863
   *
2864
   * The size of resulting bit-vector is
2865
   * - base  2: the size of the binary string
2866
   * - base 10: the min. size required to represent the decimal as a bit-vector
2867
   * - base 16: the max. size required to represent the hexadecimal as a
2868
   *            bit-vector (4 * size of the given value string)
2869
   *
2870
   * @param s the string representation of the constant
2871
   * @param base the base of the string representation (2, 10, or 16)
2872
   * @return the bit-vector constant
2873
   */
2874
  Term mkBitVector(const std::string& s, uint32_t base = 2) const;
2875
2876
  /**
2877
   * Create a bit-vector constant of a given bit-width from a given string of
2878
   * base 2, 10 or 16.
2879
   * @param size the bit-width of the constant
2880
   * @param s the string representation of the constant
2881
   * @param base the base of the string representation (2, 10, or 16)
2882
   * @return the bit-vector constant
2883
   */
2884
  Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const;
2885
2886
  /**
2887
   * Create a constant array with the provided constant value stored at every
2888
   * index
2889
   * @param sort the sort of the constant array (must be an array sort)
2890
   * @param val the constant value to store (must match the sort's element sort)
2891
   * @return the constant array term
2892
   */
2893
  Term mkConstArray(const Sort& sort, const Term& val) const;
2894
2895
  /**
2896
   * Create a positive infinity floating-point constant. Requires CVC4 to be
2897
   * compiled with SymFPU support.
2898
   * @param exp Number of bits in the exponent
2899
   * @param sig Number of bits in the significand
2900
   * @return the floating-point constant
2901
   */
2902
  Term mkPosInf(uint32_t exp, uint32_t sig) const;
2903
2904
  /**
2905
   * Create a negative infinity floating-point constant. Requires CVC4 to be
2906
   * compiled with SymFPU support.
2907
   * @param exp Number of bits in the exponent
2908
   * @param sig Number of bits in the significand
2909
   * @return the floating-point constant
2910
   */
2911
  Term mkNegInf(uint32_t exp, uint32_t sig) const;
2912
2913
  /**
2914
   * Create a not-a-number (NaN) floating-point constant. Requires CVC4 to be
2915
   * compiled with SymFPU support.
2916
   * @param exp Number of bits in the exponent
2917
   * @param sig Number of bits in the significand
2918
   * @return the floating-point constant
2919
   */
2920
  Term mkNaN(uint32_t exp, uint32_t sig) const;
2921
2922
  /**
2923
   * Create a positive zero (+0.0) floating-point constant. Requires CVC4 to be
2924
   * compiled with SymFPU support.
2925
   * @param exp Number of bits in the exponent
2926
   * @param sig Number of bits in the significand
2927
   * @return the floating-point constant
2928
   */
2929
  Term mkPosZero(uint32_t exp, uint32_t sig) const;
2930
2931
  /**
2932
   * Create a negative zero (-0.0) floating-point constant. Requires CVC4 to be
2933
   * compiled with SymFPU support.
2934
   * @param exp Number of bits in the exponent
2935
   * @param sig Number of bits in the significand
2936
   * @return the floating-point constant
2937
   */
2938
  Term mkNegZero(uint32_t exp, uint32_t sig) const;
2939
2940
  /**
2941
   * Create a roundingmode constant.
2942
   * @param rm the floating point rounding mode this constant represents
2943
   */
2944
  Term mkRoundingMode(RoundingMode rm) const;
2945
2946
  /**
2947
   * Create uninterpreted constant.
2948
   * @param arg1 Sort of the constant
2949
   * @param arg2 Index of the constant
2950
   */
2951
  Term mkUninterpretedConst(const Sort& sort, int32_t index) const;
2952
2953
  /**
2954
   * Create an abstract value constant.
2955
   * @param index Index of the abstract value
2956
   */
2957
  Term mkAbstractValue(const std::string& index) const;
2958
2959
  /**
2960
   * Create an abstract value constant.
2961
   * @param index Index of the abstract value
2962
   */
2963
  Term mkAbstractValue(uint64_t index) const;
2964
2965
  /**
2966
   * Create a floating-point constant (requires CVC4 to be compiled with symFPU
2967
   * support).
2968
   * @param exp Size of the exponent
2969
   * @param sig Size of the significand
2970
   * @param val Value of the floating-point constant as a bit-vector term
2971
   */
2972
  Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const;
2973
2974
  /* .................................................................... */
2975
  /* Create Variables                                                     */
2976
  /* .................................................................... */
2977
2978
  /**
2979
   * Create (first-order) constant (0-arity function symbol).
2980
   * SMT-LIB: ( declare-const <symbol> <sort> )
2981
   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
2982
   *
2983
   * @param sort the sort of the constant
2984
   * @param symbol the name of the constant
2985
   * @return the first-order constant
2986
   */
2987
  Term mkConst(const Sort& sort, const std::string& symbol) const;
2988
  /**
2989
   * Create (first-order) constant (0-arity function symbol), with a default
2990
   * symbol name.
2991
   *
2992
   * @param sort the sort of the constant
2993
   * @return the first-order constant
2994
   */
2995
  Term mkConst(const Sort& sort) const;
2996
2997
  /**
2998
   * Create a bound variable to be used in a binder (i.e. a quantifier, a
2999
   * lambda, or a witness binder).
3000
   * @param sort the sort of the variable
3001
   * @param symbol the name of the variable
3002
   * @return the variable
3003
   */
3004
  Term mkVar(const Sort& sort, const std::string& symbol = std::string()) const;
3005
3006
  /* .................................................................... */
3007
  /* Create datatype constructor declarations                             */
3008
  /* .................................................................... */
3009
3010
  DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
3011
3012
  /* .................................................................... */
3013
  /* Create datatype declarations                                         */
3014
  /* .................................................................... */
3015
3016
  /**
3017
   * Create a datatype declaration.
3018
   * @param name the name of the datatype
3019
   * @param isCoDatatype true if a codatatype is to be constructed
3020
   * @return the DatatypeDecl
3021
   */
3022
  DatatypeDecl mkDatatypeDecl(const std::string& name,
3023
                              bool isCoDatatype = false);
3024
3025
  /**
3026
   * Create a datatype declaration.
3027
   * Create sorts parameter with Solver::mkParamSort().
3028
   * @param name the name of the datatype
3029
   * @param param the sort parameter
3030
   * @param isCoDatatype true if a codatatype is to be constructed
3031
   * @return the DatatypeDecl
3032
   */
3033
  DatatypeDecl mkDatatypeDecl(const std::string& name,
3034
                              Sort param,
3035
                              bool isCoDatatype = false);
3036
3037
  /**
3038
   * Create a datatype declaration.
3039
   * Create sorts parameter with Solver::mkParamSort().
3040
   * @param name the name of the datatype
3041
   * @param params a list of sort parameters
3042
   * @param isCoDatatype true if a codatatype is to be constructed
3043
   * @return the DatatypeDecl
3044
   */
3045
  DatatypeDecl mkDatatypeDecl(const std::string& name,
3046
                              const std::vector<Sort>& params,
3047
                              bool isCoDatatype = false);
3048
3049
  /* .................................................................... */
3050
  /* Formula Handling                                                     */
3051
  /* .................................................................... */
3052
3053
  /**
3054
   * Simplify a formula without doing "much" work.  Does not involve
3055
   * the SAT Engine in the simplification, but uses the current
3056
   * definitions, assertions, and the current partial model, if one
3057
   * has been constructed.  It also involves theory normalization.
3058
   * @param t the formula to simplify
3059
   * @return the simplified formula
3060
   */
3061
  Term simplify(const Term& t);
3062
3063
  /**
3064
   * Assert a formula.
3065
   * SMT-LIB: ( assert <term> )
3066
   * @param term the formula to assert
3067
   */
3068
  void assertFormula(const Term& term) const;
3069
3070
  /**
3071
   * Check satisfiability.
3072
   * SMT-LIB: ( check-sat )
3073
   * @return the result of the satisfiability check.
3074
   */
3075
  Result checkSat() const;
3076
3077
  /**
3078
   * Check satisfiability assuming the given formula.
3079
   * SMT-LIB: ( check-sat-assuming ( <prop_literal> ) )
3080
   * @param assumption the formula to assume
3081
   * @return the result of the satisfiability check.
3082
   */
3083
  Result checkSatAssuming(const Term& assumption) const;
3084
3085
  /**
3086
   * Check satisfiability assuming the given formulas.
3087
   * SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) )
3088
   * @param assumptions the formulas to assume
3089
   * @return the result of the satisfiability check.
3090
   */
3091
  Result checkSatAssuming(const std::vector<Term>& assumptions) const;
3092
3093
  /**
3094
   * Check entailment of the given formula w.r.t. the current set of assertions.
3095
   * @param term the formula to check entailment for
3096
   * @return the result of the entailment check.
3097
   */
3098
  Result checkEntailed(const Term& term) const;
3099
3100
  /**
3101
   * Check entailment of the given set of given formulas w.r.t. the current
3102
   * set of assertions.
3103
   * @param terms the terms to check entailment for
3104
   * @return the result of the entailmentcheck.
3105
   */
3106
  Result checkEntailed(const std::vector<Term>& terms) const;
3107
3108
  /**
3109
   * Create datatype sort.
3110
   * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
3111
   * @param symbol the name of the datatype sort
3112
   * @param ctors the constructor declarations of the datatype sort
3113
   * @return the datatype sort
3114
   */
3115
  Sort declareDatatype(const std::string& symbol,
3116
                       const std::vector<DatatypeConstructorDecl>& ctors) const;
3117
3118
  /**
3119
   * Declare n-ary function symbol.
3120
   * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
3121
   * @param symbol the name of the function
3122
   * @param sorts the sorts of the parameters to this function
3123
   * @param sort the sort of the return value of this function
3124
   * @return the function
3125
   */
3126
  Term declareFun(const std::string& symbol,
3127
                  const std::vector<Sort>& sorts,
3128
                  const Sort& sort) const;
3129
3130
  /**
3131
   * Declare uninterpreted sort.
3132
   * SMT-LIB: ( declare-sort <symbol> <numeral> )
3133
   * @param symbol the name of the sort
3134
   * @param arity the arity of the sort
3135
   * @return the sort
3136
   */
3137
  Sort declareSort(const std::string& symbol, uint32_t arity) const;
3138
3139
  /**
3140
   * Define n-ary function.
3141
   * SMT-LIB: ( define-fun <function_def> )
3142
   * @param symbol the name of the function
3143
   * @param bound_vars the parameters to this function
3144
   * @param sort the sort of the return value of this function
3145
   * @param term the function body
3146
   * @param global determines whether this definition is global (i.e. persists
3147
   *               when popping the context)
3148
   * @return the function
3149
   */
3150
  Term defineFun(const std::string& symbol,
3151
                 const std::vector<Term>& bound_vars,
3152
                 const Sort& sort,
3153
                 const Term& term,
3154
                 bool global = false) const;
3155
  /**
3156
   * Define n-ary function.
3157
   * SMT-LIB: ( define-fun <function_def> )
3158
   * Create parameter 'fun' with mkConst().
3159
   * @param fun the sorted function
3160
   * @param bound_vars the parameters to this function
3161
   * @param term the function body
3162
   * @param global determines whether this definition is global (i.e. persists
3163
   *               when popping the context)
3164
   * @return the function
3165
   */
3166
  Term defineFun(const Term& fun,
3167
                 const std::vector<Term>& bound_vars,
3168
                 const Term& term,
3169
                 bool global = false) const;
3170
3171
  /**
3172
   * Define recursive function.
3173
   * SMT-LIB: ( define-fun-rec <function_def> )
3174
   * @param symbol the name of the function
3175
   * @param bound_vars the parameters to this function
3176
   * @param sort the sort of the return value of this function
3177
   * @param term the function body
3178
   * @param global determines whether this definition is global (i.e. persists
3179
   *               when popping the context)
3180
   * @return the function
3181
   */
3182
  Term defineFunRec(const std::string& symbol,
3183
                    const std::vector<Term>& bound_vars,
3184
                    const Sort& sort,
3185
                    const Term& term,
3186
                    bool global = false) const;
3187
3188
  /**
3189
   * Define recursive function.
3190
   * SMT-LIB: ( define-fun-rec <function_def> )
3191
   * Create parameter 'fun' with mkConst().
3192
   * @param fun the sorted function
3193
   * @param bound_vars the parameters to this function
3194
   * @param term the function body
3195
   * @param global determines whether this definition is global (i.e. persists
3196
   *               when popping the context)
3197
   * @return the function
3198
   */
3199
  Term defineFunRec(const Term& fun,
3200
                    const std::vector<Term>& bound_vars,
3201
                    const Term& term,
3202
                    bool global = false) const;
3203
3204
  /**
3205
   * Define recursive functions.
3206
   * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3207
   * Create elements of parameter 'funs' with mkConst().
3208
   * @param funs the sorted functions
3209
   * @param bound_vars the list of parameters to the functions
3210
   * @param term the list of function bodies of the functions
3211
   * @param global determines whether this definition is global (i.e. persists
3212
   *               when popping the context)
3213
   * @return the function
3214
   */
3215
  void defineFunsRec(const std::vector<Term>& funs,
3216
                     const std::vector<std::vector<Term>>& bound_vars,
3217
                     const std::vector<Term>& terms,
3218
                     bool global = false) const;
3219
3220
  /**
3221
   * Echo a given string to the given output stream.
3222
   * SMT-LIB: ( echo <std::string> )
3223
   * @param out the output stream
3224
   * @param str the string to echo
3225
   */
3226
  void echo(std::ostream& out, const std::string& str) const;
3227
3228
  /**
3229
   * Get the list of asserted formulas.
3230
   * SMT-LIB: ( get-assertions )
3231
   * @return the list of asserted formulas
3232
   */
3233
  std::vector<Term> getAssertions() const;
3234
3235
  /**
3236
   * Get info from the solver.
3237
   * SMT-LIB: ( get-info <info_flag> )
3238
   * @return the info
3239
   */
3240
  std::string getInfo(const std::string& flag) const;
3241
3242
  /**
3243
   * Get the value of a given option.
3244
   * SMT-LIB: ( get-option <keyword> )
3245
   * @param option the option for which the value is queried
3246
   * @return a string representation of the option value
3247
   */
3248
  std::string getOption(const std::string& option) const;
3249
3250
  /**
3251
   * Get the set of unsat ("failed") assumptions.
3252
   * SMT-LIB: ( get-unsat-assumptions )
3253
   * Requires to enable option 'produce-unsat-assumptions'.
3254
   * @return the set of unsat assumptions.
3255
   */
3256
  std::vector<Term> getUnsatAssumptions() const;
3257
3258
  /**
3259
   * Get the unsatisfiable core.
3260
   * SMT-LIB: ( get-unsat-core )
3261
   * Requires to enable option 'produce-unsat-cores'.
3262
   * @return a set of terms representing the unsatisfiable core
3263
   */
3264
  std::vector<Term> getUnsatCore() const;
3265
3266
  /**
3267
   * Get the value of the given term.
3268
   * SMT-LIB: ( get-value ( <term> ) )
3269
   * @param term the term for which the value is queried
3270
   * @return the value of the given term
3271
   */
3272
  Term getValue(const Term& term) const;
3273
  /**
3274
   * Get the values of the given terms.
3275
   * SMT-LIB: ( get-value ( <term>+ ) )
3276
   * @param terms the terms for which the value is queried
3277
   * @return the values of the given terms
3278
   */
3279
  std::vector<Term> getValue(const std::vector<Term>& terms) const;
3280
3281
  /**
3282
   * Do quantifier elimination.
3283
   * SMT-LIB: ( get-qe <q> )
3284
   * Requires a logic that supports quantifier elimination. Currently, the only
3285
   * logics supported by quantifier elimination is LRA and LIA.
3286
   * @param q a quantified formula of the form:
3287
   *   Q x1...xn. P( x1...xn, y1...yn )
3288
   * where P( x1...xn, y1...yn ) is a quantifier-free formula
3289
   * @return a formula ret such that, given the current set of formulas A
3290
   * asserted to this solver:
3291
   *   - ( A ^ q ) and ( A ^ ret ) are equivalent
3292
   *   - ret is quantifier-free formula containing only free variables in
3293
   *     y1...yn.
3294
   */
3295
  Term getQuantifierElimination(const Term& q) const;
3296
3297
  /**
3298
   * Do partial quantifier elimination, which can be used for incrementally
3299
   * computing the result of a quantifier elimination.
3300
   * SMT-LIB: ( get-qe-disjunct <q> )
3301
   * Requires a logic that supports quantifier elimination. Currently, the only
3302
   * logics supported by quantifier elimination is LRA and LIA.
3303
   * @param q a quantified formula of the form:
3304
   *   Q x1...xn. P( x1...xn, y1...yn )
3305
   * where P( x1...xn, y1...yn ) is a quantifier-free formula
3306
   * @return a formula ret such that, given the current set of formulas A
3307
   * asserted to this solver:
3308
   *   - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
3309
   *     exists,
3310
   *   - ret is quantifier-free formula containing only free variables in
3311
   *     y1...yn,
3312
   *   - If Q is exists, let A^Q_n be the formula
3313
   *       A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
3314
   *     where for each i=1,...n, formula ret^Q_i is the result of calling
3315
   *     getQuantifierEliminationDisjunct for q with the set of assertions
3316
   *     A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
3317
   *       A ^ ret^Q_1 ^ ... ^ ret^Q_n
3318
   *     where ret^Q_i is the same as above. In either case, we have
3319
   *     that ret^Q_j will eventually be true or false, for some finite j.
3320
   */
3321
  Term getQuantifierEliminationDisjunct(const Term& q) const;
3322
3323
  /**
3324
   * When using separation logic, this sets the location sort and the
3325
   * datatype sort to the given ones. This method should be invoked exactly
3326
   * once, before any separation logic constraints are provided.
3327
   * @param locSort The location sort of the heap
3328
   * @param dataSort The data sort of the heap
3329
   */
3330
  void declareSeparationHeap(const Sort& locSort, const Sort& dataSort) const;
3331
3332
  /**
3333
   * When using separation logic, obtain the term for the heap.
3334
   * @return The term for the heap
3335
   */
3336
  Term getSeparationHeap() const;
3337
3338
  /**
3339
   * When using separation logic, obtain the term for nil.
3340
   * @return The term for nil
3341
   */
3342
  Term getSeparationNilTerm() const;
3343
3344
  /**
3345
   * Pop (a) level(s) from the assertion stack.
3346
   * SMT-LIB: ( pop <numeral> )
3347
   * @param nscopes the number of levels to pop
3348
   */
3349
  void pop(uint32_t nscopes = 1) const;
3350
3351
  /**
3352
   * Get an interpolant
3353
   * SMT-LIB: ( get-interpol <conj> )
3354
   * Requires to enable option 'produce-interpols'.
3355
   * @param conj the conjecture term
3356
   * @param output a Term I such that A->I and I->B are valid, where A is the
3357
   *        current set of assertions and B is given in the input by conj.
3358
   * @return true if it gets I successfully, false otherwise.
3359
   */
3360
  bool getInterpolant(const Term& conj, Term& output) const;
3361
3362
  /**
3363
   * Get an interpolant
3364
   * SMT-LIB: ( get-interpol <conj> <g> )
3365
   * Requires to enable option 'produce-interpols'.
3366
   * @param conj the conjecture term
3367
   * @param grammar the grammar for the interpolant I
3368
   * @param output a Term I such that A->I and I->B are valid, where A is the
3369
   *        current set of assertions and B is given in the input by conj.
3370
   * @return true if it gets I successfully, false otherwise.
3371
   */
3372
  bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const;
3373
3374
  /**
3375
   * Get an abduct.
3376
   * SMT-LIB: ( get-abduct <conj> )
3377
   * Requires enabling option 'produce-abducts'
3378
   * @param conj the conjecture term
3379
   * @param output a term C such that A^C is satisfiable, and A^~B^C is
3380
   *        unsatisfiable, where A is the current set of assertions and B is
3381
   *        given in the input by conj
3382
   * @return true if it gets C successfully, false otherwise
3383
   */
3384
  bool getAbduct(const Term& conj, Term& output) const;
3385
3386
  /**
3387
   * Get an abduct.
3388
   * SMT-LIB: ( get-abduct <conj> <g> )
3389
   * Requires enabling option 'produce-abducts'
3390
   * @param conj the conjecture term
3391
   * @param grammar the grammar for the abduct C
3392
   * @param output a term C such that A^C is satisfiable, and A^~B^C is
3393
   *        unsatisfiable, where A is the current set of assertions and B is
3394
   *        given in the input by conj
3395
   * @return true if it gets C successfully, false otherwise
3396
   */
3397
  bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
3398
3399
  /**
3400
   * Block the current model. Can be called only if immediately preceded by a
3401
   * SAT or INVALID query.
3402
   * SMT-LIB: ( block-model )
3403
   * Requires enabling 'produce-models' option and setting 'block-models' option
3404
   * to a mode other than "none".
3405
   */
3406
  void blockModel() const;
3407
3408
  /**
3409
   * Block the current model values of (at least) the values in terms. Can be
3410
   * called only if immediately preceded by a SAT or NOT_ENTAILED query.
3411
   * SMT-LIB: ( block-model-values ( <terms>+ ) )
3412
   * Requires enabling 'produce-models' option and setting 'block-models' option
3413
   * to a mode other than "none".
3414
   */
3415
  void blockModelValues(const std::vector<Term>& terms) const;
3416
3417
  /**
3418
   * Print all instantiations made by the quantifiers module.
3419
   * @param out the output stream
3420
   */
3421
  void printInstantiations(std::ostream& out) const;
3422
3423
  /**
3424
   * Push (a) level(s) to the assertion stack.
3425
   * SMT-LIB: ( push <numeral> )
3426
   * @param nscopes the number of levels to push
3427
   */
3428
  void push(uint32_t nscopes = 1) const;
3429
3430
  /**
3431
   * Remove all assertions.
3432
   * SMT-LIB: ( reset-assertions )
3433
   */
3434
  void resetAssertions() const;
3435
3436
  /**
3437
   * Set info.
3438
   * SMT-LIB: ( set-info <attribute> )
3439
   * @param keyword the info flag
3440
   * @param value the value of the info flag
3441
   */
3442
  void setInfo(const std::string& keyword, const std::string& value) const;
3443
3444
  /**
3445
   * Set logic.
3446
   * SMT-LIB: ( set-logic <symbol> )
3447
   * @param logic the logic to set
3448
   */
3449
  void setLogic(const std::string& logic) const;
3450
3451
  /**
3452
   * Set option.
3453
   * SMT-LIB: ( set-option <option> )
3454
   * @param option the option name
3455
   * @param value the option value
3456
   */
3457
  void setOption(const std::string& option, const std::string& value) const;
3458
3459
  /**
3460
   * If needed, convert this term to a given sort. Note that the sort of the
3461
   * term must be convertible into the target sort. Currently only Int to Real
3462
   * conversions are supported.
3463
   * @param s the target sort
3464
   * @return the term wrapped into a sort conversion if needed
3465
   */
3466
  Term ensureTermSort(const Term& t, const Sort& s) const;
3467
3468
  /**
3469
   * Append <symbol> to the current list of universal variables.
3470
   * SyGuS v2: ( declare-var <symbol> <sort> )
3471
   * @param sort the sort of the universal variable
3472
   * @param symbol the name of the universal variable
3473
   * @return the universal variable
3474
   */
3475
  Term mkSygusVar(const Sort& sort,
3476
                  const std::string& symbol = std::string()) const;
3477
3478
  /**
3479
   * Create a Sygus grammar. The first non-terminal is treated as the starting
3480
   * non-terminal, so the order of non-terminals matters.
3481
   *
3482
   * @param boundVars the parameters to corresponding synth-fun/synth-inv
3483
   * @param ntSymbols the pre-declaration of the non-terminal symbols
3484
   * @return the grammar
3485
   */
3486
  Grammar mkSygusGrammar(const std::vector<Term>& boundVars,
3487
                         const std::vector<Term>& ntSymbols) const;
3488
3489
  /**
3490
   * Synthesize n-ary function.
3491
   * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> )
3492
   * @param symbol the name of the function
3493
   * @param boundVars the parameters to this function
3494
   * @param sort the sort of the return value of this function
3495
   * @return the function
3496
   */
3497
  Term synthFun(const std::string& symbol,
3498
                const std::vector<Term>& boundVars,
3499
                const Sort& sort) const;
3500
3501
  /**
3502
   * Synthesize n-ary function following specified syntactic constraints.
3503
   * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
3504
   * @param symbol the name of the function
3505
   * @param boundVars the parameters to this function
3506
   * @param sort the sort of the return value of this function
3507
   * @param grammar the syntactic constraints
3508
   * @return the function
3509
   */
3510
  Term synthFun(const std::string& symbol,
3511
                const std::vector<Term>& boundVars,
3512
                Sort sort,
3513
                Grammar& grammar) const;
3514
3515
  /**
3516
   * Synthesize invariant.
3517
   * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) )
3518
   * @param symbol the name of the invariant
3519
   * @param boundVars the parameters to this invariant
3520
   * @param sort the sort of the return value of this invariant
3521
   * @return the invariant
3522
   */
3523
  Term synthInv(const std::string& symbol,
3524
                const std::vector<Term>& boundVars) const;
3525
3526
  /**
3527
   * Synthesize invariant following specified syntactic constraints.
3528
   * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) <g> )
3529
   * @param symbol the name of the invariant
3530
   * @param boundVars the parameters to this invariant
3531
   * @param sort the sort of the return value of this invariant
3532
   * @param grammar the syntactic constraints
3533
   * @return the invariant
3534
   */
3535
  Term synthInv(const std::string& symbol,
3536
                const std::vector<Term>& boundVars,
3537
                Grammar& grammar) const;
3538
3539
  /**
3540
   * Add a forumla to the set of Sygus constraints.
3541
   * SyGuS v2: ( constraint <term> )
3542
   * @param term the formula to add as a constraint
3543
   */
3544
  void addSygusConstraint(const Term& term) const;
3545
3546
  /**
3547
   * Add a set of Sygus constraints to the current state that correspond to an
3548
   * invariant synthesis problem.
3549
   * SyGuS v2: ( inv-constraint <inv> <pre> <trans> <post> )
3550
   * @param inv the function-to-synthesize
3551
   * @param pre the pre-condition
3552
   * @param trans the transition relation
3553
   * @param post the post-condition
3554
   */
3555
  void addSygusInvConstraint(Term inv, Term pre, Term trans, Term post) const;
3556
3557
  /**
3558
   * Try to find a solution for the synthesis conjecture corresponding to the
3559
   * current list of functions-to-synthesize, universal variables and
3560
   * constraints.
3561
   * SyGuS v2: ( check-synth )
3562
   * @return the result of the synthesis conjecture.
3563
   */
3564
  Result checkSynth() const;
3565
3566
  /**
3567
   * Get the synthesis solution of the given term. This method should be called
3568
   * immediately after the solver answers unsat for sygus input.
3569
   * @param term the term for which the synthesis solution is queried
3570
   * @return the synthesis solution of the given term
3571
   */
3572
  Term getSynthSolution(Term term) const;
3573
3574
  /**
3575
   * Get the synthesis solutions of the given terms. This method should be
3576
   * called immediately after the solver answers unsat for sygus input.
3577
   * @param terms the terms for which the synthesis solutions is queried
3578
   * @return the synthesis solutions of the given terms
3579
   */
3580
  std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
3581
3582
  /**
3583
   * Print solution for synthesis conjecture to the given output stream.
3584
   * @param out the output stream
3585
   */
3586
  void printSynthSolution(std::ostream& out) const;
3587
3588
3589
  // !!! This is only temporarily available until the parser is fully migrated
3590
  // to the new API. !!!
3591
  SmtEngine* getSmtEngine(void) const;
3592
3593
  // !!! This is only temporarily available until options are refactored at
3594
  // the driver level. !!!
3595
  Options& getOptions(void);
3596
3597
 private:
3598
  /** @return the node manager of this solver */
3599
  NodeManager* getNodeManager(void) const;
3600
3601
  /** Helper to check for API misuse in mkOp functions. */
3602
  void checkMkTerm(Kind kind, uint32_t nchildren) const;
3603
  /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
3604
  template <typename T>
3605
  Term mkValHelper(T t) const;
3606
  /** Helper for mkReal functions that take a string as argument. */
3607
  Term mkRealFromStrHelper(const std::string& s) const;
3608
  /** Helper for mkBitVector functions that take a string as argument. */
3609
  Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
3610
  /**
3611
   * Helper for mkBitVector functions that take a string and a size as
3612
   * arguments.
3613
   */
3614
  Term mkBVFromStrHelper(uint32_t size,
3615
                         const std::string& s,
3616
                         uint32_t base) const;
3617
  /** Helper for mkBitVector functions that take an integer as argument. */
3618
  Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
3619
  /** Helper for functions that create tuple sorts. */
3620
  Sort mkTupleSortHelper(const std::vector<Sort>& sorts) const;
3621
  /** Helper for mkTerm functions that create Term from a Kind */
3622
  Term mkTermFromKind(Kind kind) const;
3623
  /** Helper for mkChar functions that take a string as argument. */
3624
  Term mkCharFromStrHelper(const std::string& s) const;
3625
  /** Get value helper, which accounts for subtyping */
3626
  Term getValueHelper(const Term& term) const;
3627
3628
  /**
3629
   * Helper function that ensures that a given term is of sort real (as opposed
3630
   * to being of sort integer).
3631
   * @param t a term of sort integer or real
3632
   * @return a term of sort real
3633
   */
3634
  Term ensureRealSort(const Term& t) const;
3635
3636
  /**
3637
   * Create n-ary term of given kind. This handles the cases of left/right
3638
   * associative operators, chainable operators, and cases when the number of
3639
   * children exceeds the maximum arity for the kind.
3640
   * @param kind the kind of the term
3641
   * @param children the children of the term
3642
   * @return the Term
3643
   */
3644
  Term mkTermHelper(Kind kind, const std::vector<Term>& children) const;
3645
3646
  /**
3647
   * Create n-ary term of given kind from a given operator.
3648
   * @param op the operator
3649
   * @param children the children of the term
3650
   * @return the Term
3651
   */
3652
  Term mkTermHelper(const Op& op, const std::vector<Term>& children) const;
3653
3654
  /**
3655
   * Create a vector of datatype sorts, using unresolved sorts.
3656
   * @param dtypedecls the datatype declarations from which the sort is created
3657
   * @param unresolvedSorts the list of unresolved sorts
3658
   * @return the datatype sorts
3659
   */
3660
  std::vector<Sort> mkDatatypeSortsInternal(
3661
      const std::vector<DatatypeDecl>& dtypedecls,
3662
      const std::set<Sort>& unresolvedSorts) const;
3663
3664
  /**
3665
   * Synthesize n-ary function following specified syntactic constraints.
3666
   * SMT-LIB: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
3667
   * @param symbol the name of the function
3668
   * @param boundVars the parameters to this function
3669
   * @param sort the sort of the return value of this function
3670
   * @param isInv determines whether this is synth-fun or synth-inv
3671
   * @param g the syntactic constraints
3672
   * @return the function
3673
   */
3674
  Term synthFunHelper(const std::string& symbol,
3675
                      const std::vector<Term>& boundVars,
3676
                      const Sort& sort,
3677
                      bool isInv = false,
3678
                      Grammar* grammar = nullptr) const;
3679
3680
  /** Check whether string s is a valid decimal integer. */
3681
  bool isValidInteger(const std::string& s) const;
3682
3683
  /** Increment the term stats counter. */
3684
  void increment_term_stats(Kind kind) const;
3685
  /** Increment the vars stats (if 'is_var') or consts stats counter. */
3686
  void increment_vars_consts_stats(const Sort& sort, bool is_var) const;
3687
3688
  /** The node manager of this solver. */
3689
  std::unique_ptr<NodeManager> d_nodeMgr;
3690
  /** The statistics collected on the Api level. */
3691
  std::unique_ptr<Statistics> d_stats;
3692
  /** The SMT engine of this solver. */
3693
  std::unique_ptr<SmtEngine> d_smtEngine;
3694
  /** The random number generator of this solver. */
3695
  std::unique_ptr<Random> d_rng;
3696
};
3697
3698
}  // namespace api
3699
}  // namespace CVC4
3700
#endif