- Generated by
1.9.8
|
SMTStabilizer API
Public API documentation for SMTStabilizer
|
Classes | |
| class | BitVectorUtils |
| Bitvector conversion and arithmetic helpers on SMT bitstring forms. More... | |
| class | ConversionUtils |
| Conversion and escaping helpers for parser I/O and literals. More... | |
| class | DAGNode |
| struct | ExprFrame |
| class | FloatingPointUtils |
| Floating-point conversion helpers used by parser evaluation paths. More... | |
| class | GlobalOptions |
| class | HighPrecisionInteger |
| class | HighPrecisionReal |
| class | Interval |
| struct | LetContext |
| class | MathUtils |
| Numeric helper wrappers shared by parser-side evaluation and rewrite. More... | |
| struct | NodeEqual |
| struct | NodeHash |
| class | NodeManager |
| class | Number |
| struct | PairNodePtrEqual |
| struct | PairNodePtrHash |
| class | Parser |
| class | Sort |
| class | SortManager |
| class | StringUtils |
| String theory helper functions for SMT string operators. More... | |
| class | TypeChecker |
| Lexical classifiers for SMT-LIB literals and token shapes. More... | |
| class | Value |
Typedefs | |
| typedef std::shared_ptr< DAGNode > | NodePtr |
| typedef HighPrecisionInteger | Integer |
| typedef HighPrecisionReal | Real |
| typedef std::shared_ptr< Parser > | ParserPtr |
| typedef std::shared_ptr< Sort > | SortPtr |
| typedef std::shared_ptr< SortManager > | SortManagerPtr |
Functions | |
| char * | safe_strdup (const std::string &str) |
| ParserPtr | newParser () |
| ParserPtr | newParser (const std::string &filename) |
| std::string | dumpConst (const std::string &name, const std::shared_ptr< Sort > &sort) |
| void | dumpSMTLIB2_streaming (const std::shared_ptr< DAGNode > &root, std::ostream &out) |
| std::string | dumpSMTLIB2 (const std::shared_ptr< DAGNode > &root) |
| std::string | dumpFuncDef (const std::shared_ptr< DAGNode > &node) |
| std::string | dumpFuncRec (const std::shared_ptr< DAGNode > &node) |
| std::string | dumpFuncDec (const std::shared_ptr< DAGNode > &node) |
| std::string | kindToString (const NODE_KIND &nk) |
| NODE_KIND | getNegatedKind (const NODE_KIND &nk) |
| NODE_KIND | getFlipKind (const NODE_KIND &nk) |
| NODE_KIND | getOperKind (const std::string &s) |
| bool | isIntParam (std::shared_ptr< DAGNode > param) |
| bool | isRealParam (std::shared_ptr< DAGNode > param) |
| bool | isBoolParam (std::shared_ptr< DAGNode > param) |
| bool | isBvParam (std::shared_ptr< DAGNode > param) |
| bool | isFpParam (std::shared_ptr< DAGNode > param) |
| bool | isStrParam (std::shared_ptr< DAGNode > param) |
| bool | isRegParam (std::shared_ptr< DAGNode > param) |
| bool | isArrayParam (std::shared_ptr< DAGNode > param) |
| bool | canExempt (std::shared_ptr< Sort > l, std::shared_ptr< Sort > r) |
| void | echo_error (const std::string &msg) |
| std::string | hexToBv (const std::string &hex) |
| std::string | decToBv (const std::string &dec) |
| std::shared_ptr< Value > | newValue (const std::string &string_value) |
| std::shared_ptr< Value > | newValue (const Number &number_value) |
| std::shared_ptr< Value > | newValue (const Interval &interval_value) |
| std::shared_ptr< Value > | newValue (const bool &boolean_value) |
| std::shared_ptr< Value > | newValue (const ValueType &value_type) |
| std::shared_ptr< Value > | newValue (const int &integer_value) |
| std::shared_ptr< Value > | newValue (const double &double_value) |
| std::shared_ptr< Value > | newValue (const float &float_value) |
| std::shared_ptr< Value > | newValue (const long &long_value) |
| std::shared_ptr< Value > | newValue (const short &short_value) |
| std::shared_ptr< Value > | newValue (const char &char_value) |
Variables | |
| Interval | EmptyInterval = Interval(1, -1, false, false) |
| Interval | FullInterval |
| constexpr size_t | NUM_KINDS = static_cast<size_t>(NODE_KIND::NUM_KINDS) |
| const std::unordered_set< NODE_KIND > | static_kinds |
| const std::string | PRESERVING_LET_BIND_VAR_SUFFIX |
| const std::unordered_map< std::string, NODE_KIND > | kind_key_map |
| const std::unordered_map< std::string, NODE_KIND > | oper_key_map |
| typedef std::shared_ptr<DAGNode> stabilizer::parser::NodePtr |
| typedef std::shared_ptr<Parser> stabilizer::parser::ParserPtr |
| typedef std::shared_ptr<SortManager> stabilizer::parser::SortManagerPtr |
| typedef std::shared_ptr<Sort> stabilizer::parser::SortPtr |
|
strong |
|
strong |
|
strong |
| Enumerator | |
|---|---|
| Start | |
| ReadingHead | |
| ProcessingSpecial | |
| ProcessingParams | |
| ProcessingBindings | |
| ProcessingLetBody | |
| ProcessingQuantVars | |
| ProcessingQuantBody | |
| ProcessingParamFuncArgs | |
| ProcessingParamFuncParams | |
| Finish | |
Definition at line 41 of file expr_parser.cpp.
|
strong |
|
strong |
|
strong |
|
strong |
|
strong |
|
strong |
|
strong |
| Enumerator | |
|---|---|
| None | |
| Let | |
| Exists | |
| Forall | |
| ParamFunc | |
| BV | |
| Underscore | |
Definition at line 56 of file expr_parser.cpp.
|
strong |
Definition at line 124 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkAdd(), stabilizer::parser::Parser::mkDistinct(), stabilizer::parser::Parser::mkEq(), stabilizer::parser::Parser::mkIand(), stabilizer::parser::Parser::mkLog(), stabilizer::parser::Parser::mkMax(), stabilizer::parser::Parser::mkMin(), stabilizer::parser::Parser::mkMul(), and stabilizer::parser::Parser::mkSub().
| std::string stabilizer::parser::decToBv | ( | const std::string & | dec | ) |
Definition at line 820 of file util.cpp.
References stabilizer::parser::HighPrecisionInteger::toString().
Referenced by stabilizer::parser::BitVectorUtils::natToBv().
| std::string stabilizer::parser::dumpConst | ( | const std::string & | name, |
| const std::shared_ptr< Sort > & | sort | ||
| ) |
Definition at line 69 of file dag.cpp.
Referenced by dumpSMTLIB2_streaming().
| std::string stabilizer::parser::dumpFuncDec | ( | const std::shared_ptr< DAGNode > & | node | ) |
Definition at line 1043 of file dag.cpp.
Referenced by stabilizer::parser::Parser::dumpSMT2().
| std::string stabilizer::parser::dumpFuncDef | ( | const std::shared_ptr< DAGNode > & | node | ) |
Definition at line 1009 of file dag.cpp.
References dumpSMTLIB2().
| std::string stabilizer::parser::dumpFuncRec | ( | const std::shared_ptr< DAGNode > & | node | ) |
Definition at line 1026 of file dag.cpp.
References dumpSMTLIB2().
Referenced by stabilizer::parser::Parser::dumpSMT2().
| std::string stabilizer::parser::dumpSMTLIB2 | ( | const std::shared_ptr< DAGNode > & | root | ) |
Definition at line 1003 of file dag.cpp.
References dumpSMTLIB2_streaming().
Referenced by dumpFuncDef(), dumpFuncRec(), stabilizer::parser::Parser::dumpSMT2(), and stabilizer::parser::Parser::toString().
| void stabilizer::parser::dumpSMTLIB2_streaming | ( | const std::shared_ptr< DAGNode > & | root, |
| std::ostream & | out | ||
| ) |
Definition at line 111 of file dag.cpp.
References condAssert, dumpConst(), stabilizer::parser::DAGNode::getChild(), stabilizer::parser::DAGNode::getChildren(), stabilizer::parser::DAGNode::getChildrenSize(), stabilizer::parser::DAGNode::getKind(), stabilizer::parser::DAGNode::getName(), stabilizer::parser::DAGNode::getPureName(), stabilizer::parser::DAGNode::getSort(), kindToString(), NT_ADD, NT_AND, NT_ATTRIBUTE, NT_BV_EXTRACT, NT_BV_REPEAT, NT_BV_ROTATE_LEFT, NT_BV_ROTATE_RIGHT, NT_BV_SIGN_EXT, NT_BV_ZERO_EXT, NT_CONST, NT_CONST_ARRAY, NT_CONST_E, NT_CONST_FALSE, NT_CONST_PI, NT_CONST_TRUE, NT_DISTINCT, NT_DIV_REAL, NT_DT_FUN_APPLY, NT_DT_TESTER, NT_DT_UPDATER, NT_EPSILON, NT_EQ, NT_EXISTS, NT_FORALL, NT_FP_ABS, NT_FP_ADD, NT_FP_DIV, NT_FP_EQ, NT_FP_FMA, NT_FP_GE, NT_FP_GT, NT_FP_IS_INF, NT_FP_IS_NAN, NT_FP_IS_NEG, NT_FP_IS_NORMAL, NT_FP_IS_POS, NT_FP_IS_SUBNORMAL, NT_FP_IS_ZERO, NT_FP_LE, NT_FP_LT, NT_FP_MAX, NT_FP_MIN, NT_FP_MUL, NT_FP_NEG, NT_FP_REM, NT_FP_ROUND_TO_INTEGRAL, NT_FP_SQRT, NT_FP_SUB, NT_FP_TO_FP, NT_FP_TO_FP_UNSIGNED, NT_FP_TO_REAL, NT_FP_TO_SBV, NT_FP_TO_UBV, NT_FUNC_APPLY, NT_FUNC_DEC, NT_FUNC_DEF, NT_FUNC_PARAM, NT_FUNC_REC, NT_FUNC_REC_APPLY, NT_GE, NT_GT, NT_IMPLIES, NT_INFINITY, NT_INT_TO_BV, NT_ITE, NT_LE, NT_LET, NT_LET_BIND_VAR, NT_LET_BIND_VAR_LIST, NT_LET_CHAIN, NT_LT, NT_MUL, NT_NAN, NT_NEG, NT_NEG_EPSILON, NT_NEG_INFINITY, NT_NO_PATTERN, NT_NOT, NT_OR, NT_PATTERN, NT_PLACEHOLDER_VAR, NT_POS_EPSILON, NT_POS_INFINITY, NT_QUANT_VAR, NT_REG_ALL, NT_REG_ALLCHAR, NT_REG_LOOP, NT_REG_NONE, NT_ROOT_OBJ, NT_ROOT_OF_WITH_INTERVAL, NT_SUB, NT_TEMP_VAR, NT_TUPLE_CONSTRUCTOR, NT_TUPLE_PROJECT, NT_TUPLE_SELECT, NT_TUPLE_UNIT, NT_TUPLE_UPDATE, NT_UF_APPLY, NT_VAR, NT_WEIGHT, and NT_XOR.
Referenced by dumpSMTLIB2().
| void stabilizer::parser::echo_error | ( | const std::string & | msg | ) |
Definition at line 35 of file rewrite_parser.cpp.
Referenced by stabilizer::parser::Parser::rewrite(), stabilizer::parser::Parser::rewrite(), stabilizer::parser::Parser::rewrite(), and stabilizer::parser::Parser::rewrite().
Definition at line 635 of file kind.cpp.
References NT_ADD, NT_BV_ADD, NT_BV_MUL, NT_BV_SDIV, NT_BV_SGE, NT_BV_SGT, NT_BV_SLE, NT_BV_SLT, NT_BV_SUB, NT_BV_UDIV, NT_BV_UGE, NT_BV_UGT, NT_BV_ULE, NT_BV_ULT, NT_DISTINCT, NT_DISTINCT_BOOL, NT_DISTINCT_OTHER, NT_DIV_INT, NT_DIV_REAL, NT_EQ, NT_EQ_BOOL, NT_EQ_OTHER, NT_FP_ADD, NT_FP_DIV, NT_FP_GE, NT_FP_GT, NT_FP_LE, NT_FP_LT, NT_FP_MUL, NT_FP_SUB, NT_GE, NT_GT, NT_LE, NT_LT, NT_MUL, NT_STR_GE, NT_STR_GT, NT_STR_LE, NT_STR_LT, NT_SUB, and NT_UNKNOWN.
Definition at line 577 of file kind.cpp.
References NT_BV_SGE, NT_BV_SGT, NT_BV_SLE, NT_BV_SLT, NT_BV_UGE, NT_BV_UGT, NT_BV_ULE, NT_BV_ULT, NT_DISTINCT, NT_DISTINCT_BOOL, NT_DISTINCT_OTHER, NT_EQ, NT_EQ_BOOL, NT_EQ_OTHER, NT_FP_GE, NT_FP_GT, NT_FP_LE, NT_FP_LT, NT_GE, NT_GT, NT_LE, NT_LT, NT_STR_GE, NT_STR_GT, NT_STR_LE, NT_STR_LT, and NT_UNKNOWN.
Referenced by stabilizer::parser::Parser::getNegatedKind().
| NODE_KIND stabilizer::parser::getOperKind | ( | const std::string & | s | ) |
Definition at line 718 of file kind.cpp.
References NT_UNKNOWN, and oper_key_map.
Referenced by stabilizer::parser::Parser::getKind(), and stabilizer::parser::Parser::parseOper().
| std::string stabilizer::parser::hexToBv | ( | const std::string & | hex | ) |
Definition at line 744 of file util.cpp.
References condAssert.
Referenced by stabilizer::parser::BitVectorUtils::natToBv().
| bool stabilizer::parser::isArrayParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 72 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkSelect().
| bool stabilizer::parser::isBoolParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 52 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkAnd(), stabilizer::parser::Parser::mkNot(), and stabilizer::parser::Parser::mkOr().
| bool stabilizer::parser::isBvParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 56 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkBvAdd(), stabilizer::parser::Parser::mkBvAnd(), stabilizer::parser::Parser::mkBvAshr(), stabilizer::parser::Parser::mkBvConcat(), stabilizer::parser::Parser::mkBvExtract(), stabilizer::parser::Parser::mkBvLshr(), stabilizer::parser::Parser::mkBvMul(), stabilizer::parser::Parser::mkBvNot(), stabilizer::parser::Parser::mkBvOr(), stabilizer::parser::Parser::mkBvRepeat(), stabilizer::parser::Parser::mkBvRotateLeft(), stabilizer::parser::Parser::mkBvRotateRight(), stabilizer::parser::Parser::mkBvSdiv(), stabilizer::parser::Parser::mkBvSge(), stabilizer::parser::Parser::mkBvSgt(), stabilizer::parser::Parser::mkBvShl(), stabilizer::parser::Parser::mkBvSignExt(), stabilizer::parser::Parser::mkBvSle(), stabilizer::parser::Parser::mkBvSlt(), stabilizer::parser::Parser::mkBvSmod(), stabilizer::parser::Parser::mkBvSrem(), stabilizer::parser::Parser::mkBvToInt(), stabilizer::parser::Parser::mkBvToNat(), stabilizer::parser::Parser::mkBvUdiv(), stabilizer::parser::Parser::mkBvUge(), stabilizer::parser::Parser::mkBvUgt(), stabilizer::parser::Parser::mkBvUle(), stabilizer::parser::Parser::mkBvUlt(), stabilizer::parser::Parser::mkBvUmod(), stabilizer::parser::Parser::mkBvUrem(), stabilizer::parser::Parser::mkBvXor(), stabilizer::parser::Parser::mkBvZeroExt(), stabilizer::parser::Parser::mkFpConst(), stabilizer::parser::Parser::mkSbvToInt(), stabilizer::parser::Parser::mkToFp(), stabilizer::parser::Parser::mkToFp(), stabilizer::parser::Parser::mkToFpUnsigned(), and stabilizer::parser::Parser::mkUbvToInt().
| bool stabilizer::parser::isFpParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 60 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkFpAbs(), stabilizer::parser::Parser::mkFpAdd(), stabilizer::parser::Parser::mkFpDiv(), stabilizer::parser::Parser::mkFpFma(), stabilizer::parser::Parser::mkFpIsInf(), stabilizer::parser::Parser::mkFpIsNaN(), stabilizer::parser::Parser::mkFpIsNeg(), stabilizer::parser::Parser::mkFpIsNormal(), stabilizer::parser::Parser::mkFpIsPos(), stabilizer::parser::Parser::mkFpIsSubnormal(), stabilizer::parser::Parser::mkFpIsZero(), stabilizer::parser::Parser::mkFpMul(), stabilizer::parser::Parser::mkFpNeg(), stabilizer::parser::Parser::mkFpRem(), stabilizer::parser::Parser::mkFpRoundToIntegral(), stabilizer::parser::Parser::mkFpRoundToIntegral(), stabilizer::parser::Parser::mkFpSqrt(), stabilizer::parser::Parser::mkFpSqrt(), stabilizer::parser::Parser::mkFpSub(), stabilizer::parser::Parser::mkFpToReal(), stabilizer::parser::Parser::mkFpToSbv(), stabilizer::parser::Parser::mkFpToUbv(), and stabilizer::parser::Parser::mkToFp().
| bool stabilizer::parser::isIntParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 44 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkAbs(), stabilizer::parser::Parser::mkBvExtract(), stabilizer::parser::Parser::mkBvRepeat(), stabilizer::parser::Parser::mkBvRotateLeft(), stabilizer::parser::Parser::mkBvRotateRight(), stabilizer::parser::Parser::mkBvSignExt(), stabilizer::parser::Parser::mkBvZeroExt(), stabilizer::parser::Parser::mkCeil(), stabilizer::parser::Parser::mkFact(), stabilizer::parser::Parser::mkFpToSbv(), stabilizer::parser::Parser::mkFpToUbv(), stabilizer::parser::Parser::mkGcd(), stabilizer::parser::Parser::mkIntToBv(), stabilizer::parser::Parser::mkIsDivisible(), stabilizer::parser::Parser::mkIsEven(), stabilizer::parser::Parser::mkIsOdd(), stabilizer::parser::Parser::mkIsPrime(), stabilizer::parser::Parser::mkLcm(), stabilizer::parser::Parser::mkMod(), stabilizer::parser::Parser::mkNatToBv(), stabilizer::parser::Parser::mkRegLoop(), stabilizer::parser::Parser::mkRegRepeat(), stabilizer::parser::Parser::mkSafeSqrt(), stabilizer::parser::Parser::mkSqrt(), stabilizer::parser::Parser::mkStrCharat(), stabilizer::parser::Parser::mkStrFromCode(), stabilizer::parser::Parser::mkStrFromInt(), stabilizer::parser::Parser::mkStrIndexof(), stabilizer::parser::Parser::mkStrSplitAt(), stabilizer::parser::Parser::mkStrSplitAtRe(), stabilizer::parser::Parser::mkStrSplitRest(), stabilizer::parser::Parser::mkStrSplitRestRe(), stabilizer::parser::Parser::mkStrSubstr(), stabilizer::parser::Parser::mkStrUpdate(), and stabilizer::parser::Parser::mkToReal().
| bool stabilizer::parser::isRealParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 48 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkAbs(), stabilizer::parser::Parser::mkCeil(), stabilizer::parser::Parser::mkIsInt(), stabilizer::parser::Parser::mkSafeSqrt(), stabilizer::parser::Parser::mkSqrt(), stabilizer::parser::Parser::mkToFp(), and stabilizer::parser::Parser::mkToInt().
| bool stabilizer::parser::isRegParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 68 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkIndexofReg(), stabilizer::parser::Parser::mkRegComplement(), stabilizer::parser::Parser::mkRegConcat(), stabilizer::parser::Parser::mkRegDiff(), stabilizer::parser::Parser::mkRegInter(), stabilizer::parser::Parser::mkRegLoop(), stabilizer::parser::Parser::mkRegOpt(), stabilizer::parser::Parser::mkRegPlus(), stabilizer::parser::Parser::mkRegRepeat(), stabilizer::parser::Parser::mkRegStar(), stabilizer::parser::Parser::mkRegUnion(), stabilizer::parser::Parser::mkReplaceReg(), stabilizer::parser::Parser::mkReplaceRegAll(), stabilizer::parser::Parser::mkStrIndexofReg(), stabilizer::parser::Parser::mkStrInReg(), stabilizer::parser::Parser::mkStrNumSplitsRe(), stabilizer::parser::Parser::mkStrReplaceReg(), stabilizer::parser::Parser::mkStrReplaceRegAll(), stabilizer::parser::Parser::mkStrSplitAtRe(), and stabilizer::parser::Parser::mkStrSplitRestRe().
| bool stabilizer::parser::isStrParam | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 64 of file op_parser.cpp.
Referenced by stabilizer::parser::Parser::mkIndexofReg(), stabilizer::parser::Parser::mkRegRange(), stabilizer::parser::Parser::mkReplaceReg(), stabilizer::parser::Parser::mkReplaceRegAll(), stabilizer::parser::Parser::mkStrCharat(), stabilizer::parser::Parser::mkStrConcat(), stabilizer::parser::Parser::mkStrContains(), stabilizer::parser::Parser::mkStrIndexof(), stabilizer::parser::Parser::mkStrIndexofReg(), stabilizer::parser::Parser::mkStrInReg(), stabilizer::parser::Parser::mkStrIsDigit(), stabilizer::parser::Parser::mkStrLen(), stabilizer::parser::Parser::mkStrNumSplits(), stabilizer::parser::Parser::mkStrNumSplitsRe(), stabilizer::parser::Parser::mkStrPrefixof(), stabilizer::parser::Parser::mkStrReplace(), stabilizer::parser::Parser::mkStrReplaceAll(), stabilizer::parser::Parser::mkStrReplaceReg(), stabilizer::parser::Parser::mkStrReplaceRegAll(), stabilizer::parser::Parser::mkStrRev(), stabilizer::parser::Parser::mkStrSplit(), stabilizer::parser::Parser::mkStrSplitAt(), stabilizer::parser::Parser::mkStrSplitAtRe(), stabilizer::parser::Parser::mkStrSplitRest(), stabilizer::parser::Parser::mkStrSplitRestRe(), stabilizer::parser::Parser::mkStrSubstr(), stabilizer::parser::Parser::mkStrSuffixof(), stabilizer::parser::Parser::mkStrToCode(), stabilizer::parser::Parser::mkStrToInt(), stabilizer::parser::Parser::mkStrToLower(), stabilizer::parser::Parser::mkStrToReg(), stabilizer::parser::Parser::mkStrToUpper(), and stabilizer::parser::Parser::mkStrUpdate().
| std::string stabilizer::parser::kindToString | ( | const NODE_KIND & | nk | ) |
Definition at line 35 of file kind.cpp.
References NT_ABS, NT_ACOS, NT_ACOSH, NT_ACOT, NT_ACOTH, NT_ACSC, NT_ACSCH, NT_ADD, NT_AND, NT_ASEC, NT_ASECH, NT_ASIN, NT_ASINH, NT_ATAN, NT_ATAN2, NT_ATANH, NT_BV_ADD, NT_BV_AND, NT_BV_ASHR, NT_BV_COMP, NT_BV_CONCAT, NT_BV_EXTRACT, NT_BV_LSHR, NT_BV_MUL, NT_BV_NAND, NT_BV_NEG, NT_BV_NEGO, NT_BV_NOR, NT_BV_NOT, NT_BV_OR, NT_BV_REPEAT, NT_BV_ROTATE_LEFT, NT_BV_ROTATE_RIGHT, NT_BV_SADDO, NT_BV_SDIV, NT_BV_SDIVO, NT_BV_SGE, NT_BV_SGT, NT_BV_SHL, NT_BV_SIGN_EXT, NT_BV_SLE, NT_BV_SLT, NT_BV_SMOD, NT_BV_SMODO, NT_BV_SMULO, NT_BV_SREM, NT_BV_SREMO, NT_BV_SUB, NT_BV_TO_INT, NT_BV_TO_NAT, NT_BV_UADDO, NT_BV_UDIV, NT_BV_UDIVO, NT_BV_UGE, NT_BV_UGT, NT_BV_ULE, NT_BV_ULT, NT_BV_UMOD, NT_BV_UMODO, NT_BV_UMULO, NT_BV_UREM, NT_BV_UREMO, NT_BV_XNOR, NT_BV_XOR, NT_BV_ZERO_EXT, NT_CEIL, NT_CONST, NT_CONST_ARRAY, NT_CONST_E, NT_CONST_FALSE, NT_CONST_PI, NT_CONST_TRUE, NT_COS, NT_COSH, NT_COT, NT_COTH, NT_CSC, NT_CSCH, NT_DISTINCT, NT_DISTINCT_BOOL, NT_DISTINCT_OTHER, NT_DIV_INT, NT_DIV_REAL, NT_DT_FUN_APPLY, NT_DT_TESTER, NT_DT_UPDATER, NT_EPSILON, NT_EQ, NT_EQ_BOOL, NT_EQ_OTHER, NT_ERROR, NT_EXISTS, NT_EXP, NT_FACT, NT_FLOOR, NT_FORALL, NT_FP_ABS, NT_FP_ADD, NT_FP_DIV, NT_FP_EQ, NT_FP_FMA, NT_FP_GE, NT_FP_GT, NT_FP_IS_INF, NT_FP_IS_NAN, NT_FP_IS_NEG, NT_FP_IS_NORMAL, NT_FP_IS_POS, NT_FP_IS_SUBNORMAL, NT_FP_IS_ZERO, NT_FP_LE, NT_FP_LT, NT_FP_MAX, NT_FP_MIN, NT_FP_MUL, NT_FP_NEG, NT_FP_REM, NT_FP_ROUND_TO_INTEGRAL, NT_FP_SQRT, NT_FP_SUB, NT_FP_TO_FP, NT_FP_TO_FP_UNSIGNED, NT_FP_TO_REAL, NT_FP_TO_SBV, NT_FP_TO_UBV, NT_FUNC_APPLY, NT_FUNC_DEC, NT_FUNC_DEF, NT_FUNC_PARAM, NT_FUNC_REC, NT_FUNC_REC_APPLY, NT_GCD, NT_GE, NT_GT, NT_IAND, NT_IMPLIES, NT_INFINITY, NT_INT_TO_BV, NT_IS_DIVISIBLE, NT_IS_EVEN, NT_IS_INT, NT_IS_ODD, NT_IS_PRIME, NT_ITE, NT_LB, NT_LCM, NT_LE, NT_LET, NT_LET_BIND_VAR, NT_LET_BIND_VAR_LIST, NT_LET_CHAIN, NT_LG, NT_LN, NT_LOG, NT_LT, NT_MAX, NT_MIN, NT_MOD, NT_MUL, NT_NAN, NT_NAT_TO_BV, NT_NEG, NT_NEG_EPSILON, NT_NEG_INFINITY, NT_NOT, NT_NULL, NT_OR, NT_PLACEHOLDER_VAR, NT_POS_EPSILON, NT_POS_INFINITY, NT_POW, NT_POW2, NT_QUANT_VAR, NT_REG_ALL, NT_REG_ALLCHAR, NT_REG_COMPLEMENT, NT_REG_CONCAT, NT_REG_DIFF, NT_REG_INTER, NT_REG_LOOP, NT_REG_NONE, NT_REG_OPT, NT_REG_PLUS, NT_REG_RANGE, NT_REG_REPEAT, NT_REG_STAR, NT_REG_UNION, NT_ROUND, NT_SAFESQRT, NT_SBV_TO_INT, NT_SEC, NT_SECH, NT_SELECT, NT_SIN, NT_SINH, NT_SQRT, NT_STORE, NT_STR_CHARAT, NT_STR_CONCAT, NT_STR_CONTAINS, NT_STR_FROM_CODE, NT_STR_FROM_INT, NT_STR_GE, NT_STR_GT, NT_STR_IN_REG, NT_STR_INDEXOF, NT_STR_INDEXOF_REG, NT_STR_IS_DIGIT, NT_STR_LE, NT_STR_LEN, NT_STR_LT, NT_STR_NUM_SPLITS, NT_STR_NUM_SPLITS_RE, NT_STR_PREFIXOF, NT_STR_REPLACE, NT_STR_REPLACE_ALL, NT_STR_REPLACE_REG, NT_STR_REPLACE_REG_ALL, NT_STR_REV, NT_STR_SPLIT, NT_STR_SPLIT_AT, NT_STR_SPLIT_AT_RE, NT_STR_SPLIT_REST, NT_STR_SPLIT_REST_RE, NT_STR_SUBSTR, NT_STR_SUFFIXOF, NT_STR_TO_CODE, NT_STR_TO_INT, NT_STR_TO_LOWER, NT_STR_TO_REG, NT_STR_TO_UPPER, NT_STR_UPDATE, NT_SUB, NT_TAN, NT_TANH, NT_TEMP_VAR, NT_TO_INT, NT_TO_REAL, NT_TUPLE_CONSTRUCTOR, NT_TUPLE_PROJECT, NT_TUPLE_SELECT, NT_TUPLE_UNIT, NT_TUPLE_UPDATE, NT_UBV_TO_INT, NT_UF_APPLY, NT_UNKNOWN, NT_VAR, and NT_XOR.
Referenced by dumpSMTLIB2_streaming(), stabilizer::parser::Parser::mkInternalOper(), stabilizer::parser::Parser::rewrite(), and stabilizer::parser::Parser::toString().
| ParserPtr stabilizer::parser::newParser | ( | ) |
Definition at line 3020 of file base_parser.cpp.
| ParserPtr stabilizer::parser::newParser | ( | const std::string & | filename | ) |
Definition at line 3022 of file base_parser.cpp.
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const bool & | boolean_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const char & | char_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const double & | double_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const float & | float_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const int & | integer_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const long & | long_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const short & | short_value | ) |
| std::shared_ptr< Value > stabilizer::parser::newValue | ( | const std::string & | string_value | ) |
Definition at line 168 of file value.cpp.
Referenced by stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::DAGNode(), stabilizer::parser::DAGNode::setValue(), stabilizer::parser::DAGNode::setValue(), stabilizer::parser::DAGNode::setValue(), stabilizer::parser::DAGNode::setValue(), and stabilizer::parser::DAGNode::setValue().
| char * stabilizer::parser::safe_strdup | ( | const std::string & | str | ) |
Definition at line 686 of file base_parser.cpp.
Referenced by stabilizer::parser::Parser::mkExpr(), and stabilizer::parser::Parser::parseStr().
Definition at line 185 of file interval.h.
Referenced by stabilizer::parser::Interval::abs(), stabilizer::parser::Interval::acos(), stabilizer::parser::Interval::acosh(), stabilizer::parser::Interval::acot(), stabilizer::parser::Interval::acoth(), stabilizer::parser::Interval::acsc(), stabilizer::parser::Interval::acsch(), stabilizer::parser::Interval::asec(), stabilizer::parser::Interval::asech(), stabilizer::parser::Interval::asin(), stabilizer::parser::Interval::asinh(), stabilizer::parser::Interval::atan(), stabilizer::parser::Interval::atan2(), stabilizer::parser::Interval::atan2(), stabilizer::parser::Interval::atanh(), stabilizer::parser::Interval::cos(), stabilizer::parser::Interval::cosh(), stabilizer::parser::Interval::cot(), stabilizer::parser::Interval::coth(), stabilizer::parser::Interval::csc(), stabilizer::parser::Interval::csch(), stabilizer::parser::Interval::divInt(), stabilizer::parser::Interval::divInt(), stabilizer::parser::Interval::divReal(), stabilizer::parser::Interval::divReal(), stabilizer::parser::Interval::exp(), stabilizer::parser::Interval::intersection(), stabilizer::parser::Interval::lb(), stabilizer::parser::Interval::lg(), stabilizer::parser::Interval::ln(), stabilizer::parser::Interval::mod(), stabilizer::parser::Interval::mod(), stabilizer::parser::Interval::negate(), stabilizer::parser::Interval::operate(), stabilizer::parser::Interval::operate(), stabilizer::parser::Interval::operator!(), stabilizer::parser::Interval::operator*(), stabilizer::parser::Interval::operator*(), stabilizer::parser::Interval::operator+(), stabilizer::parser::Interval::operator+(), stabilizer::parser::Interval::operator++(), stabilizer::parser::Interval::operator++(), stabilizer::parser::Interval::operator-(), stabilizer::parser::Interval::operator-(), stabilizer::parser::Interval::operator--(), stabilizer::parser::Interval::operator--(), stabilizer::parser::Interval::operator/(), stabilizer::parser::Interval::operator~(), stabilizer::parser::Interval::pow(), stabilizer::parser::Interval::pow(), stabilizer::parser::Interval::pow2(), stabilizer::parser::Interval::safeSqrt(), stabilizer::parser::Interval::sec(), stabilizer::parser::Interval::sech(), stabilizer::parser::Interval::sin(), stabilizer::parser::Interval::sinh(), stabilizer::parser::Interval::sqrt(), stabilizer::parser::Interval::tan(), stabilizer::parser::Interval::tanh(), and stabilizer::parser::Interval::unionWith().
|
inline |
Definition at line 186 of file interval.h.
Referenced by stabilizer::parser::Interval::divInt(), stabilizer::parser::Interval::divReal(), stabilizer::parser::Interval::pow(), and stabilizer::parser::Interval::tan().
| const std::unordered_map<std::string, NODE_KIND> stabilizer::parser::kind_key_map |
|
constexpr |
Definition at line 366 of file kind.h.
Referenced by stabilizer::parser::NodeManager::NodeManager().
| const std::unordered_map<std::string, NODE_KIND> stabilizer::parser::oper_key_map |
Definition at line 385 of file kind.h.
Referenced by getOperKind().
| const std::string stabilizer::parser::PRESERVING_LET_BIND_VAR_SUFFIX |
Definition at line 370 of file kind.h.
Referenced by stabilizer::parser::DAGNode::getPureName(), stabilizer::parser::Parser::parseConstFunc(), and stabilizer::parser::Parser::parsePreservingLet().
| const std::unordered_set<NODE_KIND> stabilizer::parser::static_kinds |
Definition at line 367 of file kind.h.
Referenced by stabilizer::parser::NodeManager::NodeManager().
1.9.8