src/api/cpp/cvc5.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The cvc5 C++ API.
  14  */
  15
  16 #include "cvc5_export.h"
  17
  18 #ifndef CVC5__API__CVC5_H
  19 #define CVC5__API__CVC5_H
  20
  21 #include <map>
  22 #include <memory>
  23 #include <optional>
  24 #include <set>
  25 #include <sstream>
  26 #include <string>
  27 #include <unordered_map>
  28 #include <unordered_set>
  29 #include <variant>
  30 #include <vector>
  31
  32 #include "api/cpp/cvc5_kind.h"
  33
  34 namespace cvc5 {
  35
  36 #ifndef DOXYGEN_SKIP
  37 template <bool ref_count>
  38 class NodeTemplate;
  39 typedef NodeTemplate<true> Node;
  40 #endif
  41
  42 class Command;
  43 class DType;
  44 class DTypeConstructor;
  45 class DTypeSelector;
  46 class NodeManager;
  47 class SolverEngine;
  48 class TypeNode;
  49 class Options;
  50 class Random;
  51 class Result;
  52 class StatisticsRegistry;
  53
  54 namespace main {
  55 class CommandExecutor;
  56 }
  57
  58 namespace api {
  59
  60 class Solver;
  61 class Statistics;
  62 struct APIStatistics;
  63
  64 /* -------------------------------------------------------------------------- */
  65 /* Exception                                                                  */
  66 /* -------------------------------------------------------------------------- */
  67
  68 /**
  69  * Base class for all API exceptions.
  70  * If thrown, all API objects may be in an unsafe state.
  71  */
  72 class CVC5_EXPORT CVC5ApiException : public std::exception
  73 {
  74  public:
  75   /**
  76    * Construct with message from a string.
  77    * @param str The error message.
  78    */
  79   CVC5ApiException(const std::string& str) : d_msg(str) {}
  80   /**
  81    * Construct with message from a string stream.
  82    * @param stream The error message.
  83    */
  84   CVC5ApiException(const std::stringstream& stream) : d_msg(stream.str()) {}
  85   /**
  86    * Retrieve the message from this exception.
  87    * @return The error message.
  88    */
  89   const std::string& getMessage() const { return d_msg; }
  90   /**
  91    * Retrieve the message as a C-style array.
  92    * @return The error message.
  93    */
  94   const char* what() const noexcept override { return d_msg.c_str(); }
  95
  96  private:
  97   /** The stored error message. */
  98   std::string d_msg;
  99 };
 100
 101 /**
 102  * A recoverable API exception.
 103  * If thrown, API objects can still be used.
 104  */
 105 class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
 106 {
 107  public:
 108   /**
 109    * Construct with message from a string.
 110    * @param str The error message.
 111    */
 112   CVC5ApiRecoverableException(const std::string& str) : CVC5ApiException(str) {}
 113   /**
 114    * Construct with message from a string stream.
 115    * @param stream The error message.
 116    */
 117   CVC5ApiRecoverableException(const std::stringstream& stream)
 118       : CVC5ApiException(stream.str())
 119   {
 120   }
 121 };
 122
 123 /**
 124  * Exception for unsupported command arguments.
 125  * If thrown, API objects can still be used.
 126  */
 127 class CVC5_EXPORT CVC5ApiUnsupportedException : public CVC5ApiRecoverableException
 128 {
 129  public:
 130   /**
 131    * Construct with message from a string.
 132    * @param str The error message.
 133    */
 134   CVC5ApiUnsupportedException(const std::string& str)
 135       : CVC5ApiRecoverableException(str)
 136   {
 137   }
 138   /**
 139    * Construct with message from a string stream.
 140    * @param stream The error message.
 141    */
 142   CVC5ApiUnsupportedException(const std::stringstream& stream)
 143       : CVC5ApiRecoverableException(stream.str())
 144   {
 145   }
 146 };
 147
 148 /**
 149  * An option-related API exception.
 150  * If thrown, API objects can still be used.
 151  */
 152 class CVC5_EXPORT CVC5ApiOptionException : public CVC5ApiRecoverableException
 153 {
 154  public:
 155   /**
 156    * Construct with message from a string.
 157    * @param str The error message.
 158    */
 159   CVC5ApiOptionException(const std::string& str)
 160       : CVC5ApiRecoverableException(str)
 161   {
 162   }
 163   /**
 164    * Construct with message from a string stream.
 165    * @param stream The error message.
 166    */
 167   CVC5ApiOptionException(const std::stringstream& stream)
 168       : CVC5ApiRecoverableException(stream.str())
 169   {
 170   }
 171 };
 172
 173 /* -------------------------------------------------------------------------- */
 174 /* Result                                                                     */
 175 /* -------------------------------------------------------------------------- */
 176
 177 /**
 178  * Encapsulation of a three-valued solver result, with explanations.
 179  */
 180 class CVC5_EXPORT Result
 181 {
 182   friend class Solver;
 183
 184  public:
 185   enum UnknownExplanation
 186   {
 187     REQUIRES_FULL_CHECK,
 188     INCOMPLETE,
 189     TIMEOUT,
 190     RESOURCEOUT,
 191     MEMOUT,
 192     INTERRUPTED,
 193     NO_STATUS,
 194     UNSUPPORTED,
 195     OTHER,
 196     UNKNOWN_REASON
 197   };
 198
 199   /** Constructor. */
 200   Result();
 201
 202   /**
 203    * Return true if Result is empty, i.e., a nullary Result, and not an actual
 204    * result returned from a checkSat() (and friends) query.
 205    */
 206   bool isNull() const;
 207
 208   /**
 209    * Return true if query was a satisfiable checkSat() or checkSatAssuming()
 210    * query.
 211    */
 212   bool isSat() const;
 213
 214   /**
 215    * Return true if query was an unsatisfiable checkSat() or
 216    * checkSatAssuming() query.
 217    */
 218   bool isUnsat() const;
 219
 220   /**
 221    * Return true if query was a checkSat() or checkSatAssuming() query and
 222    * cvc5 was not able to determine (un)satisfiability.
 223    */
 224   bool isSatUnknown() const;
 225
 226   /**
 227    * Return true if corresponding query was an entailed checkEntailed() query.
 228    */
 229   bool isEntailed() const;
 230
 231   /**
 232    * Return true if corresponding query was a checkEntailed() query that is
 233    * not entailed.
 234    */
 235   bool isNotEntailed() const;
 236
 237   /**
 238    * Return true if query was a checkEntailed() query and cvc5 was not able to
 239    * determine if it is entailed.
 240    */
 241   bool isEntailmentUnknown() const;
 242
 243   /**
 244    * Operator overloading for equality of two results.
 245    * @param r the result to compare to for equality
 246    * @return true if the results are equal
 247    */
 248   bool operator==(const Result& r) const;
 249
 250   /**
 251    * Operator overloading for disequality of two results.
 252    * @param r the result to compare to for disequality
 253    * @return true if the results are disequal
 254    */
 255   bool operator!=(const Result& r) const;
 256
 257   /**
 258    * @return an explanation for an unknown query result.
 259    */
 260   UnknownExplanation getUnknownExplanation() const;
 261
 262   /**
 263    * @return a string representation of this result.
 264    */
 265   std::string toString() const;
 266
 267  private:
 268   /**
 269    * Constructor.
 270    * @param r the internal result that is to be wrapped by this result
 271    * @return the Result
 272    */
 273   Result(const cvc5::Result& r);
 274
 275   /**
 276    * The interal result wrapped by this result.
 277    * Note: This is a shared_ptr rather than a unique_ptr since cvc5::Result is
 278    *       not ref counted.
 279    */
 280   std::shared_ptr<cvc5::Result> d_result;
 281 };
 282
 283 /**
 284  * Serialize a Result to given stream.
 285  * @param out the output stream
 286  * @param r the result to be serialized to the given output stream
 287  * @return the output stream
 288  */
 289 std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT;
 290
 291 /**
 292  * Serialize an UnknownExplanation to given stream.
 293  * @param out the output stream
 294  * @param e the explanation to be serialized to the given output stream
 295  * @return the output stream
 296  */
 297 std::ostream& operator<<(std::ostream& out,
 298                          enum Result::UnknownExplanation e) CVC5_EXPORT;
 299
 300 /* -------------------------------------------------------------------------- */
 301 /* Sort                                                                       */
 302 /* -------------------------------------------------------------------------- */
 303
 304 class Datatype;
 305
 306 /**
 307  * The sort of a cvc5 term.
 308  */
 309 class CVC5_EXPORT Sort
 310 {
 311   friend class cvc5::Command;
 312   friend class DatatypeConstructor;
 313   friend class DatatypeConstructorDecl;
 314   friend class DatatypeSelector;
 315   friend class DatatypeDecl;
 316   friend class Op;
 317   friend class Solver;
 318   friend class Grammar;
 319   friend struct std::hash<Sort>;
 320   friend class Term;
 321
 322  public:
 323   /**
 324    * Constructor.
 325    */
 326   Sort();
 327
 328   /**
 329    * Destructor.
 330    */
 331   ~Sort();
 332
 333   /**
 334    * Comparison for structural equality.
 335    * @param s the sort to compare to
 336    * @return true if the sorts are equal
 337    */
 338   bool operator==(const Sort& s) const;
 339
 340   /**
 341    * Comparison for structural disequality.
 342    * @param s the sort to compare to
 343    * @return true if the sorts are not equal
 344    */
 345   bool operator!=(const Sort& s) const;
 346
 347   /**
 348    * Comparison for ordering on sorts.
 349    * @param s the sort to compare to
 350    * @return true if this sort is less than s
 351    */
 352   bool operator<(const Sort& s) const;
 353
 354   /**
 355    * Comparison for ordering on sorts.
 356    * @param s the sort to compare to
 357    * @return true if this sort is greater than s
 358    */
 359   bool operator>(const Sort& s) const;
 360
 361   /**
 362    * Comparison for ordering on sorts.
 363    * @param s the sort to compare to
 364    * @return true if this sort is less than or equal to s
 365    */
 366   bool operator<=(const Sort& s) const;
 367
 368   /**
 369    * Comparison for ordering on sorts.
 370    * @param s the sort to compare to
 371    * @return true if this sort is greater than or equal to s
 372    */
 373   bool operator>=(const Sort& s) const;
 374
 375   /**
 376    * @return true if this Sort is a null sort.
 377    */
 378   bool isNull() const;
 379
 380   /**
 381    * Is this a Boolean sort?
 382    * @return true if the sort is the Boolean sort
 383    */
 384   bool isBoolean() const;
 385
 386   /**
 387    * Is this a integer sort?
 388    * @return true if the sort is the integer sort
 389    */
 390   bool isInteger() const;
 391
 392   /**
 393    * Is this a real sort?
 394    * @return true if the sort is the real sort
 395    */
 396   bool isReal() const;
 397
 398   /**
 399    * Is this a string sort?
 400    * @return true if the sort is the string sort
 401    */
 402   bool isString() const;
 403
 404   /**
 405    * Is this a regexp sort?
 406    * @return true if the sort is the regexp sort
 407    */
 408   bool isRegExp() const;
 409
 410   /**
 411    * Is this a rounding mode sort?
 412    * @return true if the sort is the rounding mode sort
 413    */
 414   bool isRoundingMode() const;
 415
 416   /**
 417    * Is this a bit-vector sort?
 418    * @return true if the sort is a bit-vector sort
 419    */
 420   bool isBitVector() const;
 421
 422   /**
 423    * Is this a floating-point sort?
 424    * @return true if the sort is a floating-point sort
 425    */
 426   bool isFloatingPoint() const;
 427
 428   /**
 429    * Is this a datatype sort?
 430    * @return true if the sort is a datatype sort
 431    */
 432   bool isDatatype() const;
 433
 434   /**
 435    * Is this a parametric datatype sort?
 436    * @return true if the sort is a parametric datatype sort
 437    */
 438   bool isParametricDatatype() const;
 439
 440   /**
 441    * Is this a constructor sort?
 442    * @return true if the sort is a constructor sort
 443    */
 444   bool isConstructor() const;
 445
 446   /**
 447    * Is this a selector sort?
 448    * @return true if the sort is a selector sort
 449    */
 450   bool isSelector() const;
 451
 452   /**
 453    * Is this a tester sort?
 454    * @return true if the sort is a tester sort
 455    */
 456   bool isTester() const;
 457   /**
 458    * Is this a datatype updater sort?
 459    * @return true if the sort is a datatype updater sort
 460    */
 461   bool isUpdater() const;
 462   /**
 463    * Is this a function sort?
 464    * @return true if the sort is a function sort
 465    */
 466   bool isFunction() const;
 467
 468   /**
 469    * Is this a predicate sort?
 470    * That is, is this a function sort mapping to Boolean? All predicate
 471    * sorts are also function sorts.
 472    * @return true if the sort is a predicate sort
 473    */
 474   bool isPredicate() const;
 475
 476   /**
 477    * Is this a tuple sort?
 478    * @return true if the sort is a tuple sort
 479    */
 480   bool isTuple() const;
 481
 482   /**
 483    * Is this a record sort?
 484    * @return true if the sort is a record sort
 485    */
 486   bool isRecord() const;
 487
 488   /**
 489    * Is this an array sort?
 490    * @return true if the sort is an array sort
 491    */
 492   bool isArray() const;
 493
 494   /**
 495    * Is this a Set sort?
 496    * @return true if the sort is a Set sort
 497    */
 498   bool isSet() const;
 499
 500   /**
 501    * Is this a Bag sort?
 502    * @return true if the sort is a Bag sort
 503    */
 504   bool isBag() const;
 505
 506   /**
 507    * Is this a Sequence sort?
 508    * @return true if the sort is a Sequence sort
 509    */
 510   bool isSequence() const;
 511
 512   /**
 513    * Is this an uninterpreted sort?
 514    * @return true if this is an uninterpreted sort
 515    */
 516   bool isUninterpretedSort() const;
 517
 518   /**
 519    * Is this a sort constructor kind?
 520    * @return true if this is a sort constructor kind
 521    */
 522   bool isSortConstructor() const;
 523
 524   /**
 525    * Is this a first-class sort?
 526    * First-class sorts are sorts for which:
 527    * 1. we handle equalities between terms of that type, and
 528    * 2. they are allowed to be parameters of parametric sorts (e.g. index or
 529    * element sorts of arrays).
 530    *
 531    * Examples of sorts that are not first-class include sort constructor sorts
 532    * and regular expression sorts.
 533    *
 534    * @return true if this is a first-class sort
 535    */
 536   bool isFirstClass() const;
 537
 538   /**
 539    * Is this a function-LIKE sort?
 540    *
 541    * Anything function-like except arrays (e.g., datatype selectors) is
 542    * considered a function here. Function-like terms can not be the argument
 543    * or return value for any term that is function-like.
 544    * This is mainly to avoid higher order.
 545    *
 546    * Note that arrays are explicitly not considered function-like here.
 547    *
 548    * @return true if this is a function-like sort
 549    */
 550   bool isFunctionLike() const;
 551
 552   /**
 553    * Is this sort a subsort of the given sort?
 554    * @return true if this sort is a subsort of s
 555    */
 556   bool isSubsortOf(const Sort& s) const;
 557
 558   /**
 559    * Is this sort comparable to the given sort (i.e., do they share
 560    * a common ancestor in the subsort tree)?
 561    * @return true if this sort is comparable to s
 562    */
 563   bool isComparableTo(const Sort& s) const;
 564
 565   /**
 566    * @return the underlying datatype of a datatype sort
 567    */
 568   Datatype getDatatype() const;
 569
 570   /**
 571    * Instantiate a parameterized datatype/sort sort.
 572    * Create sorts parameter with Solver::mkParamSort().
 573    * @param params the list of sort parameters to instantiate with
 574    */
 575   Sort instantiate(const std::vector<Sort>& params) const;
 576
 577   /**
 578    * Substitution of Sorts.
 579    * @param sort the subsort to be substituted within this sort.
 580    * @param replacement the sort replacing the substituted subsort.
 581    */
 582   Sort substitute(const Sort& sort, const Sort& replacement) const;
 583
 584   /**
 585    * Simultaneous substitution of Sorts.
 586    * @param sorts the subsorts to be substituted within this sort.
 587    * @param replacements the sort replacing the substituted subsorts.
 588    */
 589   Sort substitute(const std::vector<Sort>& sorts,
 590                   const std::vector<Sort>& replacements) const;
 591
 592   /**
 593    * Output a string representation of this sort to a given stream.
 594    * @param out the output stream
 595    */
 596   void toStream(std::ostream& out) const;
 597
 598   /**
 599    * @return a string representation of this sort
 600    */
 601   std::string toString() const;
 602
 603   /* Constructor sort ------------------------------------------------------- */
 604
 605   /**
 606    * @return the arity of a constructor sort
 607    */
 608   size_t getConstructorArity() const;
 609
 610   /**
 611    * @return the domain sorts of a constructor sort
 612    */
 613   std::vector<Sort> getConstructorDomainSorts() const;
 614
 615   /**
 616    * @return the codomain sort of a constructor sort
 617    */
 618   Sort getConstructorCodomainSort() const;
 619
 620   /* Selector sort ------------------------------------------------------- */
 621
 622   /**
 623    * @return the domain sort of a selector sort
 624    */
 625   Sort getSelectorDomainSort() const;
 626
 627   /**
 628    * @return the codomain sort of a selector sort
 629    */
 630   Sort getSelectorCodomainSort() const;
 631
 632   /* Tester sort ------------------------------------------------------- */
 633
 634   /**
 635    * @return the domain sort of a tester sort
 636    */
 637   Sort getTesterDomainSort() const;
 638
 639   /**
 640    * @return the codomain sort of a tester sort, which is the Boolean sort
 641    */
 642   Sort getTesterCodomainSort() const;
 643
 644   /* Function sort ------------------------------------------------------- */
 645
 646   /**
 647    * @return the arity of a function sort
 648    */
 649   size_t getFunctionArity() const;
 650
 651   /**
 652    * @return the domain sorts of a function sort
 653    */
 654   std::vector<Sort> getFunctionDomainSorts() const;
 655
 656   /**
 657    * @return the codomain sort of a function sort
 658    */
 659   Sort getFunctionCodomainSort() const;
 660
 661   /* Array sort ---------------------------------------------------------- */
 662
 663   /**
 664    * @return the array index sort of an array sort
 665    */
 666   Sort getArrayIndexSort() const;
 667
 668   /**
 669    * @return the array element sort of an array sort
 670    */
 671   Sort getArrayElementSort() const;
 672
 673   /* Set sort ------------------------------------------------------------ */
 674
 675   /**
 676    * @return the element sort of a set sort
 677    */
 678   Sort getSetElementSort() const;
 679
 680   /* Bag sort ------------------------------------------------------------ */
 681
 682   /**
 683    * @return the element sort of a bag sort
 684    */
 685   Sort getBagElementSort() const;
 686
 687   /* Sequence sort ------------------------------------------------------- */
 688
 689   /**
 690    * @return the element sort of a sequence sort
 691    */
 692   Sort getSequenceElementSort() const;
 693
 694   /* Uninterpreted sort -------------------------------------------------- */
 695
 696   /**
 697    * @return the name of an uninterpreted sort
 698    */
 699   std::string getUninterpretedSortName() const;
 700
 701   /**
 702    * @return true if an uninterpreted sort is parameterized
 703    */
 704   bool isUninterpretedSortParameterized() const;
 705
 706   /**
 707    * @return the parameter sorts of an uninterpreted sort
 708    */
 709   std::vector<Sort> getUninterpretedSortParamSorts() const;
 710
 711   /* Sort constructor sort ----------------------------------------------- */
 712
 713   /**
 714    * @return the name of a sort constructor sort
 715    */
 716   std::string getSortConstructorName() const;
 717
 718   /**
 719    * @return the arity of a sort constructor sort
 720    */
 721   size_t getSortConstructorArity() const;
 722
 723   /* Bit-vector sort ----------------------------------------------------- */
 724
 725   /**
 726    * @return the bit-width of the bit-vector sort
 727    */
 728   uint32_t getBitVectorSize() const;
 729
 730   /* Floating-point sort ------------------------------------------------- */
 731
 732   /**
 733    * @return the bit-width of the exponent of the floating-point sort
 734    */
 735   uint32_t getFloatingPointExponentSize() const;
 736
 737   /**
 738    * @return the width of the significand of the floating-point sort
 739    */
 740   uint32_t getFloatingPointSignificandSize() const;
 741
 742   /* Datatype sort ------------------------------------------------------- */
 743
 744   /**
 745    * @return the parameter sorts of a datatype sort
 746    */
 747   std::vector<Sort> getDatatypeParamSorts() const;
 748
 749   /**
 750    * @return the arity of a datatype sort
 751    */
 752   size_t getDatatypeArity() const;
 753
 754   /* Tuple sort ---------------------------------------------------------- */
 755
 756   /**
 757    * @return the length of a tuple sort
 758    */
 759   size_t getTupleLength() const;
 760
 761   /**
 762    * @return the element sorts of a tuple sort
 763    */
 764   std::vector<Sort> getTupleSorts() const;
 765
 766  private:
 767   /** @return the internal wrapped TypeNode of this sort. */
 768   const cvc5::TypeNode& getTypeNode(void) const;
 769
 770   /** Helper to convert a set of Sorts to internal TypeNodes. */
 771   std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts);
 772   /** Helper to convert a vector of Sorts to internal TypeNodes. */
 773   std::vector<TypeNode> static sortVectorToTypeNodes(
 774       const std::vector<Sort>& sorts);
 775   /** Helper to convert a vector of internal TypeNodes to Sorts. */
 776   std::vector<Sort> static typeNodeVectorToSorts(
 777       const Solver* slv, const std::vector<TypeNode>& types);
 778
 779   /**
 780    * Constructor.
 781    * @param slv the associated solver object
 782    * @param t the internal type that is to be wrapped by this sort
 783    * @return the Sort
 784    */
 785   Sort(const Solver* slv, const cvc5::TypeNode& t);
 786
 787   /**
 788    * Helper for isNull checks. This prevents calling an API function with
 789    * CVC5_API_CHECK_NOT_NULL
 790    */
 791   bool isNullHelper() const;
 792
 793   /**
 794    * The associated solver object.
 795    */
 796   const Solver* d_solver;
 797
 798   /**
 799    * The internal type wrapped by this sort.
 800    * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
 801    *       to memory allocation (cvc5::Type is already ref counted, so this
 802    *       could be a unique_ptr instead).
 803    */
 804   std::shared_ptr<cvc5::TypeNode> d_type;
 805 };
 806
 807 /**
 808  * Serialize a sort to given stream.
 809  * @param out the output stream
 810  * @param s the sort to be serialized to the given output stream
 811  * @return the output stream
 812  */
 813 std::ostream& operator<<(std::ostream& out, const Sort& s) CVC5_EXPORT;
 814
 815 }  // namespace api
 816 }  // namespace cvc5
 817
 818 namespace std {
 819
 820 /**
 821  * Hash function for Sorts.
 822  */
 823 template <>
 824 struct CVC5_EXPORT hash<cvc5::api::Sort>
 825 {
 826   size_t operator()(const cvc5::api::Sort& s) const;
 827 };
 828
 829 }  // namespace std
 830
 831 namespace cvc5::api {
 832
 833 /* -------------------------------------------------------------------------- */
 834 /* Op                                                                     */
 835 /* -------------------------------------------------------------------------- */
 836
 837 class Term;
 838
 839 /**
 840  * A cvc5 operator.
 841  * An operator is a term that represents certain operators, instantiated
 842  * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
 843  */
 844 class CVC5_EXPORT Op
 845 {
 846   friend class Solver;
 847   friend class Term;
 848   friend struct std::hash<Op>;
 849
 850  public:
 851   /**
 852    * Constructor.
 853    */
 854   Op();
 855
 856   /**
 857    * Destructor.
 858    */
 859   ~Op();
 860
 861   /**
 862    * Syntactic equality operator.
 863    * Return true if both operators are syntactically identical.
 864    * Both operators must belong to the same solver object.
 865    * @param t the operator to compare to for equality
 866    * @return true if the operators are equal
 867    */
 868   bool operator==(const Op& t) const;
 869
 870   /**
 871    * Syntactic disequality operator.
 872    * Return true if both operators differ syntactically.
 873    * Both terms must belong to the same solver object.
 874    * @param t the operator to compare to for disequality
 875    * @return true if operators are disequal
 876    */
 877   bool operator!=(const Op& t) const;
 878
 879   /**
 880    * @return the kind of this operator
 881    */
 882   Kind getKind() const;
 883
 884   /**
 885    * @return true if this operator is a null term
 886    */
 887   bool isNull() const;
 888
 889   /**
 890    * @return true iff this operator is indexed
 891    */
 892   bool isIndexed() const;
 893
 894   /**
 895    * @return the number of indices of this op
 896    */
 897   size_t getNumIndices() const;
 898
 899   /**
 900    * Get the index at position i.
 901    * @param i the position of the index to return
 902    * @return the index at position i
 903    */
 904
 905   Term operator[](size_t i) const;
 906
 907   /**
 908    * Get the indices used to create this Op.
 909    * Supports the following template arguments:
 910    *   - string
 911    *   - Kind
 912    *   - uint32_t
 913    *   - pair<uint32_t, uint32_t>
 914    * Check the Op Kind with getKind() to determine which argument to use.
 915    * @return the indices used to create this Op
 916    */
 917   template <typename T>
 918   T getIndices() const;
 919
 920   /**
 921    * @return a string representation of this operator
 922    */
 923   std::string toString() const;
 924
 925  private:
 926   /**
 927    * Constructor for a single kind (non-indexed operator).
 928    * @param slv the associated solver object
 929    * @param k the kind of this Op
 930    */
 931   Op(const Solver* slv, const Kind k);
 932
 933   /**
 934    * Constructor.
 935    * @param slv the associated solver object
 936    * @param k the kind of this Op
 937    * @param n the internal node that is to be wrapped by this term
 938    * @return the Term
 939    */
 940   Op(const Solver* slv, const Kind k, const cvc5::Node& n);
 941
 942   /**
 943    * Helper for isNull checks. This prevents calling an API function with
 944    * CVC5_API_CHECK_NOT_NULL
 945    */
 946   bool isNullHelper() const;
 947
 948   /**
 949    * Note: An indexed operator has a non-null internal node, d_node
 950    * Note 2: We use a helper method to avoid having API functions call
 951    *         other API functions (we need to call this internally)
 952    * @return true iff this Op is indexed
 953    */
 954   bool isIndexedHelper() const;
 955
 956   /**
 957    * Helper for getNumIndices
 958    * @return the number of indices of this op
 959    */
 960   size_t getNumIndicesHelper() const;
 961
 962   /**
 963    * Helper for operator[](size_t index).
 964    * @param index position of the index. Should be less than getNumIndicesHelper().
 965    * @return the index at position index
 966    */
 967   Term getIndexHelper(size_t index) const;
 968
 969   /**
 970    * The associated solver object.
 971    */
 972   const Solver* d_solver;
 973
 974   /** The kind of this operator. */
 975   Kind d_kind;
 976
 977   /**
 978    * The internal node wrapped by this operator.
 979    * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
 980    *       to memory allocation (cvc5::Node is already ref counted, so this
 981    *       could be a unique_ptr instead).
 982    */
 983   std::shared_ptr<cvc5::Node> d_node;
 984 };
 985
 986 /**
 987  * Serialize an operator to given stream.
 988  * @param out the output stream
 989  * @param t the operator to be serialized to the given output stream
 990  * @return the output stream
 991  */
 992 std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT;
 993
 994 }  // namespace cvc5::api
 995
 996 namespace std {
 997 /**
 998  * Hash function for Ops.
 999  */
1000 template <>
1001 struct CVC5_EXPORT hash<cvc5::api::Op>
1002 {
1003   size_t operator()(const cvc5::api::Op& t) const;
1004 };
1005 }  // namespace std
1006
1007 namespace cvc5::api {
1008 /* -------------------------------------------------------------------------- */
1009 /* Term                                                                       */
1010 /* -------------------------------------------------------------------------- */
1011
1012 /**
1013  * A cvc5 Term.
1014  */
1015 class CVC5_EXPORT Term
1016 {
1017   friend class cvc5::Command;
1018   friend class Datatype;
1019   friend class DatatypeConstructor;
1020   friend class DatatypeSelector;
1021   friend class Solver;
1022   friend class Grammar;
1023   friend struct std::hash<Term>;
1024
1025  public:
1026   /**
1027    * Constructor for a null term.
1028    */
1029   Term();
1030
1031   /**
1032    * Destructor.
1033    */
1034   ~Term();
1035
1036   /**
1037    * Syntactic equality operator.
1038    * Return true if both terms are syntactically identical.
1039    * Both terms must belong to the same solver object.
1040    * @param t the term to compare to for equality
1041    * @return true if the terms are equal
1042    */
1043   bool operator==(const Term& t) const;
1044
1045   /**
1046    * Syntactic disequality operator.
1047    * Return true if both terms differ syntactically.
1048    * Both terms must belong to the same solver object.
1049    * @param t the term to compare to for disequality
1050    * @return true if terms are disequal
1051    */
1052   bool operator!=(const Term& t) const;
1053
1054   /**
1055    * Comparison for ordering on terms by their id.
1056    * @param t the term to compare to
1057    * @return true if this term is less than t
1058    */
1059   bool operator<(const Term& t) const;
1060
1061   /**
1062    * Comparison for ordering on terms by their id.
1063    * @param t the term to compare to
1064    * @return true if this term is greater than t
1065    */
1066   bool operator>(const Term& t) const;
1067
1068   /**
1069    * Comparison for ordering on terms by their id.
1070    * @param t the term to compare to
1071    * @return true if this term is less than or equal to t
1072    */
1073   bool operator<=(const Term& t) const;
1074
1075   /**
1076    * Comparison for ordering on terms by their id.
1077    * @param t the term to compare to
1078    * @return true if this term is greater than or equal to t
1079    */
1080   bool operator>=(const Term& t) const;
1081
1082   /** @return the number of children of this term  */
1083   size_t getNumChildren() const;
1084
1085   /**
1086    * Get the child term at a given index.
1087    * @param index the index of the child term to return
1088    * @return the child term with the given index
1089    */
1090   Term operator[](size_t index) const;
1091
1092   /**
1093    * @return the id of this term
1094    */
1095   uint64_t getId() const;
1096
1097   /**
1098    * @return the kind of this term
1099    */
1100   Kind getKind() const;
1101
1102   /**
1103    * @return the sort of this term
1104    */
1105   Sort getSort() const;
1106
1107   /**
1108    * @return the result of replacing 'term' by 'replacement' in this term
1109    */
1110   Term substitute(const Term& term, const Term& replacement) const;
1111
1112   /**
1113    * @return the result of simultaneously replacing 'terms' by 'replacements'
1114    * in this term
1115    */
1116   Term substitute(const std::vector<Term>& terms,
1117                   const std::vector<Term>& replacements) const;
1118
1119   /**
1120    * @return true iff this term has an operator
1121    */
1122   bool hasOp() const;
1123
1124   /**
1125    * @return the Op used to create this term
1126    * Note: This is safe to call when hasOp() returns true.
1127    */
1128   Op getOp() const;
1129
1130   /**
1131    * @return true if this Term is a null term
1132    */
1133   bool isNull() const;
1134
1135   /**
1136    * Boolean negation.
1137    * @return the Boolean negation of this term
1138    */
1139   Term notTerm() const;
1140
1141   /**
1142    * Boolean and.
1143    * @param t a Boolean term
1144    * @return the conjunction of this term and the given term
1145    */
1146   Term andTerm(const Term& t) const;
1147
1148   /**
1149    * Boolean or.
1150    * @param t a Boolean term
1151    * @return the disjunction of this term and the given term
1152    */
1153   Term orTerm(const Term& t) const;
1154
1155   /**
1156    * Boolean exclusive or.
1157    * @param t a Boolean term
1158    * @return the exclusive disjunction of this term and the given term
1159    */
1160   Term xorTerm(const Term& t) const;
1161
1162   /**
1163    * Equality.
1164    * @param t a Boolean term
1165    * @return the Boolean equivalence of this term and the given term
1166    */
1167   Term eqTerm(const Term& t) const;
1168
1169   /**
1170    * Boolean implication.
1171    * @param t a Boolean term
1172    * @return the implication of this term and the given term
1173    */
1174   Term impTerm(const Term& t) const;
1175
1176   /**
1177    * If-then-else with this term as the Boolean condition.
1178    * @param then_t the 'then' term
1179    * @param else_t the 'else' term
1180    * @return the if-then-else term with this term as the Boolean condition
1181    */
1182   Term iteTerm(const Term& then_t, const Term& else_t) const;
1183
1184   /**
1185    * @return a string representation of this term
1186    */
1187   std::string toString() const;
1188
1189   /**
1190    * Iterator for the children of a Term.
1191    * Note: This treats uninterpreted functions as Term just like any other term
1192    *       for example, the term f(x, y) will have Kind APPLY_UF and three
1193    *       children: f, x, and y
1194    */
1195   class CVC5_EXPORT const_iterator
1196   {
1197     friend class Term;
1198
1199    public:
1200     /* The following types are required by trait std::iterator_traits */
1201
1202     /** Iterator tag */
1203     using iterator_category = std::forward_iterator_tag;
1204
1205     /** The type of the item */
1206     using value_type = Term;
1207
1208     /** The pointer type of the item */
1209     using pointer = const Term*;
1210
1211     /** The reference type of the item */
1212     using reference = const Term&;
1213
1214     /** The type returned when two iterators are subtracted */
1215     using difference_type = std::ptrdiff_t;
1216
1217     /* End of std::iterator_traits required types */
1218
1219     /**
1220      * Null Constructor.
1221      */
1222     const_iterator();
1223
1224     /**
1225      * Constructor
1226      * @param slv the associated solver object
1227      * @param e a shared pointer to the node that we're iterating over
1228      * @param p the position of the iterator (e.g. which child it's on)
1229      */
1230     const_iterator(const Solver* slv,
1231                    const std::shared_ptr<cvc5::Node>& e,
1232                    uint32_t p);
1233
1234     /**
1235      * Copy constructor.
1236      */
1237     const_iterator(const const_iterator& it);
1238
1239     /**
1240      * Assignment operator.
1241      * @param it the iterator to assign to
1242      * @return the reference to the iterator after assignment
1243      */
1244     const_iterator& operator=(const const_iterator& it);
1245
1246     /**
1247      * Equality operator.
1248      * @param it the iterator to compare to for equality
1249      * @return true if the iterators are equal
1250      */
1251     bool operator==(const const_iterator& it) const;
1252
1253     /**
1254      * Disequality operator.
1255      * @param it the iterator to compare to for disequality
1256      * @return true if the iterators are disequal
1257      */
1258     bool operator!=(const const_iterator& it) const;
1259
1260     /**
1261      * Increment operator (prefix).
1262      * @return a reference to the iterator after incrementing by one
1263      */
1264     const_iterator& operator++();
1265
1266     /**
1267      * Increment operator (postfix).
1268      * @return a reference to the iterator after incrementing by one
1269      */
1270     const_iterator operator++(int);
1271
1272     /**
1273      * Dereference operator.
1274      * @return the term this iterator points to
1275      */
1276     Term operator*() const;
1277
1278    private:
1279     /**
1280      * The associated solver object.
1281      */
1282     const Solver* d_solver;
1283     /** The original node to be iterated over. */
1284     std::shared_ptr<cvc5::Node> d_origNode;
1285     /** Keeps track of the iteration position. */
1286     uint32_t d_pos;
1287   };
1288
1289   /**
1290    * @return an iterator to the first child of this Term
1291    */
1292   const_iterator begin() const;
1293
1294   /**
1295    * @return an iterator to one-off-the-last child of this Term
1296    */
1297   const_iterator end() const;
1298
1299   /**
1300    * @return true if the term is an integer value that fits within int32_t.
1301    */
1302   bool isInt32Value() const;
1303   /**
1304    * Asserts isInt32Value().
1305    * @return the integer term as a int32_t.
1306    */
1307   int32_t getInt32Value() const;
1308   /**
1309    * @return true if the term is an integer value that fits within uint32_t.
1310    */
1311   bool isUInt32Value() const;
1312   /**
1313    * Asserts isUInt32Value().
1314    * @return the integer term as a uint32_t.
1315    */
1316   uint32_t getUInt32Value() const;
1317   /**
1318    * @return true if the term is an integer value that fits within int64_t.
1319    */
1320   bool isInt64Value() const;
1321   /**
1322    * Asserts isInt64Value().
1323    * @return the integer term as a int64_t.
1324    */
1325   int64_t getInt64Value() const;
1326   /**
1327    * @return true if the term is an integer value that fits within uint64_t.
1328    */
1329   bool isUInt64Value() const;
1330   /**
1331    * Asserts isUInt64Value().
1332    * @return the integer term as a uint64_t.
1333    */
1334   uint64_t getUInt64Value() const;
1335   /**
1336    * @return true if the term is an integer value.
1337    */
1338   bool isIntegerValue() const;
1339   /**
1340    * Asserts isIntegerValue().
1341    * @return the integer term in (decimal) string representation.
1342    */
1343   std::string getIntegerValue() const;
1344
1345   /**
1346    * @return true if the term is a string value.
1347    */
1348   bool isStringValue() const;
1349   /**
1350    * Note: This method is not to be confused with toString() which returns
1351    * the term in some string representation, whatever data it may hold. Asserts
1352    * isStringValue().
1353    * @return the string term as a native string value.
1354    */
1355   std::wstring getStringValue() const;
1356
1357   /**
1358    * @return true if the term is a rational value whose numerator and
1359    * denominator fit within int32_t and uint32_t, respectively.
1360    */
1361   bool isReal32Value() const;
1362   /**
1363    * Asserts isReal32Value().
1364    * @return the representation of a rational value as a pair of its numerator
1365    * and denominator.
1366    */
1367   std::pair<int32_t, uint32_t> getReal32Value() const;
1368   /**
1369    * @return true if the term is a rational value whose numerator and
1370    * denominator fit within int64_t and uint64_t, respectively.
1371    */
1372   bool isReal64Value() const;
1373   /**
1374    * Asserts isReal64Value().
1375    * @return the representation of a rational value as a pair of its numerator
1376    * and denominator.
1377    */
1378   std::pair<int64_t, uint64_t> getReal64Value() const;
1379   /**
1380    * @return true if the term is a rational value.
1381    *
1382    * Note that a term of kind PI is not considered to be a real value.
1383    */
1384   bool isRealValue() const;
1385   /**
1386    * Asserts isRealValue().
1387    * @return the representation of a rational value as a (rational) string.
1388    */
1389   std::string getRealValue() const;
1390
1391   /**
1392    * @return true if the term is a constant array.
1393    */
1394   bool isConstArray() const;
1395   /**
1396    * Asserts isConstArray().
1397    * @return the base (element stored at all indices) of a constant array
1398    */
1399   Term getConstArrayBase() const;
1400
1401   /**
1402    * @return true if the term is a Boolean value.
1403    */
1404   bool isBooleanValue() const;
1405   /**
1406    * Asserts isBooleanValue().
1407    * @return the representation of a Boolean value as a native Boolean value.
1408    */
1409   bool getBooleanValue() const;
1410
1411   /**
1412    * @return true if the term is a bit-vector value.
1413    */
1414   bool isBitVectorValue() const;
1415   /**
1416    * Asserts isBitVectorValue().
1417    * @return the representation of a bit-vector value in string representation.
1418    * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
1419    * string).
1420    */
1421   std::string getBitVectorValue(uint32_t base = 2) const;
1422
1423   /**
1424    * @return true if the term is an abstract value.
1425    */
1426   bool isAbstractValue() const;
1427   /**
1428    * Asserts isAbstractValue().
1429    * @return the representation of an abstract value as a string.
1430    */
1431   std::string getAbstractValue() const;
1432
1433   /**
1434    * @return true if the term is a tuple value.
1435    */
1436   bool isTupleValue() const;
1437   /**
1438    * Asserts isTupleValue().
1439    * @return the representation of a tuple value as a vector of terms.
1440    */
1441   std::vector<Term> getTupleValue() const;
1442
1443   /**
1444    * @return true if the term is the floating-point value for positive zero.
1445    */
1446   bool isFloatingPointPosZero() const;
1447   /**
1448    * @return true if the term is the floating-point value for negative zero.
1449    */
1450   bool isFloatingPointNegZero() const;
1451   /**
1452    * @return true if the term is the floating-point value for positive
1453    * infinity.
1454    */
1455   bool isFloatingPointPosInf() const;
1456   /**
1457    * @return true if the term is the floating-point value for negative
1458    * infinity.
1459    */
1460   bool isFloatingPointNegInf() const;
1461   /**
1462    * @return true if the term is the floating-point value for not a number.
1463    */
1464   bool isFloatingPointNaN() const;
1465   /**
1466    * @return true if the term is a floating-point value.
1467    */
1468   bool isFloatingPointValue() const;
1469   /**
1470    * Asserts isFloatingPointValue().
1471    * @return the representation of a floating-point value as a tuple of the
1472    * exponent width, the significand width and a bit-vector value.
1473    */
1474   std::tuple<uint32_t, uint32_t, Term> getFloatingPointValue() const;
1475
1476   /**
1477    * @return true if the term is a set value.
1478    *
1479    * A term is a set value if it is considered to be a (canonical) constant set
1480    * value.  A canonical set value is one whose AST is:
1481    * ```
1482    *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
1483    * ```
1484    * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
1485    * also @ref Term::operator>(const Term&) const).
1486    *
1487    * Note that a universe set term (kind SET_UNIVERSE) is not considered to be
1488    * a set value.
1489    */
1490   bool isSetValue() const;
1491   /**
1492    * Asserts isSetValue().
1493    * @return the representation of a set value as a set of terms.
1494    */
1495   std::set<Term> getSetValue() const;
1496
1497   /**
1498    * @return true if the term is a sequence value.
1499    */
1500   bool isSequenceValue() const;
1501   /**
1502    * Asserts isSequenceValue().
1503    * Note that it is usually necessary for sequences to call
1504    * `Solver::simplify()` to turn a sequence that is constructed by, e.g.,
1505    * concatenation of unit sequences, into a sequence value.
1506    * @return the representation of a sequence value as a vector of terms.
1507    */
1508   std::vector<Term> getSequenceValue() const;
1509
1510   /**
1511    * @return true if the term is a value from an uninterpreted sort.
1512    */
1513   bool isUninterpretedValue() const;
1514   /**
1515   bool @return() const;
1516    * Asserts isUninterpretedValue().
1517    * @return the representation of an uninterpreted value as a pair of its
1518   sort and its
1519    * index.
1520    */
1521   std::pair<Sort, int32_t> getUninterpretedValue() const;
1522
1523  protected:
1524   /**
1525    * The associated solver object.
1526    */
1527   const Solver* d_solver;
1528
1529  private:
1530   /** Helper to convert a vector of Terms to internal Nodes. */
1531   std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
1532
1533   /** Helper method to collect all elements of a set. */
1534   static void collectSet(std::set<Term>& set,
1535                          const cvc5::Node& node,
1536                          const Solver* slv);
1537   /** Helper method to collect all elements of a sequence. */
1538   static void collectSequence(std::vector<Term>& seq,
1539                               const cvc5::Node& node,
1540                               const Solver* slv);
1541
1542   /**
1543    * Constructor.
1544    * @param slv the associated solver object
1545    * @param n the internal node that is to be wrapped by this term
1546    * @return the Term
1547    */
1548   Term(const Solver* slv, const cvc5::Node& n);
1549
1550   /** @return the internal wrapped Node of this term. */
1551   const cvc5::Node& getNode(void) const;
1552
1553   /**
1554    * Helper for isNull checks. This prevents calling an API function with
1555    * CVC5_API_CHECK_NOT_NULL
1556    */
1557   bool isNullHelper() const;
1558
1559   /**
1560    * Helper function that returns the kind of the term, which takes into
1561    * account special cases of the conversion for internal to external kinds.
1562    * @return the kind of this term
1563    */
1564   Kind getKindHelper() const;
1565
1566   /**
1567    * @return true if the current term is a constant integer that is casted into
1568    * real using the operator CAST_TO_REAL, and returns false otherwise
1569    */
1570   bool isCastedReal() const;
1571   /**
1572    * The internal node wrapped by this term.
1573    * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
1574    *       to memory allocation (cvc5::Node is already ref counted, so this
1575    *       could be a unique_ptr instead).
1576    */
1577   std::shared_ptr<cvc5::Node> d_node;
1578 };
1579
1580 /**
1581  * Serialize a term to given stream.
1582  * @param out the output stream
1583  * @param t the term to be serialized to the given output stream
1584  * @return the output stream
1585  */
1586 std::ostream& operator<<(std::ostream& out, const Term& t) CVC5_EXPORT;
1587
1588 /**
1589  * Serialize a vector of terms to given stream.
1590  * @param out the output stream
1591  * @param vector the vector of terms to be serialized to the given stream
1592  * @return the output stream
1593  */
1594 std::ostream& operator<<(std::ostream& out,
1595                          const std::vector<Term>& vector) CVC5_EXPORT;
1596
1597 /**
1598  * Serialize a set of terms to the given stream.
1599  * @param out the output stream
1600  * @param set the set of terms to be serialized to the given stream
1601  * @return the output stream
1602  */
1603 std::ostream& operator<<(std::ostream& out,
1604                          const std::set<Term>& set) CVC5_EXPORT;
1605
1606 /**
1607  * Serialize an unordered_set of terms to the given stream.
1608  *
1609  * @param out the output stream
1610  * @param unordered_set the set of terms to be serialized to the given stream
1611  * @return the output stream
1612  */
1613 std::ostream& operator<<(std::ostream& out,
1614                          const std::unordered_set<Term>& unordered_set)
1615     CVC5_EXPORT;
1616
1617 /**
1618  * Serialize a map of terms to the given stream.
1619  *
1620  * @param out the output stream
1621  * @param map the map of terms to be serialized to the given stream
1622  * @return the output stream
1623  */
1624 template <typename V>
1625 std::ostream& operator<<(std::ostream& out,
1626                          const std::map<Term, V>& map) CVC5_EXPORT;
1627
1628 /**
1629  * Serialize an unordered_map of terms to the given stream.
1630  *
1631  * @param out the output stream
1632  * @param unordered_map the map of terms to be serialized to the given stream
1633  * @return the output stream
1634  */
1635 template <typename V>
1636 std::ostream& operator<<(std::ostream& out,
1637                          const std::unordered_map<Term, V>& unordered_map)
1638     CVC5_EXPORT;
1639
1640 }  // namespace cvc5::api
1641
1642 namespace std {
1643 /**
1644  * Hash function for Terms.
1645  */
1646 template <>
1647 struct CVC5_EXPORT hash<cvc5::api::Term>
1648 {
1649   size_t operator()(const cvc5::api::Term& t) const;
1650 };
1651 }  // namespace std
1652
1653 namespace cvc5::api {
1654
1655 /* -------------------------------------------------------------------------- */
1656 /* Datatypes                                                                  */
1657 /* -------------------------------------------------------------------------- */
1658
1659 class DatatypeConstructorIterator;
1660 class DatatypeIterator;
1661
1662 /**
1663  * A cvc5 datatype constructor declaration.
1664  */
1665 class CVC5_EXPORT DatatypeConstructorDecl
1666 {
1667   friend class DatatypeDecl;
1668   friend class Solver;
1669
1670  public:
1671   /** Constructor.  */
1672   DatatypeConstructorDecl();
1673
1674   /**
1675    * Destructor.
1676    */
1677   ~DatatypeConstructorDecl();
1678
1679   /**
1680    * Add datatype selector declaration.
1681    * @param name the name of the datatype selector declaration to add
1682    * @param sort the range sort of the datatype selector declaration to add
1683    */
1684   void addSelector(const std::string& name, const Sort& sort);
1685   /**
1686    * Add datatype selector declaration whose range type is the datatype itself.
1687    * @param name the name of the datatype selector declaration to add
1688    */
1689   void addSelectorSelf(const std::string& name);
1690
1691   /**
1692    * @return true if this DatatypeConstructorDecl is a null declaration.
1693    */
1694   bool isNull() const;
1695
1696   /**
1697    * @return a string representation of this datatype constructor declaration
1698    */
1699   std::string toString() const;
1700
1701  private:
1702   /**
1703    * Constructor.
1704    * @param slv the associated solver object
1705    * @param name the name of the datatype constructor
1706    * @return the DatatypeConstructorDecl
1707    */
1708   DatatypeConstructorDecl(const Solver* slv, const std::string& name);
1709
1710   /**
1711    * Helper for isNull checks. This prevents calling an API function with
1712    * CVC5_API_CHECK_NOT_NULL
1713    */
1714   bool isNullHelper() const;
1715
1716   /**
1717    * The associated solver object.
1718    */
1719   const Solver* d_solver;
1720
1721   /**
1722    * The internal (intermediate) datatype constructor wrapped by this
1723    * datatype constructor declaration.
1724    * Note: This is a shared_ptr rather than a unique_ptr since
1725    *       cvc5::DTypeConstructor is not ref counted.
1726    */
1727   std::shared_ptr<cvc5::DTypeConstructor> d_ctor;
1728 };
1729
1730 class Solver;
1731
1732 /**
1733  * A cvc5 datatype declaration.
1734  */
1735 class CVC5_EXPORT DatatypeDecl
1736 {
1737   friend class DatatypeConstructorArg;
1738   friend class Solver;
1739   friend class Grammar;
1740
1741  public:
1742   /** Constructor.  */
1743   DatatypeDecl();
1744
1745   /**
1746    * Destructor.
1747    */
1748   ~DatatypeDecl();
1749
1750   /**
1751    * Add datatype constructor declaration.
1752    * @param ctor the datatype constructor declaration to add
1753    */
1754   void addConstructor(const DatatypeConstructorDecl& ctor);
1755
1756   /** Get the number of constructors (so far) for this Datatype declaration. */
1757   size_t getNumConstructors() const;
1758
1759   /** Is this Datatype declaration parametric? */
1760   bool isParametric() const;
1761
1762   /**
1763    * @return true if this DatatypeDecl is a null object
1764    */
1765   bool isNull() const;
1766
1767   /**
1768    * @return a string representation of this datatype declaration
1769    */
1770   std::string toString() const;
1771
1772   /** @return the name of this datatype declaration. */
1773   std::string getName() const;
1774
1775  private:
1776   /**
1777    * Constructor.
1778    * @param slv the associated solver object
1779    * @param name the name of the datatype
1780    * @param isCoDatatype true if a codatatype is to be constructed
1781    * @return the DatatypeDecl
1782    */
1783   DatatypeDecl(const Solver* slv,
1784                const std::string& name,
1785                bool isCoDatatype = false);
1786
1787   /**
1788    * Constructor for parameterized datatype declaration.
1789    * Create sorts parameter with Solver::mkParamSort().
1790    * @param slv the associated solver object
1791    * @param name the name of the datatype
1792    * @param param the sort parameter
1793    * @param isCoDatatype true if a codatatype is to be constructed
1794    */
1795   DatatypeDecl(const Solver* slv,
1796                const std::string& name,
1797                const Sort& param,
1798                bool isCoDatatype = false);
1799
1800   /**
1801    * Constructor for parameterized datatype declaration.
1802    * Create sorts parameter with Solver::mkParamSort().
1803    * @param slv the associated solver object
1804    * @param name the name of the datatype
1805    * @param params a list of sort parameters
1806    * @param isCoDatatype true if a codatatype is to be constructed
1807    */
1808   DatatypeDecl(const Solver* slv,
1809                const std::string& name,
1810                const std::vector<Sort>& params,
1811                bool isCoDatatype = false);
1812
1813   /** @return the internal wrapped Dtype of this datatype declaration. */
1814   cvc5::DType& getDatatype(void) const;
1815
1816   /**
1817    * Helper for isNull checks. This prevents calling an API function with
1818    * CVC5_API_CHECK_NOT_NULL
1819    */
1820   bool isNullHelper() const;
1821
1822   /**
1823    * The associated solver object.
1824    */
1825   const Solver* d_solver;
1826
1827   /**
1828    * The internal (intermediate) datatype wrapped by this datatype
1829    * declaration.
1830    * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1831    *       not ref counted.
1832    */
1833   std::shared_ptr<cvc5::DType> d_dtype;
1834 };
1835
1836 /**
1837  * A cvc5 datatype selector.
1838  */
1839 class CVC5_EXPORT DatatypeSelector
1840 {
1841   friend class Datatype;
1842   friend class DatatypeConstructor;
1843   friend class Solver;
1844
1845  public:
1846   /**
1847    * Constructor.
1848    */
1849   DatatypeSelector();
1850
1851   /**
1852    * Destructor.
1853    */
1854   ~DatatypeSelector();
1855
1856   /** @return the name of this Datatype selector. */
1857   std::string getName() const;
1858
1859   /**
1860    * Get the selector operator of this datatype selector.
1861    * @return the selector term
1862    */
1863   Term getSelectorTerm() const;
1864
1865   /**
1866    * Get the updater operator of this datatype selector.
1867    * @return the updater term
1868    */
1869   Term getUpdaterTerm() const;
1870
1871   /** @return the range sort of this selector. */
1872   Sort getRangeSort() const;
1873
1874   /**
1875    * @return true if this DatatypeSelector is a null object
1876    */
1877   bool isNull() const;
1878
1879   /**
1880    * @return a string representation of this datatype selector
1881    */
1882   std::string toString() const;
1883
1884  private:
1885   /**
1886    * Constructor.
1887    * @param slv the associated solver object
1888    * @param stor the internal datatype selector to be wrapped
1889    * @return the DatatypeSelector
1890    */
1891   DatatypeSelector(const Solver* slv, const cvc5::DTypeSelector& stor);
1892
1893   /**
1894    * Helper for isNull checks. This prevents calling an API function with
1895    * CVC5_API_CHECK_NOT_NULL
1896    */
1897   bool isNullHelper() const;
1898
1899   /**
1900    * The associated solver object.
1901    */
1902   const Solver* d_solver;
1903
1904   /**
1905    * The internal datatype selector wrapped by this datatype selector.
1906    * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1907    *       not ref counted.
1908    */
1909   std::shared_ptr<cvc5::DTypeSelector> d_stor;
1910 };
1911
1912 /**
1913  * A cvc5 datatype constructor.
1914  */
1915 class CVC5_EXPORT DatatypeConstructor
1916 {
1917   friend class Datatype;
1918   friend class Solver;
1919
1920  public:
1921   /**
1922    * Constructor.
1923    */
1924   DatatypeConstructor();
1925
1926   /**
1927    * Destructor.
1928    */
1929   ~DatatypeConstructor();
1930
1931   /** @return the name of this Datatype constructor. */
1932   std::string getName() const;
1933
1934   /**
1935    * Get the constructor operator of this datatype constructor.
1936    * @return the constructor term
1937    */
1938   Term getConstructorTerm() const;
1939
1940   /**
1941    * Get the constructor operator of this datatype constructor whose return
1942    * type is retSort. This method is intended to be used on constructors of
1943    * parametric datatypes and can be seen as returning the constructor
1944    * term that has been explicitly cast to the given sort.
1945    *
1946    * This method is required for constructors of parametric datatypes whose
1947    * return type cannot be determined by type inference. For example, given:
1948    *   (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
1949    * The type of nil terms need to be provided by the user. In SMT version 2.6,
1950    * this is done via the syntax for qualified identifiers:
1951    *   (as nil (List Int))
1952    * This method is equivalent of applying the above, where this
1953    * DatatypeConstructor is the one corresponding to nil, and retSort is
1954    * (List Int).
1955    *
1956    * Furthermore note that the returned constructor term t is an operator,
1957    * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
1958    * (nullary) application of nil.
1959    *
1960    * @param retSort the desired return sort of the constructor
1961    * @return the constructor term
1962    */
1963   Term getSpecializedConstructorTerm(const Sort& retSort) const;
1964
1965   /**
1966    * Get the tester operator of this datatype constructor.
1967    * @return the tester operator
1968    */
1969   Term getTesterTerm() const;
1970
1971   /**
1972    * @return the number of selectors (so far) of this Datatype constructor.
1973    */
1974   size_t getNumSelectors() const;
1975
1976   /** @return the i^th DatatypeSelector. */
1977   DatatypeSelector operator[](size_t index) const;
1978   /**
1979    * Get the datatype selector with the given name.
1980    * This is a linear search through the selectors, so in case of
1981    * multiple, similarly-named selectors, the first is returned.
1982    * @param name the name of the datatype selector
1983    * @return the first datatype selector with the given name
1984    */
1985   DatatypeSelector operator[](const std::string& name) const;
1986   DatatypeSelector getSelector(const std::string& name) const;
1987
1988   /**
1989    * Get the term representation of the datatype selector with the given name.
1990    * This is a linear search through the arguments, so in case of multiple,
1991    * similarly-named arguments, the selector for the first is returned.
1992    * @param name the name of the datatype selector
1993    * @return a term representing the datatype selector with the given name
1994    */
1995   Term getSelectorTerm(const std::string& name) const;
1996
1997   /**
1998    * @return true if this DatatypeConstructor is a null object
1999    */
2000   bool isNull() const;
2001
2002   /**
2003    * @return a string representation of this datatype constructor
2004    */
2005   std::string toString() const;
2006
2007   /**
2008    * Iterator for the selectors of a datatype constructor.
2009    */
2010   class const_iterator
2011   {
2012     friend class DatatypeConstructor;  // to access constructor
2013
2014    public:
2015     /* The following types are required by trait std::iterator_traits */
2016
2017     /** Iterator tag */
2018     using iterator_category = std::forward_iterator_tag;
2019
2020     /** The type of the item */
2021     using value_type = DatatypeConstructor;
2022
2023     /** The pointer type of the item */
2024     using pointer = const DatatypeConstructor*;
2025
2026     /** The reference type of the item */
2027     using reference = const DatatypeConstructor&;
2028
2029     /** The type returned when two iterators are subtracted */
2030     using difference_type = std::ptrdiff_t;
2031
2032     /* End of std::iterator_traits required types */
2033
2034     /** Nullary constructor (required for Cython). */
2035     const_iterator();
2036
2037     /**
2038      * Assignment operator.
2039      * @param it the iterator to assign to
2040      * @return the reference to the iterator after assignment
2041      */
2042     const_iterator& operator=(const const_iterator& it);
2043
2044     /**
2045      * Equality operator.
2046      * @param it the iterator to compare to for equality
2047      * @return true if the iterators are equal
2048      */
2049     bool operator==(const const_iterator& it) const;
2050
2051     /**
2052      * Disequality operator.
2053      * @param it the iterator to compare to for disequality
2054      * @return true if the iterators are disequal
2055      */
2056     bool operator!=(const const_iterator& it) const;
2057
2058     /**
2059      * Increment operator (prefix).
2060      * @return a reference to the iterator after incrementing by one
2061      */
2062     const_iterator& operator++();
2063
2064     /**
2065      * Increment operator (postfix).
2066      * @return a reference to the iterator after incrementing by one
2067      */
2068     const_iterator operator++(int);
2069
2070     /**
2071      * Dereference operator.
2072      * @return a reference to the selector this iterator points to
2073      */
2074     const DatatypeSelector& operator*() const;
2075
2076     /**
2077      * Dereference operator.
2078      * @return a pointer to the selector this iterator points to
2079      */
2080     const DatatypeSelector* operator->() const;
2081
2082    private:
2083     /**
2084      * Constructor.
2085      * @param slv the associated Solver object
2086      * @param ctor the internal datatype constructor to iterate over
2087      * @param begin true if this is a begin() iterator
2088      */
2089     const_iterator(const Solver* slv,
2090                    const cvc5::DTypeConstructor& ctor,
2091                    bool begin);
2092
2093     /**
2094      * The associated solver object.
2095      */
2096     const Solver* d_solver;
2097
2098     /**
2099      * A pointer to the list of selectors of the internal datatype
2100      * constructor to iterate over.
2101      * This pointer is maintained for operators == and != only.
2102      */
2103     const void* d_int_stors;
2104
2105     /** The list of datatype selector (wrappers) to iterate over. */
2106     std::vector<DatatypeSelector> d_stors;
2107
2108     /** The current index of the iterator. */
2109     size_t d_idx;
2110   };
2111
2112   /**
2113    * @return an iterator to the first selector of this constructor
2114    */
2115   const_iterator begin() const;
2116
2117   /**
2118    * @return an iterator to one-off-the-last selector of this constructor
2119    */
2120   const_iterator end() const;
2121
2122  private:
2123   /**
2124    * Constructor.
2125    * @param slv the associated solver instance
2126    * @param ctor the internal datatype constructor to be wrapped
2127    * @return the DatatypeConstructor
2128    */
2129   DatatypeConstructor(const Solver* slv, const cvc5::DTypeConstructor& ctor);
2130
2131   /**
2132    * Return selector for name.
2133    * @param name The name of selector to find
2134    * @return the selector object for the name
2135    */
2136   DatatypeSelector getSelectorForName(const std::string& name) const;
2137
2138   /**
2139    * Helper for isNull checks. This prevents calling an API function with
2140    * CVC5_API_CHECK_NOT_NULL
2141    */
2142   bool isNullHelper() const;
2143
2144   /**
2145    * The associated solver object.
2146    */
2147   const Solver* d_solver;
2148
2149   /**
2150    * The internal datatype constructor wrapped by this datatype constructor.
2151    * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
2152    *       not ref counted.
2153    */
2154   std::shared_ptr<cvc5::DTypeConstructor> d_ctor;
2155 };
2156
2157 /**
2158  * A cvc5 datatype.
2159  */
2160 class CVC5_EXPORT Datatype
2161 {
2162   friend class Solver;
2163   friend class Sort;
2164
2165  public:
2166   /** Constructor. */
2167   Datatype();
2168
2169   /**
2170    * Destructor.
2171    */
2172   ~Datatype();
2173
2174   /**
2175    * Get the datatype constructor at a given index.
2176    * @param idx the index of the datatype constructor to return
2177    * @return the datatype constructor with the given index
2178    */
2179   DatatypeConstructor operator[](size_t idx) const;
2180
2181   /**
2182    * Get the datatype constructor with the given name.
2183    * This is a linear search through the constructors, so in case of multiple,
2184    * similarly-named constructors, the first is returned.
2185    * @param name the name of the datatype constructor
2186    * @return the datatype constructor with the given name
2187    */
2188   DatatypeConstructor operator[](const std::string& name) const;
2189   DatatypeConstructor getConstructor(const std::string& name) const;
2190
2191   /**
2192    * Get a term representing the datatype constructor with the given name.
2193    * This is a linear search through the constructors, so in case of multiple,
2194    * similarly-named constructors, the
2195    * first is returned.
2196    */
2197   Term getConstructorTerm(const std::string& name) const;
2198
2199   /**
2200    * Get the datatype constructor with the given name.
2201    * This is a linear search through the constructors and their selectors, so
2202    * in case of multiple, similarly-named selectors, the first is returned.
2203    * @param name the name of the datatype selector
2204    * @return the datatype selector with the given name
2205    */
2206   DatatypeSelector getSelector(const std::string& name) const;
2207
2208   /** @return the name of this Datatype. */
2209   std::string getName() const;
2210
2211   /** @return the number of constructors for this Datatype. */
2212   size_t getNumConstructors() const;
2213
2214   /** @return true if this datatype is parametric */
2215   bool isParametric() const;
2216
2217   /** @return true if this datatype corresponds to a co-datatype */
2218   bool isCodatatype() const;
2219
2220   /** @return true if this datatype corresponds to a tuple */
2221   bool isTuple() const;
2222
2223   /** @return true if this datatype corresponds to a record */
2224   bool isRecord() const;
2225
2226   /** @return true if this datatype is finite */
2227   bool isFinite() const;
2228
2229   /**
2230    * Is this datatype well-founded? If this datatype is not a codatatype,
2231    * this returns false if there are no values of this datatype that are of
2232    * finite size.
2233    *
2234    * @return true if this datatype is well-founded
2235    */
2236   bool isWellFounded() const;
2237
2238   /**
2239    * Does this datatype have nested recursion? This method returns false if a
2240    * value of this datatype includes a subterm of its type that is nested
2241    * beneath a non-datatype type constructor. For example, a datatype
2242    * T containing a constructor having a selector with range type (Set T) has
2243    * nested recursion.
2244    *
2245    * @return true if this datatype has nested recursion
2246    */
2247   bool hasNestedRecursion() const;
2248
2249   /**
2250    * @return true if this Datatype is a null object
2251    */
2252   bool isNull() const;
2253
2254   /**
2255    * @return a string representation of this datatype
2256    */
2257   std::string toString() const;
2258
2259   /**
2260    * Iterator for the constructors of a datatype.
2261    */
2262   class const_iterator
2263   {
2264     friend class Datatype;  // to access constructor
2265
2266    public:
2267     /* The following types are required by trait std::iterator_traits */
2268
2269     /** Iterator tag */
2270     using iterator_category = std::forward_iterator_tag;
2271
2272     /** The type of the item */
2273     using value_type = Datatype;
2274
2275     /** The pointer type of the item */
2276     using pointer = const Datatype*;
2277
2278     /** The reference type of the item */
2279     using reference = const Datatype&;
2280
2281     /** The type returned when two iterators are subtracted */
2282     using difference_type = std::ptrdiff_t;
2283
2284     /* End of std::iterator_traits required types */
2285
2286     /** Nullary constructor (required for Cython). */
2287     const_iterator();
2288
2289     /**
2290      * Assignment operator.
2291      * @param it the iterator to assign to
2292      * @return the reference to the iterator after assignment
2293      */
2294     const_iterator& operator=(const const_iterator& it);
2295
2296     /**
2297      * Equality operator.
2298      * @param it the iterator to compare to for equality
2299      * @return true if the iterators are equal
2300      */
2301     bool operator==(const const_iterator& it) const;
2302
2303     /**
2304      * Disequality operator.
2305      * @param it the iterator to compare to for disequality
2306      * @return true if the iterators are disequal
2307      */
2308     bool operator!=(const const_iterator& it) const;
2309
2310     /**
2311      * Increment operator (prefix).
2312      * @return a reference to the iterator after incrementing by one
2313      */
2314     const_iterator& operator++();
2315
2316     /**
2317      * Increment operator (postfix).
2318      * @return a reference to the iterator after incrementing by one
2319      */
2320     const_iterator operator++(int);
2321
2322     /**
2323      * Dereference operator.
2324      * @return a reference to the constructor this iterator points to
2325      */
2326     const DatatypeConstructor& operator*() const;
2327
2328     /**
2329      * Dereference operator.
2330      * @return a pointer to the constructor this iterator points to
2331      */
2332     const DatatypeConstructor* operator->() const;
2333
2334    private:
2335     /**
2336      * Constructor.
2337      * @param slv the associated Solver object
2338      * @param dtype the internal datatype to iterate over
2339      * @param begin true if this is a begin() iterator
2340      */
2341     const_iterator(const Solver* slv, const cvc5::DType& dtype, bool begin);
2342
2343     /**
2344      * The associated solver object.
2345      */
2346     const Solver* d_solver;
2347
2348     /**
2349      * A pointer to the list of constructors of the internal datatype
2350      * to iterate over.
2351      * This pointer is maintained for operators == and != only.
2352      */
2353     const void* d_int_ctors;
2354
2355     /** The list of datatype constructor (wrappers) to iterate over. */
2356     std::vector<DatatypeConstructor> d_ctors;
2357
2358     /** The current index of the iterator. */
2359     size_t d_idx;
2360   };
2361
2362   /**
2363    * @return an iterator to the first constructor of this datatype
2364    */
2365   const_iterator begin() const;
2366
2367   /**
2368    * @return an iterator to one-off-the-last constructor of this datatype
2369    */
2370   const_iterator end() const;
2371
2372  private:
2373   /**
2374    * Constructor.
2375    * @param slv the associated solver instance
2376    * @param dtype the internal datatype to be wrapped
2377    * @return the Datatype
2378    */
2379   Datatype(const Solver* slv, const cvc5::DType& dtype);
2380
2381   /**
2382    * Return constructor for name.
2383    * @param name The name of constructor to find
2384    * @return the constructor object for the name
2385    */
2386   DatatypeConstructor getConstructorForName(const std::string& name) const;
2387
2388   /**
2389    * Return selector for name.
2390    * @param name The name of selector to find
2391    * @return the selector object for the name
2392    */
2393   DatatypeSelector getSelectorForName(const std::string& name) const;
2394
2395   /**
2396    * Helper for isNull checks. This prevents calling an API function with
2397    * CVC5_API_CHECK_NOT_NULL
2398    */
2399   bool isNullHelper() const;
2400
2401   /**
2402    * The associated solver object.
2403    */
2404   const Solver* d_solver;
2405
2406   /**
2407    * The internal datatype wrapped by this datatype.
2408    * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
2409    *       not ref counted.
2410    */
2411   std::shared_ptr<cvc5::DType> d_dtype;
2412 };
2413
2414 /**
2415  * Serialize a datatype declaration to given stream.
2416  * @param out the output stream
2417  * @param dtdecl the datatype declaration to be serialized to the given stream
2418  * @return the output stream
2419  */
2420 std::ostream& operator<<(std::ostream& out,
2421                          const DatatypeDecl& dtdecl) CVC5_EXPORT;
2422
2423 /**
2424  * Serialize a datatype constructor declaration to given stream.
2425  * @param out the output stream
2426  * @param ctordecl the datatype constructor declaration to be serialized
2427  * @return the output stream
2428  */
2429 std::ostream& operator<<(std::ostream& out,
2430                          const DatatypeConstructorDecl& ctordecl) CVC5_EXPORT;
2431
2432 /**
2433  * Serialize a vector of datatype constructor declarations to given stream.
2434  * @param out the output stream
2435  * @param vector the vector of datatype constructor declarations to be
2436  * serialized to the given stream
2437  * @return the output stream
2438  */
2439 std::ostream& operator<<(std::ostream& out,
2440                          const std::vector<DatatypeConstructorDecl>& vector)
2441     CVC5_EXPORT;
2442
2443 /**
2444  * Serialize a datatype to given stream.
2445  * @param out the output stream
2446  * @param dtype the datatype to be serialized to given stream
2447  * @return the output stream
2448  */
2449 std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC5_EXPORT;
2450
2451 /**
2452  * Serialize a datatype constructor to given stream.
2453  * @param out the output stream
2454  * @param ctor the datatype constructor to be serialized to given stream
2455  * @return the output stream
2456  */
2457 std::ostream& operator<<(std::ostream& out,
2458                          const DatatypeConstructor& ctor) CVC5_EXPORT;
2459
2460 /**
2461  * Serialize a datatype selector to given stream.
2462  * @param out the output stream
2463  * @param stor the datatype selector to be serialized to given stream
2464  * @return the output stream
2465  */
2466 std::ostream& operator<<(std::ostream& out,
2467                          const DatatypeSelector& stor) CVC5_EXPORT;
2468
2469 /* -------------------------------------------------------------------------- */
2470 /* Grammar                                                                    */
2471 /* -------------------------------------------------------------------------- */
2472
2473 /**
2474  * A Sygus Grammar.
2475  */
2476 class CVC5_EXPORT Grammar
2477 {
2478   friend class cvc5::Command;
2479   friend class Solver;
2480
2481  public:
2482   /**
2483    * Add \p rule to the set of rules corresponding to \p ntSymbol.
2484    * @param ntSymbol the non-terminal to which the rule is added
2485    * @param rule the rule to add
2486    */
2487   void addRule(const Term& ntSymbol, const Term& rule);
2488
2489   /**
2490    * Add \p rules to the set of rules corresponding to \p ntSymbol.
2491    * @param ntSymbol the non-terminal to which the rules are added
2492    * @param rules the rules to add
2493    */
2494   void addRules(const Term& ntSymbol, const std::vector<Term>& rules);
2495
2496   /**
2497    * Allow \p ntSymbol to be an arbitrary constant.
2498    * @param ntSymbol the non-terminal allowed to be any constant
2499    */
2500   void addAnyConstant(const Term& ntSymbol);
2501
2502   /**
2503    * Allow \p ntSymbol to be any input variable to corresponding
2504    * synth-fun/synth-inv with the same sort as \p ntSymbol.
2505    * @param ntSymbol the non-terminal allowed to be any input variable
2506    */
2507   void addAnyVariable(const Term& ntSymbol);
2508
2509   /**
2510    * @return a string representation of this grammar.
2511    */
2512   std::string toString() const;
2513
2514   /**
2515    * Nullary constructor. Needed for the Cython API.
2516    */
2517   Grammar();
2518
2519  private:
2520   /**
2521    * Constructor.
2522    * @param slv the solver that created this grammar
2523    * @param sygusVars the input variables to synth-fun/synth-var
2524    * @param ntSymbols the non-terminals of this grammar
2525    */
2526   Grammar(const Solver* slv,
2527           const std::vector<Term>& sygusVars,
2528           const std::vector<Term>& ntSymbols);
2529
2530   /**
2531    * @return the resolved datatype of the Start symbol of the grammar
2532    */
2533   Sort resolve();
2534
2535   /**
2536    * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
2537    *
2538    * \p ntsToUnres contains a mapping from non-terminal symbols to the
2539    * unresolved sorts they correspond to. This map indicates how the argument
2540    * <term> should be interpreted (instances of symbols from the domain of
2541    * \p ntsToUnres correspond to constructor arguments).
2542    *
2543    * The sygus operator that is actually added to <dt> corresponds to replacing
2544    * each occurrence of non-terminal symbols from the domain of \p ntsToUnres
2545    * with bound variables via purifySygusGTerm, and binding these variables
2546    * via a lambda.
2547    *
2548    * @param dt the non-terminal's datatype to which a constructor is added
2549    * @param term the sygus operator of the constructor
2550    * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2551    */
2552   void addSygusConstructorTerm(
2553       DatatypeDecl& dt,
2554       const Term& term,
2555       const std::unordered_map<Term, Sort>& ntsToUnres) const;
2556
2557   /**
2558    * Purify SyGuS grammar term.
2559    *
2560    * This returns a term where all occurrences of non-terminal symbols (those
2561    * in the domain of \p ntsToUnres) are replaced by fresh variables. For
2562    * each variable replaced in this way, we add the fresh variable it is
2563    * replaced with to \p args, and the unresolved sorts corresponding to the
2564    * non-terminal symbol to \p cargs (constructor args). In other words,
2565    * \p args contains the free variables in the term returned by this method
2566    * (which should be bound by a lambda), and \p cargs contains the sorts of
2567    * the arguments of the sygus constructor.
2568    *
2569    * @param term the term to purify
2570    * @param args the free variables in the term returned by this method
2571    * @param cargs the sorts of the arguments of the sygus constructor
2572    * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2573    * @return the purfied term
2574    */
2575   Term purifySygusGTerm(const Term& term,
2576                         std::vector<Term>& args,
2577                         std::vector<Sort>& cargs,
2578                         const std::unordered_map<Term, Sort>& ntsToUnres) const;
2579
2580   /**
2581    * This adds constructors to \p dt for sygus variables in \p d_sygusVars
2582    * whose sort is argument \p sort. This method should be called when the
2583    * sygus grammar term (Variable sort) is encountered.
2584    *
2585    * @param dt the non-terminal's datatype to which the constructors are added
2586    * @param sort the sort of the sygus variables to add
2587    */
2588   void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const;
2589
2590   /**
2591    * Check if \p rule contains variables that are neither parameters of
2592    * the corresponding synthFun/synthInv nor non-terminals.
2593    * @param rule the non-terminal allowed to be any constant
2594    * @return true if \p rule contains free variables and false otherwise
2595    */
2596   bool containsFreeVariables(const Term& rule) const;
2597
2598   /** The solver that created this grammar. */
2599   const Solver* d_solver;
2600   /** Input variables to the corresponding function/invariant to synthesize.*/
2601   std::vector<Term> d_sygusVars;
2602   /** The non-terminal symbols of this grammar. */
2603   std::vector<Term> d_ntSyms;
2604   /** The mapping from non-terminal symbols to their production terms. */
2605   std::unordered_map<Term, std::vector<Term>> d_ntsToTerms;
2606   /** The set of non-terminals that can be arbitrary constants. */
2607   std::unordered_set<Term> d_allowConst;
2608   /** The set of non-terminals that can be sygus variables. */
2609   std::unordered_set<Term> d_allowVars;
2610   /** Did we call resolve() before? */
2611   bool d_isResolved;
2612 };
2613
2614 /**
2615  * Serialize a grammar to given stream.
2616  * @param out the output stream
2617  * @param g the grammar to be serialized to the given output stream
2618  * @return the output stream
2619  */
2620 std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT;
2621
2622 /* -------------------------------------------------------------------------- */
2623 /* Rounding Mode for Floating-Points                                          */
2624 /* -------------------------------------------------------------------------- */
2625
2626 /**
2627  * Rounding modes for floating-point numbers.
2628  *
2629  * For many floating-point operations, infinitely precise results may not be
2630  * representable with the number of available bits. Thus, the results are
2631  * rounded in a certain way to one of the representable floating-point numbers.
2632  *
2633  * \verbatim embed:rst:leading-asterisk
2634  * These rounding modes directly follow the SMT-LIB theory for floating-point
2635  * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
2636  * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
2637  * Standard 754.
2638  * \endverbatim
2639  */
2640 enum RoundingMode
2641 {
2642   /**
2643    * Round to the nearest even number.
2644    * If the two nearest floating-point numbers bracketing an unrepresentable
2645    * infinitely precise result are equally near, the one with an even least
2646    * significant digit will be delivered.
2647    */
2648   ROUND_NEAREST_TIES_TO_EVEN,
2649   /**
2650    * Round towards positive infinity (+oo).
2651    * The result shall be the format's floating-point number (possibly +oo)
2652    * closest to and no less than the infinitely precise result.
2653    */
2654   ROUND_TOWARD_POSITIVE,
2655   /**
2656    * Round towards negative infinity (-oo).
2657    * The result shall be the format's floating-point number (possibly -oo)
2658    * closest to and no less than the infinitely precise result.
2659    */
2660   ROUND_TOWARD_NEGATIVE,
2661   /**
2662    * Round towards zero.
2663    * The result shall be the format's floating-point number closest to and no
2664    * greater in magnitude than the infinitely precise result.
2665    */
2666   ROUND_TOWARD_ZERO,
2667   /**
2668    * Round to the nearest number away from zero.
2669    * If the two nearest floating-point numbers bracketing an unrepresentable
2670    * infinitely precise result are equally near, the one with larger magnitude
2671    * will be selected.
2672    */
2673   ROUND_NEAREST_TIES_TO_AWAY,
2674 };
2675
2676 }  // namespace cvc5::api
2677
2678 namespace std {
2679
2680 /**
2681  * Hash function for RoundingModes.
2682  */
2683 template <>
2684 struct CVC5_EXPORT hash<cvc5::api::RoundingMode>
2685 {
2686   size_t operator()(cvc5::api::RoundingMode rm) const;
2687 };
2688 }  // namespace std
2689 namespace cvc5::api {
2690
2691 /* -------------------------------------------------------------------------- */
2692 /* Options                                                                    */
2693 /* -------------------------------------------------------------------------- */
2694
2695 /**
2696  * Provides access to options that can not be communicated via the regular
2697  * getOption() or getOptionInfo() methods. This class does not store the options
2698  * itself, but only acts as a wrapper to the solver object. It can thus no
2699  * longer be used after the solver object has been destroyed.
2700  */
2701 class CVC5_EXPORT DriverOptions
2702 {
2703   friend class Solver;
2704
2705  public:
2706   /** Access the solvers input stream */
2707   std::istream& in() const;
2708   /** Access the solvers error output stream */
2709   std::ostream& err() const;
2710   /** Access the solvers output stream */
2711   std::ostream& out() const;
2712
2713  private:
2714   DriverOptions(const Solver& solver);
2715   const Solver& d_solver;
2716 };
2717
2718 /**
2719  * Holds some description about a particular option, including its name, its
2720  * aliases, whether the option was explicitly set by the user, and information
2721  * concerning its value. The `valueInfo` member holds any of the following
2722  * alternatives:
2723  * - VoidInfo if the option holds no value (or the value has no native type)
2724  * - ValueInfo<T> if the option is of type bool or std::string, holds the
2725  *   current value and the default value.
2726  * - NumberInfo<T> if the option is of type int64_t, uint64_t or double, holds
2727  *   the current and default value, as well as the minimum and maximum.
2728  * - ModeInfo if the option is a mode option, holds the current and default
2729  *   values, as well as a list of valid modes.
2730  * Additionally, this class provides convenience functions to obtain the
2731  * current value of an option in a type-safe manner using boolValue(),
2732  * stringValue(), intValue(), uintValue() and doubleValue(). They assert that
2733  * the option has the respective type and return the current value.
2734  */
2735 struct CVC5_EXPORT OptionInfo
2736 {
2737   /** Has no value information */
2738   struct VoidInfo {};
2739   /** Has the current and the default value */
2740   template <typename T>
2741   struct ValueInfo
2742   {
2743     T defaultValue;
2744     T currentValue;
2745   };
2746   /** Default value, current value, minimum and maximum of a numeric value */
2747   template <typename T>
2748   struct NumberInfo
2749   {
2750     T defaultValue;
2751     T currentValue;
2752     std::optional<T> minimum;
2753     std::optional<T> maximum;
2754   };
2755   /** Default value, current value and choices of a mode option */
2756   struct ModeInfo
2757   {
2758     std::string defaultValue;
2759     std::string currentValue;
2760     std::vector<std::string> modes;
2761   };
2762
2763   /** The option name */
2764   std::string name;
2765   /** The option name aliases */
2766   std::vector<std::string> aliases;
2767   /** Whether the option was explicitly set by the user */
2768   bool setByUser;
2769   /** The option value information */
2770   std::variant<VoidInfo,
2771                ValueInfo<bool>,
2772                ValueInfo<std::string>,
2773                NumberInfo<int64_t>,
2774                NumberInfo<uint64_t>,
2775                NumberInfo<double>,
2776                ModeInfo>
2777       valueInfo;
2778   /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
2779    */
2780   bool boolValue() const;
2781   /** Obtain the current value as a string. Asserts that valueInfo holds a
2782    * string. */
2783   std::string stringValue() const;
2784   /** Obtain the current value as as int. Asserts that valueInfo holds an int.
2785    */
2786   int64_t intValue() const;
2787   /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
2788    */
2789   uint64_t uintValue() const;
2790   /** Obtain the current value as a double. Asserts that valueInfo holds a
2791    * double. */
2792   double doubleValue() const;
2793 };
2794
2795 /**
2796  * Print a `OptionInfo` object to an ``std::ostream``.
2797  */
2798 std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;
2799
2800 /* -------------------------------------------------------------------------- */
2801 /* Statistics                                                                 */
2802 /* -------------------------------------------------------------------------- */
2803
2804 /**
2805  * Represents a snapshot of a single statistic value.
2806  * A value can be of type `int64_t`, `double`, `std::string` or a histogram
2807  * (`std::map<std::string, uint64_t>`).
2808  * The value type can be queried (using `isInt()`, `isDouble()`, etc.) and
2809  * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
2810  * It is possible to query whether this statistic is an expert statistic by
2811  * `isExpert()` and whether its value is the default value by `isDefault()`.
2812  */
2813 class CVC5_EXPORT Stat
2814 {
2815   struct StatData;
2816
2817  public:
2818   friend class Statistics;
2819   friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
2820   /** Representation of a histogram: maps names to frequencies. */
2821   using HistogramData = std::map<std::string, uint64_t>;
2822   /** Can only be obtained from a `Statistics` object. */
2823   Stat() = delete;
2824   /** Copy constructor */
2825   Stat(const Stat& s);
2826   /** Destructor */
2827   ~Stat();
2828   /** Copy assignment */
2829   Stat& operator=(const Stat& s);
2830
2831   /**
2832    * Is this value intended for experts only?
2833    * @return Whether this is an expert statistic.
2834    */
2835   bool isExpert() const;
2836   /**
2837    * Does this value hold the default value?
2838    * @return Whether this is a defaulted statistic.
2839    */
2840   bool isDefault() const;
2841
2842   /**
2843    * Is this value an integer?
2844    * @return Whether the value is an integer.
2845    */
2846   bool isInt() const;
2847   /**
2848    * Return the integer value.
2849    * @return The integer value.
2850    */
2851   int64_t getInt() const;
2852   /**
2853    * Is this value a double?
2854    * @return Whether the value is a double.
2855    */
2856   bool isDouble() const;
2857   /**
2858    * Return the double value.
2859    * @return The double value.
2860    */
2861   double getDouble() const;
2862   /**
2863    * Is this value a string?
2864    * @return Whether the value is a string.
2865    */
2866   bool isString() const;
2867   /**
2868    * Return the string value.
2869    * @return The string value.
2870    */
2871   const std::string& getString() const;
2872   /**
2873    * Is this value a histogram?
2874    * @return Whether the value is a histogram.
2875    */
2876   bool isHistogram() const;
2877   /**
2878    * Return the histogram value.
2879    * @return The histogram value.
2880    */
2881   const HistogramData& getHistogram() const;
2882
2883  private:
2884   Stat(bool expert, bool def, StatData&& sd);
2885   /** Whether this statistic is only meant for experts */
2886   bool d_expert;
2887   /** Whether this statistic has the default value */
2888   bool d_default;
2889   std::unique_ptr<StatData> d_data;
2890 };
2891
2892 /**
2893  * Print a `Stat` object to an ``std::ostream``.
2894  */
2895 std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT;
2896
2897 /**
2898  * Represents a snapshot of the solver statistics.
2899  * Once obtained, an instance of this class is independent of the `Solver`
2900  * object: it will not change when the solvers internal statistics do, it
2901  * will not be invalidated if the solver is destroyed.
2902  * Iterating on this class (via `begin()` and `end()`) shows only public
2903  * statistics that have been changed. By passing appropriate flags to
2904  * `begin()`, statistics that are expert, defaulted, or both, can be
2905  * included as well. A single statistic value is represented as `Stat`.
2906  */
2907 class CVC5_EXPORT Statistics
2908 {
2909  public:
2910   friend class Solver;
2911   /** How the statistics are stored internally. */
2912   using BaseType = std::map<std::string, Stat>;
2913
2914   /** Custom iterator to hide certain statistics from regular iteration */
2915   class CVC5_EXPORT iterator
2916   {
2917    public:
2918     friend class Statistics;
2919     BaseType::const_reference operator*() const;
2920     BaseType::const_pointer operator->() const;
2921     iterator& operator++();
2922     iterator operator++(int);
2923     iterator& operator--();
2924     iterator operator--(int);
2925     bool operator==(const iterator& rhs) const;
2926     bool operator!=(const iterator& rhs) const;
2927
2928    private:
2929     iterator(BaseType::const_iterator it,
2930              const BaseType& base,
2931              bool expert,
2932              bool defaulted);
2933     bool isVisible() const;
2934     BaseType::const_iterator d_it;
2935     const BaseType* d_base;
2936     bool d_showExpert = false;
2937     bool d_showDefault = false;
2938   };
2939
2940   /**
2941    * Retrieve the statistic with the given name.
2942    * Asserts that a statistic with the given name actually exists and throws
2943    * a `CVC5ApiRecoverableException` if it does not.
2944    * @param name Name of the statistic.
2945    * @return The statistic with the given name.
2946    */
2947   const Stat& get(const std::string& name);
2948   /**
2949    * Begin iteration over the statistics values.
2950    * By default, only entries that are public (non-expert) and have been set
2951    * are visible while the others are skipped.
2952    * @param expert If set to true, expert statistics are shown as well.
2953    * @param defaulted If set to true, defaulted statistics are shown as well.
2954    */
2955   iterator begin(bool expert = false, bool defaulted = false) const;
2956   /** End iteration */
2957   iterator end() const;
2958
2959  private:
2960   Statistics() = default;
2961   Statistics(const StatisticsRegistry& reg);
2962   /** Internal data */
2963   BaseType d_stats;
2964 };
2965 std::ostream& operator<<(std::ostream& out,
2966                          const Statistics& stats) CVC5_EXPORT;
2967
2968 /* -------------------------------------------------------------------------- */
2969 /* Solver                                                                     */
2970 /* -------------------------------------------------------------------------- */
2971
2972 /**
2973  * A cvc5 solver.
2974  */
2975 class CVC5_EXPORT Solver
2976 {
2977   friend class Datatype;
2978   friend class DatatypeDecl;
2979   friend class DatatypeConstructor;
2980   friend class DatatypeConstructorDecl;
2981   friend class DatatypeSelector;
2982   friend class DriverOptions;
2983   friend class Grammar;
2984   friend class Op;
2985   friend class cvc5::Command;
2986   friend class cvc5::main::CommandExecutor;
2987   friend class Sort;
2988   friend class Term;
2989
2990  private:
2991   /*
2992    * Constructs a solver with the given original options. This should only be
2993    * used internally when the Solver is reset.
2994    */
2995   Solver(std::unique_ptr<Options>&& original);
2996
2997  public:
2998   /* .................................................................... */
2999   /* Constructors/Destructors                                             */
3000   /* .................................................................... */
3001
3002   /**
3003    * Constructor.
3004    * @return the Solver
3005    */
3006   Solver();
3007
3008   /**
3009    * Destructor.
3010    */
3011   ~Solver();
3012
3013   /**
3014    * Disallow copy/assignment.
3015    */
3016   Solver(const Solver&) = delete;
3017   Solver& operator=(const Solver&) = delete;
3018
3019   /* .................................................................... */
3020   /* Sorts Handling                                                       */
3021   /* .................................................................... */
3022
3023   /**
3024    * @return sort null
3025    */
3026   Sort getNullSort() const;
3027
3028   /**
3029    * @return sort Boolean
3030    */
3031   Sort getBooleanSort() const;
3032
3033   /**
3034    * @return sort Integer (in cvc5, Integer is a subtype of Real)
3035    */
3036   Sort getIntegerSort() const;
3037
3038   /**
3039    * @return sort Real
3040    */
3041   Sort getRealSort() const;
3042
3043   /**
3044    * @return sort RegExp
3045    */
3046   Sort getRegExpSort() const;
3047
3048   /**
3049    * @return sort RoundingMode
3050    */
3051   Sort getRoundingModeSort() const;
3052
3053   /**
3054    * @return sort String
3055    */
3056   Sort getStringSort() const;
3057
3058   /**
3059    * Create an array sort.
3060    * @param indexSort the array index sort
3061    * @param elemSort the array element sort
3062    * @return the array sort
3063    */
3064   Sort mkArraySort(const Sort& indexSort, const Sort& elemSort) const;
3065
3066   /**
3067    * Create a bit-vector sort.
3068    * @param size the bit-width of the bit-vector sort
3069    * @return the bit-vector sort
3070    */
3071   Sort mkBitVectorSort(uint32_t size) const;
3072
3073   /**
3074    * Create a floating-point sort.
3075    * @param exp the bit-width of the exponent of the floating-point sort.
3076    * @param sig the bit-width of the significand of the floating-point sort.
3077    */
3078   Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const;
3079
3080   /**
3081    * Create a datatype sort.
3082    * @param dtypedecl the datatype declaration from which the sort is created
3083    * @return the datatype sort
3084    */
3085   Sort mkDatatypeSort(const DatatypeDecl& dtypedecl) const;
3086
3087   /**
3088    * Create a vector of datatype sorts. The names of the datatype declarations
3089    * must be distinct.
3090    *
3091    * @param dtypedecls the datatype declarations from which the sort is created
3092    * @return the datatype sorts
3093    */
3094   std::vector<Sort> mkDatatypeSorts(
3095       const std::vector<DatatypeDecl>& dtypedecls) const;
3096
3097   /**
3098    * Create a vector of datatype sorts using unresolved sorts. The names of
3099    * the datatype declarations in dtypedecls must be distinct.
3100    *
3101    * This method is called when the DatatypeDecl objects dtypedecls have been
3102    * built using "unresolved" sorts.
3103    *
3104    * We associate each sort in unresolvedSorts with exactly one datatype from
3105    * dtypedecls. In particular, it must have the same name as exactly one
3106    * datatype declaration in dtypedecls.
3107    *
3108    * When constructing datatypes, unresolved sorts are replaced by the datatype
3109    * sort constructed for the datatype declaration it is associated with.
3110    *
3111    * @param dtypedecls the datatype declarations from which the sort is created
3112    * @param unresolvedSorts the list of unresolved sorts
3113    * @return the datatype sorts
3114    */
3115   std::vector<Sort> mkDatatypeSorts(
3116       const std::vector<DatatypeDecl>& dtypedecls,
3117       const std::set<Sort>& unresolvedSorts) const;
3118
3119   /**
3120    * Create function sort.
3121    * @param domain the sort of the function argument
3122    * @param codomain the sort of the function return value
3123    * @return the function sort
3124    */
3125   Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const;
3126
3127   /**
3128    * Create function sort.
3129    * @param sorts the sort of the function arguments
3130    * @param codomain the sort of the function return value
3131    * @return the function sort
3132    */
3133   Sort mkFunctionSort(const std::vector<Sort>& sorts,
3134                       const Sort& codomain) const;
3135
3136   /**
3137    * Create a sort parameter.
3138    * @param symbol the name of the sort
3139    * @return the sort parameter
3140    */
3141   Sort mkParamSort(const std::string& symbol) const;
3142
3143   /**
3144    * Create a predicate sort.
3145    * @param sorts the list of sorts of the predicate
3146    * @return the predicate sort
3147    */
3148   Sort mkPredicateSort(const std::vector<Sort>& sorts) const;
3149
3150   /**
3151    * Create a record sort
3152    * @param fields the list of fields of the record
3153    * @return the record sort
3154    */
3155   Sort mkRecordSort(
3156       const std::vector<std::pair<std::string, Sort>>& fields) const;
3157
3158   /**
3159    * Create a set sort.
3160    * @param elemSort the sort of the set elements
3161    * @return the set sort
3162    */
3163   Sort mkSetSort(const Sort& elemSort) const;
3164
3165   /**
3166    * Create a bag sort.
3167    * @param elemSort the sort of the bag elements
3168    * @return the bag sort
3169    */
3170   Sort mkBagSort(const Sort& elemSort) const;
3171
3172   /**
3173    * Create a sequence sort.
3174    * @param elemSort the sort of the sequence elements
3175    * @return the sequence sort
3176    */
3177   Sort mkSequenceSort(const Sort& elemSort) const;
3178
3179   /**
3180    * Create an uninterpreted sort.
3181    * @param symbol the name of the sort
3182    * @return the uninterpreted sort
3183    */
3184   Sort mkUninterpretedSort(const std::string& symbol) const;
3185
3186   /**
3187    * Create a sort constructor sort.
3188    * @param symbol the symbol of the sort
3189    * @param arity the arity of the sort
3190    * @return the sort constructor sort
3191    */
3192   Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const;
3193
3194   /**
3195    * Create a tuple sort.
3196    * @param sorts of the elements of the tuple
3197    * @return the tuple sort
3198    */
3199   Sort mkTupleSort(const std::vector<Sort>& sorts) const;
3200
3201   /* .................................................................... */
3202   /* Create Terms                                                         */
3203   /* .................................................................... */
3204
3205   /**
3206    * Create 0-ary term of given kind.
3207    * @param kind the kind of the term
3208    * @return the Term
3209    */
3210   Term mkTerm(Kind kind) const;
3211
3212   /**
3213    * Create a unary term of given kind.
3214    * @param kind the kind of the term
3215    * @param child the child of the term
3216    * @return the Term
3217    */
3218   Term mkTerm(Kind kind, const Term& child) const;
3219
3220   /**
3221    * Create binary term of given kind.
3222    * @param kind the kind of the term
3223    * @param child1 the first child of the term
3224    * @param child2 the second child of the term
3225    * @return the Term
3226    */
3227   Term mkTerm(Kind kind, const Term& child1, const Term& child2) const;
3228
3229   /**
3230    * Create ternary term of given kind.
3231    * @param kind the kind of the term
3232    * @param child1 the first child of the term
3233    * @param child2 the second child of the term
3234    * @param child3 the third child of the term
3235    * @return the Term
3236    */
3237   Term mkTerm(Kind kind,
3238               const Term& child1,
3239               const Term& child2,
3240               const Term& child3) const;
3241
3242   /**
3243    * Create n-ary term of given kind.
3244    * @param kind the kind of the term
3245    * @param children the children of the term
3246    * @return the Term
3247    */
3248   Term mkTerm(Kind kind, const std::vector<Term>& children) const;
3249
3250   /**
3251    * Create nullary term of given kind from a given operator.
3252    * Create operators with mkOp().
3253    * @param op the operator
3254    * @return the Term
3255    */
3256   Term mkTerm(const Op& op) const;
3257
3258   /**
3259    * Create unary term of given kind from a given operator.
3260    * Create operators with mkOp().
3261    * @param op the operator
3262    * @param child the child of the term
3263    * @return the Term
3264    */
3265   Term mkTerm(const Op& op, const Term& child) const;
3266
3267   /**
3268    * Create binary term of given kind from a given operator.
3269    * Create operators with mkOp().
3270    * @param op the operator
3271    * @param child1 the first child of the term
3272    * @param child2 the second child of the term
3273    * @return the Term
3274    */
3275   Term mkTerm(const Op& op, const Term& child1, const Term& child2) const;
3276
3277   /**
3278    * Create ternary term of given kind from a given operator.
3279    * Create operators with mkOp().
3280    * @param op the operator
3281    * @param child1 the first child of the term
3282    * @param child2 the second child of the term
3283    * @param child3 the third child of the term
3284    * @return the Term
3285    */
3286   Term mkTerm(const Op& op,
3287               const Term& child1,
3288               const Term& child2,
3289               const Term& child3) const;
3290
3291   /**
3292    * Create n-ary term of given kind from a given operator.
3293    * Create operators with mkOp().
3294    * @param op the operator
3295    * @param children the children of the term
3296    * @return the Term
3297    */
3298   Term mkTerm(const Op& op, const std::vector<Term>& children) const;
3299
3300   /**
3301    * Create a tuple term. Terms are automatically converted if sorts are
3302    * compatible.
3303    * @param sorts The sorts of the elements in the tuple
3304    * @param terms The elements in the tuple
3305    * @return the tuple Term
3306    */
3307   Term mkTuple(const std::vector<Sort>& sorts,
3308                const std::vector<Term>& terms) const;
3309
3310   /* .................................................................... */
3311   /* Create Operators                                                     */
3312   /* .................................................................... */
3313
3314   /**
3315    * Create an operator for a builtin Kind
3316    * The Kind may not be the Kind for an indexed operator
3317    *   (e.g. BITVECTOR_EXTRACT)
3318    * Note: in this case, the Op simply wraps the Kind.
3319    * The Kind can be used in mkTerm directly without
3320    *   creating an op first.
3321    * @param kind the kind to wrap
3322    */
3323   Op mkOp(Kind kind) const;
3324
3325   /**
3326    * Create operator of kind:
3327    *   - DIVISIBLE (to support arbitrary precision integers)
3328    * See enum Kind for a description of the parameters.
3329    * @param kind the kind of the operator
3330    * @param arg the string argument to this operator
3331    */
3332   Op mkOp(Kind kind, const std::string& arg) const;
3333
3334   /**
3335    * Create operator of kind:
3336    *   - DIVISIBLE
3337    *   - BITVECTOR_REPEAT
3338    *   - BITVECTOR_ZERO_EXTEND
3339    *   - BITVECTOR_SIGN_EXTEND
3340    *   - BITVECTOR_ROTATE_LEFT
3341    *   - BITVECTOR_ROTATE_RIGHT
3342    *   - INT_TO_BITVECTOR
3343    *   - FLOATINGPOINT_TO_UBV
3344    *   - FLOATINGPOINT_TO_UBV_TOTAL
3345    *   - FLOATINGPOINT_TO_SBV
3346    *   - FLOATINGPOINT_TO_SBV_TOTAL
3347    *   - TUPLE_UPDATE
3348    * See enum Kind for a description of the parameters.
3349    * @param kind the kind of the operator
3350    * @param arg the uint32_t argument to this operator
3351    */
3352   Op mkOp(Kind kind, uint32_t arg) const;
3353
3354   /**
3355    * Create operator of Kind:
3356    *   - BITVECTOR_EXTRACT
3357    *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
3358    *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT
3359    *   - FLOATINGPOINT_TO_FP_REAL
3360    *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
3361    *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
3362    *   - FLOATINGPOINT_TO_FP_GENERIC
3363    * See enum Kind for a description of the parameters.
3364    * @param kind the kind of the operator
3365    * @param arg1 the first uint32_t argument to this operator
3366    * @param arg2 the second uint32_t argument to this operator
3367    */
3368   Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
3369
3370   /**
3371    * Create operator of Kind:
3372    *   - TUPLE_PROJECT
3373    * See enum Kind for a description of the parameters.
3374    * @param kind the kind of the operator
3375    * @param args the arguments (indices) of the operator
3376    */
3377   Op mkOp(Kind kind, const std::vector<uint32_t>& args) const;
3378
3379   /* .................................................................... */
3380   /* Create Constants                                                     */
3381   /* .................................................................... */
3382
3383   /**
3384    * Create a Boolean true constant.
3385    * @return the true constant
3386    */
3387   Term mkTrue() const;
3388
3389   /**
3390    * Create a Boolean false constant.
3391    * @return the false constant
3392    */
3393   Term mkFalse() const;
3394
3395   /**
3396    * Create a Boolean constant.
3397    * @return the Boolean constant
3398    * @param val the value of the constant
3399    */
3400   Term mkBoolean(bool val) const;
3401
3402   /**
3403    * Create a constant representing the number Pi.
3404    * @return a constant representing Pi
3405    */
3406   Term mkPi() const;
3407   /**
3408    * Create an integer constant from a string.
3409    * @param s the string representation of the constant, may represent an
3410    *          integer (e.g., "123").
3411    * @return a constant of sort Integer assuming 's' represents an integer)
3412    */
3413   Term mkInteger(const std::string& s) const;
3414
3415   /**
3416    * Create an integer constant from a c++ int.
3417    * @param val the value of the constant
3418    * @return a constant of sort Integer
3419    */
3420   Term mkInteger(int64_t val) const;
3421
3422   /**
3423    * Create a real constant from a string.
3424    * @param s the string representation of the constant, may represent an
3425    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
3426    * @return a constant of sort Real
3427    */
3428   Term mkReal(const std::string& s) const;
3429
3430   /**
3431    * Create a real constant from an integer.
3432    * @param val the value of the constant
3433    * @return a constant of sort Integer
3434    */
3435   Term mkReal(int64_t val) const;
3436
3437   /**
3438    * Create a real constant from a rational.
3439    * @param num the value of the numerator
3440    * @param den the value of the denominator
3441    * @return a constant of sort Real
3442    */
3443   Term mkReal(int64_t num, int64_t den) const;
3444
3445   /**
3446    * Create a regular expression all (re.all) term.
3447    * @return the all term
3448    */
3449   Term mkRegexpAll() const;
3450
3451   /**
3452    * Create a regular expression allchar (re.allchar) term.
3453    * @return the allchar term
3454    */
3455   Term mkRegexpAllchar() const;
3456
3457   /**
3458    * Create a regular expression none (re.none) term.
3459    * @return the none term
3460    */
3461   Term mkRegexpNone() const;
3462
3463   /**
3464    * Create a constant representing an empty set of the given sort.
3465    * @param sort the sort of the set elements.
3466    * @return the empty set constant
3467    */
3468   Term mkEmptySet(const Sort& sort) const;
3469
3470   /**
3471    * Create a constant representing an empty bag of the given sort.
3472    * @param sort the sort of the bag elements.
3473    * @return the empty bag constant
3474    */
3475   Term mkEmptyBag(const Sort& sort) const;
3476
3477   /**
3478    * Create a separation logic empty term.
3479    * @return the separation logic empty term
3480    */
3481   Term mkSepEmp() const;
3482
3483   /**
3484    * Create a separation logic nil term.
3485    * @param sort the sort of the nil term
3486    * @return the separation logic nil term
3487    */
3488   Term mkSepNil(const Sort& sort) const;
3489
3490   /**
3491    * Create a String constant from a `std::string` which may contain SMT-LIB
3492    * compatible escape sequences like `\u1234` to encode unicode characters.
3493    * @param s the string this constant represents
3494    * @param useEscSequences determines whether escape sequences in `s` should
3495    * be converted to the corresponding unicode character
3496    * @return the String constant
3497    */
3498   Term mkString(const std::string& s, bool useEscSequences = false) const;
3499
3500   /**
3501    * Create a String constant from a `std::wstring`.
3502    * This method does not support escape sequences as `std::wstring` already
3503    * supports unicode characters.
3504    * @param s the string this constant represents
3505    * @return the String constant
3506    */
3507   Term mkString(const std::wstring& s) const;
3508
3509   /**
3510    * Create an empty sequence of the given element sort.
3511    * @param sort The element sort of the sequence.
3512    * @return the empty sequence with given element sort.
3513    */
3514   Term mkEmptySequence(const Sort& sort) const;
3515
3516   /**
3517    * Create a universe set of the given sort.
3518    * @param sort the sort of the set elements
3519    * @return the universe set constant
3520    */
3521   Term mkUniverseSet(const Sort& sort) const;
3522
3523   /**
3524    * Create a bit-vector constant of given size and value.
3525    *
3526    * Note: The given value must fit into a bit-vector of the given size.
3527    *
3528    * @param size the bit-width of the bit-vector sort
3529    * @param val the value of the constant
3530    * @return the bit-vector constant
3531    */
3532   Term mkBitVector(uint32_t size, uint64_t val = 0) const;
3533
3534   /**
3535    * Create a bit-vector constant of a given bit-width from a given string of
3536    * base 2, 10 or 16.
3537    *
3538    * Note: The given value must fit into a bit-vector of the given size.
3539    *
3540    * @param size the bit-width of the constant
3541    * @param s the string representation of the constant
3542    * @param base the base of the string representation (2, 10, or 16)
3543    * @return the bit-vector constant
3544    */
3545   Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const;
3546
3547   /**
3548    * Create a constant array with the provided constant value stored at every
3549    * index
3550    * @param sort the sort of the constant array (must be an array sort)
3551    * @param val the constant value to store (must match the sort's element sort)
3552    * @return the constant array term
3553    */
3554   Term mkConstArray(const Sort& sort, const Term& val) const;
3555
3556   /**
3557    * Create a positive infinity floating-point constant.
3558    * @param exp Number of bits in the exponent
3559    * @param sig Number of bits in the significand
3560    * @return the floating-point constant
3561    */
3562   Term mkPosInf(uint32_t exp, uint32_t sig) const;
3563
3564   /**
3565    * Create a negative infinity floating-point constant.
3566    * @param exp Number of bits in the exponent
3567    * @param sig Number of bits in the significand
3568    * @return the floating-point constant
3569    */
3570   Term mkNegInf(uint32_t exp, uint32_t sig) const;
3571
3572   /**
3573    * Create a not-a-number (NaN) floating-point constant.
3574    * @param exp Number of bits in the exponent
3575    * @param sig Number of bits in the significand
3576    * @return the floating-point constant
3577    */
3578   Term mkNaN(uint32_t exp, uint32_t sig) const;
3579
3580   /**
3581    * Create a positive zero (+0.0) floating-point constant.
3582    * @param exp Number of bits in the exponent
3583    * @param sig Number of bits in the significand
3584    * @return the floating-point constant
3585    */
3586   Term mkPosZero(uint32_t exp, uint32_t sig) const;
3587
3588   /**
3589    * Create a negative zero (-0.0) floating-point constant.
3590    * @param exp Number of bits in the exponent
3591    * @param sig Number of bits in the significand
3592    * @return the floating-point constant
3593    */
3594   Term mkNegZero(uint32_t exp, uint32_t sig) const;
3595
3596   /**
3597    * Create a roundingmode constant.
3598    * @param rm the floating point rounding mode this constant represents
3599    */
3600   Term mkRoundingMode(RoundingMode rm) const;
3601
3602   /**
3603    * Create uninterpreted constant.
3604    * @param sort Sort of the constant
3605    * @param index Index of the constant
3606    */
3607   Term mkUninterpretedConst(const Sort& sort, int32_t index) const;
3608
3609   /**
3610    * Create an abstract value constant.
3611    * The given index needs to be a positive integer in base 10.
3612    * @param index Index of the abstract value
3613    */
3614   Term mkAbstractValue(const std::string& index) const;
3615
3616   /**
3617    * Create an abstract value constant.
3618    * The given index needs to be positive.
3619    * @param index Index of the abstract value
3620    */
3621   Term mkAbstractValue(uint64_t index) const;
3622
3623   /**
3624    * Create a floating-point constant.
3625    * @param exp Size of the exponent
3626    * @param sig Size of the significand
3627    * @param val Value of the floating-point constant as a bit-vector term
3628    */
3629   Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const;
3630
3631   /**
3632    * Create a cardinality constraint for an uninterpreted sort.
3633    * @param sort the sort the cardinality constraint is for
3634    * @param upperBound the upper bound on the cardinality of the sort
3635    * @return the cardinality constraint
3636    */
3637   Term mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const;
3638
3639   /* .................................................................... */
3640   /* Create Variables                                                     */
3641   /* .................................................................... */
3642
3643   /**
3644    * Create (first-order) constant (0-arity function symbol).
3645    * SMT-LIB:
3646    * \verbatim
3647    *   ( declare-const <symbol> <sort> )
3648    *   ( declare-fun <symbol> ( ) <sort> )
3649    * \endverbatim
3650    *
3651    * @param sort the sort of the constant
3652    * @param symbol the name of the constant
3653    * @return the first-order constant
3654    */
3655   Term mkConst(const Sort& sort, const std::string& symbol) const;
3656   /**
3657    * Create (first-order) constant (0-arity function symbol), with a default
3658    * symbol name.
3659    *
3660    * @param sort the sort of the constant
3661    * @return the first-order constant
3662    */
3663   Term mkConst(const Sort& sort) const;
3664
3665   /**
3666    * Create a bound variable to be used in a binder (i.e. a quantifier, a
3667    * lambda, or a witness binder).
3668    * @param sort the sort of the variable
3669    * @param symbol the name of the variable
3670    * @return the variable
3671    */
3672   Term mkVar(const Sort& sort, const std::string& symbol = std::string()) const;
3673
3674   /* .................................................................... */
3675   /* Create datatype constructor declarations                             */
3676   /* .................................................................... */
3677
3678   DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
3679
3680   /* .................................................................... */
3681   /* Create datatype declarations                                         */
3682   /* .................................................................... */
3683
3684   /**
3685    * Create a datatype declaration.
3686    * @param name the name of the datatype
3687    * @param isCoDatatype true if a codatatype is to be constructed
3688    * @return the DatatypeDecl
3689    */
3690   DatatypeDecl mkDatatypeDecl(const std::string& name,
3691                               bool isCoDatatype = false);
3692
3693   /**
3694    * Create a datatype declaration.
3695    * Create sorts parameter with Solver::mkParamSort().
3696    * @param name the name of the datatype
3697    * @param param the sort parameter
3698    * @param isCoDatatype true if a codatatype is to be constructed
3699    * @return the DatatypeDecl
3700    */
3701   DatatypeDecl mkDatatypeDecl(const std::string& name,
3702                               Sort param,
3703                               bool isCoDatatype = false);
3704
3705   /**
3706    * Create a datatype declaration.
3707    * Create sorts parameter with Solver::mkParamSort().
3708    * @param name the name of the datatype
3709    * @param params a list of sort parameters
3710    * @param isCoDatatype true if a codatatype is to be constructed
3711    * @return the DatatypeDecl
3712    */
3713   DatatypeDecl mkDatatypeDecl(const std::string& name,
3714                               const std::vector<Sort>& params,
3715                               bool isCoDatatype = false);
3716
3717   /* .................................................................... */
3718   /* Formula Handling                                                     */
3719   /* .................................................................... */
3720
3721   /**
3722    * Simplify a formula without doing "much" work.  Does not involve
3723    * the SAT Engine in the simplification, but uses the current
3724    * definitions, assertions, and the current partial model, if one
3725    * has been constructed.  It also involves theory normalization.
3726    * @param t the formula to simplify
3727    * @return the simplified formula
3728    */
3729   Term simplify(const Term& t);
3730
3731   /**
3732    * Assert a formula.
3733    * SMT-LIB:
3734    * \verbatim
3735    *   ( assert <term> )
3736    * \endverbatim
3737    * @param term the formula to assert
3738    */
3739   void assertFormula(const Term& term) const;
3740
3741   /**
3742    * Check satisfiability.
3743    * SMT-LIB:
3744    * \verbatim
3745    *   ( check-sat )
3746    * \endverbatim
3747    * @return the result of the satisfiability check.
3748    */
3749   Result checkSat() const;
3750
3751   /**
3752    * Check satisfiability assuming the given formula.
3753    * SMT-LIB:
3754    * \verbatim
3755    *   ( check-sat-assuming ( <prop_literal> ) )
3756    * \endverbatim
3757    * @param assumption the formula to assume
3758    * @return the result of the satisfiability check.
3759    */
3760   Result checkSatAssuming(const Term& assumption) const;
3761
3762   /**
3763    * Check satisfiability assuming the given formulas.
3764    * SMT-LIB:
3765    * \verbatim
3766    *   ( check-sat-assuming ( <prop_literal>+ ) )
3767    * \endverbatim
3768    * @param assumptions the formulas to assume
3769    * @return the result of the satisfiability check.
3770    */
3771   Result checkSatAssuming(const std::vector<Term>& assumptions) const;
3772
3773   /**
3774    * Check entailment of the given formula w.r.t. the current set of assertions.
3775    * @param term the formula to check entailment for
3776    * @return the result of the entailment check.
3777    */
3778   Result checkEntailed(const Term& term) const;
3779
3780   /**
3781    * Check entailment of the given set of given formulas w.r.t. the current
3782    * set of assertions.
3783    * @param terms the terms to check entailment for
3784    * @return the result of the entailmentcheck.
3785    */
3786   Result checkEntailed(const std::vector<Term>& terms) const;
3787
3788   /**
3789    * Create datatype sort.
3790    * SMT-LIB:
3791    * \verbatim
3792    *   ( declare-datatype <symbol> <datatype_decl> )
3793    * \endverbatim
3794    * @param symbol the name of the datatype sort
3795    * @param ctors the constructor declarations of the datatype sort
3796    * @return the datatype sort
3797    */
3798   Sort declareDatatype(const std::string& symbol,
3799                        const std::vector<DatatypeConstructorDecl>& ctors) const;
3800
3801   /**
3802    * Declare n-ary function symbol.
3803    * SMT-LIB:
3804    * \verbatim
3805    *   ( declare-fun <symbol> ( <sort>* ) <sort> )
3806    * \endverbatim
3807    * @param symbol the name of the function
3808    * @param sorts the sorts of the parameters to this function
3809    * @param sort the sort of the return value of this function
3810    * @return the function
3811    */
3812   Term declareFun(const std::string& symbol,
3813                   const std::vector<Sort>& sorts,
3814                   const Sort& sort) const;
3815
3816   /**
3817    * Declare uninterpreted sort.
3818    * SMT-LIB:
3819    * \verbatim
3820    *   ( declare-sort <symbol> <numeral> )
3821    * \endverbatim
3822    * @param symbol the name of the sort
3823    * @param arity the arity of the sort
3824    * @return the sort
3825    */
3826   Sort declareSort(const std::string& symbol, uint32_t arity) const;
3827
3828   /**
3829    * Define n-ary function.
3830    * SMT-LIB:
3831    * \verbatim
3832    *   ( define-fun <function_def> )
3833    * \endverbatim
3834    * @param symbol the name of the function
3835    * @param bound_vars the parameters to this function
3836    * @param sort the sort of the return value of this function
3837    * @param term the function body
3838    * @param global determines whether this definition is global (i.e. persists
3839    *               when popping the context)
3840    * @return the function
3841    */
3842   Term defineFun(const std::string& symbol,
3843                  const std::vector<Term>& bound_vars,
3844                  const Sort& sort,
3845                  const Term& term,
3846                  bool global = false) const;
3847
3848   /**
3849    * Define recursive function.
3850    * SMT-LIB:
3851    * \verbatim
3852    * ( define-fun-rec <function_def> )
3853    * \endverbatim
3854    * @param symbol the name of the function
3855    * @param bound_vars the parameters to this function
3856    * @param sort the sort of the return value of this function
3857    * @param term the function body
3858    * @param global determines whether this definition is global (i.e. persists
3859    *               when popping the context)
3860    * @return the function
3861    */
3862   Term defineFunRec(const std::string& symbol,
3863                     const std::vector<Term>& bound_vars,
3864                     const Sort& sort,
3865                     const Term& term,
3866                     bool global = false) const;
3867
3868   /**
3869    * Define recursive function.
3870    * SMT-LIB:
3871    * \verbatim
3872    * ( define-fun-rec <function_def> )
3873    * \endverbatim
3874    * Create parameter 'fun' with mkConst().
3875    * @param fun the sorted function
3876    * @param bound_vars the parameters to this function
3877    * @param term the function body
3878    * @param global determines whether this definition is global (i.e. persists
3879    *               when popping the context)
3880    * @return the function
3881    */
3882   Term defineFunRec(const Term& fun,
3883                     const std::vector<Term>& bound_vars,
3884                     const Term& term,
3885                     bool global = false) const;
3886
3887   /**
3888    * Define recursive functions.
3889    * SMT-LIB:
3890    * \verbatim
3891    *   ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3892    * \endverbatim
3893    * Create elements of parameter 'funs' with mkConst().
3894    * @param funs the sorted functions
3895    * @param bound_vars the list of parameters to the functions
3896    * @param terms the list of function bodies of the functions
3897    * @param global determines whether this definition is global (i.e. persists
3898    *               when popping the context)
3899    * @return the function
3900    */
3901   void defineFunsRec(const std::vector<Term>& funs,
3902                      const std::vector<std::vector<Term>>& bound_vars,
3903                      const std::vector<Term>& terms,
3904                      bool global = false) const;
3905
3906   /**
3907    * Echo a given string to the given output stream.
3908    * SMT-LIB:
3909    * \verbatim
3910    * ( echo <std::string> )
3911    * \endverbatim
3912    * @param out the output stream
3913    * @param str the string to echo
3914    */
3915   void echo(std::ostream& out, const std::string& str) const;
3916
3917   /**
3918    * Get the list of asserted formulas.
3919    * SMT-LIB:
3920    * \verbatim
3921    * ( get-assertions )
3922    * \endverbatim
3923    * @return the list of asserted formulas
3924    */
3925   std::vector<Term> getAssertions() const;
3926
3927   /**
3928    * Get info from the solver.
3929    * SMT-LIB: \verbatim( get-info <info_flag> )\endverbatim
3930    * @return the info
3931    */
3932   std::string getInfo(const std::string& flag) const;
3933
3934   /**
3935    * Get the value of a given option.
3936    * SMT-LIB:
3937    * \verbatim
3938    * ( get-option <keyword> )
3939    * \endverbatim
3940    * @param option the option for which the value is queried
3941    * @return a string representation of the option value
3942    */
3943   std::string getOption(const std::string& option) const;
3944
3945   /**
3946    * Get all option names that can be used with `setOption`, `getOption` and
3947    * `getOptionInfo`.
3948    * @return all option names
3949    */
3950   std::vector<std::string> getOptionNames() const;
3951
3952   /**
3953    * Get some information about the given option. Check the `OptionInfo` class
3954    * for more details on which information is available.
3955    * @return information about the given option
3956    */
3957   OptionInfo getOptionInfo(const std::string& option) const;
3958
3959   /**
3960    * Get the driver options, which provide access to options that can not be
3961    * communicated properly via getOption() and getOptionInfo().
3962    * @return a DriverOptions object.
3963    */
3964   DriverOptions getDriverOptions() const;
3965
3966   /**
3967    * Get the set of unsat ("failed") assumptions.
3968    * SMT-LIB:
3969    * \verbatim
3970    * ( get-unsat-assumptions )
3971    * \endverbatim
3972    * Requires to enable option 'produce-unsat-assumptions'.
3973    * @return the set of unsat assumptions.
3974    */
3975   std::vector<Term> getUnsatAssumptions() const;
3976
3977   /**
3978    * Get the unsatisfiable core.
3979    * SMT-LIB:
3980    * \verbatim
3981    * ( get-unsat-core )
3982    * \endverbatim
3983    * Requires to enable option 'produce-unsat-cores'.
3984    * @return a set of terms representing the unsatisfiable core
3985    */
3986   std::vector<Term> getUnsatCore() const;
3987
3988   /**
3989    * Get a difficulty estimate for an asserted formula. This method is
3990    * intended to be called immediately after any response to a checkSat.
3991    *
3992    * @return a map from (a subset of) the input assertions to a real value that
3993    * is an estimate of how difficult each assertion was to solve. Unmentioned
3994    * assertions can be assumed to have zero difficulty.
3995    */
3996   std::map<Term, Term> getDifficulty() const;
3997
3998   /**
3999    * Get the refutation proof
4000    * SMT-LIB:
4001    * \verbatim
4002    * ( get-proof )
4003    * \endverbatim
4004    * Requires to enable option 'produce-proofs'.
4005    * @return a string representing the proof, according to the value of
4006    * proof-format-mode.
4007    */
4008   std::string getProof() const;
4009
4010   /**
4011    * Get the value of the given term in the current model.
4012    * SMT-LIB:
4013    * \verbatim
4014    * ( get-value ( <term> ) )
4015    * \endverbatim
4016    * @param term the term for which the value is queried
4017    * @return the value of the given term
4018    */
4019   Term getValue(const Term& term) const;
4020
4021   /**
4022    * Get the values of the given terms in the current model.
4023    * SMT-LIB:
4024    * \verbatim
4025    * ( get-value ( <term>+ ) )
4026    * \endverbatim
4027    * @param terms the terms for which the value is queried
4028    * @return the values of the given terms
4029    */
4030   std::vector<Term> getValue(const std::vector<Term>& terms) const;
4031
4032   /**
4033    * Get the domain elements of uninterpreted sort s in the current model. The
4034    * current model interprets s as the finite sort whose domain elements are
4035    * given in the return value of this method.
4036    *
4037    * @param s The uninterpreted sort in question
4038    * @return the domain elements of s in the current model
4039    */
4040   std::vector<Term> getModelDomainElements(const Sort& s) const;
4041
4042   /**
4043    * This returns false if the model value of free constant v was not essential
4044    * for showing the satisfiability of the last call to checkSat using the
4045    * current model. This method will only return false (for any v) if
4046    * the model-cores option has been set.
4047    *
4048    * @param v The term in question
4049    * @return true if v is a model core symbol
4050    */
4051   bool isModelCoreSymbol(const Term& v) const;
4052
4053   /**
4054    * Get the model
4055    * SMT-LIB:
4056    * \verbatim
4057    * ( get-model )
4058    * \endverbatim
4059    * Requires to enable option 'produce-models'.
4060    * @param sorts The list of uninterpreted sorts that should be printed in the
4061    * model.
4062    * @param vars The list of free constants that should be printed in the
4063    * model. A subset of these may be printed based on isModelCoreSymbol.
4064    * @return a string representing the model.
4065    */
4066   std::string getModel(const std::vector<Sort>& sorts,
4067                        const std::vector<Term>& vars) const;
4068
4069   /**
4070    * Do quantifier elimination.
4071    * SMT-LIB:
4072    * \verbatim
4073    * ( get-qe <q> )
4074    * \endverbatim
4075    * Requires a logic that supports quantifier elimination. Currently, the only
4076    * logics supported by quantifier elimination is LRA and LIA.
4077    * @param q a quantified formula of the form:
4078    *   Q x1...xn. P( x1...xn, y1...yn )
4079    * where P( x1...xn, y1...yn ) is a quantifier-free formula
4080    * @return a formula ret such that, given the current set of formulas A
4081    * asserted to this solver:
4082    *   - ( A ^ q ) and ( A ^ ret ) are equivalent
4083    *   - ret is quantifier-free formula containing only free variables in
4084    *     y1...yn.
4085    */
4086   Term getQuantifierElimination(const Term& q) const;
4087
4088   /**
4089    * Do partial quantifier elimination, which can be used for incrementally
4090    * computing the result of a quantifier elimination.
4091    * SMT-LIB:
4092    * \verbatim
4093    * ( get-qe-disjunct <q> )
4094    * \endverbatim
4095    * Requires a logic that supports quantifier elimination. Currently, the only
4096    * logics supported by quantifier elimination is LRA and LIA.
4097    * @param q a quantified formula of the form:
4098    *   Q x1...xn. P( x1...xn, y1...yn )
4099    * where P( x1...xn, y1...yn ) is a quantifier-free formula
4100    * @return a formula ret such that, given the current set of formulas A
4101    * asserted to this solver:
4102    *   - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
4103    *     exists,
4104    *   - ret is quantifier-free formula containing only free variables in
4105    *     y1...yn,
4106    *   - If Q is exists, let A^Q_n be the formula
4107    *       A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
4108    *     where for each i=1,...n, formula ret^Q_i is the result of calling
4109    *     getQuantifierEliminationDisjunct for q with the set of assertions
4110    *     A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
4111    *       A ^ ret^Q_1 ^ ... ^ ret^Q_n
4112    *     where ret^Q_i is the same as above. In either case, we have
4113    *     that ret^Q_j will eventually be true or false, for some finite j.
4114    */
4115   Term getQuantifierEliminationDisjunct(const Term& q) const;
4116
4117   /**
4118    * When using separation logic, this sets the location sort and the
4119    * datatype sort to the given ones. This method should be invoked exactly
4120    * once, before any separation logic constraints are provided.
4121    * @param locSort The location sort of the heap
4122    * @param dataSort The data sort of the heap
4123    */
4124   void declareSepHeap(const Sort& locSort, const Sort& dataSort) const;
4125
4126   /**
4127    * When using separation logic, obtain the term for the heap.
4128    * @return The term for the heap
4129    */
4130   Term getValueSepHeap() const;
4131
4132   /**
4133    * When using separation logic, obtain the term for nil.
4134    * @return The term for nil
4135    */
4136   Term getValueSepNil() const;
4137
4138   /**
4139    * Declare a symbolic pool of terms with the given initial value.
4140    * SMT-LIB:
4141    * \verbatim
4142    * ( declare-pool <symbol> <sort> ( <term>* ) )
4143    * \endverbatim
4144    * @param symbol The name of the pool
4145    * @param sort The sort of the elements of the pool.
4146    * @param initValue The initial value of the pool
4147    */
4148   Term declarePool(const std::string& symbol,
4149                    const Sort& sort,
4150                    const std::vector<Term>& initValue) const;
4151   /**
4152    * Pop (a) level(s) from the assertion stack.
4153    * SMT-LIB:
4154    * \verbatim
4155    * ( pop <numeral> )
4156    * \endverbatim
4157    * @param nscopes the number of levels to pop
4158    */
4159   void pop(uint32_t nscopes = 1) const;
4160
4161   /**
4162    * Get an interpolant
4163    * SMT-LIB:
4164    * \verbatim
4165    * ( get-interpol <conj> )
4166    * \endverbatim
4167    * Requires to enable option 'produce-interpols'.
4168    * @param conj the conjecture term
4169    * @param output a Term I such that A->I and I->B are valid, where A is the
4170    *        current set of assertions and B is given in the input by conj.
4171    * @return true if it gets I successfully, false otherwise.
4172    */
4173   bool getInterpolant(const Term& conj, Term& output) const;
4174
4175   /**
4176    * Get an interpolant
4177    * SMT-LIB:
4178    * \verbatim
4179    * ( get-interpol <conj> <g> )
4180    * \endverbatim
4181    * Requires to enable option 'produce-interpols'.
4182    * @param conj the conjecture term
4183    * @param grammar the grammar for the interpolant I
4184    * @param output a Term I such that A->I and I->B are valid, where A is the
4185    *        current set of assertions and B is given in the input by conj.
4186    * @return true if it gets I successfully, false otherwise.
4187    */
4188   bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const;
4189
4190   /**
4191    * Get an abduct.
4192    * SMT-LIB:
4193    * \verbatim
4194    * ( get-abduct <conj> )
4195    * \endverbatim
4196    * Requires enabling option 'produce-abducts'
4197    * @param conj the conjecture term
4198    * @param output a term C such that A^C is satisfiable, and A^~B^C is
4199    *        unsatisfiable, where A is the current set of assertions and B is
4200    *        given in the input by conj
4201    * @return true if it gets C successfully, false otherwise
4202    */
4203   bool getAbduct(const Term& conj, Term& output) const;
4204
4205   /**
4206    * Get an abduct.
4207    * SMT-LIB:
4208    * \verbatim
4209    * ( get-abduct <conj> <g> )
4210    * \endverbatim
4211    * Requires enabling option 'produce-abducts'
4212    * @param conj the conjecture term
4213    * @param grammar the grammar for the abduct C
4214    * @param output a term C such that A^C is satisfiable, and A^~B^C is
4215    *        unsatisfiable, where A is the current set of assertions and B is
4216    *        given in the input by conj
4217    * @return true if it gets C successfully, false otherwise
4218    */
4219   bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
4220
4221   /**
4222    * Block the current model. Can be called only if immediately preceded by a
4223    * SAT or INVALID query.
4224    * SMT-LIB:
4225    * \verbatim
4226    * ( block-model )
4227    * \endverbatim
4228    * Requires enabling 'produce-models' option and setting 'block-models' option
4229    * to a mode other than "none".
4230    */
4231   void blockModel() const;
4232
4233   /**
4234    * Block the current model values of (at least) the values in terms. Can be
4235    * called only if immediately preceded by a SAT or NOT_ENTAILED query.
4236    * SMT-LIB:
4237    * \verbatim
4238    * ( block-model-values ( <terms>+ ) )
4239    * \endverbatim
4240    * Requires enabling 'produce-models' option and setting 'block-models' option
4241    * to a mode other than "none".
4242    */
4243   void blockModelValues(const std::vector<Term>& terms) const;
4244
4245   /**
4246    * Print all instantiations made by the quantifiers module.
4247    * @param out the output stream
4248    */
4249   void printInstantiations(std::ostream& out) const;
4250
4251   /**
4252    * Push (a) level(s) to the assertion stack.
4253    * SMT-LIB:
4254    * \verbatim
4255    * ( push <numeral> )
4256    * \endverbatim
4257    * @param nscopes the number of levels to push
4258    */
4259   void push(uint32_t nscopes = 1) const;
4260
4261   /**
4262    * Remove all assertions.
4263    * SMT-LIB:
4264    * \verbatim
4265    * ( reset-assertions )
4266    * \endverbatim
4267    */
4268   void resetAssertions() const;
4269
4270   /**
4271    * Set info.
4272    * SMT-LIB:
4273    * \verbatim
4274    * ( set-info <attribute> )
4275    * \endverbatim
4276    * @param keyword the info flag
4277    * @param value the value of the info flag
4278    */
4279   void setInfo(const std::string& keyword, const std::string& value) const;
4280
4281   /**
4282    * Set logic.
4283    * SMT-LIB:
4284    * \verbatim
4285    * ( set-logic <symbol> )
4286    * \endverbatim
4287    * @param logic the logic to set
4288    */
4289   void setLogic(const std::string& logic) const;
4290
4291   /**
4292    * Set option.
4293    * SMT-LIB:
4294    * \verbatim
4295    *   ( set-option <option> )
4296    * \endverbatim
4297    * @param option the option name
4298    * @param value the option value
4299    */
4300   void setOption(const std::string& option, const std::string& value) const;
4301
4302   /**
4303    * If needed, convert this term to a given sort. Note that the sort of the
4304    * term must be convertible into the target sort. Currently only Int to Real
4305    * conversions are supported.
4306    * @param t the term
4307    * @param s the target sort
4308    * @return the term wrapped into a sort conversion if needed
4309    */
4310   Term ensureTermSort(const Term& t, const Sort& s) const;
4311
4312   /**
4313    * Append \p symbol to the current list of universal variables.
4314    * SyGuS v2:
4315    * \verbatim
4316    *   ( declare-var <symbol> <sort> )
4317    * \endverbatim
4318    * @param sort the sort of the universal variable
4319    * @param symbol the name of the universal variable
4320    * @return the universal variable
4321    */
4322   Term mkSygusVar(const Sort& sort,
4323                   const std::string& symbol = std::string()) const;
4324
4325   /**
4326    * Create a Sygus grammar. The first non-terminal is treated as the starting
4327    * non-terminal, so the order of non-terminals matters.
4328    *
4329    * @param boundVars the parameters to corresponding synth-fun/synth-inv
4330    * @param ntSymbols the pre-declaration of the non-terminal symbols
4331    * @return the grammar
4332    */
4333   Grammar mkSygusGrammar(const std::vector<Term>& boundVars,
4334                          const std::vector<Term>& ntSymbols) const;
4335
4336   /**
4337    * Synthesize n-ary function.
4338    * SyGuS v2:
4339    * \verbatim
4340    *   ( synth-fun <symbol> ( <boundVars>* ) <sort> )
4341    * \endverbatim
4342    * @param symbol the name of the function
4343    * @param boundVars the parameters to this function
4344    * @param sort the sort of the return value of this function
4345    * @return the function
4346    */
4347   Term synthFun(const std::string& symbol,
4348                 const std::vector<Term>& boundVars,
4349                 const Sort& sort) const;
4350
4351   /**
4352    * Synthesize n-ary function following specified syntactic constraints.
4353    * SyGuS v2:
4354    * \verbatim
4355    *   ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
4356    * \endverbatim
4357    * @param symbol the name of the function
4358    * @param boundVars the parameters to this function
4359    * @param sort the sort of the return value of this function
4360    * @param grammar the syntactic constraints
4361    * @return the function
4362    */
4363   Term synthFun(const std::string& symbol,
4364                 const std::vector<Term>& boundVars,
4365                 Sort sort,
4366                 Grammar& grammar) const;
4367
4368   /**
4369    * Synthesize invariant.
4370    * SyGuS v2:
4371    * \verbatim
4372    *   ( synth-inv <symbol> ( <boundVars>* ) )
4373    * \endverbatim
4374    * @param symbol the name of the invariant
4375    * @param boundVars the parameters to this invariant
4376    * @return the invariant
4377    */
4378   Term synthInv(const std::string& symbol,
4379                 const std::vector<Term>& boundVars) const;
4380
4381   /**
4382    * Synthesize invariant following specified syntactic constraints.
4383    * SyGuS v2:
4384    * \verbatim
4385    *   ( synth-inv <symbol> ( <boundVars>* ) <g> )
4386    * \endverbatim
4387    * @param symbol the name of the invariant
4388    * @param boundVars the parameters to this invariant
4389    * @param grammar the syntactic constraints
4390    * @return the invariant
4391    */
4392   Term synthInv(const std::string& symbol,
4393                 const std::vector<Term>& boundVars,
4394                 Grammar& grammar) const;
4395
4396   /**
4397    * Add a forumla to the set of Sygus constraints.
4398    * SyGuS v2:
4399    * \verbatim
4400    *   ( constraint <term> )
4401    * \endverbatim
4402    * @param term the formula to add as a constraint
4403    */
4404   void addSygusConstraint(const Term& term) const;
4405
4406   /**
4407    * Add a forumla to the set of Sygus assumptions.
4408    * SyGuS v2:
4409    * \verbatim
4410    *   ( assume <term> )
4411    * \endverbatim
4412    * @param term the formula to add as an assumption
4413    */
4414   void addSygusAssume(const Term& term) const;
4415
4416   /**
4417    * Add a set of Sygus constraints to the current state that correspond to an
4418    * invariant synthesis problem.
4419    * SyGuS v2:
4420    * \verbatim
4421    *   ( inv-constraint <inv> <pre> <trans> <post> )
4422    * \endverbatim
4423    * @param inv the function-to-synthesize
4424    * @param pre the pre-condition
4425    * @param trans the transition relation
4426    * @param post the post-condition
4427    */
4428   void addSygusInvConstraint(Term inv, Term pre, Term trans, Term post) const;
4429
4430   /**
4431    * Try to find a solution for the synthesis conjecture corresponding to the
4432    * current list of functions-to-synthesize, universal variables and
4433    * constraints.
4434    * SyGuS v2:
4435    * \verbatim
4436    *   ( check-synth )
4437    * \endverbatim
4438    * @return the result of the synthesis conjecture.
4439    */
4440   Result checkSynth() const;
4441
4442   /**
4443    * Get the synthesis solution of the given term. This method should be called
4444    * immediately after the solver answers unsat for sygus input.
4445    * @param term the term for which the synthesis solution is queried
4446    * @return the synthesis solution of the given term
4447    */
4448   Term getSynthSolution(Term term) const;
4449
4450   /**
4451    * Get the synthesis solutions of the given terms. This method should be
4452    * called immediately after the solver answers unsat for sygus input.
4453    * @param terms the terms for which the synthesis solutions is queried
4454    * @return the synthesis solutions of the given terms
4455    */
4456   std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
4457
4458   /**
4459    * Returns a snapshot of the current state of the statistic values of this
4460    * solver. The returned object is completely decoupled from the solver and
4461    * will not change when the solver is used again.
4462    */
4463   Statistics getStatistics() const;
4464
4465   /**
4466    * Whether the output stream for the given tag is enabled. Tags can be enabled
4467    * with the `output` option (and `-o <tag>` on the command line). Raises an
4468    * exception when an invalid tag is given.
4469    */
4470   bool isOutputOn(const std::string& tag) const;
4471
4472   /**
4473    * Returns an output stream for the given tag. Tags can be enabled with the
4474    * `output` option (and `-o <tag>` on the command line). Raises an exception
4475    * when an invalid tag is given.
4476    */
4477   std::ostream& getOutput(const std::string& tag) const;
4478
4479  private:
4480   /** @return the node manager of this solver */
4481   NodeManager* getNodeManager(void) const;
4482   /** Reset the API statistics */
4483   void resetStatistics();
4484
4485   /**
4486    * Print the statistics to the given file descriptor, suitable for usage in
4487    * signal handlers.
4488    */
4489   void printStatisticsSafe(int fd) const;
4490
4491   /** Helper to check for API misuse in mkOp functions. */
4492   void checkMkTerm(Kind kind, uint32_t nchildren) const;
4493   /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
4494   template <typename T>
4495   Term mkValHelper(T t) const;
4496   /** Helper for mkReal functions that take a string as argument. */
4497   Term mkRealFromStrHelper(const std::string& s) const;
4498   /** Helper for mkBitVector functions that take a string as argument. */
4499   Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
4500   /**
4501    * Helper for mkBitVector functions that take a string and a size as
4502    * arguments.
4503    */
4504   Term mkBVFromStrHelper(uint32_t size,
4505                          const std::string& s,
4506                          uint32_t base) const;
4507   /** Helper for mkBitVector functions that take an integer as argument. */
4508   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
4509   /** Helper for functions that create tuple sorts. */
4510   Sort mkTupleSortHelper(const std::vector<Sort>& sorts) const;
4511   /** Helper for mkTerm functions that create Term from a Kind */
4512   Term mkTermFromKind(Kind kind) const;
4513   /** Helper for mkChar functions that take a string as argument. */
4514   Term mkCharFromStrHelper(const std::string& s) const;
4515   /** Get value helper, which accounts for subtyping */
4516   Term getValueHelper(const Term& term) const;
4517
4518   /**
4519    * Helper function that ensures that a given term is of sort real (as opposed
4520    * to being of sort integer).
4521    * @param t a term of sort integer or real
4522    * @return a term of sort real
4523    */
4524   Term ensureRealSort(const Term& t) const;
4525
4526   /**
4527    * Create n-ary term of given kind. This handles the cases of left/right
4528    * associative operators, chainable operators, and cases when the number of
4529    * children exceeds the maximum arity for the kind.
4530    * @param kind the kind of the term
4531    * @param children the children of the term
4532    * @return the Term
4533    */
4534   Term mkTermHelper(Kind kind, const std::vector<Term>& children) const;
4535
4536   /**
4537    * Create n-ary term of given kind from a given operator.
4538    * @param op the operator
4539    * @param children the children of the term
4540    * @return the Term
4541    */
4542   Term mkTermHelper(const Op& op, const std::vector<Term>& children) const;
4543
4544   /**
4545    * Create a vector of datatype sorts, using unresolved sorts.
4546    * @param dtypedecls the datatype declarations from which the sort is created
4547    * @param unresolvedSorts the list of unresolved sorts
4548    * @return the datatype sorts
4549    */
4550   std::vector<Sort> mkDatatypeSortsInternal(
4551       const std::vector<DatatypeDecl>& dtypedecls,
4552       const std::set<Sort>& unresolvedSorts) const;
4553
4554   /**
4555    * Synthesize n-ary function following specified syntactic constraints.
4556    * SMT-LIB:
4557    * \verbatim
4558    *   ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
4559    * \endverbatim
4560    * @param symbol the name of the function
4561    * @param boundVars the parameters to this function
4562    * @param sort the sort of the return value of this function
4563    * @param isInv determines whether this is synth-fun or synth-inv
4564    * @param grammar the syntactic constraints
4565    * @return the function
4566    */
4567   Term synthFunHelper(const std::string& symbol,
4568                       const std::vector<Term>& boundVars,
4569                       const Sort& sort,
4570                       bool isInv = false,
4571                       Grammar* grammar = nullptr) const;
4572
4573   /** Check whether string s is a valid decimal integer. */
4574   bool isValidInteger(const std::string& s) const;
4575
4576   /** Increment the term stats counter. */
4577   void increment_term_stats(Kind kind) const;
4578   /** Increment the vars stats (if 'is_var') or consts stats counter. */
4579   void increment_vars_consts_stats(const Sort& sort, bool is_var) const;
4580
4581   /** Keep a copy of the original option settings (for resets). */
4582   std::unique_ptr<Options> d_originalOptions;
4583   /** The node manager of this solver. */
4584   NodeManager* d_nodeMgr;
4585   /** The statistics collected on the Api level. */
4586   std::unique_ptr<APIStatistics> d_stats;
4587   /** The SMT engine of this solver. */
4588   std::unique_ptr<SolverEngine> d_slv;
4589   /** The random number generator of this solver. */
4590   std::unique_ptr<Random> d_rng;
4591 };
4592
4593 }  // namespace cvc5::api
4594
4595 #endif