cvc4-1.4
Data Structures | Namespaces | Typedefs | Enumerations | Functions | Variables
kind.h File Reference

kind.h More...

#include "cvc4_public.h"
#include <iostream>
#include <sstream>
#include "util/exception.h"

Go to the source code of this file.

Data Structures

struct  CVC4::kind::KindHashFunction
 
struct  CVC4::TypeConstantHashFunction
 We hash the constants with their values. More...
 

Namespaces

 CVC4
 
 CVC4::kind
 
 CVC4::theory
 

Typedefs

typedef ::CVC4::kind::Kind_t CVC4::Kind
 

Enumerations

enum  CVC4::kind::Kind_t {
  CVC4::kind::UNDEFINED_KIND, CVC4::kind::NULL_EXPR, CVC4::kind::SORT_TAG, CVC4::kind::SORT_TYPE,
  CVC4::kind::UNINTERPRETED_CONSTANT, CVC4::kind::ABSTRACT_VALUE, CVC4::kind::BUILTIN, CVC4::kind::FUNCTION,
  CVC4::kind::APPLY, CVC4::kind::EQUAL, CVC4::kind::DISTINCT, CVC4::kind::VARIABLE,
  CVC4::kind::BOUND_VARIABLE, CVC4::kind::SKOLEM, CVC4::kind::SEXPR, CVC4::kind::LAMBDA,
  CVC4::kind::CHAIN, CVC4::kind::CHAIN_OP, CVC4::kind::TYPE_CONSTANT, CVC4::kind::FUNCTION_TYPE,
  CVC4::kind::SEXPR_TYPE, CVC4::kind::SUBTYPE_TYPE, CVC4::kind::CONST_BOOLEAN, CVC4::kind::NOT,
  CVC4::kind::AND, CVC4::kind::IFF, CVC4::kind::IMPLIES, CVC4::kind::OR,
  CVC4::kind::XOR, CVC4::kind::ITE, CVC4::kind::APPLY_UF, CVC4::kind::CARDINALITY_CONSTRAINT,
  CVC4::kind::COMBINED_CARDINALITY_CONSTRAINT, CVC4::kind::PLUS, CVC4::kind::MULT, CVC4::kind::MINUS,
  CVC4::kind::UMINUS, CVC4::kind::DIVISION, CVC4::kind::DIVISION_TOTAL, CVC4::kind::INTS_DIVISION,
  CVC4::kind::INTS_DIVISION_TOTAL, CVC4::kind::INTS_MODULUS, CVC4::kind::INTS_MODULUS_TOTAL, CVC4::kind::ABS,
  CVC4::kind::DIVISIBLE, CVC4::kind::POW, CVC4::kind::DIVISIBLE_OP, CVC4::kind::SUBRANGE_TYPE,
  CVC4::kind::CONST_RATIONAL, CVC4::kind::LT, CVC4::kind::LEQ, CVC4::kind::GT,
  CVC4::kind::GEQ, CVC4::kind::IS_INTEGER, CVC4::kind::TO_INTEGER, CVC4::kind::TO_REAL,
  CVC4::kind::BITVECTOR_TYPE, CVC4::kind::CONST_BITVECTOR, CVC4::kind::BITVECTOR_CONCAT, CVC4::kind::BITVECTOR_AND,
  CVC4::kind::BITVECTOR_OR, CVC4::kind::BITVECTOR_XOR, CVC4::kind::BITVECTOR_NOT, CVC4::kind::BITVECTOR_NAND,
  CVC4::kind::BITVECTOR_NOR, CVC4::kind::BITVECTOR_XNOR, CVC4::kind::BITVECTOR_COMP, CVC4::kind::BITVECTOR_MULT,
  CVC4::kind::BITVECTOR_PLUS, CVC4::kind::BITVECTOR_SUB, CVC4::kind::BITVECTOR_NEG, CVC4::kind::BITVECTOR_UDIV,
  CVC4::kind::BITVECTOR_UREM, CVC4::kind::BITVECTOR_SDIV, CVC4::kind::BITVECTOR_SREM, CVC4::kind::BITVECTOR_SMOD,
  CVC4::kind::BITVECTOR_UDIV_TOTAL, CVC4::kind::BITVECTOR_UREM_TOTAL, CVC4::kind::BITVECTOR_SHL, CVC4::kind::BITVECTOR_LSHR,
  CVC4::kind::BITVECTOR_ASHR, CVC4::kind::BITVECTOR_ULT, CVC4::kind::BITVECTOR_ULE, CVC4::kind::BITVECTOR_UGT,
  CVC4::kind::BITVECTOR_UGE, CVC4::kind::BITVECTOR_SLT, CVC4::kind::BITVECTOR_SLE, CVC4::kind::BITVECTOR_SGT,
  CVC4::kind::BITVECTOR_SGE, CVC4::kind::BITVECTOR_EAGER_ATOM, CVC4::kind::BITVECTOR_ACKERMANIZE_UDIV, CVC4::kind::BITVECTOR_ACKERMANIZE_UREM,
  CVC4::kind::BITVECTOR_BITOF_OP, CVC4::kind::BITVECTOR_EXTRACT_OP, CVC4::kind::BITVECTOR_REPEAT_OP, CVC4::kind::BITVECTOR_ZERO_EXTEND_OP,
  CVC4::kind::BITVECTOR_SIGN_EXTEND_OP, CVC4::kind::BITVECTOR_ROTATE_LEFT_OP, CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP, CVC4::kind::BITVECTOR_BITOF,
  CVC4::kind::BITVECTOR_EXTRACT, CVC4::kind::BITVECTOR_REPEAT, CVC4::kind::BITVECTOR_ZERO_EXTEND, CVC4::kind::BITVECTOR_SIGN_EXTEND,
  CVC4::kind::BITVECTOR_ROTATE_LEFT, CVC4::kind::BITVECTOR_ROTATE_RIGHT, CVC4::kind::INT_TO_BITVECTOR_OP, CVC4::kind::INT_TO_BITVECTOR,
  CVC4::kind::BITVECTOR_TO_NAT, CVC4::kind::ARRAY_TYPE, CVC4::kind::SELECT, CVC4::kind::STORE,
  CVC4::kind::STORE_ALL, CVC4::kind::ARR_TABLE_FUN, CVC4::kind::ARRAY_LAMBDA, CVC4::kind::CONSTRUCTOR_TYPE,
  CVC4::kind::SELECTOR_TYPE, CVC4::kind::TESTER_TYPE, CVC4::kind::APPLY_CONSTRUCTOR, CVC4::kind::APPLY_SELECTOR,
  CVC4::kind::APPLY_SELECTOR_TOTAL, CVC4::kind::APPLY_TESTER, CVC4::kind::DATATYPE_TYPE, CVC4::kind::PARAMETRIC_DATATYPE,
  CVC4::kind::APPLY_TYPE_ASCRIPTION, CVC4::kind::ASCRIPTION_TYPE, CVC4::kind::TUPLE_TYPE, CVC4::kind::TUPLE,
  CVC4::kind::TUPLE_SELECT_OP, CVC4::kind::TUPLE_SELECT, CVC4::kind::TUPLE_UPDATE_OP, CVC4::kind::TUPLE_UPDATE,
  CVC4::kind::RECORD_TYPE, CVC4::kind::RECORD, CVC4::kind::RECORD_SELECT_OP, CVC4::kind::RECORD_SELECT,
  CVC4::kind::RECORD_UPDATE_OP, CVC4::kind::RECORD_UPDATE, CVC4::kind::EMPTYSET, CVC4::kind::SET_TYPE,
  CVC4::kind::UNION, CVC4::kind::INTERSECTION, CVC4::kind::SETMINUS, CVC4::kind::SUBSET,
  CVC4::kind::MEMBER, CVC4::kind::SINGLETON, CVC4::kind::INSERT, CVC4::kind::STRING_CONCAT,
  CVC4::kind::STRING_IN_REGEXP, CVC4::kind::STRING_LENGTH, CVC4::kind::STRING_SUBSTR, CVC4::kind::STRING_SUBSTR_TOTAL,
  CVC4::kind::STRING_CHARAT, CVC4::kind::STRING_STRCTN, CVC4::kind::STRING_STRIDOF, CVC4::kind::STRING_STRREPL,
  CVC4::kind::STRING_PREFIX, CVC4::kind::STRING_SUFFIX, CVC4::kind::STRING_ITOS, CVC4::kind::STRING_STOI,
  CVC4::kind::STRING_U16TOS, CVC4::kind::STRING_STOU16, CVC4::kind::STRING_U32TOS, CVC4::kind::STRING_STOU32,
  CVC4::kind::CONST_STRING, CVC4::kind::CONST_REGEXP, CVC4::kind::STRING_TO_REGEXP, CVC4::kind::REGEXP_CONCAT,
  CVC4::kind::REGEXP_UNION, CVC4::kind::REGEXP_INTER, CVC4::kind::REGEXP_STAR, CVC4::kind::REGEXP_PLUS,
  CVC4::kind::REGEXP_OPT, CVC4::kind::REGEXP_RANGE, CVC4::kind::REGEXP_LOOP, CVC4::kind::REGEXP_EMPTY,
  CVC4::kind::REGEXP_SIGMA, CVC4::kind::FORALL, CVC4::kind::EXISTS, CVC4::kind::INST_CONSTANT,
  CVC4::kind::BOUND_VAR_LIST, CVC4::kind::INST_PATTERN, CVC4::kind::INST_PATTERN_LIST, CVC4::kind::REWRITE_RULE,
  CVC4::kind::RR_REWRITE, CVC4::kind::RR_REDUCTION, CVC4::kind::RR_DEDUCTION, CVC4::kind::LAST_KIND
}
 
