parser.h

Go to the documentation of this file.

/* -*- Header -*-
 *
 * An SMT/OMT Parser
 *
 * Author: Fuqi Jia <jiafq@ios.ac.cn>
 *
 * Copyright (C) 2025 Fuqi Jia
 *
 * Permission is hereby granted, free of charge, to any person obtaining a
 * copy of this software and associated documentation files (the "Software"),
 * to deal in the Software without restriction, including without limitation
 * the rights to use, copy, modify, merge, publish, distribute, sublicense,
 * and/or sell copies of the Software, and to permit persons to whom the
 * Software is furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 * DEALINGS IN THE SOFTWARE.
 */
// Modified by Xiang Zhang, 2026
// Additional changes licensed under the MIT License
#ifndef PARSER_HEADER
#define PARSER_HEADER
 
#include <cstddef>
#include <memory>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <vector>
 
#include "dag.h"
// #include "objective.h"
#include "options.h"
#include "parser/kind.h"
#include "util.h"
 
namespace stabilizer::parser {
#undef assert
enum class SCAN_MODE {
    SM_COMMON,
    SM_SYMBOL,
    SM_COMP_SYM,
    SM_COMMENT,
    SM_STRING
};
 
// LET mode, only used in preserving let mode
enum class LET_MODE {
    LM_NON_LET,    // not in let
    LM_START_LET,  // start of let
    LM_IN_LET,     // in let
};
 
enum class KEYWORD {
    KW_ID,
    KW_WEIGHT,
    KW_COMP,
    KW_EPSILON,
    KW_M,
    KW_OPT_KIND,
    KW_NAMED,
    KW_PATTERN,
    KW_NO_PATTERN,
    KW_QID,
    KW_SKOLEMID,
    KW_LBLPOS,
    KW_LBLNEG,
    KW_NULL
};
 
enum class CMD_TYPE {
    CT_UNKNOWN,
    CT_EOF,
    // COMMANDS
    CT_ASSERT,
    CT_CHECK_SAT,
    CT_CHECK_SAT_ASSUMING,
    CT_DECLARE_CONST,
    CT_DECLARE_FUN,
    CT_DECLARE_SORT,
    CT_DEFINE_FUN,
    CT_DEFINE_FUN_REC,
    CT_DEFINE_FUNS_REC,
    CT_DEFINE_SORT,
    CT_ECHO,
    CT_EXIT,
    CT_GET_ASSERTIONS,
    CT_GET_ASSIGNMENT,
    CT_GET_INFO,
    CT_GET_MODEL,
    CT_GET_OPTION,
    CT_GET_PROOF,
    CT_GET_UNSAT_ASSUMPTIONS,
    CT_GET_UNSAT_CORE,
    CT_GET_VALUE,
    CT_POP,
    CT_PUSH,
    CT_RESET,
    CT_RESET_ASSERTIONS,
    CT_SET_INFO,
    CT_SET_LOGIC,
    CT_SET_OPTION,
    // QUANTIFIER
    CT_EXISTS,
    CT_FORALL,
    // OPTIMIZATION COMMANDS
    CT_GET_OBJECTIVES,
    CT_ASSERT_SOFT,
    CT_DEFINE_OBJ,
    CT_DEFINE_MIN_OBJ,
    CT_DEFINE_MAX_OBJ,
    CT_MINIMIZE,
    CT_MAXIMIZE,
    CT_LEX_OPTIMIZE,
    CT_PARETO_OPTIMIZE,
    CT_BOX_OPTIMIZE,
    CT_MINMAX,
    CT_MAXMIN,
    CT_MAXSAT,
    CT_MINSAT,
    CT_OPTIMIZE
    // CT_LEX_MAXIMIZE, CT_PARETO_MINIMIZE, CT_PARETO_MAXIMIZE,
    // CT_BOX_MINIMIZE, CT_BOX_MAXIMIZE, CT_MINMAX, CT_MAXMIN
};
 
enum class ERROR_TYPE {
    ERR_UNEXP_EOF,
    ERR_SYM_MIS,
    ERR_UNKWN_SYM,
    ERR_PARAM_MIS,
    ERR_PARAM_NBOOL,
    ERR_PARAM_NNUM,
    ERR_PARAM_NSAME,
    ERR_LOGIC,
    ERR_MUL_DECL,
    ERR_MUL_DEF,
    ERR_ZERO_DIVISOR,
    ERR_FUN_LOCAL_VAR,
    ERR_ARI_MIS,
    ERR_TYPE_MIS,
    ERR_NEG_PARAM
};
 
enum class RESULT_TYPE { RT_SAT,
                         RT_UNSAT,
                         RT_DELTA_SAT,
                         RT_UNKNOWN,
                         RT_ERROR };
 
/*
Parser
*/
 
// NOTE: only non-incremental mode
class Parser {
  public:
    // Datatype declarations captured for dumping
    struct DTSelectorDecl {
        std::string name;
        std::shared_ptr<Sort> sort;
    };
    struct DTConstructorDecl {
        std::string name;
        std::vector<DTSelectorDecl> selectors;
    };
    struct DTTypeDecl {
        std::string name;
        size_t arity = 0;
        std::vector<DTConstructorDecl> ctors;
    };
 
  private:
    // attributes
 
    // vars for parser
    char *buffer;
    unsigned long buflen;
    char *bufptr;
    size_t line_number;
    SCAN_MODE scan_mode;
    size_t preserving_let_counter;  // only used in preserving let mode
    LET_MODE current_let_mode;      // only used in preserving let mode
    size_t let_nesting_depth;       // track let nesting depth
    size_t quant_nesting_depth;     // track quantifier nesting depth
    bool in_quantifier_scope;
    bool allow_placeholder_vars;                 // allow creating placeholder variables
    std::shared_ptr<Sort> placeholder_var_sort;  // sort for placeholder variables
 
    bool parsing_file;
    std::vector<std::string> parse_options;
 
    // node manager
    std::unique_ptr<NodeManager> node_manager;
    // sort manager
    std::unique_ptr<SortManager> sort_manager;
 
    std::unordered_map<std::string, std::shared_ptr<DAGNode>>
        let_key_map;  // local variables, no need to hash store
    std::unordered_map<std::string, std::shared_ptr<DAGNode>>
        preserving_let_key_map;  // global variables, no need to hash store
    std::unordered_map<std::string, std::shared_ptr<DAGNode>> fun_key_map;
    std::unordered_map<std::string, std::shared_ptr<DAGNode>>
        fun_var_map;  // variables are not the same, no need to hash store
    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;  // track duplicate function names
    std::vector<std::shared_ptr<DAGNode>>
        static_functions;  // static functions without substitution
 
    // Datatype tracking for output
    std::vector<std::vector<DTTypeDecl>>
        datatype_blocks;  // list of blocks, each with types in the block
    std::unordered_set<std::string>
        datatype_sort_names;  // names declared by datatypes to suppress
                              // declare-sort
    std::unordered_set<std::string>
        datatype_function_names;  // ctor/selector names for DT_FUN_APPLY
                                  // classification
 
    // variable name list
    std::unordered_map<std::string, size_t> var_names;
    // temp var
    size_t temp_var_counter;
    std::unordered_map<std::string, size_t> temp_var_names;
    // placeholder variables
    std::unordered_map<std::string, size_t> placeholder_var_names;
 
    // temp var name list
    // function name list
    std::vector<std::string> function_names;
    // global options
    std::shared_ptr<GlobalOptions> options;
    // // (define-objective name single_opt)
    // std::unordered_map<std::string, std::shared_ptr<Objective>>
    //     objective_map;
    // conversion map
    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;  // bool_var -> atom
    std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
        cnf_bool_var_map;  // atom -> bool_var
    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
    RESULT_TYPE result_type;
    std::shared_ptr<DAGNode> result_node;
 
