|
SMTStabilizer API
Public API documentation for SMTStabilizer
|
#include <parser.h>
Classes | |
| struct | DTConstructorDecl |
| struct | DTSelectorDecl |
| struct | DTTypeDecl |
Public Member Functions | |
| Parser (const std::string &filename) | |
| Constructor with filename. | |
| Parser () | |
| Default constructor. | |
| ~Parser () | |
| Destructor. | |
| void | replaceAssertions (const std::vector< std::shared_ptr< DAGNode > > &new_assertions) |
| std::shared_ptr< DAGNode > | mkUFVNode (const std::string &name, const std::shared_ptr< Sort > &sort) |
| std::shared_ptr< DAGNode > | rebuildLetBindings (const std::shared_ptr< DAGNode > &root) |
| std::unordered_map< std::string, size_t > & | getTempVarNames () |
| std::unordered_map< std::string, size_t > & | getVarNames () |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > & | getFunKeyMap () |
| std::vector< std::string > & | getFunctionNames () |
| std::unordered_map< std::string, std::shared_ptr< Sort > > & | getSortNames () |
| std::vector< std::vector< DTTypeDecl > > & | getDatatypeBlocks () |
| void | clear_let_key_map () |
| bool | parse (const std::string &filename) |
| Parse SMT-LIB2 file. | |
| bool | parseStr (const std::string &constraint) |
| Parse a constraint. | |
| bool | assert (const std::string &constraint) |
| Assert a constraint. | |
| bool | assert (std::shared_ptr< DAGNode > node) |
| Assert a constraint. | |
| std::shared_ptr< DAGNode > | mkExpr (const std::string &expression) |
| Create a DAG node from a string expression. | |
| std::vector< std::shared_ptr< DAGNode > > | getAssertions () const |
| Get all assertions. | |
| std::unordered_map< std::string, std::unordered_set< size_t > > | getGroupedAssertions () const |
| Get grouped assertions. | |
| std::vector< std::vector< std::shared_ptr< DAGNode > > > | getAssumptions () const |
| Get assumptions. | |
| std::vector< std::shared_ptr< DAGNode > > | getSoftAssertions () const |
| Get soft assertions. | |
| std::vector< std::shared_ptr< DAGNode > > | getSoftWeights () const |
| Get soft assertion weights. | |
| std::unordered_map< std::string, std::unordered_set< size_t > > | getGroupedSoftAssertions () const |
| Get grouped soft assertions. | |
| void | setOption (const std::string &key, const std::string &value) |
| Set global options. | |
| void | setOption (const std::string &key, const int &value) |
| void | setOption (const std::string &key, const double &value) |
| void | setOption (const std::string &key, const bool &value) |
| std::shared_ptr< GlobalOptions > | getOptions () const |
| Get global options. | |
| std::vector< std::shared_ptr< DAGNode > > | getVariables () const |
| Get variables. | |
| std::vector< std::shared_ptr< DAGNode > > | getDeclaredVariables () const |
| Get declared variables. | |
| bool | isDeclaredVariable (const std::string &var_name) const |
| Check if a variable is declared. | |
| std::shared_ptr< DAGNode > | getVariable (const std::string &var_name) |
| Get variable. | |
| std::vector< std::shared_ptr< DAGNode > > | getFunctions () const |
| Get functions. | |
| bool | isDeclaredFunction (const std::string &func_name) const |
| Check if a function is declared. | |
| std::shared_ptr< Sort > | getSort (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Get sort. | |
| std::shared_ptr< Sort > | getSort (std::shared_ptr< DAGNode > param) |
| Get sort. | |
| std::shared_ptr< Sort > | getSort (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Get sort. | |
| std::shared_ptr< Sort > | getSort (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > m) |
| Get sort. | |
| NODE_KIND | getKind (const std::string &s) |
| Get kind. | |
| NODE_KIND | getKind (const std::shared_ptr< DAGNode > &node) |
| Get kind. | |
| RESULT_TYPE | getResultType () |
| Get result type. | |
| std::shared_ptr< DAGNode > | getResult () |
| Get result. | |
| RESULT_TYPE | checkSat () |
| Check satisfiability. | |
| size_t | getNodeCount () |
| Get node count. | |
| std::shared_ptr< DAGNode > | mkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, std::shared_ptr< DAGNode > p) |
| Create an operation. | |
| std::shared_ptr< DAGNode > | mkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an operation. | |
| std::shared_ptr< DAGNode > | mkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > m, std::shared_ptr< DAGNode > r) |
| Create an operation. | |
| std::shared_ptr< DAGNode > | mkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, const std::vector< std::shared_ptr< DAGNode > > &p) |
| Create an operation. | |
| std::shared_ptr< DAGNode > | rewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &p) |
| Rewrite unary operation node when simplification rule applies. | |
| std::shared_ptr< DAGNode > | rewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &l, std::shared_ptr< DAGNode > &r) |
| Rewrite binary operation node when simplification rule applies. | |
| std::shared_ptr< DAGNode > | rewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &l, std::shared_ptr< DAGNode > &m, std::shared_ptr< DAGNode > &r) |
| Rewrite ternary operation node when simplification rule applies. | |
| std::shared_ptr< DAGNode > | rewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &l, std::shared_ptr< DAGNode > &ml, std::shared_ptr< DAGNode > &mr, std::shared_ptr< DAGNode > &r) |
| Rewrite four-operand operation node when simplification rule applies. | |
| std::shared_ptr< DAGNode > | rewrite (NODE_KIND &t, std::vector< std::shared_ptr< DAGNode > > &p) |
| Rewrite variadic operation node when simplification rule applies. | |
| std::shared_ptr< DAGNode > | rewrite_oper (NODE_KIND &t, std::vector< std::shared_ptr< DAGNode > > &p) |
| Core operation rewrite helper used before node-manager creation. | |
| std::unique_ptr< NodeManager > | getNodeManager () |
| void | rebuild_node_manager () |
| std::shared_ptr< DAGNode > | mkNode (std::shared_ptr< Sort > sort, NODE_KIND t, std::string name, std::vector< std::shared_ptr< DAGNode > > params) |
| std::shared_ptr< DAGNode > | mkFuncDec (const std::string &name, const std::vector< std::shared_ptr< Sort > > ¶ms, std::shared_ptr< Sort > out_sort) |
| Create a function declaration. | |
| std::shared_ptr< DAGNode > | mkFuncDef (const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms, std::shared_ptr< Sort > out_sort, std::shared_ptr< DAGNode > body) |
| Create a function definition. | |
| std::shared_ptr< DAGNode > | mkFuncRec (const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms, std::shared_ptr< Sort > out_sort, std::shared_ptr< DAGNode > body) |
| Create a recursive function definition. | |
| std::shared_ptr< DAGNode > | mkApplyRecFunc (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a recursive function application. | |
| std::shared_ptr< DAGNode > | mkPattern (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| std::shared_ptr< DAGNode > | mkNoPattern (const std::shared_ptr< Sort > &sort, const std::string &name, std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkWeight (const std::shared_ptr< Sort > &sort, const std::string &name, std::shared_ptr< DAGNode > weight) |
| std::shared_ptr< DAGNode > | mkAttribute (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| std::shared_ptr< DAGNode > | mkApplyUF (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Apply an uninterpreted function. | |
| std::shared_ptr< Sort > | mkSortDec (const std::string &name, const size_t &arity) |
| Create a sort declaration. | |
| std::shared_ptr< Sort > | mkSortDef (const std::string &name, const std::vector< std::shared_ptr< Sort > > ¶ms, std::shared_ptr< Sort > out_sort) |
| Create a sort definition. | |
| std::shared_ptr< Sort > | mkIntSort () |
| Create an integer sort. | |
| std::shared_ptr< Sort > | mkRealSort () |
| Create a real sort. | |
| std::shared_ptr< Sort > | mkBoolSort () |
| Create a boolean sort. | |
| std::shared_ptr< Sort > | mkStrSort () |
| Create a string sort. | |
| std::shared_ptr< Sort > | mkRegSort () |
| Create a regular expression sort. | |
| std::shared_ptr< Sort > | mkRoundingModeSort () |
| Create a rounding mode sort. | |
| std::shared_ptr< Sort > | mkNatSort () |
| Create a natural sort. | |
| std::shared_ptr< Sort > | mkBVSort (const size_t &width) |
| Create a bit-vector sort. | |
| std::shared_ptr< Sort > | mkFPSort (const size_t &e, const size_t &s) |
| Create a floating-point sort. | |
| std::shared_ptr< Sort > | mkArraySort (std::shared_ptr< Sort > index, std::shared_ptr< Sort > elem) |
| Create an array sort. | |
| std::shared_ptr< DAGNode > | declareVar (const std::string &name, const std::string &sort) |
| Declare a variable. | |
| std::shared_ptr< DAGNode > | declareVar (const std::string &name, const std::shared_ptr< Sort > &sort) |
| Declare a variable. | |
| std::shared_ptr< DAGNode > | mkTrue () |
| Create a true node. | |
| std::shared_ptr< DAGNode > | mkFalse () |
| Create a false node. | |
| std::shared_ptr< DAGNode > | mkUnknown () |
| Create an unknown node. | |
| std::shared_ptr< DAGNode > | mkEq (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an equality node. | |
| std::shared_ptr< DAGNode > | mkDistinct (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a distinct node. | |
| std::shared_ptr< DAGNode > | mkConstInt (const std::string &v) |
| Create an integer constant from string. | |
| std::shared_ptr< DAGNode > | mkConstInt (const int &v) |
| Create an integer constant. | |
| std::shared_ptr< DAGNode > | mkConstInt (const Integer &v) |
| Create an integer constant. | |
| std::shared_ptr< DAGNode > | mkConstInt (const Number &v) |
| Create a real constant from number. | |
| std::shared_ptr< DAGNode > | mkConstReal (const std::string &v) |
| Create a real constant from string. | |
| std::shared_ptr< DAGNode > | mkConstReal (const Real &v) |
| Create a real constant. | |
| std::shared_ptr< DAGNode > | mkConstReal (const double &v) |
| Create a real constant from double. | |
| std::shared_ptr< DAGNode > | mkConstReal (const Integer &v) |
| Create a real constant from integer. | |
| std::shared_ptr< DAGNode > | mkConstReal (const Number &v) |
| Create a real constant from number. | |
| std::shared_ptr< DAGNode > | mkConstStr (const std::string &v) |
| Create a string constant. | |
| std::shared_ptr< DAGNode > | mkConstBv (const std::string &v, const size_t &width) |
| Create a bit-vector constant. | |
| std::shared_ptr< DAGNode > | mkConstFp (const std::string &v, const size_t &e, const size_t &s) |
| Create a floating-point constant. | |
| std::shared_ptr< DAGNode > | mkConstFP (const std::string &fp_expr) |
| Create a floating-point constant from expression. | |
| std::shared_ptr< DAGNode > | mkConstReg (const std::string &v) |
| Create a regular expression constant. | |
| std::shared_ptr< DAGNode > | mkRoundingMode (const std::string &mode) |
| Create a rounding mode constant. | |
| std::shared_ptr< DAGNode > | mkVarRoundingMode (const std::string &name) |
| Create a rounding mode variable. | |
| std::shared_ptr< DAGNode > | mkVar (const std::shared_ptr< Sort > &sort, const std::string &name) |
| Create a variable. | |
| std::shared_ptr< DAGNode > | mkPlaceholderVar (const std::string &name) |
| std::shared_ptr< DAGNode > | mkTempVar (const std::shared_ptr< Sort > &sort) |
| Create a temporary variable. | |
| std::shared_ptr< DAGNode > | mkVarBool (const std::string &name) |
| Create a boolean variable. | |
| std::shared_ptr< DAGNode > | mkVarInt (const std::string &name) |
| Create an integer variable. | |
| std::shared_ptr< DAGNode > | mkVarReal (const std::string &name) |
| Create a real variable. | |
| std::shared_ptr< DAGNode > | mkVarBv (const std::string &name, const size_t &width) |
| Create a bit-vector variable. | |
| std::shared_ptr< DAGNode > | mkVarFp (const std::string &name, const size_t &e, const size_t &s) |
| Create a floating-point variable. | |
| std::shared_ptr< DAGNode > | mkVarStr (const std::string &name) |
| Create a string variable. | |
| std::shared_ptr< DAGNode > | mkVarReg (const std::string &name) |
| Create a regular expression variable. | |
| std::shared_ptr< DAGNode > | mkFunParamVar (std::shared_ptr< Sort > sort, const std::string &name) |
| Create a function parameter variable. | |
| std::shared_ptr< DAGNode > | mkArray (const std::string &name, std::shared_ptr< Sort > index, std::shared_ptr< Sort > elem) |
| Create an array. | |
| std::shared_ptr< DAGNode > | mkConstArray (std::shared_ptr< Sort > sort, std::shared_ptr< DAGNode > value) |
| Create a constant array node. | |
| std::shared_ptr< DAGNode > | mkNot (std::shared_ptr< DAGNode > param) |
| Create a not node. | |
| std::shared_ptr< DAGNode > | mkAnd (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an and node. | |
| std::shared_ptr< DAGNode > | mkOr (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an or node. | |
| std::shared_ptr< DAGNode > | mkImplies (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an implies node. | |
| std::shared_ptr< DAGNode > | mkXor (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an xor node. | |
| std::shared_ptr< DAGNode > | mkIte (std::shared_ptr< DAGNode > cond, std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an ite node. | |
| std::shared_ptr< DAGNode > | mkIte (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an ite node. | |
| std::shared_ptr< DAGNode > | mkAdd (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an add node. | |
| std::shared_ptr< DAGNode > | mkMul (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an mul node. | |
| std::shared_ptr< DAGNode > | mkIand (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an iand node. | |
| std::shared_ptr< DAGNode > | mkPow2 (std::shared_ptr< DAGNode > param) |
| Create an pow2 node. | |
| std::shared_ptr< DAGNode > | mkPow (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an pow node. | |
| std::shared_ptr< DAGNode > | mkSub (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an sub node. | |
| std::shared_ptr< DAGNode > | mkNeg (std::shared_ptr< DAGNode > param) |
| Create an neg node. | |
| std::shared_ptr< DAGNode > | mkDiv (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an div node. | |
| std::shared_ptr< DAGNode > | mkDivInt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an div node. | |
| std::shared_ptr< DAGNode > | mkDivReal (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an div node. | |
| std::shared_ptr< DAGNode > | mkMod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an mod node. | |
| std::shared_ptr< DAGNode > | mkAbs (std::shared_ptr< DAGNode > param) |
| Create an abs node. | |
| std::shared_ptr< DAGNode > | mkSqrt (std::shared_ptr< DAGNode > param) |
| Create an sqrt node. | |
| std::shared_ptr< DAGNode > | mkSafeSqrt (std::shared_ptr< DAGNode > param) |
| Create an safeSqrt node. | |
| std::shared_ptr< DAGNode > | mkCeil (std::shared_ptr< DAGNode > param) |
| Create an ceil node. | |
| std::shared_ptr< DAGNode > | mkFloor (std::shared_ptr< DAGNode > param) |
| Create an floor node. | |
| std::shared_ptr< DAGNode > | mkRound (std::shared_ptr< DAGNode > param) |
| Create an round node. | |
| std::shared_ptr< DAGNode > | mkExp (std::shared_ptr< DAGNode > param) |
| Create an exp node. | |
| std::shared_ptr< DAGNode > | mkLn (std::shared_ptr< DAGNode > param) |
| Create an ln node. | |
| std::shared_ptr< DAGNode > | mkLg (std::shared_ptr< DAGNode > param) |
| Create an lg/log10 node. | |
| std::shared_ptr< DAGNode > | mkLb (std::shared_ptr< DAGNode > param) |
| Create an lb/log2 node. | |
| std::shared_ptr< DAGNode > | mkLog (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an log node. | |
| std::shared_ptr< DAGNode > | mkSin (std::shared_ptr< DAGNode > param) |
| Create an sin node. | |
| std::shared_ptr< DAGNode > | mkCos (std::shared_ptr< DAGNode > param) |
| Create an cos node. | |
| std::shared_ptr< DAGNode > | mkSec (std::shared_ptr< DAGNode > param) |
| Create an sec node. | |
| std::shared_ptr< DAGNode > | mkCsc (std::shared_ptr< DAGNode > param) |
| Create an csc node. | |
| std::shared_ptr< DAGNode > | mkTan (std::shared_ptr< DAGNode > param) |
| Create an tan node. | |
| std::shared_ptr< DAGNode > | mkCot (std::shared_ptr< DAGNode > param) |
| Create a cot node. | |
| std::shared_ptr< DAGNode > | mkAsin (std::shared_ptr< DAGNode > param) |
| Create an asin node. | |
| std::shared_ptr< DAGNode > | mkAcos (std::shared_ptr< DAGNode > param) |
| Create an acos node. | |
| std::shared_ptr< DAGNode > | mkAsec (std::shared_ptr< DAGNode > param) |
| Create an asec node. | |
| std::shared_ptr< DAGNode > | mkAcsc (std::shared_ptr< DAGNode > param) |
| Create an acsc node. | |
| std::shared_ptr< DAGNode > | mkAtan (std::shared_ptr< DAGNode > param) |
| Create an atan node. | |
| std::shared_ptr< DAGNode > | mkAcot (std::shared_ptr< DAGNode > param) |
| Create an acot node. | |
| std::shared_ptr< DAGNode > | mkSinh (std::shared_ptr< DAGNode > param) |
| Create a sinh node. | |
| std::shared_ptr< DAGNode > | mkCosh (std::shared_ptr< DAGNode > param) |
| Create a cosh node. | |
| std::shared_ptr< DAGNode > | mkTanh (std::shared_ptr< DAGNode > param) |
| Create a tanh node. | |
| std::shared_ptr< DAGNode > | mkSech (std::shared_ptr< DAGNode > param) |
| Create a sech node. | |
| std::shared_ptr< DAGNode > | mkCsch (std::shared_ptr< DAGNode > param) |
| Create a csch node. | |
| std::shared_ptr< DAGNode > | mkCoth (std::shared_ptr< DAGNode > param) |
| Create a coth node. | |
| std::shared_ptr< DAGNode > | mkAsinh (std::shared_ptr< DAGNode > param) |
| Create an asinh node. | |
| std::shared_ptr< DAGNode > | mkAcosh (std::shared_ptr< DAGNode > param) |
| Create an acosh node. | |
| std::shared_ptr< DAGNode > | mkAtanh (std::shared_ptr< DAGNode > param) |
| Create an atanh node. | |
| std::shared_ptr< DAGNode > | mkAsech (std::shared_ptr< DAGNode > param) |
| Create an asech node. | |
| std::shared_ptr< DAGNode > | mkAcsch (std::shared_ptr< DAGNode > param) |
| Create an acsch node. | |
| std::shared_ptr< DAGNode > | mkAcoth (std::shared_ptr< DAGNode > param) |
| Create an acoth node. | |
| std::shared_ptr< DAGNode > | mkAtan2 (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an atan2 node. | |
| std::shared_ptr< DAGNode > | mkLe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a le node. | |
| std::shared_ptr< DAGNode > | mkLt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a lt node. | |
| std::shared_ptr< DAGNode > | mkGe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a ge node. | |
| std::shared_ptr< DAGNode > | mkGt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a gt node. | |
| std::shared_ptr< DAGNode > | mkToInt (std::shared_ptr< DAGNode > param) |
| Create a to_int node. | |
| std::shared_ptr< DAGNode > | mkToReal (std::shared_ptr< DAGNode > param) |
| Create a to_real node. | |
| std::shared_ptr< DAGNode > | mkIsInt (std::shared_ptr< DAGNode > param) |
| Create a is_int node. | |
| std::shared_ptr< DAGNode > | mkIsDivisible (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a is_divisible node. | |
| std::shared_ptr< DAGNode > | mkIsPrime (std::shared_ptr< DAGNode > param) |
| Create a is_prime node. | |
| std::shared_ptr< DAGNode > | mkIsEven (std::shared_ptr< DAGNode > param) |
| Create a is_even node. | |
| std::shared_ptr< DAGNode > | mkIsOdd (std::shared_ptr< DAGNode > param) |
| Create a is_odd node. | |
| std::shared_ptr< DAGNode > | mkPi () |
| Create a pi node. | |
| std::shared_ptr< DAGNode > | mkE () |
| Create a e node. | |
| std::shared_ptr< DAGNode > | mkInfinity (std::shared_ptr< Sort > sort) |
| Create a infinity node. | |
| std::shared_ptr< DAGNode > | mkPosInfinity (std::shared_ptr< Sort > sort=nullptr) |
| Create a positive infinity node. | |
| std::shared_ptr< DAGNode > | mkNegInfinity (std::shared_ptr< Sort > sort=nullptr) |
| Create a negative infinity node. | |
| std::shared_ptr< DAGNode > | mkNaN (std::shared_ptr< Sort > sort=nullptr) |
| Create a NaN node. | |
| std::shared_ptr< DAGNode > | mkEpsilon () |
| Create a epsilon node. | |
| std::shared_ptr< DAGNode > | mkPosEpsilon () |
| Create a positive epsilon node. | |
| std::shared_ptr< DAGNode > | mkNegEpsilon () |
| Create a negative epsilon node. | |
| std::shared_ptr< DAGNode > | mkGcd (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a gcd node. | |
| std::shared_ptr< DAGNode > | mkLcm (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a lcm node. | |
| std::shared_ptr< DAGNode > | mkFact (std::shared_ptr< DAGNode > param) |
| Create a factorial node. | |
| std::shared_ptr< DAGNode > | mkBvNot (std::shared_ptr< DAGNode > param) |
| Create a bitvector not node. | |
| std::shared_ptr< DAGNode > | mkBvAnd (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector and node. | |
| std::shared_ptr< DAGNode > | mkBvOr (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector or node. | |
| std::shared_ptr< DAGNode > | mkBvXor (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector xor node. | |
| std::shared_ptr< DAGNode > | mkBvNand (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector nand node. | |
| std::shared_ptr< DAGNode > | mkBvNor (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector nor node. | |
| std::shared_ptr< DAGNode > | mkBvComp (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector comparison node. | |
| std::shared_ptr< DAGNode > | mkBvXnor (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector xnor node. | |
| std::shared_ptr< DAGNode > | mkBvNeg (std::shared_ptr< DAGNode > param) |
| Create a bitvector negation node. | |
| std::shared_ptr< DAGNode > | mkBvAdd (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector addition node. | |
| std::shared_ptr< DAGNode > | mkBvSub (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector subtraction node. | |
| std::shared_ptr< DAGNode > | mkBvMul (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector multiplication node. | |
| std::shared_ptr< DAGNode > | mkBvUdiv (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned division node. | |
| std::shared_ptr< DAGNode > | mkBvUrem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned remainder node. | |
| std::shared_ptr< DAGNode > | mkBvUmod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned modulo node. | |
| std::shared_ptr< DAGNode > | mkBvSdiv (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed division node. | |
| std::shared_ptr< DAGNode > | mkBvSrem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed remainder node. | |
| std::shared_ptr< DAGNode > | mkBvSmod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed modulo node. | |
| std::shared_ptr< DAGNode > | mkBvShl (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector shift left node. | |
| std::shared_ptr< DAGNode > | mkBvLshr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector logical shift right node. | |
| std::shared_ptr< DAGNode > | mkBvAshr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector arithmetic shift right node. | |
| std::shared_ptr< DAGNode > | mkBvConcat (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a bitvector concatenation node. | |
| std::shared_ptr< DAGNode > | mkBvExtract (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| Create a bitvector extract node. | |
| std::shared_ptr< DAGNode > | mkBvRepeat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector repeat node. | |
| std::shared_ptr< DAGNode > | mkBvZeroExt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector zero extension node. | |
| std::shared_ptr< DAGNode > | mkBvSignExt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector sign extension node. | |
| std::shared_ptr< DAGNode > | mkBvRotateLeft (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector rotate left node. | |
| std::shared_ptr< DAGNode > | mkBvRotateRight (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector rotate right node. | |
| std::shared_ptr< DAGNode > | mkBvUlt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned less than node. | |
| std::shared_ptr< DAGNode > | mkBvUle (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned less than or equal node. | |
| std::shared_ptr< DAGNode > | mkBvUgt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned greater than node. | |
| std::shared_ptr< DAGNode > | mkBvUge (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector unsigned greater than or equal node. | |
| std::shared_ptr< DAGNode > | mkBvSlt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed less than node. | |
| std::shared_ptr< DAGNode > | mkBvSle (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed less than or equal node. | |
| std::shared_ptr< DAGNode > | mkBvSgt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed greater than node. | |
| std::shared_ptr< DAGNode > | mkBvSge (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a bitvector signed greater than or equal node. | |
| std::shared_ptr< DAGNode > | mkBvToNat (std::shared_ptr< DAGNode > param) |
| Create a bitvector to natural number conversion node. | |
| std::shared_ptr< DAGNode > | mkNatToBv (std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > width) |
| Create a natural number to bitvector conversion node. | |
| std::shared_ptr< DAGNode > | mkBvToInt (std::shared_ptr< DAGNode > param) |
| Create a bitvector to integer conversion node. | |
| std::shared_ptr< DAGNode > | mkUbvToInt (std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkSbvToInt (std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkIntToBv (std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > width) |
| Create an integer to bitvector conversion node. | |
| std::shared_ptr< DAGNode > | mkFpAdd (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point addition node. | |
| std::shared_ptr< DAGNode > | mkFpSub (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point subtraction node. | |
| std::shared_ptr< DAGNode > | mkFpMul (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point multiplication node. | |
| std::shared_ptr< DAGNode > | mkFpDiv (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point division node. | |
| std::shared_ptr< DAGNode > | mkFpAbs (std::shared_ptr< DAGNode > param) |
| Create a floating-point absolute value node. | |
| std::shared_ptr< DAGNode > | mkFpNeg (std::shared_ptr< DAGNode > param) |
| Create a floating-point negation node. | |
| std::shared_ptr< DAGNode > | mkFpRem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a floating-point remainder node. | |
| std::shared_ptr< DAGNode > | mkFpFma (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point fused multiply-add node. | |
| std::shared_ptr< DAGNode > | mkFpSqrt (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param) |
| Create a floating-point square root node. | |
| std::shared_ptr< DAGNode > | mkFpSqrt (std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkFpRoundToIntegral (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param) |
| Create a floating-point round to integral node. | |
| std::shared_ptr< DAGNode > | mkFpRoundToIntegral (std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkFpMin (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a floating-point minimum node. | |
| std::shared_ptr< DAGNode > | mkFpMax (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a floating-point maximum node. | |
| std::shared_ptr< DAGNode > | mkFpLe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point less than or equal node. | |
| std::shared_ptr< DAGNode > | mkFpLt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point less than node. | |
| std::shared_ptr< DAGNode > | mkFpGe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point greater than or equal node. | |
| std::shared_ptr< DAGNode > | mkFpGt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point greater than node. | |
| std::shared_ptr< DAGNode > | mkFpEq (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a floating-point equality node. | |
| std::shared_ptr< DAGNode > | mkFpToUbv (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > size) |
| Create a floating-point to unsigned bitvector conversion node. | |
| std::shared_ptr< DAGNode > | mkFpToSbv (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > size) |
| Create a floating-point to signed bitvector conversion node. | |
| std::shared_ptr< DAGNode > | mkFpToReal (std::shared_ptr< DAGNode > param) |
| Create a floating-point to real conversion node. | |
| std::shared_ptr< DAGNode > | mkToFp (std::shared_ptr< DAGNode > eb, std::shared_ptr< DAGNode > sb, std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param) |
| Create a value to floating-point conversion node. | |
| std::shared_ptr< DAGNode > | mkToFp (std::shared_ptr< DAGNode > eb, std::shared_ptr< DAGNode > sb, std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkToFpUnsigned (std::shared_ptr< DAGNode > eb, std::shared_ptr< DAGNode > sb, std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param) |
| std::shared_ptr< DAGNode > | mkFpConst (std::shared_ptr< DAGNode > sign, std::shared_ptr< DAGNode > exp, std::shared_ptr< DAGNode > mant) |
| std::shared_ptr< DAGNode > | mkRootObj (std::shared_ptr< DAGNode > expr, int index) |
| std::shared_ptr< DAGNode > | mkRootOfWithInterval (const std::vector< std::shared_ptr< DAGNode > > &coeffs, std::shared_ptr< DAGNode > lower_bound, std::shared_ptr< DAGNode > upper_bound) |
| std::shared_ptr< DAGNode > | mkFpIsNormal (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-normal check node. | |
| std::shared_ptr< DAGNode > | mkFpIsSubnormal (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-subnormal check node. | |
| std::shared_ptr< DAGNode > | mkFpIsZero (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-zero check node. | |
| std::shared_ptr< DAGNode > | mkFpIsInf (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-infinity check node. | |
| std::shared_ptr< DAGNode > | mkFpIsNaN (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-NaN check node. | |
| std::shared_ptr< DAGNode > | mkFpIsNeg (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-negative check node. | |
| std::shared_ptr< DAGNode > | mkFpIsPos (std::shared_ptr< DAGNode > param) |
| Create a floating-point is-positive check node. | |
| std::shared_ptr< DAGNode > | mkSelect (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create an array select node. | |
| std::shared_ptr< DAGNode > | mkStore (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create an array store node. | |
| std::shared_ptr< DAGNode > | mkStrLen (std::shared_ptr< DAGNode > param) |
| Create a string length node. | |
| std::shared_ptr< DAGNode > | mkStrConcat (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a string concatenation node. | |
| std::shared_ptr< DAGNode > | mkStrSubstr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| Create a string substring node. | |
| std::shared_ptr< DAGNode > | mkStrPrefixof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string prefix check node. | |
| std::shared_ptr< DAGNode > | mkStrSuffixof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string suffix check node. | |
| std::shared_ptr< DAGNode > | mkStrIndexof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| Create a string index-of node. | |
| std::shared_ptr< DAGNode > | mkStrCharat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string char-at node. | |
| std::shared_ptr< DAGNode > | mkStrUpdate (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string update node. | |
| std::shared_ptr< DAGNode > | mkStrReplace (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace node. | |
| std::shared_ptr< DAGNode > | mkStrReplaceAll (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace-all node. | |
| std::shared_ptr< DAGNode > | mkStrReplaceReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace-regex node. | |
| std::shared_ptr< DAGNode > | mkStrReplaceRegAll (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace-regex-all node. | |
| std::shared_ptr< DAGNode > | mkStrIndexofReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string indexof-regex node. | |
| std::shared_ptr< DAGNode > | mkStrToLower (std::shared_ptr< DAGNode > param) |
| Create a string to-lower node. | |
| std::shared_ptr< DAGNode > | mkStrToUpper (std::shared_ptr< DAGNode > param) |
| Create a string to-upper node. | |
| std::shared_ptr< DAGNode > | mkStrRev (std::shared_ptr< DAGNode > param) |
| Create a string reverse node. | |
| std::shared_ptr< DAGNode > | mkStrSplit (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string split node. | |
| std::shared_ptr< DAGNode > | mkStrSplitAt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| std::shared_ptr< DAGNode > | mkStrSplitRest (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| std::shared_ptr< DAGNode > | mkStrNumSplits (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| std::shared_ptr< DAGNode > | mkStrSplitAtRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| std::shared_ptr< DAGNode > | mkStrSplitRestRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| std::shared_ptr< DAGNode > | mkStrNumSplitsRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| std::shared_ptr< DAGNode > | mkStrLt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a string less-than node. | |
| std::shared_ptr< DAGNode > | mkStrLe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a string less-than-or-equal node. | |
| std::shared_ptr< DAGNode > | mkStrGt (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a string greater-than node. | |
| std::shared_ptr< DAGNode > | mkStrGe (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a string greater-than-or-equal node. | |
| std::shared_ptr< DAGNode > | mkStrInReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string in-regex check node. | |
| std::shared_ptr< DAGNode > | mkStrContains (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string contains check node. | |
| std::shared_ptr< DAGNode > | mkStrIsDigit (std::shared_ptr< DAGNode > param) |
| Create a string is-digit check node. | |
| std::shared_ptr< DAGNode > | mkStrFromInt (std::shared_ptr< DAGNode > param) |
| Create a string from-integer conversion node. | |
| std::shared_ptr< DAGNode > | mkStrToInt (std::shared_ptr< DAGNode > param) |
| Create a string to-integer conversion node. | |
| std::shared_ptr< DAGNode > | mkStrToReg (std::shared_ptr< DAGNode > param) |
| Create a string to-regex conversion node. | |
| std::shared_ptr< DAGNode > | mkStrToCode (std::shared_ptr< DAGNode > param) |
| Create a string to-code conversion node. | |
| std::shared_ptr< DAGNode > | mkStrFromCode (std::shared_ptr< DAGNode > param) |
| Create a string from-code conversion node. | |
| std::shared_ptr< DAGNode > | mkRegNone () |
| Create a regex none node. | |
| std::shared_ptr< DAGNode > | mkRegAll () |
| Create a regex all node. | |
| std::shared_ptr< DAGNode > | mkRegAllChar () |
| Create a regex allchar node. | |
| std::shared_ptr< DAGNode > | mkRegConcat (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a regex concatenation node. | |
| std::shared_ptr< DAGNode > | mkRegUnion (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a regex union node. | |
| std::shared_ptr< DAGNode > | mkRegInter (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a regex intersection node. | |
| std::shared_ptr< DAGNode > | mkRegDiff (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a regex difference node. | |
| std::shared_ptr< DAGNode > | mkRegStar (std::shared_ptr< DAGNode > param) |
| Create a regex star node. | |
| std::shared_ptr< DAGNode > | mkRegPlus (std::shared_ptr< DAGNode > param) |
| Create a regex plus node. | |
| std::shared_ptr< DAGNode > | mkRegOpt (std::shared_ptr< DAGNode > param) |
| Create a regex option node. | |
| std::shared_ptr< DAGNode > | mkRegRange (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a regex range node. | |
| std::shared_ptr< DAGNode > | mkRegRepeat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a regex repeat node. | |
| std::shared_ptr< DAGNode > | mkRegLoop (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s) |
| Create a regex loop node. | |
| std::shared_ptr< DAGNode > | mkRegComplement (std::shared_ptr< DAGNode > param) |
| Create a regex complement node. | |
| std::shared_ptr< DAGNode > | mkReplaceReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace-regex node. | |
| std::shared_ptr< DAGNode > | mkReplaceRegAll (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v) |
| Create a string replace-all-regex node. | |
| std::shared_ptr< DAGNode > | mkIndexofReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r) |
| Create a string index-of-regex node. | |
| std::shared_ptr< DAGNode > | mkMax (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a max node. | |
| std::shared_ptr< DAGNode > | mkMin (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a min node. | |
| std::shared_ptr< DAGNode > | mkLet (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a let node. | |
| std::shared_ptr< DAGNode > | mkQuantVar (const std::string &name, std::shared_ptr< Sort > sort) |
| Create a quantifier variable node. | |
| std::shared_ptr< DAGNode > | mkForall (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a forall node. | |
| std::shared_ptr< DAGNode > | mkExists (const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create an exists node. | |
| std::shared_ptr< DAGNode > | mkApplyFunc (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Create a function application node. | |
| bool | parseSmtlib2File (const std::string filename) |
| Parse an SMT-LIB2 file. | |
| int | getArity (NODE_KIND k) const |
| Get the arity of a node kind. | |
| NODE_KIND | getAddOp (std::shared_ptr< Sort > sort) |
| Get the add operator for a sort. | |
| NODE_KIND | getNegatedKind (NODE_KIND kind) |
| Get the opposite kind of a node kind. | |
| std::shared_ptr< DAGNode > | getZero (std::shared_ptr< Sort > sort) |
| Get the zero for a sort. | |
| std::shared_ptr< DAGNode > | substitute (std::shared_ptr< DAGNode > expr, std::unordered_map< std::string, std::shared_ptr< DAGNode > > ¶ms) |
| Substitute variables in an expression. | |
| std::shared_ptr< DAGNode > | applyFun (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| Apply a function to a list of parameters. | |
| void | setEvaluatePrecision (mpfr_prec_t precision) |
| Set the precision for evaluation. | |
| mpfr_prec_t | getEvaluatePrecision () const |
| Get the precision for evaluation. | |
| void | setEvaluateUseFloating (bool use_floating) |
| Set the use floating for evaluation. | |
| bool | getEvaluateUseFloating () const |
| Get the use floating for evaluation. | |
| Real | toReal (std::shared_ptr< DAGNode > expr) |
| Convert an expression to a real. | |
| Integer | toInt (std::shared_ptr< DAGNode > expr) |
| Convert an expression to an integer. | |
| bool | isZero (std::shared_ptr< DAGNode > expr) |
| Check if an expression is zero. | |
| bool | isOne (std::shared_ptr< DAGNode > expr) |
| Check if an expression is one. | |
| bool | isOnes (std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | expandLet (std::shared_ptr< DAGNode > expr) |
| Expand a let expression. | |
| std::vector< std::shared_ptr< DAGNode > > | getSplitLemmas () |
| Get the split lemmas. | |
| std::shared_ptr< DAGNode > | remove (std::shared_ptr< DAGNode > expr, const std::unordered_set< std::shared_ptr< DAGNode > > &nodes) |
| Remove all the nodes in the expression. | |
| std::shared_ptr< DAGNode > | rename (std::shared_ptr< DAGNode > expr, const std::string &new_name) |
| Rename a node. | |
| std::string | toString (std::shared_ptr< DAGNode > expr) |
| Print an expression. | |
| std::string | toString (const NODE_KIND &kind) |
| Print a node kind. | |
| std::string | toString (std::shared_ptr< Sort > sort) |
| Print a sort. | |
| std::string | optionToString () |
| Print the options. | |
| std::string | dumpSMT2 () |
| Dump the SMT2 representation of the parsed expressions. | |
| std::string | dumpSMT2 (const std::string &filename) |
| Dump the SMT2 representation of the parsed expressions to a file. | |
| std::shared_ptr< DAGNode > | mkApplyDTFun (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > ¶ms) |
| size_t | removeFuns (const std::vector< std::string > &funcNames) |
| Remove functions by name. | |
| void | ensureNumberValue (std::shared_ptr< DAGNode > expr) |
| ensure the expression is a number | |
Static Public Member Functions | |
| static bool | isCommutative (NODE_KIND t) |
| Check whether an operation kind is treated as commutative. | |
| static std::vector< std::shared_ptr< DAGNode > > | sortParams (const std::vector< std::shared_ptr< DAGNode > > &p) |
| Return sorted operand list for deterministic commutative handling. | |
Public Attributes | |
| std::vector< std::shared_ptr< DAGNode > > | assertions |
| std::unordered_map< std::string, std::unordered_set< size_t > > | assertion_groups |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > | named_assertions |
| std::vector< std::pair< std::shared_ptr< DAGNode >, std::vector< std::vector< std::shared_ptr< DAGNode > > > > > | pattern_assertions |
| std::vector< std::vector< std::shared_ptr< DAGNode > > > | assumptions |
| std::vector< std::shared_ptr< DAGNode > > | soft_assertions |
| std::vector< std::shared_ptr< DAGNode > > | soft_weights |
| std::unordered_map< std::string, std::unordered_set< size_t > > | soft_assertion_groups |
| std::vector< std::shared_ptr< DAGNode > > | split_lemmas |
Private Member Functions | |
| std::string | getSymbol () |
| void | scanToNextSymbol () |
| void | parseLpar () |
| void | parseRpar () |
| void | skipToRpar () |
| std::string | peekSymbol () |
| CMD_TYPE | parseCommand () |
| KEYWORD | parseKeyword () |
| std::shared_ptr< Sort > | parseSort () |
| std::shared_ptr< DAGNode > | parseExpr () |
| std::shared_ptr< DAGNode > | parseConstFunc (const std::string &s) |
| std::shared_ptr< DAGNode > | parseOper (const std::string &s, const std::vector< std::shared_ptr< DAGNode > > &func_args, const std::vector< std::shared_ptr< DAGNode > > &oper_params) |
| std::vector< std::shared_ptr< DAGNode > > | parseParams () |
| std::shared_ptr< DAGNode > | parsePreservingLet () |
| std::shared_ptr< DAGNode > | parseLet () |
| std::shared_ptr< DAGNode > | mkLetBindVar (const std::string &name, const std::shared_ptr< DAGNode > &expr) |
| std::shared_ptr< DAGNode > | mkLetBindVarList (const std::vector< std::shared_ptr< DAGNode > > &bind_vars) |
| std::shared_ptr< DAGNode > | mkLetChain (const std::vector< std::shared_ptr< DAGNode > > &bind_var_lists, const std::shared_ptr< DAGNode > &body) |
| std::string | parseGroup () |
| std::string | parseWeight () |
| std::shared_ptr< DAGNode > | parseQuant (const std::string &type) |
| KEYWORD | attemptParseKeywords () |
| std::shared_ptr< DAGNode > | mkInternalOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, const std::vector< std::shared_ptr< DAGNode > > &p) |
| std::shared_ptr< DAGNode > | bindLetVar (const std::string &key, std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | bindFunVar (const std::string &key, std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | substitute (std::shared_ptr< DAGNode > expr, std::unordered_map< std::string, std::shared_ptr< DAGNode > > ¶ms, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited) |
| std::shared_ptr< DAGNode > | applyFunPostOrder (std::shared_ptr< DAGNode > node, std::unordered_map< std::string, std::shared_ptr< DAGNode > > ¶ms) |
| std::shared_ptr< DAGNode > | replaceAtoms (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &atom_map, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited, bool &is_changed) |
| std::shared_ptr< DAGNode > | replaceNodes (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &node_map, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited, bool &is_changed) |
| std::shared_ptr< DAGNode > | toCNF (std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | toTseitinCNF (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited, std::vector< std::shared_ptr< DAGNode > > &clauses) |
| std::shared_ptr< DAGNode > | toTseitinXor (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses) |
| std::shared_ptr< DAGNode > | toTseitinEq (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses) |
| std::shared_ptr< DAGNode > | toTseitinDistinct (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses) |
| std::shared_ptr< DAGNode > | toDNFEliminateAll (std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | toDNFEliminateAll (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited, bool &is_changed) |
| std::shared_ptr< DAGNode > | toDNFEliminateXOR (const std::vector< std::shared_ptr< DAGNode > > &children) |
| std::shared_ptr< DAGNode > | toDNFEliminateEq (const std::vector< std::shared_ptr< DAGNode > > &children) |
| std::shared_ptr< DAGNode > | toDNFEliminateDistinct (const std::vector< std::shared_ptr< DAGNode > > &children) |
| std::shared_ptr< DAGNode > | applyDNFDistributiveLaw (std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | applyDNFDistributiveLawRec (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited) |
| std::shared_ptr< DAGNode > | flattenDNF (std::shared_ptr< DAGNode > expr) |
| std::shared_ptr< DAGNode > | toNNF (std::shared_ptr< DAGNode > expr, bool is_not) |
| std::shared_ptr< DAGNode > | remove (std::shared_ptr< DAGNode > expr, const std::unordered_set< std::shared_ptr< DAGNode > > &nodes, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited) |
| std::shared_ptr< DAGNode > | mkErr (const ERROR_TYPE t) |
| void | err_all (const ERROR_TYPE e, const std::string s="", const size_t ln=0) const |
| void | err_all (const std::shared_ptr< DAGNode > e, const std::string s="", const size_t ln=0) const |
| void | err_unexp_eof () const |
| void | err_sym_mis (const std::string mis, const size_t ln) const |
| void | err_sym_mis (const std::string mis, const std::string nm, const size_t ln) const |
| void | err_unkwn_sym (const std::string nm, const size_t ln) const |
| void | err_param_mis (const std::string nm, const size_t ln) const |
| void | err_param_nbool (const std::string nm, const size_t ln) const |
| void | err_param_nnum (const std::string nm, const size_t ln) const |
| void | err_param_nsame (const std::string nm, const size_t ln) const |
| void | err_logic (const std::string nm, const size_t ln) const |
| void | err_mul_decl (const std::string nm, const size_t ln) const |
| void | err_mul_def (const std::string nm, const size_t ln) const |
| void | err_zero_divisor (const size_t ln) const |
| void | err_arity_mis (const std::string nm, const size_t ln) const |
| void | err_keyword (const std::string nm, const size_t ln) const |
| void | err_type_mis (const std::string nm, const size_t ln) const |
| void | err_neg_param (const size_t ln) const |
| void | err_open_file (const std::string) const |
| void | warn_cmd_nsup (const std::string nm, const size_t ln) const |
| void | collectAtoms (std::shared_ptr< DAGNode > expr, std::unordered_set< std::shared_ptr< DAGNode > > &atoms, std::unordered_set< std::shared_ptr< DAGNode > > &visited) |
| void | collectGroundAtoms (std::shared_ptr< DAGNode > expr, std::unordered_set< std::shared_ptr< DAGNode > > &atoms, std::unordered_set< std::shared_ptr< DAGNode > > &visited) |
| void | collectVars (std::shared_ptr< DAGNode > expr, std::unordered_set< std::shared_ptr< DAGNode > > &vars, std::unordered_set< std::shared_ptr< DAGNode > > &visited) |
Private Attributes | |
| char * | buffer |
| unsigned long | buflen |
| char * | bufptr |
| size_t | line_number |
| SCAN_MODE | scan_mode |
| size_t | preserving_let_counter |
| LET_MODE | current_let_mode |
| size_t | let_nesting_depth |
| size_t | quant_nesting_depth |
| bool | in_quantifier_scope |
| bool | allow_placeholder_vars |
| std::shared_ptr< Sort > | placeholder_var_sort |
| bool | parsing_file |
| std::vector< std::string > | parse_options |
| std::unique_ptr< NodeManager > | node_manager |
| std::unique_ptr< SortManager > | sort_manager |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > | let_key_map |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > | preserving_let_key_map |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > | fun_key_map |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > | fun_var_map |
| std::unordered_map< std::string, std::shared_ptr< Sort > > | sort_key_map |
| std::unordered_map< std::string, std::vector< std::shared_ptr< DAGNode > > > | quant_var_map |
| std::unordered_map< std::string, size_t > | fun_dup_count_map |
| std::vector< std::shared_ptr< DAGNode > > | static_functions |
| std::vector< std::vector< DTTypeDecl > > | datatype_blocks |
| std::unordered_set< std::string > | datatype_sort_names |
| std::unordered_set< std::string > | datatype_function_names |
| std::unordered_map< std::string, size_t > | var_names |
| size_t | temp_var_counter |
| std::unordered_map< std::string, size_t > | temp_var_names |
| std::unordered_map< std::string, size_t > | placeholder_var_names |
| std::vector< std::string > | function_names |
| std::shared_ptr< GlobalOptions > | options |
| std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > | cnf_map |
| std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > | cnf_atom_map |
| std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > | cnf_bool_var_map |
| std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > | dnf_map |
| std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > | nnf_map |
| RESULT_TYPE | result_type |
| std::shared_ptr< DAGNode > | result_node |
| size_t | num_quant_vars = 0 |
| stabilizer::parser::Parser::Parser | ( | const std::string & | filename | ) |
Constructor with filename.
Creates a Parser object and immediately tries to parse the specified SMT-LIB2 file.
| filename | Path to the SMT-LIB2 file to parse |
Definition at line 83 of file base_parser.cpp.
References allow_placeholder_vars, buffer, buflen, bufptr, fun_key_map, fun_var_map, function_names, in_quantifier_scope, let_key_map, let_nesting_depth, line_number, node_manager, options, parseSmtlib2File(), parsing_file, placeholder_var_sort, preserving_let_counter, preserving_let_key_map, quant_nesting_depth, quant_var_map, scan_mode, stabilizer::parser::SM_COMMON, sort_key_map, sort_manager, static_functions, temp_var_counter, temp_var_names, and var_names.
| stabilizer::parser::Parser::Parser | ( | ) |
Default constructor.
Creates an empty Parser object, parse method must be called later to parse a file.
Definition at line 48 of file base_parser.cpp.
References allow_placeholder_vars, buffer, buflen, bufptr, fun_key_map, fun_var_map, function_names, in_quantifier_scope, let_key_map, let_nesting_depth, line_number, node_manager, options, parsing_file, placeholder_var_sort, preserving_let_counter, preserving_let_key_map, quant_nesting_depth, quant_var_map, scan_mode, stabilizer::parser::SM_COMMON, sort_key_map, sort_manager, static_functions, temp_var_counter, temp_var_names, and var_names.
| stabilizer::parser::Parser::~Parser | ( | ) |
Destructor.
Releases all resources used by the Parser
Definition at line 116 of file base_parser.cpp.
|
private |
|
private |
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::applyFun | ( | std::shared_ptr< DAGNode > | fun, |
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Apply a function to a list of parameters.
| fun | Function node |
| params | List of parameters |
Definition at line 2060 of file base_parser.cpp.
References applyFunPostOrder(), datatype_function_names, stabilizer::parser::ERR_PARAM_MIS, mkApplyDTFun(), mkApplyFunc(), mkApplyRecFunc(), mkApplyUF(), mkErr(), node_manager, stabilizer::parser::NT_UF_APPLY, and options.
Referenced by applyFunPostOrder(), and parseOper().
|
private |
Definition at line 2128 of file base_parser.cpp.
References applyFun(), stabilizer::parser::ERR_FUN_LOCAL_VAR, mkApplyDTFun(), mkApplyRecFunc(), mkApplyUF(), mkErr(), mkOper(), and options.
Referenced by applyFun().
| bool stabilizer::parser::Parser::assert | ( | const std::string & | constraint | ) |
Assert a constraint.
Asserts the specified constraint and builds internal data structures.
| constraint | Constraint to assert |
Definition at line 717 of file base_parser.cpp.
References assertions, mkExpr(), and parsing_file.
| bool stabilizer::parser::Parser::assert | ( | std::shared_ptr< DAGNode > | node | ) |
Assert a constraint.
Asserts the specified constraint and builds internal data structures.
| node | Constraint to assert |
Definition at line 724 of file base_parser.cpp.
References assertions.
|
private |
Definition at line 33 of file opt_parser.cpp.
References bufptr, stabilizer::parser::KW_NULL, and parseKeyword().
Referenced by parseCommand(), and parseExpr().
|
private |
|
private |
| RESULT_TYPE stabilizer::parser::Parser::checkSat | ( | ) |
Check satisfiability.
Definition at line 122 of file base_parser.cpp.
References assertions, result_type, stabilizer::parser::RT_ERROR, stabilizer::parser::RT_SAT, stabilizer::parser::RT_UNKNOWN, and stabilizer::parser::RT_UNSAT.
|
inline |
Definition at line 332 of file parser.h.
References preserving_let_key_map.
Referenced by rebuildLetBindings().
|
private |
|
private |
|
private |
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::declareVar | ( | const std::string & | name, |
| const std::shared_ptr< Sort > & | sort | ||
| ) |
Declare a variable.
| name | Variable name |
| sort | Sort |
Definition at line 624 of file op_parser.cpp.
References mkVar().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::declareVar | ( | const std::string & | name, |
| const std::string & | sort | ||
| ) |
Declare a variable.
| name | Variable name |
| sort | Sort |
Definition at line 620 of file op_parser.cpp.
References mkVar(), and sort_key_map.
| std::string stabilizer::parser::Parser::dumpSMT2 | ( | ) |
Dump the SMT2 representation of the parsed expressions.
Definition at line 2851 of file base_parser.cpp.
References assertions, datatype_blocks, stabilizer::parser::dumpFuncDec(), stabilizer::parser::dumpFuncRec(), stabilizer::parser::dumpSMTLIB2(), getFunctions(), getVariables(), options, parse_options, rebuildLetBindings(), and sort_key_map.
Referenced by dumpSMT2().
| std::string stabilizer::parser::Parser::dumpSMT2 | ( | const std::string & | filename | ) |
Dump the SMT2 representation of the parsed expressions to a file.
| filename | Filename to save the SMT2 |
Definition at line 2981 of file base_parser.cpp.
References dumpSMT2().
| void stabilizer::parser::Parser::ensureNumberValue | ( | std::shared_ptr< DAGNode > | expr | ) |
ensure the expression is a number
| expr | Expression to ensure |
Definition at line 336 of file base_parser.cpp.
References err_all(), stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::TypeChecker::isReal(), and line_number.
|
private |
Definition at line 2516 of file base_parser.cpp.
References stabilizer::parser::ERR_ARI_MIS, err_arity_mis(), stabilizer::parser::ERR_FUN_LOCAL_VAR, stabilizer::parser::ERR_LOGIC, err_logic(), stabilizer::parser::ERR_MUL_DECL, err_mul_decl(), stabilizer::parser::ERR_MUL_DEF, err_mul_def(), stabilizer::parser::ERR_NEG_PARAM, err_neg_param(), stabilizer::parser::ERR_PARAM_MIS, err_param_mis(), stabilizer::parser::ERR_PARAM_NBOOL, err_param_nbool(), stabilizer::parser::ERR_PARAM_NNUM, err_param_nnum(), stabilizer::parser::ERR_PARAM_NSAME, err_param_nsame(), stabilizer::parser::ERR_SYM_MIS, err_sym_mis(), stabilizer::parser::ERR_TYPE_MIS, err_type_mis(), stabilizer::parser::ERR_UNEXP_EOF, err_unexp_eof(), stabilizer::parser::ERR_UNKWN_SYM, err_unkwn_sym(), stabilizer::parser::ERR_ZERO_DIVISOR, and err_zero_divisor().
Referenced by ensureNumberValue(), err_all(), mkAbs(), mkAdd(), mkBvAdd(), mkBvAnd(), mkBvAshr(), mkBvConcat(), mkBvExtract(), mkBvLshr(), mkBvMul(), mkBvNot(), mkBvOr(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSdiv(), mkBvSge(), mkBvSgt(), mkBvShl(), mkBvSignExt(), mkBvSle(), mkBvSlt(), mkBvSmod(), mkBvSrem(), mkBvToInt(), mkBvToNat(), mkBvUdiv(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvUmod(), mkBvUrem(), mkBvXor(), mkBvZeroExt(), mkCeil(), mkConstArray(), mkDistinct(), mkDivInt(), mkDivReal(), mkEq(), mkFact(), mkFpAbs(), mkFpAdd(), mkFpConst(), mkFpDiv(), mkFpFma(), mkFpIsInf(), mkFpIsNaN(), mkFpIsNeg(), mkFpIsNormal(), mkFpIsPos(), mkFpIsSubnormal(), mkFpIsZero(), mkFpMul(), mkFpNeg(), mkFpRem(), mkFpRoundToIntegral(), mkFpRoundToIntegral(), mkFpSqrt(), mkFpSqrt(), mkFpSub(), mkFpToReal(), mkFpToSbv(), mkFpToUbv(), mkFuncDef(), mkFuncRec(), mkGcd(), mkGe(), mkGt(), mkIand(), mkImplies(), mkIndexofReg(), mkInfinity(), mkIntToBv(), mkIsDivisible(), mkIsEven(), mkIsInt(), mkIsOdd(), mkIsPrime(), mkIte(), mkLcm(), mkLe(), mkLog(), mkLt(), mkMax(), mkMin(), mkMod(), mkMul(), mkNatToBv(), mkNegInfinity(), mkNot(), mkOper(), mkPosInfinity(), mkRegComplement(), mkRegConcat(), mkRegDiff(), mkRegInter(), mkRegLoop(), mkRegOpt(), mkRegPlus(), mkRegRange(), mkRegRepeat(), mkRegStar(), mkRegUnion(), mkReplaceReg(), mkReplaceRegAll(), mkSafeSqrt(), mkSbvToInt(), mkSelect(), mkSqrt(), mkStrCharat(), mkStrConcat(), mkStrContains(), mkStrFromCode(), mkStrFromInt(), mkStrIndexof(), mkStrIndexofReg(), mkStrInReg(), mkStrIsDigit(), mkStrLen(), mkStrNumSplits(), mkStrNumSplitsRe(), mkStrPrefixof(), mkStrReplace(), mkStrReplaceAll(), mkStrReplaceReg(), mkStrReplaceRegAll(), mkStrRev(), mkStrSplit(), mkStrSplitAt(), mkStrSplitAtRe(), mkStrSplitRest(), mkStrSplitRestRe(), mkStrSubstr(), mkStrSuffixof(), mkStrToCode(), mkStrToInt(), mkStrToLower(), mkStrToReg(), mkStrToUpper(), mkStrUpdate(), mkSub(), mkTempVar(), mkToFp(), mkToFp(), mkToFpUnsigned(), mkToInt(), mkToReal(), mkUbvToInt(), parseCommand(), parseExpr(), parseLet(), parsePreservingLet(), parseSort(), rewrite(), and rewrite().
|
private |
Definition at line 2568 of file base_parser.cpp.
References err_all().
|
private |
Definition at line 2633 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2647 of file base_parser.cpp.
|
private |
Definition at line 2613 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2618 of file base_parser.cpp.
Referenced by err_all(), and parseCommand().
|
private |
Definition at line 2623 of file base_parser.cpp.
Referenced by err_all(), and parseCommand().
|
private |
Definition at line 2642 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2655 of file base_parser.cpp.
Referenced by parseSmtlib2File().
|
private |
Definition at line 2594 of file base_parser.cpp.
Referenced by err_all(), and parseOper().
|
private |
Definition at line 2599 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2603 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2608 of file base_parser.cpp.
Referenced by err_all().
|
private |
Definition at line 2578 of file base_parser.cpp.
Referenced by err_all(), parseLet(), parseLpar(), parsePreservingLet(), and parseRpar().
|
private |
Definition at line 2582 of file base_parser.cpp.
|
private |
Definition at line 2638 of file base_parser.cpp.
|
private |
Definition at line 2573 of file base_parser.cpp.
Referenced by err_all(), err_unkwn_sym(), and getSymbol().
|
private |
Definition at line 2587 of file base_parser.cpp.
References err_unexp_eof().
Referenced by err_all(), parseCommand(), parseConstFunc(), parseExpr(), parseKeyword(), parseOper(), and parseSort().
|
private |
Definition at line 2628 of file base_parser.cpp.
Referenced by err_all().
Expand a let expression.
| expr | Let expression to expand |
|
private |
Get the add operator for a sort.
| sort | Sort |
Definition at line 2467 of file base_parser.cpp.
References stabilizer::parser::NT_ADD, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_ERROR, and stabilizer::parser::NT_FP_ADD.
| int stabilizer::parser::Parser::getArity | ( | NODE_KIND | k | ) | const |
Get the arity of a node kind.
| k | Node kind |
Definition at line 4043 of file op_parser.cpp.
References stabilizer::parser::NT_ABS, stabilizer::parser::NT_ACOS, stabilizer::parser::NT_ACOSH, stabilizer::parser::NT_ACOT, stabilizer::parser::NT_ACOTH, stabilizer::parser::NT_ACSC, stabilizer::parser::NT_ACSCH, stabilizer::parser::NT_ADD, stabilizer::parser::NT_AND, stabilizer::parser::NT_ASEC, stabilizer::parser::NT_ASECH, stabilizer::parser::NT_ASIN, stabilizer::parser::NT_ASINH, stabilizer::parser::NT_ATAN, stabilizer::parser::NT_ATAN2, stabilizer::parser::NT_ATANH, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_BV_AND, stabilizer::parser::NT_BV_ASHR, stabilizer::parser::NT_BV_COMP, stabilizer::parser::NT_BV_CONCAT, stabilizer::parser::NT_BV_EXTRACT, stabilizer::parser::NT_BV_LSHR, stabilizer::parser::NT_BV_MUL, stabilizer::parser::NT_BV_NAND, stabilizer::parser::NT_BV_NEG, stabilizer::parser::NT_BV_NEGO, stabilizer::parser::NT_BV_NOR, stabilizer::parser::NT_BV_NOT, stabilizer::parser::NT_BV_OR, stabilizer::parser::NT_BV_REPEAT, stabilizer::parser::NT_BV_ROTATE_LEFT, stabilizer::parser::NT_BV_ROTATE_RIGHT, stabilizer::parser::NT_BV_SADDO, stabilizer::parser::NT_BV_SDIV, stabilizer::parser::NT_BV_SDIVO, stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SHL, stabilizer::parser::NT_BV_SIGN_EXT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_SMOD, stabilizer::parser::NT_BV_SMODO, stabilizer::parser::NT_BV_SMULO, stabilizer::parser::NT_BV_SREM, stabilizer::parser::NT_BV_SREMO, stabilizer::parser::NT_BV_SUB, stabilizer::parser::NT_BV_TO_INT, stabilizer::parser::NT_BV_TO_NAT, stabilizer::parser::NT_BV_UADDO, stabilizer::parser::NT_BV_UDIV, stabilizer::parser::NT_BV_UDIVO, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_BV_UMOD, stabilizer::parser::NT_BV_UMODO, stabilizer::parser::NT_BV_UMULO, stabilizer::parser::NT_BV_UREM, stabilizer::parser::NT_BV_UREMO, stabilizer::parser::NT_BV_XNOR, stabilizer::parser::NT_BV_XOR, stabilizer::parser::NT_BV_ZERO_EXT, stabilizer::parser::NT_CEIL, stabilizer::parser::NT_CONST, stabilizer::parser::NT_CONST_ARRAY, stabilizer::parser::NT_CONST_E, stabilizer::parser::NT_CONST_FALSE, stabilizer::parser::NT_CONST_PI, stabilizer::parser::NT_CONST_TRUE, stabilizer::parser::NT_COS, stabilizer::parser::NT_COSH, stabilizer::parser::NT_COT, stabilizer::parser::NT_COTH, stabilizer::parser::NT_CSC, stabilizer::parser::NT_CSCH, stabilizer::parser::NT_DISTINCT, stabilizer::parser::NT_DISTINCT_BOOL, stabilizer::parser::NT_DISTINCT_OTHER, stabilizer::parser::NT_DIV_INT, stabilizer::parser::NT_DIV_REAL, stabilizer::parser::NT_EPSILON, stabilizer::parser::NT_EQ, stabilizer::parser::NT_EQ_BOOL, stabilizer::parser::NT_EQ_OTHER, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_EXP, stabilizer::parser::NT_FACT, stabilizer::parser::NT_FLOOR, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ABS, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_DIV, stabilizer::parser::NT_FP_EQ, stabilizer::parser::NT_FP_FMA, stabilizer::parser::NT_FP_GE, stabilizer::parser::NT_FP_GT, stabilizer::parser::NT_FP_IS_INF, stabilizer::parser::NT_FP_IS_NAN, stabilizer::parser::NT_FP_IS_NEG, stabilizer::parser::NT_FP_IS_NORMAL, stabilizer::parser::NT_FP_IS_POS, stabilizer::parser::NT_FP_IS_SUBNORMAL, stabilizer::parser::NT_FP_IS_ZERO, stabilizer::parser::NT_FP_LE, stabilizer::parser::NT_FP_LT, stabilizer::parser::NT_FP_MAX, stabilizer::parser::NT_FP_MIN, stabilizer::parser::NT_FP_MUL, stabilizer::parser::NT_FP_NEG, stabilizer::parser::NT_FP_REM, stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL, stabilizer::parser::NT_FP_SQRT, stabilizer::parser::NT_FP_SUB, stabilizer::parser::NT_FP_TO_FP, stabilizer::parser::NT_FP_TO_REAL, stabilizer::parser::NT_FP_TO_SBV, stabilizer::parser::NT_FP_TO_UBV, stabilizer::parser::NT_GCD, stabilizer::parser::NT_GE, stabilizer::parser::NT_GT, stabilizer::parser::NT_IAND, stabilizer::parser::NT_IMPLIES, stabilizer::parser::NT_INFINITY, stabilizer::parser::NT_INT_TO_BV, stabilizer::parser::NT_IS_DIVISIBLE, stabilizer::parser::NT_IS_EVEN, stabilizer::parser::NT_IS_INT, stabilizer::parser::NT_IS_ODD, stabilizer::parser::NT_IS_PRIME, stabilizer::parser::NT_ITE, stabilizer::parser::NT_LB, stabilizer::parser::NT_LCM, stabilizer::parser::NT_LE, stabilizer::parser::NT_LG, stabilizer::parser::NT_LN, stabilizer::parser::NT_LOG, stabilizer::parser::NT_LT, stabilizer::parser::NT_MAX, stabilizer::parser::NT_MIN, stabilizer::parser::NT_MOD, stabilizer::parser::NT_MUL, stabilizer::parser::NT_NAN, stabilizer::parser::NT_NAT_TO_BV, stabilizer::parser::NT_NEG, stabilizer::parser::NT_NEG_EPSILON, stabilizer::parser::NT_NEG_INFINITY, stabilizer::parser::NT_NOT, stabilizer::parser::NT_NULL, stabilizer::parser::NT_OR, stabilizer::parser::NT_POS_EPSILON, stabilizer::parser::NT_POS_INFINITY, stabilizer::parser::NT_POW, stabilizer::parser::NT_POW2, stabilizer::parser::NT_QUANT_VAR, stabilizer::parser::NT_REG_ALL, stabilizer::parser::NT_REG_ALLCHAR, stabilizer::parser::NT_REG_COMPLEMENT, stabilizer::parser::NT_REG_CONCAT, stabilizer::parser::NT_REG_DIFF, stabilizer::parser::NT_REG_INTER, stabilizer::parser::NT_REG_LOOP, stabilizer::parser::NT_REG_NONE, stabilizer::parser::NT_REG_OPT, stabilizer::parser::NT_REG_PLUS, stabilizer::parser::NT_REG_RANGE, stabilizer::parser::NT_REG_REPEAT, stabilizer::parser::NT_REG_STAR, stabilizer::parser::NT_REG_UNION, stabilizer::parser::NT_ROUND, stabilizer::parser::NT_SAFESQRT, stabilizer::parser::NT_SBV_TO_INT, stabilizer::parser::NT_SEC, stabilizer::parser::NT_SECH, stabilizer::parser::NT_SELECT, stabilizer::parser::NT_SIN, stabilizer::parser::NT_SINH, stabilizer::parser::NT_SQRT, stabilizer::parser::NT_STORE, stabilizer::parser::NT_STR_CHARAT, stabilizer::parser::NT_STR_CONCAT, stabilizer::parser::NT_STR_CONTAINS, stabilizer::parser::NT_STR_FROM_CODE, stabilizer::parser::NT_STR_FROM_INT, stabilizer::parser::NT_STR_GE, stabilizer::parser::NT_STR_GT, stabilizer::parser::NT_STR_IN_REG, stabilizer::parser::NT_STR_INDEXOF, stabilizer::parser::NT_STR_INDEXOF_REG, stabilizer::parser::NT_STR_IS_DIGIT, stabilizer::parser::NT_STR_LE, stabilizer::parser::NT_STR_LEN, stabilizer::parser::NT_STR_LT, stabilizer::parser::NT_STR_NUM_SPLITS_RE, stabilizer::parser::NT_STR_PREFIXOF, 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_REV, stabilizer::parser::NT_STR_SPLIT, stabilizer::parser::NT_STR_SPLIT_AT, stabilizer::parser::NT_STR_SPLIT_AT_RE, stabilizer::parser::NT_STR_SPLIT_REST, stabilizer::parser::NT_STR_SPLIT_REST_RE, stabilizer::parser::NT_STR_SUBSTR, stabilizer::parser::NT_STR_SUFFIXOF, stabilizer::parser::NT_STR_TO_CODE, stabilizer::parser::NT_STR_TO_INT, stabilizer::parser::NT_STR_TO_LOWER, stabilizer::parser::NT_STR_TO_REG, stabilizer::parser::NT_STR_TO_UPPER, stabilizer::parser::NT_STR_UPDATE, stabilizer::parser::NT_SUB, stabilizer::parser::NT_TAN, stabilizer::parser::NT_TANH, stabilizer::parser::NT_TEMP_VAR, stabilizer::parser::NT_TO_INT, stabilizer::parser::NT_TO_REAL, stabilizer::parser::NT_UBV_TO_INT, stabilizer::parser::NT_VAR, and stabilizer::parser::NT_XOR.
Referenced by rewrite_oper().
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getAssertions | ( | ) | const |
Get all assertions.
Definition at line 201 of file base_parser.cpp.
References assertions.
| std::vector< std::vector< std::shared_ptr< DAGNode > > > stabilizer::parser::Parser::getAssumptions | ( | ) | const |
Get assumptions.
Returns a vector of all assumptions. Use (check-sat-assuming (assumptions)) to check satisfiability under the given assumptions.
Definition at line 209 of file base_parser.cpp.
References assumptions.
|
inline |
Definition at line 329 of file parser.h.
References datatype_blocks.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getDeclaredVariables | ( | ) | const |
Get declared variables.
Definition at line 254 of file base_parser.cpp.
References node_manager, and var_names.
| mpfr_prec_t stabilizer::parser::Parser::getEvaluatePrecision | ( | ) | const |
Get the precision for evaluation.
Definition at line 281 of file base_parser.cpp.
References options.
Referenced by toReal().
| bool stabilizer::parser::Parser::getEvaluateUseFloating | ( | ) | const |
|
inline |
Definition at line 325 of file parser.h.
References function_names.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getFunctions | ( | ) | const |
Get functions.
Returns a vector of all functions. Use (define-fun name (params) body) to define a function.
Definition at line 270 of file base_parser.cpp.
References fun_key_map, and function_names.
Referenced by dumpSMT2().
|
inline |
Definition at line 322 of file parser.h.
References fun_key_map.
| std::unordered_map< std::string, std::unordered_set< size_t > > stabilizer::parser::Parser::getGroupedAssertions | ( | ) | const |
Get grouped assertions.
Returns assertion groups map. Use (assert expr :id group_name) to assign assertions to groups. Assertions without an ID go to the default group.
Definition at line 205 of file base_parser.cpp.
References assertion_groups.
| std::unordered_map< std::string, std::unordered_set< size_t > > stabilizer::parser::Parser::getGroupedSoftAssertions | ( | ) | const |
Get grouped soft assertions.
Returns a map of soft assertion groups. Use (assert-soft expr :weight weight :id group_name) to group and weight them.
Definition at line 219 of file base_parser.cpp.
References soft_assertion_groups.
Get kind.
| node | Node |
| NODE_KIND stabilizer::parser::Parser::getKind | ( | const std::string & | s | ) |
Get kind.
| s | String token |
Definition at line 897 of file expr_parser.cpp.
References fun_key_map, stabilizer::parser::getOperKind(), stabilizer::parser::NT_FUNC_APPLY, and stabilizer::parser::NT_UNKNOWN.
Get the opposite kind of a node kind.
| kind | Node kind |
Definition at line 2481 of file base_parser.cpp.
References stabilizer::parser::getNegatedKind().
| size_t stabilizer::parser::Parser::getNodeCount | ( | ) |
Get node count.
Definition at line 157 of file base_parser.cpp.
References assertions, assumptions, soft_assertions, and soft_weights.
|
inline |
Definition at line 764 of file parser.h.
References node_manager.
| std::shared_ptr< GlobalOptions > stabilizer::parser::Parser::getOptions | ( | ) | const |
Get global options.
Definition at line 235 of file base_parser.cpp.
References options.
Referenced by stabilizer::api::SMTStabilizer::configure_parser().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::getResult | ( | ) |
| RESULT_TYPE stabilizer::parser::Parser::getResultType | ( | ) |
Get result type.
Definition at line 118 of file base_parser.cpp.
References result_type.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getSoftAssertions | ( | ) | const |
Get soft assertions.
Returns soft assertions. Use (assert-soft expr :weight weight :id group_name) to group and weight them.
Definition at line 212 of file base_parser.cpp.
References soft_assertions.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getSoftWeights | ( | ) | const |
Get soft assertion weights.
Definition at line 215 of file base_parser.cpp.
References soft_weights.
| std::shared_ptr< Sort > stabilizer::parser::Parser::getSort | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Get sort.
| params | Vector of parameters |
Definition at line 131 of file op_parser.cpp.
References getSort(), stabilizer::parser::SortManager::INT_SORT, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by getSort(), getSort(), getSort(), mkAdd(), mkBvAdd(), mkBvAnd(), mkBvMul(), mkBvNand(), mkBvNor(), mkBvOr(), mkBvSub(), mkBvXnor(), mkBvXor(), mkDistinct(), mkEq(), mkFpAdd(), mkFpDiv(), mkFpFma(), mkFpMax(), mkFpMin(), mkFpMul(), mkFpSub(), mkIand(), mkMax(), mkMin(), mkMul(), mkSub(), and parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::getSort | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Get sort.
| l | Left operand |
| r | Right operand |
Definition at line 162 of file op_parser.cpp.
References getSort().
| std::shared_ptr< Sort > stabilizer::parser::Parser::getSort | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | m | ||
| ) |
Get sort.
| l | First operand |
| r | Second operand |
| m | Third operand |
Definition at line 166 of file op_parser.cpp.
References getSort().
|
inline |
Definition at line 326 of file parser.h.
References sort_key_map.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getSplitLemmas | ( | ) |
Get the split lemmas.
|
private |
Definition at line 367 of file base_parser.cpp.
References buffer, buflen, bufptr, condAssert, err_unexp_eof(), stabilizer::parser::TypeChecker::isBV(), stabilizer::parser::TypeChecker::isFP(), stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::TypeChecker::isNumber(), stabilizer::parser::TypeChecker::isReal(), stabilizer::parser::TypeChecker::isScientificNotation(), stabilizer::parser::TypeChecker::isString(), line_number, parsing_file, scan_mode, scanToNextSymbol(), stabilizer::parser::SM_COMP_SYM, stabilizer::parser::SM_STRING, and stabilizer::parser::SM_SYMBOL.
Referenced by parseCommand(), parseExpr(), parseKeyword(), parseLet(), parsePreservingLet(), parseQuant(), parseSort(), and peekSymbol().
|
inline |
Definition at line 318 of file parser.h.
References temp_var_names.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::getVariable | ( | const std::string & | var_name | ) |
Get variable.
| var_name | Variable name |
Definition at line 261 of file base_parser.cpp.
References node_manager, stabilizer::parser::NodeManager::NULL_NODE, temp_var_names, and var_names.
| std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getVariables | ( | ) | const |
Get variables.
Definition at line 236 of file base_parser.cpp.
References node_manager, temp_var_names, and var_names.
Referenced by dumpSMT2().
|
inline |
Get the zero for a sort.
| sort | Sort |
Definition at line 2484 of file base_parser.cpp.
References stabilizer::parser::ERR_UNKWN_SYM, mkConstBv(), mkConstFp(), mkConstInt(), mkConstReal(), mkConstStr(), and mkErr().
|
static |
Check whether an operation kind is treated as commutative.
Definition at line 84 of file op_parser.cpp.
References stabilizer::parser::NT_ADD, stabilizer::parser::NT_AND, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_BV_AND, stabilizer::parser::NT_BV_COMP, stabilizer::parser::NT_BV_MUL, stabilizer::parser::NT_BV_NAND, stabilizer::parser::NT_BV_NOR, stabilizer::parser::NT_BV_OR, stabilizer::parser::NT_BV_SADDO, stabilizer::parser::NT_BV_UADDO, stabilizer::parser::NT_BV_UMULO, stabilizer::parser::NT_BV_XNOR, stabilizer::parser::NT_BV_XOR, stabilizer::parser::NT_DISTINCT, stabilizer::parser::NT_EQ, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_EQ, stabilizer::parser::NT_FP_MAX, stabilizer::parser::NT_FP_MIN, stabilizer::parser::NT_FP_MUL, stabilizer::parser::NT_IAND, stabilizer::parser::NT_MAX, stabilizer::parser::NT_MIN, stabilizer::parser::NT_MUL, stabilizer::parser::NT_OR, and stabilizer::parser::NT_XOR.
Referenced by mkInternalOper(), and mkNode().
| bool stabilizer::parser::Parser::isDeclaredFunction | ( | const std::string & | func_name | ) | const |
Check if a function is declared.
| func_name | Function name |
Definition at line 2508 of file base_parser.cpp.
References fun_key_map.
| bool stabilizer::parser::Parser::isDeclaredVariable | ( | const std::string & | var_name | ) | const |
Check if a variable is declared.
| var_name | Variable name |
Definition at line 2505 of file base_parser.cpp.
References var_names.
| bool stabilizer::parser::Parser::isOne | ( | std::shared_ptr< DAGNode > | expr | ) |
Check if an expression is one.
| expr | Expression to check |
Definition at line 317 of file base_parser.cpp.
References toInt(), toReal(), and stabilizer::parser::HighPrecisionInteger::toString().
| bool stabilizer::parser::Parser::isOnes | ( | std::shared_ptr< DAGNode > | expr | ) |
Definition at line 328 of file base_parser.cpp.
| bool stabilizer::parser::Parser::isZero | ( | std::shared_ptr< DAGNode > | expr | ) |
Check if an expression is zero.
| expr | Expression to check |
Definition at line 306 of file base_parser.cpp.
References toInt(), toReal(), and stabilizer::parser::HighPrecisionInteger::toString().
Referenced by mkAdd(), mkMul(), mkSub(), rewrite(), rewrite(), and rewrite().
Create an abs node.
| param | Parameter |
Definition at line 1434 of file op_parser.cpp.
References err_all(), stabilizer::parser::isIntParam(), stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_ABS.
Referenced by parseOper().
Create an acos node.
| param | Parameter |
Definition at line 1572 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACOS, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an acosh node.
| param | Parameter |
Definition at line 1644 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACOSH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an acot node.
| param | Parameter |
Definition at line 1596 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACOT, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an acoth node.
| param | Parameter |
Definition at line 1668 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACOTH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an acsc node.
| param | Parameter |
Definition at line 1584 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACSC, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an acsch node.
| param | Parameter |
Definition at line 1662 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ACSCH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAdd | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an add node.
| params | Parameters |
Definition at line 1119 of file op_parser.cpp.
References stabilizer::parser::canExempt(), condAssert, err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::SortManager::INT_SORT, isZero(), line_number, mkConstInt(), mkConstReal(), mkOper(), mkUnknown(), stabilizer::parser::NT_ADD, options, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAnd | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an and node.
| params | Parameters |
Definition at line 927 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_type_mis(), stabilizer::parser::isBoolParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_AND.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkApplyDTFun | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Definition at line 2292 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_UF_APPLY.
Referenced by applyFun(), applyFunPostOrder(), and parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkApplyFunc | ( | std::shared_ptr< DAGNode > | fun, |
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Create a function application node.
| fun | Function node |
| params | List of parameters |
Definition at line 2244 of file base_parser.cpp.
References stabilizer::parser::NT_FUNC_APPLY, and static_functions.
Referenced by applyFun().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkApplyRecFunc | ( | std::shared_ptr< DAGNode > | fun, |
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Create a recursive function application.
| fun | Recursive function symbol node |
| params | Argument list |
Definition at line 2254 of file base_parser.cpp.
References stabilizer::parser::NT_FUNC_REC_APPLY, and static_functions.
Referenced by applyFun(), and applyFunPostOrder().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkApplyUF | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Apply an uninterpreted function.
| sort | Sort |
| name | Function name |
| params | Parameters |
Definition at line 2287 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_UF_APPLY.
Referenced by applyFun(), applyFunPostOrder(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkArray | ( | const std::string & | name, |
| std::shared_ptr< Sort > | index, | ||
| std::shared_ptr< Sort > | elem | ||
| ) |
Create an array.
| name | Array name |
| index | Index sort |
| elem | Element sort |
Definition at line 877 of file op_parser.cpp.
References mkVar(), sort_key_map, and sort_manager.
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkArraySort | ( | std::shared_ptr< Sort > | index, |
| std::shared_ptr< Sort > | elem | ||
| ) |
Create an array sort.
| index | Index sort |
| elem | Element sort |
Definition at line 506 of file op_parser.cpp.
References sort_manager.
Create an asec node.
| param | Parameter |
Definition at line 1578 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ASEC, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an asech node.
| param | Parameter |
Definition at line 1656 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ASECH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an asin node.
| param | Parameter |
Definition at line 1566 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ASIN, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an asinh node.
| param | Parameter |
Definition at line 1638 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ASINH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an atan node.
| param | Parameter |
Definition at line 1590 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ATAN, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAtan2 | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an atan2 node.
| l | Left parameter (y-coordinate) |
| r | Right parameter (x-coordinate) |
Definition at line 1674 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ATAN2, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an atanh node.
| param | Parameter |
Definition at line 1650 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_ATANH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAttribute | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Definition at line 2283 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_ATTRIBUTE.
Referenced by parseExpr().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkBoolSort | ( | ) |
Create a boolean sort.
Definition at line 493 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvAdd | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector addition node.
| params | Parameters |
Definition at line 2071 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_ADD.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvAnd | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector and node.
| params | Parameters |
Definition at line 1933 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isBvParam(), line_number, mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_AND.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvAshr | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector arithmetic shift right node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2228 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_ASHR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvComp | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector comparison node.
| params | Operand list; the first two operands are compared. |
Definition at line 2046 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_BV_COMP, and sort_manager.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvConcat | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector concatenation node.
| params | Parameters |
Definition at line 2240 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_CONCAT, and sort_manager.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvExtract | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Create a bitvector extract node.
Creates a bitvector extract node that extracts a range of bits.
| l | Source bitvector |
| r | Upper index (inclusive) |
| s | Lower index (inclusive) |
Definition at line 2269 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_EXTRACT, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvLshr | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector logical shift right node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2217 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_LSHR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvMul | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector multiplication node.
| params | Parameters |
Definition at line 2111 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_MUL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNand | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector nand node.
| l | Left operand |
| r | Right operand |
Definition at line 2025 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_BV_NAND.
Referenced by parseOper().
Create a bitvector negation node.
| param | Parameter |
Definition at line 2066 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_BV_NEG.
Referenced by parseOper(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNor | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector nor node.
| l | Left operand |
| r | Right operand |
Definition at line 2035 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_BV_NOR.
Referenced by parseOper().
Create a bitvector not node.
| param | Parameter |
Definition at line 1925 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_NOT.
Referenced by parseOper(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvOr | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector or node.
| params | Parameters |
Definition at line 1966 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_OR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvRepeat | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector repeat node.
Creates a bitvector repeat node that repeats the bitvector r times.
| l | Source bitvector |
| r | Repeat count |
Definition at line 2286 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_REPEAT, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvRotateLeft | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector rotate left node.
| l | Source bitvector |
| r | Rotation amount |
Definition at line 2329 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_ROTATE_LEFT, and sort_manager.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvRotateRight | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector rotate right node.
| l | Source bitvector |
| r | Rotation amount |
Definition at line 2344 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_ROTATE_RIGHT, and sort_manager.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSdiv | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed division node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2173 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_SDIV.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSge | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed greater than or equal node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2499 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_SGE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSgt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed greater than node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2478 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_SGT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvShl | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector shift left node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2206 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_SHL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSignExt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector sign extension node.
Creates a bitvector sign extension node that extends the bitvector with r sign bits.
| l | Source bitvector |
| r | Number of bits to extend |
Definition at line 2314 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_SIGN_EXT, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSle | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed less than or equal node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2457 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_SLE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSlt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed less than node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2436 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_SLT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSmod | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed modulo node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2195 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_SMOD.
Referenced by parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkBVSort | ( | const size_t & | width | ) |
Create a bit-vector sort.
| width | Width of the bit-vector |
Definition at line 500 of file op_parser.cpp.
References sort_manager.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSrem | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector signed remainder node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2184 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_SREM.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSub | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector subtraction node.
| l | Left operand |
| r | Right operand |
Definition at line 2099 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_BV_SUB.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvToInt | ( | std::shared_ptr< DAGNode > | param | ) |
Create a bitvector to integer conversion node.
| param | Parameter |
Definition at line 2545 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_TO_INT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvToNat | ( | std::shared_ptr< DAGNode > | param | ) |
Create a bitvector to natural number conversion node.
| param | Parameter |
Definition at line 2521 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_TO_NAT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUdiv | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned division node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2140 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_UDIV.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUge | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned greater than or equal node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2415 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_UGE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUgt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned greater than node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2394 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_UGT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUle | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned less than or equal node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2373 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::BitVectorUtils::bvComp(), err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_BV_ULE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUlt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned less than node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2359 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_ULT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUmod | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned modulo node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2162 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_UMOD.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUrem | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector unsigned remainder node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2151 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_UREM.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvXnor | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector xnor node.
| l | Left operand |
| r | Right operand |
Definition at line 2052 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_BV_XNOR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvXor | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a bitvector xor node.
| params | Parameters |
Definition at line 1996 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isBvParam(), line_number, mkFalse(), mkOper(), mkUnknown(), and stabilizer::parser::NT_BV_XOR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvZeroExt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a bitvector zero extension node.
Creates a bitvector zero extension node that extends the bitvector with r zero bits.
| l | Source bitvector |
| r | Number of bits to extend |
Definition at line 2300 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_BV_ZERO_EXT, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper(), and rewrite().
Create an ceil node.
| param | Parameter |
Definition at line 1466 of file op_parser.cpp.
References err_all(), stabilizer::parser::isIntParam(), stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_CEIL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstArray | ( | std::shared_ptr< Sort > | sort, |
| std::shared_ptr< DAGNode > | value | ||
| ) |
Create a constant array node.
| sort | Array sort |
| value | Constant value for all elements |
Definition at line 898 of file op_parser.cpp.
References err_all(), line_number, mkUnknown(), node_manager, and stabilizer::parser::NT_CONST_ARRAY.
Referenced by parseExpr().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstBv | ( | const std::string & | v, |
| const size_t & | width | ||
| ) |
Create a bit-vector constant.
| v | Value (string) |
| width | Width of the bit-vector |
Definition at line 727 of file op_parser.cpp.
References stabilizer::parser::BitVectorUtils::natToBv(), node_manager, stabilizer::parser::NT_CONST, sort_key_map, and sort_manager.
Referenced by getZero(), mkFpToSbv(), mkFpToUbv(), parseConstFunc(), parseExpr(), rewrite(), rewrite(), rewrite(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstFP | ( | const std::string & | fp_expr | ) |
Create a floating-point constant from expression.
| fp_expr | Floating-point expression string |
Definition at line 758 of file op_parser.cpp.
References node_manager, and stabilizer::parser::NT_CONST.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstFp | ( | const std::string & | v, |
| const size_t & | e, | ||
| const size_t & | s | ||
| ) |
Create a floating-point constant.
| v | Value (string) |
| e | Exponent size |
| s | Significand size |
Definition at line 742 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, sort_key_map, and sort_manager.
Referenced by getZero().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt | ( | const int & | v | ) |
Create an integer constant.
| v | Value (int) |
Definition at line 683 of file op_parser.cpp.
References mkConstInt().
Create an integer constant.
| v | Value (Integer) |
Definition at line 674 of file op_parser.cpp.
References stabilizer::parser::SortManager::INTOREAL_SORT, node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::ConversionUtils::toString().
Create a real constant from number.
Definition at line 686 of file op_parser.cpp.
References mkConstInt(), and stabilizer::parser::Number::toInteger().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt | ( | const std::string & | v | ) |
Create an integer constant from string.
| v | Value (string) |
Definition at line 680 of file op_parser.cpp.
References mkConstInt().
Referenced by getZero(), mkAdd(), mkConstInt(), mkConstInt(), mkConstInt(), mkIand(), mkMul(), mkRootObj(), mkSub(), parseConstFunc(), rewrite(), rewrite(), rewrite(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal | ( | const double & | v | ) |
Create a real constant from double.
| v | Value (double) |
Definition at line 702 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::SortManager::REAL_SORT.
Create a real constant from integer.
| v | Value (Integer) |
Definition at line 706 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, stabilizer::parser::SortManager::REAL_SORT, and stabilizer::parser::ConversionUtils::toString().
Create a real constant from number.
Definition at line 710 of file op_parser.cpp.
References mkConstReal(), and stabilizer::parser::Number::toReal().
Create a real constant.
| v | Value (Real) |
Definition at line 698 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, stabilizer::parser::SortManager::REAL_SORT, and stabilizer::parser::ConversionUtils::toString().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal | ( | const std::string & | v | ) |
Create a real constant from string.
| v | Value (string) |
Definition at line 689 of file op_parser.cpp.
References condAssert, stabilizer::parser::NodeManager::E_NODE, stabilizer::parser::TypeChecker::isReal(), node_manager, stabilizer::parser::NT_CONST, stabilizer::parser::NodeManager::PI_NODE, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by getZero(), mkAdd(), mkConstReal(), mkMul(), mkSub(), parseConstFunc(), rewrite(), rewrite(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReg | ( | const std::string & | v | ) |
Create a regular expression constant.
| v | Value (string) |
Definition at line 761 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::SortManager::REG_SORT.
Referenced by mkRegAll(), mkRegAllChar(), and mkRegNone().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstStr | ( | const std::string & | v | ) |
Create a string constant.
| v | Value (string) |
Definition at line 713 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::SortManager::STR_SORT.
Referenced by getZero(), mkStrConcat(), parseConstFunc(), rewrite(), rewrite(), rewrite(), and rewrite().
Create an cos node.
| param | Parameter |
Definition at line 1536 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_COS, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a cosh node.
| param | Parameter |
Definition at line 1608 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_COSH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a cot node.
| param | Parameter |
Definition at line 1560 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_COT, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a coth node.
| param | Parameter |
Definition at line 1632 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_COTH, and stabilizer::parser::SortManager::REAL_SORT.
Create an csc node.
| param | Parameter |
Definition at line 1548 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_CSC, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a csch node.
| param | Parameter |
Definition at line 1626 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_CSCH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDistinct | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a distinct node.
| params | Parameters |
Definition at line 567 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_PARAM_MIS, getSort(), line_number, mkFalse(), mkOper(), mkUnknown(), and stabilizer::parser::NT_DISTINCT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDiv | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an div node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1404 of file op_parser.cpp.
References mkDivReal().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDivInt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an div node.
| params | Parameters |
Definition at line 1392 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::SortManager::INT_SORT, line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_DIV_INT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDivReal | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an div node.
| params | Parameters |
Definition at line 1409 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_DIV_REAL, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by mkDiv(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkE | ( | ) |
Create a e node.
Definition at line 1788 of file op_parser.cpp.
References stabilizer::parser::NodeManager::E_NODE.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkEpsilon | ( | ) |
Create a epsilon node.
Definition at line 1872 of file op_parser.cpp.
References stabilizer::parser::NodeManager::EPSILON_NODE.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkEq | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an equality node.
| params | Parameters |
Definition at line 513 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_PARAM_MIS, getSort(), line_number, mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_EQ.
Referenced by parseExpr(), parseOper(), and rewrite().
|
private |
Definition at line 2513 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_ERROR.
Referenced by applyFun(), applyFunPostOrder(), getZero(), mkExpr(), mkLetChain(), parseConstFunc(), parseExpr(), parseLet(), parseOper(), and parsePreservingLet().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkExists | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an exists node.
| params | List of (variable, sort) pairs |
Definition at line 2362 of file base_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_EXISTS.
Referenced by parseQuant().
Create an exp node.
| param | Parameter |
Definition at line 1489 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_EXP, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkExpr | ( | const std::string & | expression | ) |
Create a DAG node from a string expression.
Parses the specified string expression and returns the corresponding DAG node.
| expression | String expression to parse |
Definition at line 729 of file base_parser.cpp.
References buffer, buflen, bufptr, stabilizer::parser::ERR_UNEXP_EOF, line_number, mkErr(), parseExpr(), parsing_file, stabilizer::parser::safe_strdup(), and scanToNextSymbol().
Referenced by assert().
Create a factorial node.
| param | Parameter |
Definition at line 1914 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FACT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFalse | ( | ) |
Create a false node.
Definition at line 79 of file op_parser.cpp.
References stabilizer::parser::NodeManager::FALSE_NODE.
Referenced by mkAnd(), mkBvOr(), mkBvSge(), mkBvSgt(), mkBvSle(), mkBvSlt(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvXor(), mkDistinct(), mkOr(), mkXor(), parseConstFunc(), rewrite(), rewrite(), and rewrite().
Create an floor node.
| param | Parameter |
Definition at line 1476 of file op_parser.cpp.
References stabilizer::parser::SortManager::INT_SORT, mkOper(), and stabilizer::parser::NT_FLOOR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkForall | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a forall node.
| params | List of (variable, sort) pairs |
Definition at line 2358 of file base_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FORALL.
Referenced by parseQuant().
Create a floating-point absolute value node.
| param | Parameter |
Definition at line 2758 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_ABS.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpAdd | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point addition node.
| params | Parameters |
Definition at line 2587 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_ADD.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpConst | ( | std::shared_ptr< DAGNode > | sign, |
| std::shared_ptr< DAGNode > | exp, | ||
| std::shared_ptr< DAGNode > | mant | ||
| ) |
Definition at line 3172 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkUnknown(), node_manager, stabilizer::parser::NT_CONST, and sort_manager.
Referenced by parseExpr().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpDiv | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point division node.
| params | Parameters |
Definition at line 2716 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_DIV.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpEq | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point equality node.
| params | Parameters |
Definition at line 2973 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FP_EQ.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpFma | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point fused multiply-add node.
| params | Parameters (should have exactly 3 elements) |
Definition at line 2793 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_FMA.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpGe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point greater than or equal node.
| params | Parameters |
Definition at line 2947 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FP_GE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpGt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point greater than node.
| params | Parameters |
Definition at line 2960 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FP_GT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsInf | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-infinity check node.
| param | Parameter to check |
Definition at line 3237 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_INF.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNaN | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-NaN check node.
| param | Parameter to check |
Definition at line 3248 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_NAN.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNeg | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-negative check node.
| param | Parameter to check |
Definition at line 3259 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_NEG.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNormal | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-normal check node.
| param | Parameter to check |
Definition at line 3203 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_NORMAL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsPos | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-positive check node.
| param | Parameter to check |
Definition at line 3270 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_POS.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsSubnormal | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-subnormal check node.
| param | Parameter to check |
Definition at line 3215 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_SUBNORMAL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsZero | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point is-zero check node.
| param | Parameter to check |
Definition at line 3226 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_IS_ZERO.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpLe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point less than or equal node.
| params | Parameters |
Definition at line 2919 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FP_LE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpLt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point less than node.
| params | Parameters |
Definition at line 2933 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FP_LT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMax | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a floating-point maximum node.
| l | Left operand |
| r | Right operand |
Definition at line 2904 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_FP_MAX.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMin | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a floating-point minimum node.
| l | Left operand |
| r | Right operand |
Definition at line 2891 of file op_parser.cpp.
References getSort(), mkOper(), and stabilizer::parser::NT_FP_MIN.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMul | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point multiplication node.
| params | Parameters |
Definition at line 2673 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_MUL.
Referenced by parseOper().
Create a floating-point negation node.
| param | Parameter |
Definition at line 2769 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_NEG.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpRem | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a floating-point remainder node.
| l | Left parameter |
| r | Right parameter |
Definition at line 2780 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_REM.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpRoundToIntegral | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 2880 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpRoundToIntegral | ( | std::shared_ptr< DAGNode > | rm, |
| std::shared_ptr< DAGNode > | param | ||
| ) |
Create a floating-point round to integral node.
| rm | Rounding mode |
| param | Operand |
Definition at line 2864 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL.
Referenced by parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkFPSort | ( | const size_t & | e, |
| const size_t & | s | ||
| ) |
Create a floating-point sort.
| e | Exponent size |
| s | Significand size |
Definition at line 503 of file op_parser.cpp.
References sort_manager.
Definition at line 2852 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_SQRT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpSqrt | ( | std::shared_ptr< DAGNode > | rm, |
| std::shared_ptr< DAGNode > | param | ||
| ) |
Create a floating-point square root node.
| rm | Rounding mode |
| param | Operand |
Definition at line 2837 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_SQRT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpSub | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a floating-point subtraction node.
| params | Parameters |
Definition at line 2630 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_FP_SUB.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpToReal | ( | std::shared_ptr< DAGNode > | param | ) |
Create a floating-point to real conversion node.
| param | Floating-point value |
Definition at line 3027 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isFpParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_REAL, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpToSbv | ( | std::shared_ptr< DAGNode > | rm, |
| std::shared_ptr< DAGNode > | param, | ||
| std::shared_ptr< DAGNode > | size | ||
| ) |
Create a floating-point to signed bitvector conversion node.
| param | Floating-point value |
| size | Size of resulting bitvector |
Definition at line 3007 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::FloatingPointUtils::fpToSbv(), stabilizer::parser::isFpParam(), stabilizer::parser::isIntParam(), line_number, mkConstBv(), mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_SBV, sort_manager, and toInt().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpToUbv | ( | std::shared_ptr< DAGNode > | rm, |
| std::shared_ptr< DAGNode > | param, | ||
| std::shared_ptr< DAGNode > | size | ||
| ) |
Create a floating-point to unsigned bitvector conversion node.
| param | Floating-point value |
| size | Size of resulting bitvector |
Definition at line 2987 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::FloatingPointUtils::fpToUbv(), stabilizer::parser::isFpParam(), stabilizer::parser::isIntParam(), line_number, mkConstBv(), mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_UBV, sort_manager, and toInt().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFuncDec | ( | const std::string & | name, |
| const std::vector< std::shared_ptr< Sort > > & | params, | ||
| std::shared_ptr< Sort > | out_sort | ||
| ) |
Create a function declaration.
| name | Function name |
| params | Parameters |
| out_sort | Output sort |
Definition at line 346 of file op_parser.cpp.
References fun_dup_count_map, fun_key_map, node_manager, stabilizer::parser::NT_FUNC_DEC, stabilizer::parser::NT_FUNC_PARAM, and stabilizer::parser::NodeManager::NULL_NODE.
Referenced by parseCommand().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFuncDef | ( | const std::string & | name, |
| const std::vector< std::shared_ptr< DAGNode > > & | params, | ||
| std::shared_ptr< Sort > | out_sort, | ||
| std::shared_ptr< DAGNode > | body | ||
| ) |
Create a function definition.
| name | Function name |
| params | Parameters |
| out_sort | Output sort |
| body | Body |
Definition at line 397 of file op_parser.cpp.
References condAssert, err_all(), stabilizer::parser::ERR_MUL_DEF, fun_key_map, line_number, mkUnknown(), node_manager, stabilizer::parser::NT_FUNC_DEC, and stabilizer::parser::NT_FUNC_DEF.
Referenced by parseCommand().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFuncRec | ( | const std::string & | name, |
| const std::vector< std::shared_ptr< DAGNode > > & | params, | ||
| std::shared_ptr< Sort > | out_sort, | ||
| std::shared_ptr< DAGNode > | body | ||
| ) |
Create a recursive function definition.
| name | Function name |
| params | Parameters |
| out_sort | Output sort |
| body | Body |
Definition at line 438 of file op_parser.cpp.
References condAssert, err_all(), stabilizer::parser::ERR_MUL_DEF, fun_key_map, line_number, mkUnknown(), node_manager, stabilizer::parser::NT_FUNC_DEC, and stabilizer::parser::NT_FUNC_REC.
Referenced by parseCommand().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFunParamVar | ( | std::shared_ptr< Sort > | sort, |
| const std::string & | name | ||
| ) |
Create a function parameter variable.
| sort | Sort |
| name | Variable name |
Definition at line 868 of file op_parser.cpp.
References node_manager, and stabilizer::parser::NT_FUNC_PARAM.
Referenced by parseCommand().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGcd | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a gcd node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1892 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_GCD.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a ge node.
| params | Parameters |
Definition at line 1696 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_GE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a gt node.
| params | Parameters |
Definition at line 1706 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_GT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIand | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an iand node.
| params | Parameters |
Definition at line 1273 of file op_parser.cpp.
References stabilizer::parser::canExempt(), condAssert, err_all(), stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::SortManager::INT_SORT, line_number, mkConstInt(), mkOper(), mkUnknown(), stabilizer::parser::NT_IAND, options, stabilizer::parser::SortManager::REAL_SORT, and toInt().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkImplies | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an implies node.
| params | Parameters |
Definition at line 1022 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_IMPLIES.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIndexofReg | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string index-of-regex node.
Creates a node that returns the index of the first match of a regex pattern.
| l | String |
| r | Regex pattern |
Definition at line 3967 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_INDEXOF_REG.
Create a infinity node.
Definition at line 1789 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::NodeManager::INT_INF_NODE, stabilizer::parser::SortManager::INT_SORT, line_number, mkUnknown(), stabilizer::parser::NodeManager::REAL_INF_NODE, stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::NodeManager::STR_INF_NODE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseConstFunc().
|
private |
Definition at line 294 of file op_parser.cpp.
References isCommutative(), stabilizer::parser::kindToString(), node_manager, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_MUL, rewrite_oper(), and sortParams().
Referenced by mkOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkIntSort | ( | ) |
Create an integer sort.
Definition at line 491 of file op_parser.cpp.
References stabilizer::parser::SortManager::INT_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIntToBv | ( | std::shared_ptr< DAGNode > | param, |
| std::shared_ptr< DAGNode > | width | ||
| ) |
Create an integer to bitvector conversion node.
| param | Parameter (integer number) |
| width | Width of the resulting bitvector |
Definition at line 2571 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_INT_TO_BV, sort_manager, and toInt().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsDivisible | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a is_divisible node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1748 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_IS_DIVISIBLE.
Referenced by parseOper().
Create a is_even node.
| param | Parameter |
Definition at line 1769 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_IS_EVEN.
Referenced by parseOper().
Create a is_int node.
| param | Parameter |
Definition at line 1738 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_IS_INT.
Referenced by parseOper().
Create a is_odd node.
| param | Parameter |
Definition at line 1779 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_IS_ODD.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsPrime | ( | std::shared_ptr< DAGNode > | param | ) |
Create a is_prime node.
| param | Parameter |
Definition at line 1759 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_IS_PRIME.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIte | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an ite node.
| params | Parameters |
Definition at line 1108 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkIte(), and mkUnknown().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIte | ( | std::shared_ptr< DAGNode > | cond, |
| std::shared_ptr< DAGNode > | l, | ||
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an ite node.
| cond | Condition |
| l | Left parameter |
| r | Right parameter |
Definition at line 1096 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_ITE.
Referenced by mkIte(), parseExpr(), and parseOper().
Create an lb/log2 node.
| param | Parameter |
Definition at line 1501 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_LB, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLcm | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a lcm node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1903 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_LCM.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a le node.
| params | Parameters |
Definition at line 1680 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_LE.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLet | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a let node.
| params | List of (key, value) pairs |
|
private |
Definition at line 631 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_LET_BIND_VAR, and preserving_let_key_map.
Referenced by parsePreservingLet(), and rebuildLetBindings().
|
private |
Definition at line 648 of file op_parser.cpp.
References node_manager, and stabilizer::parser::NT_LET_BIND_VAR_LIST.
Referenced by parsePreservingLet(), and rebuildLetBindings().
|
private |
Definition at line 658 of file op_parser.cpp.
References stabilizer::parser::ERR_UNKWN_SYM, mkErr(), node_manager, and stabilizer::parser::NT_LET_CHAIN.
Referenced by parsePreservingLet(), and rebuildLetBindings().
Create an lg/log10 node.
| param | Parameter |
Definition at line 1507 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_LG, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create an ln node.
| param | Parameter |
Definition at line 1495 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_LN, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLog | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an log node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1513 of file op_parser.cpp.
References stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_TYPE_MIS, line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_LOG, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a lt node.
| params | Parameters |
Definition at line 1688 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_LT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMax | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a max node.
| params | List of parameters |
Definition at line 3979 of file op_parser.cpp.
References stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_MAX.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMin | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a min node.
| params | List of parameters |
Definition at line 4011 of file op_parser.cpp.
References stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_MIN.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMod | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an mod node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1422 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_MOD.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMul | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an mul node.
| params | Parameters |
Definition at line 1189 of file op_parser.cpp.
References stabilizer::parser::canExempt(), condAssert, err_all(), stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::SortManager::INT_SORT, isOne(), isZero(), line_number, mkConstInt(), mkConstReal(), mkOper(), mkUnknown(), stabilizer::parser::NT_MUL, options, stabilizer::parser::SortManager::REAL_SORT, toInt(), and toReal().
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNaN | ( | std::shared_ptr< Sort > | sort = nullptr | ) |
Create a NaN node.
| sort | Optional sort (for FP types, will include eb sb in name) |
Definition at line 1856 of file op_parser.cpp.
References stabilizer::parser::NodeManager::NAN_NODE, node_manager, and stabilizer::parser::NT_NAN.
Referenced by parseConstFunc(), and parseExpr().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkNatSort | ( | ) |
Create a natural sort.
Definition at line 499 of file op_parser.cpp.
References stabilizer::parser::SortManager::NAT_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNatToBv | ( | std::shared_ptr< DAGNode > | param, |
| std::shared_ptr< DAGNode > | width | ||
| ) |
Create a natural number to bitvector conversion node.
| param | Parameter (natural number) |
| width | Width of the resulting bitvector |
Definition at line 2532 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_NAT_TO_BV, sort_manager, and toInt().
Referenced by parseOper().
Create an neg node.
| param | Parameter |
Definition at line 1387 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_NEG.
Referenced by mkSub(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNegEpsilon | ( | ) |
Create a negative epsilon node.
Definition at line 1878 of file op_parser.cpp.
References stabilizer::parser::NodeManager::NEG_EPSILON_NODE.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNegInfinity | ( | std::shared_ptr< Sort > | sort = nullptr | ) |
Create a negative infinity node.
| sort | Optional sort (for FP types, will include eb sb in name) |
Definition at line 1830 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::NodeManager::INT_NEG_INF_NODE, stabilizer::parser::SortManager::INT_SORT, line_number, mkUnknown(), node_manager, stabilizer::parser::NT_NEG_INFINITY, stabilizer::parser::NodeManager::REAL_NEG_INF_NODE, stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::NodeManager::STR_NEG_INF_NODE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseConstFunc(), and parseExpr().
|
inline |
Definition at line 771 of file parser.h.
References isCommutative(), node_manager, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_MUL, rewrite_oper(), and sortParams().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNoPattern | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| std::shared_ptr< DAGNode > | param | ||
| ) |
Definition at line 2270 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_NO_PATTERN.
Referenced by parseExpr().
Create a not node.
| param | Parameter |
Definition at line 916 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::isBoolParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_NOT.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOper | ( | const std::shared_ptr< Sort > & | sort, |
| const NODE_KIND & | t, | ||
| const std::vector< std::shared_ptr< DAGNode > > & | p | ||
| ) |
Create an operation.
| sort | Sort |
| t | Operation kind |
| p | Parameters |
Definition at line 233 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkInternalOper(), mkUnknown(), stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_GE, stabilizer::parser::NT_FP_GT, stabilizer::parser::NT_FP_LE, stabilizer::parser::NT_FP_LT, stabilizer::parser::NT_GE, stabilizer::parser::NT_GT, stabilizer::parser::NT_LE, stabilizer::parser::NT_LT, stabilizer::parser::NT_STR_GE, stabilizer::parser::NT_STR_GT, stabilizer::parser::NT_STR_LE, and stabilizer::parser::NT_STR_LT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOper | ( | const std::shared_ptr< Sort > & | sort, |
| const NODE_KIND & | t, | ||
| std::shared_ptr< DAGNode > | l, | ||
| std::shared_ptr< DAGNode > | m, | ||
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an operation.
| sort | Sort |
| t | Operation kind |
| l | Left parameter |
| m | Middle parameter |
| r | Right parameter |
Definition at line 221 of file op_parser.cpp.
References mkOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOper | ( | const std::shared_ptr< Sort > & | sort, |
| const NODE_KIND & | t, | ||
| std::shared_ptr< DAGNode > | l, | ||
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an operation.
| sort | Sort |
| t | Operation kind |
| l | Left parameter |
| r | Right parameter |
Definition at line 212 of file op_parser.cpp.
References mkOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOper | ( | const std::shared_ptr< Sort > & | sort, |
| const NODE_KIND & | t, | ||
| std::shared_ptr< DAGNode > | p | ||
| ) |
Create an operation.
| sort | Sort |
| t | Operation kind |
| p | Parameters |
Definition at line 205 of file op_parser.cpp.
References mkOper().
Referenced by applyFunPostOrder(), mkAbs(), mkAcos(), mkAcosh(), mkAcot(), mkAcoth(), mkAcsc(), mkAcsch(), mkAdd(), mkAnd(), mkAsec(), mkAsech(), mkAsin(), mkAsinh(), mkAtan(), mkAtan2(), mkAtanh(), mkBvAdd(), mkBvAnd(), mkBvAshr(), mkBvComp(), mkBvConcat(), mkBvExtract(), mkBvLshr(), mkBvMul(), mkBvNand(), mkBvNeg(), mkBvNor(), mkBvNot(), mkBvOr(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSdiv(), mkBvSge(), mkBvSgt(), mkBvShl(), mkBvSignExt(), mkBvSle(), mkBvSlt(), mkBvSmod(), mkBvSrem(), mkBvSub(), mkBvToInt(), mkBvToNat(), mkBvUdiv(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvUmod(), mkBvUrem(), mkBvXnor(), mkBvXor(), mkBvZeroExt(), mkCeil(), mkCos(), mkCosh(), mkCot(), mkCoth(), mkCsc(), mkCsch(), mkDistinct(), mkDivInt(), mkDivReal(), mkEq(), mkExists(), mkExp(), mkFact(), mkFloor(), mkForall(), mkFpAbs(), mkFpAdd(), mkFpDiv(), mkFpEq(), mkFpFma(), mkFpGe(), mkFpGt(), mkFpIsInf(), mkFpIsNaN(), mkFpIsNeg(), mkFpIsNormal(), mkFpIsPos(), mkFpIsSubnormal(), mkFpIsZero(), mkFpLe(), mkFpLt(), mkFpMax(), mkFpMin(), mkFpMul(), mkFpNeg(), mkFpRem(), mkFpRoundToIntegral(), mkFpRoundToIntegral(), mkFpSqrt(), mkFpSqrt(), mkFpSub(), mkFpToReal(), mkFpToSbv(), mkFpToUbv(), mkGcd(), mkGe(), mkGt(), mkIand(), mkImplies(), mkIndexofReg(), mkIntToBv(), mkIsDivisible(), mkIsEven(), mkIsInt(), mkIsOdd(), mkIsPrime(), mkIte(), mkLb(), mkLcm(), mkLe(), mkLg(), mkLn(), mkLog(), mkLt(), mkMax(), mkMin(), mkMod(), mkMul(), mkNatToBv(), mkNeg(), mkNot(), mkOper(), mkOper(), mkOper(), mkOr(), mkPow(), mkPow2(), mkRegComplement(), mkRegConcat(), mkRegDiff(), mkRegInter(), mkRegLoop(), mkRegOpt(), mkRegPlus(), mkRegRange(), mkRegRepeat(), mkRegStar(), mkRegUnion(), mkReplaceReg(), mkReplaceRegAll(), mkRound(), mkSafeSqrt(), mkSbvToInt(), mkSec(), mkSech(), mkSelect(), mkSin(), mkSinh(), mkSqrt(), mkStore(), mkStrCharat(), mkStrConcat(), mkStrContains(), mkStrFromCode(), mkStrFromInt(), mkStrGe(), mkStrGt(), mkStrIndexof(), mkStrIndexofReg(), mkStrInReg(), mkStrIsDigit(), mkStrLe(), mkStrLen(), mkStrLt(), mkStrNumSplits(), mkStrNumSplitsRe(), mkStrPrefixof(), mkStrReplace(), mkStrReplaceAll(), mkStrReplaceReg(), mkStrReplaceRegAll(), mkStrRev(), mkStrSplit(), mkStrSplitAt(), mkStrSplitAtRe(), mkStrSplitRest(), mkStrSplitRestRe(), mkStrSubstr(), mkStrSuffixof(), mkStrToCode(), mkStrToInt(), mkStrToLower(), mkStrToReg(), mkStrToUpper(), mkStrUpdate(), mkSub(), mkTan(), mkTanh(), mkToFp(), mkToFp(), mkToFpUnsigned(), mkToInt(), mkToReal(), mkUbvToInt(), mkXor(), and substitute().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOr | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an or node.
| params | Parameters |
Definition at line 975 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_type_mis(), stabilizer::parser::isBoolParam(), line_number, mkFalse(), mkOper(), mkTrue(), mkUnknown(), and stabilizer::parser::NT_OR.
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPattern | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| const std::vector< std::shared_ptr< DAGNode > > & | params | ||
| ) |
Definition at line 2266 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_PATTERN.
Referenced by parseExpr().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPi | ( | ) |
Create a pi node.
Definition at line 1787 of file op_parser.cpp.
References stabilizer::parser::NodeManager::PI_NODE.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPlaceholderVar | ( | const std::string & | name | ) |
Definition at line 799 of file op_parser.cpp.
References condAssert, node_manager, stabilizer::parser::NT_PLACEHOLDER_VAR, placeholder_var_names, placeholder_var_sort, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPosEpsilon | ( | ) |
Create a positive epsilon node.
Definition at line 1875 of file op_parser.cpp.
References stabilizer::parser::NodeManager::POS_EPSILON_NODE.
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPosInfinity | ( | std::shared_ptr< Sort > | sort = nullptr | ) |
Create a positive infinity node.
| sort | Optional sort (for FP types, will include eb sb in name) |
Definition at line 1804 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::NodeManager::INT_POS_INF_NODE, stabilizer::parser::SortManager::INT_SORT, line_number, mkUnknown(), node_manager, stabilizer::parser::NT_POS_INFINITY, stabilizer::parser::NodeManager::REAL_POS_INF_NODE, stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::NodeManager::STR_POS_INF_NODE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseConstFunc(), and parseExpr().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPow | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an pow node.
| l | Left parameter |
| r | Right parameter |
Definition at line 1321 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_POW.
Referenced by parseOper().
Create an pow2 node.
| param | Parameter |
Definition at line 1318 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_POW2.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkQuantVar | ( | const std::string & | name, |
| std::shared_ptr< Sort > | sort | ||
| ) |
Create a quantifier variable node.
| name | Variable name |
| sort | Variable sort |
Definition at line 2298 of file base_parser.cpp.
References node_manager, stabilizer::parser::NT_QUANT_VAR, num_quant_vars, and quant_var_map.
Referenced by parseQuant().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkRealSort | ( | ) |
Create a real sort.
Definition at line 492 of file op_parser.cpp.
References stabilizer::parser::SortManager::REAL_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegAll | ( | ) |
Create a regex all node.
Creates a regex node that matches any string.
Definition at line 3746 of file op_parser.cpp.
References mkConstReg().
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegAllChar | ( | ) |
Create a regex allchar node.
Creates a regex node that matches any single character.
Definition at line 3747 of file op_parser.cpp.
References mkConstReg().
Referenced by parseConstFunc().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegComplement | ( | std::shared_ptr< DAGNode > | param | ) |
Create a regex complement node.
Creates a regex complement node that matches strings not matching the pattern.
| param | Regex pattern |
Definition at line 3925 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_COMPLEMENT, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegConcat | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a regex concatenation node.
Creates a regex concatenation node that matches the concatenation of patterns.
| params | Regex patterns |
Definition at line 3755 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_CONCAT, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegDiff | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a regex difference node.
Creates a regex difference node that matches strings matching the first pattern but not subsequent patterns.
| params | Regex patterns |
Definition at line 3833 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_DIFF, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegInter | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a regex intersection node.
Creates a regex intersection node that matches strings that match all patterns.
| params | Regex patterns |
Definition at line 3807 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_INTER, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegLoop | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Create a regex loop node.
Creates a regex loop node that matches between r and s occurrences of the pattern.
| l | Regex pattern |
| r | Minimum number of repetitions |
| s | Maximum number of repetitions |
Definition at line 3909 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_LOOP, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegNone | ( | ) |
Create a regex none node.
Creates a regex node that matches nothing.
Definition at line 3745 of file op_parser.cpp.
References mkConstReg().
Referenced by parseConstFunc().
Create a regex option node.
Creates a regex option node that matches zero or one occurrence of the pattern.
| param | Regex pattern |
Definition at line 3872 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_OPT, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegPlus | ( | std::shared_ptr< DAGNode > | param | ) |
Create a regex plus node.
Creates a regex plus node that matches one or more occurrences of the pattern.
| param | Regex pattern |
Definition at line 3861 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_PLUS, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegRange | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a regex range node.
Creates a regex range node that matches characters in the specified range.
| l | Lower bound (inclusive) |
| r | Upper bound (inclusive) |
Definition at line 3883 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_RANGE, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegRepeat | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a regex repeat node.
Creates a regex repeat node that matches exactly r occurrences of the pattern.
| l | Regex pattern |
| r | Number of repetitions |
Definition at line 3895 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_REPEAT, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkRegSort | ( | ) |
Create a regular expression sort.
Definition at line 495 of file op_parser.cpp.
References stabilizer::parser::SortManager::REG_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegStar | ( | std::shared_ptr< DAGNode > | param | ) |
Create a regex star node.
Creates a regex star node that matches zero or more occurrences of the pattern.
| param | Regex pattern |
Definition at line 3850 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_STAR, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegUnion | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a regex union node.
Creates a regex union node that matches any of the patterns.
| params | Regex patterns |
Definition at line 3781 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_REG_UNION, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkReplaceReg | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace-regex node.
Creates a node that replaces the first match of a regex pattern.
| l | String |
| r | Regex pattern |
| v | Replacement string |
Definition at line 3937 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_REPLACE_REG, and stabilizer::parser::SortManager::STR_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkReplaceRegAll | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace-all-regex node.
Creates a node that replaces all matches of a regex pattern.
| l | String |
| r | Regex pattern |
| v | Replacement string |
Definition at line 3952 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_REPLACE_REG_ALL, and stabilizer::parser::SortManager::STR_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRootObj | ( | std::shared_ptr< DAGNode > | expr, |
| int | index | ||
| ) |
Definition at line 4295 of file op_parser.cpp.
References mkConstInt(), node_manager, stabilizer::parser::NT_ROOT_OBJ, stabilizer::parser::SortManager::REAL_SORT, and toString().
Referenced by parseExpr(), and parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRootOfWithInterval | ( | const std::vector< std::shared_ptr< DAGNode > > & | coeffs, |
| std::shared_ptr< DAGNode > | lower_bound, | ||
| std::shared_ptr< DAGNode > | upper_bound | ||
| ) |
Definition at line 4312 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_ROOT_OF_WITH_INTERVAL, stabilizer::parser::SortManager::REAL_SORT, and toString().
Referenced by parseExpr().
Create an round node.
| param | Parameter |
Definition at line 1482 of file op_parser.cpp.
References stabilizer::parser::SortManager::INT_SORT, mkOper(), and stabilizer::parser::NT_ROUND.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRoundingMode | ( | const std::string & | mode | ) |
Create a rounding mode constant.
| mode | Rounding mode string (RNE, RNA, RTP, RTN, RTZ) |
Definition at line 765 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::SortManager::ROUNDING_MODE_SORT.
Referenced by parseConstFunc().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkRoundingModeSort | ( | ) |
Create a rounding mode sort.
Definition at line 496 of file op_parser.cpp.
References stabilizer::parser::SortManager::ROUNDING_MODE_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSafeSqrt | ( | std::shared_ptr< DAGNode > | param | ) |
Create an safeSqrt node.
| param | Parameter |
Definition at line 1456 of file op_parser.cpp.
References err_all(), stabilizer::parser::isIntParam(), stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_SAFESQRT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSbvToInt | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 2561 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_SBV_TO_INT.
Create an sec node.
| param | Parameter |
Definition at line 1542 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_SEC, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a sech node.
| param | Parameter |
Definition at line 1620 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_SECH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSelect | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create an array select node.
| l | Array |
| r | Index |
Definition at line 3282 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isArrayParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_SELECT.
Referenced by parseOper().
Create an sin node.
| param | Parameter |
Definition at line 1530 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_SIN, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a sinh node.
| param | Parameter |
Definition at line 1602 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_SINH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkSortDec | ( | const std::string & | name, |
| const size_t & | arity | ||
| ) |
Create a sort declaration.
| name | Sort name |
| arity | Arity |
Definition at line 480 of file op_parser.cpp.
References sort_manager.
Referenced by parseCommand().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkSortDef | ( | const std::string & | name, |
| const std::vector< std::shared_ptr< Sort > > & | params, | ||
| std::shared_ptr< Sort > | out_sort | ||
| ) |
Create a sort definition.
| name | Sort name |
| params | Parameters |
| out_sort | Output sort |
Definition at line 486 of file op_parser.cpp.
References sort_manager.
Referenced by parseCommand().
Create an sqrt node.
| param | Parameter |
Definition at line 1445 of file op_parser.cpp.
References err_all(), stabilizer::parser::isIntParam(), stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_SQRT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStore | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create an array store node.
| l | Array |
| r | Index |
| v | Value |
Definition at line 3294 of file op_parser.cpp.
References mkOper(), and stabilizer::parser::NT_STORE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrCharat | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string char-at node.
| l | String |
| r | Index |
Definition at line 3405 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_CHARAT, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrConcat | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a string concatenation node.
| params | Strings to concatenate |
Definition at line 3322 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkConstStr(), mkOper(), mkUnknown(), stabilizer::parser::NT_STR_CONCAT, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrContains | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string contains check node.
| l | String |
| r | Substring |
Definition at line 3671 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_CONTAINS.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrFromCode | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string from-code conversion node.
Creates a node that converts an ASCII code to a string.
| param | ASCII code |
Definition at line 3736 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_FROM_CODE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrFromInt | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string from-integer conversion node.
| param | Integer |
Definition at line 3692 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_FROM_INT, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrGe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a string greater-than-or-equal node.
| params | Operand list containing two strings |
Definition at line 3648 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_STR_GE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrGt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a string greater-than node.
| params | Operand list containing two strings |
Definition at line 3641 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_STR_GT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrIndexof | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Create a string index-of node.
| l | String |
| r | Substring to find |
| s | Start index |
Definition at line 3390 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_INDEXOF.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrIndexofReg | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string indexof-regex node.
| l | String |
| r | Regular expression |
Definition at line 3498 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_INDEXOF_REG.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrInReg | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string in-regex check node.
| l | String |
| r | Regular expression |
Definition at line 3656 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_IN_REG.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrIsDigit | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string is-digit check node.
| param | String |
Definition at line 3683 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_IS_DIGIT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrLe | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a string less-than-or-equal node.
| params | Operand list containing two strings |
Definition at line 3634 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_STR_LE.
Referenced by parseOper().
Create a string length node.
| param | String |
Definition at line 3310 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_LEN.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrLt | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create a string less-than node.
| params | Operand list containing two strings |
Definition at line 3623 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_STR_LT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrNumSplits | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Definition at line 3575 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_NUM_SPLITS.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrNumSplitsRe | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Definition at line 3610 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_NUM_SPLITS_RE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrPrefixof | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string prefix check node.
| l | Prefix |
| r | String |
Definition at line 3366 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_PREFIXOF.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrReplace | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace node.
| l | String |
| r | Substring to replace |
| v | Replacement string |
Definition at line 3432 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_REPLACE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrReplaceAll | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace-all node.
| l | String |
| r | Substring to replace |
| v | Replacement string |
Definition at line 3447 of file op_parser.cpp.
References err_all(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_REPLACE_ALL.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrReplaceReg | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace-regex node.
| l | String |
| r | Regular expression |
| v | Replacement string |
Definition at line 3467 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_REPLACE_REG.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrReplaceRegAll | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string replace-regex-all node.
| l | String |
| r | Regular expression |
| v | Replacement string |
Definition at line 3483 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_REPLACE_REG_ALL.
Referenced by parseOper().
Create a string reverse node.
| param | String |
Definition at line 3534 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_REV, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< Sort > stabilizer::parser::Parser::mkStrSort | ( | ) |
Create a string sort.
Definition at line 494 of file op_parser.cpp.
References stabilizer::parser::SortManager::STR_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplit | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string split node.
| l | String |
| r | Delimiter |
Definition at line 3545 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_SPLIT, sort_manager, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitAt | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Definition at line 3557 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_SPLIT_AT, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitAtRe | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Definition at line 3586 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_SPLIT_AT_RE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitRest | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Definition at line 3566 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_SPLIT_REST, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitRestRe | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Definition at line 3598 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isRegParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_SPLIT_REST_RE, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSubstr | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | s | ||
| ) |
Create a string substring node.
| l | String |
| r | Start index |
| s | Length |
Definition at line 3351 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_SUBSTR.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSuffixof | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r | ||
| ) |
Create a string suffix check node.
| l | Suffix |
| r | String |
Definition at line 3378 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_SUFFIXOF.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToCode | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string to-code conversion node.
Creates a node that converts a string to its ASCII code.
| param | String |
Definition at line 3725 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_TO_CODE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToInt | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string to-integer conversion node.
| param | String |
Definition at line 3703 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_TO_INT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToLower | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string to-lower node.
| param | String |
Definition at line 3512 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_TO_LOWER, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToReg | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string to-regex conversion node.
| param | String |
Definition at line 3714 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_TO_REG, and stabilizer::parser::SortManager::REG_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToUpper | ( | std::shared_ptr< DAGNode > | param | ) |
Create a string to-upper node.
| param | String |
Definition at line 3523 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_STR_TO_UPPER, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrUpdate | ( | std::shared_ptr< DAGNode > | l, |
| std::shared_ptr< DAGNode > | r, | ||
| std::shared_ptr< DAGNode > | v | ||
| ) |
Create a string update node.
| l | String |
| r | Index |
| v | New character |
Definition at line 3417 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), stabilizer::parser::isStrParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_STR_UPDATE.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSub | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an sub node.
| params | Parameters |
Definition at line 1327 of file op_parser.cpp.
References stabilizer::parser::canExempt(), err_all(), stabilizer::parser::ERR_PARAM_MIS, stabilizer::parser::ERR_TYPE_MIS, getSort(), stabilizer::parser::SortManager::INT_SORT, isZero(), line_number, mkConstInt(), mkConstReal(), mkNeg(), mkOper(), mkUnknown(), stabilizer::parser::NT_SUB, options, stabilizer::parser::SortManager::REAL_SORT, toInt(), and toReal().
Referenced by parseExpr(), and parseOper().
Create an tan node.
| param | Parameter |
Definition at line 1554 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_TAN, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
Create a tanh node.
| param | Parameter |
Definition at line 1614 of file op_parser.cpp.
References mkOper(), stabilizer::parser::NT_TANH, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTempVar | ( | const std::shared_ptr< Sort > & | sort | ) |
Create a temporary variable.
| sort | Sort |
Definition at line 772 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkUnknown(), node_manager, stabilizer::parser::NT_TEMP_VAR, temp_var_counter, and temp_var_names.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToFp | ( | std::shared_ptr< DAGNode > | eb, |
| std::shared_ptr< DAGNode > | sb, | ||
| std::shared_ptr< DAGNode > | param | ||
| ) |
Definition at line 3091 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_FP, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToFp | ( | std::shared_ptr< DAGNode > | eb, |
| std::shared_ptr< DAGNode > | sb, | ||
| std::shared_ptr< DAGNode > | rm, | ||
| std::shared_ptr< DAGNode > | param | ||
| ) |
Create a value to floating-point conversion node.
| eb | Exponent bit width |
| sb | Significand bit width |
| param | Value to convert |
Definition at line 3044 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), stabilizer::parser::isFpParam(), stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_FP, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToFpUnsigned | ( | std::shared_ptr< DAGNode > | eb, |
| std::shared_ptr< DAGNode > | sb, | ||
| std::shared_ptr< DAGNode > | rm, | ||
| std::shared_ptr< DAGNode > | param | ||
| ) |
Definition at line 3129 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_FP_TO_FP_UNSIGNED, sort_manager, toInt(), and stabilizer::parser::HighPrecisionInteger::toULong().
Referenced by parseOper().
Create a to_int node.
| param | Parameter |
Definition at line 1717 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isRealParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_TO_INT.
Referenced by parseOper().
Create a to_real node.
| param | Parameter |
Definition at line 1727 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::isIntParam(), line_number, mkOper(), mkUnknown(), stabilizer::parser::NT_TO_REAL, and stabilizer::parser::SortManager::REAL_SORT.
Referenced by parseOper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTrue | ( | ) |
Create a true node.
Definition at line 78 of file op_parser.cpp.
References stabilizer::parser::NodeManager::TRUE_NODE.
Referenced by mkAnd(), mkBvAnd(), mkBvSge(), mkBvSgt(), mkBvSle(), mkBvSlt(), mkBvUge(), mkBvUgt(), mkBvUle(), mkEq(), mkImplies(), mkOr(), parseConstFunc(), rewrite(), rewrite(), and rewrite().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkUbvToInt | ( | std::shared_ptr< DAGNode > | param | ) |
Definition at line 2553 of file op_parser.cpp.
References err_all(), stabilizer::parser::ERR_TYPE_MIS, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::isBvParam(), line_number, mkOper(), mkUnknown(), and stabilizer::parser::NT_UBV_TO_INT.
Referenced by parseOper().
|
inline |
Definition at line 311 of file parser.h.
References node_manager, and stabilizer::parser::NT_UF_NAME.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkUnknown | ( | ) |
Create an unknown node.
Definition at line 80 of file op_parser.cpp.
References stabilizer::parser::NodeManager::UNKNOWN_NODE.
Referenced by mkAbs(), mkAdd(), mkAnd(), mkBvAdd(), mkBvAnd(), mkBvAshr(), mkBvConcat(), mkBvExtract(), mkBvLshr(), mkBvMul(), mkBvNot(), mkBvOr(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSdiv(), mkBvSge(), mkBvSgt(), mkBvShl(), mkBvSignExt(), mkBvSle(), mkBvSlt(), mkBvSmod(), mkBvSrem(), mkBvToInt(), mkBvToNat(), mkBvUdiv(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvUmod(), mkBvUrem(), mkBvXor(), mkBvZeroExt(), mkCeil(), mkConstArray(), mkDistinct(), mkDivInt(), mkDivReal(), mkEq(), mkFact(), mkFpAbs(), mkFpAdd(), mkFpConst(), mkFpDiv(), mkFpFma(), mkFpIsInf(), mkFpIsNaN(), mkFpIsNeg(), mkFpIsNormal(), mkFpIsPos(), mkFpIsSubnormal(), mkFpIsZero(), mkFpMul(), mkFpNeg(), mkFpRem(), mkFpRoundToIntegral(), mkFpRoundToIntegral(), mkFpSqrt(), mkFpSqrt(), mkFpSub(), mkFpToReal(), mkFpToSbv(), mkFpToUbv(), mkFuncDef(), mkFuncRec(), mkGcd(), mkGe(), mkGt(), mkIand(), mkImplies(), mkIndexofReg(), mkInfinity(), mkIntToBv(), mkIsDivisible(), mkIsEven(), mkIsInt(), mkIsOdd(), mkIsPrime(), mkIte(), mkLcm(), mkLe(), mkLog(), mkLt(), mkMax(), mkMin(), mkMod(), mkMul(), mkNatToBv(), mkNegInfinity(), mkNot(), mkOper(), mkOr(), mkPosInfinity(), mkRegComplement(), mkRegConcat(), mkRegDiff(), mkRegInter(), mkRegLoop(), mkRegOpt(), mkRegPlus(), mkRegRange(), mkRegRepeat(), mkRegStar(), mkRegUnion(), mkReplaceReg(), mkReplaceRegAll(), mkSafeSqrt(), mkSbvToInt(), mkSelect(), mkSqrt(), mkStrCharat(), mkStrConcat(), mkStrContains(), mkStrFromCode(), mkStrFromInt(), mkStrIndexof(), mkStrIndexofReg(), mkStrInReg(), mkStrIsDigit(), mkStrLen(), mkStrNumSplits(), mkStrNumSplitsRe(), mkStrPrefixof(), mkStrReplace(), mkStrReplaceAll(), mkStrReplaceReg(), mkStrReplaceRegAll(), mkStrRev(), mkStrSplit(), mkStrSplitAt(), mkStrSplitAtRe(), mkStrSplitRest(), mkStrSplitRestRe(), mkStrSubstr(), mkStrSuffixof(), mkStrToCode(), mkStrToInt(), mkStrToLower(), mkStrToReg(), mkStrToUpper(), mkStrUpdate(), mkSub(), mkTempVar(), mkToFp(), mkToFp(), mkToFpUnsigned(), mkToInt(), mkToReal(), and mkUbvToInt().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVar | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name | ||
| ) |
Create a variable.
| sort | Sort |
| name | Variable name |
Definition at line 784 of file op_parser.cpp.
References node_manager, stabilizer::parser::NT_VAR, and var_names.
Referenced by declareVar(), declareVar(), mkArray(), mkVarBool(), mkVarBv(), mkVarFp(), mkVarInt(), mkVarReal(), mkVarReg(), mkVarRoundingMode(), mkVarStr(), and parseCommand().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarBool | ( | const std::string & | name | ) |
Create a boolean variable.
| name | Variable name |
Definition at line 817 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, and mkVar().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarBv | ( | const std::string & | name, |
| const size_t & | width | ||
| ) |
Create a bit-vector variable.
| name | Variable name |
| width | Width of the bit-vector |
Definition at line 826 of file op_parser.cpp.
References mkVar(), sort_key_map, and sort_manager.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarFp | ( | const std::string & | name, |
| const size_t & | e, | ||
| const size_t & | s | ||
| ) |
Create a floating-point variable.
| name | Variable name |
| e | Exponent size |
| s | Significand size |
Definition at line 840 of file op_parser.cpp.
References mkVar(), sort_key_map, and sort_manager.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarInt | ( | const std::string & | name | ) |
Create an integer variable.
| name | Variable name |
Definition at line 820 of file op_parser.cpp.
References stabilizer::parser::SortManager::INT_SORT, and mkVar().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarReal | ( | const std::string & | name | ) |
Create a real variable.
| name | Variable name |
Definition at line 823 of file op_parser.cpp.
References mkVar(), and stabilizer::parser::SortManager::REAL_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarReg | ( | const std::string & | name | ) |
Create a regular expression variable.
| name | Variable name |
Definition at line 859 of file op_parser.cpp.
References mkVar(), and stabilizer::parser::SortManager::REG_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarRoundingMode | ( | const std::string & | name | ) |
Create a rounding mode variable.
| name | Variable name |
Definition at line 862 of file op_parser.cpp.
References mkVar(), and stabilizer::parser::SK_ROUNDING_MODE.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarStr | ( | const std::string & | name | ) |
Create a string variable.
| name | Variable name |
Definition at line 856 of file op_parser.cpp.
References mkVar(), and stabilizer::parser::SortManager::STR_SORT.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkWeight | ( | const std::shared_ptr< Sort > & | sort, |
| const std::string & | name, | ||
| std::shared_ptr< DAGNode > | weight | ||
| ) |
Definition at line 2276 of file base_parser.cpp.
References node_manager, and stabilizer::parser::NT_WEIGHT.
Referenced by parseExpr().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkXor | ( | const std::vector< std::shared_ptr< DAGNode > > & | params | ) |
Create an xor node.
| params | Parameters |
Definition at line 1059 of file op_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, mkFalse(), mkOper(), and stabilizer::parser::NT_XOR.
Referenced by parseOper().
| std::string stabilizer::parser::Parser::optionToString | ( | ) |
Print the options.
Definition at line 2688 of file base_parser.cpp.
References options.
| bool stabilizer::parser::Parser::parse | ( | const std::string & | filename | ) |
Parse SMT-LIB2 file.
Parses the specified SMT-LIB2 file and builds internal data structures.
| filename | Path to the SMT-LIB2 file to parse |
Definition at line 79 of file base_parser.cpp.
References parseSmtlib2File().
Referenced by stabilizer::api::SMTStabilizer::apply_file().
|
private |
Definition at line 800 of file base_parser.cpp.
References stabilizer::parser::Parser::DTTypeDecl::arity, assertion_groups, assertions, assumptions, attemptParseKeywords(), bufptr, stabilizer::parser::CT_ASSERT, stabilizer::parser::CT_CHECK_SAT, stabilizer::parser::CT_CHECK_SAT_ASSUMING, stabilizer::parser::CT_DECLARE_CONST, stabilizer::parser::CT_DECLARE_FUN, stabilizer::parser::CT_DECLARE_SORT, stabilizer::parser::CT_DEFINE_FUN, stabilizer::parser::CT_DEFINE_FUN_REC, stabilizer::parser::CT_DEFINE_FUNS_REC, stabilizer::parser::CT_DEFINE_SORT, stabilizer::parser::CT_ECHO, stabilizer::parser::CT_EXISTS, stabilizer::parser::CT_EXIT, stabilizer::parser::CT_FORALL, stabilizer::parser::CT_GET_ASSERTIONS, stabilizer::parser::CT_GET_ASSIGNMENT, stabilizer::parser::CT_GET_INFO, stabilizer::parser::CT_GET_MODEL, stabilizer::parser::CT_GET_OPTION, stabilizer::parser::CT_GET_PROOF, stabilizer::parser::CT_GET_UNSAT_ASSUMPTIONS, stabilizer::parser::CT_GET_UNSAT_CORE, stabilizer::parser::CT_GET_VALUE, stabilizer::parser::CT_POP, stabilizer::parser::CT_PUSH, stabilizer::parser::CT_RESET, stabilizer::parser::CT_RESET_ASSERTIONS, stabilizer::parser::CT_SET_INFO, stabilizer::parser::CT_SET_LOGIC, stabilizer::parser::CT_SET_OPTION, stabilizer::parser::CT_UNKNOWN, stabilizer::parser::Parser::DTTypeDecl::ctors, datatype_blocks, datatype_function_names, datatype_sort_names, err_all(), err_mul_decl(), err_mul_def(), err_unkwn_sym(), fun_key_map, fun_var_map, function_names, getSymbol(), in_quantifier_scope, stabilizer::parser::KW_ID, stabilizer::parser::KW_NAMED, line_number, mkFuncDec(), mkFuncDef(), mkFuncRec(), mkFunParamVar(), mkSortDec(), mkSortDef(), mkVar(), stabilizer::parser::Parser::DTConstructorDecl::name, stabilizer::parser::Parser::DTTypeDecl::name, named_assertions, stabilizer::parser::NT_FUNC_DEF, options, parse_options, parseExpr(), parseLpar(), parseQuant(), parseRpar(), parseSort(), quant_nesting_depth, scan_mode, scanToNextSymbol(), stabilizer::parser::Parser::DTConstructorDecl::selectors, skipToRpar(), stabilizer::parser::SM_COMMENT, stabilizer::parser::SM_COMMON, stabilizer::parser::SM_COMP_SYM, stabilizer::parser::SM_STRING, sort_key_map, sort_manager, and warn_cmd_nsup().
Referenced by parseSmtlib2File(), and parseStr().
|
private |
Definition at line 696 of file expr_parser.cpp.
References allow_placeholder_vars, current_let_mode, datatype_function_names, stabilizer::parser::ERR_UNKWN_SYM, err_unkwn_sym(), fun_key_map, fun_var_map, in_quantifier_scope, stabilizer::parser::SortManager::INT_SORT, stabilizer::parser::TypeChecker::isBV(), stabilizer::parser::TypeChecker::isFP(), stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::TypeChecker::isNumber(), stabilizer::parser::TypeChecker::isReal(), stabilizer::parser::TypeChecker::isScientificNotation(), stabilizer::parser::TypeChecker::isString(), let_key_map, line_number, stabilizer::parser::LM_NON_LET, mkApplyDTFun(), mkConstBv(), mkConstFP(), mkConstInt(), mkConstReal(), mkConstStr(), mkE(), mkEpsilon(), mkErr(), mkFalse(), mkInfinity(), mkNaN(), mkNegEpsilon(), mkNegInfinity(), mkPi(), mkPlaceholderVar(), mkPosEpsilon(), mkPosInfinity(), mkRegAll(), mkRegAllChar(), mkRegNone(), mkRoundingMode(), mkTrue(), node_manager, options, stabilizer::parser::ConversionUtils::parseScientificNotation(), placeholder_var_names, stabilizer::parser::PRESERVING_LET_BIND_VAR_SUFFIX, preserving_let_counter, preserving_let_key_map, quant_var_map, stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::HighPrecisionInteger::toString(), and var_names.
Referenced by parseExpr().
|
private |
Definition at line 85 of file expr_parser.cpp.
References allow_placeholder_vars, attemptParseKeywords(), bufptr, condAssert, current_let_mode, err_all(), stabilizer::parser::ERR_UNKWN_SYM, err_unkwn_sym(), stabilizer::parser::Finish, stabilizer::parser::ExprFrame::func_args, stabilizer::parser::SortManager::getNull(), getSymbol(), stabilizer::parser::ExprFrame::headSymbol, in_quantifier_scope, stabilizer::parser::KW_LBLNEG, stabilizer::parser::KW_LBLPOS, stabilizer::parser::KW_NAMED, stabilizer::parser::KW_NO_PATTERN, stabilizer::parser::KW_NULL, stabilizer::parser::KW_PATTERN, stabilizer::parser::KW_QID, stabilizer::parser::KW_SKOLEMID, stabilizer::parser::KW_WEIGHT, let_nesting_depth, stabilizer::parser::ExprFrame::line, line_number, stabilizer::parser::LM_IN_LET, stabilizer::parser::LM_NON_LET, stabilizer::parser::LM_START_LET, mkAdd(), mkAnd(), mkAttribute(), mkBvSge(), mkBvSgt(), mkBvSle(), mkBvSlt(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkConstArray(), mkConstBv(), mkDistinct(), mkEq(), mkErr(), mkFpConst(), mkGe(), mkGt(), mkImplies(), mkIte(), mkLe(), mkLt(), mkMul(), mkNaN(), mkNegInfinity(), mkNoPattern(), mkNot(), mkOr(), mkPattern(), mkPosInfinity(), mkRootObj(), mkRootOfWithInterval(), mkSub(), mkWeight(), named_assertions, node_manager, stabilizer::parser::NT_CONST, stabilizer::parser::ExprFrame::oper_params, options, stabilizer::parser::ParamFunc, parseConstFunc(), parseExpr(), parseLet(), parseLpar(), parseOper(), parsePreservingLet(), parseQuant(), parseRpar(), parseSort(), placeholder_var_sort, preserving_let_counter, stabilizer::parser::ProcessingParamFuncArgs, stabilizer::parser::ProcessingParamFuncParams, stabilizer::parser::ProcessingParams, quant_nesting_depth, stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::ExprFrame::result, scanToNextSymbol(), stabilizer::parser::ExprFrame::second_symbol, sort_manager, stabilizer::parser::ExprFrame::special_type, stabilizer::parser::Start, and stabilizer::parser::ExprFrame::state.
Referenced by mkExpr(), parseCommand(), parseExpr(), parseLet(), parseParams(), parsePreservingLet(), and parseQuant().
|
private |
|
private |
Definition at line 753 of file base_parser.cpp.
References err_unkwn_sym(), getSymbol(), stabilizer::parser::KW_COMP, stabilizer::parser::KW_EPSILON, stabilizer::parser::KW_ID, stabilizer::parser::KW_LBLNEG, stabilizer::parser::KW_LBLPOS, stabilizer::parser::KW_M, stabilizer::parser::KW_NAMED, stabilizer::parser::KW_NO_PATTERN, stabilizer::parser::KW_NULL, stabilizer::parser::KW_PATTERN, stabilizer::parser::KW_QID, stabilizer::parser::KW_SKOLEMID, stabilizer::parser::KW_WEIGHT, and line_number.
Referenced by attemptParseKeywords().
|
private |
Definition at line 1927 of file base_parser.cpp.
References bufptr, condAssert, err_all(), err_sym_mis(), stabilizer::parser::ERR_UNEXP_EOF, getSymbol(), let_key_map, line_number, mkErr(), parseExpr(), parseLpar(), parseRpar(), and peekSymbol().
Referenced by parseExpr().
|
private |
Definition at line 573 of file base_parser.cpp.
References bufptr, err_sym_mis(), line_number, and scanToNextSymbol().
Referenced by parseCommand(), parseExpr(), parseLet(), parsePreservingLet(), parseQuant(), parseSmtlib2File(), parseSort(), and parseStr().
|
private |
Definition at line 907 of file expr_parser.cpp.
References applyFun(), stabilizer::parser::SortManager::BOOL_SORT, condAssert, stabilizer::parser::ERR_PARAM_MIS, err_param_mis(), stabilizer::parser::ERR_UNKWN_SYM, err_unkwn_sym(), fun_key_map, stabilizer::parser::getOperKind(), getSort(), line_number, mkAbs(), mkAcos(), mkAcosh(), mkAcot(), mkAcoth(), mkAcsc(), mkAcsch(), mkAdd(), mkAnd(), mkApplyUF(), mkAsec(), mkAsech(), mkAsin(), mkAsinh(), mkAtan(), mkAtan2(), mkAtanh(), mkBvAdd(), mkBvAnd(), mkBvAshr(), mkBvComp(), mkBvConcat(), mkBvExtract(), mkBvLshr(), mkBvMul(), mkBvNand(), mkBvNeg(), mkBvNor(), mkBvNot(), mkBvOr(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSdiv(), mkBvSge(), mkBvSgt(), mkBvShl(), mkBvSignExt(), mkBvSle(), mkBvSlt(), mkBvSmod(), mkBvSrem(), mkBvSub(), mkBvToInt(), mkBvToNat(), mkBvUdiv(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvUrem(), mkBvXnor(), mkBvXor(), mkBvZeroExt(), mkCeil(), mkCos(), mkCosh(), mkCot(), mkCsc(), mkCsch(), mkDistinct(), mkDivInt(), mkDivReal(), mkEq(), mkErr(), mkExp(), mkFact(), mkFloor(), mkFpAbs(), mkFpAdd(), mkFpDiv(), mkFpEq(), mkFpFma(), mkFpGe(), mkFpGt(), mkFpIsInf(), mkFpIsNaN(), mkFpIsNeg(), mkFpIsNormal(), mkFpIsPos(), mkFpIsSubnormal(), mkFpIsZero(), mkFpLe(), mkFpLt(), mkFpMax(), mkFpMin(), mkFpMul(), mkFpNeg(), mkFpRem(), mkFpRoundToIntegral(), mkFpSqrt(), mkFpSub(), mkFpToReal(), mkFpToSbv(), mkFpToUbv(), mkGcd(), mkGe(), mkGt(), mkIand(), mkImplies(), mkIntToBv(), mkIsDivisible(), mkIsEven(), mkIsInt(), mkIsOdd(), mkIsPrime(), mkIte(), mkLb(), mkLcm(), mkLe(), mkLg(), mkLn(), mkLog(), mkLt(), mkMod(), mkMul(), mkNatToBv(), mkNeg(), mkNot(), mkOr(), mkPow(), mkPow2(), mkRegComplement(), mkRegConcat(), mkRegDiff(), mkRegInter(), mkRegLoop(), mkRegOpt(), mkRegPlus(), mkRegRange(), mkRegRepeat(), mkRegStar(), mkRegUnion(), mkRootObj(), mkRound(), mkSafeSqrt(), mkSec(), mkSech(), mkSelect(), mkSin(), mkSinh(), mkSqrt(), mkStore(), mkStrCharat(), mkStrConcat(), mkStrContains(), mkStrFromCode(), mkStrFromInt(), mkStrGe(), mkStrGt(), mkStrIndexof(), mkStrIndexofReg(), mkStrInReg(), mkStrIsDigit(), mkStrLe(), mkStrLen(), mkStrLt(), mkStrNumSplits(), mkStrNumSplitsRe(), mkStrPrefixof(), mkStrReplace(), mkStrReplaceAll(), mkStrReplaceReg(), mkStrReplaceRegAll(), mkStrRev(), mkStrSplit(), mkStrSplitAt(), mkStrSplitAtRe(), mkStrSplitRest(), mkStrSplitRestRe(), mkStrSubstr(), mkStrSuffixof(), mkStrToCode(), mkStrToInt(), mkStrToLower(), mkStrToReg(), mkStrToUpper(), mkStrUpdate(), mkSub(), mkTan(), mkTanh(), mkToFp(), mkToFpUnsigned(), mkToInt(), mkToReal(), mkUbvToInt(), mkXor(), node_manager, stabilizer::parser::NT_ABS, stabilizer::parser::NT_ACOS, stabilizer::parser::NT_ACOSH, stabilizer::parser::NT_ACOT, stabilizer::parser::NT_ACOTH, stabilizer::parser::NT_ACSC, stabilizer::parser::NT_ACSCH, stabilizer::parser::NT_ADD, stabilizer::parser::NT_AND, stabilizer::parser::NT_ASEC, stabilizer::parser::NT_ASECH, stabilizer::parser::NT_ASIN, stabilizer::parser::NT_ASINH, stabilizer::parser::NT_ATAN, stabilizer::parser::NT_ATAN2, stabilizer::parser::NT_ATANH, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_BV_AND, stabilizer::parser::NT_BV_ASHR, stabilizer::parser::NT_BV_COMP, stabilizer::parser::NT_BV_CONCAT, stabilizer::parser::NT_BV_EXTRACT, stabilizer::parser::NT_BV_LSHR, stabilizer::parser::NT_BV_MUL, stabilizer::parser::NT_BV_NAND, stabilizer::parser::NT_BV_NEG, stabilizer::parser::NT_BV_NOR, stabilizer::parser::NT_BV_NOT, stabilizer::parser::NT_BV_OR, stabilizer::parser::NT_BV_REPEAT, stabilizer::parser::NT_BV_ROTATE_LEFT, stabilizer::parser::NT_BV_ROTATE_RIGHT, stabilizer::parser::NT_BV_SDIV, stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SHL, stabilizer::parser::NT_BV_SIGN_EXT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_SMOD, stabilizer::parser::NT_BV_SREM, stabilizer::parser::NT_BV_SUB, stabilizer::parser::NT_BV_TO_INT, stabilizer::parser::NT_BV_TO_NAT, stabilizer::parser::NT_BV_UDIV, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_BV_UREM, stabilizer::parser::NT_BV_XNOR, stabilizer::parser::NT_BV_XOR, stabilizer::parser::NT_BV_ZERO_EXT, stabilizer::parser::NT_CEIL, stabilizer::parser::NT_CONST, stabilizer::parser::NT_CONST_ARRAY, stabilizer::parser::NT_CONST_FALSE, stabilizer::parser::NT_CONST_TRUE, stabilizer::parser::NT_COS, stabilizer::parser::NT_COSH, stabilizer::parser::NT_COT, stabilizer::parser::NT_CSC, stabilizer::parser::NT_CSCH, stabilizer::parser::NT_DISTINCT, stabilizer::parser::NT_DIV_INT, stabilizer::parser::NT_DIV_REAL, stabilizer::parser::NT_DT_TESTER, stabilizer::parser::NT_DT_UPDATER, stabilizer::parser::NT_EQ, stabilizer::parser::NT_ERROR, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_EXP, stabilizer::parser::NT_FACT, stabilizer::parser::NT_FLOOR, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ABS, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_DIV, stabilizer::parser::NT_FP_EQ, stabilizer::parser::NT_FP_FMA, stabilizer::parser::NT_FP_GE, stabilizer::parser::NT_FP_GT, stabilizer::parser::NT_FP_IS_INF, stabilizer::parser::NT_FP_IS_NAN, stabilizer::parser::NT_FP_IS_NEG, stabilizer::parser::NT_FP_IS_NORMAL, stabilizer::parser::NT_FP_IS_POS, stabilizer::parser::NT_FP_IS_SUBNORMAL, stabilizer::parser::NT_FP_IS_ZERO, stabilizer::parser::NT_FP_LE, stabilizer::parser::NT_FP_LT, stabilizer::parser::NT_FP_MAX, stabilizer::parser::NT_FP_MIN, stabilizer::parser::NT_FP_MUL, stabilizer::parser::NT_FP_NEG, stabilizer::parser::NT_FP_REM, stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL, stabilizer::parser::NT_FP_SQRT, stabilizer::parser::NT_FP_SUB, stabilizer::parser::NT_FP_TO_FP, stabilizer::parser::NT_FP_TO_FP_UNSIGNED, stabilizer::parser::NT_FP_TO_REAL, stabilizer::parser::NT_FP_TO_SBV, stabilizer::parser::NT_FP_TO_UBV, stabilizer::parser::NT_FUNC_PARAM, stabilizer::parser::NT_GCD, stabilizer::parser::NT_GE, stabilizer::parser::NT_GT, stabilizer::parser::NT_IAND, stabilizer::parser::NT_IMPLIES, stabilizer::parser::NT_INT_TO_BV, stabilizer::parser::NT_IS_DIVISIBLE, stabilizer::parser::NT_IS_EVEN, stabilizer::parser::NT_IS_INT, stabilizer::parser::NT_IS_ODD, stabilizer::parser::NT_IS_PRIME, stabilizer::parser::NT_ITE, stabilizer::parser::NT_LB, stabilizer::parser::NT_LCM, stabilizer::parser::NT_LE, stabilizer::parser::NT_LET, stabilizer::parser::NT_LET_BIND_VAR, stabilizer::parser::NT_LET_BIND_VAR_LIST, stabilizer::parser::NT_LET_CHAIN, stabilizer::parser::NT_LG, stabilizer::parser::NT_LN, stabilizer::parser::NT_LOG, stabilizer::parser::NT_LT, stabilizer::parser::NT_MAX, stabilizer::parser::NT_MIN, stabilizer::parser::NT_MOD, stabilizer::parser::NT_MUL, stabilizer::parser::NT_NAT_TO_BV, stabilizer::parser::NT_NEG, stabilizer::parser::NT_NOT, stabilizer::parser::NT_NULL, stabilizer::parser::NT_OR, stabilizer::parser::NT_POW, stabilizer::parser::NT_POW2, stabilizer::parser::NT_QUANT_VAR, stabilizer::parser::NT_REG_COMPLEMENT, stabilizer::parser::NT_REG_CONCAT, stabilizer::parser::NT_REG_DIFF, stabilizer::parser::NT_REG_INTER, stabilizer::parser::NT_REG_LOOP, stabilizer::parser::NT_REG_OPT, stabilizer::parser::NT_REG_PLUS, stabilizer::parser::NT_REG_RANGE, stabilizer::parser::NT_REG_REPEAT, stabilizer::parser::NT_REG_STAR, stabilizer::parser::NT_REG_UNION, stabilizer::parser::NT_ROUND, stabilizer::parser::NT_SAFESQRT, stabilizer::parser::NT_SBV_TO_INT, stabilizer::parser::NT_SEC, stabilizer::parser::NT_SECH, stabilizer::parser::NT_SELECT, stabilizer::parser::NT_SIN, stabilizer::parser::NT_SINH, stabilizer::parser::NT_SQRT, stabilizer::parser::NT_STORE, stabilizer::parser::NT_STR_CHARAT, stabilizer::parser::NT_STR_CONCAT, stabilizer::parser::NT_STR_CONTAINS, stabilizer::parser::NT_STR_FROM_CODE, stabilizer::parser::NT_STR_FROM_INT, stabilizer::parser::NT_STR_GE, stabilizer::parser::NT_STR_GT, stabilizer::parser::NT_STR_IN_REG, stabilizer::parser::NT_STR_INDEXOF, stabilizer::parser::NT_STR_INDEXOF_REG, stabilizer::parser::NT_STR_IS_DIGIT, stabilizer::parser::NT_STR_LE, stabilizer::parser::NT_STR_LEN, stabilizer::parser::NT_STR_LT, stabilizer::parser::NT_STR_NUM_SPLITS, stabilizer::parser::NT_STR_NUM_SPLITS_RE, stabilizer::parser::NT_STR_PREFIXOF, 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_REV, stabilizer::parser::NT_STR_SPLIT, stabilizer::parser::NT_STR_SPLIT_AT, stabilizer::parser::NT_STR_SPLIT_AT_RE, stabilizer::parser::NT_STR_SPLIT_REST, stabilizer::parser::NT_STR_SPLIT_REST_RE, stabilizer::parser::NT_STR_SUBSTR, stabilizer::parser::NT_STR_SUFFIXOF, stabilizer::parser::NT_STR_TO_CODE, stabilizer::parser::NT_STR_TO_INT, stabilizer::parser::NT_STR_TO_LOWER, stabilizer::parser::NT_STR_TO_REG, stabilizer::parser::NT_STR_TO_UPPER, stabilizer::parser::NT_STR_UPDATE, stabilizer::parser::NT_SUB, stabilizer::parser::NT_TAN, stabilizer::parser::NT_TANH, stabilizer::parser::NT_TEMP_VAR, stabilizer::parser::NT_TO_INT, stabilizer::parser::NT_TO_REAL, stabilizer::parser::NT_TUPLE_CONSTRUCTOR, stabilizer::parser::NT_TUPLE_PROJECT, stabilizer::parser::NT_TUPLE_SELECT, stabilizer::parser::NT_TUPLE_UNIT, stabilizer::parser::NT_TUPLE_UPDATE, stabilizer::parser::NT_UBV_TO_INT, stabilizer::parser::NT_UNKNOWN, stabilizer::parser::NT_VAR, stabilizer::parser::NT_XOR, stabilizer::parser::SortManager::NULL_SORT, stabilizer::parser::NUM_KINDS, and sort_manager.
Referenced by parseExpr().
|
private |
Definition at line 1768 of file base_parser.cpp.
References bufptr, and parseExpr().
|
private |
Definition at line 1801 of file base_parser.cpp.
References bufptr, condAssert, err_all(), err_sym_mis(), stabilizer::parser::ERR_UNEXP_EOF, getSymbol(), line_number, mkErr(), mkLetBindVar(), mkLetBindVarList(), mkLetChain(), parseExpr(), parseLpar(), parseRpar(), peekSymbol(), stabilizer::parser::PRESERVING_LET_BIND_VAR_SUFFIX, preserving_let_counter, and preserving_let_key_map.
Referenced by parseExpr().
|
private |
Definition at line 2312 of file base_parser.cpp.
References bufptr, condAssert, getSymbol(), mkExists(), mkForall(), mkQuantVar(), stabilizer::parser::NodeManager::NULL_NODE, parseExpr(), parseLpar(), parseRpar(), parseSort(), and quant_var_map.
Referenced by parseCommand(), and parseExpr().
|
private |
Definition at line 583 of file base_parser.cpp.
References bufptr, err_sym_mis(), line_number, and scanToNextSymbol().
Referenced by parseCommand(), parseExpr(), parseLet(), parsePreservingLet(), parseQuant(), parseSmtlib2File(), parseSort(), and parseStr().
| bool stabilizer::parser::Parser::parseSmtlib2File | ( | const std::string | filename | ) |
Parse an SMT-LIB2 file.
Parses an SMT-LIB2 file and returns a boolean indicating success.
| filename | Path to the SMT-LIB2 file |
Definition at line 633 of file base_parser.cpp.
References buffer, buflen, bufptr, stabilizer::parser::CT_EXIT, err_open_file(), line_number, parseCommand(), parseLpar(), parseRpar(), parsing_file, and scanToNextSymbol().
|
private |
Definition at line 1605 of file base_parser.cpp.
References stabilizer::parser::SortManager::BOOL_SORT, bufptr, err_all(), stabilizer::parser::ERR_TYPE_MIS, err_unkwn_sym(), stabilizer::parser::SortManager::FLOAT16_SORT, stabilizer::parser::SortManager::FLOAT32_SORT, stabilizer::parser::SortManager::FLOAT64_SORT, getSymbol(), stabilizer::parser::SortManager::INT_SORT, line_number, stabilizer::parser::SortManager::NULL_SORT, parseLpar(), parseRpar(), parseSort(), stabilizer::parser::SortManager::REAL_SORT, stabilizer::parser::SortManager::REG_SORT, stabilizer::parser::SortManager::ROUNDING_MODE_SORT, scanToNextSymbol(), sort_key_map, sort_manager, and stabilizer::parser::SortManager::STR_SORT.
Referenced by parseCommand(), parseExpr(), parseQuant(), and parseSort().
| bool stabilizer::parser::Parser::parseStr | ( | const std::string & | constraint | ) |
Parse a constraint.
Parses the specified constraint and builds internal data structures.
| constraint | Constraint to parse |
Definition at line 698 of file base_parser.cpp.
References buffer, buflen, bufptr, stabilizer::parser::CT_EXIT, line_number, parseCommand(), parseLpar(), parseRpar(), stabilizer::parser::safe_strdup(), and scanToNextSymbol().
Referenced by stabilizer::api::SMTStabilizer::apply_text().
|
private |
|
private |
Definition at line 2036 of file base_parser.cpp.
References bufptr, getSymbol(), line_number, scan_mode, and scanToNextSymbol().
Referenced by parseLet(), and parsePreservingLet().
|
inline |
Definition at line 767 of file parser.h.
References node_manager.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rebuildLetBindings | ( | const std::shared_ptr< DAGNode > & | root | ) |
Definition at line 2691 of file base_parser.cpp.
References clear_let_key_map(), mkLetBindVar(), mkLetBindVarList(), mkLetChain(), stabilizer::parser::NT_EXISTS, and stabilizer::parser::NT_FORALL.
Referenced by dumpSMT2().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::remove | ( | std::shared_ptr< DAGNode > | expr, |
| const std::unordered_set< std::shared_ptr< DAGNode > > & | nodes | ||
| ) |
Remove all the nodes in the expression.
| expr | Expression to remove nodes from |
| nodes | Nodes to remove |
|
private |
| size_t stabilizer::parser::Parser::removeFuns | ( | const std::vector< std::string > & | funcNames | ) |
Remove functions by name.
| funcNames | Vector of function names to remove |
Definition at line 2988 of file base_parser.cpp.
References fun_key_map, and function_names.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rename | ( | std::shared_ptr< DAGNode > | expr, |
| const std::string & | new_name | ||
| ) |
Rename a node.
| expr | Expression to rename |
| new_name | New name |
Definition at line 2659 of file base_parser.cpp.
References condAssert, temp_var_names, and var_names.
|
inline |
Definition at line 307 of file parser.h.
References assertions.
|
private |
|
private |
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite | ( | NODE_KIND & | t, |
| std::shared_ptr< DAGNode > & | l, | ||
| std::shared_ptr< DAGNode > & | m, | ||
| std::shared_ptr< DAGNode > & | r | ||
| ) |
Rewrite ternary operation node when simplification rule applies.
| t | Operation kind (may be updated during rewrite). |
| l | First operand. |
| m | Second operand. |
| r | Third operand. |
Definition at line 932 of file rewrite_parser.cpp.
References stabilizer::parser::BitVectorUtils::bvExtract(), stabilizer::parser::echo_error(), isZero(), mkConstBv(), mkConstInt(), mkConstStr(), stabilizer::parser::NT_BV_EXTRACT, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_DIV, stabilizer::parser::NT_FP_MUL, stabilizer::parser::NT_FP_SUB, stabilizer::parser::NT_FP_TO_SBV, stabilizer::parser::NT_FP_TO_UBV, stabilizer::parser::NT_ITE, stabilizer::parser::NT_REG_LOOP, stabilizer::parser::NT_STORE, stabilizer::parser::NT_STR_INDEXOF, stabilizer::parser::NT_STR_INDEXOF_REG, 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_SPLIT_AT, stabilizer::parser::NT_STR_SPLIT_AT_RE, stabilizer::parser::NT_STR_SPLIT_REST, stabilizer::parser::NT_STR_SPLIT_REST_RE, stabilizer::parser::NT_STR_SUBSTR, stabilizer::parser::NT_STR_UPDATE, rewrite(), stabilizer::parser::StringUtils::strIndexof(), stabilizer::parser::StringUtils::strReplace(), stabilizer::parser::StringUtils::strReplaceAll(), stabilizer::parser::StringUtils::strSubstr(), stabilizer::parser::StringUtils::strUpdate(), toInt(), and stabilizer::parser::HighPrecisionInteger::toString().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite | ( | NODE_KIND & | t, |
| std::shared_ptr< DAGNode > & | l, | ||
| std::shared_ptr< DAGNode > & | ml, | ||
| std::shared_ptr< DAGNode > & | mr, | ||
| std::shared_ptr< DAGNode > & | r | ||
| ) |
Rewrite four-operand operation node when simplification rule applies.
| t | Operation kind (may be updated during rewrite). |
| l | First operand. |
| ml | Second operand. |
| mr | Third operand. |
| r | Fourth operand. |
Definition at line 1007 of file rewrite_parser.cpp.
References stabilizer::parser::echo_error(), and stabilizer::parser::NT_FP_FMA.
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite | ( | NODE_KIND & | t, |
| std::shared_ptr< DAGNode > & | l, | ||
| std::shared_ptr< DAGNode > & | r | ||
| ) |
Rewrite binary operation node when simplification rule applies.
| t | Operation kind (may be updated during rewrite). |
| l | Left operand. |
| r | Right operand. |
Definition at line 531 of file rewrite_parser.cpp.
References stabilizer::parser::HighPrecisionReal::atan2(), stabilizer::parser::BitVectorUtils::bvAshr(), stabilizer::parser::BitVectorUtils::bvComp(), stabilizer::parser::BitVectorUtils::bvCompareToUint(), stabilizer::parser::BitVectorUtils::bvIsMaxSigned(), stabilizer::parser::BitVectorUtils::bvIsMaxUnsigned(), stabilizer::parser::BitVectorUtils::bvIsMinSigned(), stabilizer::parser::BitVectorUtils::bvIsNegOne(), stabilizer::parser::BitVectorUtils::bvLshr(), stabilizer::parser::BitVectorUtils::bvNand(), stabilizer::parser::BitVectorUtils::bvNor(), stabilizer::parser::BitVectorUtils::bvRepeat(), stabilizer::parser::BitVectorUtils::bvRotateLeft(), stabilizer::parser::BitVectorUtils::bvRotateRight(), stabilizer::parser::BitVectorUtils::bvSdiv(), stabilizer::parser::BitVectorUtils::bvShl(), stabilizer::parser::BitVectorUtils::bvSignExtend(), stabilizer::parser::BitVectorUtils::bvSmod(), stabilizer::parser::BitVectorUtils::bvSrem(), stabilizer::parser::BitVectorUtils::bvSub(), stabilizer::parser::BitVectorUtils::bvUdiv(), stabilizer::parser::BitVectorUtils::bvUrem(), stabilizer::parser::BitVectorUtils::bvXnor(), stabilizer::parser::BitVectorUtils::bvZeroExtend(), err_all(), stabilizer::parser::MathUtils::gcd(), getEvaluateUseFloating(), stabilizer::parser::BitVectorUtils::intToBv(), isOne(), isOnes(), isZero(), stabilizer::parser::MathUtils::lcm(), line_number, mkBvNeg(), mkBvNot(), mkConstBv(), mkConstInt(), mkConstReal(), mkConstStr(), mkEq(), mkFalse(), stabilizer::parser::BitVectorUtils::mkOnes(), mkTrue(), stabilizer::parser::BitVectorUtils::natToBv(), stabilizer::parser::NT_ATAN2, stabilizer::parser::NT_BV_ASHR, stabilizer::parser::NT_BV_LSHR, stabilizer::parser::NT_BV_NAND, stabilizer::parser::NT_BV_NOR, stabilizer::parser::NT_BV_REPEAT, stabilizer::parser::NT_BV_ROTATE_LEFT, stabilizer::parser::NT_BV_ROTATE_RIGHT, stabilizer::parser::NT_BV_SDIV, stabilizer::parser::NT_BV_SDIVO, stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SHL, stabilizer::parser::NT_BV_SIGN_EXT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_SMOD, stabilizer::parser::NT_BV_SMODO, stabilizer::parser::NT_BV_SREM, stabilizer::parser::NT_BV_SREMO, stabilizer::parser::NT_BV_SUB, stabilizer::parser::NT_BV_UDIV, stabilizer::parser::NT_BV_UDIVO, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_BV_UMOD, stabilizer::parser::NT_BV_UMODO, stabilizer::parser::NT_BV_UREM, stabilizer::parser::NT_BV_UREMO, stabilizer::parser::NT_BV_XNOR, stabilizer::parser::NT_BV_ZERO_EXT, stabilizer::parser::NT_FP_MAX, stabilizer::parser::NT_FP_MIN, stabilizer::parser::NT_FP_REM, stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL, stabilizer::parser::NT_FP_SQRT, stabilizer::parser::NT_GCD, stabilizer::parser::NT_INT_TO_BV, stabilizer::parser::NT_IS_DIVISIBLE, stabilizer::parser::NT_LCM, stabilizer::parser::NT_LOG, stabilizer::parser::NT_MOD, stabilizer::parser::NT_NAT_TO_BV, stabilizer::parser::NT_POW, stabilizer::parser::NT_REG_RANGE, stabilizer::parser::NT_REG_REPEAT, stabilizer::parser::NT_SELECT, stabilizer::parser::NT_STR_CHARAT, stabilizer::parser::NT_STR_CONTAINS, stabilizer::parser::NT_STR_IN_REG, stabilizer::parser::NT_STR_NUM_SPLITS_RE, stabilizer::parser::NT_STR_PREFIXOF, stabilizer::parser::NT_STR_SPLIT, stabilizer::parser::NT_STR_SUFFIXOF, rewrite(), stabilizer::parser::StringUtils::strCharAt(), stabilizer::parser::StringUtils::strContains(), stabilizer::parser::StringUtils::strPrefixof(), stabilizer::parser::StringUtils::strSuffixof(), toInt(), and toReal().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite | ( | NODE_KIND & | t, |
| std::shared_ptr< DAGNode > & | p | ||
| ) |
Rewrite unary operation node when simplification rule applies.
| t | Operation kind (may be updated during rewrite). |
| p | Operand node. |
Definition at line 39 of file rewrite_parser.cpp.
References stabilizer::parser::BitVectorUtils::bvNeg(), stabilizer::parser::BitVectorUtils::bvNot(), stabilizer::parser::BitVectorUtils::bvToInt(), stabilizer::parser::BitVectorUtils::bvToNat(), stabilizer::parser::echo_error(), err_all(), stabilizer::parser::MathUtils::factorial(), getEvaluateUseFloating(), stabilizer::parser::MathUtils::isEven(), stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::MathUtils::isOdd(), stabilizer::parser::MathUtils::isPrime(), line_number, mkConstBv(), mkConstInt(), mkConstReal(), mkConstStr(), mkFalse(), mkTrue(), stabilizer::parser::NodeManager::NAN_NODE, stabilizer::parser::NT_ABS, stabilizer::parser::NT_ACOS, stabilizer::parser::NT_ACOSH, stabilizer::parser::NT_ACOT, stabilizer::parser::NT_ACOTH, stabilizer::parser::NT_ACSC, stabilizer::parser::NT_ACSCH, stabilizer::parser::NT_ASEC, stabilizer::parser::NT_ASECH, stabilizer::parser::NT_ASIN, stabilizer::parser::NT_ASINH, stabilizer::parser::NT_ATAN, stabilizer::parser::NT_ATANH, stabilizer::parser::NT_BV_NEG, stabilizer::parser::NT_BV_NEGO, stabilizer::parser::NT_BV_NOT, stabilizer::parser::NT_BV_TO_INT, stabilizer::parser::NT_BV_TO_NAT, stabilizer::parser::NT_CEIL, stabilizer::parser::NT_CONST_ARRAY, stabilizer::parser::NT_COS, stabilizer::parser::NT_COSH, stabilizer::parser::NT_COT, stabilizer::parser::NT_COTH, stabilizer::parser::NT_CSC, stabilizer::parser::NT_CSCH, stabilizer::parser::NT_EXP, stabilizer::parser::NT_FACT, stabilizer::parser::NT_FLOOR, stabilizer::parser::NT_FP_ABS, stabilizer::parser::NT_FP_IS_INF, stabilizer::parser::NT_FP_IS_NAN, stabilizer::parser::NT_FP_IS_NEG, stabilizer::parser::NT_FP_IS_NORMAL, stabilizer::parser::NT_FP_IS_POS, stabilizer::parser::NT_FP_IS_SUBNORMAL, stabilizer::parser::NT_FP_IS_ZERO, stabilizer::parser::NT_FP_NEG, stabilizer::parser::NT_FP_TO_REAL, stabilizer::parser::NT_IS_EVEN, stabilizer::parser::NT_IS_INT, stabilizer::parser::NT_IS_ODD, stabilizer::parser::NT_IS_PRIME, stabilizer::parser::NT_LB, stabilizer::parser::NT_LG, stabilizer::parser::NT_LN, stabilizer::parser::NT_NEG, stabilizer::parser::NT_NOT, stabilizer::parser::NT_POW2, stabilizer::parser::NT_REG_COMPLEMENT, stabilizer::parser::NT_REG_OPT, stabilizer::parser::NT_REG_PLUS, stabilizer::parser::NT_REG_STAR, stabilizer::parser::NT_ROUND, stabilizer::parser::NT_SAFESQRT, stabilizer::parser::NT_SBV_TO_INT, stabilizer::parser::NT_SEC, stabilizer::parser::NT_SECH, stabilizer::parser::NT_SIN, stabilizer::parser::NT_SINH, stabilizer::parser::NT_SQRT, stabilizer::parser::NT_STR_FROM_CODE, stabilizer::parser::NT_STR_FROM_INT, stabilizer::parser::NT_STR_IS_DIGIT, stabilizer::parser::NT_STR_LEN, stabilizer::parser::NT_STR_REV, stabilizer::parser::NT_STR_TO_CODE, stabilizer::parser::NT_STR_TO_INT, stabilizer::parser::NT_STR_TO_LOWER, stabilizer::parser::NT_STR_TO_REG, stabilizer::parser::NT_STR_TO_UPPER, stabilizer::parser::NT_TAN, stabilizer::parser::NT_TANH, stabilizer::parser::NT_TO_INT, stabilizer::parser::NT_TO_REAL, stabilizer::parser::NT_UBV_TO_INT, stabilizer::parser::MathUtils::pow(), stabilizer::parser::StringUtils::strRev(), stabilizer::parser::StringUtils::strToLower(), stabilizer::parser::StringUtils::strToUpper(), stabilizer::parser::StringUtils::strUnquate(), toInt(), and toReal().
Referenced by rewrite(), rewrite(), rewrite(), and rewrite_oper().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite | ( | NODE_KIND & | t, |
| std::vector< std::shared_ptr< DAGNode > > & | p | ||
| ) |
Rewrite variadic operation node when simplification rule applies.
| t | Operation kind (may be updated during rewrite). |
| p | Operand list. |
Definition at line 1019 of file rewrite_parser.cpp.
References stabilizer::parser::BitVectorUtils::bvAdd(), stabilizer::parser::BitVectorUtils::bvAnd(), stabilizer::parser::BitVectorUtils::bvConcat(), stabilizer::parser::BitVectorUtils::bvMul(), stabilizer::parser::BitVectorUtils::bvOr(), stabilizer::parser::BitVectorUtils::bvXor(), stabilizer::parser::echo_error(), getEvaluateUseFloating(), stabilizer::parser::BitVectorUtils::intToBv(), isOne(), isOnes(), isZero(), stabilizer::parser::kindToString(), mkBvZeroExt(), mkConstBv(), mkConstInt(), mkConstReal(), mkConstStr(), mkFalse(), stabilizer::parser::BitVectorUtils::mkOnes(), mkTrue(), stabilizer::parser::NT_ADD, stabilizer::parser::NT_AND, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_BV_AND, stabilizer::parser::NT_BV_COMP, stabilizer::parser::NT_BV_CONCAT, stabilizer::parser::NT_BV_MUL, stabilizer::parser::NT_BV_OR, stabilizer::parser::NT_BV_SADDO, stabilizer::parser::NT_BV_SMULO, stabilizer::parser::NT_BV_UADDO, stabilizer::parser::NT_BV_UMULO, stabilizer::parser::NT_BV_XOR, stabilizer::parser::NT_DISTINCT, stabilizer::parser::NT_DISTINCT_BOOL, stabilizer::parser::NT_DISTINCT_OTHER, stabilizer::parser::NT_DIV_INT, stabilizer::parser::NT_DIV_REAL, stabilizer::parser::NT_EQ, stabilizer::parser::NT_EQ_BOOL, stabilizer::parser::NT_EQ_OTHER, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_EQ, stabilizer::parser::NT_FP_GE, stabilizer::parser::NT_FP_GT, stabilizer::parser::NT_FP_LE, stabilizer::parser::NT_FP_LT, stabilizer::parser::NT_GE, stabilizer::parser::NT_GT, stabilizer::parser::NT_IAND, stabilizer::parser::NT_IMPLIES, stabilizer::parser::NT_LE, stabilizer::parser::NT_LT, stabilizer::parser::NT_MAX, stabilizer::parser::NT_MIN, stabilizer::parser::NT_MUL, stabilizer::parser::NT_OR, stabilizer::parser::NT_REG_CONCAT, stabilizer::parser::NT_REG_DIFF, stabilizer::parser::NT_REG_INTER, stabilizer::parser::NT_REG_UNION, stabilizer::parser::NT_STR_CONCAT, stabilizer::parser::NT_STR_GE, stabilizer::parser::NT_STR_GT, stabilizer::parser::NT_STR_LE, stabilizer::parser::NT_STR_LT, stabilizer::parser::NT_SUB, stabilizer::parser::NT_XOR, rewrite(), toInt(), and toReal().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite_oper | ( | NODE_KIND & | t, |
| std::vector< std::shared_ptr< DAGNode > > & | p | ||
| ) |
Core operation rewrite helper used before node-manager creation.
| t | Operation kind (may be updated during rewrite). |
| p | Operand list. |
Definition at line 1865 of file rewrite_parser.cpp.
References getArity(), stabilizer::parser::NT_ABS, stabilizer::parser::NT_ACOS, stabilizer::parser::NT_ACOSH, stabilizer::parser::NT_ACOT, stabilizer::parser::NT_ACOTH, stabilizer::parser::NT_ACSC, stabilizer::parser::NT_ACSCH, stabilizer::parser::NT_ADD, stabilizer::parser::NT_AND, stabilizer::parser::NT_ASEC, stabilizer::parser::NT_ASECH, stabilizer::parser::NT_ASIN, stabilizer::parser::NT_ASINH, stabilizer::parser::NT_ATAN, stabilizer::parser::NT_ATAN2, stabilizer::parser::NT_ATANH, stabilizer::parser::NT_BV_ADD, stabilizer::parser::NT_BV_AND, stabilizer::parser::NT_BV_ASHR, stabilizer::parser::NT_BV_COMP, stabilizer::parser::NT_BV_CONCAT, stabilizer::parser::NT_BV_EXTRACT, stabilizer::parser::NT_BV_LSHR, stabilizer::parser::NT_BV_MUL, stabilizer::parser::NT_BV_NAND, stabilizer::parser::NT_BV_NEG, stabilizer::parser::NT_BV_NEGO, stabilizer::parser::NT_BV_NOR, stabilizer::parser::NT_BV_NOT, stabilizer::parser::NT_BV_OR, stabilizer::parser::NT_BV_REPEAT, stabilizer::parser::NT_BV_ROTATE_LEFT, stabilizer::parser::NT_BV_ROTATE_RIGHT, stabilizer::parser::NT_BV_SADDO, stabilizer::parser::NT_BV_SDIV, stabilizer::parser::NT_BV_SDIVO, stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SHL, stabilizer::parser::NT_BV_SIGN_EXT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_SMOD, stabilizer::parser::NT_BV_SMODO, stabilizer::parser::NT_BV_SMULO, stabilizer::parser::NT_BV_SREM, stabilizer::parser::NT_BV_SREMO, stabilizer::parser::NT_BV_SUB, stabilizer::parser::NT_BV_TO_INT, stabilizer::parser::NT_BV_TO_NAT, stabilizer::parser::NT_BV_UADDO, stabilizer::parser::NT_BV_UDIV, stabilizer::parser::NT_BV_UDIVO, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_BV_UMOD, stabilizer::parser::NT_BV_UMODO, stabilizer::parser::NT_BV_UMULO, stabilizer::parser::NT_BV_UREM, stabilizer::parser::NT_BV_UREMO, stabilizer::parser::NT_BV_XNOR, stabilizer::parser::NT_BV_XOR, stabilizer::parser::NT_BV_ZERO_EXT, stabilizer::parser::NT_CEIL, stabilizer::parser::NT_CONST, stabilizer::parser::NT_CONST_ARRAY, stabilizer::parser::NT_CONST_E, stabilizer::parser::NT_CONST_FALSE, stabilizer::parser::NT_CONST_PI, stabilizer::parser::NT_CONST_TRUE, stabilizer::parser::NT_COS, stabilizer::parser::NT_COSH, stabilizer::parser::NT_COT, stabilizer::parser::NT_COTH, stabilizer::parser::NT_CSC, stabilizer::parser::NT_CSCH, stabilizer::parser::NT_DISTINCT, stabilizer::parser::NT_DISTINCT_BOOL, stabilizer::parser::NT_DISTINCT_OTHER, stabilizer::parser::NT_DIV_INT, stabilizer::parser::NT_DIV_REAL, stabilizer::parser::NT_EPSILON, stabilizer::parser::NT_EQ, stabilizer::parser::NT_EQ_BOOL, stabilizer::parser::NT_EQ_OTHER, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_EXP, stabilizer::parser::NT_FACT, stabilizer::parser::NT_FLOOR, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ABS, stabilizer::parser::NT_FP_ADD, stabilizer::parser::NT_FP_DIV, stabilizer::parser::NT_FP_EQ, stabilizer::parser::NT_FP_FMA, stabilizer::parser::NT_FP_GE, stabilizer::parser::NT_FP_GT, stabilizer::parser::NT_FP_IS_INF, stabilizer::parser::NT_FP_IS_NAN, stabilizer::parser::NT_FP_IS_NEG, stabilizer::parser::NT_FP_IS_NORMAL, stabilizer::parser::NT_FP_IS_POS, stabilizer::parser::NT_FP_IS_SUBNORMAL, stabilizer::parser::NT_FP_IS_ZERO, stabilizer::parser::NT_FP_LE, stabilizer::parser::NT_FP_LT, stabilizer::parser::NT_FP_MAX, stabilizer::parser::NT_FP_MIN, stabilizer::parser::NT_FP_MUL, stabilizer::parser::NT_FP_NEG, stabilizer::parser::NT_FP_REM, stabilizer::parser::NT_FP_ROUND_TO_INTEGRAL, stabilizer::parser::NT_FP_SQRT, stabilizer::parser::NT_FP_SUB, stabilizer::parser::NT_FP_TO_FP, stabilizer::parser::NT_FP_TO_REAL, stabilizer::parser::NT_FP_TO_SBV, stabilizer::parser::NT_FP_TO_UBV, stabilizer::parser::NT_GCD, stabilizer::parser::NT_GE, stabilizer::parser::NT_GT, stabilizer::parser::NT_IAND, stabilizer::parser::NT_IMPLIES, stabilizer::parser::NT_INFINITY, stabilizer::parser::NT_INT_TO_BV, stabilizer::parser::NT_IS_DIVISIBLE, stabilizer::parser::NT_IS_EVEN, stabilizer::parser::NT_IS_INT, stabilizer::parser::NT_IS_ODD, stabilizer::parser::NT_IS_PRIME, stabilizer::parser::NT_ITE, stabilizer::parser::NT_LB, stabilizer::parser::NT_LCM, stabilizer::parser::NT_LE, stabilizer::parser::NT_LG, stabilizer::parser::NT_LN, stabilizer::parser::NT_LOG, stabilizer::parser::NT_LT, stabilizer::parser::NT_MAX, stabilizer::parser::NT_MIN, stabilizer::parser::NT_MOD, stabilizer::parser::NT_MUL, stabilizer::parser::NT_NAN, stabilizer::parser::NT_NAT_TO_BV, stabilizer::parser::NT_NEG, stabilizer::parser::NT_NEG_EPSILON, stabilizer::parser::NT_NEG_INFINITY, stabilizer::parser::NT_NOT, stabilizer::parser::NT_NULL, stabilizer::parser::NT_OR, stabilizer::parser::NT_POS_EPSILON, stabilizer::parser::NT_POS_INFINITY, stabilizer::parser::NT_POW, stabilizer::parser::NT_POW2, stabilizer::parser::NT_QUANT_VAR, stabilizer::parser::NT_REG_ALL, stabilizer::parser::NT_REG_ALLCHAR, stabilizer::parser::NT_REG_COMPLEMENT, stabilizer::parser::NT_REG_CONCAT, stabilizer::parser::NT_REG_DIFF, stabilizer::parser::NT_REG_INTER, stabilizer::parser::NT_REG_LOOP, stabilizer::parser::NT_REG_NONE, stabilizer::parser::NT_REG_OPT, stabilizer::parser::NT_REG_PLUS, stabilizer::parser::NT_REG_RANGE, stabilizer::parser::NT_REG_REPEAT, stabilizer::parser::NT_REG_STAR, stabilizer::parser::NT_REG_UNION, stabilizer::parser::NT_ROUND, stabilizer::parser::NT_SAFESQRT, stabilizer::parser::NT_SBV_TO_INT, stabilizer::parser::NT_SEC, stabilizer::parser::NT_SECH, stabilizer::parser::NT_SELECT, stabilizer::parser::NT_SIN, stabilizer::parser::NT_SINH, stabilizer::parser::NT_SQRT, stabilizer::parser::NT_STORE, stabilizer::parser::NT_STR_CHARAT, stabilizer::parser::NT_STR_CONCAT, stabilizer::parser::NT_STR_CONTAINS, stabilizer::parser::NT_STR_FROM_CODE, stabilizer::parser::NT_STR_FROM_INT, stabilizer::parser::NT_STR_GE, stabilizer::parser::NT_STR_GT, stabilizer::parser::NT_STR_IN_REG, stabilizer::parser::NT_STR_INDEXOF, stabilizer::parser::NT_STR_INDEXOF_REG, stabilizer::parser::NT_STR_IS_DIGIT, stabilizer::parser::NT_STR_LE, stabilizer::parser::NT_STR_LEN, stabilizer::parser::NT_STR_LT, stabilizer::parser::NT_STR_NUM_SPLITS_RE, stabilizer::parser::NT_STR_PREFIXOF, 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_REV, stabilizer::parser::NT_STR_SPLIT, stabilizer::parser::NT_STR_SPLIT_AT, stabilizer::parser::NT_STR_SPLIT_AT_RE, stabilizer::parser::NT_STR_SPLIT_REST, stabilizer::parser::NT_STR_SPLIT_REST_RE, stabilizer::parser::NT_STR_SUBSTR, stabilizer::parser::NT_STR_SUFFIXOF, stabilizer::parser::NT_STR_TO_CODE, stabilizer::parser::NT_STR_TO_INT, stabilizer::parser::NT_STR_TO_LOWER, stabilizer::parser::NT_STR_TO_REG, stabilizer::parser::NT_STR_TO_UPPER, stabilizer::parser::NT_STR_UPDATE, stabilizer::parser::NT_SUB, stabilizer::parser::NT_TAN, stabilizer::parser::NT_TANH, stabilizer::parser::NT_TEMP_VAR, stabilizer::parser::NT_TO_INT, stabilizer::parser::NT_TO_REAL, stabilizer::parser::NT_UBV_TO_INT, stabilizer::parser::NT_VAR, stabilizer::parser::NT_XOR, options, and rewrite().
Referenced by mkInternalOper(), and mkNode().
|
private |
Definition at line 533 of file base_parser.cpp.
References bufptr, line_number, scan_mode, stabilizer::parser::SM_COMMENT, stabilizer::parser::SM_COMMON, stabilizer::parser::SM_COMP_SYM, stabilizer::parser::SM_STRING, and stabilizer::parser::SM_SYMBOL.
Referenced by getSymbol(), mkExpr(), parseCommand(), parseExpr(), parseLpar(), parseRpar(), parseSmtlib2File(), parseSort(), parseStr(), and peekSymbol().
| void stabilizer::parser::Parser::setEvaluatePrecision | ( | mpfr_prec_t | precision | ) |
Set the precision for evaluation.
| precision | Precision |
Definition at line 278 of file base_parser.cpp.
References options.
| void stabilizer::parser::Parser::setEvaluateUseFloating | ( | bool | use_floating | ) |
Set the use floating for evaluation.
| use_floating | Use floating |
Definition at line 284 of file base_parser.cpp.
References options.
| void stabilizer::parser::Parser::setOption | ( | const std::string & | key, |
| const bool & | value | ||
| ) |
Definition at line 232 of file base_parser.cpp.
References options.
| void stabilizer::parser::Parser::setOption | ( | const std::string & | key, |
| const double & | value | ||
| ) |
Definition at line 229 of file base_parser.cpp.
References options.
| void stabilizer::parser::Parser::setOption | ( | const std::string & | key, |
| const int & | value | ||
| ) |
Definition at line 226 of file base_parser.cpp.
References options.
| void stabilizer::parser::Parser::setOption | ( | const std::string & | key, |
| const std::string & | value | ||
| ) |
Set global options.
| key | Option name |
| value | Option value |
Definition at line 223 of file base_parser.cpp.
References options.
|
private |
Definition at line 593 of file base_parser.cpp.
References bufptr, line_number, scan_mode, stabilizer::parser::SM_COMMENT, stabilizer::parser::SM_COMMON, stabilizer::parser::SM_COMP_SYM, and stabilizer::parser::SM_STRING.
Referenced by parseCommand().
|
static |
Return sorted operand list for deterministic commutative handling.
Definition at line 173 of file op_parser.cpp.
Referenced by mkInternalOper(), and mkNode().
| std::shared_ptr< DAGNode > stabilizer::parser::Parser::substitute | ( | std::shared_ptr< DAGNode > | expr, |
| std::unordered_map< std::string, std::shared_ptr< DAGNode > > & | params | ||
| ) |
Substitute variables in an expression.
| expr | Expression to substitute |
| params | Map of variable names to their corresponding values |
Definition at line 2366 of file base_parser.cpp.
References substitute().
Referenced by substitute().
|
private |
Definition at line 2374 of file base_parser.cpp.
References mkOper(), and node_manager.
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
Convert an expression to an integer.
| expr | Expression to convert |
Definition at line 300 of file base_parser.cpp.
References condAssert, and ensureNumberValue().
Referenced by isOne(), isZero(), mkBvExtract(), mkBvRepeat(), mkBvSignExt(), mkBvZeroExt(), mkFpToSbv(), mkFpToUbv(), mkIand(), mkIntToBv(), mkMul(), mkNatToBv(), mkSub(), mkToFp(), mkToFp(), mkToFpUnsigned(), rewrite(), rewrite(), rewrite(), and rewrite().
|
private |
Convert an expression to a real.
| expr | Expression to convert |
Definition at line 290 of file base_parser.cpp.
References condAssert, stabilizer::parser::HighPrecisionReal::e(), ensureNumberValue(), getEvaluatePrecision(), and stabilizer::parser::HighPrecisionReal::pi().
Referenced by isOne(), isZero(), mkMul(), mkSub(), rewrite(), rewrite(), and rewrite().
| std::string stabilizer::parser::Parser::toString | ( | const NODE_KIND & | kind | ) |
Print a node kind.
| kind | Node kind to print |
Definition at line 2684 of file base_parser.cpp.
References stabilizer::parser::kindToString().
| std::string stabilizer::parser::Parser::toString | ( | std::shared_ptr< DAGNode > | expr | ) |
Print an expression.
| expr | Expression to print |
Definition at line 2676 of file base_parser.cpp.
References stabilizer::parser::dumpSMTLIB2().
Referenced by mkRootObj(), and mkRootOfWithInterval().
| std::string stabilizer::parser::Parser::toString | ( | std::shared_ptr< Sort > | sort | ) |
Print a sort.
| sort | Sort to print |
Definition at line 2680 of file base_parser.cpp.
|
private |
|
private |
|
private |
|
private |
|
private |
Definition at line 3015 of file base_parser.cpp.
Referenced by parseCommand().
|
private |
Definition at line 194 of file parser.h.
Referenced by parseConstFunc(), parseExpr(), Parser(), and Parser().
| std::unordered_map<std::string, std::unordered_set<size_t> > stabilizer::parser::Parser::assertion_groups |
Definition at line 266 of file parser.h.
Referenced by getGroupedAssertions(), and parseCommand().
| std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::assertions |
Definition at line 265 of file parser.h.
Referenced by assert(), assert(), checkSat(), dumpSMT2(), getAssertions(), getNodeCount(), parseCommand(), and replaceAssertions().
| std::vector<std::vector<std::shared_ptr<DAGNode> > > stabilizer::parser::Parser::assumptions |
Definition at line 273 of file parser.h.
Referenced by getAssumptions(), getNodeCount(), and parseCommand().
|
private |
Definition at line 184 of file parser.h.
Referenced by getSymbol(), mkExpr(), Parser(), Parser(), parseSmtlib2File(), and parseStr().
|
private |
Definition at line 185 of file parser.h.
Referenced by getSymbol(), mkExpr(), Parser(), Parser(), parseSmtlib2File(), and parseStr().
|
private |
Definition at line 186 of file parser.h.
Referenced by attemptParseKeywords(), getSymbol(), mkExpr(), parseCommand(), parseExpr(), parseLet(), parseLpar(), parseParams(), parsePreservingLet(), parseQuant(), Parser(), Parser(), parseRpar(), parseSmtlib2File(), parseSort(), parseStr(), peekSymbol(), scanToNextSymbol(), and skipToRpar().
|
private |
Definition at line 190 of file parser.h.
Referenced by parseConstFunc(), and parseExpr().
|
private |
Definition at line 222 of file parser.h.
Referenced by dumpSMT2(), getDatatypeBlocks(), and parseCommand().
|
private |
Definition at line 227 of file parser.h.
Referenced by applyFun(), parseCommand(), and parseConstFunc().
|
private |
Definition at line 224 of file parser.h.
Referenced by parseCommand().
|
private |
Definition at line 216 of file parser.h.
Referenced by mkFuncDec().
|
private |
Definition at line 209 of file parser.h.
Referenced by getFunctions(), getFunKeyMap(), getKind(), isDeclaredFunction(), mkFuncDec(), mkFuncDef(), mkFuncRec(), parseCommand(), parseConstFunc(), parseOper(), Parser(), Parser(), and removeFuns().
|
private |
Definition at line 211 of file parser.h.
Referenced by parseCommand(), parseConstFunc(), Parser(), and Parser().
|
private |
Definition at line 240 of file parser.h.
Referenced by getFunctionNames(), getFunctions(), parseCommand(), Parser(), Parser(), and removeFuns().
|
private |
Definition at line 193 of file parser.h.
Referenced by parseCommand(), parseConstFunc(), parseExpr(), Parser(), and Parser().
|
private |
Definition at line 206 of file parser.h.
Referenced by parseConstFunc(), parseLet(), Parser(), and Parser().
|
private |
Definition at line 191 of file parser.h.
Referenced by parseExpr(), Parser(), and Parser().
|
private |
Definition at line 187 of file parser.h.
Referenced by ensureNumberValue(), getSymbol(), mkAbs(), mkAdd(), mkAnd(), mkBvAdd(), mkBvAnd(), mkBvAshr(), mkBvConcat(), mkBvExtract(), mkBvLshr(), mkBvMul(), mkBvNot(), mkBvOr(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSdiv(), mkBvSge(), mkBvSgt(), mkBvShl(), mkBvSignExt(), mkBvSle(), mkBvSlt(), mkBvSmod(), mkBvSrem(), mkBvToInt(), mkBvToNat(), mkBvUdiv(), mkBvUge(), mkBvUgt(), mkBvUle(), mkBvUlt(), mkBvUmod(), mkBvUrem(), mkBvXor(), mkBvZeroExt(), mkCeil(), mkConstArray(), mkDistinct(), mkDivInt(), mkDivReal(), mkEq(), mkExpr(), mkFact(), mkFpAbs(), mkFpAdd(), mkFpConst(), mkFpDiv(), mkFpFma(), mkFpIsInf(), mkFpIsNaN(), mkFpIsNeg(), mkFpIsNormal(), mkFpIsPos(), mkFpIsSubnormal(), mkFpIsZero(), mkFpMul(), mkFpNeg(), mkFpRem(), mkFpRoundToIntegral(), mkFpRoundToIntegral(), mkFpSqrt(), mkFpSqrt(), mkFpSub(), mkFpToReal(), mkFpToSbv(), mkFpToUbv(), mkFuncDef(), mkFuncRec(), mkGcd(), mkGe(), mkGt(), mkIand(), mkImplies(), mkIndexofReg(), mkInfinity(), mkIntToBv(), mkIsDivisible(), mkIsEven(), mkIsInt(), mkIsOdd(), mkIsPrime(), mkIte(), mkLcm(), mkLe(), mkLog(), mkLt(), mkMax(), mkMin(), mkMod(), mkMul(), mkNatToBv(), mkNegInfinity(), mkNot(), mkOper(), mkOr(), mkPosInfinity(), mkRegComplement(), mkRegConcat(), mkRegDiff(), mkRegInter(), mkRegLoop(), mkRegOpt(), mkRegPlus(), mkRegRange(), mkRegRepeat(), mkRegStar(), mkRegUnion(), mkReplaceReg(), mkReplaceRegAll(), mkSafeSqrt(), mkSbvToInt(), mkSelect(), mkSqrt(), mkStrCharat(), mkStrConcat(), mkStrContains(), mkStrFromCode(), mkStrFromInt(), mkStrIndexof(), mkStrIndexofReg(), mkStrInReg(), mkStrIsDigit(), mkStrLen(), mkStrNumSplits(), mkStrNumSplitsRe(), mkStrPrefixof(), mkStrReplace(), mkStrReplaceAll(), mkStrReplaceReg(), mkStrReplaceRegAll(), mkStrRev(), mkStrSplit(), mkStrSplitAt(), mkStrSplitAtRe(), mkStrSplitRest(), mkStrSplitRestRe(), mkStrSubstr(), mkStrSuffixof(), mkStrToCode(), mkStrToInt(), mkStrToLower(), mkStrToReg(), mkStrToUpper(), mkStrUpdate(), mkSub(), mkTempVar(), mkToFp(), mkToFp(), mkToFpUnsigned(), mkToInt(), mkToReal(), mkUbvToInt(), parseCommand(), parseConstFunc(), parseExpr(), parseKeyword(), parseLet(), parseLpar(), parseOper(), parsePreservingLet(), Parser(), Parser(), parseRpar(), parseSmtlib2File(), parseSort(), parseStr(), peekSymbol(), rewrite(), rewrite(), scanToNextSymbol(), and skipToRpar().
| std::unordered_map<std::string, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::named_assertions |
Definition at line 268 of file parser.h.
Referenced by parseCommand(), and parseExpr().
|
private |
Definition at line 201 of file parser.h.
Referenced by applyFun(), getDeclaredVariables(), getNodeManager(), getVariable(), getVariables(), mkApplyDTFun(), mkApplyUF(), mkAttribute(), mkConstArray(), mkConstBv(), mkConstFP(), mkConstFp(), mkConstInt(), mkConstReal(), mkConstReal(), mkConstReal(), mkConstReal(), mkConstReg(), mkConstStr(), mkErr(), mkFpConst(), mkFuncDec(), mkFuncDef(), mkFuncRec(), mkFunParamVar(), mkInternalOper(), mkLetBindVar(), mkLetBindVarList(), mkLetChain(), mkNaN(), mkNegInfinity(), mkNode(), mkNoPattern(), mkPattern(), mkPlaceholderVar(), mkPosInfinity(), mkQuantVar(), mkRootObj(), mkRootOfWithInterval(), mkRoundingMode(), mkTempVar(), mkUFVNode(), mkVar(), mkWeight(), parseConstFunc(), parseExpr(), parseOper(), Parser(), Parser(), rebuild_node_manager(), and substitute().
|
private |
Definition at line 262 of file parser.h.
Referenced by mkQuantVar().
|
private |
Definition at line 242 of file parser.h.
Referenced by applyFun(), applyFunPostOrder(), dumpSMT2(), getEvaluatePrecision(), getEvaluateUseFloating(), getOptions(), mkAdd(), mkIand(), mkMul(), mkSub(), optionToString(), parseCommand(), parseConstFunc(), parseExpr(), Parser(), Parser(), rewrite_oper(), setEvaluatePrecision(), setEvaluateUseFloating(), setOption(), setOption(), setOption(), and setOption().
|
private |
Definition at line 198 of file parser.h.
Referenced by dumpSMT2(), and parseCommand().
|
private |
Definition at line 197 of file parser.h.
Referenced by assert(), getSymbol(), mkExpr(), Parser(), Parser(), and parseSmtlib2File().
|
private |
Definition at line 236 of file parser.h.
Referenced by mkPlaceholderVar(), and parseConstFunc().
|
private |
Definition at line 195 of file parser.h.
Referenced by mkPlaceholderVar(), parseExpr(), Parser(), and Parser().
|
private |
Definition at line 189 of file parser.h.
Referenced by parseConstFunc(), parseExpr(), parsePreservingLet(), Parser(), and Parser().
|
private |
Definition at line 208 of file parser.h.
Referenced by clear_let_key_map(), mkLetBindVar(), parseConstFunc(), parsePreservingLet(), Parser(), and Parser().
|
private |
Definition at line 192 of file parser.h.
Referenced by parseCommand(), parseExpr(), Parser(), and Parser().
|
private |
Definition at line 214 of file parser.h.
Referenced by mkQuantVar(), parseConstFunc(), parseQuant(), Parser(), and Parser().
|
private |
Definition at line 260 of file parser.h.
Referenced by getResult().
|
private |
Definition at line 259 of file parser.h.
Referenced by checkSat(), and getResultType().
|
private |
Definition at line 188 of file parser.h.
Referenced by getSymbol(), parseCommand(), Parser(), Parser(), peekSymbol(), scanToNextSymbol(), and skipToRpar().
| std::unordered_map<std::string, std::unordered_set<size_t> > stabilizer::parser::Parser::soft_assertion_groups |
Definition at line 277 of file parser.h.
Referenced by getGroupedSoftAssertions().
| std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::soft_assertions |
Definition at line 274 of file parser.h.
Referenced by getNodeCount(), and getSoftAssertions().
| std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::soft_weights |
Definition at line 275 of file parser.h.
Referenced by getNodeCount(), and getSoftWeights().
|
private |
Definition at line 212 of file parser.h.
Referenced by declareVar(), dumpSMT2(), getSortNames(), mkArray(), mkConstBv(), mkConstFp(), mkVarBv(), mkVarFp(), parseCommand(), Parser(), Parser(), and parseSort().
|
private |
Definition at line 203 of file parser.h.
Referenced by mkArray(), mkArraySort(), mkBvComp(), mkBvConcat(), mkBvExtract(), mkBvRepeat(), mkBvRotateLeft(), mkBvRotateRight(), mkBvSignExt(), mkBVSort(), mkBvZeroExt(), mkConstBv(), mkConstFp(), mkFpConst(), mkFPSort(), mkFpToSbv(), mkFpToUbv(), mkIntToBv(), mkNatToBv(), mkSortDec(), mkSortDef(), mkStrSplit(), mkToFp(), mkToFp(), mkToFpUnsigned(), mkVarBv(), mkVarFp(), parseCommand(), parseExpr(), parseOper(), Parser(), Parser(), and parseSort().
| std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::split_lemmas |
|
private |
Definition at line 218 of file parser.h.
Referenced by mkApplyFunc(), mkApplyRecFunc(), Parser(), and Parser().
|
private |
Definition at line 233 of file parser.h.
Referenced by mkTempVar(), Parser(), and Parser().
|
private |
Definition at line 234 of file parser.h.
Referenced by getTempVarNames(), getVariable(), getVariables(), mkTempVar(), Parser(), Parser(), and rename().
|
private |
Definition at line 231 of file parser.h.
Referenced by getDeclaredVariables(), getVariable(), getVariables(), getVarNames(), isDeclaredVariable(), mkVar(), parseConstFunc(), Parser(), Parser(), and rename().