cvc4-1.4
kind.h
Go to the documentation of this file.
1 /********************* */
14 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20 
21 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27 
28 /* Edit the template file instead: */
29 /* /builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h */
30 
31 /********************* */
47 #include "cvc4_public.h"
48 
49 #ifndef __CVC4__KIND_H
50 #define __CVC4__KIND_H
51 
52 #include <iostream>
53 #include <sstream>
54 
55 #include "util/exception.h"
56 
57 namespace CVC4 {
58 namespace kind {
59 
64  /* from builtin */
86  /* from booleans */
88  NOT,
89  AND,
90  IFF,
92  OR,
93  XOR,
94  ITE,
96  /* from uf */
101  /* from arith */
112  ABS,
114  POW,
118  LT,
119  LEQ,
120  GT,
121  GEQ,
126  /* from bv */
181  /* from arrays */
189  /* from datatypes */
214  /* from sets */
225  /* from strings */
257  /* from quantifiers */
269  /* from idl */
270 
273 };/* enum Kind_t */
274 
275 }/* CVC4::kind namespace */
276 
277 // import Kind into the "CVC4" namespace but keep the individual kind
278 // constants under kind::
280 
281 namespace kind {
282 
283 inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
284 inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
285  using namespace CVC4::kind;
286 
287  switch(k) {
288 
289  /* special cases */
290  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
291  case NULL_EXPR: out << "NULL"; break;
292 
293  /* from builtin */
294  case SORT_TAG: out << "SORT_TAG"; break;
295  case SORT_TYPE: out << "SORT_TYPE"; break;
296  case UNINTERPRETED_CONSTANT: out << "UNINTERPRETED_CONSTANT"; break;
297  case ABSTRACT_VALUE: out << "ABSTRACT_VALUE"; break;
298  case BUILTIN: out << "BUILTIN"; break;
299  case FUNCTION: out << "FUNCTION"; break;
300  case APPLY: out << "APPLY"; break;
301  case EQUAL: out << "EQUAL"; break;
302  case DISTINCT: out << "DISTINCT"; break;
303  case VARIABLE: out << "VARIABLE"; break;
304  case BOUND_VARIABLE: out << "BOUND_VARIABLE"; break;
305  case SKOLEM: out << "SKOLEM"; break;
306  case SEXPR: out << "SEXPR"; break;
307  case LAMBDA: out << "LAMBDA"; break;
308  case CHAIN: out << "CHAIN"; break;
309  case CHAIN_OP: out << "CHAIN_OP"; break;
310  case TYPE_CONSTANT: out << "TYPE_CONSTANT"; break;
311  case FUNCTION_TYPE: out << "FUNCTION_TYPE"; break;
312  case SEXPR_TYPE: out << "SEXPR_TYPE"; break;
313  case SUBTYPE_TYPE: out << "SUBTYPE_TYPE"; break;
314 
315  /* from booleans */
316  case CONST_BOOLEAN: out << "CONST_BOOLEAN"; break;
317  case NOT: out << "NOT"; break;
318  case AND: out << "AND"; break;
319  case IFF: out << "IFF"; break;
320  case IMPLIES: out << "IMPLIES"; break;
321  case OR: out << "OR"; break;
322  case XOR: out << "XOR"; break;
323  case ITE: out << "ITE"; break;
324 
325  /* from uf */
326  case APPLY_UF: out << "APPLY_UF"; break;
327  case CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; break;
328  case COMBINED_CARDINALITY_CONSTRAINT: out << "COMBINED_CARDINALITY_CONSTRAINT"; break;
329 
330  /* from arith */
331  case PLUS: out << "PLUS"; break;
332  case MULT: out << "MULT"; break;
333  case MINUS: out << "MINUS"; break;
334  case UMINUS: out << "UMINUS"; break;
335  case DIVISION: out << "DIVISION"; break;
336  case DIVISION_TOTAL: out << "DIVISION_TOTAL"; break;
337  case INTS_DIVISION: out << "INTS_DIVISION"; break;
338  case INTS_DIVISION_TOTAL: out << "INTS_DIVISION_TOTAL"; break;
339  case INTS_MODULUS: out << "INTS_MODULUS"; break;
340  case INTS_MODULUS_TOTAL: out << "INTS_MODULUS_TOTAL"; break;
341  case ABS: out << "ABS"; break;
342  case DIVISIBLE: out << "DIVISIBLE"; break;
343  case POW: out << "POW"; break;
344  case DIVISIBLE_OP: out << "DIVISIBLE_OP"; break;
345  case SUBRANGE_TYPE: out << "SUBRANGE_TYPE"; break;
346  case CONST_RATIONAL: out << "CONST_RATIONAL"; break;
347  case LT: out << "LT"; break;
348  case LEQ: out << "LEQ"; break;
349  case GT: out << "GT"; break;
350  case GEQ: out << "GEQ"; break;
351  case IS_INTEGER: out << "IS_INTEGER"; break;
352  case TO_INTEGER: out << "TO_INTEGER"; break;
353  case TO_REAL: out << "TO_REAL"; break;
354 
355  /* from bv */
356  case BITVECTOR_TYPE: out << "BITVECTOR_TYPE"; break;
357  case CONST_BITVECTOR: out << "CONST_BITVECTOR"; break;
358  case BITVECTOR_CONCAT: out << "BITVECTOR_CONCAT"; break;
359  case BITVECTOR_AND: out << "BITVECTOR_AND"; break;
360  case BITVECTOR_OR: out << "BITVECTOR_OR"; break;
361  case BITVECTOR_XOR: out << "BITVECTOR_XOR"; break;
362  case BITVECTOR_NOT: out << "BITVECTOR_NOT"; break;
363  case BITVECTOR_NAND: out << "BITVECTOR_NAND"; break;
364  case BITVECTOR_NOR: out << "BITVECTOR_NOR"; break;
365  case BITVECTOR_XNOR: out << "BITVECTOR_XNOR"; break;
366  case BITVECTOR_COMP: out << "BITVECTOR_COMP"; break;
367  case BITVECTOR_MULT: out << "BITVECTOR_MULT"; break;
368  case BITVECTOR_PLUS: out << "BITVECTOR_PLUS"; break;
369  case BITVECTOR_SUB: out << "BITVECTOR_SUB"; break;
370  case BITVECTOR_NEG: out << "BITVECTOR_NEG"; break;
371  case BITVECTOR_UDIV: out << "BITVECTOR_UDIV"; break;
372  case BITVECTOR_UREM: out << "BITVECTOR_UREM"; break;
373  case BITVECTOR_SDIV: out << "BITVECTOR_SDIV"; break;
374  case BITVECTOR_SREM: out << "BITVECTOR_SREM"; break;
375  case BITVECTOR_SMOD: out << "BITVECTOR_SMOD"; break;
376  case BITVECTOR_UDIV_TOTAL: out << "BITVECTOR_UDIV_TOTAL"; break;
377  case BITVECTOR_UREM_TOTAL: out << "BITVECTOR_UREM_TOTAL"; break;
378  case BITVECTOR_SHL: out << "BITVECTOR_SHL"; break;
379  case BITVECTOR_LSHR: out << "BITVECTOR_LSHR"; break;
380  case BITVECTOR_ASHR: out << "BITVECTOR_ASHR"; break;
381  case BITVECTOR_ULT: out << "BITVECTOR_ULT"; break;
382  case BITVECTOR_ULE: out << "BITVECTOR_ULE"; break;
383  case BITVECTOR_UGT: out << "BITVECTOR_UGT"; break;
384  case BITVECTOR_UGE: out << "BITVECTOR_UGE"; break;
385  case BITVECTOR_SLT: out << "BITVECTOR_SLT"; break;
386  case BITVECTOR_SLE: out << "BITVECTOR_SLE"; break;
387  case BITVECTOR_SGT: out << "BITVECTOR_SGT"; break;
388  case BITVECTOR_SGE: out << "BITVECTOR_SGE"; break;
389  case BITVECTOR_EAGER_ATOM: out << "BITVECTOR_EAGER_ATOM"; break;
390  case BITVECTOR_ACKERMANIZE_UDIV: out << "BITVECTOR_ACKERMANIZE_UDIV"; break;
391  case BITVECTOR_ACKERMANIZE_UREM: out << "BITVECTOR_ACKERMANIZE_UREM"; break;
392  case BITVECTOR_BITOF_OP: out << "BITVECTOR_BITOF_OP"; break;
393  case BITVECTOR_EXTRACT_OP: out << "BITVECTOR_EXTRACT_OP"; break;
394  case BITVECTOR_REPEAT_OP: out << "BITVECTOR_REPEAT_OP"; break;
395  case BITVECTOR_ZERO_EXTEND_OP: out << "BITVECTOR_ZERO_EXTEND_OP"; break;
396  case BITVECTOR_SIGN_EXTEND_OP: out << "BITVECTOR_SIGN_EXTEND_OP"; break;
397  case BITVECTOR_ROTATE_LEFT_OP: out << "BITVECTOR_ROTATE_LEFT_OP"; break;
398  case BITVECTOR_ROTATE_RIGHT_OP: out << "BITVECTOR_ROTATE_RIGHT_OP"; break;
399  case BITVECTOR_BITOF: out << "BITVECTOR_BITOF"; break;
400  case BITVECTOR_EXTRACT: out << "BITVECTOR_EXTRACT"; break;
401  case BITVECTOR_REPEAT: out << "BITVECTOR_REPEAT"; break;
402  case BITVECTOR_ZERO_EXTEND: out << "BITVECTOR_ZERO_EXTEND"; break;
403  case BITVECTOR_SIGN_EXTEND: out << "BITVECTOR_SIGN_EXTEND"; break;
404  case BITVECTOR_ROTATE_LEFT: out << "BITVECTOR_ROTATE_LEFT"; break;
405  case BITVECTOR_ROTATE_RIGHT: out << "BITVECTOR_ROTATE_RIGHT"; break;
406  case INT_TO_BITVECTOR_OP: out << "INT_TO_BITVECTOR_OP"; break;
407  case INT_TO_BITVECTOR: out << "INT_TO_BITVECTOR"; break;
408  case BITVECTOR_TO_NAT: out << "BITVECTOR_TO_NAT"; break;
409 
410  /* from arrays */
411  case ARRAY_TYPE: out << "ARRAY_TYPE"; break;
412  case SELECT: out << "SELECT"; break;
413  case STORE: out << "STORE"; break;
414  case STORE_ALL: out << "STORE_ALL"; break;
415  case ARR_TABLE_FUN: out << "ARR_TABLE_FUN"; break;
416  case ARRAY_LAMBDA: out << "ARRAY_LAMBDA"; break;
417 
418  /* from datatypes */
419  case CONSTRUCTOR_TYPE: out << "CONSTRUCTOR_TYPE"; break;
420  case SELECTOR_TYPE: out << "SELECTOR_TYPE"; break;
421  case TESTER_TYPE: out << "TESTER_TYPE"; break;
422  case APPLY_CONSTRUCTOR: out << "APPLY_CONSTRUCTOR"; break;
423  case APPLY_SELECTOR: out << "APPLY_SELECTOR"; break;
424  case APPLY_SELECTOR_TOTAL: out << "APPLY_SELECTOR_TOTAL"; break;
425  case APPLY_TESTER: out << "APPLY_TESTER"; break;
426  case DATATYPE_TYPE: out << "DATATYPE_TYPE"; break;
427  case PARAMETRIC_DATATYPE: out << "PARAMETRIC_DATATYPE"; break;
428  case APPLY_TYPE_ASCRIPTION: out << "APPLY_TYPE_ASCRIPTION"; break;
429  case ASCRIPTION_TYPE: out << "ASCRIPTION_TYPE"; break;
430  case TUPLE_TYPE: out << "TUPLE_TYPE"; break;
431  case TUPLE: out << "TUPLE"; break;
432  case TUPLE_SELECT_OP: out << "TUPLE_SELECT_OP"; break;
433  case TUPLE_SELECT: out << "TUPLE_SELECT"; break;
434  case TUPLE_UPDATE_OP: out << "TUPLE_UPDATE_OP"; break;
435  case TUPLE_UPDATE: out << "TUPLE_UPDATE"; break;
436  case RECORD_TYPE: out << "RECORD_TYPE"; break;
437  case RECORD: out << "RECORD"; break;
438  case RECORD_SELECT_OP: out << "RECORD_SELECT_OP"; break;
439  case RECORD_SELECT: out << "RECORD_SELECT"; break;
440  case RECORD_UPDATE_OP: out << "RECORD_UPDATE_OP"; break;
441  case RECORD_UPDATE: out << "RECORD_UPDATE"; break;
442 
443  /* from sets */
444  case EMPTYSET: out << "EMPTYSET"; break;
445  case SET_TYPE: out << "SET_TYPE"; break;
446  case UNION: out << "UNION"; break;
447  case INTERSECTION: out << "INTERSECTION"; break;
448  case SETMINUS: out << "SETMINUS"; break;
449  case SUBSET: out << "SUBSET"; break;
450  case MEMBER: out << "MEMBER"; break;
451  case SINGLETON: out << "SINGLETON"; break;
452  case INSERT: out << "INSERT"; break;
453 
454  /* from strings */
455  case STRING_CONCAT: out << "STRING_CONCAT"; break;
456  case STRING_IN_REGEXP: out << "STRING_IN_REGEXP"; break;
457  case STRING_LENGTH: out << "STRING_LENGTH"; break;
458  case STRING_SUBSTR: out << "STRING_SUBSTR"; break;
459  case STRING_SUBSTR_TOTAL: out << "STRING_SUBSTR_TOTAL"; break;
460  case STRING_CHARAT: out << "STRING_CHARAT"; break;
461  case STRING_STRCTN: out << "STRING_STRCTN"; break;
462  case STRING_STRIDOF: out << "STRING_STRIDOF"; break;
463  case STRING_STRREPL: out << "STRING_STRREPL"; break;
464  case STRING_PREFIX: out << "STRING_PREFIX"; break;
465  case STRING_SUFFIX: out << "STRING_SUFFIX"; break;
466  case STRING_ITOS: out << "STRING_ITOS"; break;
467  case STRING_STOI: out << "STRING_STOI"; break;
468  case STRING_U16TOS: out << "STRING_U16TOS"; break;
469  case STRING_STOU16: out << "STRING_STOU16"; break;
470  case STRING_U32TOS: out << "STRING_U32TOS"; break;
471  case STRING_STOU32: out << "STRING_STOU32"; break;
472  case CONST_STRING: out << "CONST_STRING"; break;
473  case CONST_REGEXP: out << "CONST_REGEXP"; break;
474  case STRING_TO_REGEXP: out << "STRING_TO_REGEXP"; break;
475  case REGEXP_CONCAT: out << "REGEXP_CONCAT"; break;
476  case REGEXP_UNION: out << "REGEXP_UNION"; break;
477  case REGEXP_INTER: out << "REGEXP_INTER"; break;
478  case REGEXP_STAR: out << "REGEXP_STAR"; break;
479  case REGEXP_PLUS: out << "REGEXP_PLUS"; break;
480  case REGEXP_OPT: out << "REGEXP_OPT"; break;
481  case REGEXP_RANGE: out << "REGEXP_RANGE"; break;
482  case REGEXP_LOOP: out << "REGEXP_LOOP"; break;
483  case REGEXP_EMPTY: out << "REGEXP_EMPTY"; break;
484  case REGEXP_SIGMA: out << "REGEXP_SIGMA"; break;
485 
486  /* from quantifiers */
487  case FORALL: out << "FORALL"; break;
488  case EXISTS: out << "EXISTS"; break;
489  case INST_CONSTANT: out << "INST_CONSTANT"; break;
490  case BOUND_VAR_LIST: out << "BOUND_VAR_LIST"; break;
491  case INST_PATTERN: out << "INST_PATTERN"; break;
492  case INST_PATTERN_LIST: out << "INST_PATTERN_LIST"; break;
493  case REWRITE_RULE: out << "REWRITE_RULE"; break;
494  case RR_REWRITE: out << "RR_REWRITE"; break;
495  case RR_REDUCTION: out << "RR_REDUCTION"; break;
496  case RR_DEDUCTION: out << "RR_DEDUCTION"; break;
497 
498  /* from idl */
499 
500  case LAST_KIND: out << "LAST_KIND"; break;
501  default: out << "UNKNOWNKIND!" << int(k); break;
502  }
503 
504  return out;
505 }
506 
507 #line 64 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
508 
512 /* TODO: This could be generated. */
513 inline bool isAssociative(::CVC4::Kind k) {
514  switch(k) {
515  case kind::AND:
516  case kind::OR:
517  case kind::MULT:
518  case kind::PLUS:
519  return true;
520 
521  default:
522  return false;
523  }
524 }
525 
526 inline std::string kindToString(::CVC4::Kind k) {
527  std::stringstream ss;
528  ss << k;
529  return ss.str();
530 }
531 
533  inline size_t operator()(::CVC4::Kind k) const {
534  return k;
535  }
536 };/* struct KindHashFunction */
537 
538 }/* CVC4::kind namespace */
539 
555 #line 102 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
557 };/* enum TypeConstant */
558 
563  inline size_t operator()(TypeConstant tc) const {
564  return tc;
565  }
566 };/* struct TypeConstantHashFunction */
567 
568 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
569  switch(typeConstant) {
570  case BUILTIN_OPERATOR_TYPE: out << "the type for built-in operators"; break;
571  case BOOLEAN_TYPE: out << "Boolean type"; break;
572  case REAL_TYPE: out << "real type"; break;
573  case INTEGER_TYPE: out << "integer type"; break;
574  case STRING_TYPE: out << "String type"; break;
575  case REGEXP_TYPE: out << "RegExp type"; break;
576  case BOUND_VAR_LIST_TYPE: out << "the type of bound variable lists"; break;
577  case INST_PATTERN_TYPE: out << "instantiation pattern type"; break;
578  case INST_PATTERN_LIST_TYPE: out << "the type of instantiation pattern lists"; break;
579  case RRHB_TYPE: out << "head and body of the rule type (for rewrite-rules theory)"; break;
580 
581 #line 118 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
582  default:
583  out << "UNKNOWN_TYPE_CONSTANT";
584  break;
585  }
586  return out;
587 }
588 
589 namespace theory {
590 
591 enum TheoryId {
602 
603 #line 130 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
605 };/* enum TheoryId */
606 
607 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
609 
611  return id = static_cast<TheoryId>(((int)id) + 1);
612 }
613 
614 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
615  switch(theoryId) {
616  case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
617  case THEORY_BOOL: out << "THEORY_BOOL"; break;
618  case THEORY_UF: out << "THEORY_UF"; break;
619  case THEORY_ARITH: out << "THEORY_ARITH"; break;
620  case THEORY_BV: out << "THEORY_BV"; break;
621  case THEORY_ARRAY: out << "THEORY_ARRAY"; break;
622  case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
623  case THEORY_SETS: out << "THEORY_SETS"; break;
624  case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
625  case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
626 
627 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
628  default:
629  out << "UNKNOWN_THEORY";
630  break;
631  }
632  return out;
633 }
634 
636  switch(k) {
638  case kind::NULL_EXPR:
639  break;
640  case kind::SORT_TAG: return THEORY_BUILTIN;
641  case kind::SORT_TYPE: return THEORY_BUILTIN;
644  case kind::BUILTIN: return THEORY_BUILTIN;
645  case kind::FUNCTION: return THEORY_BUILTIN;
646  case kind::APPLY: return THEORY_BUILTIN;
647  case kind::EQUAL: return THEORY_BUILTIN;
648  case kind::DISTINCT: return THEORY_BUILTIN;
649  case kind::VARIABLE: return THEORY_BUILTIN;
651  case kind::SKOLEM: return THEORY_BUILTIN;
652  case kind::SEXPR: return THEORY_BUILTIN;
653  case kind::LAMBDA: return THEORY_BUILTIN;
654  case kind::CHAIN: return THEORY_BUILTIN;
655  case kind::CHAIN_OP: return THEORY_BUILTIN;
656  case kind::TYPE_CONSTANT: return THEORY_BUILTIN;
657  case kind::FUNCTION_TYPE: return THEORY_BUILTIN;
658  case kind::SEXPR_TYPE: return THEORY_BUILTIN;
659  case kind::SUBTYPE_TYPE: return THEORY_BUILTIN;
660  case kind::CONST_BOOLEAN: return THEORY_BOOL;
661  case kind::NOT: return THEORY_BOOL;
662  case kind::AND: return THEORY_BOOL;
663  case kind::IFF: return THEORY_BOOL;
664  case kind::IMPLIES: return THEORY_BOOL;
665  case kind::OR: return THEORY_BOOL;
666  case kind::XOR: return THEORY_BOOL;
667  case kind::ITE: return THEORY_BOOL;
668  case kind::APPLY_UF: return THEORY_UF;
671  case kind::PLUS: return THEORY_ARITH;
672  case kind::MULT: return THEORY_ARITH;
673  case kind::MINUS: return THEORY_ARITH;
674  case kind::UMINUS: return THEORY_ARITH;
675  case kind::DIVISION: return THEORY_ARITH;
676  case kind::DIVISION_TOTAL: return THEORY_ARITH;
677  case kind::INTS_DIVISION: return THEORY_ARITH;
679  case kind::INTS_MODULUS: return THEORY_ARITH;
681  case kind::ABS: return THEORY_ARITH;
682  case kind::DIVISIBLE: return THEORY_ARITH;
683  case kind::POW: return THEORY_ARITH;
684  case kind::DIVISIBLE_OP: return THEORY_ARITH;
685  case kind::SUBRANGE_TYPE: return THEORY_ARITH;
686  case kind::CONST_RATIONAL: return THEORY_ARITH;
687  case kind::LT: return THEORY_ARITH;
688  case kind::LEQ: return THEORY_ARITH;
689  case kind::GT: return THEORY_ARITH;
690  case kind::GEQ: return THEORY_ARITH;
691  case kind::IS_INTEGER: return THEORY_ARITH;
692  case kind::TO_INTEGER: return THEORY_ARITH;
693  case kind::TO_REAL: return THEORY_ARITH;
694  case kind::BITVECTOR_TYPE: return THEORY_BV;
695  case kind::CONST_BITVECTOR: return THEORY_BV;
696  case kind::BITVECTOR_CONCAT: return THEORY_BV;
697  case kind::BITVECTOR_AND: return THEORY_BV;
698  case kind::BITVECTOR_OR: return THEORY_BV;
699  case kind::BITVECTOR_XOR: return THEORY_BV;
700  case kind::BITVECTOR_NOT: return THEORY_BV;
701  case kind::BITVECTOR_NAND: return THEORY_BV;
702  case kind::BITVECTOR_NOR: return THEORY_BV;
703  case kind::BITVECTOR_XNOR: return THEORY_BV;
704  case kind::BITVECTOR_COMP: return THEORY_BV;
705  case kind::BITVECTOR_MULT: return THEORY_BV;
706  case kind::BITVECTOR_PLUS: return THEORY_BV;
707  case kind::BITVECTOR_SUB: return THEORY_BV;
708  case kind::BITVECTOR_NEG: return THEORY_BV;
709  case kind::BITVECTOR_UDIV: return THEORY_BV;
710  case kind::BITVECTOR_UREM: return THEORY_BV;
711  case kind::BITVECTOR_SDIV: return THEORY_BV;
712  case kind::BITVECTOR_SREM: return THEORY_BV;
713  case kind::BITVECTOR_SMOD: return THEORY_BV;
716  case kind::BITVECTOR_SHL: return THEORY_BV;
717  case kind::BITVECTOR_LSHR: return THEORY_BV;
718  case kind::BITVECTOR_ASHR: return THEORY_BV;
719  case kind::BITVECTOR_ULT: return THEORY_BV;
720  case kind::BITVECTOR_ULE: return THEORY_BV;
721  case kind::BITVECTOR_UGT: return THEORY_BV;
722  case kind::BITVECTOR_UGE: return THEORY_BV;
723  case kind::BITVECTOR_SLT: return THEORY_BV;
724  case kind::BITVECTOR_SLE: return THEORY_BV;
725  case kind::BITVECTOR_SGT: return THEORY_BV;
726  case kind::BITVECTOR_SGE: return THEORY_BV;
730  case kind::BITVECTOR_BITOF_OP: return THEORY_BV;
737  case kind::BITVECTOR_BITOF: return THEORY_BV;
738  case kind::BITVECTOR_EXTRACT: return THEORY_BV;
739  case kind::BITVECTOR_REPEAT: return THEORY_BV;
745  case kind::INT_TO_BITVECTOR: return THEORY_BV;
746  case kind::BITVECTOR_TO_NAT: return THEORY_BV;
747  case kind::ARRAY_TYPE: return THEORY_ARRAY;
748  case kind::SELECT: return THEORY_ARRAY;
749  case kind::STORE: return THEORY_ARRAY;
750  case kind::STORE_ALL: return THEORY_ARRAY;
751  case kind::ARR_TABLE_FUN: return THEORY_ARRAY;
752  case kind::ARRAY_LAMBDA: return THEORY_ARRAY;
755  case kind::TESTER_TYPE: return THEORY_DATATYPES;
764  case kind::TUPLE_TYPE: return THEORY_DATATYPES;
765  case kind::TUPLE: return THEORY_DATATYPES;
770  case kind::RECORD_TYPE: return THEORY_DATATYPES;
771  case kind::RECORD: return THEORY_DATATYPES;
776  case kind::EMPTYSET: return THEORY_SETS;
777  case kind::SET_TYPE: return THEORY_SETS;
778  case kind::UNION: return THEORY_SETS;
779  case kind::INTERSECTION: return THEORY_SETS;
780  case kind::SETMINUS: return THEORY_SETS;
781  case kind::SUBSET: return THEORY_SETS;
782  case kind::MEMBER: return THEORY_SETS;
783  case kind::SINGLETON: return THEORY_SETS;
784  case kind::INSERT: return THEORY_SETS;
785  case kind::STRING_CONCAT: return THEORY_STRINGS;
787  case kind::STRING_LENGTH: return THEORY_STRINGS;
788  case kind::STRING_SUBSTR: return THEORY_STRINGS;
790  case kind::STRING_CHARAT: return THEORY_STRINGS;
791  case kind::STRING_STRCTN: return THEORY_STRINGS;
794  case kind::STRING_PREFIX: return THEORY_STRINGS;
795  case kind::STRING_SUFFIX: return THEORY_STRINGS;
796  case kind::STRING_ITOS: return THEORY_STRINGS;
797  case kind::STRING_STOI: return THEORY_STRINGS;
798  case kind::STRING_U16TOS: return THEORY_STRINGS;
799  case kind::STRING_STOU16: return THEORY_STRINGS;
800  case kind::STRING_U32TOS: return THEORY_STRINGS;
801  case kind::STRING_STOU32: return THEORY_STRINGS;
802  case kind::CONST_STRING: return THEORY_STRINGS;
803  case kind::CONST_REGEXP: return THEORY_STRINGS;
805  case kind::REGEXP_CONCAT: return THEORY_STRINGS;
806  case kind::REGEXP_UNION: return THEORY_STRINGS;
807  case kind::REGEXP_INTER: return THEORY_STRINGS;
808  case kind::REGEXP_STAR: return THEORY_STRINGS;
809  case kind::REGEXP_PLUS: return THEORY_STRINGS;
810  case kind::REGEXP_OPT: return THEORY_STRINGS;
811  case kind::REGEXP_RANGE: return THEORY_STRINGS;
812  case kind::REGEXP_LOOP: return THEORY_STRINGS;
813  case kind::REGEXP_EMPTY: return THEORY_STRINGS;
814  case kind::REGEXP_SIGMA: return THEORY_STRINGS;
815  case kind::FORALL: return THEORY_QUANTIFIERS;
816  case kind::EXISTS: return THEORY_QUANTIFIERS;
825 
826 #line 158 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
827  case kind::LAST_KIND:
828  break;
829  }
830  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
831 }
832 
834  switch(typeConstant) {
836  case BOOLEAN_TYPE: return THEORY_BOOL;
837  case REAL_TYPE: return THEORY_ARITH;
838  case INTEGER_TYPE: return THEORY_ARITH;
839  case STRING_TYPE: return THEORY_STRINGS;
840  case REGEXP_TYPE: return THEORY_STRINGS;
844  case RRHB_TYPE: return THEORY_QUANTIFIERS;
845 
846 #line 168 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
847  case LAST_TYPE:
848  break;
849  }
850  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
851 }
852 
853 }/* CVC4::theory namespace */
854 }/* CVC4 namespace */
855 
856 #endif /* __CVC4__KIND_H */
Boolean type.
Definition: kind.h:545
bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (1...
Definition: kind.h:175
unary negation of a bit-vector (69)
Definition: kind.h:141
truth and falsity; payload is a (C++) bool (21)
Definition: kind.h:87
integer modulus with interpreted division by 0 (internal symbol) (41)
Definition: kind.h:111
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:543
multiplication of two or more bit-vectors (66)
Definition: kind.h:138
the kind of expressions representing abstract values (other than uninterpreted sort constants); paylo...
Definition: kind.h:68
bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (79) ...
Definition: kind.h:151
general rewrite rule (for rewrite-rules theory) (182)
Definition: kind.h:264
logical equivalence (exactly two parameters) (24)
Definition: kind.h:90
existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body...
Definition: kind.h:259
bitwise nand of two bit-vectors (62)
Definition: kind.h:134
bitwise or of two or more bit-vectors (59)
Definition: kind.h:131
regexp range (172)
Definition: kind.h:252
a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (47) ...
Definition: kind.h:117
operator for a record update; payload is an instance CVC4::RecordSelect class (135) ...
Definition: kind.h:211
specifies types of user-declared 'uninterpreted' sorts (2)
Definition: kind.h:66
string to uint32 (162)
Definition: kind.h:242
integer modulus, division by 0 undefined (user symbol) (40)
Definition: kind.h:110
operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend clas...
Definition: kind.h:166
regexp all characters (175)
Definition: kind.h:255
divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (43) ...
Definition: kind.h:113
the set of the single element given as a parameter (144)
Definition: kind.h:222
2's complement signed remainder (sign follows dividend) (73)
Definition: kind.h:145
a datatype type (121)
Definition: kind.h:197
arithmetic unary negation (35)
Definition: kind.h:105
bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (87) ...
Definition: kind.h:159
string concat (N-ary) (146)
Definition: kind.h:226
TheoryId kindToTheoryId(::CVC4::Kind k)
Definition: kind.h:635
a tuple (N-ary) (126)
Definition: kind.h:202
const TheoryId THEORY_SAT_SOLVER
Definition: kind.h:608
the chained operator; payload is an instance of the CVC4::Chain class (16)
Definition: kind.h:80
operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class (93) ...
Definition: kind.h:165
string substr (user symbol) (149)
Definition: kind.h:229
set union (139)
Definition: kind.h:217
head and body of the rule type (for rewrite-rules theory)
Definition: kind.h:553
exclusive or (exactly two parameters) (27)
Definition: kind.h:93
a list of instantiation patterns (181)
Definition: kind.h:263
bool isAssociative(::CVC4::Kind k)
Returns true if the given kind is associative.
Definition: kind.h:513
string to integer (total function) (158)
Definition: kind.h:238
a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values f...
Definition: kind.h:208
actual reduction rule (for rewrite-rules theory) (184)
Definition: kind.h:266
predicate subtype; payload is an instance of the CVC4::Predicate class (20)
Definition: kind.h:84
selector (115)
Definition: kind.h:191
a defined function (6)
Definition: kind.h:70
string substr (internal symbol) (150)
Definition: kind.h:230
integer division, division by 0 undefined (user symbol) (38)
Definition: kind.h:108
bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term ...
Definition: kind.h:176
the type for built-in operators
Definition: kind.h:544
tester application; first parameter is a tester, second is a datatype term (120)
Definition: kind.h:196
regexp intersection (168)
Definition: kind.h:248
subtraction of two bit-vectors (68)
Definition: kind.h:140
::CVC4::kind::Kind_t Kind
Definition: kind.h:279
selector application; parameter is a datatype term (undefined if mis-applied) (118) ...
Definition: kind.h:194
bit-vector unsigned greater than (the two bit-vector parameters must have same width) (82) ...
Definition: kind.h:154
size_t operator()(TypeConstant tc) const
Definition: kind.h:563
operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (45...
Definition: kind.h:115
uint16 to string (159)
Definition: kind.h:239
bit-vector signed less than (the two bit-vector parameters must have same width) (84) ...
Definition: kind.h:156
chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoinin...
Definition: kind.h:79
operator for a tuple select; payload is an instance of the CVC4::TupleSelect class (127) ...
Definition: kind.h:203
operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector...
Definition: kind.h:177
bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term ...
Definition: kind.h:170
bit-vector unsigned less than (the two bit-vector parameters must have same width) (80) ...
Definition: kind.h:152
TheoryId & operator++(TheoryId &id)
Definition: kind.h:610
const TheoryId THEORY_FIRST
Definition: kind.h:607
a variable (not permitted in bindings) (10)
Definition: kind.h:74
CVC4's exception base class and some associated utilities.
a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (11) ...
Definition: kind.h:75
bitwise xnor of two bit-vectors (64)
Definition: kind.h:136
a function type (18)
Definition: kind.h:82
a string of characters (163)
Definition: kind.h:243
array type (108)
Definition: kind.h:182
array select; first parameter is an array term, second is the selection index (109) ...
Definition: kind.h:183
array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by ar...
Definition: kind.h:185
a regular expression (164)
Definition: kind.h:244
real division with interpreted division by 0 (internal symbol) (37)
Definition: kind.h:107
operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class (92) ...
Definition: kind.h:164
membership (147)
Definition: kind.h:227
addition of two or more bit-vectors (67)
Definition: kind.h:139
string length (148)
Definition: kind.h:228
a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (56) ...
Definition: kind.h:128
regexp loop (173)
Definition: kind.h:253
bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (100) ...
Definition: kind.h:172
string suffixof (156)
Definition: kind.h:236
marks the upper-bound of this enumeration
Definition: kind.h:271
disequality (N-ary, sorts must match) (9)
Definition: kind.h:73
arithmetic power (44)
Definition: kind.h:114
application of an uninterpreted function; first parameter is the function, remaining ones are paramet...
Definition: kind.h:97
absolute value (42)
Definition: kind.h:112
bitwise nor of two bit-vectors (63)
Definition: kind.h:135
greater than, x > y (50)
Definition: kind.h:120
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
bit-vector signed greater than (the two bit-vector parameters must have same width) (86) ...
Definition: kind.h:158
regexp * (169)
Definition: kind.h:249
arithmetic multiplication (N-ary) (33)
Definition: kind.h:103
std::ostream & operator<<(std::ostream &, CVC4::Kind)
Definition: kind.h:284
operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight cl...
Definition: kind.h:169
bit-vector signed less than or equal (the two bit-vector parameters must have same width) (85) ...
Definition: kind.h:157
actual rewrite rule (for rewrite-rules theory) (183)
Definition: kind.h:265
set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (145) ...
Definition: kind.h:223
type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (123)
Definition: kind.h:199
bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (99) ...
Definition: kind.h:171
arithmetic binary subtraction operator (34)
Definition: kind.h:104
set type, takes as parameter the type of the elements (138)
Definition: kind.h:216
set intersection (140)
Definition: kind.h:218
logical implication (exactly two parameters) (25)
Definition: kind.h:91
logical not (22)
Definition: kind.h:88
real division, division by 0 undefined (user symbol) (36)
Definition: kind.h:106
the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::Uni...
Definition: kind.h:67
the type of an integer subrange (46)
Definition: kind.h:116
a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (14) ...
Definition: kind.h:78
record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from (134) ...
Definition: kind.h:210
unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend...
Definition: kind.h:148
bitwise xor of two or more bit-vectors (60)
Definition: kind.h:132
2's complement signed remainder (sign follows divisor) (74)
Definition: kind.h:146
operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft clas...
Definition: kind.h:168
constructor application; first parameter is the constructor, remaining parameters (if any) are parame...
Definition: kind.h:193
Macros that should be defined everywhere during the building of the libraries and driver binary...
array table function (internal-only symbol) (112)
Definition: kind.h:186
greater than or equal, x >= y (51)
Definition: kind.h:121
regexp empty (174)
Definition: kind.h:254
operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend clas...
Definition: kind.h:167
logical and (N-ary) (23)
Definition: kind.h:89
regexp ? (171)
Definition: kind.h:251
less than or equal, x <= y (49)
Definition: kind.h:119
bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (1...
Definition: kind.h:174
application of a defined function (7)
Definition: kind.h:71
instantiation constant (178)
Definition: kind.h:260
the type of instantiation pattern lists
Definition: kind.h:552
Null kind.
Definition: kind.h:62
convert term to integer by the floor function (parameter is a real-sorted term) (53) ...
Definition: kind.h:123
integer division with interpreted division by 0 (internal symbol) (39)
Definition: kind.h:109
the type of a symbolic expression (19)
Definition: kind.h:83
instantiation pattern (180)
Definition: kind.h:262
regexp union (167)
Definition: kind.h:247
term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal...
Definition: kind.h:162
regexp concat (166)
Definition: kind.h:246
arithmetic addition (N-ary) (32)
Definition: kind.h:102
String type.
Definition: kind.h:548
sort tag (1)
Definition: kind.h:65
uint32 to string (161)
Definition: kind.h:241
the type of bound variable lists
Definition: kind.h:550
regexp + (170)
Definition: kind.h:250
logical or (N-ary) (26)
Definition: kind.h:92
bitwise and of two or more bit-vectors (58)
Definition: kind.h:130
a list of bound variables (used to bind variables under a quantifier) (179)
Definition: kind.h:261
2's complement signed division (72)
Definition: kind.h:144
set subtraction (141)
Definition: kind.h:219
equality (two parameters only, sorts must match) (8)
Definition: kind.h:72
unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0) (70) ...
Definition: kind.h:142
string replace (154)
Definition: kind.h:234
unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern...
Definition: kind.h:147
term-is-integer predicate (parameter is a real-sorted term) (52)
Definition: kind.h:122
integer type
Definition: kind.h:547
std::string kindToString(::CVC4::Kind k)
Definition: kind.h:526
term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal...
Definition: kind.h:161
parametric datatype (122)
Definition: kind.h:198
a symbolic expression (any arity) (13)
Definition: kind.h:77
string contains (152)
Definition: kind.h:232
TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
Definition: kind.h:833
operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (129) ...
Definition: kind.h:205
less than, x < y (48)
Definition: kind.h:118
a Skolem variable (internal only) (12)
Definition: kind.h:76
tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple (128)
Definition: kind.h:204
struct CVC4::options::out__option_t out
array lambda (internal-only symbol) (113)
Definition: kind.h:187
string charat (user symbol) (151)
Definition: kind.h:231
bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (1...
Definition: kind.h:173
instantiation pattern type
Definition: kind.h:551
bit-vector shift left (the two bit-vector parameters must have same width) (77)
Definition: kind.h:149
operator for a record select; payload is an instance CVC4::RecordSelect class (133) ...
Definition: kind.h:209
cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subt...
Definition: kind.h:124
tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple...
Definition: kind.h:206
selector application; parameter is a datatype term (defined rigidly if mis-applied) (119) ...
Definition: kind.h:195
size_t operator()(::CVC4::Kind k) const
Definition: kind.h:533
tuple type (125)
Definition: kind.h:201
concatenation of two or more bit-vectors (57)
Definition: kind.h:129
tester (116)
Definition: kind.h:192
subset predicate; first parameter a subset of second (142)
Definition: kind.h:220
bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (81) ...
Definition: kind.h:153
combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of th...
Definition: kind.h:99
the kind of expressions representing built-in operators (5)
Definition: kind.h:69
record type (131)
Definition: kind.h:207
a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (124) ...
Definition: kind.h:200
array store; first parameter is an array term, second is the store index, third is the term to store ...
Definition: kind.h:184
operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf c...
Definition: kind.h:163
bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (107)
Definition: kind.h:179
actual deduction rule (for rewrite-rules theory) (185)
Definition: kind.h:267
record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record t...
Definition: kind.h:212
convert string to regexp (165)
Definition: kind.h:245
bit-vector type (55)
Definition: kind.h:127
constructor (114)
Definition: kind.h:190
set membership predicate; first parameter a member of second (143)
Definition: kind.h:221
RegExp type.
Definition: kind.h:549
a representation for basic types (17)
Definition: kind.h:81
integer to string (157)
Definition: kind.h:237
integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer ter...
Definition: kind.h:178
unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0) (71) ...
Definition: kind.h:143
string indexof (153)
Definition: kind.h:233
bitwise not of a bit-vector (61)
Definition: kind.h:133
Kind_t
Definition: kind.h:60
the empty set constant; payload is an instance of the CVC4::EmptySet class (137)
Definition: kind.h:215
string prefixof (155)
Definition: kind.h:235
equality comparison of two bit-vectors (returns one bit) (65)
Definition: kind.h:137
bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (83) ...
Definition: kind.h:155
We hash the constants with their values.
Definition: kind.h:562
universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body...
Definition: kind.h:258
formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (88) ...
Definition: kind.h:160
string to uint16 (160)
Definition: kind.h:240
if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) cond...
Definition: kind.h:94
cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integ...
Definition: kind.h:98
real type
Definition: kind.h:546
bit-vector logical shift right (the two bit-vector parameters must have same width) (78) ...
Definition: kind.h:150