    size_t num_quant_vars = 0;
 
  public:
    std::vector<std::shared_ptr<DAGNode>> assertions;
    std::unordered_map<std::string, std::unordered_set<size_t>> assertion_groups;
    //: named
    std::unordered_map<std::string, std::shared_ptr<DAGNode>> named_assertions;
    //: pattern
    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<Objective>> objectives;
    std::vector<std::shared_ptr<DAGNode>> split_lemmas;
 
  public:
    Parser(const std::string &filename);
 
    Parser();
 
    ~Parser();
 
    void replaceAssertions(
        const std::vector<std::shared_ptr<DAGNode>> &new_assertions) {
        assertions = new_assertions;
    }
    std::shared_ptr<DAGNode> mkUFVNode(const std::string &name,
                                       const std::shared_ptr<Sort> &sort) {
        return node_manager->createNode(sort, NODE_KIND::NT_UF_NAME, name);
    }
    std::shared_ptr<DAGNode>
    rebuildLetBindings(const std::shared_ptr<DAGNode> &root);
 
    std::unordered_map<std::string, size_t> &getTempVarNames() {
        return temp_var_names;
    }
    std::unordered_map<std::string, size_t> &getVarNames() { return var_names; }
    std::unordered_map<std::string, std::shared_ptr<DAGNode>> &getFunKeyMap() {
        return fun_key_map;
    }
    std::vector<std::string> &getFunctionNames() { return function_names; }
    std::unordered_map<std::string, std::shared_ptr<Sort>> &getSortNames() {
        return sort_key_map;
    }
    std::vector<std::vector<DTTypeDecl>> &getDatatypeBlocks() {
        return datatype_blocks;
    }
    void clear_let_key_map() { preserving_let_key_map.clear(); }
    bool parse(const std::string &filename);
 
    bool parseStr(const std::string &constraint);
 
    bool assert(const std::string &constraint);
 
    bool assert(std::shared_ptr<DAGNode> node);
 
    std::shared_ptr<DAGNode> mkExpr(const std::string &expression);
 
    // to solver
    std::vector<std::shared_ptr<DAGNode>> getAssertions() const;
 
    std::unordered_map<std::string, std::unordered_set<size_t>>
    getGroupedAssertions() const;
 
    std::vector<std::vector<std::shared_ptr<DAGNode>>> getAssumptions() const;
 
    std::vector<std::shared_ptr<DAGNode>> getSoftAssertions() const;
 
    std::vector<std::shared_ptr<DAGNode>> getSoftWeights() const;
 
    std::unordered_map<std::string, std::unordered_set<size_t>>
    getGroupedSoftAssertions() const;
 
    // /**
    //  * @brief Get objectives
    //  *
    //  * @return Vector of all objectives
    //  */
    // std::vector<std::shared_ptr<Objective>> getObjectives() const;
 
    void setOption(const std::string &key, const std::string &value);
    void setOption(const std::string &key, const int &value);
    void setOption(const std::string &key, const double &value);
    void setOption(const std::string &key, const bool &value);
 
    std::shared_ptr<GlobalOptions> getOptions() const;
 
    std::vector<std::shared_ptr<DAGNode>> getVariables() const;
 
    std::vector<std::shared_ptr<DAGNode>> getDeclaredVariables() const;
 
    bool isDeclaredVariable(const std::string &var_name) const;
 
    std::shared_ptr<DAGNode> getVariable(const std::string &var_name);
 
    std::vector<std::shared_ptr<DAGNode>> getFunctions() const;
 
    bool isDeclaredFunction(const std::string &func_name) const;
 
    // get sort
    std::shared_ptr<Sort>
    getSort(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<Sort> getSort(std::shared_ptr<DAGNode> param);
 
    std::shared_ptr<Sort> getSort(std::shared_ptr<DAGNode> l,
                                  std::shared_ptr<DAGNode> r);
 
    std::shared_ptr<Sort> getSort(std::shared_ptr<DAGNode> l,
                                  std::shared_ptr<DAGNode> r,
                                  std::shared_ptr<DAGNode> m);
 
    NODE_KIND getKind(const std::string &s);
 
    NODE_KIND getKind(const std::shared_ptr<DAGNode> &node);
 
    // get result type
    RESULT_TYPE getResultType();
 
    // get result
    std::shared_ptr<DAGNode> getResult();
 
    // check sat
    RESULT_TYPE checkSat();
 
    // get node count
    size_t getNodeCount();
 
    // mk oper
    std::shared_ptr<DAGNode> mkOper(const std::shared_ptr<Sort> &sort,
                                    const NODE_KIND &t,
                                    std::shared_ptr<DAGNode> p);
 
    std::shared_ptr<DAGNode> mkOper(const std::shared_ptr<Sort> &sort,
                                    const NODE_KIND &t,
                                    std::shared_ptr<DAGNode> l,
                                    std::shared_ptr<DAGNode> r);
 
    std::shared_ptr<DAGNode> mkOper(const std::shared_ptr<Sort> &sort,
                                    const NODE_KIND &t,
                                    std::shared_ptr<DAGNode> l,
                                    std::shared_ptr<DAGNode> m,
                                    std::shared_ptr<DAGNode> r);
 
    std::shared_ptr<DAGNode>
    mkOper(const std::shared_ptr<Sort> &sort, const NODE_KIND &t, const std::vector<std::shared_ptr<DAGNode>> &p);
 
    // /**
    //  * @brief Simplify an operation
    //  *
    //  * @note The parameters are assumed to be constant.
    //  *
    //  * @param t Operation kind
    //  * @param p Parameters
    //  * @return Simplified operation node
    //  */
    // std::shared_ptr<DAGNode> simp_oper(const NODE_KIND& t,
    // std::shared_ptr<DAGNode> p);
 
    // /**
    //  * @brief Simplify an operation
    //  *
    //  * @note The parameters are assumed to be constant.
    //  *
    //  * @param t Operation kind
    //  * @param l Left parameter
    //  * @param r Right parameter
    //  * @return Simplified operation node
    //  */
    // std::shared_ptr<DAGNode> simp_oper(const NODE_KIND& t,
    // std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r);
 
    // /**
    //  * @brief Simplify an operation
    //  *
    //  * @note The parameters are assumed to be constant.
    //  *
    //  * @param t Operation kind
    //  * @param l Left parameter
    //  * @param m Middle parameter
    //  * @param r Right parameter
    //  * @return Simplified operation node
    //  */
    // std::shared_ptr<DAGNode> simp_oper(const NODE_KIND& t,
    // std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> m,
    // std::shared_ptr<DAGNode> r);
 
    // /**
    //  * @brief Simplify an operation
    //  *
    //  * @param t Operation kind
    //  * @param p Parameters
    //  * @return Simplified operation node
    //  */
    // std::shared_ptr<DAGNode> simp_oper(const NODE_KIND& t, const
    // std::vector<std::shared_ptr<DAGNode>>& p);
 
    std::shared_ptr<DAGNode> rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &p);
 
    std::shared_ptr<DAGNode> rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &r);
 
