SMTStabilizer API
Public API documentation for SMTStabilizer
Loading...
Searching...
No Matches
stabilizer::parser::Parser Class Reference

#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< DAGNodemkUFVNode (const std::string &name, const std::shared_ptr< Sort > &sort)
 
std::shared_ptr< DAGNoderebuildLetBindings (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< DAGNodemkExpr (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< GlobalOptionsgetOptions () 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< DAGNodegetVariable (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< SortgetSort (const std::vector< std::shared_ptr< DAGNode > > &params)
 Get sort.
 
std::shared_ptr< SortgetSort (std::shared_ptr< DAGNode > param)
 Get sort.
 
std::shared_ptr< SortgetSort (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Get sort.
 
std::shared_ptr< SortgetSort (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< DAGNodegetResult ()
 Get result.
 
RESULT_TYPE checkSat ()
 Check satisfiability.
 
size_t getNodeCount ()
 Get node count.
 
std::shared_ptr< DAGNodemkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, std::shared_ptr< DAGNode > p)
 Create an operation.
 
std::shared_ptr< DAGNodemkOper (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< DAGNodemkOper (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< DAGNodemkOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, const std::vector< std::shared_ptr< DAGNode > > &p)
 Create an operation.
 
std::shared_ptr< DAGNoderewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &p)
 Rewrite unary operation node when simplification rule applies.
 
std::shared_ptr< DAGNoderewrite (NODE_KIND &t, std::shared_ptr< DAGNode > &l, std::shared_ptr< DAGNode > &r)
 Rewrite binary operation node when simplification rule applies.
 
std::shared_ptr< DAGNoderewrite (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< DAGNoderewrite (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< DAGNoderewrite (NODE_KIND &t, std::vector< std::shared_ptr< DAGNode > > &p)
 Rewrite variadic operation node when simplification rule applies.
 
std::shared_ptr< DAGNoderewrite_oper (NODE_KIND &t, std::vector< std::shared_ptr< DAGNode > > &p)
 Core operation rewrite helper used before node-manager creation.
 
std::unique_ptr< NodeManagergetNodeManager ()
 
void rebuild_node_manager ()
 
std::shared_ptr< DAGNodemkNode (std::shared_ptr< Sort > sort, NODE_KIND t, std::string name, std::vector< std::shared_ptr< DAGNode > > params)
 
std::shared_ptr< DAGNodemkFuncDec (const std::string &name, const std::vector< std::shared_ptr< Sort > > &params, std::shared_ptr< Sort > out_sort)
 Create a function declaration.
 
std::shared_ptr< DAGNodemkFuncDef (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.
 
std::shared_ptr< DAGNodemkFuncRec (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.
 
std::shared_ptr< DAGNodemkApplyRecFunc (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a recursive function application.
 
std::shared_ptr< DAGNodemkPattern (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > &params)
 
std::shared_ptr< DAGNodemkNoPattern (const std::shared_ptr< Sort > &sort, const std::string &name, std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkWeight (const std::shared_ptr< Sort > &sort, const std::string &name, std::shared_ptr< DAGNode > weight)
 
std::shared_ptr< DAGNodemkAttribute (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > &params)
 
std::shared_ptr< DAGNodemkApplyUF (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > &params)
 Apply an uninterpreted function.
 
std::shared_ptr< SortmkSortDec (const std::string &name, const size_t &arity)
 Create a sort declaration.
 
std::shared_ptr< SortmkSortDef (const std::string &name, const std::vector< std::shared_ptr< Sort > > &params, std::shared_ptr< Sort > out_sort)
 Create a sort definition.
 
std::shared_ptr< SortmkIntSort ()
 Create an integer sort.
 
std::shared_ptr< SortmkRealSort ()
 Create a real sort.
 
std::shared_ptr< SortmkBoolSort ()
 Create a boolean sort.
 
std::shared_ptr< SortmkStrSort ()
 Create a string sort.
 
std::shared_ptr< SortmkRegSort ()
 Create a regular expression sort.
 
std::shared_ptr< SortmkRoundingModeSort ()
 Create a rounding mode sort.
 
std::shared_ptr< SortmkNatSort ()
 Create a natural sort.
 
std::shared_ptr< SortmkBVSort (const size_t &width)
 Create a bit-vector sort.
 
std::shared_ptr< SortmkFPSort (const size_t &e, const size_t &s)
 Create a floating-point sort.
 
std::shared_ptr< SortmkArraySort (std::shared_ptr< Sort > index, std::shared_ptr< Sort > elem)
 Create an array sort.
 
std::shared_ptr< DAGNodedeclareVar (const std::string &name, const std::string &sort)
 Declare a variable.
 
std::shared_ptr< DAGNodedeclareVar (const std::string &name, const std::shared_ptr< Sort > &sort)
 Declare a variable.
 
std::shared_ptr< DAGNodemkTrue ()
 Create a true node.
 
std::shared_ptr< DAGNodemkFalse ()
 Create a false node.
 
std::shared_ptr< DAGNodemkUnknown ()
 Create an unknown node.
 
std::shared_ptr< DAGNodemkEq (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an equality node.
 
std::shared_ptr< DAGNodemkDistinct (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a distinct node.
 
std::shared_ptr< DAGNodemkConstInt (const std::string &v)
 Create an integer constant from string.
 
std::shared_ptr< DAGNodemkConstInt (const int &v)
 Create an integer constant.
 
std::shared_ptr< DAGNodemkConstInt (const Integer &v)
 Create an integer constant.
 
std::shared_ptr< DAGNodemkConstInt (const Number &v)
 Create a real constant from number.
 
std::shared_ptr< DAGNodemkConstReal (const std::string &v)
 Create a real constant from string.
 
std::shared_ptr< DAGNodemkConstReal (const Real &v)
 Create a real constant.
 
std::shared_ptr< DAGNodemkConstReal (const double &v)
 Create a real constant from double.
 
std::shared_ptr< DAGNodemkConstReal (const Integer &v)
 Create a real constant from integer.
 
std::shared_ptr< DAGNodemkConstReal (const Number &v)
 Create a real constant from number.
 
std::shared_ptr< DAGNodemkConstStr (const std::string &v)
 Create a string constant.
 
std::shared_ptr< DAGNodemkConstBv (const std::string &v, const size_t &width)
 Create a bit-vector constant.
 
std::shared_ptr< DAGNodemkConstFp (const std::string &v, const size_t &e, const size_t &s)
 Create a floating-point constant.
 
std::shared_ptr< DAGNodemkConstFP (const std::string &fp_expr)
 Create a floating-point constant from expression.
 
std::shared_ptr< DAGNodemkConstReg (const std::string &v)
 Create a regular expression constant.
 
std::shared_ptr< DAGNodemkRoundingMode (const std::string &mode)
 Create a rounding mode constant.
 
std::shared_ptr< DAGNodemkVarRoundingMode (const std::string &name)
 Create a rounding mode variable.
 
std::shared_ptr< DAGNodemkVar (const std::shared_ptr< Sort > &sort, const std::string &name)
 Create a variable.
 
std::shared_ptr< DAGNodemkPlaceholderVar (const std::string &name)
 
std::shared_ptr< DAGNodemkTempVar (const std::shared_ptr< Sort > &sort)
 Create a temporary variable.
 
std::shared_ptr< DAGNodemkVarBool (const std::string &name)
 Create a boolean variable.
 
std::shared_ptr< DAGNodemkVarInt (const std::string &name)
 Create an integer variable.
 
std::shared_ptr< DAGNodemkVarReal (const std::string &name)
 Create a real variable.
 
std::shared_ptr< DAGNodemkVarBv (const std::string &name, const size_t &width)
 Create a bit-vector variable.
 
std::shared_ptr< DAGNodemkVarFp (const std::string &name, const size_t &e, const size_t &s)
 Create a floating-point variable.
 
std::shared_ptr< DAGNodemkVarStr (const std::string &name)
 Create a string variable.
 
std::shared_ptr< DAGNodemkVarReg (const std::string &name)
 Create a regular expression variable.
 
std::shared_ptr< DAGNodemkFunParamVar (std::shared_ptr< Sort > sort, const std::string &name)
 Create a function parameter variable.
 
std::shared_ptr< DAGNodemkArray (const std::string &name, std::shared_ptr< Sort > index, std::shared_ptr< Sort > elem)
 Create an array.
 
std::shared_ptr< DAGNodemkConstArray (std::shared_ptr< Sort > sort, std::shared_ptr< DAGNode > value)
 Create a constant array node.
 
std::shared_ptr< DAGNodemkNot (std::shared_ptr< DAGNode > param)
 Create a not node.
 
std::shared_ptr< DAGNodemkAnd (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an and node.
 
std::shared_ptr< DAGNodemkOr (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an or node.
 
std::shared_ptr< DAGNodemkImplies (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an implies node.
 
std::shared_ptr< DAGNodemkXor (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an xor node.
 
std::shared_ptr< DAGNodemkIte (std::shared_ptr< DAGNode > cond, std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an ite node.
 
std::shared_ptr< DAGNodemkIte (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an ite node.
 
std::shared_ptr< DAGNodemkAdd (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an add node.
 
std::shared_ptr< DAGNodemkMul (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an mul node.
 
std::shared_ptr< DAGNodemkIand (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an iand node.
 
std::shared_ptr< DAGNodemkPow2 (std::shared_ptr< DAGNode > param)
 Create an pow2 node.
 
std::shared_ptr< DAGNodemkPow (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an pow node.
 
std::shared_ptr< DAGNodemkSub (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an sub node.
 
std::shared_ptr< DAGNodemkNeg (std::shared_ptr< DAGNode > param)
 Create an neg node.
 
std::shared_ptr< DAGNodemkDiv (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an div node.
 
std::shared_ptr< DAGNodemkDivInt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an div node.
 
std::shared_ptr< DAGNodemkDivReal (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an div node.
 
std::shared_ptr< DAGNodemkMod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an mod node.
 
std::shared_ptr< DAGNodemkAbs (std::shared_ptr< DAGNode > param)
 Create an abs node.
 
std::shared_ptr< DAGNodemkSqrt (std::shared_ptr< DAGNode > param)
 Create an sqrt node.
 
std::shared_ptr< DAGNodemkSafeSqrt (std::shared_ptr< DAGNode > param)
 Create an safeSqrt node.
 
std::shared_ptr< DAGNodemkCeil (std::shared_ptr< DAGNode > param)
 Create an ceil node.
 
std::shared_ptr< DAGNodemkFloor (std::shared_ptr< DAGNode > param)
 Create an floor node.
 
std::shared_ptr< DAGNodemkRound (std::shared_ptr< DAGNode > param)
 Create an round node.
 
std::shared_ptr< DAGNodemkExp (std::shared_ptr< DAGNode > param)
 Create an exp node.
 
std::shared_ptr< DAGNodemkLn (std::shared_ptr< DAGNode > param)
 Create an ln node.
 
std::shared_ptr< DAGNodemkLg (std::shared_ptr< DAGNode > param)
 Create an lg/log10 node.
 
std::shared_ptr< DAGNodemkLb (std::shared_ptr< DAGNode > param)
 Create an lb/log2 node.
 
std::shared_ptr< DAGNodemkLog (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an log node.
 
std::shared_ptr< DAGNodemkSin (std::shared_ptr< DAGNode > param)
 Create an sin node.
 
std::shared_ptr< DAGNodemkCos (std::shared_ptr< DAGNode > param)
 Create an cos node.
 
std::shared_ptr< DAGNodemkSec (std::shared_ptr< DAGNode > param)
 Create an sec node.
 
std::shared_ptr< DAGNodemkCsc (std::shared_ptr< DAGNode > param)
 Create an csc node.
 
std::shared_ptr< DAGNodemkTan (std::shared_ptr< DAGNode > param)
 Create an tan node.
 
std::shared_ptr< DAGNodemkCot (std::shared_ptr< DAGNode > param)
 Create a cot node.
 
std::shared_ptr< DAGNodemkAsin (std::shared_ptr< DAGNode > param)
 Create an asin node.
 
std::shared_ptr< DAGNodemkAcos (std::shared_ptr< DAGNode > param)
 Create an acos node.
 
std::shared_ptr< DAGNodemkAsec (std::shared_ptr< DAGNode > param)
 Create an asec node.
 
std::shared_ptr< DAGNodemkAcsc (std::shared_ptr< DAGNode > param)
 Create an acsc node.
 
std::shared_ptr< DAGNodemkAtan (std::shared_ptr< DAGNode > param)
 Create an atan node.
 
std::shared_ptr< DAGNodemkAcot (std::shared_ptr< DAGNode > param)
 Create an acot node.
 
std::shared_ptr< DAGNodemkSinh (std::shared_ptr< DAGNode > param)
 Create a sinh node.
 
std::shared_ptr< DAGNodemkCosh (std::shared_ptr< DAGNode > param)
 Create a cosh node.
 
std::shared_ptr< DAGNodemkTanh (std::shared_ptr< DAGNode > param)
 Create a tanh node.
 
std::shared_ptr< DAGNodemkSech (std::shared_ptr< DAGNode > param)
 Create a sech node.
 
std::shared_ptr< DAGNodemkCsch (std::shared_ptr< DAGNode > param)
 Create a csch node.
 
std::shared_ptr< DAGNodemkCoth (std::shared_ptr< DAGNode > param)
 Create a coth node.
 
std::shared_ptr< DAGNodemkAsinh (std::shared_ptr< DAGNode > param)
 Create an asinh node.
 
std::shared_ptr< DAGNodemkAcosh (std::shared_ptr< DAGNode > param)
 Create an acosh node.
 
std::shared_ptr< DAGNodemkAtanh (std::shared_ptr< DAGNode > param)
 Create an atanh node.
 
std::shared_ptr< DAGNodemkAsech (std::shared_ptr< DAGNode > param)
 Create an asech node.
 
std::shared_ptr< DAGNodemkAcsch (std::shared_ptr< DAGNode > param)
 Create an acsch node.
 
std::shared_ptr< DAGNodemkAcoth (std::shared_ptr< DAGNode > param)
 Create an acoth node.
 
std::shared_ptr< DAGNodemkAtan2 (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an atan2 node.
 
std::shared_ptr< DAGNodemkLe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a le node.
 
std::shared_ptr< DAGNodemkLt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a lt node.
 
std::shared_ptr< DAGNodemkGe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a ge node.
 
std::shared_ptr< DAGNodemkGt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a gt node.
 
std::shared_ptr< DAGNodemkToInt (std::shared_ptr< DAGNode > param)
 Create a to_int node.
 
std::shared_ptr< DAGNodemkToReal (std::shared_ptr< DAGNode > param)
 Create a to_real node.
 
std::shared_ptr< DAGNodemkIsInt (std::shared_ptr< DAGNode > param)
 Create a is_int node.
 
std::shared_ptr< DAGNodemkIsDivisible (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a is_divisible node.
 
std::shared_ptr< DAGNodemkIsPrime (std::shared_ptr< DAGNode > param)
 Create a is_prime node.
 
std::shared_ptr< DAGNodemkIsEven (std::shared_ptr< DAGNode > param)
 Create a is_even node.
 
std::shared_ptr< DAGNodemkIsOdd (std::shared_ptr< DAGNode > param)
 Create a is_odd node.
 
std::shared_ptr< DAGNodemkPi ()
 Create a pi node.
 
std::shared_ptr< DAGNodemkE ()
 Create a e node.
 
std::shared_ptr< DAGNodemkInfinity (std::shared_ptr< Sort > sort)
 Create a infinity node.
 
std::shared_ptr< DAGNodemkPosInfinity (std::shared_ptr< Sort > sort=nullptr)
 Create a positive infinity node.
 
std::shared_ptr< DAGNodemkNegInfinity (std::shared_ptr< Sort > sort=nullptr)
 Create a negative infinity node.
 
std::shared_ptr< DAGNodemkNaN (std::shared_ptr< Sort > sort=nullptr)
 Create a NaN node.
 
std::shared_ptr< DAGNodemkEpsilon ()
 Create a epsilon node.
 
std::shared_ptr< DAGNodemkPosEpsilon ()
 Create a positive epsilon node.
 
std::shared_ptr< DAGNodemkNegEpsilon ()
 Create a negative epsilon node.
 
std::shared_ptr< DAGNodemkGcd (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a gcd node.
 
std::shared_ptr< DAGNodemkLcm (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a lcm node.
 
std::shared_ptr< DAGNodemkFact (std::shared_ptr< DAGNode > param)
 Create a factorial node.
 
std::shared_ptr< DAGNodemkBvNot (std::shared_ptr< DAGNode > param)
 Create a bitvector not node.
 
std::shared_ptr< DAGNodemkBvAnd (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector and node.
 
std::shared_ptr< DAGNodemkBvOr (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector or node.
 
std::shared_ptr< DAGNodemkBvXor (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector xor node.
 
std::shared_ptr< DAGNodemkBvNand (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector nand node.
 
std::shared_ptr< DAGNodemkBvNor (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector nor node.
 
std::shared_ptr< DAGNodemkBvComp (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector comparison node.
 
std::shared_ptr< DAGNodemkBvXnor (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector xnor node.
 
std::shared_ptr< DAGNodemkBvNeg (std::shared_ptr< DAGNode > param)
 Create a bitvector negation node.
 
std::shared_ptr< DAGNodemkBvAdd (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector addition node.
 
std::shared_ptr< DAGNodemkBvSub (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector subtraction node.
 
std::shared_ptr< DAGNodemkBvMul (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector multiplication node.
 
std::shared_ptr< DAGNodemkBvUdiv (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned division node.
 
std::shared_ptr< DAGNodemkBvUrem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned remainder node.
 
std::shared_ptr< DAGNodemkBvUmod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned modulo node.
 
std::shared_ptr< DAGNodemkBvSdiv (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed division node.
 
std::shared_ptr< DAGNodemkBvSrem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed remainder node.
 
std::shared_ptr< DAGNodemkBvSmod (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed modulo node.
 
std::shared_ptr< DAGNodemkBvShl (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector shift left node.
 
std::shared_ptr< DAGNodemkBvLshr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector logical shift right node.
 
std::shared_ptr< DAGNodemkBvAshr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector arithmetic shift right node.
 
std::shared_ptr< DAGNodemkBvConcat (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a bitvector concatenation node.
 
std::shared_ptr< DAGNodemkBvExtract (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 Create a bitvector extract node.
 
std::shared_ptr< DAGNodemkBvRepeat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector repeat node.
 
std::shared_ptr< DAGNodemkBvZeroExt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector zero extension node.
 
std::shared_ptr< DAGNodemkBvSignExt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector sign extension node.
 
std::shared_ptr< DAGNodemkBvRotateLeft (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector rotate left node.
 
std::shared_ptr< DAGNodemkBvRotateRight (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector rotate right node.
 
std::shared_ptr< DAGNodemkBvUlt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned less than node.
 
std::shared_ptr< DAGNodemkBvUle (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned less than or equal node.
 
std::shared_ptr< DAGNodemkBvUgt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned greater than node.
 
std::shared_ptr< DAGNodemkBvUge (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector unsigned greater than or equal node.
 
std::shared_ptr< DAGNodemkBvSlt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed less than node.
 
std::shared_ptr< DAGNodemkBvSle (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed less than or equal node.
 
std::shared_ptr< DAGNodemkBvSgt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed greater than node.
 
std::shared_ptr< DAGNodemkBvSge (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a bitvector signed greater than or equal node.
 
std::shared_ptr< DAGNodemkBvToNat (std::shared_ptr< DAGNode > param)
 Create a bitvector to natural number conversion node.
 
std::shared_ptr< DAGNodemkNatToBv (std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > width)
 Create a natural number to bitvector conversion node.
 
std::shared_ptr< DAGNodemkBvToInt (std::shared_ptr< DAGNode > param)
 Create a bitvector to integer conversion node.
 
std::shared_ptr< DAGNodemkUbvToInt (std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkSbvToInt (std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkIntToBv (std::shared_ptr< DAGNode > param, std::shared_ptr< DAGNode > width)
 Create an integer to bitvector conversion node.
 
std::shared_ptr< DAGNodemkFpAdd (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point addition node.
 
std::shared_ptr< DAGNodemkFpSub (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point subtraction node.
 
std::shared_ptr< DAGNodemkFpMul (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point multiplication node.
 
std::shared_ptr< DAGNodemkFpDiv (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point division node.
 
std::shared_ptr< DAGNodemkFpAbs (std::shared_ptr< DAGNode > param)
 Create a floating-point absolute value node.
 
std::shared_ptr< DAGNodemkFpNeg (std::shared_ptr< DAGNode > param)
 Create a floating-point negation node.
 
std::shared_ptr< DAGNodemkFpRem (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a floating-point remainder node.
 
std::shared_ptr< DAGNodemkFpFma (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point fused multiply-add node.
 
std::shared_ptr< DAGNodemkFpSqrt (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param)
 Create a floating-point square root node.
 
std::shared_ptr< DAGNodemkFpSqrt (std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkFpRoundToIntegral (std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param)
 Create a floating-point round to integral node.
 
std::shared_ptr< DAGNodemkFpRoundToIntegral (std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkFpMin (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a floating-point minimum node.
 
std::shared_ptr< DAGNodemkFpMax (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a floating-point maximum node.
 
std::shared_ptr< DAGNodemkFpLe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point less than or equal node.
 
std::shared_ptr< DAGNodemkFpLt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point less than node.
 
std::shared_ptr< DAGNodemkFpGe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point greater than or equal node.
 
std::shared_ptr< DAGNodemkFpGt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point greater than node.
 
std::shared_ptr< DAGNodemkFpEq (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a floating-point equality node.
 
std::shared_ptr< DAGNodemkFpToUbv (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< DAGNodemkFpToSbv (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< DAGNodemkFpToReal (std::shared_ptr< DAGNode > param)
 Create a floating-point to real conversion node.
 
std::shared_ptr< DAGNodemkToFp (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< DAGNodemkToFp (std::shared_ptr< DAGNode > eb, std::shared_ptr< DAGNode > sb, std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkToFpUnsigned (std::shared_ptr< DAGNode > eb, std::shared_ptr< DAGNode > sb, std::shared_ptr< DAGNode > rm, std::shared_ptr< DAGNode > param)
 
std::shared_ptr< DAGNodemkFpConst (std::shared_ptr< DAGNode > sign, std::shared_ptr< DAGNode > exp, std::shared_ptr< DAGNode > mant)
 
std::shared_ptr< DAGNodemkRootObj (std::shared_ptr< DAGNode > expr, int index)
 
std::shared_ptr< DAGNodemkRootOfWithInterval (const std::vector< std::shared_ptr< DAGNode > > &coeffs, std::shared_ptr< DAGNode > lower_bound, std::shared_ptr< DAGNode > upper_bound)
 
std::shared_ptr< DAGNodemkFpIsNormal (std::shared_ptr< DAGNode > param)
 Create a floating-point is-normal check node.
 
std::shared_ptr< DAGNodemkFpIsSubnormal (std::shared_ptr< DAGNode > param)
 Create a floating-point is-subnormal check node.
 
std::shared_ptr< DAGNodemkFpIsZero (std::shared_ptr< DAGNode > param)
 Create a floating-point is-zero check node.
 
std::shared_ptr< DAGNodemkFpIsInf (std::shared_ptr< DAGNode > param)
 Create a floating-point is-infinity check node.
 
std::shared_ptr< DAGNodemkFpIsNaN (std::shared_ptr< DAGNode > param)
 Create a floating-point is-NaN check node.
 
std::shared_ptr< DAGNodemkFpIsNeg (std::shared_ptr< DAGNode > param)
 Create a floating-point is-negative check node.
 
std::shared_ptr< DAGNodemkFpIsPos (std::shared_ptr< DAGNode > param)
 Create a floating-point is-positive check node.
 
std::shared_ptr< DAGNodemkSelect (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create an array select node.
 
std::shared_ptr< DAGNodemkStore (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create an array store node.
 
std::shared_ptr< DAGNodemkStrLen (std::shared_ptr< DAGNode > param)
 Create a string length node.
 
std::shared_ptr< DAGNodemkStrConcat (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a string concatenation node.
 
std::shared_ptr< DAGNodemkStrSubstr (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 Create a string substring node.
 
std::shared_ptr< DAGNodemkStrPrefixof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string prefix check node.
 
std::shared_ptr< DAGNodemkStrSuffixof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string suffix check node.
 
std::shared_ptr< DAGNodemkStrIndexof (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 Create a string index-of node.
 
std::shared_ptr< DAGNodemkStrCharat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string char-at node.
 
std::shared_ptr< DAGNodemkStrUpdate (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create a string update node.
 
std::shared_ptr< DAGNodemkStrReplace (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create a string replace node.
 
std::shared_ptr< DAGNodemkStrReplaceAll (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create a string replace-all node.
 
std::shared_ptr< DAGNodemkStrReplaceReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create a string replace-regex node.
 
std::shared_ptr< DAGNodemkStrReplaceRegAll (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< DAGNodemkStrIndexofReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string indexof-regex node.
 
std::shared_ptr< DAGNodemkStrToLower (std::shared_ptr< DAGNode > param)
 Create a string to-lower node.
 
std::shared_ptr< DAGNodemkStrToUpper (std::shared_ptr< DAGNode > param)
 Create a string to-upper node.
 
std::shared_ptr< DAGNodemkStrRev (std::shared_ptr< DAGNode > param)
 Create a string reverse node.
 
std::shared_ptr< DAGNodemkStrSplit (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string split node.
 
std::shared_ptr< DAGNodemkStrSplitAt (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 
std::shared_ptr< DAGNodemkStrSplitRest (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 
std::shared_ptr< DAGNodemkStrNumSplits (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 
std::shared_ptr< DAGNodemkStrSplitAtRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 
std::shared_ptr< DAGNodemkStrSplitRestRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 
std::shared_ptr< DAGNodemkStrNumSplitsRe (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 
std::shared_ptr< DAGNodemkStrLt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a string less-than node.
 
std::shared_ptr< DAGNodemkStrLe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a string less-than-or-equal node.
 
std::shared_ptr< DAGNodemkStrGt (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a string greater-than node.
 
std::shared_ptr< DAGNodemkStrGe (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a string greater-than-or-equal node.
 
std::shared_ptr< DAGNodemkStrInReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string in-regex check node.
 
std::shared_ptr< DAGNodemkStrContains (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string contains check node.
 
std::shared_ptr< DAGNodemkStrIsDigit (std::shared_ptr< DAGNode > param)
 Create a string is-digit check node.
 
std::shared_ptr< DAGNodemkStrFromInt (std::shared_ptr< DAGNode > param)
 Create a string from-integer conversion node.
 
std::shared_ptr< DAGNodemkStrToInt (std::shared_ptr< DAGNode > param)
 Create a string to-integer conversion node.
 
std::shared_ptr< DAGNodemkStrToReg (std::shared_ptr< DAGNode > param)
 Create a string to-regex conversion node.
 
std::shared_ptr< DAGNodemkStrToCode (std::shared_ptr< DAGNode > param)
 Create a string to-code conversion node.
 
std::shared_ptr< DAGNodemkStrFromCode (std::shared_ptr< DAGNode > param)
 Create a string from-code conversion node.
 
std::shared_ptr< DAGNodemkRegNone ()
 Create a regex none node.
 
std::shared_ptr< DAGNodemkRegAll ()
 Create a regex all node.
 
std::shared_ptr< DAGNodemkRegAllChar ()
 Create a regex allchar node.
 
std::shared_ptr< DAGNodemkRegConcat (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a regex concatenation node.
 
std::shared_ptr< DAGNodemkRegUnion (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a regex union node.
 
std::shared_ptr< DAGNodemkRegInter (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a regex intersection node.
 
std::shared_ptr< DAGNodemkRegDiff (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a regex difference node.
 
std::shared_ptr< DAGNodemkRegStar (std::shared_ptr< DAGNode > param)
 Create a regex star node.
 
std::shared_ptr< DAGNodemkRegPlus (std::shared_ptr< DAGNode > param)
 Create a regex plus node.
 
std::shared_ptr< DAGNodemkRegOpt (std::shared_ptr< DAGNode > param)
 Create a regex option node.
 
std::shared_ptr< DAGNodemkRegRange (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a regex range node.
 
std::shared_ptr< DAGNodemkRegRepeat (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a regex repeat node.
 
std::shared_ptr< DAGNodemkRegLoop (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > s)
 Create a regex loop node.
 
std::shared_ptr< DAGNodemkRegComplement (std::shared_ptr< DAGNode > param)
 Create a regex complement node.
 
std::shared_ptr< DAGNodemkReplaceReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r, std::shared_ptr< DAGNode > v)
 Create a string replace-regex node.
 
std::shared_ptr< DAGNodemkReplaceRegAll (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< DAGNodemkIndexofReg (std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
 Create a string index-of-regex node.
 
std::shared_ptr< DAGNodemkMax (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a max node.
 
std::shared_ptr< DAGNodemkMin (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a min node.
 
std::shared_ptr< DAGNodemkLet (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a let node.
 
std::shared_ptr< DAGNodemkQuantVar (const std::string &name, std::shared_ptr< Sort > sort)
 Create a quantifier variable node.
 
std::shared_ptr< DAGNodemkForall (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create a forall node.
 
std::shared_ptr< DAGNodemkExists (const std::vector< std::shared_ptr< DAGNode > > &params)
 Create an exists node.
 
std::shared_ptr< DAGNodemkApplyFunc (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > &params)
 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< DAGNodegetZero (std::shared_ptr< Sort > sort)
 Get the zero for a sort.
 
std::shared_ptr< DAGNodesubstitute (std::shared_ptr< DAGNode > expr, std::unordered_map< std::string, std::shared_ptr< DAGNode > > &params)
 Substitute variables in an expression.
 
std::shared_ptr< DAGNodeapplyFun (std::shared_ptr< DAGNode > fun, const std::vector< std::shared_ptr< DAGNode > > &params)
 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< DAGNodeexpandLet (std::shared_ptr< DAGNode > expr)
 Expand a let expression.
 
std::vector< std::shared_ptr< DAGNode > > getSplitLemmas ()
 Get the split lemmas.
 
std::shared_ptr< DAGNoderemove (std::shared_ptr< DAGNode > expr, const std::unordered_set< std::shared_ptr< DAGNode > > &nodes)
 Remove all the nodes in the expression.
 
std::shared_ptr< DAGNoderename (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< DAGNodemkApplyDTFun (const std::shared_ptr< Sort > &sort, const std::string &name, const std::vector< std::shared_ptr< DAGNode > > &params)
 
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< SortparseSort ()
 
std::shared_ptr< DAGNodeparseExpr ()
 
std::shared_ptr< DAGNodeparseConstFunc (const std::string &s)
 
std::shared_ptr< DAGNodeparseOper (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< DAGNodeparsePreservingLet ()
 
std::shared_ptr< DAGNodeparseLet ()
 
std::shared_ptr< DAGNodemkLetBindVar (const std::string &name, const std::shared_ptr< DAGNode > &expr)
 
std::shared_ptr< DAGNodemkLetBindVarList (const std::vector< std::shared_ptr< DAGNode > > &bind_vars)
 
std::shared_ptr< DAGNodemkLetChain (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< DAGNodeparseQuant (const std::string &type)
 
KEYWORD attemptParseKeywords ()
 
std::shared_ptr< DAGNodemkInternalOper (const std::shared_ptr< Sort > &sort, const NODE_KIND &t, const std::vector< std::shared_ptr< DAGNode > > &p)
 
std::shared_ptr< DAGNodebindLetVar (const std::string &key, std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodebindFunVar (const std::string &key, std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodesubstitute (std::shared_ptr< DAGNode > expr, std::unordered_map< std::string, std::shared_ptr< DAGNode > > &params, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited)
 
std::shared_ptr< DAGNodeapplyFunPostOrder (std::shared_ptr< DAGNode > node, std::unordered_map< std::string, std::shared_ptr< DAGNode > > &params)
 
std::shared_ptr< DAGNodereplaceAtoms (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< DAGNodereplaceNodes (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< DAGNodetoCNF (std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodetoTseitinCNF (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< DAGNodetoTseitinXor (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses)
 
std::shared_ptr< DAGNodetoTseitinEq (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses)
 
std::shared_ptr< DAGNodetoTseitinDistinct (std::shared_ptr< DAGNode > a, std::shared_ptr< DAGNode > b, std::vector< std::shared_ptr< DAGNode > > &clauses)
 
std::shared_ptr< DAGNodetoDNFEliminateAll (std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodetoDNFEliminateAll (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited, bool &is_changed)
 
std::shared_ptr< DAGNodetoDNFEliminateXOR (const std::vector< std::shared_ptr< DAGNode > > &children)
 
std::shared_ptr< DAGNodetoDNFEliminateEq (const std::vector< std::shared_ptr< DAGNode > > &children)
 
std::shared_ptr< DAGNodetoDNFEliminateDistinct (const std::vector< std::shared_ptr< DAGNode > > &children)
 
std::shared_ptr< DAGNodeapplyDNFDistributiveLaw (std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodeapplyDNFDistributiveLawRec (std::shared_ptr< DAGNode > expr, std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &visited)
 
std::shared_ptr< DAGNodeflattenDNF (std::shared_ptr< DAGNode > expr)
 
std::shared_ptr< DAGNodetoNNF (std::shared_ptr< DAGNode > expr, bool is_not)
 
std::shared_ptr< DAGNoderemove (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< DAGNodemkErr (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< Sortplaceholder_var_sort
 
bool parsing_file
 
std::vector< std::string > parse_options
 
std::unique_ptr< NodeManagernode_manager
 
std::unique_ptr< SortManagersort_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< GlobalOptionsoptions
 
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< DAGNoderesult_node
 
size_t num_quant_vars = 0
 

Detailed Description

Definition at line 163 of file parser.h.

Constructor & Destructor Documentation

◆ Parser() [1/2]

stabilizer::parser::Parser::Parser ( const std::string &  filename)

◆ Parser() [2/2]

◆ ~Parser()

stabilizer::parser::Parser::~Parser ( )

Destructor.

Releases all resources used by the Parser

Definition at line 116 of file base_parser.cpp.

Member Function Documentation

◆ applyDNFDistributiveLaw()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::applyDNFDistributiveLaw ( std::shared_ptr< DAGNode expr)
private

◆ applyDNFDistributiveLawRec()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::applyDNFDistributiveLawRec ( std::shared_ptr< DAGNode expr,
std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &  visited 
)
private

◆ applyFun()

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.

Parameters
funFunction node
paramsList of parameters
Returns
Applied function (fun(p1, p2, ..., pn))

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().

◆ applyFunPostOrder()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::applyFunPostOrder ( std::shared_ptr< DAGNode node,
std::unordered_map< std::string, std::shared_ptr< DAGNode > > &  params 
)
private

◆ assert() [1/2]

bool stabilizer::parser::Parser::assert ( const std::string &  constraint)

Assert a constraint.

Asserts the specified constraint and builds internal data structures.

Note
Any variables in the constraint must be declared before assertion.
Parameters
constraintConstraint to assert
Returns
True if assertion was successful, false otherwise

Definition at line 717 of file base_parser.cpp.

References assertions, mkExpr(), and parsing_file.

◆ assert() [2/2]

bool stabilizer::parser::Parser::assert ( std::shared_ptr< DAGNode node)

Assert a constraint.

Asserts the specified constraint and builds internal data structures.

Parameters
nodeConstraint to assert
Returns
True if assertion was successful, false otherwise

Definition at line 724 of file base_parser.cpp.

References assertions.

◆ attemptParseKeywords()

KEYWORD stabilizer::parser::Parser::attemptParseKeywords ( )
private

Definition at line 33 of file opt_parser.cpp.

References bufptr, stabilizer::parser::KW_NULL, and parseKeyword().

Referenced by parseCommand(), and parseExpr().

◆ bindFunVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::bindFunVar ( const std::string &  key,
std::shared_ptr< DAGNode expr 
)
private

◆ bindLetVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::bindLetVar ( const std::string &  key,
std::shared_ptr< DAGNode expr 
)
private

◆ checkSat()

RESULT_TYPE stabilizer::parser::Parser::checkSat ( )

Check satisfiability.

Returns
True if satisfiable, false otherwise

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.

◆ clear_let_key_map()

void stabilizer::parser::Parser::clear_let_key_map ( )
inline

Definition at line 332 of file parser.h.

References preserving_let_key_map.

Referenced by rebuildLetBindings().

◆ collectAtoms()

void stabilizer::parser::Parser::collectAtoms ( std::shared_ptr< DAGNode expr,
std::unordered_set< std::shared_ptr< DAGNode > > &  atoms,
std::unordered_set< std::shared_ptr< DAGNode > > &  visited 
)
private

◆ collectGroundAtoms()

void stabilizer::parser::Parser::collectGroundAtoms ( std::shared_ptr< DAGNode expr,
std::unordered_set< std::shared_ptr< DAGNode > > &  atoms,
std::unordered_set< std::shared_ptr< DAGNode > > &  visited 
)
private

◆ collectVars()

void stabilizer::parser::Parser::collectVars ( std::shared_ptr< DAGNode expr,
std::unordered_set< std::shared_ptr< DAGNode > > &  vars,
std::unordered_set< std::shared_ptr< DAGNode > > &  visited 
)
private

◆ declareVar() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::declareVar ( const std::string &  name,
const std::shared_ptr< Sort > &  sort 
)

Declare a variable.

Parameters
nameVariable name
sortSort

Definition at line 624 of file op_parser.cpp.

References mkVar().

◆ declareVar() [2/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::declareVar ( const std::string &  name,
const std::string &  sort 
)

Declare a variable.

Parameters
nameVariable name
sortSort

Definition at line 620 of file op_parser.cpp.

References mkVar(), and sort_key_map.

◆ dumpSMT2() [1/2]

std::string stabilizer::parser::Parser::dumpSMT2 ( )

Dump the SMT2 representation of the parsed expressions.

Returns
String representation of the SMT2

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().

◆ dumpSMT2() [2/2]

std::string stabilizer::parser::Parser::dumpSMT2 ( const std::string &  filename)

Dump the SMT2 representation of the parsed expressions to a file.

Parameters
filenameFilename to save the SMT2
Returns
Filename

Definition at line 2981 of file base_parser.cpp.

References dumpSMT2().

◆ ensureNumberValue()

void stabilizer::parser::Parser::ensureNumberValue ( std::shared_ptr< DAGNode expr)

ensure the expression is a number

Parameters
exprExpression 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.

Referenced by toInt(), and toReal().

◆ err_all() [1/2]

void stabilizer::parser::Parser::err_all ( const ERROR_TYPE  e,
const std::string  s = "",
const size_t  ln = 0 
) const
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().

◆ err_all() [2/2]

void stabilizer::parser::Parser::err_all ( const std::shared_ptr< DAGNode e,
const std::string  s = "",
const size_t  ln = 0 
) const
private

Definition at line 2568 of file base_parser.cpp.

References err_all().

◆ err_arity_mis()

void stabilizer::parser::Parser::err_arity_mis ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2633 of file base_parser.cpp.

Referenced by err_all().

◆ err_keyword()

void stabilizer::parser::Parser::err_keyword ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2647 of file base_parser.cpp.

◆ err_logic()

void stabilizer::parser::Parser::err_logic ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2613 of file base_parser.cpp.

Referenced by err_all().

◆ err_mul_decl()

void stabilizer::parser::Parser::err_mul_decl ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2618 of file base_parser.cpp.

Referenced by err_all(), and parseCommand().

◆ err_mul_def()

void stabilizer::parser::Parser::err_mul_def ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2623 of file base_parser.cpp.

Referenced by err_all(), and parseCommand().

◆ err_neg_param()

void stabilizer::parser::Parser::err_neg_param ( const size_t  ln) const
private

Definition at line 2642 of file base_parser.cpp.

Referenced by err_all().

◆ err_open_file()

void stabilizer::parser::Parser::err_open_file ( const std::string  filename) const
private

Definition at line 2655 of file base_parser.cpp.

Referenced by parseSmtlib2File().

◆ err_param_mis()

void stabilizer::parser::Parser::err_param_mis ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2594 of file base_parser.cpp.

Referenced by err_all(), and parseOper().

◆ err_param_nbool()

void stabilizer::parser::Parser::err_param_nbool ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2599 of file base_parser.cpp.

Referenced by err_all().

◆ err_param_nnum()

void stabilizer::parser::Parser::err_param_nnum ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2603 of file base_parser.cpp.

Referenced by err_all().

◆ err_param_nsame()

void stabilizer::parser::Parser::err_param_nsame ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2608 of file base_parser.cpp.

Referenced by err_all().

◆ err_sym_mis() [1/2]

void stabilizer::parser::Parser::err_sym_mis ( const std::string  mis,
const size_t  ln 
) const
private

Definition at line 2578 of file base_parser.cpp.

Referenced by err_all(), parseLet(), parseLpar(), parsePreservingLet(), and parseRpar().

◆ err_sym_mis() [2/2]

void stabilizer::parser::Parser::err_sym_mis ( const std::string  mis,
const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2582 of file base_parser.cpp.

◆ err_type_mis()

void stabilizer::parser::Parser::err_type_mis ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 2638 of file base_parser.cpp.

Referenced by err_all(), mkAnd(), and mkOr().

◆ err_unexp_eof()

void stabilizer::parser::Parser::err_unexp_eof ( ) const
private

Definition at line 2573 of file base_parser.cpp.

Referenced by err_all(), err_unkwn_sym(), and getSymbol().

◆ err_unkwn_sym()

void stabilizer::parser::Parser::err_unkwn_sym ( const std::string  nm,
const size_t  ln 
) const
private

◆ err_zero_divisor()

void stabilizer::parser::Parser::err_zero_divisor ( const size_t  ln) const
private

Definition at line 2628 of file base_parser.cpp.

Referenced by err_all().

◆ expandLet()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::expandLet ( std::shared_ptr< DAGNode expr)

Expand a let expression.

Parameters
exprLet expression to expand
Returns
Expanded expression

◆ flattenDNF()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::flattenDNF ( std::shared_ptr< DAGNode expr)
private

◆ getAddOp()

NODE_KIND stabilizer::parser::Parser::getAddOp ( std::shared_ptr< Sort sort)

Get the add operator for a sort.

Parameters
sortSort
Returns
Add operator for the 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.

◆ getArity()

int stabilizer::parser::Parser::getArity ( NODE_KIND  k) const

Get the arity of a node kind.

Parameters
kNode kind
Returns
Arity of the 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().

◆ getAssertions()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getAssertions ( ) const

Get all assertions.

Returns
Vector of all assertions

Definition at line 201 of file base_parser.cpp.

References assertions.

◆ getAssumptions()

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.

Returns
Vector of all assumptions

Definition at line 209 of file base_parser.cpp.

References assumptions.

◆ getDatatypeBlocks()

std::vector< std::vector< DTTypeDecl > > & stabilizer::parser::Parser::getDatatypeBlocks ( )
inline

Definition at line 329 of file parser.h.

References datatype_blocks.

◆ getDeclaredVariables()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getDeclaredVariables ( ) const

Get declared variables.

Returns
Vector of all declared variables

Definition at line 254 of file base_parser.cpp.

References node_manager, and var_names.

◆ getEvaluatePrecision()

mpfr_prec_t stabilizer::parser::Parser::getEvaluatePrecision ( ) const

Get the precision for evaluation.

Returns
Precision

Definition at line 281 of file base_parser.cpp.

References options.

Referenced by toReal().

◆ getEvaluateUseFloating()

bool stabilizer::parser::Parser::getEvaluateUseFloating ( ) const

Get the use floating for evaluation.

Returns
Use floating

Definition at line 287 of file base_parser.cpp.

References options.

Referenced by rewrite(), rewrite(), and rewrite().

◆ getFunctionNames()

std::vector< std::string > & stabilizer::parser::Parser::getFunctionNames ( )
inline

Definition at line 325 of file parser.h.

References function_names.

◆ getFunctions()

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.

Returns
Vector of all functions

Definition at line 270 of file base_parser.cpp.

References fun_key_map, and function_names.

Referenced by dumpSMT2().

◆ getFunKeyMap()

std::unordered_map< std::string, std::shared_ptr< DAGNode > > & stabilizer::parser::Parser::getFunKeyMap ( )
inline

Definition at line 322 of file parser.h.

References fun_key_map.

◆ getGroupedAssertions()

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.

Returns
Map from group names to sets of assertion indices

Definition at line 205 of file base_parser.cpp.

References assertion_groups.

◆ getGroupedSoftAssertions()

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.

Returns
Map from group names to sets of soft assertion indices

Definition at line 219 of file base_parser.cpp.

References soft_assertion_groups.

◆ getKind() [1/2]

NODE_KIND stabilizer::parser::Parser::getKind ( const std::shared_ptr< DAGNode > &  node)

Get kind.

Parameters
nodeNode
Returns
NODE_KIND

◆ getKind() [2/2]

NODE_KIND stabilizer::parser::Parser::getKind ( const std::string &  s)

Get kind.

Parameters
sString token
Returns
NODE_KIND

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.

◆ getNegatedKind()

NODE_KIND stabilizer::parser::Parser::getNegatedKind ( NODE_KIND  kind)

Get the opposite kind of a node kind.

Parameters
kindNode kind
Returns
Opposite kind of the node kind

Definition at line 2481 of file base_parser.cpp.

References stabilizer::parser::getNegatedKind().

◆ getNodeCount()

size_t stabilizer::parser::Parser::getNodeCount ( )

Get node count.

Returns
Node count

Definition at line 157 of file base_parser.cpp.

References assertions, assumptions, soft_assertions, and soft_weights.

◆ getNodeManager()

std::unique_ptr< NodeManager > stabilizer::parser::Parser::getNodeManager ( )
inline

Definition at line 764 of file parser.h.

References node_manager.

◆ getOptions()

std::shared_ptr< GlobalOptions > stabilizer::parser::Parser::getOptions ( ) const

Get global options.

Returns
Pointer to global options

Definition at line 235 of file base_parser.cpp.

References options.

Referenced by stabilizer::api::SMTStabilizer::configure_parser().

◆ getResult()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::getResult ( )

Get result.

Returns
Result

Definition at line 120 of file base_parser.cpp.

References result_node.

◆ getResultType()

RESULT_TYPE stabilizer::parser::Parser::getResultType ( )

Get result type.

Returns
Result type

Definition at line 118 of file base_parser.cpp.

References result_type.

◆ getSoftAssertions()

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.

Returns
Vector of all soft assertions

Definition at line 212 of file base_parser.cpp.

References soft_assertions.

◆ getSoftWeights()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getSoftWeights ( ) const

Get soft assertion weights.

Returns
Vector of all soft assertion weights

Definition at line 215 of file base_parser.cpp.

References soft_weights.

◆ getSort() [1/4]

std::shared_ptr< Sort > stabilizer::parser::Parser::getSort ( const std::vector< std::shared_ptr< DAGNode > > &  params)

◆ getSort() [2/4]

std::shared_ptr< Sort > stabilizer::parser::Parser::getSort ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Get sort.

Parameters
lLeft operand
rRight operand
Returns
Sort

Definition at line 162 of file op_parser.cpp.

References getSort().

◆ getSort() [3/4]

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.

Parameters
lFirst operand
rSecond operand
mThird operand
Returns
Sort

Definition at line 166 of file op_parser.cpp.

References getSort().

◆ getSort() [4/4]

std::shared_ptr< Sort > stabilizer::parser::Parser::getSort ( std::shared_ptr< DAGNode param)

Get sort.

Parameters
paramParameter
Returns
Sort

Definition at line 159 of file op_parser.cpp.

◆ getSortNames()

std::unordered_map< std::string, std::shared_ptr< Sort > > & stabilizer::parser::Parser::getSortNames ( )
inline

Definition at line 326 of file parser.h.

References sort_key_map.

◆ getSplitLemmas()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getSplitLemmas ( )

Get the split lemmas.

Note
Return the split lemmas generated by splitOp last time.
Returns
Split lemmas

◆ getSymbol()

◆ getTempVarNames()

std::unordered_map< std::string, size_t > & stabilizer::parser::Parser::getTempVarNames ( )
inline

Definition at line 318 of file parser.h.

References temp_var_names.

◆ getVariable()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::getVariable ( const std::string &  var_name)

Get variable.

Parameters
var_nameVariable name
Returns
Variable node

Definition at line 261 of file base_parser.cpp.

References node_manager, stabilizer::parser::NodeManager::NULL_NODE, temp_var_names, and var_names.

◆ getVariables()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::getVariables ( ) const

Get variables.

Returns
Vector of all variables

Definition at line 236 of file base_parser.cpp.

References node_manager, temp_var_names, and var_names.

Referenced by dumpSMT2().

◆ getVarNames()

std::unordered_map< std::string, size_t > & stabilizer::parser::Parser::getVarNames ( )
inline

Definition at line 321 of file parser.h.

References var_names.

◆ getZero()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::getZero ( std::shared_ptr< Sort sort)

Get the zero for a sort.

Parameters
sortSort
Returns
Zero for the sort

Definition at line 2484 of file base_parser.cpp.

References stabilizer::parser::ERR_UNKWN_SYM, mkConstBv(), mkConstFp(), mkConstInt(), mkConstReal(), mkConstStr(), and mkErr().

◆ isCommutative()

◆ isDeclaredFunction()

bool stabilizer::parser::Parser::isDeclaredFunction ( const std::string &  func_name) const

Check if a function is declared.

Parameters
func_nameFunction name
Returns
True if the function is declared, false otherwise

Definition at line 2508 of file base_parser.cpp.

References fun_key_map.

◆ isDeclaredVariable()

bool stabilizer::parser::Parser::isDeclaredVariable ( const std::string &  var_name) const

Check if a variable is declared.

Parameters
var_nameVariable name
Returns
True if the variable is declared, false otherwise

Definition at line 2505 of file base_parser.cpp.

References var_names.

◆ isOne()

bool stabilizer::parser::Parser::isOne ( std::shared_ptr< DAGNode expr)

Check if an expression is one.

Parameters
exprExpression to check
Returns
true if the expression is one, false otherwise

Definition at line 317 of file base_parser.cpp.

References toInt(), toReal(), and stabilizer::parser::HighPrecisionInteger::toString().

Referenced by mkMul(), rewrite(), and rewrite().

◆ isOnes()

bool stabilizer::parser::Parser::isOnes ( std::shared_ptr< DAGNode expr)

Definition at line 328 of file base_parser.cpp.

Referenced by rewrite(), and rewrite().

◆ isZero()

bool stabilizer::parser::Parser::isZero ( std::shared_ptr< DAGNode expr)

Check if an expression is zero.

Parameters
exprExpression to check
Returns
true if the expression is zero, false otherwise

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().

◆ mkAbs()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAbs ( std::shared_ptr< DAGNode param)

Create an abs node.

Parameters
paramParameter
Returns
Abs node (|param|)

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().

◆ mkAcos()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcos ( std::shared_ptr< DAGNode param)

Create an acos node.

Note
assert(param >= -1 && param <= 1)
Parameters
paramParameter
Returns
Acos node (acos(param))

Definition at line 1572 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACOS, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAcosh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcosh ( std::shared_ptr< DAGNode param)

Create an acosh node.

Note
assert(param >= 1)
Parameters
paramParameter
Returns
Acosh node (acosh(param))

Definition at line 1644 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACOSH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAcot()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcot ( std::shared_ptr< DAGNode param)

Create an acot node.

Parameters
paramParameter
Returns
Acot node (acot(param))

Definition at line 1596 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACOT, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAcoth()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcoth ( std::shared_ptr< DAGNode param)

Create an acoth node.

Note
assert(param < -1 || param > 1)
Parameters
paramParameter
Returns
Acoth node (acoth(param))

Definition at line 1668 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACOTH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAcsc()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcsc ( std::shared_ptr< DAGNode param)

Create an acsc node.

Note
assert(param <= -1 || param >= 1)
Parameters
paramParameter
Returns
Acsc node (acsc(param))

Definition at line 1584 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACSC, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAcsch()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAcsch ( std::shared_ptr< DAGNode param)

Create an acsch node.

Note
assert(param != 0)
Parameters
paramParameter
Returns
Acsch node (acsch(param))

Definition at line 1662 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ACSCH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAdd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAdd ( const std::vector< std::shared_ptr< DAGNode > > &  params)

◆ mkAnd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAnd ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an and node.

Parameters
paramsParameters
Returns
And node (l and m and r and ...)

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().

◆ mkApplyDTFun()

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().

◆ mkApplyFunc()

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.

Parameters
funFunction node
paramsList of parameters
Returns
Function application node (fun(p1, p2, ..., pn))

Definition at line 2244 of file base_parser.cpp.

References stabilizer::parser::NT_FUNC_APPLY, and static_functions.

Referenced by applyFun().

◆ mkApplyRecFunc()

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.

Parameters
funRecursive function symbol node
paramsArgument list
Returns
Recursive function application node

Definition at line 2254 of file base_parser.cpp.

References stabilizer::parser::NT_FUNC_REC_APPLY, and static_functions.

Referenced by applyFun(), and applyFunPostOrder().

◆ mkApplyUF()

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.

Parameters
sortSort
nameFunction name
paramsParameters
Returns
Uninterpreted function application node

Definition at line 2287 of file base_parser.cpp.

References node_manager, and stabilizer::parser::NT_UF_APPLY.

Referenced by applyFun(), applyFunPostOrder(), and parseOper().

◆ mkArray()

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.

Parameters
nameArray name
indexIndex sort
elemElement sort
Returns
Array node

Definition at line 877 of file op_parser.cpp.

References mkVar(), sort_key_map, and sort_manager.

◆ mkArraySort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkArraySort ( std::shared_ptr< Sort index,
std::shared_ptr< Sort elem 
)

Create an array sort.

Parameters
indexIndex sort
elemElement sort
Returns
Array sort

Definition at line 506 of file op_parser.cpp.

References sort_manager.

◆ mkAsec()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAsec ( std::shared_ptr< DAGNode param)

Create an asec node.

Note
assert(param <= -1 || param >= 1)
Parameters
paramParameter
Returns
Asec node (asec(param))

Definition at line 1578 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ASEC, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAsech()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAsech ( std::shared_ptr< DAGNode param)

Create an asech node.

Note
assert(param > 0 && param <= 1)
Parameters
paramParameter
Returns
Asech node (asech(param))

Definition at line 1656 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ASECH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAsin()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAsin ( std::shared_ptr< DAGNode param)

Create an asin node.

Note
assert(param >= -1 && param <= 1)
Parameters
paramParameter
Returns
Asin node (asin(param))

Definition at line 1566 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ASIN, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAsinh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAsinh ( std::shared_ptr< DAGNode param)

Create an asinh node.

Parameters
paramParameter
Returns
Asinh node (asinh(param))

Definition at line 1638 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ASINH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAtan()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAtan ( std::shared_ptr< DAGNode param)

Create an atan node.

Parameters
paramParameter
Returns
Atan node (atan(param))

Definition at line 1590 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ATAN, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAtan2()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAtan2 ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create an atan2 node.

Note
Represents the angle in radians between the positive x-axis and the ray to point (r, l)
atan2(l, r) = atan(l/r) with appropriate quadrant adjustment
Parameters
lLeft parameter (y-coordinate)
rRight parameter (x-coordinate)
Returns
Atan2 node (atan2(l, r))

Definition at line 1674 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ATAN2, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAtanh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkAtanh ( std::shared_ptr< DAGNode param)

Create an atanh node.

Note
assert(param > -1 && param < 1)
Parameters
paramParameter
Returns
Atanh node (atanh(param))

Definition at line 1650 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_ATANH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkAttribute()

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().

◆ mkBoolSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkBoolSort ( )

Create a boolean sort.

Returns
Boolean sort

Definition at line 493 of file op_parser.cpp.

References stabilizer::parser::SortManager::BOOL_SORT.

◆ mkBvAdd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvAdd ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector addition node.

Parameters
paramsParameters
Returns
Bitvector addition node (l + r + ...)

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().

◆ mkBvAnd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvAnd ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector and node.

Parameters
paramsParameters
Returns
Bitvector and node (l & r & ...)

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().

◆ mkBvAshr()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector arithmetic shift right node (l >> r)

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().

◆ mkBvComp()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvComp ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector comparison node.

Parameters
paramsOperand list; the first two operands are compared.
Returns
Bitvector comparison node (l = r ? #b1 : #b0)

Definition at line 2046 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_BV_COMP, and sort_manager.

Referenced by parseOper().

◆ mkBvConcat()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvConcat ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector concatenation node.

Parameters
paramsParameters
Returns
Bitvector concatenation node (l ++ r ++ ...)

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().

◆ mkBvExtract()

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.

Note
assert(r >= s && r < bitwidth(l))
Parameters
lSource bitvector
rUpper index (inclusive)
sLower index (inclusive)
Returns
Bitvector extract node (l[r:s])

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().

◆ mkBvLshr()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector logical shift right node (l >> r)

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().

◆ mkBvMul()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvMul ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector multiplication node.

Parameters
paramsParameters
Returns
Bitvector multiplication node (l * r * ...)

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().

◆ mkBvNand()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNand ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector nand node.

Parameters
lLeft operand
rRight operand
Returns
Bitvector nand node (~(l & r & ...))

Definition at line 2025 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_BV_NAND.

Referenced by parseOper().

◆ mkBvNeg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNeg ( std::shared_ptr< DAGNode param)

Create a bitvector negation node.

Parameters
paramParameter
Returns
Bitvector negation node (-param)

Definition at line 2066 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_BV_NEG.

Referenced by parseOper(), and rewrite().

◆ mkBvNor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNor ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector nor node.

Parameters
lLeft operand
rRight operand
Returns
Bitvector nor node (~(l | r | ...))

Definition at line 2035 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_BV_NOR.

Referenced by parseOper().

◆ mkBvNot()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvNot ( std::shared_ptr< DAGNode param)

Create a bitvector not node.

Parameters
paramParameter
Returns
Bitvector not node (~param)

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().

◆ mkBvOr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvOr ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector or node.

Parameters
paramsParameters
Returns
Bitvector or node (l | r | ...)

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().

◆ mkBvRepeat()

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.

Note
assert(r > 0)
Parameters
lSource bitvector
rRepeat count
Returns
Bitvector repeat node (l repeated r times)

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().

◆ mkBvRotateLeft()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvRotateLeft ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector rotate left node.

Parameters
lSource bitvector
rRotation amount
Returns
Bitvector rotate left node (l <<< r)

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().

◆ mkBvRotateRight()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvRotateRight ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector rotate right node.

Parameters
lSource bitvector
rRotation amount
Returns
Bitvector rotate right node (l >>> r)

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().

◆ mkBvSdiv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSdiv ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector signed division node.

Note
if r == 0, then return all ones bit-vector if l is positive, otherwise 1
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed division node (l / r)

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().

◆ mkBvSge()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed greater than or equal node (l >= r)

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().

◆ mkBvSgt()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed greater than node (l > r)

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().

◆ mkBvShl()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvShl ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector shift left node.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector shift left node (l << r)

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().

◆ mkBvSignExt()

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.

Parameters
lSource bitvector
rNumber of bits to extend
Returns
Bitvector sign extension node (l sign_extend r)

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().

◆ mkBvSle()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed less than or equal node (l <= r)

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().

◆ mkBvSlt()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed less than node (l < r)

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().

◆ mkBvSmod()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSmod ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector signed modulo node.

Note
if r == 0, then return l
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed modulo node (l % r)

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().

◆ mkBVSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkBVSort ( const size_t &  width)

Create a bit-vector sort.

Parameters
widthWidth of the bit-vector
Returns
Bit-vector sort

Definition at line 500 of file op_parser.cpp.

References sort_manager.

◆ mkBvSrem()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSrem ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector signed remainder node.

Note
if r == 0, then return l
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector signed remainder node (l % r)

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().

◆ mkBvSub()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvSub ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector subtraction node.

Parameters
lLeft operand
rRight operand
Returns
Bitvector subtraction node (l - r - ...)

Definition at line 2099 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_BV_SUB.

Referenced by parseOper().

◆ mkBvToInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvToInt ( std::shared_ptr< DAGNode param)

Create a bitvector to integer conversion node.

Parameters
paramParameter
Returns
Bitvector to integer conversion node (to_int(param))

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().

◆ mkBvToNat()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvToNat ( std::shared_ptr< DAGNode param)

Create a bitvector to natural number conversion node.

Parameters
paramParameter
Returns
Bitvector to natural number conversion node (to_nat(param))

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().

◆ mkBvUdiv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUdiv ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector unsigned division node.

Note
if r == 0, then return all ones bit-vector
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned division node (l / r)

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().

◆ mkBvUge()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned greater than or equal node (l >= r)

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().

◆ mkBvUgt()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned greater than node (l > r)

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().

◆ mkBvUle()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned less than or equal node (l <= r)

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().

◆ mkBvUlt()

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.

Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned less than node (l < r)

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().

◆ mkBvUmod()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUmod ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector unsigned modulo node.

Note
if r == 0, then return l
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned modulo node (l % r)

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.

◆ mkBvUrem()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvUrem ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector unsigned remainder node.

Note
if r == 0, then return l
Parameters
lLeft parameter
rRight parameter
Returns
Bitvector unsigned remainder node (l % r)

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().

◆ mkBvXnor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvXnor ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a bitvector xnor node.

Parameters
lLeft operand
rRight operand
Returns
Bitvector xnor node (~(l ^ r ^ ...))

Definition at line 2052 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_BV_XNOR.

Referenced by parseOper().

◆ mkBvXor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkBvXor ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a bitvector xor node.

Parameters
paramsParameters
Returns
Bitvector xor node (l ^ r ^ ...)

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().

◆ mkBvZeroExt()

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.

Parameters
lSource bitvector
rNumber of bits to extend
Returns
Bitvector zero extension node (l zero_extend r)

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().

◆ mkCeil()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCeil ( std::shared_ptr< DAGNode param)

Create an ceil node.

Parameters
paramParameter
Returns
Ceil node (ceil(param))

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().

◆ mkConstArray()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstArray ( std::shared_ptr< Sort sort,
std::shared_ptr< DAGNode value 
)

Create a constant array node.

Parameters
sortArray sort
valueConstant value for all elements
Returns
Constant array node

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().

◆ mkConstBv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstBv ( const std::string &  v,
const size_t &  width 
)

Create a bit-vector constant.

Parameters
vValue (string)
widthWidth of the bit-vector
Returns
Bit-vector constant node

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().

◆ mkConstFP()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstFP ( const std::string &  fp_expr)

Create a floating-point constant from expression.

Parameters
fp_exprFloating-point expression string
Returns
Floating-point constant node

Definition at line 758 of file op_parser.cpp.

References node_manager, and stabilizer::parser::NT_CONST.

Referenced by parseConstFunc().

◆ mkConstFp()

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.

Parameters
vValue (string)
eExponent size
sSignificand size
Returns
Floating-point constant node

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().

◆ mkConstInt() [1/4]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt ( const int &  v)

Create an integer constant.

Parameters
vValue (int)
Returns
Integer constant node

Definition at line 683 of file op_parser.cpp.

References mkConstInt().

◆ mkConstInt() [2/4]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt ( const Integer v)

Create an integer constant.

Parameters
vValue (Integer)
Returns
Integer constant node

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().

◆ mkConstInt() [3/4]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt ( const Number v)

Create a real constant from number.

Parameters
vValue (Number)
Returns
Real constant node

Definition at line 686 of file op_parser.cpp.

References mkConstInt(), and stabilizer::parser::Number::toInteger().

◆ mkConstInt() [4/4]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstInt ( const std::string &  v)

Create an integer constant from string.

Parameters
vValue (string)
Returns
Integer constant node

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().

◆ mkConstReal() [1/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal ( const double &  v)

Create a real constant from double.

Parameters
vValue (double)
Returns
Real constant node

Definition at line 702 of file op_parser.cpp.

References node_manager, stabilizer::parser::NT_CONST, and stabilizer::parser::SortManager::REAL_SORT.

◆ mkConstReal() [2/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal ( const Integer v)

Create a real constant from integer.

Parameters
vValue (Integer)
Returns
Real constant node

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().

◆ mkConstReal() [3/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal ( const Number v)

Create a real constant from number.

Parameters
vValue (Number)
Returns
Real constant node

Definition at line 710 of file op_parser.cpp.

References mkConstReal(), and stabilizer::parser::Number::toReal().

◆ mkConstReal() [4/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal ( const Real v)

Create a real constant.

Parameters
vValue (Real)
Returns
Real constant node

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().

◆ mkConstReal() [5/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReal ( const std::string &  v)

◆ mkConstReg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstReg ( const std::string &  v)

Create a regular expression constant.

Parameters
vValue (string)
Returns
Regular expression constant node

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().

◆ mkConstStr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkConstStr ( const std::string &  v)

Create a string constant.

Parameters
vValue (string)
Returns
String constant node

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().

◆ mkCos()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCos ( std::shared_ptr< DAGNode param)

Create an cos node.

Parameters
paramParameter
Returns
Cos node (cos(param))

Definition at line 1536 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_COS, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkCosh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCosh ( std::shared_ptr< DAGNode param)

Create a cosh node.

Parameters
paramParameter
Returns
Cosh node (cosh(param))

Definition at line 1608 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_COSH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkCot()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCot ( std::shared_ptr< DAGNode param)

Create a cot node.

Note
assert(param != k*pi)
Parameters
paramParameter
Returns
Cot node (cot(param))

Definition at line 1560 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_COT, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkCoth()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCoth ( std::shared_ptr< DAGNode param)

Create a coth node.

Note
assert(param < -1 || param > 1)
Parameters
paramParameter
Returns
Coth node (coth(param))

Definition at line 1632 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_COTH, and stabilizer::parser::SortManager::REAL_SORT.

◆ mkCsc()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCsc ( std::shared_ptr< DAGNode param)

Create an csc node.

Parameters
paramParameter
Returns
Csc node (csc(param))

Definition at line 1548 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_CSC, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkCsch()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkCsch ( std::shared_ptr< DAGNode param)

Create a csch node.

Note
assert(param != 0)
Parameters
paramParameter
Returns
Csch node (csch(param))

Definition at line 1626 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_CSCH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkDistinct()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDistinct ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a distinct node.

Parameters
paramsParameters
Returns
Distinct node

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().

◆ mkDiv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDiv ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an div node.

Note
This is the real division operator.
Parameters
lLeft parameter
rRight parameter
Returns
Div node (l / r / ...)

Definition at line 1404 of file op_parser.cpp.

References mkDivReal().

◆ mkDivInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDivInt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an div node.

Parameters
paramsParameters
Returns
Div node (l / r / ...)

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().

◆ mkDivReal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkDivReal ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an div node.

Parameters
paramsParameters
Returns
Div node (l / r / ...)

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().

◆ mkE()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkE ( )

Create a e node.

Returns
E node (e, i.e., the base of the natural logarithm)

Definition at line 1788 of file op_parser.cpp.

References stabilizer::parser::NodeManager::E_NODE.

Referenced by parseConstFunc().

◆ mkEpsilon()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkEpsilon ( )

Create a epsilon node.

Returns
Epsilon node (epsilon, i.e., a infinitesimal number)

Definition at line 1872 of file op_parser.cpp.

References stabilizer::parser::NodeManager::EPSILON_NODE.

Referenced by parseConstFunc().

◆ mkEq()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkEq ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an equality node.

Parameters
paramsParameters
Returns
Equality node

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().

◆ mkErr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkErr ( const ERROR_TYPE  t)
private

◆ mkExists()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkExists ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an exists node.

Parameters
paramsList of (variable, sort) pairs
Returns
Exists node (exists((var1, sort1), (var2, sort2), ..., body))

Definition at line 2362 of file base_parser.cpp.

References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_EXISTS.

Referenced by parseQuant().

◆ mkExp()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkExp ( std::shared_ptr< DAGNode param)

Create an exp node.

Parameters
paramParameter
Returns
Exp node (exp(param))

Definition at line 1489 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_EXP, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkExpr()

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.

Parameters
expressionString expression to parse
Returns
Parsed DAG node

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().

◆ mkFact()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFact ( std::shared_ptr< DAGNode param)

Create a factorial node.

Note
assert(param >= 0)
Parameters
paramParameter
Returns
Factorial node (factorial(param))

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().

◆ mkFalse()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFalse ( )

◆ mkFloor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFloor ( std::shared_ptr< DAGNode param)

Create an floor node.

Parameters
paramParameter
Returns
Floor node (floor(param))

Definition at line 1476 of file op_parser.cpp.

References stabilizer::parser::SortManager::INT_SORT, mkOper(), and stabilizer::parser::NT_FLOOR.

Referenced by parseOper().

◆ mkForall()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkForall ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a forall node.

Parameters
paramsList of (variable, sort) pairs
Returns
Forall node (forall((var1, sort1), (var2, sort2), ..., body))

Definition at line 2358 of file base_parser.cpp.

References stabilizer::parser::SortManager::BOOL_SORT, mkOper(), and stabilizer::parser::NT_FORALL.

Referenced by parseQuant().

◆ mkFpAbs()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpAbs ( std::shared_ptr< DAGNode param)

Create a floating-point absolute value node.

Parameters
paramParameter
Returns
Floating-point absolute value node (fp.abs(param))

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().

◆ mkFpAdd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpAdd ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point addition node.

Parameters
paramsParameters
Returns
Floating-point addition node (fp.add(l, r, ...))

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().

◆ mkFpConst()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpConst ( std::shared_ptr< DAGNode sign,
std::shared_ptr< DAGNode exp,
std::shared_ptr< DAGNode mant 
)

◆ mkFpDiv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpDiv ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point division node.

Note
Division by zero results in appropriate IEEE-754 behavior
Parameters
paramsParameters
Returns
Floating-point division node (fp.div(l, r, ...))

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().

◆ mkFpEq()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpEq ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point equality node.

Note
This is IEEE-754 equality (NaN != NaN)
Parameters
paramsParameters
Returns
Floating-point equality node (fp.eq(params))

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().

◆ mkFpFma()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpFma ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point fused multiply-add node.

Note
The operation (a * b + c) performed with only one rounding
Parameters
paramsParameters (should have exactly 3 elements)
Returns
Floating-point fused multiply-add node (fp.fma(a, b, c) = a * b + c)

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().

◆ mkFpGe()

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.

Parameters
paramsParameters
Returns
Floating-point greater than or equal node (fp.geq(params)

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().

◆ mkFpGt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpGt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point greater than node.

Parameters
paramsParameters
Returns
Floating-point greater than node (fp.gt(params))

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().

◆ mkFpIsInf()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsInf ( std::shared_ptr< DAGNode param)

Create a floating-point is-infinity check node.

Parameters
paramParameter to check
Returns
Is-infinity check node (fp.isInf(param))

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().

◆ mkFpIsNaN()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNaN ( std::shared_ptr< DAGNode param)

Create a floating-point is-NaN check node.

Parameters
paramParameter to check
Returns
Is-NaN check node (fp.isNaN(param))

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().

◆ mkFpIsNeg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNeg ( std::shared_ptr< DAGNode param)

Create a floating-point is-negative check node.

Parameters
paramParameter to check
Returns
Is-negative check node (fp.isNegative(param))

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().

◆ mkFpIsNormal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsNormal ( std::shared_ptr< DAGNode param)

Create a floating-point is-normal check node.

Parameters
paramParameter to check
Returns
Is-normal check node (fp.isNormal(param))

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().

◆ mkFpIsPos()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsPos ( std::shared_ptr< DAGNode param)

Create a floating-point is-positive check node.

Parameters
paramParameter to check
Returns
Is-positive check node (fp.isPositive(param))

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().

◆ mkFpIsSubnormal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsSubnormal ( std::shared_ptr< DAGNode param)

Create a floating-point is-subnormal check node.

Parameters
paramParameter to check
Returns
Is-subnormal check node (fp.isSubnormal(param))

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().

◆ mkFpIsZero()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpIsZero ( std::shared_ptr< DAGNode param)

Create a floating-point is-zero check node.

Parameters
paramParameter to check
Returns
Is-zero check node (fp.isZero(param))

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().

◆ mkFpLe()

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.

Parameters
paramsParameters
Returns
Floating-point less than or equal node (fp.leq(params))

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().

◆ mkFpLt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpLt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point less than node.

Parameters
paramsParameters
Returns
Floating-point less than node (fp.lt(params))

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().

◆ mkFpMax()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMax ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a floating-point maximum node.

Parameters
lLeft operand
rRight operand
Returns
Floating-point maximum node (fp.max(params))

Definition at line 2904 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_FP_MAX.

Referenced by parseOper().

◆ mkFpMin()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMin ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a floating-point minimum node.

Parameters
lLeft operand
rRight operand
Returns
Floating-point minimum node (fp.min(params))

Definition at line 2891 of file op_parser.cpp.

References getSort(), mkOper(), and stabilizer::parser::NT_FP_MIN.

Referenced by parseOper().

◆ mkFpMul()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpMul ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point multiplication node.

Parameters
paramsParameters
Returns
Floating-point multiplication node (fp.mul(l, r, ...))

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().

◆ mkFpNeg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpNeg ( std::shared_ptr< DAGNode param)

Create a floating-point negation node.

Parameters
paramParameter
Returns
Floating-point negation node (fp.neg(param))

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().

◆ mkFpRem()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpRem ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a floating-point remainder node.

Note
IEEE-754 remainder operation
Parameters
lLeft parameter
rRight parameter
Returns
Floating-point remainder node (fp.rem(l, r))

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().

◆ mkFpRoundToIntegral() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpRoundToIntegral ( std::shared_ptr< DAGNode param)

◆ mkFpRoundToIntegral() [2/2]

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.

Parameters
rmRounding mode
paramOperand
Returns
Floating-point round to integral node (fp.roundToIntegral(param))

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().

◆ mkFPSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkFPSort ( const size_t &  e,
const size_t &  s 
)

Create a floating-point sort.

Parameters
eExponent size
sSignificand size
Returns
Floating-point sort

Definition at line 503 of file op_parser.cpp.

References sort_manager.

◆ mkFpSqrt() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpSqrt ( std::shared_ptr< DAGNode param)

◆ mkFpSqrt() [2/2]

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.

Note
Returns NaN for negative values
Parameters
rmRounding mode
paramOperand
Returns
Floating-point square root node (fp.sqrt(param))

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().

◆ mkFpSub()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpSub ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a floating-point subtraction node.

Parameters
paramsParameters
Returns
Floating-point subtraction node (fp.sub(l, r, ...))

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().

◆ mkFpToReal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFpToReal ( std::shared_ptr< DAGNode param)

Create a floating-point to real conversion node.

Note
NaN and infinity cannot be converted to real
Parameters
paramFloating-point value
Returns
Floating-point to real conversion node (fp.to_real(param))

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().

◆ mkFpToSbv()

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.

Note
Rounds toward zero, returns max/min representable value if out of range
Parameters
paramFloating-point value
sizeSize of resulting bitvector
Returns
Floating-point to signed bitvector conversion node (fp.to_sbv(param, size))

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().

◆ mkFpToUbv()

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.

Note
Rounds toward zero, returns max representable value if out of range
Parameters
paramFloating-point value
sizeSize of resulting bitvector
Returns
Floating-point to unsigned bitvector conversion node (fp.to_ubv(param, size))

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().

◆ mkFuncDec()

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.

Parameters
nameFunction name
paramsParameters
out_sortOutput sort
Returns
Function declaration node

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().

◆ mkFuncDef()

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.

Parameters
nameFunction name
paramsParameters
out_sortOutput sort
bodyBody
Returns
Function definition node

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().

◆ mkFuncRec()

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.

Parameters
nameFunction name
paramsParameters
out_sortOutput sort
bodyBody
Returns
Recursive function definition node

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().

◆ mkFunParamVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkFunParamVar ( std::shared_ptr< Sort sort,
const std::string &  name 
)

Create a function parameter variable.

Parameters
sortSort
nameVariable name
Returns
Function parameter variable node

Definition at line 868 of file op_parser.cpp.

References node_manager, and stabilizer::parser::NT_FUNC_PARAM.

Referenced by parseCommand().

◆ mkGcd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGcd ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a gcd node.

Note
assert(l != 0 || r != 0)
Parameters
lLeft parameter
rRight parameter
Returns
Gcd node (gcd(l, r))

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().

◆ mkGe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGe ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a ge node.

Parameters
paramsParameters
Returns
Ge node (l >= r >= ... >= s)

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().

◆ mkGt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkGt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a gt node.

Parameters
paramsParameters
Returns
Gt node (l > r > ... > s)

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().

◆ mkIand()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIand ( const std::vector< std::shared_ptr< DAGNode > > &  params)

◆ mkImplies()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkImplies ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an implies node.

Parameters
paramsParameters
Returns
Implies node (l -> r -> ...)

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().

◆ mkIndexofReg()

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.

Parameters
lString
rRegex pattern
Returns
String index-of-regex node (str.indexof(l, r))

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.

◆ mkInfinity()

◆ mkInternalOper()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkInternalOper ( const std::shared_ptr< Sort > &  sort,
const NODE_KIND t,
const std::vector< std::shared_ptr< DAGNode > > &  p 
)
private

◆ mkIntSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkIntSort ( )

Create an integer sort.

Returns
Integer sort

Definition at line 491 of file op_parser.cpp.

References stabilizer::parser::SortManager::INT_SORT.

◆ mkIntToBv()

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.

Note
assert(width > 0 && param >= -2^(width-1) && param < 2^(width-1))
Parameters
paramParameter (integer number)
widthWidth of the resulting bitvector
Returns
Integer to bitvector conversion node (to_bv(param, width))

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().

◆ mkIsDivisible()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsDivisible ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a is_divisible node.

Parameters
lLeft parameter
rRight parameter
Returns
Is_divisible node (is_divisible(l, r), l divides r)

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().

◆ mkIsEven()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsEven ( std::shared_ptr< DAGNode param)

Create a is_even node.

Parameters
paramParameter
Returns
Is_even node (is_even(param))

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().

◆ mkIsInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsInt ( std::shared_ptr< DAGNode param)

Create a is_int node.

Parameters
paramParameter
Returns
Is_int node (is_int(param))

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().

◆ mkIsOdd()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsOdd ( std::shared_ptr< DAGNode param)

Create a is_odd node.

Parameters
paramParameter
Returns
Is_odd node (is_odd(param))

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().

◆ mkIsPrime()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIsPrime ( std::shared_ptr< DAGNode param)

Create a is_prime node.

Parameters
paramParameter
Returns
Is_prime node (is_prime(param))

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().

◆ mkIte() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkIte ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an ite node.

Note
It only accepts 3 parameters.
Parameters
paramsParameters
Returns
Ite node (cond ? l : r)

Definition at line 1108 of file op_parser.cpp.

References err_all(), stabilizer::parser::ERR_PARAM_MIS, line_number, mkIte(), and mkUnknown().

◆ mkIte() [2/2]

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.

Parameters
condCondition
lLeft parameter
rRight parameter
Returns
Ite node (cond ? l : r)

Definition at line 1096 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_ITE.

Referenced by mkIte(), parseExpr(), and parseOper().

◆ mkLb()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLb ( std::shared_ptr< DAGNode param)

Create an lb/log2 node.

Note
assert(param > 0)
Parameters
paramParameter
Returns
Lb node (lb(param))

Definition at line 1501 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_LB, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkLcm()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLcm ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a lcm node.

Note
assert(l != 0 && r != 0)
Parameters
lLeft parameter
rRight parameter
Returns
Lcm node (lcm(l, r))

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().

◆ mkLe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLe ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a le node.

Parameters
paramsParameters
Returns
Le node (l <= r <= ... <= s)

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().

◆ mkLet()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLet ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a let node.

Parameters
paramsList of (key, value) pairs
Returns
Let node (let((key1, val1), (key2, val2), ...))

◆ mkLetBindVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLetBindVar ( const std::string &  name,
const std::shared_ptr< DAGNode > &  expr 
)
private

◆ mkLetBindVarList()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLetBindVarList ( const std::vector< std::shared_ptr< DAGNode > > &  bind_vars)
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().

◆ mkLetChain()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLetChain ( const std::vector< std::shared_ptr< DAGNode > > &  bind_var_lists,
const std::shared_ptr< DAGNode > &  body 
)
private

◆ mkLg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLg ( std::shared_ptr< DAGNode param)

Create an lg/log10 node.

Note
assert(param > 0)
Parameters
paramParameter
Returns
Lg node (lg(param))

Definition at line 1507 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_LG, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkLn()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLn ( std::shared_ptr< DAGNode param)

Create an ln node.

Note
assert(param > 0)
Parameters
paramParameter
Returns
Ln node (ln(param))

Definition at line 1495 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_LN, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkLog()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLog ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create an log node.

Note
r is the base, l is the argument
assert(r > 0 && r != 1 && l > 0)
Parameters
lLeft parameter
rRight parameter
Returns
Log node (log_r(l))

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().

◆ mkLt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkLt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a lt node.

Parameters
paramsParameters
Returns
Lt node (l < r < ... < s)

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().

◆ mkMax()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMax ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a max node.

Parameters
paramsList of parameters
Returns
Max node (max(p1, p2, ...))

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.

◆ mkMin()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMin ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a min node.

Parameters
paramsList of parameters
Returns
Min node (min(p1, p2, ...))

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.

◆ mkMod()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMod ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create an mod node.

Parameters
lLeft parameter
rRight parameter
Returns
Mod node (l % r)

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().

◆ mkMul()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkMul ( const std::vector< std::shared_ptr< DAGNode > > &  params)

◆ mkNaN()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNaN ( std::shared_ptr< Sort sort = nullptr)

Create a NaN node.

Parameters
sortOptional sort (for FP types, will include eb sb in name)
Returns
NaN node (nan, i.e., Not a Number)

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().

◆ mkNatSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkNatSort ( )

Create a natural sort.

Returns
Natural sort

Definition at line 499 of file op_parser.cpp.

References stabilizer::parser::SortManager::NAT_SORT.

◆ mkNatToBv()

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.

Note
assert(param >= 0 && width > 0 && param < 2^width)
Parameters
paramParameter (natural number)
widthWidth of the resulting bitvector
Returns
Natural number to bitvector conversion node (to_bv(param, width))

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().

◆ mkNeg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNeg ( std::shared_ptr< DAGNode param)

Create an neg node.

Parameters
paramParameter
Returns
Neg node (-param)

Definition at line 1387 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_NEG.

Referenced by mkSub(), and parseOper().

◆ mkNegEpsilon()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNegEpsilon ( )

Create a negative epsilon node.

Returns
Negative epsilon node (-epsilon)

Definition at line 1878 of file op_parser.cpp.

References stabilizer::parser::NodeManager::NEG_EPSILON_NODE.

Referenced by parseConstFunc().

◆ mkNegInfinity()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNegInfinity ( std::shared_ptr< Sort sort = nullptr)

◆ mkNode()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNode ( std::shared_ptr< Sort sort,
NODE_KIND  t,
std::string  name,
std::vector< std::shared_ptr< DAGNode > >  params 
)
inline

◆ mkNoPattern()

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().

◆ mkNot()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkNot ( std::shared_ptr< DAGNode param)

Create a not node.

Parameters
paramParameter
Returns
Not node (not param)

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().

◆ mkOper() [1/4]

◆ mkOper() [2/4]

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.

Parameters
sortSort
tOperation kind
lLeft parameter
mMiddle parameter
rRight parameter
Returns
Operation Node

Definition at line 221 of file op_parser.cpp.

References mkOper().

◆ mkOper() [3/4]

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.

Parameters
sortSort
tOperation kind
lLeft parameter
rRight parameter
Returns
Operation Node

Definition at line 212 of file op_parser.cpp.

References mkOper().

◆ mkOper() [4/4]

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.

Parameters
sortSort
tOperation kind
pParameters
Returns
Operation Node

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().

◆ mkOr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkOr ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an or node.

Parameters
paramsParameters
Returns
Or node (l or m or r or ...)

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().

◆ mkPattern()

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().

◆ mkPi()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPi ( )

Create a pi node.

Returns
Pi node (pi, i.e., the ratio of the circumference of a circle to its diameter)

Definition at line 1787 of file op_parser.cpp.

References stabilizer::parser::NodeManager::PI_NODE.

Referenced by parseConstFunc().

◆ mkPlaceholderVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPlaceholderVar ( const std::string &  name)

◆ mkPosEpsilon()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPosEpsilon ( )

Create a positive epsilon node.

Returns
Positive epsilon node (+epsilon)

Definition at line 1875 of file op_parser.cpp.

References stabilizer::parser::NodeManager::POS_EPSILON_NODE.

Referenced by parseConstFunc().

◆ mkPosInfinity()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPosInfinity ( std::shared_ptr< Sort sort = nullptr)

◆ mkPow()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPow ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create an pow node.

Parameters
lLeft parameter
rRight parameter
Returns
Pow node (l^r)

Definition at line 1321 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_POW.

Referenced by parseOper().

◆ mkPow2()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkPow2 ( std::shared_ptr< DAGNode param)

Create an pow2 node.

Parameters
paramParameter
Returns
Pow2 node (2^param)

Definition at line 1318 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_POW2.

Referenced by parseOper().

◆ mkQuantVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkQuantVar ( const std::string &  name,
std::shared_ptr< Sort sort 
)

Create a quantifier variable node.

Parameters
nameVariable name
sortVariable sort
Returns
Quantifier variable node (var1, sort1)

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().

◆ mkRealSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkRealSort ( )

Create a real sort.

Returns
Real sort

Definition at line 492 of file op_parser.cpp.

References stabilizer::parser::SortManager::REAL_SORT.

◆ mkRegAll()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegAll ( )

Create a regex all node.

Creates a regex node that matches any string.

Returns
Regex all node (re.all)

Definition at line 3746 of file op_parser.cpp.

References mkConstReg().

Referenced by parseConstFunc().

◆ mkRegAllChar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegAllChar ( )

Create a regex allchar node.

Creates a regex node that matches any single character.

Returns
Regex allchar node (re.allchar)

Definition at line 3747 of file op_parser.cpp.

References mkConstReg().

Referenced by parseConstFunc().

◆ mkRegComplement()

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.

Parameters
paramRegex pattern
Returns
Regex complement node (re.complement(param), i.e., ~param)

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().

◆ mkRegConcat()

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.

Parameters
paramsRegex patterns
Returns
Regex concatenation node (re.++(l, r, ...))

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().

◆ mkRegDiff()

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.

Parameters
paramsRegex patterns
Returns
Regex difference node (re.diff(l, r, ...))

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().

◆ mkRegInter()

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.

Parameters
paramsRegex patterns
Returns
Regex intersection node (re.inter(l, r, ...))

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().

◆ mkRegLoop()

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.

Parameters
lRegex pattern
rMinimum number of repetitions
sMaximum number of repetitions
Returns
Regex loop node (re.loop(l, r, s), i.e., l{r,s})

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().

◆ mkRegNone()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegNone ( )

Create a regex none node.

Creates a regex node that matches nothing.

Returns
Regex none node (re.none)

Definition at line 3745 of file op_parser.cpp.

References mkConstReg().

Referenced by parseConstFunc().

◆ mkRegOpt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRegOpt ( std::shared_ptr< DAGNode param)

Create a regex option node.

Creates a regex option node that matches zero or one occurrence of the pattern.

Parameters
paramRegex pattern
Returns
Regex option node (re.?(param)/re.opt(param), i.e., param?)

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().

◆ mkRegPlus()

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.

Parameters
paramRegex pattern
Returns
Regex plus node (re.+(param), i.e., param+)

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().

◆ mkRegRange()

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.

Parameters
lLower bound (inclusive)
rUpper bound (inclusive)
Returns
Regex range node (re.range(l, r), i.e., l..r)

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().

◆ mkRegRepeat()

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.

Parameters
lRegex pattern
rNumber of repetitions
Returns
Regex repeat node (re.^(n, l), i.e., l^n)

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().

◆ mkRegSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkRegSort ( )

Create a regular expression sort.

Returns
Regular expression sort

Definition at line 495 of file op_parser.cpp.

References stabilizer::parser::SortManager::REG_SORT.

◆ mkRegStar()

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.

Parameters
paramRegex pattern
Returns
Regex star node (re.*(param), i.e., param*)

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().

◆ mkRegUnion()

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.

Parameters
paramsRegex patterns
Returns
Regex union node (re.union(l, r, ...))

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().

◆ mkReplaceReg()

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.

Parameters
lString
rRegex pattern
vReplacement string
Returns
String replace-regex node (str.replace_re(l, r, v))

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.

◆ mkReplaceRegAll()

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.

Parameters
lString
rRegex pattern
vReplacement string
Returns
String replace-all-regex node (str.replace_all_re(l, r, v))

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.

◆ mkRootObj()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRootObj ( std::shared_ptr< DAGNode expr,
int  index 
)

◆ mkRootOfWithInterval()

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 
)

◆ mkRound()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRound ( std::shared_ptr< DAGNode param)

Create an round node.

Parameters
paramParameter
Returns
Round node (round(param))

Definition at line 1482 of file op_parser.cpp.

References stabilizer::parser::SortManager::INT_SORT, mkOper(), and stabilizer::parser::NT_ROUND.

Referenced by parseOper().

◆ mkRoundingMode()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkRoundingMode ( const std::string &  mode)

Create a rounding mode constant.

Parameters
modeRounding mode string (RNE, RNA, RTP, RTN, RTZ)
Returns
Rounding mode constant node

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().

◆ mkRoundingModeSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkRoundingModeSort ( )

Create a rounding mode sort.

Returns
Rounding mode sort

Definition at line 496 of file op_parser.cpp.

References stabilizer::parser::SortManager::ROUNDING_MODE_SORT.

◆ mkSafeSqrt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSafeSqrt ( std::shared_ptr< DAGNode param)

Create an safeSqrt node.

Note
if param < 0, return 0
Parameters
paramParameter
Returns
Safesqrt node (safeSqrt(param))

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().

◆ mkSbvToInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSbvToInt ( std::shared_ptr< DAGNode param)

◆ mkSec()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSec ( std::shared_ptr< DAGNode param)

Create an sec node.

Parameters
paramParameter
Returns
Sec node (sec(param))

Definition at line 1542 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_SEC, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkSech()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSech ( std::shared_ptr< DAGNode param)

Create a sech node.

Parameters
paramParameter
Returns
Sech node (sech(param))

Definition at line 1620 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_SECH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkSelect()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSelect ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create an array select node.

Parameters
lArray
rIndex
Returns
Array select node (l[r])

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().

◆ mkSin()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSin ( std::shared_ptr< DAGNode param)

Create an sin node.

Parameters
paramParameter
Returns
Sin node (sin(param))

Definition at line 1530 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_SIN, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkSinh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSinh ( std::shared_ptr< DAGNode param)

Create a sinh node.

Parameters
paramParameter
Returns
Sinh node (sinh(param))

Definition at line 1602 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_SINH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkSortDec()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkSortDec ( const std::string &  name,
const size_t &  arity 
)

Create a sort declaration.

Parameters
nameSort name
arityArity
Returns
Sort declaration node

Definition at line 480 of file op_parser.cpp.

References sort_manager.

Referenced by parseCommand().

◆ mkSortDef()

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.

Parameters
nameSort name
paramsParameters
out_sortOutput sort
Returns
Sort definition node

Definition at line 486 of file op_parser.cpp.

References sort_manager.

Referenced by parseCommand().

◆ mkSqrt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSqrt ( std::shared_ptr< DAGNode param)

Create an sqrt node.

Note
assert(param >= 0)
Parameters
paramParameter
Returns
Sqrt node (sqrt(param))

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().

◆ mkStore()

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.

Note
Returns a new array, the original array is not modified
Parameters
lArray
rIndex
vValue
Returns
Array store node (l[r] = v)

Definition at line 3294 of file op_parser.cpp.

References mkOper(), and stabilizer::parser::NT_STORE.

Referenced by parseOper().

◆ mkStrCharat()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrCharat ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string char-at node.

Parameters
lString
rIndex
Returns
String char-at node (str.at(l, r))

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().

◆ mkStrConcat()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrConcat ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a string concatenation node.

Parameters
paramsStrings to concatenate
Returns
String concatenation node (str.++(param1, param2, ...))

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().

◆ mkStrContains()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrContains ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string contains check node.

Parameters
lString
rSubstring
Returns
String contains check node (str.contains(l, r))

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().

◆ mkStrFromCode()

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.

Parameters
paramASCII code
Returns
String from-code conversion node (str.from_code(param))

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().

◆ mkStrFromInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrFromInt ( std::shared_ptr< DAGNode param)

Create a string from-integer conversion node.

Parameters
paramInteger
Returns
String from-integer conversion node (str.from_int(param))

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().

◆ mkStrGe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrGe ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a string greater-than-or-equal node.

Parameters
paramsOperand list containing two strings
Returns
String greater-than-or-equal node (str.>=(l, r))

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().

◆ mkStrGt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrGt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a string greater-than node.

Parameters
paramsOperand list containing two strings
Returns
String greater-than node (str.>(l, r))

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().

◆ mkStrIndexof()

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.

Parameters
lString
rSubstring to find
sStart index
Returns
String index-of node (str.indexof(l, r, s))

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().

◆ mkStrIndexofReg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrIndexofReg ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string indexof-regex node.

Parameters
lString
rRegular expression
Returns
String indexof-regex node (str.indexof_re(l, r))

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().

◆ mkStrInReg()

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.

Parameters
lString
rRegular expression
Returns
String in-regex check node (str.in_re(l, r))

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().

◆ mkStrIsDigit()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrIsDigit ( std::shared_ptr< DAGNode param)

Create a string is-digit check node.

Parameters
paramString
Returns
String is-digit check node (str.is_digit(param))

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().

◆ mkStrLe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrLe ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a string less-than-or-equal node.

Parameters
paramsOperand list containing two strings
Returns
String less-than-or-equal node (str.<=(l, r))

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().

◆ mkStrLen()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrLen ( std::shared_ptr< DAGNode param)

Create a string length node.

Parameters
paramString
Returns
String length node (str.len(param))

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().

◆ mkStrLt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrLt ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create a string less-than node.

Parameters
paramsOperand list containing two strings
Returns
String less-than node (str.<(l, r))

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().

◆ mkStrNumSplits()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrNumSplits ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

◆ mkStrNumSplitsRe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrNumSplitsRe ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

◆ mkStrPrefixof()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrPrefixof ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string prefix check node.

Parameters
lPrefix
rString
Returns
String prefix check node (str.prefixof(l, r))

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().

◆ mkStrReplace()

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.

Parameters
lString
rSubstring to replace
vReplacement string
Returns
String replace node (str.replace(l, r, v))

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().

◆ mkStrReplaceAll()

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.

Parameters
lString
rSubstring to replace
vReplacement string
Returns
String replace-all node (str.replace_all(l, r, v))

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().

◆ mkStrReplaceReg()

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.

Parameters
lString
rRegular expression
vReplacement string
Returns
String replace-regex node (str.replace_re(l, r, v))

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().

◆ mkStrReplaceRegAll()

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.

Parameters
lString
rRegular expression
vReplacement string
Returns
String replace-regex-all node (str.replace_re_all(l, r, v))

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().

◆ mkStrRev()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrRev ( std::shared_ptr< DAGNode param)

Create a string reverse node.

Parameters
paramString
Returns
String reverse node (str.rev(param))

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().

◆ mkStrSort()

std::shared_ptr< Sort > stabilizer::parser::Parser::mkStrSort ( )

Create a string sort.

Returns
String sort

Definition at line 494 of file op_parser.cpp.

References stabilizer::parser::SortManager::STR_SORT.

◆ mkStrSplit()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplit ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string split node.

Parameters
lString
rDelimiter
Returns
String split node (str.split(l, r))

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().

◆ mkStrSplitAt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitAt ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r,
std::shared_ptr< DAGNode s 
)

◆ mkStrSplitAtRe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitAtRe ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r,
std::shared_ptr< DAGNode s 
)

◆ mkStrSplitRest()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitRest ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r,
std::shared_ptr< DAGNode s 
)

◆ mkStrSplitRestRe()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSplitRestRe ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r,
std::shared_ptr< DAGNode s 
)

◆ mkStrSubstr()

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.

Parameters
lString
rStart index
sLength
Returns
String substring node (str.substr(l, r, s), i.e., l[r, r+s))

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().

◆ mkStrSuffixof()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrSuffixof ( std::shared_ptr< DAGNode l,
std::shared_ptr< DAGNode r 
)

Create a string suffix check node.

Parameters
lSuffix
rString
Returns
String suffix check node (str.suffixof(l, r))

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().

◆ mkStrToCode()

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.

Note
Assumes the string has exactly one character
Parameters
paramString
Returns
String to-code conversion node (str.to_code(param))

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().

◆ mkStrToInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToInt ( std::shared_ptr< DAGNode param)

Create a string to-integer conversion node.

Note
Returns -1 if the string does not represent a valid integer
Parameters
paramString
Returns
String to-integer conversion node (str.to_int(param))

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().

◆ mkStrToLower()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToLower ( std::shared_ptr< DAGNode param)

Create a string to-lower node.

Parameters
paramString
Returns
String to-lower node (str.to_lower(param))

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().

◆ mkStrToReg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToReg ( std::shared_ptr< DAGNode param)

Create a string to-regex conversion node.

Parameters
paramString
Returns
String to-regex conversion node (str.to_reg(param))

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().

◆ mkStrToUpper()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkStrToUpper ( std::shared_ptr< DAGNode param)

Create a string to-upper node.

Parameters
paramString
Returns
String to-upper node (str.to_upper(param))

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().

◆ mkStrUpdate()

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.

Parameters
lString
rIndex
vNew character
Returns
String update node (str.update(l, r, v), i.e., l[r] = v)

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().

◆ mkSub()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkSub ( const std::vector< std::shared_ptr< DAGNode > > &  params)

◆ mkTan()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTan ( std::shared_ptr< DAGNode param)

Create an tan node.

Note
assert(param != (pi/2) + k*pi)
Parameters
paramParameter
Returns
Tan node (tan(param))

Definition at line 1554 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_TAN, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkTanh()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTanh ( std::shared_ptr< DAGNode param)

Create a tanh node.

Parameters
paramParameter
Returns
Tanh node (tanh(param))

Definition at line 1614 of file op_parser.cpp.

References mkOper(), stabilizer::parser::NT_TANH, and stabilizer::parser::SortManager::REAL_SORT.

Referenced by parseOper().

◆ mkTempVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTempVar ( const std::shared_ptr< Sort > &  sort)

Create a temporary variable.

Parameters
sortSort
Returns
Temporary variable node

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.

◆ mkToFp() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToFp ( std::shared_ptr< DAGNode eb,
std::shared_ptr< DAGNode sb,
std::shared_ptr< DAGNode param 
)

◆ mkToFp() [2/2]

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.

Parameters
ebExponent bit width
sbSignificand bit width
paramValue to convert
Returns
Value to floating-point conversion node (to_fp(eb, sb, param))

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().

◆ mkToFpUnsigned()

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 
)

◆ mkToInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToInt ( std::shared_ptr< DAGNode param)

Create a to_int node.

Parameters
paramParameter
Returns
To_int node (to_int(param))

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().

◆ mkToReal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkToReal ( std::shared_ptr< DAGNode param)

Create a to_real node.

Parameters
paramParameter
Returns
To_real node (to_real(param))

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().

◆ mkTrue()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkTrue ( )

◆ mkUbvToInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkUbvToInt ( std::shared_ptr< DAGNode param)

◆ mkUFVNode()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkUFVNode ( const std::string &  name,
const std::shared_ptr< Sort > &  sort 
)
inline

Definition at line 311 of file parser.h.

References node_manager, and stabilizer::parser::NT_UF_NAME.

◆ mkUnknown()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkUnknown ( )

Create an unknown node.

Returns
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().

◆ mkVar()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVar ( const std::shared_ptr< Sort > &  sort,
const std::string &  name 
)

Create a variable.

Parameters
sortSort
nameVariable name
Returns
Variable node

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().

◆ mkVarBool()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarBool ( const std::string &  name)

Create a boolean variable.

Parameters
nameVariable name
Returns
Boolean variable node

Definition at line 817 of file op_parser.cpp.

References stabilizer::parser::SortManager::BOOL_SORT, and mkVar().

◆ mkVarBv()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarBv ( const std::string &  name,
const size_t &  width 
)

Create a bit-vector variable.

Parameters
nameVariable name
widthWidth of the bit-vector
Returns
Bit-vector variable node

Definition at line 826 of file op_parser.cpp.

References mkVar(), sort_key_map, and sort_manager.

◆ mkVarFp()

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.

Parameters
nameVariable name
eExponent size
sSignificand size
Returns
Floating-point variable node

Definition at line 840 of file op_parser.cpp.

References mkVar(), sort_key_map, and sort_manager.

◆ mkVarInt()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarInt ( const std::string &  name)

Create an integer variable.

Parameters
nameVariable name
Returns
Integer variable node

Definition at line 820 of file op_parser.cpp.

References stabilizer::parser::SortManager::INT_SORT, and mkVar().

◆ mkVarReal()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarReal ( const std::string &  name)

Create a real variable.

Parameters
nameVariable name
Returns
Real variable node

Definition at line 823 of file op_parser.cpp.

References mkVar(), and stabilizer::parser::SortManager::REAL_SORT.

◆ mkVarReg()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarReg ( const std::string &  name)

Create a regular expression variable.

Parameters
nameVariable name
Returns
Regular expression variable node

Definition at line 859 of file op_parser.cpp.

References mkVar(), and stabilizer::parser::SortManager::REG_SORT.

◆ mkVarRoundingMode()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarRoundingMode ( const std::string &  name)

Create a rounding mode variable.

Parameters
nameVariable name
Returns
Rounding mode variable node

Definition at line 862 of file op_parser.cpp.

References mkVar(), and stabilizer::parser::SK_ROUNDING_MODE.

◆ mkVarStr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkVarStr ( const std::string &  name)

Create a string variable.

Parameters
nameVariable name
Returns
String variable node

Definition at line 856 of file op_parser.cpp.

References mkVar(), and stabilizer::parser::SortManager::STR_SORT.

◆ mkWeight()

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().

◆ mkXor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::mkXor ( const std::vector< std::shared_ptr< DAGNode > > &  params)

Create an xor node.

Parameters
paramsParameters
Returns
Xor node (l xor m xor r xor ...)

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().

◆ optionToString()

std::string stabilizer::parser::Parser::optionToString ( )

Print the options.

Returns
String representation of the options

Definition at line 2688 of file base_parser.cpp.

References options.

◆ parse()

bool stabilizer::parser::Parser::parse ( const std::string &  filename)

Parse SMT-LIB2 file.

Parses the specified SMT-LIB2 file and builds internal data structures.

Parameters
filenamePath to the SMT-LIB2 file to parse
Returns
True if parsing was successful, false otherwise

Definition at line 79 of file base_parser.cpp.

References parseSmtlib2File().

Referenced by stabilizer::api::SMTStabilizer::apply_file().

◆ parseCommand()

CMD_TYPE stabilizer::parser::Parser::parseCommand ( )
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().

◆ parseConstFunc()

◆ parseExpr()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::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().

◆ parseGroup()

std::string stabilizer::parser::Parser::parseGroup ( )
private

◆ parseKeyword()

◆ parseLet()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::parseLet ( )
private

◆ parseLpar()

void stabilizer::parser::Parser::parseLpar ( )
private

◆ parseOper()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::parseOper ( const std::string &  s,
const std::vector< std::shared_ptr< DAGNode > > &  func_args,
const std::vector< std::shared_ptr< DAGNode > > &  oper_params 
)
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().

◆ parseParams()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::parseParams ( )
private

Definition at line 1768 of file base_parser.cpp.

References bufptr, and parseExpr().

◆ parsePreservingLet()

◆ parseQuant()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::parseQuant ( const std::string &  type)
private

◆ parseRpar()

void stabilizer::parser::Parser::parseRpar ( )
private

◆ parseSmtlib2File()

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.

Parameters
filenamePath to the SMT-LIB2 file
Returns
Boolean indicating success

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().

Referenced by parse(), and Parser().

◆ parseSort()

◆ parseStr()

bool stabilizer::parser::Parser::parseStr ( const std::string &  constraint)

Parse a constraint.

Parses the specified constraint and builds internal data structures.

Parameters
constraintConstraint to parse
Returns
True if parsing was successful, false otherwise

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().

◆ parseWeight()

std::string stabilizer::parser::Parser::parseWeight ( )
private

◆ peekSymbol()

std::string stabilizer::parser::Parser::peekSymbol ( )
private

Definition at line 2036 of file base_parser.cpp.

References bufptr, getSymbol(), line_number, scan_mode, and scanToNextSymbol().

Referenced by parseLet(), and parsePreservingLet().

◆ rebuild_node_manager()

void stabilizer::parser::Parser::rebuild_node_manager ( )
inline

Definition at line 767 of file parser.h.

References node_manager.

◆ rebuildLetBindings()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::rebuildLetBindings ( const std::shared_ptr< DAGNode > &  root)

◆ remove() [1/2]

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.

Parameters
exprExpression to remove nodes from
nodesNodes to remove
Returns
Expression with removed nodes

◆ remove() [2/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::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 
)
private

◆ removeFuns()

size_t stabilizer::parser::Parser::removeFuns ( const std::vector< std::string > &  funcNames)

Remove functions by name.

Parameters
funcNamesVector of function names to remove
Returns
Number of functions actually removed

Definition at line 2988 of file base_parser.cpp.

References fun_key_map, and function_names.

◆ rename()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::rename ( std::shared_ptr< DAGNode expr,
const std::string &  new_name 
)

Rename a node.

Parameters
exprExpression to rename
new_nameNew name
Returns
Expression with renamed node

Definition at line 2659 of file base_parser.cpp.

References condAssert, temp_var_names, and var_names.

◆ replaceAssertions()

void stabilizer::parser::Parser::replaceAssertions ( const std::vector< std::shared_ptr< DAGNode > > &  new_assertions)
inline

Definition at line 307 of file parser.h.

References assertions.

◆ replaceAtoms()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::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 
)
private

◆ replaceNodes()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::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 
)
private

◆ rewrite() [1/5]

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.

Parameters
tOperation kind (may be updated during rewrite).
lFirst operand.
mSecond operand.
rThird operand.
Returns
Rewritten node, or nullptr when no rewrite is applied.

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().

◆ rewrite() [2/5]

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.

Parameters
tOperation kind (may be updated during rewrite).
lFirst operand.
mlSecond operand.
mrThird operand.
rFourth operand.
Returns
Rewritten node, or nullptr when no rewrite is applied.

Definition at line 1007 of file rewrite_parser.cpp.

References stabilizer::parser::echo_error(), and stabilizer::parser::NT_FP_FMA.

◆ rewrite() [3/5]

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.

Parameters
tOperation kind (may be updated during rewrite).
lLeft operand.
rRight operand.
Returns
Rewritten node, or nullptr when no rewrite is applied.

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().

◆ rewrite() [4/5]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::rewrite ( NODE_KIND t,
std::shared_ptr< DAGNode > &  p 
)

Rewrite unary operation node when simplification rule applies.

Parameters
tOperation kind (may be updated during rewrite).
pOperand node.
Returns
Rewritten node, or nullptr when no rewrite is applied.

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().

◆ rewrite() [5/5]

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.

Parameters
tOperation kind (may be updated during rewrite).
pOperand list.
Returns
Rewritten node, or nullptr when no rewrite is applied.

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().

◆ rewrite_oper()

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.

Parameters
tOperation kind (may be updated during rewrite).
pOperand list.
Returns
Rewritten node, or nullptr when caller should create a fresh node.

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().

◆ scanToNextSymbol()

◆ setEvaluatePrecision()

void stabilizer::parser::Parser::setEvaluatePrecision ( mpfr_prec_t  precision)

Set the precision for evaluation.

Parameters
precisionPrecision

Definition at line 278 of file base_parser.cpp.

References options.

◆ setEvaluateUseFloating()

void stabilizer::parser::Parser::setEvaluateUseFloating ( bool  use_floating)

Set the use floating for evaluation.

Parameters
use_floatingUse floating

Definition at line 284 of file base_parser.cpp.

References options.

◆ setOption() [1/4]

void stabilizer::parser::Parser::setOption ( const std::string &  key,
const bool &  value 
)

Definition at line 232 of file base_parser.cpp.

References options.

◆ setOption() [2/4]

void stabilizer::parser::Parser::setOption ( const std::string &  key,
const double &  value 
)

Definition at line 229 of file base_parser.cpp.

References options.

◆ setOption() [3/4]

void stabilizer::parser::Parser::setOption ( const std::string &  key,
const int &  value 
)

Definition at line 226 of file base_parser.cpp.

References options.

◆ setOption() [4/4]

void stabilizer::parser::Parser::setOption ( const std::string &  key,
const std::string &  value 
)

Set global options.

Parameters
keyOption name
valueOption value

Definition at line 223 of file base_parser.cpp.

References options.

◆ skipToRpar()

void stabilizer::parser::Parser::skipToRpar ( )
private

◆ sortParams()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::Parser::sortParams ( const std::vector< std::shared_ptr< DAGNode > > &  p)
static

Return sorted operand list for deterministic commutative handling.

Definition at line 173 of file op_parser.cpp.

Referenced by mkInternalOper(), and mkNode().

◆ substitute() [1/2]

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.

Note
This function is used to substitute variables in an expression but not simplify the expression.
Parameters
exprExpression to substitute
paramsMap of variable names to their corresponding values
Returns
Substituted expression

Definition at line 2366 of file base_parser.cpp.

References substitute().

Referenced by substitute().

◆ substitute() [2/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::substitute ( std::shared_ptr< DAGNode expr,
std::unordered_map< std::string, std::shared_ptr< DAGNode > > &  params,
std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &  visited 
)
private

Definition at line 2374 of file base_parser.cpp.

References mkOper(), and node_manager.

◆ toCNF()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toCNF ( std::shared_ptr< DAGNode expr)
private

◆ toDNFEliminateAll() [1/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toDNFEliminateAll ( std::shared_ptr< DAGNode expr)
private

◆ toDNFEliminateAll() [2/2]

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toDNFEliminateAll ( std::shared_ptr< DAGNode expr,
std::unordered_map< std::shared_ptr< DAGNode >, std::shared_ptr< DAGNode > > &  visited,
bool &  is_changed 
)
private

◆ toDNFEliminateDistinct()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toDNFEliminateDistinct ( const std::vector< std::shared_ptr< DAGNode > > &  children)
private

◆ toDNFEliminateEq()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toDNFEliminateEq ( const std::vector< std::shared_ptr< DAGNode > > &  children)
private

◆ toDNFEliminateXOR()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toDNFEliminateXOR ( const std::vector< std::shared_ptr< DAGNode > > &  children)
private

◆ toInt()

Integer stabilizer::parser::Parser::toInt ( std::shared_ptr< DAGNode expr)

Convert an expression to an integer.

Parameters
exprExpression to convert
Returns
Integer

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().

◆ toNNF()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toNNF ( std::shared_ptr< DAGNode expr,
bool  is_not 
)
private

◆ toReal()

Real stabilizer::parser::Parser::toReal ( std::shared_ptr< DAGNode expr)

Convert an expression to a real.

Parameters
exprExpression to convert
Returns
Real

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().

◆ toString() [1/3]

std::string stabilizer::parser::Parser::toString ( const NODE_KIND kind)

Print a node kind.

Parameters
kindNode kind to print
Returns
String representation of the node kind

Definition at line 2684 of file base_parser.cpp.

References stabilizer::parser::kindToString().

◆ toString() [2/3]

std::string stabilizer::parser::Parser::toString ( std::shared_ptr< DAGNode expr)

Print an expression.

Parameters
exprExpression to print
Returns
String representation of the expression

Definition at line 2676 of file base_parser.cpp.

References stabilizer::parser::dumpSMTLIB2().

Referenced by mkRootObj(), and mkRootOfWithInterval().

◆ toString() [3/3]

std::string stabilizer::parser::Parser::toString ( std::shared_ptr< Sort sort)

Print a sort.

Parameters
sortSort to print
Returns
String representation of the sort

Definition at line 2680 of file base_parser.cpp.

◆ toTseitinCNF()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::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 
)
private

◆ toTseitinDistinct()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toTseitinDistinct ( std::shared_ptr< DAGNode a,
std::shared_ptr< DAGNode b,
std::vector< std::shared_ptr< DAGNode > > &  clauses 
)
private

◆ toTseitinEq()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toTseitinEq ( std::shared_ptr< DAGNode a,
std::shared_ptr< DAGNode b,
std::vector< std::shared_ptr< DAGNode > > &  clauses 
)
private

◆ toTseitinXor()

std::shared_ptr< DAGNode > stabilizer::parser::Parser::toTseitinXor ( std::shared_ptr< DAGNode a,
std::shared_ptr< DAGNode b,
std::vector< std::shared_ptr< DAGNode > > &  clauses 
)
private

◆ warn_cmd_nsup()

void stabilizer::parser::Parser::warn_cmd_nsup ( const std::string  nm,
const size_t  ln 
) const
private

Definition at line 3015 of file base_parser.cpp.

Referenced by parseCommand().

Member Data Documentation

◆ allow_placeholder_vars

bool stabilizer::parser::Parser::allow_placeholder_vars
private

Definition at line 194 of file parser.h.

Referenced by parseConstFunc(), parseExpr(), Parser(), and Parser().

◆ assertion_groups

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().

◆ assertions

std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::assertions

◆ assumptions

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().

◆ buffer

char* stabilizer::parser::Parser::buffer
private

Definition at line 184 of file parser.h.

Referenced by getSymbol(), mkExpr(), Parser(), Parser(), parseSmtlib2File(), and parseStr().

◆ buflen

unsigned long stabilizer::parser::Parser::buflen
private

Definition at line 185 of file parser.h.

Referenced by getSymbol(), mkExpr(), Parser(), Parser(), parseSmtlib2File(), and parseStr().

◆ bufptr

◆ cnf_atom_map

std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::cnf_atom_map
private

Definition at line 250 of file parser.h.

◆ cnf_bool_var_map

std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::cnf_bool_var_map
private

Definition at line 252 of file parser.h.

◆ cnf_map

std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::cnf_map
private

Definition at line 248 of file parser.h.

◆ current_let_mode

LET_MODE stabilizer::parser::Parser::current_let_mode
private

Definition at line 190 of file parser.h.

Referenced by parseConstFunc(), and parseExpr().

◆ datatype_blocks

std::vector<std::vector<DTTypeDecl> > stabilizer::parser::Parser::datatype_blocks
private

Definition at line 222 of file parser.h.

Referenced by dumpSMT2(), getDatatypeBlocks(), and parseCommand().

◆ datatype_function_names

std::unordered_set<std::string> stabilizer::parser::Parser::datatype_function_names
private

Definition at line 227 of file parser.h.

Referenced by applyFun(), parseCommand(), and parseConstFunc().

◆ datatype_sort_names

std::unordered_set<std::string> stabilizer::parser::Parser::datatype_sort_names
private

Definition at line 224 of file parser.h.

Referenced by parseCommand().

◆ dnf_map

std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::dnf_map
private

Definition at line 254 of file parser.h.

◆ fun_dup_count_map

std::unordered_map<std::string, size_t> stabilizer::parser::Parser::fun_dup_count_map
private

Definition at line 216 of file parser.h.

Referenced by mkFuncDec().

◆ fun_key_map

std::unordered_map<std::string, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::fun_key_map
private

◆ fun_var_map

std::unordered_map<std::string, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::fun_var_map
private

Definition at line 211 of file parser.h.

Referenced by parseCommand(), parseConstFunc(), Parser(), and Parser().

◆ function_names

std::vector<std::string> stabilizer::parser::Parser::function_names
private

Definition at line 240 of file parser.h.

Referenced by getFunctionNames(), getFunctions(), parseCommand(), Parser(), Parser(), and removeFuns().

◆ in_quantifier_scope

bool stabilizer::parser::Parser::in_quantifier_scope
private

Definition at line 193 of file parser.h.

Referenced by parseCommand(), parseConstFunc(), parseExpr(), Parser(), and Parser().

◆ let_key_map

std::unordered_map<std::string, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::let_key_map
private

Definition at line 206 of file parser.h.

Referenced by parseConstFunc(), parseLet(), Parser(), and Parser().

◆ let_nesting_depth

size_t stabilizer::parser::Parser::let_nesting_depth
private

Definition at line 191 of file parser.h.

Referenced by parseExpr(), Parser(), and Parser().

◆ line_number

size_t stabilizer::parser::Parser::line_number
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().

◆ named_assertions

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().

◆ nnf_map

std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::nnf_map
private

Definition at line 256 of file parser.h.

◆ node_manager

◆ num_quant_vars

size_t stabilizer::parser::Parser::num_quant_vars = 0
private

Definition at line 262 of file parser.h.

Referenced by mkQuantVar().

◆ options

◆ parse_options

std::vector<std::string> stabilizer::parser::Parser::parse_options
private

Definition at line 198 of file parser.h.

Referenced by dumpSMT2(), and parseCommand().

◆ parsing_file

bool stabilizer::parser::Parser::parsing_file
private

Definition at line 197 of file parser.h.

Referenced by assert(), getSymbol(), mkExpr(), Parser(), Parser(), and parseSmtlib2File().

◆ pattern_assertions

std::vector<std::pair<std::shared_ptr<DAGNode>, std::vector<std::vector<std::shared_ptr<DAGNode> > > > > stabilizer::parser::Parser::pattern_assertions

Definition at line 272 of file parser.h.

◆ placeholder_var_names

std::unordered_map<std::string, size_t> stabilizer::parser::Parser::placeholder_var_names
private

Definition at line 236 of file parser.h.

Referenced by mkPlaceholderVar(), and parseConstFunc().

◆ placeholder_var_sort

std::shared_ptr<Sort> stabilizer::parser::Parser::placeholder_var_sort
private

Definition at line 195 of file parser.h.

Referenced by mkPlaceholderVar(), parseExpr(), Parser(), and Parser().

◆ preserving_let_counter

size_t stabilizer::parser::Parser::preserving_let_counter
private

Definition at line 189 of file parser.h.

Referenced by parseConstFunc(), parseExpr(), parsePreservingLet(), Parser(), and Parser().

◆ preserving_let_key_map

std::unordered_map<std::string, std::shared_ptr<DAGNode> > stabilizer::parser::Parser::preserving_let_key_map
private

◆ quant_nesting_depth

size_t stabilizer::parser::Parser::quant_nesting_depth
private

Definition at line 192 of file parser.h.

Referenced by parseCommand(), parseExpr(), Parser(), and Parser().

◆ quant_var_map

std::unordered_map<std::string, std::vector<std::shared_ptr<DAGNode> > > stabilizer::parser::Parser::quant_var_map
private

Definition at line 214 of file parser.h.

Referenced by mkQuantVar(), parseConstFunc(), parseQuant(), Parser(), and Parser().

◆ result_node

std::shared_ptr<DAGNode> stabilizer::parser::Parser::result_node
private

Definition at line 260 of file parser.h.

Referenced by getResult().

◆ result_type

RESULT_TYPE stabilizer::parser::Parser::result_type
private

Definition at line 259 of file parser.h.

Referenced by checkSat(), and getResultType().

◆ scan_mode

SCAN_MODE stabilizer::parser::Parser::scan_mode
private

Definition at line 188 of file parser.h.

Referenced by getSymbol(), parseCommand(), Parser(), Parser(), peekSymbol(), scanToNextSymbol(), and skipToRpar().

◆ soft_assertion_groups

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().

◆ soft_assertions

std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::soft_assertions

Definition at line 274 of file parser.h.

Referenced by getNodeCount(), and getSoftAssertions().

◆ soft_weights

std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::soft_weights

Definition at line 275 of file parser.h.

Referenced by getNodeCount(), and getSoftWeights().

◆ sort_key_map

std::unordered_map<std::string, std::shared_ptr<Sort> > stabilizer::parser::Parser::sort_key_map
private

◆ sort_manager

◆ split_lemmas

std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::split_lemmas

Definition at line 279 of file parser.h.

◆ static_functions

std::vector<std::shared_ptr<DAGNode> > stabilizer::parser::Parser::static_functions
private

Definition at line 218 of file parser.h.

Referenced by mkApplyFunc(), mkApplyRecFunc(), Parser(), and Parser().

◆ temp_var_counter

size_t stabilizer::parser::Parser::temp_var_counter
private

Definition at line 233 of file parser.h.

Referenced by mkTempVar(), Parser(), and Parser().

◆ temp_var_names

std::unordered_map<std::string, size_t> stabilizer::parser::Parser::temp_var_names
private

Definition at line 234 of file parser.h.

Referenced by getTempVarNames(), getVariable(), getVariables(), mkTempVar(), Parser(), Parser(), and rename().

◆ var_names

std::unordered_map<std::string, size_t> stabilizer::parser::Parser::var_names
private

The documentation for this class was generated from the following files: