cvc4-1.3
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.3/builds/aarch64-redhat-linux-gnu/default-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 */
178  /* from arrays */
185  /* from datatypes */
209  /* from quantifiers */
217  /* from rewriterules */
223  /* from idl */
224 
225  /* from strings */
243 };/* enum Kind_t */
244 
245 }/* CVC4::kind namespace */
246 
247 // import Kind into the "CVC4" namespace but keep the individual kind
248 // constants under kind::
250 
251 namespace kind {
252 
253 inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
254 inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
255  using namespace CVC4::kind;
256 
257  switch(k) {
258 
259  /* special cases */
260  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
261  case NULL_EXPR: out << "NULL"; break;
262 
263  /* from builtin */
264  case SORT_TAG: out << "SORT_TAG"; break;
265  case SORT_TYPE: out << "SORT_TYPE"; break;
266  case UNINTERPRETED_CONSTANT: out << "UNINTERPRETED_CONSTANT"; break;
267  case ABSTRACT_VALUE: out << "ABSTRACT_VALUE"; break;
268  case BUILTIN: out << "BUILTIN"; break;
269  case FUNCTION: out << "FUNCTION"; break;
270  case APPLY: out << "APPLY"; break;
271  case EQUAL: out << "EQUAL"; break;
272  case DISTINCT: out << "DISTINCT"; break;
273  case VARIABLE: out << "VARIABLE"; break;
274  case BOUND_VARIABLE: out << "BOUND_VARIABLE"; break;
275  case SKOLEM: out << "SKOLEM"; break;
276  case SEXPR: out << "SEXPR"; break;
277  case LAMBDA: out << "LAMBDA"; break;
278  case CHAIN: out << "CHAIN"; break;
279  case CHAIN_OP: out << "CHAIN_OP"; break;
280  case TYPE_CONSTANT: out << "TYPE_CONSTANT"; break;
281  case FUNCTION_TYPE: out << "FUNCTION_TYPE"; break;
282  case SEXPR_TYPE: out << "SEXPR_TYPE"; break;
283  case SUBTYPE_TYPE: out << "SUBTYPE_TYPE"; break;
284 
285  /* from booleans */
286  case CONST_BOOLEAN: out << "CONST_BOOLEAN"; break;
287  case NOT: out << "NOT"; break;
288  case AND: out << "AND"; break;
289  case IFF: out << "IFF"; break;
290  case IMPLIES: out << "IMPLIES"; break;
291  case OR: out << "OR"; break;
292  case XOR: out << "XOR"; break;
293  case ITE: out << "ITE"; break;
294 
295  /* from uf */
296  case APPLY_UF: out << "APPLY_UF"; break;
297  case CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; break;
298  case COMBINED_CARDINALITY_CONSTRAINT: out << "COMBINED_CARDINALITY_CONSTRAINT"; break;
299 
300  /* from arith */
301  case PLUS: out << "PLUS"; break;
302  case MULT: out << "MULT"; break;
303  case MINUS: out << "MINUS"; break;
304  case UMINUS: out << "UMINUS"; break;
305  case DIVISION: out << "DIVISION"; break;
306  case DIVISION_TOTAL: out << "DIVISION_TOTAL"; break;
307  case INTS_DIVISION: out << "INTS_DIVISION"; break;
308  case INTS_DIVISION_TOTAL: out << "INTS_DIVISION_TOTAL"; break;
309  case INTS_MODULUS: out << "INTS_MODULUS"; break;
310  case INTS_MODULUS_TOTAL: out << "INTS_MODULUS_TOTAL"; break;
311  case ABS: out << "ABS"; break;
312  case DIVISIBLE: out << "DIVISIBLE"; break;
313  case POW: out << "POW"; break;
314  case DIVISIBLE_OP: out << "DIVISIBLE_OP"; break;
315  case SUBRANGE_TYPE: out << "SUBRANGE_TYPE"; break;
316  case CONST_RATIONAL: out << "CONST_RATIONAL"; break;
317  case LT: out << "LT"; break;
318  case LEQ: out << "LEQ"; break;
319  case GT: out << "GT"; break;
320  case GEQ: out << "GEQ"; break;
321  case IS_INTEGER: out << "IS_INTEGER"; break;
322  case TO_INTEGER: out << "TO_INTEGER"; break;
323  case TO_REAL: out << "TO_REAL"; break;
324 
325  /* from bv */
326  case BITVECTOR_TYPE: out << "BITVECTOR_TYPE"; break;
327  case CONST_BITVECTOR: out << "CONST_BITVECTOR"; break;
328  case BITVECTOR_CONCAT: out << "BITVECTOR_CONCAT"; break;
329  case BITVECTOR_AND: out << "BITVECTOR_AND"; break;
330  case BITVECTOR_OR: out << "BITVECTOR_OR"; break;
331  case BITVECTOR_XOR: out << "BITVECTOR_XOR"; break;
332  case BITVECTOR_NOT: out << "BITVECTOR_NOT"; break;
333  case BITVECTOR_NAND: out << "BITVECTOR_NAND"; break;
334  case BITVECTOR_NOR: out << "BITVECTOR_NOR"; break;
335  case BITVECTOR_XNOR: out << "BITVECTOR_XNOR"; break;
336  case BITVECTOR_COMP: out << "BITVECTOR_COMP"; break;
337  case BITVECTOR_MULT: out << "BITVECTOR_MULT"; break;
338  case BITVECTOR_PLUS: out << "BITVECTOR_PLUS"; break;
339  case BITVECTOR_SUB: out << "BITVECTOR_SUB"; break;
340  case BITVECTOR_NEG: out << "BITVECTOR_NEG"; break;
341  case BITVECTOR_UDIV: out << "BITVECTOR_UDIV"; break;
342  case BITVECTOR_UREM: out << "BITVECTOR_UREM"; break;
343  case BITVECTOR_SDIV: out << "BITVECTOR_SDIV"; break;
344  case BITVECTOR_SREM: out << "BITVECTOR_SREM"; break;
345  case BITVECTOR_SMOD: out << "BITVECTOR_SMOD"; break;
346  case BITVECTOR_UDIV_TOTAL: out << "BITVECTOR_UDIV_TOTAL"; break;
347  case BITVECTOR_UREM_TOTAL: out << "BITVECTOR_UREM_TOTAL"; break;
348  case BITVECTOR_SHL: out << "BITVECTOR_SHL"; break;
349  case BITVECTOR_LSHR: out << "BITVECTOR_LSHR"; break;
350  case BITVECTOR_ASHR: out << "BITVECTOR_ASHR"; break;
351  case BITVECTOR_ULT: out << "BITVECTOR_ULT"; break;
352  case BITVECTOR_ULE: out << "BITVECTOR_ULE"; break;
353  case BITVECTOR_UGT: out << "BITVECTOR_UGT"; break;
354  case BITVECTOR_UGE: out << "BITVECTOR_UGE"; break;
355  case BITVECTOR_SLT: out << "BITVECTOR_SLT"; break;
356  case BITVECTOR_SLE: out << "BITVECTOR_SLE"; break;
357  case BITVECTOR_SGT: out << "BITVECTOR_SGT"; break;
358  case BITVECTOR_SGE: out << "BITVECTOR_SGE"; break;
359  case BITVECTOR_BITOF_OP: out << "BITVECTOR_BITOF_OP"; break;
360  case BITVECTOR_EXTRACT_OP: out << "BITVECTOR_EXTRACT_OP"; break;
361  case BITVECTOR_REPEAT_OP: out << "BITVECTOR_REPEAT_OP"; break;
362  case BITVECTOR_ZERO_EXTEND_OP: out << "BITVECTOR_ZERO_EXTEND_OP"; break;
363  case BITVECTOR_SIGN_EXTEND_OP: out << "BITVECTOR_SIGN_EXTEND_OP"; break;
364  case BITVECTOR_ROTATE_LEFT_OP: out << "BITVECTOR_ROTATE_LEFT_OP"; break;
365  case BITVECTOR_ROTATE_RIGHT_OP: out << "BITVECTOR_ROTATE_RIGHT_OP"; break;
366  case BITVECTOR_BITOF: out << "BITVECTOR_BITOF"; break;
367  case BITVECTOR_EXTRACT: out << "BITVECTOR_EXTRACT"; break;
368  case BITVECTOR_REPEAT: out << "BITVECTOR_REPEAT"; break;
369  case BITVECTOR_ZERO_EXTEND: out << "BITVECTOR_ZERO_EXTEND"; break;
370  case BITVECTOR_SIGN_EXTEND: out << "BITVECTOR_SIGN_EXTEND"; break;
371  case BITVECTOR_ROTATE_LEFT: out << "BITVECTOR_ROTATE_LEFT"; break;
372  case BITVECTOR_ROTATE_RIGHT: out << "BITVECTOR_ROTATE_RIGHT"; break;
373  case INT_TO_BITVECTOR_OP: out << "INT_TO_BITVECTOR_OP"; break;
374  case INT_TO_BITVECTOR: out << "INT_TO_BITVECTOR"; break;
375  case BITVECTOR_TO_NAT: out << "BITVECTOR_TO_NAT"; break;
376 
377  /* from arrays */
378  case ARRAY_TYPE: out << "ARRAY_TYPE"; break;
379  case SELECT: out << "SELECT"; break;
380  case STORE: out << "STORE"; break;
381  case STORE_ALL: out << "STORE_ALL"; break;
382  case ARR_TABLE_FUN: out << "ARR_TABLE_FUN"; break;
383 
384  /* from datatypes */
385  case CONSTRUCTOR_TYPE: out << "CONSTRUCTOR_TYPE"; break;
386  case SELECTOR_TYPE: out << "SELECTOR_TYPE"; break;
387  case TESTER_TYPE: out << "TESTER_TYPE"; break;
388  case APPLY_CONSTRUCTOR: out << "APPLY_CONSTRUCTOR"; break;
389  case APPLY_SELECTOR: out << "APPLY_SELECTOR"; break;
390  case APPLY_TESTER: out << "APPLY_TESTER"; break;
391  case DATATYPE_TYPE: out << "DATATYPE_TYPE"; break;
392  case PARAMETRIC_DATATYPE: out << "PARAMETRIC_DATATYPE"; break;
393  case APPLY_TYPE_ASCRIPTION: out << "APPLY_TYPE_ASCRIPTION"; break;
394  case ASCRIPTION_TYPE: out << "ASCRIPTION_TYPE"; break;
395  case TUPLE_TYPE: out << "TUPLE_TYPE"; break;
396  case TUPLE: out << "TUPLE"; break;
397  case TUPLE_SELECT_OP: out << "TUPLE_SELECT_OP"; break;
398  case TUPLE_SELECT: out << "TUPLE_SELECT"; break;
399  case TUPLE_UPDATE_OP: out << "TUPLE_UPDATE_OP"; break;
400  case TUPLE_UPDATE: out << "TUPLE_UPDATE"; break;
401  case RECORD_TYPE: out << "RECORD_TYPE"; break;
402  case RECORD: out << "RECORD"; break;
403  case RECORD_SELECT_OP: out << "RECORD_SELECT_OP"; break;
404  case RECORD_SELECT: out << "RECORD_SELECT"; break;
405  case RECORD_UPDATE_OP: out << "RECORD_UPDATE_OP"; break;
406  case RECORD_UPDATE: out << "RECORD_UPDATE"; break;
407 
408  /* from quantifiers */
409  case FORALL: out << "FORALL"; break;
410  case EXISTS: out << "EXISTS"; break;
411  case INST_CONSTANT: out << "INST_CONSTANT"; break;
412  case BOUND_VAR_LIST: out << "BOUND_VAR_LIST"; break;
413  case INST_PATTERN: out << "INST_PATTERN"; break;
414  case INST_PATTERN_LIST: out << "INST_PATTERN_LIST"; break;
415 
416  /* from rewriterules */
417  case REWRITE_RULE: out << "REWRITE_RULE"; break;
418  case RR_REWRITE: out << "RR_REWRITE"; break;
419  case RR_REDUCTION: out << "RR_REDUCTION"; break;
420  case RR_DEDUCTION: out << "RR_DEDUCTION"; break;
421 
422  /* from idl */
423 
424  /* from strings */
425  case STRING_CONCAT: out << "STRING_CONCAT"; break;
426  case STRING_IN_REGEXP: out << "STRING_IN_REGEXP"; break;
427  case STRING_LENGTH: out << "STRING_LENGTH"; break;
428  case STRING_SUBSTR: out << "STRING_SUBSTR"; break;
429  case CONST_STRING: out << "CONST_STRING"; break;
430  case CONST_REGEXP: out << "CONST_REGEXP"; break;
431  case STRING_TO_REGEXP: out << "STRING_TO_REGEXP"; break;
432  case REGEXP_CONCAT: out << "REGEXP_CONCAT"; break;
433  case REGEXP_OR: out << "REGEXP_OR"; break;
434  case REGEXP_INTER: out << "REGEXP_INTER"; break;
435  case REGEXP_STAR: out << "REGEXP_STAR"; break;
436  case REGEXP_PLUS: out << "REGEXP_PLUS"; break;
437  case REGEXP_OPT: out << "REGEXP_OPT"; break;
438  case REGEXP_RANGE: out << "REGEXP_RANGE"; break;
439 
440  case LAST_KIND: out << "LAST_KIND"; break;
441  default: out << "UNKNOWNKIND!" << int(k); break;
442  }
443 
444  return out;
445 }
446 
447 #line 64 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
448 
452 /* TODO: This could be generated. */
453 inline bool isAssociative(::CVC4::Kind k) {
454  switch(k) {
455  case kind::AND:
456  case kind::OR:
457  case kind::MULT:
458  case kind::PLUS:
459  return true;
460 
461  default:
462  return false;
463  }
464 }
465 
466 inline std::string kindToString(::CVC4::Kind k) {
467  std::stringstream ss;
468  ss << k;
469  return ss.str();
470 }
471 
473  inline size_t operator()(::CVC4::Kind k) const {
474  return k;
475  }
476 };/* struct KindHashFunction */
477 
478 }/* CVC4::kind namespace */
479 
495 #line 102 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
497 };/* enum TypeConstant */
498 
503  inline size_t operator()(TypeConstant tc) const {
504  return tc;
505  }
506 };/* struct TypeConstantHashFunction */
507 
508 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
509  switch(typeConstant) {
510  case BUILTIN_OPERATOR_TYPE: out << "Built in type for built in operators"; break;
511  case BOOLEAN_TYPE: out << "Boolean type"; break;
512  case REAL_TYPE: out << "Real type"; break;
513  case INTEGER_TYPE: out << "Integer type"; break;
514  case BOUND_VAR_LIST_TYPE: out << "Bound Var type"; break;
515  case INST_PATTERN_TYPE: out << "Instantiation pattern type"; break;
516  case INST_PATTERN_LIST_TYPE: out << "Instantiation pattern list type"; break;
517  case RRHB_TYPE: out << "head and body of the rule type"; break;
518  case STRING_TYPE: out << "String type"; break;
519  case REGEXP_TYPE: out << "RegExp type"; break;
520 
521 #line 118 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
522  default:
523  out << "UNKNOWN_TYPE_CONSTANT";
524  break;
525  }
526  return out;
527 }
528 
529 namespace theory {
530 
531 enum TheoryId {
542 
543 #line 130 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
545 };/* enum TheoryId */
546 
547 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
549 
551  return id = static_cast<TheoryId>(((int)id) + 1);
552 }
553 
554 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
555  switch(theoryId) {
556  case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
557  case THEORY_BOOL: out << "THEORY_BOOL"; break;
558  case THEORY_UF: out << "THEORY_UF"; break;
559  case THEORY_ARITH: out << "THEORY_ARITH"; break;
560  case THEORY_BV: out << "THEORY_BV"; break;
561  case THEORY_ARRAY: out << "THEORY_ARRAY"; break;
562  case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
563  case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
564  case THEORY_REWRITERULES: out << "THEORY_REWRITERULES"; break;
565  case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
566 
567 #line 144 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
568  default:
569  out << "UNKNOWN_THEORY";
570  break;
571  }
572  return out;
573 }
574 
576  switch(k) {
578  case kind::NULL_EXPR:
579  break;
580  case kind::SORT_TAG: return THEORY_BUILTIN;
581  case kind::SORT_TYPE: return THEORY_BUILTIN;
584  case kind::BUILTIN: return THEORY_BUILTIN;
585  case kind::FUNCTION: return THEORY_BUILTIN;
586  case kind::APPLY: return THEORY_BUILTIN;
587  case kind::EQUAL: return THEORY_BUILTIN;
588  case kind::DISTINCT: return THEORY_BUILTIN;
589  case kind::VARIABLE: return THEORY_BUILTIN;
591  case kind::SKOLEM: return THEORY_BUILTIN;
592  case kind::SEXPR: return THEORY_BUILTIN;
593  case kind::LAMBDA: return THEORY_BUILTIN;
594  case kind::CHAIN: return THEORY_BUILTIN;
595  case kind::CHAIN_OP: return THEORY_BUILTIN;
596  case kind::TYPE_CONSTANT: return THEORY_BUILTIN;
597  case kind::FUNCTION_TYPE: return THEORY_BUILTIN;
598  case kind::SEXPR_TYPE: return THEORY_BUILTIN;
599  case kind::SUBTYPE_TYPE: return THEORY_BUILTIN;
600  case kind::CONST_BOOLEAN: return THEORY_BOOL;
601  case kind::NOT: return THEORY_BOOL;
602  case kind::AND: return THEORY_BOOL;
603  case kind::IFF: return THEORY_BOOL;
604  case kind::IMPLIES: return THEORY_BOOL;
605  case kind::OR: return THEORY_BOOL;
606  case kind::XOR: return THEORY_BOOL;
607  case kind::ITE: return THEORY_BOOL;
608  case kind::APPLY_UF: return THEORY_UF;
611  case kind::PLUS: return THEORY_ARITH;
612  case kind::MULT: return THEORY_ARITH;
613  case kind::MINUS: return THEORY_ARITH;
614  case kind::UMINUS: return THEORY_ARITH;
615  case kind::DIVISION: return THEORY_ARITH;
616  case kind::DIVISION_TOTAL: return THEORY_ARITH;
617  case kind::INTS_DIVISION: return THEORY_ARITH;
619  case kind::INTS_MODULUS: return THEORY_ARITH;
621  case kind::ABS: return THEORY_ARITH;
622  case kind::DIVISIBLE: return THEORY_ARITH;
623  case kind::POW: return THEORY_ARITH;
624  case kind::DIVISIBLE_OP: return THEORY_ARITH;
625  case kind::SUBRANGE_TYPE: return THEORY_ARITH;
626  case kind::CONST_RATIONAL: return THEORY_ARITH;
627  case kind::LT: return THEORY_ARITH;
628  case kind::LEQ: return THEORY_ARITH;
629  case kind::GT: return THEORY_ARITH;
630  case kind::GEQ: return THEORY_ARITH;
631  case kind::IS_INTEGER: return THEORY_ARITH;
632  case kind::TO_INTEGER: return THEORY_ARITH;
633  case kind::TO_REAL: return THEORY_ARITH;
634  case kind::BITVECTOR_TYPE: return THEORY_BV;
635  case kind::CONST_BITVECTOR: return THEORY_BV;
636  case kind::BITVECTOR_CONCAT: return THEORY_BV;
637  case kind::BITVECTOR_AND: return THEORY_BV;
638  case kind::BITVECTOR_OR: return THEORY_BV;
639  case kind::BITVECTOR_XOR: return THEORY_BV;
640  case kind::BITVECTOR_NOT: return THEORY_BV;
641  case kind::BITVECTOR_NAND: return THEORY_BV;
642  case kind::BITVECTOR_NOR: return THEORY_BV;
643  case kind::BITVECTOR_XNOR: return THEORY_BV;
644  case kind::BITVECTOR_COMP: return THEORY_BV;
645  case kind::BITVECTOR_MULT: return THEORY_BV;
646  case kind::BITVECTOR_PLUS: return THEORY_BV;
647  case kind::BITVECTOR_SUB: return THEORY_BV;
648  case kind::BITVECTOR_NEG: return THEORY_BV;
649  case kind::BITVECTOR_UDIV: return THEORY_BV;
650  case kind::BITVECTOR_UREM: return THEORY_BV;
651  case kind::BITVECTOR_SDIV: return THEORY_BV;
652  case kind::BITVECTOR_SREM: return THEORY_BV;
653  case kind::BITVECTOR_SMOD: return THEORY_BV;
656  case kind::BITVECTOR_SHL: return THEORY_BV;
657  case kind::BITVECTOR_LSHR: return THEORY_BV;
658  case kind::BITVECTOR_ASHR: return THEORY_BV;
659  case kind::BITVECTOR_ULT: return THEORY_BV;
660  case kind::BITVECTOR_ULE: return THEORY_BV;
661  case kind::BITVECTOR_UGT: return THEORY_BV;
662  case kind::BITVECTOR_UGE: return THEORY_BV;
663  case kind::BITVECTOR_SLT: return THEORY_BV;
664  case kind::BITVECTOR_SLE: return THEORY_BV;
665  case kind::BITVECTOR_SGT: return THEORY_BV;
666  case kind::BITVECTOR_SGE: return THEORY_BV;
667  case kind::BITVECTOR_BITOF_OP: return THEORY_BV;
674  case kind::BITVECTOR_BITOF: return THEORY_BV;
675  case kind::BITVECTOR_EXTRACT: return THEORY_BV;
676  case kind::BITVECTOR_REPEAT: return THEORY_BV;
682  case kind::INT_TO_BITVECTOR: return THEORY_BV;
683  case kind::BITVECTOR_TO_NAT: return THEORY_BV;
684  case kind::ARRAY_TYPE: return THEORY_ARRAY;
685  case kind::SELECT: return THEORY_ARRAY;
686  case kind::STORE: return THEORY_ARRAY;
687  case kind::STORE_ALL: return THEORY_ARRAY;
688  case kind::ARR_TABLE_FUN: return THEORY_ARRAY;
691  case kind::TESTER_TYPE: return THEORY_DATATYPES;
699  case kind::TUPLE_TYPE: return THEORY_DATATYPES;
700  case kind::TUPLE: return THEORY_DATATYPES;
705  case kind::RECORD_TYPE: return THEORY_DATATYPES;
706  case kind::RECORD: return THEORY_DATATYPES;
711  case kind::FORALL: return THEORY_QUANTIFIERS;
712  case kind::EXISTS: return THEORY_QUANTIFIERS;
721  case kind::STRING_CONCAT: return THEORY_STRINGS;
723  case kind::STRING_LENGTH: return THEORY_STRINGS;
724  case kind::STRING_SUBSTR: return THEORY_STRINGS;
725  case kind::CONST_STRING: return THEORY_STRINGS;
726  case kind::CONST_REGEXP: return THEORY_STRINGS;
728  case kind::REGEXP_CONCAT: return THEORY_STRINGS;
729  case kind::REGEXP_OR: return THEORY_STRINGS;
730  case kind::REGEXP_INTER: return THEORY_STRINGS;
731  case kind::REGEXP_STAR: return THEORY_STRINGS;
732  case kind::REGEXP_PLUS: return THEORY_STRINGS;
733  case kind::REGEXP_OPT: return THEORY_STRINGS;
734  case kind::REGEXP_RANGE: return THEORY_STRINGS;
735 
736 #line 158 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
737  case kind::LAST_KIND:
738  break;
739  }
740  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
741 }
742 
744  switch(typeConstant) {
746  case BOOLEAN_TYPE: return THEORY_BOOL;
747  case REAL_TYPE: return THEORY_ARITH;
748  case INTEGER_TYPE: return THEORY_ARITH;
752  case RRHB_TYPE: return THEORY_REWRITERULES;
753  case STRING_TYPE: return THEORY_STRINGS;
754  case REGEXP_TYPE: return THEORY_STRINGS;
755 
756 #line 168 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
757  case LAST_TYPE:
758  break;
759  }
760  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
761 }
762 
763 }/* CVC4::theory namespace */
764 }/* CVC4 namespace */
765 
766 #endif /* __CVC4__KIND_H */
Boolean type.
Definition: kind.h:485
bit-vector rotate left
Definition: kind.h:172
bit-vector unary negation
Definition: kind.h:141
truth and falsity
Definition: kind.h:87
ints modulus with interpreted division by 0 (internal symbol)
Definition: kind.h:111
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:483
bit-vector multiplication
Definition: kind.h:138
The kind of expressions representing abstract values (other than uninterpreted sort constants) ...
Definition: kind.h:68
bit-vector arithmetic shift right
Definition: kind.h:151
general rewrite rule
Definition: kind.h:218
logical equivalence
Definition: kind.h:90
existentially quantified formula
Definition: kind.h:211
bitwise nand
Definition: kind.h:134
bitwise or
Definition: kind.h:131
regexp range
Definition: kind.h:239
a multiple-precision rational constant
Definition: kind.h:117
operator for a record update
Definition: kind.h:206
sort type
Definition: kind.h:66
ints modulus (user symbol)
Definition: kind.h:110
operator for the bit-vector zero-extend
Definition: kind.h:163
divisibility-by-k predicate
Definition: kind.h:113
bit-vector 2's complement signed remainder (sign follows dividend)
Definition: kind.h:145
datatype type
Definition: kind.h:192
arithmetic unary negation
Definition: kind.h:105
signed greater than or equal
Definition: kind.h:159
string concat
Definition: kind.h:226
TheoryId kindToTheoryId(::CVC4::Kind k)
Definition: kind.h:575
a tuple
Definition: kind.h:197
const TheoryId THEORY_SAT_SOLVER
Definition: kind.h:548
the chained operator
Definition: kind.h:80
operator for the bit-vector repeat
Definition: kind.h:162
string substr
Definition: kind.h:229
head and body of the rule type
Definition: kind.h:491
exclusive or
Definition: kind.h:93
instantiation pattern list
Definition: kind.h:215
bool isAssociative(::CVC4::Kind k)
Returns true if the given kind is associative.
Definition: kind.h:453
a record
Definition: kind.h:203
actual reduction rule
Definition: kind.h:220
predicate subtype
Definition: kind.h:84
function
Definition: kind.h:70
ints division (user symbol)
Definition: kind.h:108
bit-vector rotate right
Definition: kind.h:173
Built in type for built in operators.
Definition: kind.h:484
tester application
Definition: kind.h:191
regexp intersection
Definition: kind.h:235
bit-vector subtraction
Definition: kind.h:140
::CVC4::kind::Kind_t Kind
Definition: kind.h:249
selector application
Definition: kind.h:190
bit-vector unsigned greater than
Definition: kind.h:154
size_t operator()(TypeConstant tc) const
Definition: kind.h:503
operator for the divisibility-by-k predicate
Definition: kind.h:115
bit-vector signed less than
Definition: kind.h:156
chained operator
Definition: kind.h:79
operator for a tuple select
Definition: kind.h:198
operator for the integer conversion to bit-vector
Definition: kind.h:174
bit-vector boolean bit extract
Definition: kind.h:167
bit-vector unsigned less than
Definition: kind.h:152
TheoryId & operator++(TheoryId &id)
Definition: kind.h:550
const TheoryId THEORY_FIRST
Definition: kind.h:547
variable
Definition: kind.h:74
CVC4's exception base class and some associated utilities.
bound variable
Definition: kind.h:75
bitwise xnor
Definition: kind.h:136
regexp or
Definition: kind.h:234
function type
Definition: kind.h:82
a string of characters
Definition: kind.h:230
array type
Definition: kind.h:179
array select
Definition: kind.h:180
array store-all
Definition: kind.h:182
a regular expression
Definition: kind.h:231
real division with interpreted division by 0 (internal symbol)
Definition: kind.h:107
operator for the bit-vector extract
Definition: kind.h:161
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
bit-vector addition
Definition: kind.h:139
string length
Definition: kind.h:228
a fixed-width bit-vector constant
Definition: kind.h:128
bit-vector repeat
Definition: kind.h:169
marks the upper-bound of this enumeration
Definition: kind.h:241
disequality
Definition: kind.h:73
arithmetic power
Definition: kind.h:114
uninterpreted function application
Definition: kind.h:97
absolute value
Definition: kind.h:112
bitwise nor
Definition: kind.h:135
greater than, x > y
Definition: kind.h:120
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory(or a combination of such theories).It is the fourth in the Cooperating Validity Checker family of tools(CVC
bit-vector signed greater than
Definition: kind.h:158
arithmetic multiplication
Definition: kind.h:103
std::ostream & operator<<(std::ostream &, CVC4::Kind)
Definition: kind.h:254
operator for the bit-vector rotate right
Definition: kind.h:166
bit-vector signed less than or equal
Definition: kind.h:157
actual rewrite rule
Definition: kind.h:219
type ascription, for datatype constructor applications
Definition: kind.h:194
bit-vector extract
Definition: kind.h:168
arithmetic binary subtraction operator
Definition: kind.h:104
logical implication
Definition: kind.h:91
logical not
Definition: kind.h:88
real division (user symbol)
Definition: kind.h:106
The kind of expressions representing uninterpreted constants.
Definition: kind.h:67
the type of an integer subrange
Definition: kind.h:116
lambda
Definition: kind.h:78
record select
Definition: kind.h:205
bit-vector total unsigned remainder from truncating division (undefined if divisor is 0) ...
Definition: kind.h:148
bitwise xor
Definition: kind.h:132
bit-vector 2's complement signed remainder (sign follows divisor)
Definition: kind.h:146
operator for the bit-vector rotate left
Definition: kind.h:165
constructor application
Definition: kind.h:189
Macros that should be defined everywhere during the building of the libraries and driver binary...
array table function (internal symbol)
Definition: kind.h:183
greater than or equal, x >= y
Definition: kind.h:121
operator for the bit-vector sign-extend
Definition: kind.h:164
logical and
Definition: kind.h:89
less than or equal, x <= y
Definition: kind.h:119
bit-vector sign-extend
Definition: kind.h:171
defined function application
Definition: kind.h:71
instantiation constant
Definition: kind.h:212
Instantiation pattern list type.
Definition: kind.h:490
Null kind.
Definition: kind.h:62
cast term to integer
Definition: kind.h:123
ints division with interpreted division by 0 (internal symbol)
Definition: kind.h:109
symbolic expression type
Definition: kind.h:83
instantiation pattern
Definition: kind.h:214
regexp concat
Definition: kind.h:233
arithmetic addition
Definition: kind.h:102
String type.
Definition: kind.h:492
sort tag
Definition: kind.h:65
Bound Var type.
Definition: kind.h:488
logical or
Definition: kind.h:92
bitwise and
Definition: kind.h:130
bound variables
Definition: kind.h:213
bit-vector 2's complement signed division
Definition: kind.h:144
equality
Definition: kind.h:72
bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)
Definition: kind.h:142
bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0) ...
Definition: kind.h:147
term is integer
Definition: kind.h:122
Integer type.
Definition: kind.h:487
std::string kindToString(::CVC4::Kind k)
Definition: kind.h:466
parametric datatype
Definition: kind.h:193
a symbolic expression
Definition: kind.h:77
TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
Definition: kind.h:743
operator for a tuple update
Definition: kind.h:200
less than, x < y
Definition: kind.h:118
skolem var
Definition: kind.h:76
tuple select
Definition: kind.h:199
struct CVC4::options::out__option_t out
bit-vector zero-extend
Definition: kind.h:170
Instantiation pattern type.
Definition: kind.h:489
bit-vector left shift
Definition: kind.h:149
operator for a record select
Definition: kind.h:204
cast term to real
Definition: kind.h:124
tuple update
Definition: kind.h:201
size_t operator()(::CVC4::Kind k) const
Definition: kind.h:473
tuple type
Definition: kind.h:196
bit-vector concatenation
Definition: kind.h:129
bit-vector unsigned less than or equal
Definition: kind.h:153
combined cardinality constraint
Definition: kind.h:99
The kind of expressions representing built-in operators.
Definition: kind.h:69
record type
Definition: kind.h:202
a type parameter for type ascription
Definition: kind.h:195
array store
Definition: kind.h:181
operator for the bit-vector boolean bit extract
Definition: kind.h:160
bit-vector conversion to (nonnegative) integer
Definition: kind.h:176
actual deduction rule
Definition: kind.h:221
record update
Definition: kind.h:207
convert string to regexp
Definition: kind.h:232
bit-vector type
Definition: kind.h:127
RegExp type.
Definition: kind.h:493
basic types
Definition: kind.h:81
integer conversion to bit-vector
Definition: kind.h:175
bit-vector unsigned remainder from truncating division (undefined if divisor is 0) ...
Definition: kind.h:143
bitwise not
Definition: kind.h:133
Kind_t
Definition: kind.h:60
equality comparison (returns one bit)
Definition: kind.h:137
bit-vector unsigned greater than or equal
Definition: kind.h:155
We hash the constants with their values.
Definition: kind.h:502
universally quantified formula
Definition: kind.h:210
if-then-else
Definition: kind.h:94
cardinality constraint
Definition: kind.h:98
Real type.
Definition: kind.h:486
bit-vector logical shift right
Definition: kind.h:150