    std::shared_ptr<DAGNode> rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &m, std::shared_ptr<DAGNode> &r);
 
    std::shared_ptr<DAGNode> rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &ml, std::shared_ptr<DAGNode> &mr, std::shared_ptr<DAGNode> &r);
 
    std::shared_ptr<DAGNode> rewrite(NODE_KIND &t,
                                     std::vector<std::shared_ptr<DAGNode>> &p);
 
    std::shared_ptr<DAGNode>
    rewrite_oper(NODE_KIND &t, std::vector<std::shared_ptr<DAGNode>> &p);
 
    std::unique_ptr<NodeManager> getNodeManager() {
        return std::move(node_manager);
    }
    void rebuild_node_manager() {
        node_manager = std::make_unique<NodeManager>();
    }
    std::shared_ptr<DAGNode>
    mkNode(std::shared_ptr<Sort> sort, NODE_KIND t, std::string name, std::vector<std::shared_ptr<DAGNode>> params) {
        auto result = rewrite_oper(t, params);
        if (isCommutative(t)) {
            if (result != nullptr)
                throw std::runtime_error(
                    "rewrite_oper should return nullptr for commutative operators");
            switch (t) {
                case NODE_KIND::NT_FORALL:
                case NODE_KIND::NT_EXISTS:
                case NODE_KIND::NT_FP_ADD:
                case NODE_KIND::NT_FP_MUL: {
                    std::vector<std::shared_ptr<DAGNode>> nparams(params.begin() + 1,
                                                                  params.end());
                    nparams = sortParams(nparams);
                    nparams.insert(nparams.begin(), params[0]);
                    params = nparams;
                    break;
                }
                default:
                    params = sortParams(params);
                    break;
            }
 
            // result->rep
        }
 
        // auto result = nullptr;
        if (result != nullptr)
            return result;
        else
            return node_manager->createNode(sort, t, name, params);
    }
    static bool isCommutative(NODE_KIND t);
 
    static std::vector<std::shared_ptr<DAGNode>>
    sortParams(const std::vector<std::shared_ptr<DAGNode>> &p);
    // std::shared_ptr<DAGNode> mkNode(std::shared_ptr<Sort> sort, NODE_KIND t,
    // std::string name, std::shared_ptr<Value> value, const
    // std::vector<std::shared_ptr<DAGNode>>& children); mk function
    std::shared_ptr<DAGNode>
    mkFuncDec(const std::string &name,
              const std::vector<std::shared_ptr<Sort>> &params,
              std::shared_ptr<Sort> out_sort);
 
    std::shared_ptr<DAGNode>
    mkFuncDef(const std::string &name,
              const std::vector<std::shared_ptr<DAGNode>> &params,
              std::shared_ptr<Sort> out_sort,
              std::shared_ptr<DAGNode> body);
 
    std::shared_ptr<DAGNode>
    mkFuncRec(const std::string &name,
              const std::vector<std::shared_ptr<DAGNode>> &params,
              std::shared_ptr<Sort> out_sort,
              std::shared_ptr<DAGNode> body);
 
    std::shared_ptr<DAGNode>
    mkApplyRecFunc(std::shared_ptr<DAGNode> fun,
                   const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode>
    mkPattern(const std::shared_ptr<Sort> &sort, const std::string &name, const std::vector<std::shared_ptr<DAGNode>> &params);
    std::shared_ptr<DAGNode> mkNoPattern(const std::shared_ptr<Sort> &sort,
                                         const std::string &name,
                                         std::shared_ptr<DAGNode> param);
    std::shared_ptr<DAGNode> mkWeight(const std::shared_ptr<Sort> &sort,
                                      const std::string &name,
                                      std::shared_ptr<DAGNode> weight);
    std::shared_ptr<DAGNode>
    mkAttribute(const std::shared_ptr<Sort> &sort, const std::string &name, const std::vector<std::shared_ptr<DAGNode>> &params);
    std::shared_ptr<DAGNode>
    mkApplyUF(const std::shared_ptr<Sort> &sort, const std::string &name, const std::vector<std::shared_ptr<DAGNode>> &params);
 
    // mk sort
    std::shared_ptr<Sort> mkSortDec(const std::string &name, const size_t &arity);
 
    std::shared_ptr<Sort>
    mkSortDef(const std::string &name,
              const std::vector<std::shared_ptr<Sort>> &params,
              std::shared_ptr<Sort> out_sort);
 
    // mk special sort
    std::shared_ptr<Sort> mkIntSort();
    std::shared_ptr<Sort> mkRealSort();
    std::shared_ptr<Sort> mkBoolSort();
    std::shared_ptr<Sort> mkStrSort();
    std::shared_ptr<Sort> mkRegSort();
    std::shared_ptr<Sort> mkRoundingModeSort();
    std::shared_ptr<Sort> mkNatSort();
    std::shared_ptr<Sort> mkBVSort(const size_t &width);
    std::shared_ptr<Sort> mkFPSort(const size_t &e, const size_t &s);
    std::shared_ptr<Sort> mkArraySort(std::shared_ptr<Sort> index,
                                      std::shared_ptr<Sort> elem);
 
    // declare var
    std::shared_ptr<DAGNode> declareVar(const std::string &name,
                                        const std::string &sort);
 
    std::shared_ptr<DAGNode> declareVar(const std::string &name,
                                        const std::shared_ptr<Sort> &sort);
 
    // mk true/false
    std::shared_ptr<DAGNode> mkTrue();  // true
 
    std::shared_ptr<DAGNode> mkFalse();  // false
 
    std::shared_ptr<DAGNode> mkUnknown();  // unknown
    // CORE OPERATORS
    std::shared_ptr<DAGNode>
    mkEq(const std::vector<std::shared_ptr<DAGNode>> &params);  // l = r = ...
 
    std::shared_ptr<DAGNode> mkDistinct(
        const std::vector<std::shared_ptr<DAGNode>> &params);  // l != r != ...
 
    // CONST
    std::shared_ptr<DAGNode> mkConstInt(const std::string &v);  // CONST_INT
 
    std::shared_ptr<DAGNode> mkConstInt(const int &v);  // CONST_INT
 
    std::shared_ptr<DAGNode> mkConstInt(const Integer &v);  // CONST_INT
 
    std::shared_ptr<DAGNode> mkConstInt(const Number &v);  // CONST_INT
 
    std::shared_ptr<DAGNode> mkConstReal(const std::string &v);  // CONST_REAL
 
    std::shared_ptr<DAGNode> mkConstReal(const Real &v);  // CONST_REAL
 
    std::shared_ptr<DAGNode> mkConstReal(const double &v);  // CONST_REAL
 
    std::shared_ptr<DAGNode> mkConstReal(const Integer &v);  // CONST_REAL
 
    std::shared_ptr<DAGNode> mkConstReal(const Number &v);  // CONST_REAL
 
    std::shared_ptr<DAGNode> mkConstStr(const std::string &v);  // CONST_Str
 
    std::shared_ptr<DAGNode> mkConstBv(const std::string &v,
                                       const size_t &width);  // CONST_BV
 
    std::shared_ptr<DAGNode> mkConstFp(const std::string &v, const size_t &e,
                                       const size_t &s);  // CONST_FP
 
    std::shared_ptr<DAGNode>
    mkConstFP(const std::string &fp_expr);  // CONST_FP from expression
 
    std::shared_ptr<DAGNode> mkConstReg(const std::string &v);  // CONST_REG
 
    std::shared_ptr<DAGNode>
    mkRoundingMode(const std::string &mode);  // ROUNDING_MODE
 
    std::shared_ptr<DAGNode>
    mkVarRoundingMode(const std::string &name);  // VAR_ROUNDING_MODE
 
    // VAR
    std::shared_ptr<DAGNode> mkVar(const std::shared_ptr<Sort> &sort,
                                   const std::string &name);  // VAR
    std::shared_ptr<DAGNode>
    mkPlaceholderVar(const std::string &name);  // PLACEHOLDER_VAR
 
    std::shared_ptr<DAGNode>
    mkTempVar(const std::shared_ptr<Sort> &sort);  // TEMP_VAR
 
    std::shared_ptr<DAGNode> mkVarBool(const std::string &name);  // VAR_BOOL
 
    std::shared_ptr<DAGNode> mkVarInt(const std::string &name);  // VAR_INT
 
    std::shared_ptr<DAGNode> mkVarReal(const std::string &name);  // VAR_REAL
 
    std::shared_ptr<DAGNode> mkVarBv(const std::string &name,
                                     const size_t &width);  // VAR_BV
 
    std::shared_ptr<DAGNode> mkVarFp(const std::string &name, const size_t &e,
                                     const size_t &s);  // VAR_FP
 
    std::shared_ptr<DAGNode> mkVarStr(const std::string &name);  // VAR_STR
 
    std::shared_ptr<DAGNode> mkVarReg(const std::string &name);  // VAR_REG
 
    std::shared_ptr<DAGNode>
    mkFunParamVar(std::shared_ptr<Sort> sort,
                  const std::string &name);  // FUN_PARAM_VAR
 
    std::shared_ptr<DAGNode> mkArray(const std::string &name,
                                     std::shared_ptr<Sort> index,
                                     std::shared_ptr<Sort> elem);  // ARRAY
 
    std::shared_ptr<DAGNode>
    mkConstArray(std::shared_ptr<Sort> sort,
                 std::shared_ptr<DAGNode> value);  // CONST ARRAY
 
    // BOOLEAN
    std::shared_ptr<DAGNode> mkNot(std::shared_ptr<DAGNode> param);
 
    std::shared_ptr<DAGNode>
    mkAnd(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode>
    mkOr(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode>
    mkImplies(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode>
    mkXor(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode> mkIte(std::shared_ptr<DAGNode> cond,
                                   std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);
 
    std::shared_ptr<DAGNode>
    mkIte(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    // ARITHMATIC COMMON OPERATORS
    std::shared_ptr<DAGNode>
    mkAdd(const std::vector<std::shared_ptr<DAGNode>> &params);  // l + r + ...
 
    std::shared_ptr<DAGNode>
    mkMul(const std::vector<std::shared_ptr<DAGNode>> &params);  // l * r * ...
 
    std::shared_ptr<DAGNode>
    mkIand(const std::vector<std::shared_ptr<DAGNode>> &params);  // l & r & ...
 
    std::shared_ptr<DAGNode> mkPow2(std::shared_ptr<DAGNode> param);  // 2^param
 
    std::shared_ptr<DAGNode> mkPow(std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);  // l^r
 
    std::shared_ptr<DAGNode>
    mkSub(const std::vector<std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode> mkNeg(std::shared_ptr<DAGNode> param);  // -param
 
    std::shared_ptr<DAGNode>
    mkDiv(const std::vector<std::shared_ptr<DAGNode>> &params);  // l / r / ...
 
    std::shared_ptr<DAGNode>
    mkDivInt(const std::vector<std::shared_ptr<DAGNode>> &params);  // l / r / ...
 
    std::shared_ptr<DAGNode>
    mkDivReal(const std::vector<std::shared_ptr<DAGNode>> &params);  // l / r / ...
 
    std::shared_ptr<DAGNode> mkMod(std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkAbs(std::shared_ptr<DAGNode> param);  // |param|
 
    std::shared_ptr<DAGNode>
    mkSqrt(std::shared_ptr<DAGNode> param);  // sqrt(param)
 
    std::shared_ptr<DAGNode>
    mkSafeSqrt(std::shared_ptr<DAGNode> param);  // safeSqrt(param)
 
    std::shared_ptr<DAGNode>
    mkCeil(std::shared_ptr<DAGNode> param);  // ceil(param)
 
    std::shared_ptr<DAGNode>
    mkFloor(std::shared_ptr<DAGNode> param);  // floor(param)
 
    std::shared_ptr<DAGNode>
    mkRound(std::shared_ptr<DAGNode> param);  // round(param)
 
    // TRANSCENDENTAL ARITHMATIC
    std::shared_ptr<DAGNode> mkExp(std::shared_ptr<DAGNode> param);  // exp(param)
 
    std::shared_ptr<DAGNode> mkLn(std::shared_ptr<DAGNode> param);  // ln(param)
 
    std::shared_ptr<DAGNode> mkLg(std::shared_ptr<DAGNode> param);  // lg(param)
 
    std::shared_ptr<DAGNode> mkLb(std::shared_ptr<DAGNode> param);  // lb(param)
 
    std::shared_ptr<DAGNode> mkLog(std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);  // log_l(r)
 
    std::shared_ptr<DAGNode> mkSin(std::shared_ptr<DAGNode> param);  // sin(param)
 
    std::shared_ptr<DAGNode> mkCos(std::shared_ptr<DAGNode> param);  // cos(param)
 
    std::shared_ptr<DAGNode> mkSec(std::shared_ptr<DAGNode> param);  // sec(param)
 
    std::shared_ptr<DAGNode> mkCsc(std::shared_ptr<DAGNode> param);  // csc(param)
 
    std::shared_ptr<DAGNode> mkTan(std::shared_ptr<DAGNode> param);  // tan(param)
 
    std::shared_ptr<DAGNode> mkCot(std::shared_ptr<DAGNode> param);  // cot(param)
 
    std::shared_ptr<DAGNode>
    mkAsin(std::shared_ptr<DAGNode> param);  // asin(param)
 
    std::shared_ptr<DAGNode>
    mkAcos(std::shared_ptr<DAGNode> param);  // acos(param)
 
    std::shared_ptr<DAGNode>
    mkAsec(std::shared_ptr<DAGNode> param);  // asec(param)
 
    std::shared_ptr<DAGNode>
    mkAcsc(std::shared_ptr<DAGNode> param);  // acsc(param)
 
    std::shared_ptr<DAGNode>
    mkAtan(std::shared_ptr<DAGNode> param);  // atan(param)
 
    std::shared_ptr<DAGNode>
    mkAcot(std::shared_ptr<DAGNode> param);  // acot(param)
 
    std::shared_ptr<DAGNode>
    mkSinh(std::shared_ptr<DAGNode> param);  // sinh(param)
 
    std::shared_ptr<DAGNode>
    mkCosh(std::shared_ptr<DAGNode> param);  // cosh(param)
 
    std::shared_ptr<DAGNode>
    mkTanh(std::shared_ptr<DAGNode> param);  // tanh(param)
 
    std::shared_ptr<DAGNode>
    mkSech(std::shared_ptr<DAGNode> param);  // sech(param)
 
    std::shared_ptr<DAGNode>
    mkCsch(std::shared_ptr<DAGNode> param);  // csch(param)
 
    std::shared_ptr<DAGNode>
    mkCoth(std::shared_ptr<DAGNode> param);  // coth(param)
 
    std::shared_ptr<DAGNode>
    mkAsinh(std::shared_ptr<DAGNode> param);  // asinh(param)
 
    std::shared_ptr<DAGNode>
    mkAcosh(std::shared_ptr<DAGNode> param);  // acosh(param)
 
    std::shared_ptr<DAGNode>
    mkAtanh(std::shared_ptr<DAGNode> param);  // atanh(param)
 
    std::shared_ptr<DAGNode>
    mkAsech(std::shared_ptr<DAGNode> param);  // asech(param)
 
    std::shared_ptr<DAGNode>
    mkAcsch(std::shared_ptr<DAGNode> param);  // acsch(param)
 
    std::shared_ptr<DAGNode>
    mkAcoth(std::shared_ptr<DAGNode> param);  // acoth(param)
 
    std::shared_ptr<DAGNode> mkAtan2(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);
    // ARITHMATIC COMP
    std::shared_ptr<DAGNode>
    mkLe(const std::vector<std::shared_ptr<DAGNode>> &params);  // l <= r
 
    std::shared_ptr<DAGNode>
    mkLt(const std::vector<std::shared_ptr<DAGNode>> &params);  // l < r
 
    std::shared_ptr<DAGNode> mkGe(const std::vector<std::shared_ptr<DAGNode>>
                                      &params);  // l >= r >= ... >= s
 
    std::shared_ptr<DAGNode>
    mkGt(const std::vector<std::shared_ptr<DAGNode>> &params);  // l > r > ... > s
 
    // ARITHMATIC CONVERSION
 
    std::shared_ptr<DAGNode>
    mkToInt(std::shared_ptr<DAGNode> param);  // to_int(param)
 
    std::shared_ptr<DAGNode>
    mkToReal(std::shared_ptr<DAGNode> param);  // to_real(param)
 
    // ARITHMATIC PROPERTIES
    std::shared_ptr<DAGNode>
    mkIsInt(std::shared_ptr<DAGNode> param);  // is_int(param)
 
    std::shared_ptr<DAGNode>
    mkIsDivisible(std::shared_ptr<DAGNode> l,
                  std::shared_ptr<DAGNode> r);  // is_divisible(l, r)
 
    std::shared_ptr<DAGNode>
    mkIsPrime(std::shared_ptr<DAGNode> param);  // is_prime(param)
 
    std::shared_ptr<DAGNode>
    mkIsEven(std::shared_ptr<DAGNode> param);  // is_even(param)
 
    std::shared_ptr<DAGNode>
    mkIsOdd(std::shared_ptr<DAGNode> param);  // is_odd(param)
 
    // ARITHMATIC CONSTANTS
 
    std::shared_ptr<DAGNode> mkPi();  // pi
 
    std::shared_ptr<DAGNode> mkE();  // e
 
    std::shared_ptr<DAGNode> mkInfinity(std::shared_ptr<Sort> sort);  // infinity
 
    std::shared_ptr<DAGNode>
    mkPosInfinity(std::shared_ptr<Sort> sort = nullptr);  // +infinity
 
    std::shared_ptr<DAGNode>
    mkNegInfinity(std::shared_ptr<Sort> sort = nullptr);  // -infinity
 
    std::shared_ptr<DAGNode> mkNaN(std::shared_ptr<Sort> sort = nullptr);  // nan
 
    std::shared_ptr<DAGNode> mkEpsilon();  // epsilon
 
    std::shared_ptr<DAGNode> mkPosEpsilon();  // +epsilon
 
    std::shared_ptr<DAGNode> mkNegEpsilon();  // -epsilon
 
    // ARITHMATIC FUNCTIONS
 
    std::shared_ptr<DAGNode> mkGcd(std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);  // gcd(l, r)
 
    std::shared_ptr<DAGNode> mkLcm(std::shared_ptr<DAGNode> l,
                                   std::shared_ptr<DAGNode> r);  // lcm(l, r)
 
    std::shared_ptr<DAGNode>
    mkFact(std::shared_ptr<DAGNode> param);  // factorial(param)
 
    // BITVECTOR COMMON OPERATORS
    std::shared_ptr<DAGNode> mkBvNot(std::shared_ptr<DAGNode> param);  // ~param
 
    std::shared_ptr<DAGNode>
    mkBvAnd(const std::vector<std::shared_ptr<DAGNode>> &params);  // l & r & ...
 
    std::shared_ptr<DAGNode>
    mkBvOr(const std::vector<std::shared_ptr<DAGNode>> &params);  // l | r | ...
 
    std::shared_ptr<DAGNode>
    mkBvXor(const std::vector<std::shared_ptr<DAGNode>> &params);  // l ^ r ^ ...
 
    std::shared_ptr<DAGNode>
    mkBvNand(std::shared_ptr<DAGNode> l,
             std::shared_ptr<DAGNode> r);  // ~(l & r & ...)
 
    std::shared_ptr<DAGNode>
    mkBvNor(std::shared_ptr<DAGNode> l,
            std::shared_ptr<DAGNode> r);  // ~(l | r | ...)
 
    std::shared_ptr<DAGNode>
    mkBvComp(const std::vector<std::shared_ptr<DAGNode>> &params);  // l = r
 
    std::shared_ptr<DAGNode>
    mkBvXnor(std::shared_ptr<DAGNode> l,
             std::shared_ptr<DAGNode> r);  // ~(l ^ r ^ ...)
 
    std::shared_ptr<DAGNode> mkBvNeg(std::shared_ptr<DAGNode> param);  // -param
 
    std::shared_ptr<DAGNode>
    mkBvAdd(const std::vector<std::shared_ptr<DAGNode>> &params);  // l + r + ...
 
    std::shared_ptr<DAGNode> mkBvSub(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l - r - ...
 
    std::shared_ptr<DAGNode>
    mkBvMul(const std::vector<std::shared_ptr<DAGNode>> &params);  // l * r * ...
 
    std::shared_ptr<DAGNode> mkBvUdiv(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l / r
 
    std::shared_ptr<DAGNode> mkBvUrem(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkBvUmod(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkBvSdiv(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l / r
 
    std::shared_ptr<DAGNode> mkBvSrem(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkBvSmod(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkBvShl(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l << r
 
    std::shared_ptr<DAGNode> mkBvLshr(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l >> r
 
    std::shared_ptr<DAGNode> mkBvAshr(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l >> r
 
    std::shared_ptr<DAGNode> mkBvConcat(
        const std::vector<std::shared_ptr<DAGNode>> &params);  // l ++ r ++ ...
 
    std::shared_ptr<DAGNode> mkBvExtract(std::shared_ptr<DAGNode> l,
                                         std::shared_ptr<DAGNode> r,
                                         std::shared_ptr<DAGNode> s);  // l[r:s]
 
    std::shared_ptr<DAGNode> mkBvRepeat(std::shared_ptr<DAGNode> l,
                                        std::shared_ptr<DAGNode> r);  // l * r
 
    std::shared_ptr<DAGNode>
    mkBvZeroExt(std::shared_ptr<DAGNode> l,
                std::shared_ptr<DAGNode> r);  // l zero_extend r
 
    std::shared_ptr<DAGNode>
    mkBvSignExt(std::shared_ptr<DAGNode> l,
                std::shared_ptr<DAGNode> r);  // l sign_extend r
 
    std::shared_ptr<DAGNode>
    mkBvRotateLeft(std::shared_ptr<DAGNode> l,
                   std::shared_ptr<DAGNode> r);  // l <<< r
 
    std::shared_ptr<DAGNode>
    mkBvRotateRight(std::shared_ptr<DAGNode> l,
                    std::shared_ptr<DAGNode> r);  // l >>> r
 
    // BITVECTOR COMP
    std::shared_ptr<DAGNode> mkBvUlt(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l < r
 
    std::shared_ptr<DAGNode> mkBvUle(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l <= r
 
    std::shared_ptr<DAGNode> mkBvUgt(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l > r
 
    std::shared_ptr<DAGNode> mkBvUge(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l >= r
 
    std::shared_ptr<DAGNode> mkBvSlt(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l < r
 
    std::shared_ptr<DAGNode> mkBvSle(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l <= r
 
    std::shared_ptr<DAGNode> mkBvSgt(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l > r
 
    std::shared_ptr<DAGNode> mkBvSge(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l >= r
 
    // BITVECTOR CONVERSION
    std::shared_ptr<DAGNode>
    mkBvToNat(std::shared_ptr<DAGNode> param);  // to_nat(param)
 
    std::shared_ptr<DAGNode>
    mkNatToBv(std::shared_ptr<DAGNode> param,
              std::shared_ptr<DAGNode> width);  // to_bv(param, width)
 
    std::shared_ptr<DAGNode>
    mkBvToInt(std::shared_ptr<DAGNode> param);  // to_int(param)
    std::shared_ptr<DAGNode> mkUbvToInt(std::shared_ptr<DAGNode> param);
    std::shared_ptr<DAGNode> mkSbvToInt(std::shared_ptr<DAGNode> param);
 
    std::shared_ptr<DAGNode>
    mkIntToBv(std::shared_ptr<DAGNode> param,
              std::shared_ptr<DAGNode> width);  // to_bv(param, width)
 
    // FLOATING POINT COMMON OPERATORS
    std::shared_ptr<DAGNode>
    mkFpAdd(const std::vector<std::shared_ptr<DAGNode>> &params);  // l + r + ...
 
    std::shared_ptr<DAGNode>
    mkFpSub(const std::vector<std::shared_ptr<DAGNode>> &params);  // l - r - ...
 
    std::shared_ptr<DAGNode>
    mkFpMul(const std::vector<std::shared_ptr<DAGNode>> &params);  // l * r * ...
 
    std::shared_ptr<DAGNode>
    mkFpDiv(const std::vector<std::shared_ptr<DAGNode>> &params);  // l / r / ...
 
    std::shared_ptr<DAGNode> mkFpAbs(std::shared_ptr<DAGNode> param);  // |param|
 
    std::shared_ptr<DAGNode> mkFpNeg(std::shared_ptr<DAGNode> param);  // -param
 
    std::shared_ptr<DAGNode> mkFpRem(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r);  // l % r
 
    std::shared_ptr<DAGNode> mkFpFma(const std::vector<std::shared_ptr<DAGNode>>
                                         &params);  // fma(a, b, c) = a * b + c
 
    std::shared_ptr<DAGNode>
    mkFpSqrt(std::shared_ptr<DAGNode> rm,
             std::shared_ptr<DAGNode> param);  // sqrt(rm, param)
    std::shared_ptr<DAGNode>
    mkFpSqrt(std::shared_ptr<DAGNode> param);  // sqrt(param)
 
    std::shared_ptr<DAGNode> mkFpRoundToIntegral(
        std::shared_ptr<DAGNode> rm,
        std::shared_ptr<DAGNode> param);  // round_to_integral(rm, param)
    std::shared_ptr<DAGNode> mkFpRoundToIntegral(
        std::shared_ptr<DAGNode> param);  // round_to_integral(param)
 
    std::shared_ptr<DAGNode>
    mkFpMin(std::shared_ptr<DAGNode> l,
            std::shared_ptr<DAGNode> r);  // fp.min(params)
 
    std::shared_ptr<DAGNode>
    mkFpMax(std::shared_ptr<DAGNode> l,
            std::shared_ptr<DAGNode> r);  // fp.max(params)
 
    // FLOATING POINT COMP
    std::shared_ptr<DAGNode>
    mkFpLe(const std::vector<std::shared_ptr<DAGNode>> &params);  // l <= r
 
    std::shared_ptr<DAGNode>
    mkFpLt(const std::vector<std::shared_ptr<DAGNode>> &params);  // l < r
 
    std::shared_ptr<DAGNode>
    mkFpGe(const std::vector<std::shared_ptr<DAGNode>> &params);  // l >= r
 
    std::shared_ptr<DAGNode>
    mkFpGt(const std::vector<std::shared_ptr<DAGNode>> &params);  // l > r
 
    std::shared_ptr<DAGNode>
    mkFpEq(const std::vector<std::shared_ptr<DAGNode>> &params);  // l = r
 
    // FLOATING POINT CONVERSION
    std::shared_ptr<DAGNode>
    mkFpToUbv(std::shared_ptr<DAGNode> rm, std::shared_ptr<DAGNode> param,
              std::shared_ptr<DAGNode> size);  // to_ubv(rm, param, size)
 
    std::shared_ptr<DAGNode>
    mkFpToSbv(std::shared_ptr<DAGNode> rm, std::shared_ptr<DAGNode> param,
              std::shared_ptr<DAGNode> size);  // to_sbv(rm, param, size)
 
    std::shared_ptr<DAGNode>
    mkFpToReal(std::shared_ptr<DAGNode> param);  // to_real(param)
 
    std::shared_ptr<DAGNode>
    mkToFp(std::shared_ptr<DAGNode> eb, std::shared_ptr<DAGNode> sb, std::shared_ptr<DAGNode> rm,
           std::shared_ptr<DAGNode> param);  // to_fp(eb, sb, rm, param)
    std::shared_ptr<DAGNode>
    mkToFp(std::shared_ptr<DAGNode> eb, std::shared_ptr<DAGNode> sb,
           std::shared_ptr<DAGNode> param);  // to_fp(eb, sb, param)
    std::shared_ptr<DAGNode> mkToFpUnsigned(
        std::shared_ptr<DAGNode> eb, std::shared_ptr<DAGNode> sb, std::shared_ptr<DAGNode> rm,
        std::shared_ptr<DAGNode> param);  // to_fp_unsigned(eb, sb, rm, param)
    std::shared_ptr<DAGNode>
    mkFpConst(std::shared_ptr<DAGNode> sign, std::shared_ptr<DAGNode> exp,
              std::shared_ptr<DAGNode> mant);  // fp(sign, exp, mant)
 
    // ROOT OBJECT
    std::shared_ptr<DAGNode> mkRootObj(std::shared_ptr<DAGNode> expr,
                                       int index);  // root-obj(expr, index)
    std::shared_ptr<DAGNode> mkRootOfWithInterval(
        const std::vector<std::shared_ptr<DAGNode>> &coeffs,
        std::shared_ptr<DAGNode> lower_bound,
        std::shared_ptr<DAGNode> upper_bound);  // root-of-with-interval(coeffs,
                                                // lower_bound, upper_bound)
 
    // FLOATING POINT PROPERTIES
    std::shared_ptr<DAGNode>
    mkFpIsNormal(std::shared_ptr<DAGNode> param);  // is_normal(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsSubnormal(std::shared_ptr<DAGNode> param);  // is_subnormal(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsZero(std::shared_ptr<DAGNode> param);  // is_zero(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsInf(std::shared_ptr<DAGNode> param);  // is_inf(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsNaN(std::shared_ptr<DAGNode> param);  // is_nan(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsNeg(std::shared_ptr<DAGNode> param);  // is_neg(param)
 
    std::shared_ptr<DAGNode>
    mkFpIsPos(std::shared_ptr<DAGNode> param);  // is_pos(param)
 
    // ARRAY
    std::shared_ptr<DAGNode> mkSelect(std::shared_ptr<DAGNode> l,
                                      std::shared_ptr<DAGNode> r);  // l[r]
 
    std::shared_ptr<DAGNode> mkStore(std::shared_ptr<DAGNode> l,
                                     std::shared_ptr<DAGNode> r,
                                     std::shared_ptr<DAGNode> v);  // l[r] = v
 
    // STRINGS COMMON OPERATORS
    std::shared_ptr<DAGNode>
    mkStrLen(std::shared_ptr<DAGNode> param);  // str.len(param)
 
    std::shared_ptr<DAGNode>
    mkStrConcat(const std::vector<std::shared_ptr<DAGNode>>
                    &params);  // str.++(param1, param2, ...)
 
    std::shared_ptr<DAGNode>
    mkStrSubstr(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                std::shared_ptr<DAGNode> s);  // str.substr(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrPrefixof(std::shared_ptr<DAGNode> l,
                  std::shared_ptr<DAGNode> r);  // str.prefixof(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrSuffixof(std::shared_ptr<DAGNode> l,
                  std::shared_ptr<DAGNode> r);  // str.suffixof(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrIndexof(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                 std::shared_ptr<DAGNode> s);  // str.indexof(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrCharat(std::shared_ptr<DAGNode> l,
                std::shared_ptr<DAGNode> r);  // str.charAt(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrUpdate(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                std::shared_ptr<DAGNode> v);  // str.update(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkStrReplace(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                 std::shared_ptr<DAGNode> v);  // str.replace(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkStrReplaceAll(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                    std::shared_ptr<DAGNode> v);  // str.replace_all(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkStrReplaceReg(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                    std::shared_ptr<DAGNode> v);  // str.replace_re(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkStrReplaceRegAll(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                       std::shared_ptr<DAGNode> v);  // str.replace_re_all(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkStrIndexofReg(std::shared_ptr<DAGNode> l,
                    std::shared_ptr<DAGNode> r);  // str.indexof_re(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrToLower(std::shared_ptr<DAGNode> param);  // str.to_lower(param)
 
    std::shared_ptr<DAGNode>
    mkStrToUpper(std::shared_ptr<DAGNode> param);  // str.to_upper(param)
 
    std::shared_ptr<DAGNode>
    mkStrRev(std::shared_ptr<DAGNode> param);  // str.rev(param)
 
    std::shared_ptr<DAGNode>
    mkStrSplit(std::shared_ptr<DAGNode> l,
               std::shared_ptr<DAGNode> r);  // str.split(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrSplitAt(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                 std::shared_ptr<DAGNode> s);  // str.split_at(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrSplitRest(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                   std::shared_ptr<DAGNode> s);  // str.split_rest(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrNumSplits(std::shared_ptr<DAGNode> l,
                   std::shared_ptr<DAGNode> r);  // str.num_splits(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrSplitAtRe(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                   std::shared_ptr<DAGNode> s);  // str.split_at_re(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrSplitRestRe(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                     std::shared_ptr<DAGNode> s);  // str.split_rest_re(l, r, s)
 
    std::shared_ptr<DAGNode>
    mkStrNumSplitsRe(std::shared_ptr<DAGNode> l,
                     std::shared_ptr<DAGNode> r);  // str.num_splits_re(l, r)
 
    // STRINGS COMP
    std::shared_ptr<DAGNode>
    mkStrLt(const std::vector<std::shared_ptr<DAGNode>> &params);  // str.<(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrLe(const std::vector<std::shared_ptr<DAGNode>> &params);  // str.<=(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrGt(const std::vector<std::shared_ptr<DAGNode>> &params);  // str.>(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrGe(const std::vector<std::shared_ptr<DAGNode>> &params);  // str.>=(l, r)
 
    // STRINGS PROPERTIES
    std::shared_ptr<DAGNode>
    mkStrInReg(std::shared_ptr<DAGNode> l,
               std::shared_ptr<DAGNode> r);  // str.in_re(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrContains(std::shared_ptr<DAGNode> l,
                  std::shared_ptr<DAGNode> r);  // str.contains(l, r)
 
    std::shared_ptr<DAGNode>
    mkStrIsDigit(std::shared_ptr<DAGNode> param);  // str.is_digit(param)
 
    // STRINGS CONVERSION
    std::shared_ptr<DAGNode>
    mkStrFromInt(std::shared_ptr<DAGNode> param);  // str.from_int(param)
 
    std::shared_ptr<DAGNode>
    mkStrToInt(std::shared_ptr<DAGNode> param);  // str.to_int(param)
 
    std::shared_ptr<DAGNode>
    mkStrToReg(std::shared_ptr<DAGNode> param);  // str.to_reg(param)
 
    std::shared_ptr<DAGNode>
    mkStrToCode(std::shared_ptr<DAGNode> param);  // str.to_code(param) assci code
 
    std::shared_ptr<DAGNode> mkStrFromCode(
        std::shared_ptr<DAGNode> param);  // str.from_code(param) assci code
 
    // STRINGS RE CONSTANTS
    std::shared_ptr<DAGNode> mkRegNone();  // re.none
 
    std::shared_ptr<DAGNode> mkRegAll();  // re.all
 
    std::shared_ptr<DAGNode> mkRegAllChar();  // re.allchar
 
    // STRINGS RE COMMON OPERATORS
    std::shared_ptr<DAGNode> mkRegConcat(
        const std::vector<std::shared_ptr<DAGNode>> &params);  // re.++(l, r, ...)
 
    std::shared_ptr<DAGNode>
    mkRegUnion(const std::vector<std::shared_ptr<DAGNode>>
                   &params);  // re.union(l, r, ...)
 
    std::shared_ptr<DAGNode>
    mkRegInter(const std::vector<std::shared_ptr<DAGNode>>
                   &params);  // re.inter(l, r, ...)
 
    std::shared_ptr<DAGNode> mkRegDiff(const std::vector<std::shared_ptr<DAGNode>>
                                           &params);  // re.diff(l, r, ...)
 
    std::shared_ptr<DAGNode>
    mkRegStar(std::shared_ptr<DAGNode> param);  // re.*(param)
 
    std::shared_ptr<DAGNode> mkRegPlus(std::shared_ptr<DAGNode> param);  // param+
 
    std::shared_ptr<DAGNode> mkRegOpt(std::shared_ptr<DAGNode> param);  // param?
 
    std::shared_ptr<DAGNode> mkRegRange(std::shared_ptr<DAGNode> l,
                                        std::shared_ptr<DAGNode> r);  // l..r
 
    std::shared_ptr<DAGNode>
    mkRegRepeat(std::shared_ptr<DAGNode> l,
                std::shared_ptr<DAGNode> r);  // re.^(n, l)
 
    std::shared_ptr<DAGNode> mkRegLoop(std::shared_ptr<DAGNode> l,
                                       std::shared_ptr<DAGNode> r,
                                       std::shared_ptr<DAGNode> s);  // l{r,s}
 
    std::shared_ptr<DAGNode>
    mkRegComplement(std::shared_ptr<DAGNode> param);  // ~param
 
    // STRINGS RE FUNCTIONS
    std::shared_ptr<DAGNode>
    mkReplaceReg(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                 std::shared_ptr<DAGNode> v);  // replace(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkReplaceRegAll(std::shared_ptr<DAGNode> l, std::shared_ptr<DAGNode> r,
                    std::shared_ptr<DAGNode> v);  // replace_all(l, r, v)
 
    std::shared_ptr<DAGNode>
    mkIndexofReg(std::shared_ptr<DAGNode> l,
                 std::shared_ptr<DAGNode> r);  // indexof(l, r)
 
    // INTERVAL
    std::shared_ptr<DAGNode> mkMax(
        const std::vector<std::shared_ptr<DAGNode>> &params);  // max(p1, p2, ...)
 
    std::shared_ptr<DAGNode> mkMin(
        const std::vector<std::shared_ptr<DAGNode>> &params);  // min(p1, p2, ...)
 
    // LET
    std::shared_ptr<DAGNode>
    mkLet(const std::vector<std::shared_ptr<DAGNode>>
              &params);  // let((key1, val1), (key2, val2), ...)
 
    // QUANTIFIERS
    std::shared_ptr<DAGNode> mkQuantVar(const std::string &name,
                                        std::shared_ptr<Sort> sort);
 
    std::shared_ptr<DAGNode>
    mkForall(const std::vector<std::shared_ptr<DAGNode>>
                 &params);  // forall((var1, sort1), (var2, sort2), ..., body)
 
    std::shared_ptr<DAGNode>
    mkExists(const std::vector<std::shared_ptr<DAGNode>>
                 &params);  // exists((var1, sort1), (var2, sort2), ..., body)
 
    // FUNCTION
    std::shared_ptr<DAGNode>
    mkApplyFunc(std::shared_ptr<DAGNode> fun,
                const std::vector<std::shared_ptr<DAGNode>>
                    &params);  // static apply function, only (f p1 p2 ... pn)
                               // without substitution
 
    // parse smt-lib2 file
    bool parseSmtlib2File(const std::string filename);
 
    int getArity(NODE_KIND k) const;
 
    // aux functions
    NODE_KIND getAddOp(std::shared_ptr<Sort> sort);  // mk unique add
 
    NODE_KIND getNegatedKind(NODE_KIND kind);
 
    std::shared_ptr<DAGNode>
    getZero(std::shared_ptr<Sort> sort);  // mk unique zero
 
    // additional functions
    std::shared_ptr<DAGNode>
    substitute(std::shared_ptr<DAGNode> expr,
               std::unordered_map<std::string, std::shared_ptr<DAGNode>> &params);
 
    // apply function
    std::shared_ptr<DAGNode>
    applyFun(std::shared_ptr<DAGNode> fun,
             const std::vector<std::shared_ptr<DAGNode>> &params);
 
    // evaluate: return true if the evaluation has changed the expression
    void setEvaluatePrecision(mpfr_prec_t precision);
 
    mpfr_prec_t getEvaluatePrecision() const;
 
    void setEvaluateUseFloating(bool use_floating);
 
    bool getEvaluateUseFloating() const;
 
    // type conversion
    Real toReal(std::shared_ptr<DAGNode> expr);
 
    Integer toInt(std::shared_ptr<DAGNode> expr);
 
    bool isZero(std::shared_ptr<DAGNode> expr);
 
    bool isOne(std::shared_ptr<DAGNode> expr);
 
    bool isOnes(std::shared_ptr<DAGNode> expr);
 
    // Format conversion
    std::shared_ptr<DAGNode> expandLet(std::shared_ptr<DAGNode> expr);
 
    std::vector<std::shared_ptr<DAGNode>> getSplitLemmas();
 
    std::shared_ptr<DAGNode>
    remove(std::shared_ptr<DAGNode> expr,
           const std::unordered_set<std::shared_ptr<DAGNode>> &nodes);
 
    std::shared_ptr<DAGNode> rename(std::shared_ptr<DAGNode> expr,
                                    const std::string &new_name);
 
    // print
    std::string toString(std::shared_ptr<DAGNode> expr);
 
    std::string toString(const NODE_KIND &kind);
 
    std::string toString(std::shared_ptr<Sort> sort);
 
    std::string optionToString();
 
    std::string dumpSMT2();
 
    std::string dumpSMT2(const std::string &filename);
 
    // Create a datatype function application (constructors/selectors)
    std::shared_ptr<DAGNode>
    mkApplyDTFun(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);
 
    void ensureNumberValue(std::shared_ptr<DAGNode> expr);
 
  private:
    // parse smt-lib2 file
    std::string getSymbol();
    void scanToNextSymbol();
    void parseLpar();
    void parseRpar();
    void skipToRpar();
    std::string peekSymbol();
 
    CMD_TYPE parseCommand();
    KEYWORD parseKeyword();
    std::shared_ptr<Sort> parseSort();
    std::shared_ptr<DAGNode> parseExpr();
    std::shared_ptr<DAGNode> parseConstFunc(const std::string &s);
    std::shared_ptr<DAGNode>
    parseOper(const std::string &s,
              const std::vector<std::shared_ptr<DAGNode>> &func_args,
              const std::vector<std::shared_ptr<DAGNode>> &oper_params);
    std::vector<std::shared_ptr<DAGNode>> parseParams();
    std::shared_ptr<DAGNode> parsePreservingLet();
    std::shared_ptr<DAGNode> parseLet();
    std::shared_ptr<DAGNode> mkLetBindVar(const std::string &name,
                                          const std::shared_ptr<DAGNode> &expr);
    std::shared_ptr<DAGNode>
    mkLetBindVarList(const std::vector<std::shared_ptr<DAGNode>> &bind_vars);
    std::shared_ptr<DAGNode>
    mkLetChain(const std::vector<std::shared_ptr<DAGNode>> &bind_var_lists,
               const std::shared_ptr<DAGNode> &body);
    std::string parseGroup();
    std::string parseWeight();
    std::shared_ptr<DAGNode> parseQuant(const std::string &type);
 
    KEYWORD attemptParseKeywords();
 
    // auxilary functions
 
    std::shared_ptr<DAGNode>
    mkInternalOper(const std::shared_ptr<Sort> &sort, const NODE_KIND &t, const std::vector<std::shared_ptr<DAGNode>> &p);
 
    std::shared_ptr<DAGNode> bindLetVar(const std::string &key,
                                        std::shared_ptr<DAGNode> expr);
    std::shared_ptr<DAGNode> bindFunVar(const std::string &key,
                                        std::shared_ptr<DAGNode> expr);
    // conversion
    std::shared_ptr<DAGNode> 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);
    std::shared_ptr<DAGNode> applyFunPostOrder(
        std::shared_ptr<DAGNode> node,
        std::unordered_map<std::string, std::shared_ptr<DAGNode>> &params);
 
    std::shared_ptr<DAGNode> replaceAtoms(
        std::shared_ptr<DAGNode> expr,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &atom_map,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &visited,
        bool &is_changed);
    std::shared_ptr<DAGNode> replaceNodes(
        std::shared_ptr<DAGNode> expr,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &node_map,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &visited,
        bool &is_changed);
    std::shared_ptr<DAGNode> toCNF(std::shared_ptr<DAGNode> expr);
    std::shared_ptr<DAGNode> toTseitinCNF(
        std::shared_ptr<DAGNode> expr,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &visited,
        std::vector<std::shared_ptr<DAGNode>> &clauses);
    std::shared_ptr<DAGNode>
    toTseitinXor(std::shared_ptr<DAGNode> a, std::shared_ptr<DAGNode> b, std::vector<std::shared_ptr<DAGNode>> &clauses);
    std::shared_ptr<DAGNode>
    toTseitinEq(std::shared_ptr<DAGNode> a, std::shared_ptr<DAGNode> b, std::vector<std::shared_ptr<DAGNode>> &clauses);
    std::shared_ptr<DAGNode>
    toTseitinDistinct(std::shared_ptr<DAGNode> a, std::shared_ptr<DAGNode> b, std::vector<std::shared_ptr<DAGNode>> &clauses);
    std::shared_ptr<DAGNode> toDNFEliminateAll(std::shared_ptr<DAGNode> expr);
    std::shared_ptr<DAGNode> toDNFEliminateAll(
        std::shared_ptr<DAGNode> expr,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &visited,
        bool &is_changed);
    std::shared_ptr<DAGNode>
    toDNFEliminateXOR(const std::vector<std::shared_ptr<DAGNode>> &children);
    std::shared_ptr<DAGNode>
    toDNFEliminateEq(const std::vector<std::shared_ptr<DAGNode>> &children);
    std::shared_ptr<DAGNode>
    toDNFEliminateDistinct(const std::vector<std::shared_ptr<DAGNode>> &children);
 
    std::shared_ptr<DAGNode>
    applyDNFDistributiveLaw(std::shared_ptr<DAGNode> expr);
    std::shared_ptr<DAGNode> applyDNFDistributiveLawRec(
        std::shared_ptr<DAGNode> expr,
        std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
            &visited);
    std::shared_ptr<DAGNode> flattenDNF(std::shared_ptr<DAGNode> expr);
 
    std::shared_ptr<DAGNode> toNNF(std::shared_ptr<DAGNode> expr, bool is_not);
 
    std::shared_ptr<DAGNode>
    remove(std::shared_ptr<DAGNode> expr,
           const std::unordered_set<std::shared_ptr<DAGNode>> &nodes,
           std::unordered_map<std::shared_ptr<DAGNode>, std::shared_ptr<DAGNode>>
               &visited);
 
    // errors & warnings
    //  mk errror node
    std::shared_ptr<DAGNode> mkErr(const ERROR_TYPE t);
    // error/warning information
    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;
 
    // collect atoms
    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);
};
 
// smart pointer
typedef std::shared_ptr<Parser> ParserPtr;
ParserPtr newParser();
ParserPtr newParser(const std::string &filename);
}  // namespace stabilizer::parser
#endif