1 /********************* */ 2 /*! \file cvc4cppkind.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Aina Niemetz 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 term kinds of the CVC4 C++ API. 13 ** 14 ** The term kinds of the CVC4 C++ API. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef __CVC4__API__CVC4CPPKIND_H 20 #define __CVC4__API__CVC4CPPKIND_H 21 22 #include <ostream> 23 24 namespace CVC4 { 25 namespace api { 26 27 /* -------------------------------------------------------------------------- */ 28 /* Kind */ 29 /* -------------------------------------------------------------------------- */ 30 31 /** 32 * The kind of a CVC4 term. 33 * 34 * Note that the underlying type of Kind must be signed (to enable range 35 * checks for validity). The size of this type depends on the size of 36 * CVC4::Kind (__CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits, 37 * see expr/metakind_template.h). 38 */ 39 enum CVC4_PUBLIC Kind : int32_t 40 { 41 /** 42 * Internal kind. 43 * Should never be exposed or created via the API. 44 */ 45 INTERNAL_KIND = -2, 46 /** 47 * Undefined kind. 48 * Should never be exposed or created via the API. 49 */ 50 UNDEFINED_KIND = -1, 51 /** 52 * Null kind (kind of null term Term()). 53 * Do not explicitly create via API functions other than Term(). 54 */ 55 NULL_EXPR, 56 57 /* Builtin --------------------------------------------------------------- */ 58 59 /** 60 * Uninterpreted constant. 61 * Parameters: 2 62 * -[1]: Sort of the constant 63 * -[2]: Index of the constant 64 * Create with: 65 * mkUninterpretedConst(Sort sort, int32_t index) 66 */ 67 UNINTERPRETED_CONSTANT, 68 /** 69 * Abstract value (other than uninterpreted sort constants). 70 * Parameters: 1 71 * -[1]: Index of the abstract value 72 * Create with: 73 * mkAbstractValue(const std::string& index); 74 * mkAbstractValue(uint64_t index); 75 */ 76 ABSTRACT_VALUE, 77 #if 0 78 /* Built-in operator */ 79 BUILTIN, 80 #endif 81 /** 82 * Defined function. 83 * Parameters: 3 (4) 84 * See defineFun(). 85 * Create with: 86 * defineFun(const std::string& symbol, 87 * const std::vector<Term>& bound_vars, 88 * Sort sort, 89 * Term term) 90 * defineFun(Term fun, 91 * const std::vector<Term>& bound_vars, 92 * Term term) 93 */ 94 FUNCTION, 95 /** 96 * Application of a defined function. 97 * Parameters: n > 1 98 * -[1]..[n]: Function argument instantiation Terms 99 * Create with: 100 * mkTerm(Kind kind, Term child) 101 * mkTerm(Kind kind, Term child1, Term child2) 102 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 103 * mkTerm(Kind kind, const std::vector<Term>& children) 104 */ 105 APPLY, 106 /** 107 * Equality. 108 * Parameters: 2 109 * -[1]..[2]: Terms with same sort 110 * Create with: 111 * mkTerm(Kind kind, Term child1, Term child2) 112 * mkTerm(Kind kind, const std::vector<Term>& children) 113 */ 114 EQUAL, 115 /** 116 * Disequality. 117 * Parameters: n > 1 118 * -[1]..[n]: Terms with same sort 119 * Create with: 120 * mkTerm(Kind kind, Term child1, Term child2) 121 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 122 * mkTerm(Kind kind, const std::vector<Term>& children) 123 */ 124 DISTINCT, 125 /** 126 * Variable. 127 * Not permitted in bindings (forall, exists, ...). 128 * Parameters: 129 * See mkVar(). 130 * Create with: 131 * mkVar(const std::string& symbol, Sort sort) 132 * mkVar(Sort sort) 133 */ 134 VARIABLE, 135 /** 136 * Bound variable. 137 * Permitted in bindings and in the lambda and quantifier bodies only. 138 * Parameters: 139 * See mkBoundVar(). 140 * Create with: 141 * mkBoundVar(const std::string& symbol, Sort sort) 142 * mkBoundVar(Sort sort) 143 */ 144 BOUND_VARIABLE, 145 #if 0 146 /* Skolem variable (internal only) */ 147 SKOLEM, 148 /* Symbolic expression (any arity) */ 149 SEXPR, 150 #endif 151 /** 152 * Lambda expression. 153 * Parameters: 2 154 * -[1]: BOUND_VAR_LIST 155 * -[2]: Lambda body 156 * Create with: 157 * mkTerm(Kind kind, Term child1, Term child2) 158 * mkTerm(Kind kind, const std::vector<Term>& children) 159 */ 160 LAMBDA, 161 /** 162 * Hilbert choice (epsilon) expression. 163 * Parameters: 2 164 * -[1]: BOUND_VAR_LIST 165 * -[2]: Hilbert choice body 166 * Create with: 167 * mkTerm(Kind kind, Term child1, Term child2) 168 * mkTerm(Kind kind, const std::vector<Term>& children) 169 */ 170 CHOICE, 171 /** 172 * Chained operation. 173 * Parameters: n > 1 174 * -[1]: Term of kind CHAIN_OP (represents a binary op) 175 * -[2]..[n]: Arguments to that operator 176 * Create with: 177 * mkTerm(Kind kind, Term child1, Term child2) 178 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 179 * mkTerm(Kind kind, const std::vector<Term>& children) 180 * Turned into a conjunction of binary applications of the operator on 181 * adjoining parameters. 182 */ 183 CHAIN, 184 /** 185 * Chained operator. 186 * Parameters: 1 187 * -[1]: Kind of the binary operation 188 * Create with: 189 * mkOpTerm(Kind opkind, Kind kind) 190 */ 191 CHAIN_OP, 192 193 /* Boolean --------------------------------------------------------------- */ 194 195 /** 196 * Boolean constant. 197 * Parameters: 1 198 * -[1]: Boolean value of the constant 199 * Create with: 200 * mkTrue() 201 * mkFalse() 202 * mkBoolean(bool val) 203 */ 204 CONST_BOOLEAN, 205 /* Logical not. 206 * Parameters: 1 207 * -[1]: Boolean Term to negate 208 * Create with: 209 * mkTerm(Kind kind, Term child) 210 */ 211 NOT, 212 /* Logical and. 213 * Parameters: n > 1 214 * -[1]..[n]: Boolean Term of the conjunction 215 * Create with: 216 * mkTerm(Kind kind, Term child1, Term child2) 217 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 218 * mkTerm(Kind kind, const std::vector<Term>& children) 219 */ 220 AND, 221 /** 222 * Logical implication. 223 * Parameters: 2 224 * -[1]..[2]: Boolean Terms, [1] implies [2] 225 * Create with: 226 * mkTerm(Kind kind, Term child1, Term child2) 227 * mkTerm(Kind kind, const std::vector<Term>& children) 228 */ 229 IMPLIES, 230 /* Logical or. 231 * Parameters: n > 1 232 * -[1]..[n]: Boolean Term of the disjunction 233 * Create with: 234 * mkTerm(Kind kind, Term child1, Term child2) 235 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 236 * mkTerm(Kind kind, const std::vector<Term>& children) 237 */ 238 OR, 239 /* Logical exclusive or. 240 * Parameters: 2 241 * -[1]..[2]: Boolean Terms, [1] xor [2] 242 * Create with: 243 * mkTerm(Kind kind, Term child1, Term child2) 244 * mkTerm(Kind kind, const std::vector<Term>& children) 245 */ 246 XOR, 247 /* If-then-else. 248 * Parameters: 3 249 * -[1] is a Boolean condition Term 250 * -[2] the 'then' Term 251 * -[3] the 'else' Term 252 * 'then' and 'else' term must have same base sort. 253 * Create with: 254 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 255 * mkTerm(Kind kind, const std::vector<Term>& children) 256 */ 257 ITE, 258 259 /* UF -------------------------------------------------------------------- */ 260 261 /* Application of an uninterpreted function. 262 * Parameters: n > 1 263 * -[1]: Function Term 264 * -[2]..[n]: Function argument instantiation Terms 265 * Create with: 266 * mkTerm(Kind kind, Term child1, Term child2) 267 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 268 * mkTerm(Kind kind, const std::vector<Term>& children) 269 */ 270 APPLY_UF, 271 #if 0 272 /* Boolean term variable */ 273 BOOLEAN_TERM_VARIABLE, 274 #endif 275 /** 276 * Cardinality constraint on sort S. 277 * Parameters: 2 278 * -[1]: Term of sort S 279 * -[2]: Positive integer constant that bounds the cardinality of sort S 280 * Create with: 281 * mkTerm(Kind kind, Term child1, Term child2) 282 * mkTerm(Kind kind, const std::vector<Term>& children) 283 */ 284 CARDINALITY_CONSTRAINT, 285 #if 0 286 /* Combined cardinality constraint. */ 287 COMBINED_CARDINALITY_CONSTRAINT, 288 /* Partial uninterpreted function application. */ 289 PARTIAL_APPLY_UF, 290 /* cardinality value of sort S: 291 * first parameter is (any) term of sort S */ 292 CARDINALITY_VALUE, 293 #endif 294 /** 295 * Higher-order applicative encoding of function application. 296 * Parameters: 2 297 * -[1]: Function to apply 298 * -[2]: Argument of the function 299 * Create with: 300 * mkTerm(Kind kind, Term child1, Term child2) 301 * mkTerm(Kind kind, const std::vector<Term>& children) 302 */ 303 HO_APPLY, 304 305 /* Arithmetic ------------------------------------------------------------ */ 306 307 /** 308 * Arithmetic addition. 309 * Parameters: n > 1 310 * -[1]..[n]: Terms of sort Integer, Real (sorts must match) 311 * Create with: 312 * mkTerm(Kind kind, Term child1, Term child2) 313 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 314 * mkTerm(Kind kind, const std::vector<Term>& children) 315 */ 316 PLUS, 317 /** 318 * Arithmetic multiplication. 319 * Parameters: n > 1 320 * -[1]..[n]: Terms of sort Integer, Real (sorts must match) 321 * Create with: 322 * mkTerm(Kind kind, Term child1, Term child2) 323 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 324 * mkTerm(Kind kind, const std::vector<Term>& children) 325 */ 326 MULT, 327 #if 0 328 /* Synonym for MULT. */ 329 NONLINEAR_MULT, 330 #endif 331 /** 332 * Arithmetic subtraction. 333 * Parameters: 2 334 * -[1]..[2]: Terms of sort Integer, Real (sorts must match) 335 * Create with: 336 * mkTerm(Kind kind, Term child1, Term child2) 337 * mkTerm(Kind kind, const std::vector<Term>& children) 338 */ 339 MINUS, 340 /** 341 * Arithmetic negation. 342 * Parameters: 1 343 * -[1]: Term of sort Integer, Real 344 * Create with: 345 * mkTerm(Kind kind, Term child) 346 */ 347 UMINUS, 348 /** 349 * Real division, division by 0 undefined 350 * Parameters: 2 351 * -[1]..[2]: Terms of sort Integer, Real 352 * Create with: 353 * mkTerm(Kind kind, Term child1, Term child2) 354 * mkTerm(Kind kind, const std::vector<Term>& children) 355 */ 356 DIVISION, 357 /** 358 * Real division with interpreted division by 0 359 * Parameters: 2 360 * -[1]..[2]: Terms of sort Integer, Real 361 * Create with: 362 * mkTerm(Kind kind, Term child1, Term child2) 363 * mkTerm(Kind kind, const std::vector<Term>& children) 364 */ 365 DIVISION_TOTAL, 366 /** 367 * Integer division, division by 0 undefined. 368 * Parameters: 2 369 * -[1]..[2]: Terms of sort Integer 370 * Create with: 371 * mkTerm(Kind kind, Term child1, Term child2) 372 * mkTerm(Kind kind, const std::vector<Term>& children) 373 */ 374 INTS_DIVISION, 375 /** 376 * Integer division with interpreted division by 0. 377 * Parameters: 2 378 * -[1]..[2]: Terms of sort Integer 379 * Create with: 380 * mkTerm(Kind kind, Term child1, Term child2) 381 * mkTerm(Kind kind, const std::vector<Term>& children) 382 */ 383 INTS_DIVISION_TOTAL, 384 /** 385 * Integer modulus, division by 0 undefined. 386 * Parameters: 2 387 * -[1]..[2]: Terms of sort Integer 388 * Create with: 389 * mkTerm(Kind kind, Term child1, Term child2) 390 * mkTerm(Kind kind, const std::vector<Term>& children) 391 */ 392 INTS_MODULUS, 393 /** 394 * Integer modulus with interpreted division by 0. 395 * Parameters: 2 396 * -[1]..[2]: Terms of sort Integer 397 * Create with: 398 * mkTerm(Kind kind, Term child1, Term child2) 399 * mkTerm(Kind kind, const std::vector<Term>& children) 400 */ 401 INTS_MODULUS_TOTAL, 402 /** 403 * Absolute value. 404 * Parameters: 1 405 * -[1]: Term of sort Integer 406 * Create with: 407 * mkTerm(Kind kind, Term child) 408 */ 409 ABS, 410 /** 411 * Divisibility-by-k predicate. 412 * Parameters: 2 413 * -[1]: DIVISIBLE_OP Term 414 * -[2]: Integer Term 415 * Create with: 416 * mkTerm(Kind kind, Term child1, Term child2) 417 * mkTerm(Kind kind, const std::vector<Term>& children) 418 */ 419 DIVISIBLE, 420 /** 421 * Arithmetic power. 422 * Parameters: 2 423 * -[1]..[2]: Terms of sort Integer, Real 424 * Create with: 425 * mkTerm(Kind kind, Term child1, Term child2) 426 * mkTerm(Kind kind, const std::vector<Term>& children) 427 */ 428 POW, 429 /** 430 * Exponential. 431 * Parameters: 1 432 * -[1]: Term of sort Integer, Real 433 * Create with: 434 * mkTerm(Kind kind, Term child) 435 */ 436 EXPONENTIAL, 437 /** 438 * Sine. 439 * Parameters: 1 440 * -[1]: Term of sort Integer, Real 441 * Create with: 442 * mkTerm(Kind kind, Term child) 443 */ 444 SINE, 445 /** 446 * Cosine. 447 * Parameters: 1 448 * -[1]: Term of sort Integer, Real 449 * Create with: 450 * mkTerm(Kind kind, Term child) 451 */ 452 COSINE, 453 /** 454 * Tangent. 455 * Parameters: 1 456 * -[1]: Term of sort Integer, Real 457 * Create with: 458 * mkTerm(Kind kind, Term child) 459 */ 460 TANGENT, 461 /** 462 * Cosecant. 463 * Parameters: 1 464 * -[1]: Term of sort Integer, Real 465 * Create with: 466 * mkTerm(Kind kind, Term child) 467 */ 468 COSECANT, 469 /** 470 * Secant. 471 * Parameters: 1 472 * -[1]: Term of sort Integer, Real 473 * Create with: 474 * mkTerm(Kind kind, Term child) 475 */ 476 SECANT, 477 /** 478 * Cotangent. 479 * Parameters: 1 480 * -[1]: Term of sort Integer, Real 481 * Create with: 482 * mkTerm(Kind kind, Term child) 483 */ 484 COTANGENT, 485 /** 486 * Arc sine. 487 * Parameters: 1 488 * -[1]: Term of sort Integer, Real 489 * Create with: 490 * mkTerm(Kind kind, Term child) 491 */ 492 ARCSINE, 493 /** 494 * Arc cosine. 495 * Parameters: 1 496 * -[1]: Term of sort Integer, Real 497 * Create with: 498 * mkTerm(Kind kind, Term child) 499 */ 500 ARCCOSINE, 501 /** 502 * Arc tangent. 503 * Parameters: 1 504 * -[1]: Term of sort Integer, Real 505 * Create with: 506 * mkTerm(Kind kind, Term child) 507 */ 508 ARCTANGENT, 509 /** 510 * Arc cosecant. 511 * Parameters: 1 512 * -[1]: Term of sort Integer, Real 513 * Create with: 514 * mkTerm(Kind kind, Term child) 515 */ 516 ARCCOSECANT, 517 /** 518 * Arc secant. 519 * Parameters: 1 520 * -[1]: Term of sort Integer, Real 521 * Create with: 522 * mkTerm(Kind kind, Term child) 523 */ 524 ARCSECANT, 525 /** 526 * Arc cotangent. 527 * Parameters: 1 528 * -[1]: Term of sort Integer, Real 529 * Create with: 530 * mkTerm(Kind kind, Term child) 531 */ 532 ARCCOTANGENT, 533 /** 534 * Square root. 535 * Parameters: 1 536 * -[1]: Term of sort Integer, Real 537 * Create with: 538 * mkTerm(Kind kind, Term child) 539 */ 540 SQRT, 541 /** 542 * Operator for the divisibility-by-k predicate. 543 * Parameter: 1 544 * -[1]: The k to divide by (sort Integer) 545 * Create with: 546 * mkOpTerm(Kind kind, uint32_t param) 547 */ 548 DIVISIBLE_OP, 549 /** 550 * Multiple-precision rational constant. 551 * Parameters: 552 * See mkInteger(), mkReal(), mkRational() 553 * Create with: 554 * mkInteger(const char* s, uint32_t base = 10) 555 * mkInteger(const std::string& s, uint32_t base = 10) 556 * mkInteger(int32_t val) 557 * mkInteger(uint32_t val) 558 * mkInteger(int64_t val) 559 * mkInteger(uint64_t val) 560 * mkReal(const char* s, uint32_t base = 10) 561 * mkReal(const std::string& s, uint32_t base = 10) 562 * mkReal(int32_t val) 563 * mkReal(int64_t val) 564 * mkReal(uint32_t val) 565 * mkReal(uint64_t val) 566 * mkReal(int32_t num, int32_t den) 567 * mkReal(int64_t num, int64_t den) 568 * mkReal(uint32_t num, uint32_t den) 569 * mkReal(uint64_t num, uint64_t den) 570 */ 571 CONST_RATIONAL, 572 /** 573 * Less than. 574 * Parameters: 2 575 * -[1]..[2]: Terms of sort Integer, Real; [1] < [2] 576 * Create with: 577 * mkTerm(Kind kind, Term child1, Term child2) 578 * mkTerm(Kind kind, const std::vector<Term>& children) 579 */ 580 LT, 581 /** 582 * Less than or equal. 583 * Parameters: 2 584 * -[1]..[2]: Terms of sort Integer, Real; [1] <= [2] 585 * Create with: 586 * mkTerm(Kind kind, Term child1, Term child2) 587 * mkTerm(Kind kind, const std::vector<Term>& children) 588 */ 589 LEQ, 590 /** 591 * Greater than. 592 * Parameters: 2 593 * -[1]..[2]: Terms of sort Integer, Real, [1] > [2] 594 * Create with: 595 * mkTerm(Kind kind, Term child1, Term child2) 596 * mkTerm(Kind kind, const std::vector<Term>& children) 597 */ 598 GT, 599 /** 600 * Greater than or equal. 601 * Parameters: 2 602 * -[1]..[2]: Terms of sort Integer, Real; [1] >= [2] 603 * Create with: 604 * mkTerm(Kind kind, Term child1, Term child2) 605 * mkTerm(Kind kind, const std::vector<Term>& children) 606 */ 607 GEQ, 608 /** 609 * Is-integer predicate. 610 * Parameters: 1 611 * -[1]: Term of sort Integer, Real 612 * Create with: 613 * mkTerm(Kind kind, Term child) 614 */ 615 IS_INTEGER, 616 /** 617 * Convert Term to Integer by the floor function. 618 * Parameters: 1 619 * -[1]: Term of sort Integer, Real 620 * Create with: 621 * mkTerm(Kind kind, Term child) 622 */ 623 TO_INTEGER, 624 /** 625 * Convert Term to Real. 626 * Parameters: 1 627 * -[1]: Term of sort Integer, Real 628 * This is a no-op in CVC4, as Integer is a subtype of Real. 629 */ 630 TO_REAL, 631 /** 632 * Pi constant. 633 * Create with: 634 * mkPi() 635 * mkTerm(Kind kind) 636 */ 637 PI, 638 639 /* BV -------------------------------------------------------------------- */ 640 641 /** 642 * Fixed-size bit-vector constant. 643 * Parameters: 644 * See mkBitVector(). 645 * Create with: 646 * mkBitVector(uint32_t size, uint64_t val) 647 * mkBitVector(const char* s, uint32_t base = 2) 648 * mkBitVector(std::string& s, uint32_t base = 2) 649 */ 650 CONST_BITVECTOR, 651 /** 652 * Concatenation of two or more bit-vectors. 653 * Parameters: n > 1 654 * -[1]..[n]: Terms of bit-vector sort 655 * Create with: 656 * mkTerm(Kind kind, Term child1, Term child2) 657 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 658 * mkTerm(Kind kind, const std::vector<Term>& children) 659 */ 660 BITVECTOR_CONCAT, 661 /** 662 * Bit-wise and. 663 * Parameters: n > 1 664 * -[1]..[n]: Terms of bit-vector sort (sorts must match) 665 * Create with: 666 * mkTerm(Kind kind, Term child1, Term child2) 667 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 668 * mkTerm(Kind kind, const std::vector<Term>& children) 669 */ 670 BITVECTOR_AND, 671 /** 672 * Bit-wise or. 673 * Parameters: n > 1 674 * -[1]..[n]: Terms of bit-vector sort (sorts must match) 675 * Create with: 676 * mkTerm(Kind kind, Term child1, Term child2) 677 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 678 * mkTerm(Kind kind, const std::vector<Term>& children) 679 */ 680 BITVECTOR_OR, 681 /** 682 * Bit-wise xor. 683 * Parameters: n > 1 684 * -[1]..[n]: Terms of bit-vector sort (sorts must match) 685 * Create with: 686 * mkTerm(Kind kind, Term child1, Term child2) 687 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 688 * mkTerm(Kind kind, const std::vector<Term>& children) 689 */ 690 BITVECTOR_XOR, 691 /** 692 * Bit-wise negation. 693 * Parameters: 1 694 * -[1]: Term of bit-vector sort 695 * Create with: 696 * mkTerm(Kind kind, Term child) 697 */ 698 BITVECTOR_NOT, 699 /** 700 * Bit-wise nand. 701 * Parameters: 2 702 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 703 * Create with: 704 * mkTerm(Kind kind, Term child1, Term child2) 705 * mkTerm(Kind kind, const std::vector<Term>& children) 706 */ 707 BITVECTOR_NAND, 708 /** 709 * Bit-wise nor. 710 * Parameters: 2 711 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 712 * Create with: 713 * mkTerm(Kind kind, Term child1, Term child2) 714 * mkTerm(Kind kind, const std::vector<Term>& children) 715 */ 716 BITVECTOR_NOR, 717 /** 718 * Bit-wise xnor. 719 * Parameters: 2 720 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 721 * Create with: 722 * mkTerm(Kind kind, Term child1, Term child2) 723 * mkTerm(Kind kind, const std::vector<Term>& children) 724 */ 725 BITVECTOR_XNOR, 726 /** 727 * Equality comparison (returns bit-vector of size 1). 728 * Parameters: 2 729 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 730 * Create with: 731 * mkTerm(Kind kind, Term child1, Term child2) 732 * mkTerm(Kind kind, const std::vector<Term>& children) 733 */ 734 BITVECTOR_COMP, 735 /** 736 * Multiplication of two or more bit-vectors. 737 * Parameters: n > 1 738 * -[1]..[n]: Terms of bit-vector sort (sorts must match) 739 * Create with: 740 * mkTerm(Kind kind, Term child1, Term child2) 741 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 742 * mkTerm(Kind kind, const std::vector<Term>& children) 743 */ 744 BITVECTOR_MULT, 745 /** 746 * Addition of two or more bit-vectors. 747 * Parameters: n > 1 748 * -[1]..[n]: Terms of bit-vector sort (sorts must match) 749 * Create with: 750 * mkTerm(Kind kind, Term child1, Term child2) 751 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 752 * mkTerm(Kind kind, const std::vector<Term>& children) 753 */ 754 BITVECTOR_PLUS, 755 /** 756 * Subtraction of two bit-vectors. 757 * Parameters: 2 758 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 759 * Create with: 760 * mkTerm(Kind kind, Term child1, Term child2) 761 * mkTerm(Kind kind, const std::vector<Term>& children) 762 */ 763 BITVECTOR_SUB, 764 /** 765 * Negation of a bit-vector (two's complement). 766 * Parameters: 1 767 * -[1]: Term of bit-vector sort 768 * Create with: 769 * mkTerm(Kind kind, Term child) 770 */ 771 BITVECTOR_NEG, 772 /** 773 * Unsigned division of two bit-vectors, truncating towards 0. 774 * Parameters: 2 775 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 776 * Create with: 777 * mkTerm(Kind kind, Term child1, Term child2) 778 * mkTerm(Kind kind, const std::vector<Term>& children) 779 */ 780 BITVECTOR_UDIV, 781 /** 782 * Unsigned remainder from truncating division of two bit-vectors. 783 * Parameters: 2 784 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 785 * Create with: 786 * mkTerm(Kind kind, Term child1, Term child2) 787 * mkTerm(Kind kind, const std::vector<Term>& children) 788 */ 789 BITVECTOR_UREM, 790 /** 791 * Two's complement signed division of two bit-vectors. 792 * Parameters: 2 793 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 794 * Create with: 795 * mkTerm(Kind kind, Term child1, Term child2) 796 * mkTerm(Kind kind, const std::vector<Term>& children) 797 */ 798 BITVECTOR_SDIV, 799 /** 800 * Two's complement signed remainder of two bit-vectors 801 * (sign follows dividend). 802 * Parameters: 2 803 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 804 * Create with: 805 * mkTerm(Kind kind, Term child1, Term child2) 806 * mkTerm(Kind kind, const std::vector<Term>& children) 807 */ 808 BITVECTOR_SREM, 809 /** 810 * Two's complement signed remainder 811 * (sign follows divisor). 812 * Parameters: 2 813 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 814 * Create with: 815 * mkTerm(Kind kind, Term child1, Term child2) 816 * mkTerm(Kind kind, const std::vector<Term>& children) 817 */ 818 BITVECTOR_SMOD, 819 /** 820 * Unsigned division of two bit-vectors, truncating towards 0 821 * (defined to be the all-ones bit pattern, if divisor is 0). 822 * Parameters: 2 823 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 824 * Create with: 825 * mkTerm(Kind kind, Term child1, Term child2) 826 * mkTerm(Kind kind, const std::vector<Term>& children) 827 */ 828 BITVECTOR_UDIV_TOTAL, 829 /** 830 * Unsigned remainder from truncating division of two bit-vectors 831 * (defined to be equal to the dividend, if divisor is 0). 832 * Parameters: 2 833 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 834 * Create with: 835 * mkTerm(Kind kind, Term child1, Term child2) 836 * mkTerm(Kind kind, const std::vector<Term>& children) 837 */ 838 BITVECTOR_UREM_TOTAL, 839 /** 840 * Bit-vector shift left. 841 * The two bit-vector parameters must have same width. 842 * Parameters: 2 843 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 844 * Create with: 845 * mkTerm(Kind kind, Term child1, Term child2) 846 * mkTerm(Kind kind, const std::vector<Term>& children) 847 */ 848 BITVECTOR_SHL, 849 /** 850 * Bit-vector logical shift right. 851 * The two bit-vector parameters must have same width. 852 * Parameters: 2 853 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 854 * Create with: 855 * mkTerm(Kind kind, Term child1, Term child2) 856 * mkTerm(Kind kind, const std::vector<Term>& children) 857 */ 858 BITVECTOR_LSHR, 859 /** 860 * Bit-vector arithmetic shift right. 861 * The two bit-vector parameters must have same width. 862 * Parameters: 2 863 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 864 * Create with: 865 * mkTerm(Kind kind, Term child1, Term child2) 866 * mkTerm(Kind kind, const std::vector<Term>& children) 867 */ 868 BITVECTOR_ASHR, 869 /** 870 * Bit-vector unsigned less than. 871 * The two bit-vector parameters must have same width. 872 * Parameters: 2 873 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 874 * Create with: 875 * mkTerm(Kind kind, Term child1, Term child2) 876 * mkTerm(Kind kind, const std::vector<Term>& children) 877 */ 878 BITVECTOR_ULT, 879 /** 880 * Bit-vector unsigned less than or equal. 881 * The two bit-vector parameters must have same width. 882 * Parameters: 2 883 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 884 * Create with: 885 * mkTerm(Kind kind, Term child1, Term child2) 886 * mkTerm(Kind kind, const std::vector<Term>& children) 887 */ 888 BITVECTOR_ULE, 889 /** 890 * Bit-vector unsigned greater than. 891 * The two bit-vector parameters must have same width. 892 * Parameters: 2 893 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 894 * Create with: 895 * mkTerm(Kind kind, Term child1, Term child2) 896 * mkTerm(Kind kind, const std::vector<Term>& children) 897 */ 898 BITVECTOR_UGT, 899 /** 900 * Bit-vector unsigned greater than or equal. 901 * The two bit-vector parameters must have same width. 902 * Parameters: 2 903 * Create with: 904 * mkTerm(Kind kind, Term child1, Term child2) 905 * mkTerm(Kind kind, const std::vector<Term>& children) 906 */ 907 BITVECTOR_UGE, 908 /* Bit-vector signed less than. 909 * The two bit-vector parameters must have same width. 910 * Parameters: 2 911 * Create with: 912 * mkTerm(Kind kind, Term child1, Term child2) 913 * mkTerm(Kind kind, const std::vector<Term>& children) 914 */ 915 BITVECTOR_SLT, 916 /** 917 * Bit-vector signed less than or equal. 918 * The two bit-vector parameters must have same width. 919 * Parameters: 2 920 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 921 * Create with: 922 * mkTerm(Kind kind, Term child1, Term child2) 923 * mkTerm(Kind kind, const std::vector<Term>& children) 924 */ 925 BITVECTOR_SLE, 926 /** 927 * Bit-vector signed greater than. 928 * The two bit-vector parameters must have same width. 929 * Parameters: 2 930 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 931 * Create with: 932 * mkTerm(Kind kind, Term child1, Term child2) 933 * mkTerm(Kind kind, const std::vector<Term>& children) 934 */ 935 BITVECTOR_SGT, 936 /** 937 * Bit-vector signed greater than or equal. 938 * The two bit-vector parameters must have same width. 939 * Parameters: 2 940 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 941 * Create with: 942 * mkTerm(Kind kind, Term child1, Term child2) 943 * mkTerm(Kind kind, const std::vector<Term>& children) 944 */ 945 BITVECTOR_SGE, 946 /** 947 * Bit-vector unsigned less than, returns bit-vector of size 1. 948 * Parameters: 2 949 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 950 * Create with: 951 * mkTerm(Kind kind, Term child1, Term child2) 952 * mkTerm(Kind kind, const std::vector<Term>& children) 953 */ 954 BITVECTOR_ULTBV, 955 /** 956 * Bit-vector signed less than. returns bit-vector of size 1. 957 * Parameters: 2 958 * -[1]..[2]: Terms of bit-vector sort (sorts must match) 959 * Create with: 960 * mkTerm(Kind kind, Term child1, Term child2) 961 * mkTerm(Kind kind, const std::vector<Term>& children) 962 */ 963 BITVECTOR_SLTBV, 964 /** 965 * Same semantics as regular ITE, but condition is bit-vector of size 1. 966 * Parameters: 3 967 * -[1]: Term of bit-vector sort of size 1, representing the condition 968 * -[2]: Term reprsenting the 'then' branch 969 * -[3]: Term representing the 'else' branch 970 * 'then' and 'else' term must have same base sort. 971 * Create with: 972 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 973 * mkTerm(Kind kind, const std::vector<Term>& children) 974 */ 975 BITVECTOR_ITE, 976 /** 977 * Bit-vector redor. 978 * Parameters: 1 979 * -[1]: Term of bit-vector sort 980 * Create with: 981 * mkTerm(Kind kind, Term child) 982 */ 983 BITVECTOR_REDOR, 984 /** 985 * Bit-vector redand. 986 * Parameters: 1 987 * -[1]: Term of bit-vector sort 988 * Create with: 989 * mkTerm(Kind kind, Term child) 990 */ 991 BITVECTOR_REDAND, 992 #if 0 993 /* formula to be treated as a bv atom via eager bit-blasting 994 * (internal-only symbol) */ 995 BITVECTOR_EAGER_ATOM, 996 /* term to be treated as a variable. used for eager bit-blasting Ackermann 997 * expansion of bvudiv (internal-only symbol) */ 998 BITVECTOR_ACKERMANIZE_UDIV, 999 /* term to be treated as a variable. used for eager bit-blasting Ackermann 1000 * expansion of bvurem (internal-only symbol) */ 1001 BITVECTOR_ACKERMANIZE_UREM, 1002 /* operator for the bit-vector boolean bit extract. 1003 * One parameter, parameter is the index of the bit to extract */ 1004 BITVECTOR_BITOF_OP, 1005 #endif 1006 /** 1007 * Operator for bit-vector extract (from index 'high' to 'low'). 1008 * Parameters: 2 1009 * -[1]: The 'high' index 1010 * -[2]: The 'low' index 1011 * Create with: 1012 * mkOpTerm(Kind kind, uint32_t param, uint32_t param) 1013 */ 1014 BITVECTOR_EXTRACT_OP, 1015 /** 1016 * Operator for bit-vector repeat. 1017 * Parameter 1: 1018 * -[1]: Number of times to repeat a given bit-vector 1019 * Create with: 1020 * mkOpTerm(Kind kind, uint32_t param). 1021 */ 1022 BITVECTOR_REPEAT_OP, 1023 /** 1024 * Operator for bit-vector zero-extend. 1025 * Parameter 1: 1026 * -[1]: Number of bits by which a given bit-vector is to be extended 1027 * Create with: 1028 * mkOpTerm(Kind kind, uint32_t param). 1029 */ 1030 BITVECTOR_ZERO_EXTEND_OP, 1031 /** 1032 * Operator for bit-vector sign-extend. 1033 * Parameter 1: 1034 * -[1]: Number of bits by which a given bit-vector is to be extended 1035 * Create with: 1036 * mkOpTerm(Kind kind, uint32_t param). 1037 */ 1038 BITVECTOR_SIGN_EXTEND_OP, 1039 /** 1040 * Operator for bit-vector rotate left. 1041 * Parameter 1: 1042 * -[1]: Number of bits by which a given bit-vector is to be rotated 1043 * Create with: 1044 * mkOpTerm(Kind kind, uint32_t param). 1045 */ 1046 BITVECTOR_ROTATE_LEFT_OP, 1047 /** 1048 * Operator for bit-vector rotate right. 1049 * Parameter 1: 1050 * -[1]: Number of bits by which a given bit-vector is to be rotated 1051 * Create with: 1052 * mkOpTerm(Kind kind, uint32_t param). 1053 */ 1054 BITVECTOR_ROTATE_RIGHT_OP, 1055 #if 0 1056 /* bit-vector boolean bit extract. 1057 * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */ 1058 BITVECTOR_BITOF, 1059 #endif 1060 /* Bit-vector extract. 1061 * Parameters: 2 1062 * -[1]: BITVECTOR_EXTRACT_OP Term 1063 * -[2]: Term of bit-vector sort 1064 * Create with: 1065 * mkTerm(Term opTerm, Term child) 1066 * mkTerm(Term opTerm, const std::vector<Term>& children) 1067 */ 1068 BITVECTOR_EXTRACT, 1069 /* Bit-vector repeat. 1070 * Parameters: 2 1071 * -[1]: BITVECTOR_REPEAT_OP Term 1072 * -[2]: Term of bit-vector sort 1073 * Create with: 1074 * mkTerm(Term opTerm, Term child) 1075 * mkTerm(Term opTerm, const std::vector<Term>& children) 1076 */ 1077 BITVECTOR_REPEAT, 1078 /* Bit-vector zero-extend. 1079 * Parameters: 2 1080 * -[1]: BITVECTOR_ZERO_EXTEND_OP Term 1081 * -[2]: Term of bit-vector sort 1082 * Create with: 1083 * mkTerm(Term opTerm, Term child) 1084 * mkTerm(Term opTerm, const std::vector<Term>& children) 1085 */ 1086 BITVECTOR_ZERO_EXTEND, 1087 /* Bit-vector sign-extend. 1088 * Parameters: 2 1089 * -[1]: BITVECTOR_SIGN_EXTEND_OP Term 1090 * -[2]: Term of bit-vector sort 1091 * Create with: 1092 * mkTerm(Term opTerm, Term child) 1093 * mkTerm(Term opTerm, const std::vector<Term>& children) 1094 */ 1095 BITVECTOR_SIGN_EXTEND, 1096 /* Bit-vector rotate left. 1097 * Parameters: 2 1098 * -[1]: BITVECTOR_ROTATE_LEFT_OP Term 1099 * -[2]: Term of bit-vector sort 1100 * Create with: 1101 * mkTerm(Term opTerm, Term child) 1102 * mkTerm(Term opTerm, const std::vector<Term>& children) 1103 */ 1104 BITVECTOR_ROTATE_LEFT, 1105 /** 1106 * Bit-vector rotate right. 1107 * Parameters: 2 1108 * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term 1109 * -[2]: Term of bit-vector sort 1110 * Create with: 1111 * mkTerm(Term opTerm, Term child) 1112 * mkTerm(Term opTerm, const std::vector<Term>& children) 1113 */ 1114 BITVECTOR_ROTATE_RIGHT, 1115 /** 1116 * Operator for the conversion from Integer to bit-vector. 1117 * Parameter: 1 1118 * -[1]: Size of the bit-vector to convert to 1119 * Create with: 1120 * mkOpTerm(Kind kind, uint32_t param). 1121 */ 1122 INT_TO_BITVECTOR_OP, 1123 /** 1124 * Integer conversion to bit-vector. 1125 * Parameters: 2 1126 * -[1]: INT_TO_BITVECTOR_OP Term 1127 * -[2]: Integer term 1128 * Create with: 1129 * mkTerm(Kind kind, Term child1, Term child2) 1130 * mkTerm(Kind kind, const std::vector<Term>& children) 1131 */ 1132 INT_TO_BITVECTOR, 1133 /** 1134 * Bit-vector conversion to (nonnegative) integer. 1135 * Parameter: 1 1136 * -[1]: Term of bit-vector sort 1137 * Create with: 1138 * mkTerm(Kind kind, Term child) 1139 */ 1140 BITVECTOR_TO_NAT, 1141 1142 /* FP -------------------------------------------------------------------- */ 1143 1144 /** 1145 * Floating-point constant, constructed from a double or string. 1146 * Parameters: 3 1147 * -[1]: Size of the exponent 1148 * -[2]: Size of the significand 1149 * -[3]: Value of the floating-point constant as a bit-vector term 1150 * Create with: 1151 * mkFloatingPoint(uint32_t sig, uint32_t exp, Term val) 1152 */ 1153 CONST_FLOATINGPOINT, 1154 /** 1155 * Floating-point rounding mode term. 1156 * Create with: 1157 * mkRoundingMode(RoundingMode rm) 1158 */ 1159 CONST_ROUNDINGMODE, 1160 /** 1161 * Create floating-point literal from bit-vector triple. 1162 * Parameters: 3 1163 * -[1]: Sign bit as a bit-vector term 1164 * -[2]: Exponent bits as a bit-vector term 1165 * -[3]: Significand bits as a bit-vector term (without hidden bit) 1166 * Create with: 1167 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1168 * mkTerm(Kind kind, const std::vector<Term>& children) 1169 */ 1170 FLOATINGPOINT_FP, 1171 /** 1172 * Floating-point equality. 1173 * Parameters: 2 1174 * -[1]..[2]: Terms of floating point sort 1175 * Create with: 1176 * mkTerm(Kind kind, Term child1, Term child2) 1177 * mkTerm(Kind kind, const std::vector<Term>& children) 1178 */ 1179 FLOATINGPOINT_EQ, 1180 /** 1181 * Floating-point absolute value. 1182 * Parameters: 1 1183 * -[1]: Term of floating point sort 1184 * Create with: 1185 * mkTerm(Kind kind, Term child) 1186 */ 1187 FLOATINGPOINT_ABS, 1188 /** 1189 * Floating-point negation. 1190 * Parameters: 1 1191 * -[1]: Term of floating point sort 1192 * Create with: 1193 * mkTerm(Kind kind, Term child) 1194 */ 1195 FLOATINGPOINT_NEG, 1196 /** 1197 * Floating-point addition. 1198 * Parameters: 3 1199 * -[1]: CONST_ROUNDINGMODE 1200 * -[2]: Term of sort FloatingPoint 1201 * -[3]: Term of sort FloatingPoint 1202 * Create with: 1203 * mkTerm(Kind kind, Term child1, Term child2, child3) 1204 * mkTerm(Kind kind, const std::vector<Term>& children) 1205 */ 1206 FLOATINGPOINT_PLUS, 1207 /** 1208 * Floating-point sutraction. 1209 * Parameters: 3 1210 * -[1]: CONST_ROUNDINGMODE 1211 * -[2]: Term of sort FloatingPoint 1212 * -[3]: Term of sort FloatingPoint 1213 * Create with: 1214 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1215 * mkTerm(Kind kind, const std::vector<Term>& children) 1216 */ 1217 FLOATINGPOINT_SUB, 1218 /** 1219 * Floating-point multiply. 1220 * Parameters: 3 1221 * -[1]: CONST_ROUNDINGMODE 1222 * -[2]: Term of sort FloatingPoint 1223 * -[3]: Term of sort FloatingPoint 1224 * Create with: 1225 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1226 * mkTerm(Kind kind, const std::vector<Term>& children) 1227 */ 1228 FLOATINGPOINT_MULT, 1229 /** 1230 * Floating-point division. 1231 * Parameters: 3 1232 * -[1]: CONST_ROUNDINGMODE 1233 * -[2]: Term of sort FloatingPoint 1234 * -[3]: Term of sort FloatingPoint 1235 * Create with: 1236 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1237 * mkTerm(Kind kind, const std::vector<Term>& children) 1238 */ 1239 FLOATINGPOINT_DIV, 1240 /** 1241 * Floating-point fused multiply and add. 1242 * Parameters: 4 1243 * -[1]: CONST_ROUNDINGMODE 1244 * -[2]: Term of sort FloatingPoint 1245 * -[3]: Term of sort FloatingPoint 1246 * -[4]: Term of sort FloatingPoint 1247 * Create with: 1248 * mkTerm(Kind kind, const std::vector<Term>& children) 1249 */ 1250 FLOATINGPOINT_FMA, 1251 /** 1252 * Floating-point square root. 1253 * Parameters: 2 1254 * -[1]: CONST_ROUNDINGMODE 1255 * -[2]: Term of sort FloatingPoint 1256 * Create with: 1257 * mkTerm(Kind kind, Term child1, Term child2) 1258 * mkTerm(Kind kind, const std::vector<Term>& children) 1259 */ 1260 FLOATINGPOINT_SQRT, 1261 /** 1262 * Floating-point remainder. 1263 * Parameters: 2 1264 * -[1]..[2]: Terms of floating point sort 1265 * Create with: 1266 * mkTerm(Kind kind, Term child1, Term child2) 1267 * mkTerm(Kind kind, const std::vector<Term>& children) 1268 */ 1269 FLOATINGPOINT_REM, 1270 /** 1271 * Floating-point round to integral. 1272 * Parameters: 2 1273 * -[1]..[2]: Terms of floating point sort 1274 * Create with: 1275 * mkTerm(Kind kind, Term child1, Term child2) 1276 * mkTerm(Kind kind, const std::vector<Term>& children) 1277 */ 1278 FLOATINGPOINT_RTI, 1279 /** 1280 * Floating-point minimum. 1281 * Parameters: 2 1282 * -[1]..[2]: Terms of floating point sort 1283 * Create with: 1284 * mkTerm(Kind kind, Term child1, Term child2) 1285 * mkTerm(Kind kind, const std::vector<Term>& children) 1286 */ 1287 FLOATINGPOINT_MIN, 1288 /** 1289 * Floating-point maximum. 1290 * Parameters: 2 1291 * -[1]..[2]: Terms of floating point sort 1292 * Create with: 1293 * mkTerm(Kind kind, Term child1, Term child2) 1294 * mkTerm(Kind kind, const std::vector<Term>& children) 1295 */ 1296 FLOATINGPOINT_MAX, 1297 #if 0 1298 /* floating-point minimum (defined for all inputs) */ 1299 FLOATINGPOINT_MIN_TOTAL, 1300 /* floating-point maximum (defined for all inputs) */ 1301 FLOATINGPOINT_MAX_TOTAL, 1302 #endif 1303 /** 1304 * Floating-point less than or equal. 1305 * Parameters: 2 1306 * -[1]..[2]: Terms of floating point sort 1307 * Create with: 1308 * mkTerm(Kind kind, Term child1, Term child2) 1309 * mkTerm(Kind kind, const std::vector<Term>& children) 1310 */ 1311 FLOATINGPOINT_LEQ, 1312 /** 1313 * Floating-point less than. 1314 * Parameters: 2 1315 * -[1]..[2]: Terms of floating point sort 1316 * Create with: 1317 * mkTerm(Kind kind, Term child1, Term child2) 1318 * mkTerm(Kind kind, const std::vector<Term>& children) 1319 */ 1320 FLOATINGPOINT_LT, 1321 /** 1322 * Floating-point greater than or equal. 1323 * Parameters: 2 1324 * -[1]..[2]: Terms of floating point sort 1325 * Create with: 1326 * mkTerm(Kind kind, Term child1, Term child2) 1327 * mkTerm(Kind kind, const std::vector<Term>& children) 1328 */ 1329 FLOATINGPOINT_GEQ, 1330 /** 1331 * Floating-point greater than. 1332 * Parameters: 2 1333 * Create with: 1334 * mkTerm(Kind kind, Term child1, Term child2) 1335 * mkTerm(Kind kind, const std::vector<Term>& children) 1336 */ 1337 FLOATINGPOINT_GT, 1338 /** 1339 * Floating-point is normal. 1340 * Parameters: 1 1341 * -[1]: Term of floating point sort 1342 * Create with: 1343 * mkTerm(Kind kind, Term child) 1344 */ 1345 FLOATINGPOINT_ISN, 1346 /** 1347 * Floating-point is sub-normal. 1348 * Parameters: 1 1349 * -[1]: Term of floating point sort 1350 * Create with: 1351 * mkTerm(Kind kind, Term child) 1352 */ 1353 FLOATINGPOINT_ISSN, 1354 /** 1355 * Floating-point is zero. 1356 * Parameters: 1 1357 * -[1]: Term of floating point sort 1358 * Create with: 1359 * mkTerm(Kind kind, Term child) 1360 */ 1361 FLOATINGPOINT_ISZ, 1362 /** 1363 * Floating-point is infinite. 1364 * Parameters: 1 1365 * -[1]: Term of floating point sort 1366 * Create with: 1367 * mkTerm(Kind kind, Term child) 1368 */ 1369 FLOATINGPOINT_ISINF, 1370 /** 1371 * Floating-point is NaN. 1372 * Parameters: 1 1373 * -[1]: Term of floating point sort 1374 * Create with: 1375 * mkTerm(Kind kind, Term child) 1376 */ 1377 FLOATINGPOINT_ISNAN, 1378 /** 1379 * Floating-point is negative. 1380 * Parameters: 1 1381 * -[1]: Term of floating point sort 1382 * Create with: 1383 * mkTerm(Kind kind, Term child) 1384 */ 1385 FLOATINGPOINT_ISNEG, 1386 /** 1387 * Floating-point is positive. 1388 * Parameters: 1 1389 * -[1]: Term of floating point sort 1390 * Create with: 1391 * mkTerm(Kind kind, Term child) 1392 */ 1393 FLOATINGPOINT_ISPOS, 1394 /** 1395 * Operator for to_fp from bit vector. 1396 * Parameters: 2 1397 * -[1]: Exponent size 1398 * -[2]: Significand size 1399 * Create with: 1400 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1401 */ 1402 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 1403 /** 1404 * Conversion from an IEEE-754 bit vector to floating-point. 1405 * Parameters: 2 1406 * -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term 1407 * -[2]: Term of sort FloatingPoint 1408 * Create with: 1409 * mkTerm(Term opTerm, Term child) 1410 * mkTerm(Term opTerm, const std::vector<Term>& children) 1411 */ 1412 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 1413 /** 1414 * Operator for to_fp from floating point. 1415 * Parameters: 2 1416 * -[1]: Exponent size 1417 * -[2]: Significand size 1418 * Create with: 1419 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1420 */ 1421 FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 1422 /** 1423 * Conversion between floating-point sorts. 1424 * Parameters: 2 1425 * -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term 1426 * -[2]: Term of sort FloatingPoint 1427 * Create with: 1428 * mkTerm(Term opTerm, Term child) 1429 * mkTerm(Term opTerm, const std::vector<Term>& children) 1430 */ 1431 FLOATINGPOINT_TO_FP_FLOATINGPOINT, 1432 /** 1433 * Operator for to_fp from real. 1434 * Parameters: 2 1435 * -[1]: Exponent size 1436 * -[2]: Significand size 1437 * Create with: 1438 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1439 */ 1440 FLOATINGPOINT_TO_FP_REAL_OP, 1441 /** 1442 * Conversion from a real to floating-point. 1443 * Parameters: 2 1444 * -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term 1445 * -[2]: Term of sort FloatingPoint 1446 * Create with: 1447 * mkTerm(Term opTerm, Term child) 1448 * mkTerm(Term opTerm, const std::vector<Term>& children) 1449 */ 1450 FLOATINGPOINT_TO_FP_REAL, 1451 /* 1452 * Operator for to_fp from signed bit vector. 1453 * Parameters: 2 1454 * -[1]: Exponent size 1455 * -[2]: Significand size 1456 * Create with: 1457 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1458 */ 1459 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 1460 /** 1461 * Conversion from a signed bit vector to floating-point. 1462 * Parameters: 2 1463 * -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term 1464 * -[2]: Term of sort FloatingPoint 1465 * Create with: 1466 * mkTerm(Term opTerm, Term child) 1467 * mkTerm(Term opTerm, const std::vector<Term>& children) 1468 */ 1469 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 1470 /** 1471 * Operator for to_fp from unsigned bit vector. 1472 * Parameters: 2 1473 * -[1]: Exponent size 1474 * -[2]: Significand size 1475 * Create with: 1476 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1477 */ 1478 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 1479 /** 1480 * Operator for converting an unsigned bit vector to floating-point. 1481 * Parameters: 2 1482 * -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term 1483 * -[2]: Term of sort FloatingPoint 1484 * Create with: 1485 * mkTerm(Term opTerm, Term child) 1486 * mkTerm(Term opTerm, const std::vector<Term>& children) 1487 */ 1488 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 1489 /** 1490 * Operator for a generic to_fp. 1491 * Parameters: 2 1492 * -[1]: exponent size 1493 * -[2]: Significand size 1494 * Create with: 1495 * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) 1496 */ 1497 FLOATINGPOINT_TO_FP_GENERIC_OP, 1498 /** 1499 * Generic conversion to floating-point, used in parsing only. 1500 * Parameters: 2 1501 * -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term 1502 * -[2]: Term of sort FloatingPoint 1503 * Create with: 1504 * mkTerm(Term opTerm, Term child) 1505 * mkTerm(Term opTerm, const std::vector<Term>& children) 1506 */ 1507 FLOATINGPOINT_TO_FP_GENERIC, 1508 /** 1509 * Operator for to_ubv. 1510 * Parameters: 1 1511 * -[1]: Size of the bit-vector to convert to 1512 * Create with: 1513 * mkOpTerm(Kind kind, uint32_t param) 1514 */ 1515 FLOATINGPOINT_TO_UBV_OP, 1516 /** 1517 * Conversion from a floating-point value to an unsigned bit vector. 1518 * Parameters: 2 1519 * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term 1520 * -[2]: Term of sort FloatingPoint 1521 * Create with: 1522 * mkTerm(Term opTerm, Term child) 1523 * mkTerm(Term opTerm, const std::vector<Term>& children) 1524 */ 1525 FLOATINGPOINT_TO_UBV, 1526 /** 1527 * Operator for to_ubv_total. 1528 * Parameters: 1 1529 * -[1]: Size of the bit-vector to convert to 1530 * Create with: 1531 * mkOpTerm(Kind kind, uint32_t param) 1532 */ 1533 FLOATINGPOINT_TO_UBV_TOTAL_OP, 1534 /** 1535 * Conversion from a floating-point value to an unsigned bit vector 1536 * (defined for all inputs). 1537 * Parameters: 2 1538 * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term 1539 * -[2]: Term of sort FloatingPoint 1540 * Create with: 1541 * mkTerm(Term opTerm, Term child) 1542 * mkTerm(Term opTerm, const std::vector<Term>& children) 1543 */ 1544 FLOATINGPOINT_TO_UBV_TOTAL, 1545 /** 1546 * Operator for to_sbv. 1547 * Parameters: 1 1548 * -[1]: Size of the bit-vector to convert to 1549 * Create with: 1550 * mkOpTerm(Kind kind, uint32_t param) 1551 */ 1552 FLOATINGPOINT_TO_SBV_OP, 1553 /** 1554 * Conversion from a floating-point value to a signed bit vector. 1555 * Parameters: 2 1556 * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term 1557 * -[2]: Term of sort FloatingPoint 1558 * Create with: 1559 * mkTerm(Term opTerm, Term child) 1560 * mkTerm(Term opTerm, const std::vector<Term>& children) 1561 */ 1562 FLOATINGPOINT_TO_SBV, 1563 /** 1564 * Operator for to_sbv_total. 1565 * Parameters: 1 1566 * -[1]: Size of the bit-vector to convert to 1567 * Create with: 1568 * mkOpTerm(Kind kind, uint32_t param) 1569 */ 1570 FLOATINGPOINT_TO_SBV_TOTAL_OP, 1571 /** 1572 * Conversion from a floating-point value to a signed bit vector 1573 * (defined for all inputs). 1574 * Parameters: 2 1575 * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term 1576 * -[2]: Term of sort FloatingPoint 1577 * Create with: 1578 * mkTerm(Term opTerm, Term child) 1579 * mkTerm(Term opTerm, const std::vector<Term>& children) 1580 */ 1581 FLOATINGPOINT_TO_SBV_TOTAL, 1582 /** 1583 * Floating-point to real. 1584 * Parameters: 1 1585 * -[1]: Term of sort FloatingPoint 1586 * Create with: 1587 * mkTerm(Kind kind, Term child) 1588 */ 1589 FLOATINGPOINT_TO_REAL, 1590 /** 1591 * Floating-point to real (defined for all inputs). 1592 * Parameters: 1 1593 * -[1]: Term of sort FloatingPoint 1594 * Create with: 1595 * mkTerm(Kind kind, Term child) 1596 */ 1597 FLOATINGPOINT_TO_REAL_TOTAL, 1598 1599 /* Arrays ---------------------------------------------------------------- */ 1600 1601 /** 1602 * Aarray select. 1603 * Parameters: 2 1604 * -[1]: Term of array sort 1605 * -[2]: Selection index 1606 * Create with: 1607 * mkTerm(Term opTerm, Term child1, Term child2) 1608 * mkTerm(Term opTerm, const std::vector<Term>& children) 1609 */ 1610 SELECT, 1611 /** 1612 * Array store. 1613 * Parameters: 3 1614 * -[1]: Term of array sort 1615 * -[2]: Store index 1616 * -[3]: Term to store at the index 1617 * Create with: 1618 * mkTerm(Term opTerm, Term child1, Term child2, Term child3) 1619 * mkTerm(Term opTerm, const std::vector<Term>& children) 1620 */ 1621 STORE, 1622 /** 1623 * Constant array. 1624 * Parameters: 2 1625 * -[1]: Array sort 1626 * -[2]: Term representing a constant 1627 * Create with: 1628 * mkTerm(Term opTerm, Term child1, Term child2) 1629 * mkTerm(Term opTerm, const std::vector<Term>& children) 1630 * 1631 * Note: We currently support the creation of constant arrays, but under some 1632 * conditions when there is a chain of equalities connecting two constant 1633 * arrays, the solver doesn't know what to do and aborts (Issue #1667). 1634 */ 1635 STORE_ALL, 1636 #if 0 1637 /* array table function (internal-only symbol) */ 1638 ARR_TABLE_FUN, 1639 /* array lambda (internal-only symbol) */ 1640 ARRAY_LAMBDA, 1641 /* partial array select, for internal use only */ 1642 PARTIAL_SELECT_0, 1643 /* partial array select, for internal use only */ 1644 PARTIAL_SELECT_1, 1645 #endif 1646 1647 /* Datatypes ------------------------------------------------------------- */ 1648 1649 /** 1650 * Constructor application. 1651 * Paramters: n > 0 1652 * -[1]: Constructor (operator term) 1653 * -[2]..[n]: Parameters to the constructor 1654 * Create with: 1655 * mkTerm(Kind kind, OpTerm opTerm) 1656 * mkTerm(Kind kind, OpTerm opTerm, Term child) 1657 * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) 1658 * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) 1659 * mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children) 1660 */ 1661 APPLY_CONSTRUCTOR, 1662 /** 1663 * Datatype selector application. 1664 * Parameters: 1 1665 * -[1]: Selector (operator term) 1666 * -[2]: Datatype term (undefined if mis-applied) 1667 * Create with: 1668 * mkTerm(Kind kind, OpTerm opTerm, Term child) 1669 */ 1670 APPLY_SELECTOR, 1671 /** 1672 * Datatype selector application. 1673 * Parameters: 1 1674 * -[1]: Selector (operator term) 1675 * -[2]: Datatype term (defined rigidly if mis-applied) 1676 * Create with: 1677 * mkTerm(Kind kind, OpTerm opTerm, Term child) 1678 */ 1679 APPLY_SELECTOR_TOTAL, 1680 /** 1681 * Datatype tester application. 1682 * Parameters: 2 1683 * -[1]: Tester term 1684 * -[2]: Datatype term 1685 * Create with: 1686 * mkTerm(Kind kind, Term child1, Term child2) 1687 * mkTerm(Kind kind, const std::vector<Term>& children) 1688 */ 1689 APPLY_TESTER, 1690 #if 0 1691 /* Parametric datatype term. */ 1692 PARAMETRIC_DATATYPE, 1693 /* type ascription, for datatype constructor applications; 1694 * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor 1695 * application being ascribed */ 1696 APPLY_TYPE_ASCRIPTION, 1697 #endif 1698 /** 1699 * Operator for a tuple update. 1700 * Parameters: 1 1701 * -[1]: Index of the tuple to be updated 1702 * Create with: 1703 * mkOpTerm(Kind kind, uint32_t param) 1704 */ 1705 TUPLE_UPDATE_OP, 1706 /** 1707 * Tuple update. 1708 * Parameters: 3 1709 * -[1]: TUPLE_UPDATE_OP (which references an index) 1710 * -[2]: Tuple 1711 * -[3]: Element to store in the tuple at the given index 1712 * Create with: 1713 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1714 * mkTerm(Kind kind, const std::vector<Term>& children) 1715 */ 1716 TUPLE_UPDATE, 1717 /** 1718 * Operator for a record update. 1719 * Parameters: 1 1720 * -[1]: Name of the field to be updated 1721 * Create with: 1722 * mkOpTerm(Kind kind, const std::string& param) 1723 */ 1724 RECORD_UPDATE_OP, 1725 /** 1726 * Record update. 1727 * Parameters: 3 1728 * -[1]: RECORD_UPDATE_OP Term (which references a field) 1729 * -[2]: Record term to update 1730 * -[3]: Element to store in the record in the given field 1731 * Create with: 1732 * mkTerm(Kind kind, Term child1, Term child2) 1733 * mkTerm(Kind kind, const std::vector<Term>& children) 1734 */ 1735 RECORD_UPDATE, 1736 #if 0 1737 /* datatypes size */ 1738 DT_SIZE, 1739 /* datatypes height bound */ 1740 DT_HEIGHT_BOUND, 1741 /* datatypes height bound */ 1742 DT_SIZE_BOUND, 1743 /* datatypes sygus bound */ 1744 DT_SYGUS_BOUND, 1745 /* datatypes sygus term order */ 1746 DT_SYGUS_TERM_ORDER, 1747 /* datatypes sygus is constant */ 1748 DT_SYGUS_IS_CONST, 1749 #endif 1750 1751 /* Separation Logic ------------------------------------------------------ */ 1752 1753 /** 1754 * Separation logic nil term. 1755 * Parameters: 0 1756 * Create with: 1757 * mkSepNil(Sort sort) 1758 */ 1759 SEP_NIL, 1760 /** 1761 * Separation logic empty heap. 1762 * Parameters: 2 1763 * -[1]: Term of the same sort as the sort of the location of the heap 1764 * that is constrained to be empty 1765 * -[2]: Term of the same sort as the data sort of the heap that is 1766 * that is constrained to be empty 1767 * Create with: 1768 * mkTerm(Kind kind, Term child1, Term child2) 1769 * mkTerm(Kind kind, const std::vector<Term>& children) 1770 */ 1771 SEP_EMP, 1772 /** 1773 * Separation logic points-to relation. 1774 * Parameters: 2 1775 * -[1]: Location of the points-to constraint 1776 * -[2]: Data of the points-to constraint 1777 * Create with: 1778 * mkTerm(Kind kind, Term child1, Term child2) 1779 * mkTerm(Kind kind, const std::vector<Term>& children) 1780 */ 1781 SEP_PTO, 1782 /** 1783 * Separation logic star. 1784 * Parameters: n >= 2 1785 * -[1]..[n]: Child constraints that hold in disjoint (separated) heaps 1786 * Create with: 1787 * mkTerm(Kind kind, Term child1, Term child2) 1788 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1789 * mkTerm(Kind kind, const std::vector<Term>& children) 1790 */ 1791 SEP_STAR, 1792 /** 1793 * Separation logic magic wand. 1794 * Parameters: 2 1795 * -[1]: Antecendant of the magic wand constraint 1796 * -[2]: Conclusion of the magic wand constraint, which is asserted to 1797 * hold in all heaps that are disjoint extensions of the antecedent. 1798 * Create with: 1799 * mkTerm(Kind kind, Term child1, Term child2) 1800 * mkTerm(Kind kind, const std::vector<Term>& children) 1801 */ 1802 SEP_WAND, 1803 #if 0 1804 /* separation label (internal use only) */ 1805 SEP_LABEL, 1806 #endif 1807 1808 /* Sets ------------------------------------------------------------------ */ 1809 1810 /** 1811 * Empty set constant. 1812 * Parameters: 1 1813 * -[1]: Sort of the set elements 1814 * Create with: 1815 * mkEmptySet(Sort sort) 1816 */ 1817 EMPTYSET, 1818 /** 1819 * Set union. 1820 * Parameters: 2 1821 * -[1]..[2]: Terms of set sort 1822 * Create with: 1823 * mkTerm(Kind kind, Term child1, Term child2) 1824 * mkTerm(Kind kind, const std::vector<Term>& children) 1825 */ 1826 UNION, 1827 /** 1828 * Set intersection. 1829 * Parameters: 2 1830 * -[1]..[2]: Terms of set sort 1831 * Create with: 1832 * mkTerm(Kind kind, Term child1, Term child2) 1833 * mkTerm(Kind kind, const std::vector<Term>& children) 1834 */ 1835 INTERSECTION, 1836 /** 1837 * Set subtraction. 1838 * Parameters: 2 1839 * -[1]..[2]: Terms of set sort 1840 * Create with: 1841 * mkTerm(Kind kind, Term child1, Term child2) 1842 * mkTerm(Kind kind, const std::vector<Term>& children) 1843 */ 1844 SETMINUS, 1845 /** 1846 * Subset predicate. 1847 * Parameters: 2 1848 * -[1]..[2]: Terms of set sort, [1] a subset of set [2]? 1849 * Create with: 1850 * mkTerm(Kind kind, Term child1, Term child2) 1851 * mkTerm(Kind kind, const std::vector<Term>& children) 1852 */ 1853 SUBSET, 1854 /** 1855 * Set membership predicate. 1856 * Parameters: 2 1857 * -[1]..[2]: Terms of set sort, [1] a member of set [2]? 1858 * Create with: 1859 * mkTerm(Kind kind, Term child1, Term child2) 1860 * mkTerm(Kind kind, const std::vector<Term>& children) 1861 */ 1862 MEMBER, 1863 /** 1864 * The set of the single element given as a parameter. 1865 * Parameters: 1 1866 * -[1]: Single element 1867 * Create with: 1868 * mkTerm(Kind kind, Term child) 1869 */ 1870 SINGLETON, 1871 /** 1872 * The set obtained by inserting elements; 1873 * Parameters: n > 0 1874 * -[1]..[n-1]: Elements inserted into set [n] 1875 * -[n]: Set Term 1876 * Create with: 1877 * mkTerm(Kind kind, Term child) 1878 * mkTerm(Kind kind, Term child1, Term child2) 1879 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1880 * mkTerm(Kind kind, const std::vector<Term>& children) 1881 */ 1882 INSERT, 1883 /** 1884 * Set cardinality. 1885 * Parameters: 1 1886 * -[1]: Set to determine the cardinality of 1887 * Create with: 1888 * mkTerm(Kind kind, Term child) 1889 */ 1890 CARD, 1891 /** 1892 * Set complement with respect to finite universe. 1893 * Parameters: 1 1894 * -[1]: Set to complement 1895 * Create with: 1896 * mkTerm(Kind kind, Term child) 1897 */ 1898 COMPLEMENT, 1899 /** 1900 * Finite universe set. 1901 * All set variables must be interpreted as subsets of it. 1902 * Create with: 1903 * mkUniverseSet(Sort sort) 1904 */ 1905 UNIVERSE_SET, 1906 /** 1907 * Set join. 1908 * Parameters: 2 1909 * -[1]..[2]: Terms of set sort 1910 * Create with: 1911 * mkTerm(Kind kind, Term child1, Term child2) 1912 * mkTerm(Kind kind, const std::vector<Term>& children) 1913 */ 1914 JOIN, 1915 /** 1916 * Set cartesian product. 1917 * Parameters: 2 1918 * -[1]..[2]: Terms of set sort 1919 * Create with: 1920 * mkTerm(Kind kind, Term child1, Term child2) 1921 * mkTerm(Kind kind, const std::vector<Term>& children) 1922 */ 1923 PRODUCT, 1924 /** 1925 * Set transpose. 1926 * Parameters: 1 1927 * -[1]: Term of set sort 1928 * Create with: 1929 * mkTerm(Kind kind, Term child) 1930 */ 1931 TRANSPOSE, 1932 /** 1933 * Set transitive closure. 1934 * Parameters: 1 1935 * -[1]: Term of set sort 1936 * Create with: 1937 * mkTerm(Kind kind, Term child) 1938 */ 1939 TCLOSURE, 1940 /** 1941 * Set join image. 1942 * Parameters: 2 1943 * -[1]..[2]: Terms of set sort 1944 * Create with: 1945 * mkTerm(Kind kind, Term child1, Term child2) 1946 * mkTerm(Kind kind, const std::vector<Term>& children) 1947 */ 1948 JOIN_IMAGE, 1949 /** 1950 * Set identity. 1951 * Parameters: 1 1952 * -[1]: Term of set sort 1953 * Create with: 1954 * mkTerm(Kind kind, Term child) 1955 */ 1956 IDEN, 1957 1958 /* Strings --------------------------------------------------------------- */ 1959 1960 /** 1961 * String concat. 1962 * Parameters: n > 1 1963 * -[1]..[n]: Terms of String sort 1964 * Create with: 1965 * mkTerm(Kind kind, Term child1, Term child2) 1966 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1967 * mkTerm(Kind kind, const std::vector<Term>& children) 1968 */ 1969 STRING_CONCAT, 1970 /** 1971 * String membership. 1972 * Parameters: 2 1973 * -[1]..[2]: Terms of String sort 1974 * Create with: 1975 * mkTerm(Kind kind, Term child1, Term child2) 1976 * mkTerm(Kind kind, const std::vector<Term>& children) 1977 */ 1978 STRING_IN_REGEXP, 1979 /** 1980 * String length. 1981 * Parameters: 1 1982 * -[1]: Term of String sort 1983 * Create with: 1984 * mkTerm(Kind kind, Term child) 1985 */ 1986 STRING_LENGTH, 1987 /** 1988 * String substring. 1989 * Extracts a substring, starting at index i and of length l, from a string 1990 * s. If the start index is negative, the start index is greater than the 1991 * length of the string, or the length is negative, the result is the empty 1992 * string. 1993 * Parameters: 3 1994 * -[1]: Term of sort String 1995 * -[2]: Term of sort Integer (index i) 1996 * -[3]: Term of sort Integer (length l) 1997 * Create with: 1998 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 1999 * mkTerm(Kind kind, const std::vector<Term>& children) 2000 */ 2001 STRING_SUBSTR, 2002 /** 2003 * String character at. 2004 * Returns the character at index i from a string s. If the index is negative 2005 * or the index is greater than the length of the string, the result is the 2006 * empty string. Otherwise the result is a string of length 1. 2007 * Parameters: 2 2008 * -[1]: Term of sort String (string s) 2009 * -[2]: Term of sort Integer (index i) 2010 * Create with: 2011 * mkTerm(Kind kind, Term child1, Term child2) 2012 * mkTerm(Kind kind, const std::vector<Term>& children) 2013 */ 2014 STRING_CHARAT, 2015 /** 2016 * String contains. 2017 * Checks whether a string s1 contains another string s2. If s2 is empty, the 2018 * result is always true. 2019 * Parameters: 2 2020 * -[1]: Term of sort String (the string s1) 2021 * -[2]: Term of sort String (the string s2) 2022 * Create with: 2023 * mkTerm(Kind kind, Term child1, Term child2) 2024 * mkTerm(Kind kind, const std::vector<Term>& children) 2025 */ 2026 STRING_STRCTN, 2027 /** 2028 * String index-of. 2029 * Returns the index of a substring s2 in a string s1 starting at index i. If 2030 * the index is negative or greater than the length of string s1 or the 2031 * substring s2 does not appear in string s1 after index i, the result is -1. 2032 * Parameters: 3 2033 * -[1]: Term of sort String (substring s1) 2034 * -[2]: Term of sort String (substring s2) 2035 * -[3]: Term of sort Integer (index i) 2036 * Create with: 2037 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 2038 * mkTerm(Kind kind, const std::vector<Term>& children) 2039 */ 2040 STRING_STRIDOF, 2041 /** 2042 * String replace. 2043 * Replaces a string s2 in a string s1 with string s3. If s2 does not appear 2044 * in s1, s1 is returned unmodified. 2045 * Parameters: 3 2046 * -[1]: Term of sort String (string s1) 2047 * -[2]: Term of sort String (string s2) 2048 * -[3]: Term of sort String (string s3) 2049 * Create with: 2050 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 2051 * mkTerm(Kind kind, const std::vector<Term>& children) 2052 */ 2053 STRING_STRREPL, 2054 /** 2055 * String prefix-of. 2056 * Checks whether a string s1 is a prefix of string s2. If string s1 is 2057 * empty, this operator returns true. 2058 * Parameters: 2 2059 * -[1]: Term of sort String (string s1) 2060 * -[2]: Term of sort String (string s2) 2061 * Create with: 2062 * mkTerm(Kind kind, Term child1, Term child2) 2063 * mkTerm(Kind kind, const std::vector<Term>& children) 2064 */ 2065 STRING_PREFIX, 2066 /** 2067 * String suffix-of. 2068 * Checks whether a string s1 is a suffix of string 2. If string s1 is empty, 2069 * this operator returns true. 2070 * Parameters: 2 2071 * -[1]: Term of sort String (string s1) 2072 * -[2]: Term of sort String (string s2) 2073 * Create with: 2074 * mkTerm(Kind kind, Term child1, Term child2) 2075 * mkTerm(Kind kind, const std::vector<Term>& children) 2076 */ 2077 STRING_SUFFIX, 2078 /** 2079 * Integer to string. 2080 * If the integer is negative this operator returns the empty string. 2081 * Parameters: 1 2082 * -[1]: Term of sort Integer 2083 * Create with: 2084 * mkTerm(Kind kind, Term child) 2085 */ 2086 STRING_ITOS, 2087 /** 2088 * String to integer (total function). 2089 * If the string does not contain an integer or the integer is negative, the 2090 * operator returns -1. 2091 * Parameters: 1 2092 * -[1]: Term of sort String 2093 * Create with: 2094 * mkTerm(Kind kind, Term child) 2095 */ 2096 STRING_STOI, 2097 /** 2098 * Constant string. 2099 * Parameters: 2100 * See mkString() 2101 * Create with: 2102 * mkString(const char* s) 2103 * mkString(const std::string& s) 2104 * mkString(const unsigned char c) 2105 * mkString(const std::vector<unsigned>& s) 2106 */ 2107 CONST_STRING, 2108 /** 2109 * Conversion from string to regexp. 2110 * Parameters: 1 2111 * -[1]: Term of sort String 2112 * Create with: 2113 * mkTerm(Kind kind, Term child) 2114 */ 2115 STRING_TO_REGEXP, 2116 /** 2117 * Regexp Concatenation . 2118 * Parameters: 2 2119 * -[1]..[2]: Terms of Regexp sort 2120 * Create with: 2121 * mkTerm(Kind kind, Term child1, Term child2) 2122 * mkTerm(Kind kind, const std::vector<Term>& children) 2123 */ 2124 REGEXP_CONCAT, 2125 /** 2126 * Regexp union. 2127 * Parameters: 2 2128 * -[1]..[2]: Terms of Regexp sort 2129 * Create with: 2130 * mkTerm(Kind kind, Term child1, Term child2) 2131 * mkTerm(Kind kind, const std::vector<Term>& children) 2132 */ 2133 REGEXP_UNION, 2134 /** 2135 * Regexp intersection. 2136 * Parameters: 2 2137 * -[1]..[2]: Terms of Regexp sort 2138 * Create with: 2139 * mkTerm(Kind kind, Term child1, Term child2) 2140 * mkTerm(Kind kind, const std::vector<Term>& children) 2141 */ 2142 REGEXP_INTER, 2143 /** 2144 * Regexp *. 2145 * Parameters: 1 2146 * -[1]: Term of sort Regexp 2147 * Create with: 2148 * mkTerm(Kind kind, Term child) 2149 */ 2150 REGEXP_STAR, 2151 /** 2152 * Regexp +. 2153 * Parameters: 1 2154 * -[1]: Term of sort Regexp 2155 * Create with: 2156 * mkTerm(Kind kind, Term child) 2157 */ 2158 REGEXP_PLUS, 2159 /** 2160 * Regexp ?. 2161 * Parameters: 1 2162 * -[1]: Term of sort Regexp 2163 * Create with: 2164 * mkTerm(Kind kind, Term child) 2165 */ 2166 REGEXP_OPT, 2167 /** 2168 * Regexp range. 2169 * Parameters: 2 2170 * -[1]: Lower bound character for the range 2171 * -[2]: Upper bound character for the range 2172 * Create with: 2173 * mkTerm(Kind kind, Term child1, Term child2) 2174 * mkTerm(Kind kind, const std::vector<Term>& children) 2175 */ 2176 REGEXP_RANGE, 2177 /** 2178 * Regexp loop. 2179 * Parameters: 2 (3) 2180 * -[1]: Term of sort RegExp 2181 * -[2]: Lower bound for the number of repetitions of the first argument 2182 * -[3]: Upper bound for the number of repetitions of the first argument 2183 * Create with: 2184 * mkTerm(Kind kind, Term child1, Term child2) 2185 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 2186 * mkTerm(Kind kind, const std::vector<Term>& children) 2187 */ 2188 REGEXP_LOOP, 2189 /** 2190 * Regexp empty. 2191 * Parameters: 0 2192 * Create with: 2193 * mkRegexpEmpty() 2194 * mkTerm(Kind kind) 2195 */ 2196 REGEXP_EMPTY, 2197 /** 2198 * Regexp all characters. 2199 * Parameters: 0 2200 * Create with: 2201 * mkRegexpSigma() 2202 * mkTerm(Kind kind) 2203 */ 2204 REGEXP_SIGMA, 2205 #if 0 2206 /* regexp rv (internal use only) */ 2207 REGEXP_RV, 2208 #endif 2209 2210 /* Quantifiers ----------------------------------------------------------- */ 2211 2212 /** 2213 * Universally quantified formula. 2214 * Parameters: 2 (3) 2215 * -[1]: BOUND_VAR_LIST Term 2216 * -[2]: Quantifier body 2217 * -[3]: (optional) INST_PATTERN_LIST Term 2218 * Create with: 2219 * mkTerm(Kind kind, Term child1, Term child2) 2220 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 2221 * mkTerm(Kind kind, const std::vector<Term>& children) 2222 */ 2223 FORALL, 2224 /** 2225 * Existentially quantified formula. 2226 * Parameters: 2 (3) 2227 * -[1]: BOUND_VAR_LIST Term 2228 * -[2]: Quantifier body 2229 * -[3]: (optional) INST_PATTERN_LIST Term 2230 * Create with: 2231 * mkTerm(Kind kind, Term child1, Term child2) 2232 * mkTerm(Kind kind, Term child1, Term child2, Term child3) 2233 * mkTerm(Kind kind, const std::vector<Term>& children) 2234 */ 2235 EXISTS, 2236 #if 0 2237 /* instantiation constant */ 2238 INST_CONSTANT, 2239 /* instantiation pattern */ 2240 INST_PATTERN, 2241 /* a list of bound variables (used to bind variables under a quantifier) */ 2242 BOUND_VAR_LIST, 2243 /* instantiation no-pattern */ 2244 INST_NO_PATTERN, 2245 /* instantiation attribute */ 2246 INST_ATTRIBUTE, 2247 /* a list of instantiation patterns */ 2248 INST_PATTERN_LIST, 2249 /* predicate for specifying term in instantiation closure. */ 2250 INST_CLOSURE, 2251 /* general rewrite rule (for rewrite-rules theory) */ 2252 REWRITE_RULE, 2253 /* actual rewrite rule (for rewrite-rules theory) */ 2254 RR_REWRITE, 2255 /* actual reduction rule (for rewrite-rules theory) */ 2256 RR_REDUCTION, 2257 /* actual deduction rule (for rewrite-rules theory) */ 2258 RR_DEDUCTION, 2259 2260 /* Sort Kinds ------------------------------------------------------------ */ 2261 2262 /* array type */ 2263 ARRAY_TYPE, 2264 /* a type parameter for type ascription */ 2265 ASCRIPTION_TYPE, 2266 /* constructor */ 2267 CONSTRUCTOR_TYPE, 2268 /* a datatype type index */ 2269 DATATYPE_TYPE, 2270 /* selector */ 2271 SELECTOR_TYPE, 2272 /* set type, takes as parameter the type of the elements */ 2273 SET_TYPE, 2274 /* sort tag */ 2275 SORT_TAG, 2276 /* specifies types of user-declared 'uninterpreted' sorts */ 2277 SORT_TYPE, 2278 /* tester */ 2279 TESTER_TYPE, 2280 /* a representation for basic types */ 2281 TYPE_CONSTANT, 2282 /* a function type */ 2283 FUNCTION_TYPE, 2284 /* the type of a symbolic expression */ 2285 SEXPR_TYPE, 2286 /* bit-vector type */ 2287 BITVECTOR_TYPE, 2288 /* floating-point type */ 2289 FLOATINGPOINT_TYPE, 2290 #endif 2291 2292 /* ----------------------------------------------------------------------- */ 2293 /* marks the upper-bound of this enumeration */ 2294 LAST_KIND 2295 }; 2296 2297 /** 2298 * Get the string representation of a given kind. 2299 * @param k the kind 2300 * @return the string representation of kind k 2301 */ 2302 std::string kindToString(Kind k) CVC4_PUBLIC; 2303 2304 /** 2305 * Serialize a kind to given stream. 2306 * @param out the output stream 2307 * @param k the kind to be serialized to the given output stream 2308 * @return the output stream 2309 */ 2310 std::ostream& operator<<(std::ostream& out, Kind k) CVC4_PUBLIC; 2311 2312 /** 2313 * Hash function for Kinds. 2314 */ 2315 struct CVC4_PUBLIC KindHashFunction 2316 { 2317 size_t operator()(Kind k) const; 2318 }; 2319 2320 } // namespace api 2321 } // namespace CVC4 2322 2323 #endif 2324