SMTStabilizer API
Public API documentation for SMTStabilizer
Loading...
Searching...
No Matches
Namespaces | Enumerations | Functions | Variables
kind.h File Reference
#include <string>
#include <unordered_map>
#include <unordered_set>
Include dependency graph for kind.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

namespace  stabilizer
 
namespace  stabilizer::parser
 

Enumerations

enum class  stabilizer::parser::State { stabilizer::parser::UNKNOWN = -1 , stabilizer::parser::UNSAT , stabilizer::parser::SAT }
 
enum class  stabilizer::parser::NODE_KIND {
  stabilizer::parser::NT_UNKNOWN = 0 , stabilizer::parser::NT_ERROR , stabilizer::parser::NT_NULL , stabilizer::parser::NT_UF_NAME ,
  stabilizer::parser::NT_PATTERN , stabilizer::parser::NT_NO_PATTERN , stabilizer::parser::NT_WEIGHT , stabilizer::parser::NT_ATTRIBUTE ,
  stabilizer::parser::NT_CONST , stabilizer::parser::NT_VAR , stabilizer::parser::NT_CONST_TRUE , stabilizer::parser::NT_CONST_FALSE ,
  stabilizer::parser::NT_TEMP_VAR , stabilizer::parser::NT_CONST_ARRAY , stabilizer::parser::NT_PLACEHOLDER_VAR , stabilizer::parser::NT_AND ,
  stabilizer::parser::NT_OR , stabilizer::parser::NT_NOT , stabilizer::parser::NT_IMPLIES , stabilizer::parser::NT_XOR ,
  stabilizer::parser::NT_EQ , stabilizer::parser::NT_DISTINCT , stabilizer::parser::NT_ITE , stabilizer::parser::NT_ADD ,
  stabilizer::parser::NT_NEG , stabilizer::parser::NT_SUB , stabilizer::parser::NT_MUL , stabilizer::parser::NT_DT_FUN_APPLY ,
  stabilizer::parser::NT_IAND , stabilizer::parser::NT_POW2 , stabilizer::parser::NT_POW , stabilizer::parser::NT_DIV_INT ,
  stabilizer::parser::NT_DIV_REAL , stabilizer::parser::NT_MOD , stabilizer::parser::NT_ABS , stabilizer::parser::NT_SQRT ,
  stabilizer::parser::NT_SAFESQRT , stabilizer::parser::NT_CEIL , stabilizer::parser::NT_FLOOR , stabilizer::parser::NT_ROUND ,
  stabilizer::parser::NT_EXP , stabilizer::parser::NT_LN , stabilizer::parser::NT_LG , stabilizer::parser::NT_LB ,
  stabilizer::parser::NT_LOG , stabilizer::parser::NT_SIN , stabilizer::parser::NT_COS , stabilizer::parser::NT_TAN ,
  stabilizer::parser::NT_COT , stabilizer::parser::NT_SEC , stabilizer::parser::NT_CSC , stabilizer::parser::NT_ASIN ,
  stabilizer::parser::NT_ACOS , stabilizer::parser::NT_ATAN , stabilizer::parser::NT_ACOT , stabilizer::parser::NT_ASEC ,
  stabilizer::parser::NT_ACSC , stabilizer::parser::NT_SINH , stabilizer::parser::NT_COSH , stabilizer::parser::NT_TANH ,
  stabilizer::parser::NT_ASECH , stabilizer::parser::NT_ACSCH , stabilizer::parser::NT_ACOTH , stabilizer::parser::NT_ATAN2 ,
  stabilizer::parser::NT_ASINH , stabilizer::parser::NT_ACOSH , stabilizer::parser::NT_ATANH , stabilizer::parser::NT_SECH ,
  stabilizer::parser::NT_CSCH , stabilizer::parser::NT_COTH , stabilizer::parser::NT_LE , stabilizer::parser::NT_LT ,
  stabilizer::parser::NT_GE , stabilizer::parser::NT_GT , stabilizer::parser::NT_TO_INT , stabilizer::parser::NT_TO_REAL ,
  stabilizer::parser::NT_IS_INT , stabilizer::parser::NT_IS_DIVISIBLE , stabilizer::parser::NT_IS_PRIME , stabilizer::parser::NT_IS_EVEN ,
  stabilizer::parser::NT_IS_ODD , stabilizer::parser::NT_GCD , stabilizer::parser::NT_LCM , stabilizer::parser::NT_FACT ,
  stabilizer::parser::NT_BV_NOT , stabilizer::parser::NT_BV_NEG , stabilizer::parser::NT_BV_AND , stabilizer::parser::NT_BV_OR ,
  stabilizer::parser::NT_BV_XOR , stabilizer::parser::NT_BV_NAND , stabilizer::parser::NT_BV_NOR , stabilizer::parser::NT_BV_XNOR ,
  stabilizer::parser::NT_BV_COMP , stabilizer::parser::NT_BV_ADD , stabilizer::parser::NT_BV_SUB , stabilizer::parser::NT_BV_MUL ,
  stabilizer::parser::NT_BV_UDIV , stabilizer::parser::NT_BV_SDIV , stabilizer::parser::NT_BV_UREM , stabilizer::parser::NT_BV_SREM ,
  stabilizer::parser::NT_BV_UMOD , stabilizer::parser::NT_BV_SMOD , stabilizer::parser::NT_BV_SHL , stabilizer::parser::NT_BV_LSHR ,
  stabilizer::parser::NT_BV_ASHR , stabilizer::parser::NT_BV_ULT , stabilizer::parser::NT_BV_ULE , stabilizer::parser::NT_BV_UGT ,
  stabilizer::parser::NT_BV_UGE , stabilizer::parser::NT_BV_SLT , stabilizer::parser::NT_BV_SLE , stabilizer::parser::NT_BV_SGT ,
  stabilizer::parser::NT_BV_SGE , stabilizer::parser::NT_BV_CONCAT , stabilizer::parser::NT_BV_TO_NAT , stabilizer::parser::NT_NAT_TO_BV ,
  stabilizer::parser::NT_BV_TO_INT , stabilizer::parser::NT_INT_TO_BV , stabilizer::parser::NT_UBV_TO_INT , stabilizer::parser::NT_SBV_TO_INT ,
  stabilizer::parser::NT_BV_EXTRACT , stabilizer::parser::NT_BV_REPEAT , stabilizer::parser::NT_BV_ZERO_EXT , stabilizer::parser::NT_BV_SIGN_EXT ,
  stabilizer::parser::NT_BV_ROTATE_LEFT , stabilizer::parser::NT_BV_ROTATE_RIGHT , stabilizer::parser::NT_FP_ADD , stabilizer::parser::NT_FP_SUB ,
  stabilizer::parser::NT_FP_MUL , stabilizer::parser::NT_FP_DIV , stabilizer::parser::NT_FP_ABS , stabilizer::parser::NT_FP_NEG ,
  stabilizer::parser::NT_FP_REM , stabilizer::parser::NT_FP_FMA , stabilizer::parser::NT_FP_SQRT , stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL ,
  stabilizer::parser::NT_FP_MIN , stabilizer::parser::NT_FP_MAX , stabilizer::parser::NT_FP_LE , stabilizer::parser::NT_FP_LT ,
  stabilizer::parser::NT_FP_GE , stabilizer::parser::NT_FP_GT , stabilizer::parser::NT_FP_EQ , stabilizer::parser::NT_FP_TO_UBV ,
  stabilizer::parser::NT_FP_TO_SBV , stabilizer::parser::NT_FP_TO_REAL , stabilizer::parser::NT_FP_TO_FP , stabilizer::parser::NT_FP_TO_FP_UNSIGNED ,
  stabilizer::parser::NT_FP_IS_NORMAL , stabilizer::parser::NT_FP_IS_SUBNORMAL , stabilizer::parser::NT_FP_IS_ZERO , stabilizer::parser::NT_FP_IS_INF ,
  stabilizer::parser::NT_FP_IS_NAN , stabilizer::parser::NT_FP_IS_NEG , stabilizer::parser::NT_FP_IS_POS , stabilizer::parser::NT_SELECT ,
  stabilizer::parser::NT_STORE , stabilizer::parser::NT_DT_TESTER , stabilizer::parser::NT_DT_UPDATER , stabilizer::parser::NT_TUPLE_CONSTRUCTOR ,
  stabilizer::parser::NT_TUPLE_UNIT , stabilizer::parser::NT_TUPLE_SELECT , stabilizer::parser::NT_TUPLE_UPDATE , stabilizer::parser::NT_TUPLE_PROJECT ,
  stabilizer::parser::NT_STR_LEN , stabilizer::parser::NT_STR_CONCAT , stabilizer::parser::NT_STR_SUBSTR , stabilizer::parser::NT_STR_INDEXOF ,
  stabilizer::parser::NT_STR_CHARAT , stabilizer::parser::NT_STR_UPDATE , stabilizer::parser::NT_STR_REPLACE , stabilizer::parser::NT_STR_REPLACE_ALL ,
  stabilizer::parser::NT_STR_REPLACE_REG , stabilizer::parser::NT_STR_REPLACE_REG_ALL , stabilizer::parser::NT_STR_INDEXOF_REG , stabilizer::parser::NT_STR_TO_LOWER ,
  stabilizer::parser::NT_STR_TO_UPPER , stabilizer::parser::NT_STR_REV , stabilizer::parser::NT_STR_SPLIT , stabilizer::parser::NT_STR_SPLIT_AT ,
  stabilizer::parser::NT_STR_SPLIT_REST , stabilizer::parser::NT_STR_NUM_SPLITS , stabilizer::parser::NT_STR_SPLIT_AT_RE , stabilizer::parser::NT_STR_SPLIT_REST_RE ,
  stabilizer::parser::NT_STR_NUM_SPLITS_RE , stabilizer::parser::NT_STR_LT , stabilizer::parser::NT_STR_LE , stabilizer::parser::NT_STR_GT ,
  stabilizer::parser::NT_STR_GE , stabilizer::parser::NT_STR_IN_REG , stabilizer::parser::NT_STR_CONTAINS , stabilizer::parser::NT_STR_IS_DIGIT ,
  stabilizer::parser::NT_STR_PREFIXOF , stabilizer::parser::NT_STR_SUFFIXOF , stabilizer::parser::NT_STR_FROM_INT , stabilizer::parser::NT_STR_TO_INT ,
  stabilizer::parser::NT_STR_TO_REG , stabilizer::parser::NT_STR_TO_CODE , stabilizer::parser::NT_STR_FROM_CODE , stabilizer::parser::NT_REG_CONCAT ,
  stabilizer::parser::NT_REG_UNION , stabilizer::parser::NT_REG_INTER , stabilizer::parser::NT_REG_DIFF , stabilizer::parser::NT_REG_STAR ,
  stabilizer::parser::NT_REG_PLUS , stabilizer::parser::NT_REG_OPT , stabilizer::parser::NT_REG_RANGE , stabilizer::parser::NT_REG_REPEAT ,
  stabilizer::parser::NT_REG_COMPLEMENT , stabilizer::parser::NT_REG_LOOP , stabilizer::parser::NT_FUNC_APPLY , stabilizer::parser::NT_FUNC_DEC ,
  stabilizer::parser::NT_FUNC_DEF , stabilizer::parser::NT_FUNC_REC , stabilizer::parser::NT_FUNC_REC_APPLY , stabilizer::parser::NT_BV_NEGO ,
  stabilizer::parser::NT_BV_UADDO , stabilizer::parser::NT_BV_SADDO , stabilizer::parser::NT_BV_UMULO , stabilizer::parser::NT_BV_SMULO ,
  stabilizer::parser::NT_BV_UDIVO , stabilizer::parser::NT_BV_SDIVO , stabilizer::parser::NT_BV_UREMO , stabilizer::parser::NT_BV_SREMO ,
  stabilizer::parser::NT_BV_UMODO , stabilizer::parser::NT_BV_SMODO , stabilizer::parser::NT_EQ_BOOL , stabilizer::parser::NT_EQ_OTHER ,
  stabilizer::parser::NT_DISTINCT_BOOL , stabilizer::parser::NT_DISTINCT_OTHER , stabilizer::parser::NT_UF_APPLY , stabilizer::parser::NT_CONST_PI ,
  stabilizer::parser::NT_CONST_E , stabilizer::parser::NT_INFINITY , stabilizer::parser::NT_NAN , stabilizer::parser::NT_EPSILON ,
  stabilizer::parser::NT_POS_INFINITY , stabilizer::parser::NT_NEG_INFINITY , stabilizer::parser::NT_POS_EPSILON , stabilizer::parser::NT_NEG_EPSILON ,
  stabilizer::parser::NT_REG_NONE , stabilizer::parser::NT_REG_ALL , stabilizer::parser::NT_REG_ALLCHAR , stabilizer::parser::NT_MAX ,
  stabilizer::parser::NT_MIN , stabilizer::parser::NT_LET , stabilizer::parser::NT_LET_CHAIN , stabilizer::parser::NT_LET_BIND_VAR ,
  stabilizer::parser::NT_LET_BIND_VAR_LIST , stabilizer::parser::NT_FORALL , stabilizer::parser::NT_EXISTS , stabilizer::parser::NT_QUANT_VAR ,
  stabilizer::parser::NT_FUNC_PARAM , stabilizer::parser::NT_ROOT_OBJ , stabilizer::parser::NT_ROOT_OF_WITH_INTERVAL , stabilizer::parser::NUM_KINDS
}
 

Functions

std::string stabilizer::parser::kindToString (const NODE_KIND &nk)
 
NODE_KIND stabilizer::parser::getFlipKind (const NODE_KIND &nk)
 
NODE_KIND stabilizer::parser::getNegatedKind (const NODE_KIND &nk)
 
NODE_KIND stabilizer::parser::getOperKind (const std::string &s)
 

Variables

constexpr size_t stabilizer::parser::NUM_KINDS = static_cast<size_t>(NODE_KIND::NUM_KINDS)
 
const std::unordered_set< NODE_KIND > stabilizer::parser::static_kinds
 
const std::string stabilizer::parser::PRESERVING_LET_BIND_VAR_SUFFIX
 
const std::unordered_map< std::string, NODE_KIND > stabilizer::parser::kind_key_map
 
const std::unordered_map< std::string, NODE_KIND > stabilizer::parser::oper_key_map