enum  CVC4::TypeConstant {
  CVC4::BUILTIN_OPERATOR_TYPE, CVC4::BOOLEAN_TYPE, CVC4::REAL_TYPE, CVC4::INTEGER_TYPE,
  CVC4::STRING_TYPE, CVC4::REGEXP_TYPE, CVC4::BOUND_VAR_LIST_TYPE, CVC4::INST_PATTERN_TYPE,
  CVC4::INST_PATTERN_LIST_TYPE, CVC4::RRHB_TYPE, CVC4::LAST_TYPE
}
 The enumeration for the built-in atomic types. More...
 
enum  CVC4::theory::TheoryId {
  CVC4::theory::THEORY_BUILTIN, CVC4::theory::THEORY_BOOL, CVC4::theory::THEORY_UF, CVC4::theory::THEORY_ARITH,
  CVC4::theory::THEORY_BV, CVC4::theory::THEORY_ARRAY, CVC4::theory::THEORY_DATATYPES, CVC4::theory::THEORY_SETS,
  CVC4::theory::THEORY_STRINGS, CVC4::theory::THEORY_QUANTIFIERS, CVC4::theory::THEORY_LAST
}
 

Functions

std::ostream & CVC4::kind::operator<< (std::ostream &, CVC4::Kind)
 
bool CVC4::kind::isAssociative (::CVC4::Kind k)
 Returns true if the given kind is associative. More...
 
std::string CVC4::kind::kindToString (::CVC4::Kind k)
 
std::ostream & CVC4::operator<< (std::ostream &out, TypeConstant typeConstant)
 
TheoryId & CVC4::theory::operator++ (TheoryId &id)
 
std::ostream & CVC4::theory::operator<< (std::ostream &out, TheoryId theoryId)
 
TheoryId CVC4::theory::kindToTheoryId (::CVC4::Kind k)
 
TheoryId CVC4::theory::typeConstantToTheoryId (::CVC4::TypeConstant typeConstant)
 

Variables

const TheoryId CVC4::theory::THEORY_FIRST
 
const TheoryId CVC4::theory::THEORY_SAT_SOLVER
 

Detailed Description

kind.h

Copyright 2010-2014 New York University and The University of Iowa, and as below.

This header file automatically generated by: 

/builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/expr/mkkind /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/uf/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/quantifiers/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/idl/kinds

for the CVC4 project.

** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014  New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.

Template for the Node kind header

Template for the Node kind header.

Definition in file kind.h.