1 /********************* */ 2 /*! \file cvc4cpp.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Aina Niemetz, Andres Noetzli 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief The CVC4 C++ API. 13 ** 14 ** The CVC4 C++ API. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef __CVC4__API__CVC4CPP_H 20 #define __CVC4__API__CVC4CPP_H 21 22 #include "api/cvc4cppkind.h" 23 24 #include <map> 25 #include <memory> 26 #include <set> 27 #include <sstream> 28 #include <string> 29 #include <unordered_map> 30 #include <unordered_set> 31 #include <vector> 32 33 namespace CVC4 { 34 35 class Expr; 36 class Datatype; 37 class DatatypeConstructor; 38 class DatatypeConstructorArg; 39 class ExprManager; 40 class SmtEngine; 41 class Type; 42 class Options; 43 class Random; 44 class Result; 45 46 namespace api { 47 48 /* -------------------------------------------------------------------------- */ 49 /* Exception */ 50 /* -------------------------------------------------------------------------- */ 51 52 class CVC4_PUBLIC CVC4ApiException : public std::exception 53 { 54 public: CVC4ApiException(const std::string & str)55 CVC4ApiException(const std::string& str) : d_msg(str) {} CVC4ApiException(const std::stringstream & stream)56 CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {} getMessage()57 std::string getMessage() const { return d_msg; } what()58 const char* what() const noexcept override { return d_msg.c_str(); } 59 60 private: 61 std::string d_msg; 62 }; 63 64 /* -------------------------------------------------------------------------- */ 65 /* Result */ 66 /* -------------------------------------------------------------------------- */ 67 68 /** 69 * Encapsulation of a three-valued solver result, with explanations. 70 */ 71 class CVC4_PUBLIC Result 72 { 73 friend class Solver; 74 75 public: 76 // !!! This constructor is only temporarily public until the parser is fully 77 // migrated to the new API. !!! 78 /** 79 * Constructor. 80 * @param r the internal result that is to be wrapped by this result 81 * @return the Result 82 */ 83 Result(const CVC4::Result& r); 84 85 /** 86 * Return true if query was a satisfiable checkSat() or checkSatAssuming() 87 * query. 88 */ 89 bool isSat() const; 90 91 /** 92 * Return true if query was an unsatisfiable checkSat() or 93 * checkSatAssuming() query. 94 */ 95 bool isUnsat() const; 96 97 /** 98 * Return true if query was a checkSat() or checkSatAssuming() query and 99 * CVC4 was not able to determine (un)satisfiability. 100 */ 101 bool isSatUnknown() const; 102 103 /** 104 * Return true if corresponding query was a valid checkValid() or 105 * checkValidAssuming() query. 106 */ 107 bool isValid() const; 108 109 /** 110 * Return true if corresponding query was an invalid checkValid() or 111 * checkValidAssuming() query. 112 */ 113 bool isInvalid() const; 114 115 /** 116 * Return true if query was a checkValid() or checkValidAssuming() query 117 * and CVC4 was not able to determine (in)validity. 118 */ 119 bool isValidUnknown() const; 120 121 /** 122 * Operator overloading for equality of two results. 123 * @param r the result to compare to for equality 124 * @return true if the results are equal 125 */ 126 bool operator==(const Result& r) const; 127 128 /** 129 * Operator overloading for disequality of two results. 130 * @param r the result to compare to for disequality 131 * @return true if the results are disequal 132 */ 133 bool operator!=(const Result& r) const; 134 135 /** 136 * @return an explanation for an unknown query result. 137 */ 138 std::string getUnknownExplanation() const; 139 140 /** 141 * @return a string representation of this result. 142 */ 143 std::string toString() const; 144 145 // !!! This is only temporarily available until the parser is fully migrated 146 // to the new API. !!! 147 CVC4::Result getResult(void) const; 148 149 private: 150 /** 151 * The interal result wrapped by this result. 152 * This is a shared_ptr rather than a unique_ptr since CVC4::Result is 153 * not ref counted. 154 */ 155 std::shared_ptr<CVC4::Result> d_result; 156 }; 157 158 /** 159 * Serialize a result to given stream. 160 * @param out the output stream 161 * @param r the result to be serialized to the given output stream 162 * @return the output stream 163 */ 164 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; 165 166 /* -------------------------------------------------------------------------- */ 167 /* Sort */ 168 /* -------------------------------------------------------------------------- */ 169 170 class Datatype; 171 172 /** 173 * The sort of a CVC4 term. 174 */ 175 class CVC4_PUBLIC Sort 176 { 177 friend class DatatypeConstructorDecl; 178 friend class DatatypeDecl; 179 friend class DatatypeSelectorDecl; 180 friend class OpTerm; 181 friend class Solver; 182 friend struct SortHashFunction; 183 friend class Term; 184 185 public: 186 // !!! This constructor is only temporarily public until the parser is fully 187 // migrated to the new API. !!! 188 /** 189 * Constructor. 190 * @param t the internal type that is to be wrapped by this sort 191 * @return the Sort 192 */ 193 Sort(const CVC4::Type& t); 194 195 /** 196 * Constructor. 197 */ 198 Sort(); 199 200 /** 201 * Destructor. 202 */ 203 ~Sort(); 204 205 /** 206 * Comparison for structural equality. 207 * @param s the sort to compare to 208 * @return true if the sorts are equal 209 */ 210 bool operator==(const Sort& s) const; 211 212 /** 213 * Comparison for structural disequality. 214 * @param s the sort to compare to 215 * @return true if the sorts are not equal 216 */ 217 bool operator!=(const Sort& s) const; 218 219 /** 220 * @return true if this Sort is a null sort. 221 */ 222 bool isNull() const; 223 224 /** 225 * Is this a Boolean sort? 226 * @return true if the sort is a Boolean sort 227 */ 228 bool isBoolean() const; 229 230 /** 231 * Is this a integer sort? 232 * @return true if the sort is a integer sort 233 */ 234 bool isInteger() const; 235 236 /** 237 * Is this a real sort? 238 * @return true if the sort is a real sort 239 */ 240 bool isReal() const; 241 242 /** 243 * Is this a string sort? 244 * @return true if the sort is the string sort 245 */ 246 bool isString() const; 247 248 /** 249 * Is this a regexp sort? 250 * @return true if the sort is the regexp sort 251 */ 252 bool isRegExp() const; 253 254 /** 255 * Is this a rounding mode sort? 256 * @return true if the sort is the rounding mode sort 257 */ 258 bool isRoundingMode() const; 259 260 /** 261 * Is this a bit-vector sort? 262 * @return true if the sort is a bit-vector sort 263 */ 264 bool isBitVector() const; 265 266 /** 267 * Is this a floating-point sort? 268 * @return true if the sort is a floating-point sort 269 */ 270 bool isFloatingPoint() const; 271 272 /** 273 * Is this a datatype sort? 274 * @return true if the sort is a datatype sort 275 */ 276 bool isDatatype() const; 277 278 /** 279 * Is this a parametric datatype sort? 280 * @return true if the sort is a parametric datatype sort 281 */ 282 bool isParametricDatatype() const; 283 284 /** 285 * Is this a function sort? 286 * @return true if the sort is a function sort 287 */ 288 bool isFunction() const; 289 290 /** 291 * Is this a predicate sort? 292 * That is, is this a function sort mapping to Boolean? All predicate 293 * sorts are also function sorts. 294 * @return true if the sort is a predicate sort 295 */ 296 bool isPredicate() const; 297 298 /** 299 * Is this a tuple sort? 300 * @return true if the sort is a tuple sort 301 */ 302 bool isTuple() const; 303 304 /** 305 * Is this a record sort? 306 * @return true if the sort is a record sort 307 */ 308 bool isRecord() const; 309 310 /** 311 * Is this an array sort? 312 * @return true if the sort is a array sort 313 */ 314 bool isArray() const; 315 316 /** 317 * Is this a Set sort? 318 * @return true if the sort is a Set sort 319 */ 320 bool isSet() const; 321 322 /** 323 * Is this a sort kind? 324 * @return true if this is a sort kind 325 */ 326 bool isUninterpretedSort() const; 327 328 /** 329 * Is this a sort constructor kind? 330 * @return true if this is a sort constructor kind 331 */ 332 bool isSortConstructor() const; 333 334 /** 335 * Is this a first-class sort? 336 * First-class sorts are sorts for which: 337 * (1) we handle equalities between terms of that type, and 338 * (2) they are allowed to be parameters of parametric sorts (e.g. index or 339 * element sorts of arrays). 340 * 341 * Examples of sorts that are not first-class include sort constructor sorts 342 * and regular expression sorts. 343 * 344 * @return true if this is a first-class sort 345 */ 346 bool isFirstClass() const; 347 348 /** 349 * Is this a function-LIKE sort? 350 * 351 * Anything function-like except arrays (e.g., datatype selectors) is 352 * considered a function here. Function-like terms can not be the argument 353 * or return value for any term that is function-like. 354 * This is mainly to avoid higher order. 355 * 356 * Note that arrays are explicitly not considered function-like here. 357 * 358 * @return true if this is a function-like sort 359 */ 360 bool isFunctionLike() const; 361 362 /** 363 * @return the underlying datatype of a datatype sort 364 */ 365 Datatype getDatatype() const; 366 367 /** 368 * Instantiate a parameterized datatype/sort sort. 369 * Create sorts parameter with Solver::mkParamSort(). 370 * @param params the list of sort parameters to instantiate with 371 */ 372 Sort instantiate(const std::vector<Sort>& params) const; 373 374 /** 375 * Output a string representation of this sort to a given stream. 376 * @param out the output stream 377 */ 378 void toStream(std::ostream& out) const; 379 380 /** 381 * @return a string representation of this sort 382 */ 383 std::string toString() const; 384 385 // !!! This is only temporarily available until the parser is fully migrated 386 // to the new API. !!! 387 CVC4::Type getType(void) const; 388 389 /* Function sort ------------------------------------------------------- */ 390 391 /** 392 * @return the arity of a function sort 393 */ 394 size_t getFunctionArity() const; 395 396 /** 397 * @return the domain sorts of a function sort 398 */ 399 std::vector<Sort> getFunctionDomainSorts() const; 400 401 /** 402 * @return the codomain sort of a function sort 403 */ 404 Sort getFunctionCodomainSort() const; 405 406 /* Array sort ---------------------------------------------------------- */ 407 408 /** 409 * @return the array index sort of an array sort 410 */ 411 Sort getArrayIndexSort() const; 412 413 /** 414 * @return the array element sort of an array element sort 415 */ 416 Sort getArrayElementSort() const; 417 418 /* Set sort ------------------------------------------------------------ */ 419 420 /** 421 * @return the element sort of a set sort 422 */ 423 Sort getSetElementSort() const; 424 425 /* Uninterpreted sort -------------------------------------------------- */ 426 427 /** 428 * @return the name of an uninterpreted sort 429 */ 430 std::string getUninterpretedSortName() const; 431 432 /** 433 * @return true if an uninterpreted sort is parameterezied 434 */ 435 bool isUninterpretedSortParameterized() const; 436 437 /** 438 * @return the parameter sorts of an uninterpreted sort 439 */ 440 std::vector<Sort> getUninterpretedSortParamSorts() const; 441 442 /* Sort constructor sort ----------------------------------------------- */ 443 444 /** 445 * @return the name of a sort constructor sort 446 */ 447 std::string getSortConstructorName() const; 448 449 /** 450 * @return the arity of a sort constructor sort 451 */ 452 size_t getSortConstructorArity() const; 453 454 /* Bit-vector sort ----------------------------------------------------- */ 455 456 /** 457 * @return the bit-width of the bit-vector sort 458 */ 459 uint32_t getBVSize() const; 460 461 /* Floating-point sort ------------------------------------------------- */ 462 463 /** 464 * @return the bit-width of the exponent of the floating-point sort 465 */ 466 uint32_t getFPExponentSize() const; 467 468 /** 469 * @return the width of the significand of the floating-point sort 470 */ 471 uint32_t getFPSignificandSize() const; 472 473 /* Datatype sort ------------------------------------------------------- */ 474 475 /** 476 * @return the parameter sorts of a datatype sort 477 */ 478 std::vector<Sort> getDatatypeParamSorts() const; 479 480 /** 481 * @return the arity of a datatype sort 482 */ 483 size_t getDatatypeArity() const; 484 485 /* Tuple sort ---------------------------------------------------------- */ 486 487 /** 488 * @return the length of a tuple sort 489 */ 490 size_t getTupleLength() const; 491 492 /** 493 * @return the element sorts of a tuple sort 494 */ 495 std::vector<Sort> getTupleSorts() const; 496 497 private: 498 /* Helper to convert a vector of sorts into a vector of internal types. */ 499 std::vector<Sort> typeVectorToSorts( 500 const std::vector<CVC4::Type>& vector) const; 501 /** 502 * The interal type wrapped by this sort. 503 * This is a shared_ptr rather than a unique_ptr to avoid overhead due to 504 * memory allocation (CVC4::Type is already ref counted, so this could be 505 * a unique_ptr instead). 506 */ 507 std::shared_ptr<CVC4::Type> d_type; 508 }; 509 510 /** 511 * Serialize a sort to given stream. 512 * @param out the output stream 513 * @param s the sort to be serialized to the given output stream 514 * @return the output stream 515 */ 516 std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_PUBLIC; 517 518 /** 519 * Hash function for Sorts. 520 */ 521 struct CVC4_PUBLIC SortHashFunction 522 { 523 size_t operator()(const Sort& s) const; 524 }; 525 526 /* -------------------------------------------------------------------------- */ 527 /* Term */ 528 /* -------------------------------------------------------------------------- */ 529 530 /** 531 * A CVC4 Term. 532 */ 533 class CVC4_PUBLIC Term 534 { 535 friend class Datatype; 536 friend class DatatypeConstructor; 537 friend class Solver; 538 friend struct TermHashFunction; 539 540 public: 541 // !!! This constructor is only temporarily public until the parser is fully 542 // migrated to the new API. !!! 543 /** 544 * Constructor. 545 * @param e the internal expression that is to be wrapped by this term 546 * @return the Term 547 */ 548 Term(const CVC4::Expr& e); 549 550 /** 551 * Constructor. 552 */ 553 Term(); 554 555 /** 556 * Destructor. 557 */ 558 ~Term(); 559 560 /** 561 * Syntactic equality operator. 562 * Return true if both terms are syntactically identical. 563 * Both terms must belong to the same solver object. 564 * @param t the term to compare to for equality 565 * @return true if the terms are equal 566 */ 567 bool operator==(const Term& t) const; 568 569 /** 570 * Syntactic disequality operator. 571 * Return true if both terms differ syntactically. 572 * Both terms must belong to the same solver object. 573 * @param t the term to compare to for disequality 574 * @return true if terms are disequal 575 */ 576 bool operator!=(const Term& t) const; 577 578 /** 579 * @return the kind of this term 580 */ 581 Kind getKind() const; 582 583 /** 584 * @return the sort of this term 585 */ 586 Sort getSort() const; 587 588 /** 589 * @return true if this Term is a null term 590 */ 591 bool isNull() const; 592 593 /** 594 * Boolean negation. 595 * @return the Boolean negation of this term 596 */ 597 Term notTerm() const; 598 599 /** 600 * Boolean and. 601 * @param t a Boolean term 602 * @return the conjunction of this term and the given term 603 */ 604 Term andTerm(const Term& t) const; 605 606 /** 607 * Boolean or. 608 * @param t a Boolean term 609 * @return the disjunction of this term and the given term 610 */ 611 Term orTerm(const Term& t) const; 612 613 /** 614 * Boolean exclusive or. 615 * @param t a Boolean term 616 * @return the exclusive disjunction of this term and the given term 617 */ 618 Term xorTerm(const Term& t) const; 619 620 /** 621 * Equality. 622 * @param t a Boolean term 623 * @return the Boolean equivalence of this term and the given term 624 */ 625 Term eqTerm(const Term& t) const; 626 627 /** 628 * Boolean implication. 629 * @param t a Boolean term 630 * @return the implication of this term and the given term 631 */ 632 Term impTerm(const Term& t) const; 633 634 /** 635 * If-then-else with this term as the Boolean condition. 636 * @param then_t the 'then' term 637 * @param else_t the 'else' term 638 * @return the if-then-else term with this term as the Boolean condition 639 */ 640 Term iteTerm(const Term& then_t, const Term& else_t) const; 641 642 /** 643 * @return a string representation of this term 644 */ 645 std::string toString() const; 646 647 /** 648 * Iterator for the children of a Term. 649 */ 650 class const_iterator : public std::iterator<std::input_iterator_tag, Term> 651 { 652 friend class Term; 653 654 public: 655 /** 656 * Constructor. 657 */ 658 const_iterator(); 659 660 /** 661 * Copy constructor. 662 */ 663 const_iterator(const const_iterator& it); 664 665 /** 666 * Destructor. 667 */ 668 ~const_iterator(); 669 670 /** 671 * Assignment operator. 672 * @param it the iterator to assign to 673 * @return the reference to the iterator after assignment 674 */ 675 const_iterator& operator=(const const_iterator& it); 676 677 /** 678 * Equality operator. 679 * @param it the iterator to compare to for equality 680 * @return true if the iterators are equal 681 */ 682 bool operator==(const const_iterator& it) const; 683 684 /** 685 * Disequality operator. 686 * @param it the iterator to compare to for disequality 687 * @return true if the iterators are disequal 688 */ 689 bool operator!=(const const_iterator& it) const; 690 691 /** 692 * Increment operator (prefix). 693 * @return a reference to the iterator after incrementing by one 694 */ 695 const_iterator& operator++(); 696 697 /** 698 * Increment operator (postfix). 699 * @return a reference to the iterator after incrementing by one 700 */ 701 const_iterator operator++(int); 702 703 /** 704 * Dereference operator. 705 * @return the term this iterator points to 706 */ 707 Term operator*() const; 708 709 private: 710 /* The internal expression iterator wrapped by this iterator. */ 711 void* d_iterator; 712 /* Constructor. */ 713 explicit const_iterator(void*); 714 }; 715 716 /** 717 * @return an iterator to the first child of this Term 718 */ 719 const_iterator begin() const; 720 721 /** 722 * @return an iterator to one-off-the-last child of this Term 723 */ 724 const_iterator end() const; 725 726 // !!! This is only temporarily available until the parser is fully migrated 727 // to the new API. !!! 728 CVC4::Expr getExpr(void) const; 729 730 private: 731 /** 732 * The internal expression wrapped by this term. 733 * This is a shared_ptr rather than a unique_ptr to avoid overhead due to 734 * memory allocation (CVC4::Expr is already ref counted, so this could be 735 * a unique_ptr instead). 736 */ 737 std::shared_ptr<CVC4::Expr> d_expr; 738 }; 739 740 /** 741 * Hash function for Terms. 742 */ 743 struct CVC4_PUBLIC TermHashFunction 744 { 745 size_t operator()(const Term& t) const; 746 }; 747 748 /** 749 * Serialize a term to given stream. 750 * @param out the output stream 751 * @param t the term to be serialized to the given output stream 752 * @return the output stream 753 */ 754 std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_PUBLIC; 755 756 /** 757 * Serialize a vector of terms to given stream. 758 * @param out the output stream 759 * @param vector the vector of terms to be serialized to the given stream 760 * @return the output stream 761 */ 762 std::ostream& operator<<(std::ostream& out, 763 const std::vector<Term>& vector) CVC4_PUBLIC; 764 765 /** 766 * Serialize a set of terms to the given stream. 767 * @param out the output stream 768 * @param set the set of terms to be serialized to the given stream 769 * @return the output stream 770 */ 771 std::ostream& operator<<(std::ostream& out, 772 const std::set<Term>& set) CVC4_PUBLIC; 773 774 /** 775 * Serialize an unordered_set of terms to the given stream. 776 * 777 * @param out the output stream 778 * @param unordered_set the set of terms to be serialized to the given stream 779 * @return the output stream 780 */ 781 std::ostream& operator<<(std::ostream& out, 782 const std::unordered_set<Term, TermHashFunction>& 783 unordered_set) CVC4_PUBLIC; 784 785 /** 786 * Serialize a map of terms to the given stream. 787 * 788 * @param out the output stream 789 * @param map the map of terms to be serialized to the given stream 790 * @return the output stream 791 */ 792 template <typename V> 793 std::ostream& operator<<(std::ostream& out, 794 const std::map<Term, V>& map) CVC4_PUBLIC; 795 796 /** 797 * Serialize an unordered_map of terms to the given stream. 798 * 799 * @param out the output stream 800 * @param unordered_map the map of terms to be serialized to the given stream 801 * @return the output stream 802 */ 803 template <typename V> 804 std::ostream& operator<<(std::ostream& out, 805 const std::unordered_map<Term, V, TermHashFunction>& 806 unordered_map) CVC4_PUBLIC; 807 808 /* -------------------------------------------------------------------------- */ 809 /* OpTerm */ 810 /* -------------------------------------------------------------------------- */ 811 812 /** 813 * A CVC4 operator term. 814 * An operator term is a term that represents certain operators, instantiated 815 * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. 816 */ 817 class CVC4_PUBLIC OpTerm 818 { 819 friend class Solver; 820 friend struct OpTermHashFunction; 821 822 public: 823 /** 824 * Constructor. 825 */ 826 OpTerm(); 827 828 // !!! This constructor is only temporarily public until the parser is fully 829 // migrated to the new API. !!! 830 /** 831 * Constructor. 832 * @param e the internal expression that is to be wrapped by this term 833 * @return the Term 834 */ 835 OpTerm(const CVC4::Expr& e); 836 837 /** 838 * Destructor. 839 */ 840 ~OpTerm(); 841 842 /** 843 * Syntactic equality operator. 844 * Return true if both operator terms are syntactically identical. 845 * Both operator terms must belong to the same solver object. 846 * @param t the operator term to compare to for equality 847 * @return true if the operator terms are equal 848 */ 849 bool operator==(const OpTerm& t) const; 850 851 /** 852 * Syntactic disequality operator. 853 * Return true if both operator terms differ syntactically. 854 * Both terms must belong to the same solver object. 855 * @param t the operator term to compare to for disequality 856 * @return true if operator terms are disequal 857 */ 858 bool operator!=(const OpTerm& t) const; 859 860 /** 861 * @return the kind of this operator term 862 */ 863 Kind getKind() const; 864 865 /** 866 * @return the sort of this operator term 867 */ 868 Sort getSort() const; 869 870 /** 871 * @return true if this operator term is a null term 872 */ 873 bool isNull() const; 874 875 /** 876 * @return a string representation of this operator term 877 */ 878 std::string toString() const; 879 880 // !!! This is only temporarily available until the parser is fully migrated 881 // to the new API. !!! 882 CVC4::Expr getExpr(void) const; 883 884 private: 885 /** 886 * The internal expression wrapped by this operator term. 887 * This is a shared_ptr rather than a unique_ptr to avoid overhead due to 888 * memory allocation (CVC4::Expr is already ref counted, so this could be 889 * a unique_ptr instead). 890 */ 891 std::shared_ptr<CVC4::Expr> d_expr; 892 }; 893 894 /** 895 * Serialize an operator term to given stream. 896 * @param out the output stream 897 * @param t the operator term to be serialized to the given output stream 898 * @return the output stream 899 */ 900 std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC; 901 902 /** 903 * Hash function for OpTerms. 904 */ 905 struct CVC4_PUBLIC OpTermHashFunction 906 { 907 size_t operator()(const OpTerm& t) const; 908 }; 909 910 /* -------------------------------------------------------------------------- */ 911 /* Datatypes */ 912 /* -------------------------------------------------------------------------- */ 913 914 class DatatypeConstructorIterator; 915 class DatatypeIterator; 916 917 /** 918 * A place-holder sort to allow a DatatypeDecl to refer to itself. 919 * Self-sorted fields of DatatypeDecls will be properly sorted when a Sort is 920 * created for the DatatypeDecl. 921 */ 922 class CVC4_PUBLIC DatatypeDeclSelfSort 923 { 924 }; 925 926 /** 927 * A CVC4 datatype selector declaration. 928 */ 929 class CVC4_PUBLIC DatatypeSelectorDecl 930 { 931 friend class DatatypeConstructorDecl; 932 933 public: 934 /** 935 * Constructor. 936 * @param name the name of the datatype selector 937 * @param sort the sort of the datatype selector 938 * @return the DatatypeSelectorDecl 939 */ 940 DatatypeSelectorDecl(const std::string& name, Sort sort); 941 942 /** 943 * Constructor. 944 * @param name the name of the datatype selector 945 * @param sort the sort of the datatype selector 946 * @return the DAtatypeSelectorDecl 947 */ 948 DatatypeSelectorDecl(const std::string& name, DatatypeDeclSelfSort sort); 949 950 /** 951 * @return a string representation of this datatype selector 952 */ 953 std::string toString() const; 954 955 private: 956 /* The name of the datatype selector. */ 957 std::string d_name; 958 /* The sort of the datatype selector. */ 959 Sort d_sort; 960 }; 961 962 /** 963 * A CVC4 datatype constructor declaration. 964 */ 965 class CVC4_PUBLIC DatatypeConstructorDecl 966 { 967 friend class DatatypeDecl; 968 969 public: 970 /** 971 * Constructor. 972 * @param name the name of the datatype constructor 973 * @return the DatatypeConstructorDecl 974 */ 975 DatatypeConstructorDecl(const std::string& name); 976 977 /** 978 * Add datatype selector declaration. 979 * @param stor the datatype selector declaration to add 980 */ 981 void addSelector(const DatatypeSelectorDecl& stor); 982 983 /** 984 * @return a string representation of this datatype constructor declaration 985 */ 986 std::string toString() const; 987 988 // !!! This is only temporarily available until the parser is fully migrated 989 // to the new API. !!! 990 CVC4::DatatypeConstructor getDatatypeConstructor(void) const; 991 992 private: 993 /** 994 * The internal (intermediate) datatype constructor wrapped by this 995 * datatype constructor declaration. 996 * This is a shared_ptr rather than a unique_ptr since 997 * CVC4::DatatypeConstructor is not ref counted. 998 */ 999 std::shared_ptr<CVC4::DatatypeConstructor> d_ctor; 1000 }; 1001 1002 /** 1003 * A CVC4 datatype declaration. 1004 */ 1005 class CVC4_PUBLIC DatatypeDecl 1006 { 1007 friend class DatatypeConstructorArg; 1008 friend class Solver; 1009 1010 public: 1011 /** 1012 * Constructor. 1013 * @param name the name of the datatype 1014 * @param isCoDatatype true if a codatatype is to be constructed 1015 * @return the DatatypeDecl 1016 */ 1017 DatatypeDecl(const std::string& name, bool isCoDatatype = false); 1018 1019 /** 1020 * Constructor for parameterized datatype declaration. 1021 * Create sorts parameter with Solver::mkParamSort(). 1022 * @param name the name of the datatype 1023 * @param param the sort parameter 1024 * @param isCoDatatype true if a codatatype is to be constructed 1025 */ 1026 DatatypeDecl(const std::string& name, Sort param, bool isCoDatatype = false); 1027 1028 /** 1029 * Constructor for parameterized datatype declaration. 1030 * Create sorts parameter with Solver::mkParamSort(). 1031 * @param name the name of the datatype 1032 * @param params a list of sort parameters 1033 * @param isCoDatatype true if a codatatype is to be constructed 1034 */ 1035 DatatypeDecl(const std::string& name, 1036 const std::vector<Sort>& params, 1037 bool isCoDatatype = false); 1038 1039 /** 1040 * Destructor. 1041 */ 1042 ~DatatypeDecl(); 1043 1044 /** 1045 * Add datatype constructor declaration. 1046 * @param ctor the datatype constructor declaration to add 1047 */ 1048 void addConstructor(const DatatypeConstructorDecl& ctor); 1049 1050 /** Get the number of constructors (so far) for this Datatype declaration. */ 1051 size_t getNumConstructors() const; 1052 1053 /** Is this Datatype declaration parametric? */ 1054 bool isParametric() const; 1055 1056 /** 1057 * @return a string representation of this datatype declaration 1058 */ 1059 std::string toString() const; 1060 1061 // !!! This is only temporarily available until the parser is fully migrated 1062 // to the new API. !!! 1063 CVC4::Datatype getDatatype(void) const; 1064 1065 private: 1066 /* The internal (intermediate) datatype wrapped by this datatype 1067 * declaration 1068 * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is 1069 * not ref counted. 1070 */ 1071 std::shared_ptr<CVC4::Datatype> d_dtype; 1072 }; 1073 1074 /** 1075 * A CVC4 datatype selector. 1076 */ 1077 class CVC4_PUBLIC DatatypeSelector 1078 { 1079 friend class DatatypeConstructor; 1080 friend class Solver; 1081 1082 public: 1083 /** 1084 * Constructor. 1085 */ 1086 DatatypeSelector(); 1087 1088 // !!! This constructor is only temporarily public until the parser is fully 1089 // migrated to the new API. !!! 1090 /** 1091 * Constructor. 1092 * @param stor the internal datatype selector to be wrapped 1093 * @return the DatatypeSelector 1094 */ 1095 DatatypeSelector(const CVC4::DatatypeConstructorArg& stor); 1096 1097 /** 1098 * Destructor. 1099 */ 1100 ~DatatypeSelector(); 1101 1102 /** 1103 * @return true if this datatype selector has been resolved. 1104 */ 1105 bool isResolved() const; 1106 1107 /** 1108 * Get the selector operator of this datatype selector. 1109 * @return the selector operator 1110 */ 1111 OpTerm getSelectorTerm() const; 1112 1113 /** 1114 * @return a string representation of this datatype selector 1115 */ 1116 std::string toString() const; 1117 1118 // !!! This is only temporarily available until the parser is fully migrated 1119 // to the new API. !!! 1120 CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const; 1121 1122 private: 1123 /** 1124 * The internal datatype selector wrapped by this datatype selector. 1125 * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is 1126 * not ref counted. 1127 */ 1128 std::shared_ptr<CVC4::DatatypeConstructorArg> d_stor; 1129 }; 1130 1131 /** 1132 * A CVC4 datatype constructor. 1133 */ 1134 class CVC4_PUBLIC DatatypeConstructor 1135 { 1136 friend class Datatype; 1137 friend class Solver; 1138 1139 public: 1140 /** 1141 * Constructor. 1142 */ 1143 DatatypeConstructor(); 1144 1145 // !!! This constructor is only temporarily public until the parser is fully 1146 // migrated to the new API. !!! 1147 /** 1148 * Constructor. 1149 * @param ctor the internal datatype constructor to be wrapped 1150 * @return the DatatypeConstructor 1151 */ 1152 DatatypeConstructor(const CVC4::DatatypeConstructor& ctor); 1153 1154 /** 1155 * Destructor. 1156 */ 1157 ~DatatypeConstructor(); 1158 1159 /** 1160 * @return true if this datatype constructor has been resolved. 1161 */ 1162 bool isResolved() const; 1163 1164 /** 1165 * Get the constructor operator of this datatype constructor. 1166 * @return the constructor operator 1167 */ 1168 OpTerm getConstructorTerm() const; 1169 1170 /** 1171 * Get the datatype selector with the given name. 1172 * This is a linear search through the selectors, so in case of 1173 * multiple, similarly-named selectors, the first is returned. 1174 * @param name the name of the datatype selector 1175 * @return the first datatype selector with the given name 1176 */ 1177 DatatypeSelector operator[](const std::string& name) const; 1178 DatatypeSelector getSelector(const std::string& name) const; 1179 1180 /** 1181 * Get the term representation of the datatype selector with the given name. 1182 * This is a linear search through the arguments, so in case of multiple, 1183 * similarly-named arguments, the selector for the first is returned. 1184 * @param name the name of the datatype selector 1185 * @return a term representing the datatype selector with the given name 1186 */ 1187 OpTerm getSelectorTerm(const std::string& name) const; 1188 1189 /** 1190 * @return a string representation of this datatype constructor 1191 */ 1192 std::string toString() const; 1193 1194 /** 1195 * Iterator for the selectors of a datatype constructor. 1196 */ 1197 class const_iterator 1198 : public std::iterator<std::input_iterator_tag, DatatypeConstructor> 1199 { 1200 friend class DatatypeConstructor; // to access constructor 1201 1202 public: 1203 /** 1204 * Assignment operator. 1205 * @param it the iterator to assign to 1206 * @return the reference to the iterator after assignment 1207 */ 1208 const_iterator& operator=(const const_iterator& it); 1209 1210 /** 1211 * Equality operator. 1212 * @param it the iterator to compare to for equality 1213 * @return true if the iterators are equal 1214 */ 1215 bool operator==(const const_iterator& it) const; 1216 1217 /** 1218 * Disequality operator. 1219 * @param it the iterator to compare to for disequality 1220 * @return true if the iterators are disequal 1221 */ 1222 bool operator!=(const const_iterator& it) const; 1223 1224 /** 1225 * Increment operator (prefix). 1226 * @return a reference to the iterator after incrementing by one 1227 */ 1228 const_iterator& operator++(); 1229 1230 /** 1231 * Increment operator (postfix). 1232 * @return a reference to the iterator after incrementing by one 1233 */ 1234 const_iterator operator++(int); 1235 1236 /** 1237 * Dereference operator. 1238 * @return a reference to the selector this iterator points to 1239 */ 1240 const DatatypeSelector& operator*() const; 1241 1242 /** 1243 * Dereference operator. 1244 * @return a pointer to the selector this iterator points to 1245 */ 1246 const DatatypeSelector* operator->() const; 1247 1248 private: 1249 /** 1250 * Constructor. 1251 * @param ctor the internal datatype constructor to iterate over 1252 * @param true if this is a begin() iterator 1253 */ 1254 const_iterator(const CVC4::DatatypeConstructor& ctor, bool begin); 1255 /* A pointer to the list of selectors of the internal datatype 1256 * constructor to iterate over. 1257 * This pointer is maintained for operators == and != only. */ 1258 const void* d_int_stors; 1259 /* The list of datatype selector (wrappers) to iterate over. */ 1260 std::vector<DatatypeSelector> d_stors; 1261 /* The current index of the iterator. */ 1262 size_t d_idx; 1263 }; 1264 1265 /** 1266 * @return an iterator to the first selector of this constructor 1267 */ 1268 const_iterator begin() const; 1269 1270 /** 1271 * @return an iterator to one-off-the-last selector of this constructor 1272 */ 1273 const_iterator end() const; 1274 1275 // !!! This is only temporarily available until the parser is fully migrated 1276 // to the new API. !!! 1277 CVC4::DatatypeConstructor getDatatypeConstructor(void) const; 1278 1279 private: 1280 /** 1281 * The internal datatype constructor wrapped by this datatype constructor. 1282 * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is 1283 * not ref counted. 1284 */ 1285 std::shared_ptr<CVC4::DatatypeConstructor> d_ctor; 1286 }; 1287 1288 /* 1289 * A CVC4 datatype. 1290 */ 1291 class CVC4_PUBLIC Datatype 1292 { 1293 friend class Solver; 1294 friend class Sort; 1295 1296 public: 1297 // !!! This constructor is only temporarily public until the parser is fully 1298 // migrated to the new API. !!! 1299 /** 1300 * Constructor. 1301 * @param dtype the internal datatype to be wrapped 1302 * @return the Datatype 1303 */ 1304 Datatype(const CVC4::Datatype& dtype); 1305 1306 /** 1307 * Destructor. 1308 */ 1309 ~Datatype(); 1310 1311 /** 1312 * Get the datatype constructor at a given index. 1313 * @param idx the index of the datatype constructor to return 1314 * @return the datatype constructor with the given index 1315 */ 1316 DatatypeConstructor operator[](size_t idx) const; 1317 1318 /** 1319 * Get the datatype constructor with the given name. 1320 * This is a linear search through the constructors, so in case of multiple, 1321 * similarly-named constructors, the first is returned. 1322 * @param name the name of the datatype constructor 1323 * @return the datatype constructor with the given name 1324 */ 1325 DatatypeConstructor operator[](const std::string& name) const; 1326 DatatypeConstructor getConstructor(const std::string& name) const; 1327 1328 /** 1329 * Get a term representing the datatype constructor with the given name. 1330 * This is a linear search through the constructors, so in case of multiple, 1331 * similarly-named constructors, the 1332 * first is returned. 1333 */ 1334 OpTerm getConstructorTerm(const std::string& name) const; 1335 1336 /** Get the number of constructors for this Datatype. */ 1337 size_t getNumConstructors() const; 1338 1339 /** Is this Datatype parametric? */ 1340 bool isParametric() const; 1341 1342 /** 1343 * @return a string representation of this datatype 1344 */ 1345 std::string toString() const; 1346 1347 /** 1348 * Iterator for the constructors of a datatype. 1349 */ 1350 class const_iterator : public std::iterator<std::input_iterator_tag, Datatype> 1351 { 1352 friend class Datatype; // to access constructor 1353 1354 public: 1355 /** 1356 * Assignment operator. 1357 * @param it the iterator to assign to 1358 * @return the reference to the iterator after assignment 1359 */ 1360 const_iterator& operator=(const const_iterator& it); 1361 1362 /** 1363 * Equality operator. 1364 * @param it the iterator to compare to for equality 1365 * @return true if the iterators are equal 1366 */ 1367 bool operator==(const const_iterator& it) const; 1368 1369 /** 1370 * Disequality operator. 1371 * @param it the iterator to compare to for disequality 1372 * @return true if the iterators are disequal 1373 */ 1374 bool operator!=(const const_iterator& it) const; 1375 1376 /** 1377 * Increment operator (prefix). 1378 * @return a reference to the iterator after incrementing by one 1379 */ 1380 const_iterator& operator++(); 1381 1382 /** 1383 * Increment operator (postfix). 1384 * @return a reference to the iterator after incrementing by one 1385 */ 1386 const_iterator operator++(int); 1387 1388 /** 1389 * Dereference operator. 1390 * @return a reference to the constructor this iterator points to 1391 */ 1392 const DatatypeConstructor& operator*() const; 1393 1394 /** 1395 * Dereference operator. 1396 * @return a pointer to the constructor this iterator points to 1397 */ 1398 const DatatypeConstructor* operator->() const; 1399 1400 private: 1401 /** 1402 * Constructor. 1403 * @param dtype the internal datatype to iterate over 1404 * @param true if this is a begin() iterator 1405 */ 1406 const_iterator(const CVC4::Datatype& dtype, bool begin); 1407 /* A pointer to the list of constructors of the internal datatype 1408 * to iterate over. 1409 * This pointer is maintained for operators == and != only. */ 1410 const void* d_int_ctors; 1411 /* The list of datatype constructor (wrappers) to iterate over. */ 1412 std::vector<DatatypeConstructor> d_ctors; 1413 /* The current index of the iterator. */ 1414 size_t d_idx; 1415 }; 1416 1417 /** 1418 * @return an iterator to the first constructor of this datatype 1419 */ 1420 const_iterator begin() const; 1421 1422 /** 1423 * @return an iterator to one-off-the-last constructor of this datatype 1424 */ 1425 const_iterator end() const; 1426 1427 // !!! This is only temporarily available until the parser is fully migrated 1428 // to the new API. !!! 1429 CVC4::Datatype getDatatype(void) const; 1430 1431 private: 1432 /** 1433 * The internal datatype wrapped by this datatype. 1434 * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is 1435 * not ref counted. 1436 */ 1437 std::shared_ptr<CVC4::Datatype> d_dtype; 1438 }; 1439 1440 /** 1441 * Serialize a datatype declaration to given stream. 1442 * @param out the output stream 1443 * @param dtdecl the datatype declaration to be serialized to the given stream 1444 * @return the output stream 1445 */ 1446 std::ostream& operator<<(std::ostream& out, 1447 const DatatypeDecl& dtdecl) CVC4_PUBLIC; 1448 1449 /** 1450 * Serialize a datatype constructor declaration to given stream. 1451 * @param out the output stream 1452 * @param ctordecl the datatype constructor declaration to be serialized 1453 * @return the output stream 1454 */ 1455 std::ostream& operator<<(std::ostream& out, 1456 const DatatypeConstructorDecl& ctordecl) CVC4_PUBLIC; 1457 1458 /** 1459 * Serialize a vector of datatype constructor declarations to given stream. 1460 * @param out the output stream 1461 * @param vector the vector of datatype constructor declarations to be 1462 * serialized to the given stream 1463 * @return the output stream 1464 */ 1465 std::ostream& operator<<(std::ostream& out, 1466 const std::vector<DatatypeConstructorDecl>& vector); 1467 1468 /** 1469 * Serialize a datatype selector declaration to given stream. 1470 * @param out the output stream 1471 * @param stordecl the datatype selector declaration to be serialized 1472 * @return the output stream 1473 */ 1474 std::ostream& operator<<(std::ostream& out, 1475 const DatatypeSelectorDecl& stordecl) CVC4_PUBLIC; 1476 1477 /** 1478 * Serialize a datatype to given stream. 1479 * @param out the output stream 1480 * @param dtdecl the datatype to be serialized to given stream 1481 * @return the output stream 1482 */ 1483 std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_PUBLIC; 1484 1485 /** 1486 * Serialize a datatype constructor to given stream. 1487 * @param out the output stream 1488 * @param ctor the datatype constructor to be serialized to given stream 1489 * @return the output stream 1490 */ 1491 std::ostream& operator<<(std::ostream& out, 1492 const DatatypeConstructor& ctor) CVC4_PUBLIC; 1493 1494 /** 1495 * Serialize a datatype selector to given stream. 1496 * @param out the output stream 1497 * @param ctor the datatype selector to be serialized to given stream 1498 * @return the output stream 1499 */ 1500 std::ostream& operator<<(std::ostream& out, 1501 const DatatypeSelector& stor) CVC4_PUBLIC; 1502 1503 /* -------------------------------------------------------------------------- */ 1504 /* Rounding Mode for Floating Points */ 1505 /* -------------------------------------------------------------------------- */ 1506 1507 /** 1508 * A CVC4 floating point rounding mode. 1509 */ 1510 enum CVC4_PUBLIC RoundingMode 1511 { 1512 ROUND_NEAREST_TIES_TO_EVEN, 1513 ROUND_TOWARD_POSITIVE, 1514 ROUND_TOWARD_NEGATIVE, 1515 ROUND_TOWARD_ZERO, 1516 ROUND_NEAREST_TIES_TO_AWAY, 1517 }; 1518 1519 /** 1520 * Hash function for RoundingModes. 1521 */ 1522 struct CVC4_PUBLIC RoundingModeHashFunction 1523 { 1524 inline size_t operator()(const RoundingMode& rm) const; 1525 }; 1526 1527 /* -------------------------------------------------------------------------- */ 1528 /* Solver */ 1529 /* -------------------------------------------------------------------------- */ 1530 1531 /* 1532 * A CVC4 solver. 1533 */ 1534 class CVC4_PUBLIC Solver 1535 { 1536 public: 1537 /* .................................................................... */ 1538 /* Constructors/Destructors */ 1539 /* .................................................................... */ 1540 1541 /** 1542 * Constructor. 1543 * @param opts a pointer to a solver options object (for parser only) 1544 * @return the Solver 1545 */ 1546 Solver(Options* opts = nullptr); 1547 1548 /** 1549 * Destructor. 1550 */ 1551 ~Solver(); 1552 1553 /** 1554 * Disallow copy/assignment. 1555 */ 1556 Solver(const Solver&) = delete; 1557 Solver& operator=(const Solver&) = delete; 1558 1559 /* .................................................................... */ 1560 /* Sorts Handling */ 1561 /* .................................................................... */ 1562 1563 /** 1564 * @return sort null 1565 */ 1566 Sort getNullSort() const; 1567 1568 /** 1569 * @return sort Boolean 1570 */ 1571 Sort getBooleanSort() const; 1572 1573 /** 1574 * @return sort Integer (in CVC4, Integer is a subtype of Real) 1575 */ 1576 Sort getIntegerSort() const; 1577 1578 /** 1579 * @return sort Real 1580 */ 1581 Sort getRealSort() const; 1582 1583 /** 1584 * @return sort RegExp 1585 */ 1586 Sort getRegExpSort() const; 1587 1588 /** 1589 * @return sort RoundingMode 1590 */ 1591 Sort getRoundingmodeSort() const; 1592 1593 /** 1594 * @return sort String 1595 */ 1596 Sort getStringSort() const; 1597 1598 /** 1599 * Create an array sort. 1600 * @param indexSort the array index sort 1601 * @param elemSort the array element sort 1602 * @return the array sort 1603 */ 1604 Sort mkArraySort(Sort indexSort, Sort elemSort) const; 1605 1606 /** 1607 * Create a bit-vector sort. 1608 * @param size the bit-width of the bit-vector sort 1609 * @return the bit-vector sort 1610 */ 1611 Sort mkBitVectorSort(uint32_t size) const; 1612 1613 /** 1614 * Create a floating-point sort. 1615 * @param exp the bit-width of the exponent of the floating-point sort. 1616 * @param sig the bit-width of the significand of the floating-point sort. 1617 */ 1618 Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const; 1619 1620 /** 1621 * Create a datatype sort. 1622 * @param dtypedecl the datatype declaration from which the sort is created 1623 * @return the datatype sort 1624 */ 1625 Sort mkDatatypeSort(DatatypeDecl dtypedecl) const; 1626 1627 /** 1628 * Create function sort. 1629 * @param domain the sort of the fuction argument 1630 * @param codomain the sort of the function return value 1631 * @return the function sort 1632 */ 1633 Sort mkFunctionSort(Sort domain, Sort codomain) const; 1634 1635 /** 1636 * Create function sort. 1637 * @param sorts the sort of the function arguments 1638 * @param codomain the sort of the function return value 1639 * @return the function sort 1640 */ 1641 Sort mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const; 1642 1643 /** 1644 * Create a sort parameter. 1645 * @param symbol the name of the sort 1646 * @return the sort parameter 1647 */ 1648 Sort mkParamSort(const std::string& symbol) const; 1649 1650 /** 1651 * Create a predicate sort. 1652 * @param sorts the list of sorts of the predicate 1653 * @return the predicate sort 1654 */ 1655 Sort mkPredicateSort(const std::vector<Sort>& sorts) const; 1656 1657 /** 1658 * Create a record sort 1659 * @param fields the list of fields of the record 1660 * @return the record sort 1661 */ 1662 Sort mkRecordSort( 1663 const std::vector<std::pair<std::string, Sort>>& fields) const; 1664 1665 /** 1666 * Create a set sort. 1667 * @param elemSort the sort of the set elements 1668 * @return the set sort 1669 */ 1670 Sort mkSetSort(Sort elemSort) const; 1671 1672 /** 1673 * Create an uninterpreted sort. 1674 * @param symbol the name of the sort 1675 * @return the uninterpreted sort 1676 */ 1677 Sort mkUninterpretedSort(const std::string& symbol) const; 1678 1679 /** 1680 * Create a sort constructor sort. 1681 * @param symbol the symbol of the sort 1682 * @param arity the arity of the sort 1683 * @return the sort constructor sort 1684 */ 1685 Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const; 1686 1687 /** 1688 * Create a tuple sort. 1689 * @param sorts of the elements of the tuple 1690 * @return the tuple sort 1691 */ 1692 Sort mkTupleSort(const std::vector<Sort>& sorts) const; 1693 1694 /* .................................................................... */ 1695 /* Create Terms */ 1696 /* .................................................................... */ 1697 1698 /** 1699 * Create 0-ary term of given kind. 1700 * @param kind the kind of the term 1701 * @return the Term 1702 */ 1703 Term mkTerm(Kind kind) const; 1704 1705 /** 1706 * Create a unary term of given kind. 1707 * @param kind the kind of the term 1708 * @param child the child of the term 1709 * @return the Term 1710 */ 1711 Term mkTerm(Kind kind, Term child) const; 1712 1713 /** 1714 * Create binary term of given kind. 1715 * @param kind the kind of the term 1716 * @param child1 the first child of the term 1717 * @param child2 the second child of the term 1718 * @return the Term 1719 */ 1720 Term mkTerm(Kind kind, Term child1, Term child2) const; 1721 1722 /** 1723 * Create ternary term of given kind. 1724 * @param kind the kind of the term 1725 * @param child1 the first child of the term 1726 * @param child2 the second child of the term 1727 * @param child3 the third child of the term 1728 * @return the Term 1729 */ 1730 Term mkTerm(Kind kind, Term child1, Term child2, Term child3) const; 1731 1732 /** 1733 * Create n-ary term of given kind. 1734 * @param kind the kind of the term 1735 * @param children the children of the term 1736 * @return the Term 1737 */ 1738 Term mkTerm(Kind kind, const std::vector<Term>& children) const; 1739 1740 /** 1741 * Create nullary term of given kind from a given operator term. 1742 * Create operator terms with mkOpTerm(). 1743 * @param kind the kind of the term 1744 * @param the operator term 1745 * @return the Term 1746 */ 1747 Term mkTerm(Kind kind, OpTerm opTerm) const; 1748 1749 /** 1750 * Create unary term of given kind from a given operator term. 1751 * Create operator terms with mkOpTerm(). 1752 * @param kind the kind of the term 1753 * @param the operator term 1754 * @child the child of the term 1755 * @return the Term 1756 */ 1757 Term mkTerm(Kind kind, OpTerm opTerm, Term child) const; 1758 1759 /** 1760 * Create binary term of given kind from a given operator term. 1761 * @param kind the kind of the term 1762 * Create operator terms with mkOpTerm(). 1763 * @param the operator term 1764 * @child1 the first child of the term 1765 * @child2 the second child of the term 1766 * @return the Term 1767 */ 1768 Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const; 1769 1770 /** 1771 * Create ternary term of given kind from a given operator term. 1772 * Create operator terms with mkOpTerm(). 1773 * @param kind the kind of the term 1774 * @param the operator term 1775 * @child1 the first child of the term 1776 * @child2 the second child of the term 1777 * @child3 the third child of the term 1778 * @return the Term 1779 */ 1780 Term mkTerm( 1781 Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const; 1782 1783 /** 1784 * Create n-ary term of given kind from a given operator term. 1785 * Create operator terms with mkOpTerm(). 1786 * @param kind the kind of the term 1787 * @param the operator term 1788 * @children the children of the term 1789 * @return the Term 1790 */ 1791 Term mkTerm(Kind kind, 1792 OpTerm opTerm, 1793 const std::vector<Term>& children) const; 1794 1795 /** 1796 * Create a tuple term. Terms are automatically converted if sorts are 1797 * compatible. 1798 * @param sorts The sorts of the elements in the tuple 1799 * @param terms The elements in the tuple 1800 * @return the tuple Term 1801 */ 1802 Term mkTuple(const std::vector<Sort>& sorts, 1803 const std::vector<Term>& terms) const; 1804 1805 /* .................................................................... */ 1806 /* Create Operator Terms */ 1807 /* .................................................................... */ 1808 1809 /** 1810 * Create operator term of kind: 1811 * - CHAIN_OP 1812 * See enum Kind for a description of the parameters. 1813 * @param kind the kind of the operator 1814 * @param k the kind argument to this operator 1815 */ 1816 OpTerm mkOpTerm(Kind kind, Kind k); 1817 1818 /** 1819 * Create operator of kind: 1820 * - RECORD_UPDATE_OP 1821 * See enum Kind for a description of the parameters. 1822 * @param kind the kind of the operator 1823 * @param arg the string argument to this operator 1824 */ 1825 OpTerm mkOpTerm(Kind kind, const std::string& arg); 1826 1827 /** 1828 * Create operator of kind: 1829 * - DIVISIBLE_OP 1830 * - BITVECTOR_REPEAT_OP 1831 * - BITVECTOR_ZERO_EXTEND_OP 1832 * - BITVECTOR_SIGN_EXTEND_OP 1833 * - BITVECTOR_ROTATE_LEFT_OP 1834 * - BITVECTOR_ROTATE_RIGHT_OP 1835 * - INT_TO_BITVECTOR_OP 1836 * - FLOATINGPOINT_TO_UBV_OP 1837 * - FLOATINGPOINT_TO_UBV_TOTAL_OP 1838 * - FLOATINGPOINT_TO_SBV_OP 1839 * - FLOATINGPOINT_TO_SBV_TOTAL_OP 1840 * - TUPLE_UPDATE_OP 1841 * See enum Kind for a description of the parameters. 1842 * @param kind the kind of the operator 1843 * @param arg the uint32_t argument to this operator 1844 */ 1845 OpTerm mkOpTerm(Kind kind, uint32_t arg); 1846 1847 /** 1848 * Create operator of Kind: 1849 * - BITVECTOR_EXTRACT_OP 1850 * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1851 * - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 1852 * - FLOATINGPOINT_TO_FP_REAL_OP 1853 * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 1854 * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 1855 * - FLOATINGPOINT_TO_FP_GENERIC_OP 1856 * See enum Kind for a description of the parameters. 1857 * @param kind the kind of the operator 1858 * @param arg1 the first uint32_t argument to this operator 1859 * @param arg2 the second uint32_t argument to this operator 1860 */ 1861 OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2); 1862 1863 /* .................................................................... */ 1864 /* Create Constants */ 1865 /* .................................................................... */ 1866 1867 /** 1868 * Create a Boolean true constant. 1869 * @return the true constant 1870 */ 1871 Term mkTrue() const; 1872 1873 /** 1874 * Create a Boolean false constant. 1875 * @return the false constant 1876 */ 1877 Term mkFalse() const; 1878 1879 /** 1880 * Create a Boolean constant. 1881 * @return the Boolean constant 1882 * @param val the value of the constant 1883 */ 1884 Term mkBoolean(bool val) const; 1885 1886 /** 1887 * Create a constant representing the number Pi. 1888 * @return a constant representing Pi 1889 */ 1890 Term mkPi() const; 1891 1892 /** 1893 * Create a real constant from a string. 1894 * @param s the string representation of the constant, may represent an 1895 * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). 1896 * @return a constant of sort Real or Integer (if 's' represents an integer) 1897 */ 1898 Term mkReal(const char* s) const; 1899 1900 /** 1901 * Create a real constant from a string. 1902 * @param s the string representation of the constant, may represent an 1903 * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). 1904 * @return a constant of sort Real or Integer (if 's' represents an integer) 1905 */ 1906 Term mkReal(const std::string& s) const; 1907 1908 /** 1909 * Create a real constant from an integer. 1910 * @param val the value of the constant 1911 * @return a constant of sort Integer 1912 */ 1913 Term mkReal(int32_t val) const; 1914 1915 /** 1916 * Create a real constant from an integer. 1917 * @param val the value of the constant 1918 * @return a constant of sort Integer 1919 */ 1920 Term mkReal(int64_t val) const; 1921 1922 /** 1923 * Create a real constant from an unsigned integer. 1924 * @param val the value of the constant 1925 * @return a constant of sort Integer 1926 */ 1927 Term mkReal(uint32_t val) const; 1928 1929 /** 1930 * Create a real constant from an unsigned integer. 1931 * @param val the value of the constant 1932 * @return a constant of sort Integer 1933 */ 1934 Term mkReal(uint64_t val) const; 1935 1936 /** 1937 * Create a real constant from a rational. 1938 * @param num the value of the numerator 1939 * @param den the value of the denominator 1940 * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') 1941 */ 1942 Term mkReal(int32_t num, int32_t den) const; 1943 1944 /** 1945 * Create a real constant from a rational. 1946 * @param num the value of the numerator 1947 * @param den the value of the denominator 1948 * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') 1949 */ 1950 Term mkReal(int64_t num, int64_t den) const; 1951 1952 /** 1953 * Create a real constant from a rational. 1954 * @param num the value of the numerator 1955 * @param den the value of the denominator 1956 * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') 1957 */ 1958 Term mkReal(uint32_t num, uint32_t den) const; 1959 1960 /** 1961 * Create a real constant from a rational. 1962 * @param num the value of the numerator 1963 * @param den the value of the denominator 1964 * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') 1965 */ 1966 Term mkReal(uint64_t num, uint64_t den) const; 1967 1968 /** 1969 * Create a regular expression empty term. 1970 * @return the empty term 1971 */ 1972 Term mkRegexpEmpty() const; 1973 1974 /** 1975 * Create a regular expression sigma term. 1976 * @return the sigma term 1977 */ 1978 Term mkRegexpSigma() const; 1979 1980 /** 1981 * Create a constant representing an empty set of the given sort. 1982 * @param s the sort of the set elements. 1983 * @return the empty set constant 1984 */ 1985 Term mkEmptySet(Sort s) const; 1986 1987 /** 1988 * Create a separation logic nil term. 1989 * @param sort the sort of the nil term 1990 * @return the separation logic nil term 1991 */ 1992 Term mkSepNil(Sort sort) const; 1993 1994 /** 1995 * Create a String constant. 1996 * @param s the string this constant represents 1997 * @param useEscSequences determines whether escape sequences in \p s should 1998 * be converted to the corresponding character 1999 * @return the String constant 2000 */ 2001 Term mkString(const char* s, bool useEscSequences = false) const; 2002 2003 /** 2004 * Create a String constant. 2005 * @param s the string this constant represents 2006 * @param useEscSequences determines whether escape sequences in \p s should 2007 * be converted to the corresponding character 2008 * @return the String constant 2009 */ 2010 Term mkString(const std::string& s, bool useEscSequences = false) const; 2011 2012 /** 2013 * Create a String constant. 2014 * @param c the character this constant represents 2015 * @return the String constant 2016 */ 2017 Term mkString(const unsigned char c) const; 2018 2019 /** 2020 * Create a String constant. 2021 * @param s a list of unsigned values this constant represents as string 2022 * @return the String constant 2023 */ 2024 Term mkString(const std::vector<unsigned>& s) const; 2025 2026 /** 2027 * Create a universe set of the given sort. 2028 * @param sort the sort of the set elements 2029 * @return the universe set constant 2030 */ 2031 Term mkUniverseSet(Sort sort) const; 2032 2033 /** 2034 * Create a bit-vector constant of given size and value. 2035 * @param size the bit-width of the bit-vector sort 2036 * @param val the value of the constant 2037 * @return the bit-vector constant 2038 */ 2039 Term mkBitVector(uint32_t size, uint64_t val = 0) const; 2040 2041 /** 2042 * Create a bit-vector constant from a given string. 2043 * @param s the string representation of the constant 2044 * @param base the base of the string representation (2, 10, or 16) 2045 * @return the bit-vector constant 2046 */ 2047 Term mkBitVector(const char* s, uint32_t base = 2) const; 2048 2049 /** 2050 * Create a bit-vector constant from a given string of base 2, 10 or 16. 2051 * 2052 * The size of resulting bit-vector is 2053 * - base 2: the size of the binary string 2054 * - base 10: the min. size required to represent the decimal as a bit-vector 2055 * - base 16: the max. size required to represent the hexadecimal as a 2056 * bit-vector (4 * size of the given value string) 2057 * 2058 * @param s the string representation of the constant 2059 * @param base the base of the string representation (2, 10, or 16) 2060 * @return the bit-vector constant 2061 */ 2062 Term mkBitVector(const std::string& s, uint32_t base = 2) const; 2063 2064 /** 2065 * Create a bit-vector constant of a given bit-width from a given string of 2066 * base 2, 10 or 16. 2067 * 2068 * @param size the bit-width of the constant 2069 * @param s the string representation of the constant 2070 * @param base the base of the string representation (2, 10, or 16) 2071 * @return the bit-vector constant 2072 */ 2073 Term mkBitVector(uint32_t size, const char* s, uint32_t base) const; 2074 2075 /** 2076 * Create a bit-vector constant of a given bit-width from a given string of 2077 * base 2, 10 or 16. 2078 * @param size the bit-width of the constant 2079 * @param s the string representation of the constant 2080 * @param base the base of the string representation (2, 10, or 16) 2081 * @return the bit-vector constant 2082 */ 2083 Term mkBitVector(uint32_t size, std::string& s, uint32_t base) const; 2084 2085 /** 2086 * Create a positive infinity floating-point constant. Requires CVC4 to be 2087 * compiled with SymFPU support. 2088 * @param exp Number of bits in the exponent 2089 * @param sig Number of bits in the significand 2090 * @return the floating-point constant 2091 */ 2092 Term mkPosInf(uint32_t exp, uint32_t sig) const; 2093 2094 /** 2095 * Create a negative infinity floating-point constant. Requires CVC4 to be 2096 * compiled with SymFPU support. 2097 * @param exp Number of bits in the exponent 2098 * @param sig Number of bits in the significand 2099 * @return the floating-point constant 2100 */ 2101 Term mkNegInf(uint32_t exp, uint32_t sig) const; 2102 2103 /** 2104 * Create a not-a-number (NaN) floating-point constant. Requires CVC4 to be 2105 * compiled with SymFPU support. 2106 * @param exp Number of bits in the exponent 2107 * @param sig Number of bits in the significand 2108 * @return the floating-point constant 2109 */ 2110 Term mkNaN(uint32_t exp, uint32_t sig) const; 2111 2112 /** 2113 * Create a positive zero (+0.0) floating-point constant. Requires CVC4 to be 2114 * compiled with SymFPU support. 2115 * @param exp Number of bits in the exponent 2116 * @param sig Number of bits in the significand 2117 * @return the floating-point constant 2118 */ 2119 Term mkPosZero(uint32_t exp, uint32_t sig) const; 2120 2121 /** 2122 * Create a negative zero (-0.0) floating-point constant. Requires CVC4 to be 2123 * compiled with SymFPU support. 2124 * @param exp Number of bits in the exponent 2125 * @param sig Number of bits in the significand 2126 * @return the floating-point constant 2127 */ 2128 Term mkNegZero(uint32_t exp, uint32_t sig) const; 2129 2130 /** 2131 * Create a roundingmode constant. 2132 * @param rm the floating point rounding mode this constant represents 2133 */ 2134 Term mkRoundingMode(RoundingMode rm) const; 2135 2136 /** 2137 * Create uninterpreted constant. 2138 * @param arg1 Sort of the constant 2139 * @param arg2 Index of the constant 2140 */ 2141 Term mkUninterpretedConst(Sort sort, int32_t index) const; 2142 2143 /** 2144 * Create an abstract value constant. 2145 * @param index Index of the abstract value 2146 */ 2147 Term mkAbstractValue(const std::string& index) const; 2148 2149 /** 2150 * Create an abstract value constant. 2151 * @param index Index of the abstract value 2152 */ 2153 Term mkAbstractValue(uint64_t index) const; 2154 2155 /** 2156 * Create a floating-point constant (requires CVC4 to be compiled with symFPU 2157 * support). 2158 * @param exp Size of the exponent 2159 * @param sig Size of the significand 2160 * @param val Value of the floating-point constant as a bit-vector term 2161 */ 2162 Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const; 2163 2164 /* .................................................................... */ 2165 /* Create Variables */ 2166 /* .................................................................... */ 2167 2168 /** 2169 * Create variable. 2170 * @param sort the sort of the variable 2171 * @param symbol the name of the variable 2172 * @return the variable 2173 */ 2174 Term mkVar(Sort sort, const std::string& symbol = std::string()) const; 2175 2176 /** 2177 * Create bound variable. 2178 * @param sort the sort of the variable 2179 * @param symbol the name of the variable 2180 * @return the variable 2181 */ 2182 Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const; 2183 2184 /* .................................................................... */ 2185 /* Formula Handling */ 2186 /* .................................................................... */ 2187 2188 /** 2189 * Simplify a formula without doing "much" work. Does not involve 2190 * the SAT Engine in the simplification, but uses the current 2191 * definitions, assertions, and the current partial model, if one 2192 * has been constructed. It also involves theory normalization. 2193 * @param t the formula to simplify 2194 * @return the simplified formula 2195 */ 2196 Term simplify(const Term& t); 2197 2198 /** 2199 * Assert a formula. 2200 * SMT-LIB: ( assert <term> ) 2201 * @param term the formula to assert 2202 */ 2203 void assertFormula(Term term) const; 2204 2205 /** 2206 * Check satisfiability. 2207 * SMT-LIB: ( check-sat ) 2208 * @return the result of the satisfiability check. 2209 */ 2210 Result checkSat() const; 2211 2212 /** 2213 * Check satisfiability assuming the given formula. 2214 * SMT-LIB: ( check-sat-assuming ( <prop_literal> ) ) 2215 * @param assumption the formula to assume 2216 * @return the result of the satisfiability check. 2217 */ 2218 Result checkSatAssuming(Term assumption) const; 2219 2220 /** 2221 * Check satisfiability assuming the given formulas. 2222 * SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) ) 2223 * @param assumptions the formulas to assume 2224 * @return the result of the satisfiability check. 2225 */ 2226 Result checkSatAssuming(const std::vector<Term>& assumptions) const; 2227 2228 /** 2229 * Check validity. 2230 * @return the result of the validity check. 2231 */ 2232 Result checkValid() const; 2233 2234 /** 2235 * Check validity assuming the given formula. 2236 * @param assumption the formula to assume 2237 * @return the result of the validity check. 2238 */ 2239 Result checkValidAssuming(Term assumption) const; 2240 2241 /** 2242 * Check validity assuming the given formulas. 2243 * @param assumptions the formulas to assume 2244 * @return the result of the validity check. 2245 */ 2246 Result checkValidAssuming(const std::vector<Term>& assumptions) const; 2247 2248 /** 2249 * Declare first-order constant (0-arity function symbol). 2250 * SMT-LIB: ( declare-const <symbol> <sort> ) 2251 * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) 2252 * This command corresponds to mkVar(). 2253 * @param symbol the name of the first-order constant 2254 * @param sort the sort of the first-order constant 2255 * @return the first-order constant 2256 */ 2257 Term declareConst(const std::string& symbol, Sort sort) const; 2258 2259 /** 2260 * Create datatype sort. 2261 * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> ) 2262 * @param symbol the name of the datatype sort 2263 * @param ctors the constructor declarations of the datatype sort 2264 * @return the datatype sort 2265 */ 2266 Sort declareDatatype(const std::string& symbol, 2267 const std::vector<DatatypeConstructorDecl>& ctors) const; 2268 2269 /** 2270 * Declare n-ary function symbol. 2271 * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> ) 2272 * @param symbol the name of the function 2273 * @param sorts the sorts of the parameters to this function 2274 * @param sort the sort of the return value of this function 2275 * @return the function 2276 */ 2277 Term declareFun(const std::string& symbol, 2278 const std::vector<Sort>& sorts, 2279 Sort sort) const; 2280 2281 /** 2282 * Declare uninterpreted sort. 2283 * SMT-LIB: ( declare-sort <symbol> <numeral> ) 2284 * @param symbol the name of the sort 2285 * @param arity the arity of the sort 2286 * @return the sort 2287 */ 2288 Sort declareSort(const std::string& symbol, uint32_t arity) const; 2289 2290 /** 2291 * Define n-ary function. 2292 * SMT-LIB: ( define-fun <function_def> ) 2293 * @param symbol the name of the function 2294 * @param bound_vars the parameters to this function 2295 * @param sort the sort of the return value of this function 2296 * @param term the function body 2297 * @return the function 2298 */ 2299 Term defineFun(const std::string& symbol, 2300 const std::vector<Term>& bound_vars, 2301 Sort sort, 2302 Term term) const; 2303 /** 2304 * Define n-ary function. 2305 * SMT-LIB: ( define-fun <function_def> ) 2306 * Create parameter 'fun' with mkVar(). 2307 * @param fun the sorted function 2308 * @param bound_vars the parameters to this function 2309 * @param term the function body 2310 * @return the function 2311 */ 2312 Term defineFun(Term fun, 2313 const std::vector<Term>& bound_vars, 2314 Term term) const; 2315 2316 /** 2317 * Define recursive function. 2318 * SMT-LIB: ( define-fun-rec <function_def> ) 2319 * @param symbol the name of the function 2320 * @param bound_vars the parameters to this function 2321 * @param sort the sort of the return value of this function 2322 * @param term the function body 2323 * @return the function 2324 */ 2325 Term defineFunRec(const std::string& symbol, 2326 const std::vector<Term>& bound_vars, 2327 Sort sort, 2328 Term term) const; 2329 2330 /** 2331 * Define recursive function. 2332 * SMT-LIB: ( define-fun-rec <function_def> ) 2333 * Create parameter 'fun' with mkVar(). 2334 * @param fun the sorted function 2335 * @param bound_vars the parameters to this function 2336 * @param term the function body 2337 * @return the function 2338 */ 2339 Term defineFunRec(Term fun, 2340 const std::vector<Term>& bound_vars, 2341 Term term) const; 2342 2343 /** 2344 * Define recursive functions. 2345 * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) 2346 * Create elements of parameter 'funs' with mkVar(). 2347 * @param funs the sorted functions 2348 * @param bound_vars the list of parameters to the functions 2349 * @param term the list of function bodies of the functions 2350 * @return the function 2351 */ 2352 void defineFunsRec(const std::vector<Term>& funs, 2353 const std::vector<std::vector<Term>>& bound_vars, 2354 const std::vector<Term>& terms) const; 2355 2356 /** 2357 * Echo a given string to the given output stream. 2358 * SMT-LIB: ( echo <std::string> ) 2359 * @param out the output stream 2360 * @param str the string to echo 2361 */ 2362 void echo(std::ostream& out, const std::string& str) const; 2363 2364 /** 2365 * Get the list of asserted formulas. 2366 * SMT-LIB: ( get-assertions ) 2367 * @return the list of asserted formulas 2368 */ 2369 std::vector<Term> getAssertions() const; 2370 2371 /** 2372 * Get the assignment of asserted formulas. 2373 * SMT-LIB: ( get-assignment ) 2374 * Requires to enable option 'produce-assignments'. 2375 * @return a list of formula-assignment pairs 2376 */ 2377 std::vector<std::pair<Term, Term>> getAssignment() const; 2378 2379 /** 2380 * Get info from the solver. 2381 * SMT-LIB: ( get-info <info_flag> ) 2382 * @return the info 2383 */ 2384 std::string getInfo(const std::string& flag) const; 2385 2386 /** 2387 * Get the value of a given option. 2388 * SMT-LIB: ( get-option <keyword> ) 2389 * @param option the option for which the value is queried 2390 * @return a string representation of the option value 2391 */ 2392 std::string getOption(const std::string& option) const; 2393 2394 /** 2395 * Get the set of unsat ("failed") assumptions. 2396 * SMT-LIB: ( get-unsat-assumptions ) 2397 * Requires to enable option 'produce-unsat-assumptions'. 2398 * @return the set of unsat assumptions. 2399 */ 2400 std::vector<Term> getUnsatAssumptions() const; 2401 2402 /** 2403 * Get the unsatisfiable core. 2404 * SMT-LIB: ( get-unsat-core ) 2405 * Requires to enable option 'produce-unsat-cores'. 2406 * @return a set of terms representing the unsatisfiable core 2407 */ 2408 std::vector<Term> getUnsatCore() const; 2409 2410 /** 2411 * Get the value of the given term. 2412 * SMT-LIB: ( get-value ( <term> ) ) 2413 * @param term the term for which the value is queried 2414 * @return the value of the given term 2415 */ 2416 Term getValue(Term term) const; 2417 /** 2418 * Get the values of the given terms. 2419 * SMT-LIB: ( get-value ( <term>+ ) ) 2420 * @param terms the terms for which the value is queried 2421 * @return the values of the given terms 2422 */ 2423 std::vector<Term> getValue(const std::vector<Term>& terms) const; 2424 2425 /** 2426 * Pop (a) level(s) from the assertion stack. 2427 * SMT-LIB: ( pop <numeral> ) 2428 * @param nscopes the number of levels to pop 2429 */ 2430 void pop(uint32_t nscopes = 1) const; 2431 2432 /** 2433 * Print the model of a satisfiable query to the given output stream. 2434 * Requires to enable option 'produce-models'. 2435 * @param out the output stream 2436 */ 2437 void printModel(std::ostream& out) const; 2438 2439 /** 2440 * Push (a) level(s) to the assertion stack. 2441 * SMT-LIB: ( push <numeral> ) 2442 * @param nscopes the number of levels to push 2443 */ 2444 void push(uint32_t nscopes = 1) const; 2445 2446 /** 2447 * Reset the solver. 2448 * SMT-LIB: ( reset ) 2449 */ 2450 void reset() const; 2451 2452 /** 2453 * Remove all assertions. 2454 * SMT-LIB: ( reset-assertions ) 2455 */ 2456 void resetAssertions() const; 2457 2458 /** 2459 * Set info. 2460 * SMT-LIB: ( set-info <attribute> ) 2461 * @param keyword the info flag 2462 * @param value the value of the info flag 2463 */ 2464 void setInfo(const std::string& keyword, const std::string& value) const; 2465 2466 /** 2467 * Set logic. 2468 * SMT-LIB: ( set-logic <symbol> ) 2469 * @param logic the logic to set 2470 */ 2471 void setLogic(const std::string& logic) const; 2472 2473 /** 2474 * Set option. 2475 * SMT-LIB: ( set-option <option> ) 2476 * @param option the option name 2477 * @param value the option value 2478 */ 2479 void setOption(const std::string& option, const std::string& value) const; 2480 2481 /** 2482 * If needed, convert this term to a given sort. Note that the sort of the 2483 * term must be convertible into the target sort. Currently only Int to Real 2484 * conversions are supported. 2485 * @param s the target sort 2486 * @return the term wrapped into a sort conversion if needed 2487 */ 2488 Term ensureTermSort(const Term& t, const Sort& s) const; 2489 2490 // !!! This is only temporarily available until the parser is fully migrated 2491 // to the new API. !!! 2492 ExprManager* getExprManager(void) const; 2493 2494 // !!! This is only temporarily available until the parser is fully migrated 2495 // to the new API. !!! 2496 SmtEngine* getSmtEngine(void) const; 2497 2498 private: 2499 /* Helper to convert a vector of internal types to sorts. */ 2500 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; 2501 /* Helper to convert a vector of sorts to internal types. */ 2502 std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const; 2503 /* Helper to check for API misuse in mkTerm functions. */ 2504 void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const; 2505 /* Helper to check for API misuse in mkOpTerm functions. */ 2506 void checkMkTerm(Kind kind, uint32_t nchildren) const; 2507 /* Helper for mk-functions that call d_exprMgr->mkConst(). */ 2508 template <typename T> 2509 Term mkConstHelper(T t) const; 2510 /* Helper for mkReal functions that take a string as argument. */ 2511 Term mkRealFromStrHelper(std::string s) const; 2512 /* Helper for mkBitVector functions that take a string as argument. */ 2513 Term mkBVFromStrHelper(std::string s, uint32_t base) const; 2514 /* Helper for mkBitVector functions that take a string and a size as 2515 * arguments. */ 2516 Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const; 2517 /* Helper for mkBitVector functions that take an integer as argument. */ 2518 Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; 2519 /* Helper for setLogic. */ 2520 void setLogicHelper(const std::string& logic) const; 2521 2522 /** 2523 * Helper function that ensures that a given term is of sort real (as opposed 2524 * to being of sort integer). 2525 * @param term a term of sort integer or real 2526 * @return a term of sort real 2527 */ 2528 Term ensureRealSort(Term expr) const; 2529 2530 /* The expression manager of this solver. */ 2531 std::unique_ptr<ExprManager> d_exprMgr; 2532 /* The SMT engine of this solver. */ 2533 std::unique_ptr<SmtEngine> d_smtEngine; 2534 /* The random number generator of this solver. */ 2535 std::unique_ptr<Random> d_rng; 2536 }; 2537 2538 } // namespace api 2539 } // namespace CVC4 2540 #endif 2541