z3-src 503.2.1

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    arith_decl_plugin.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-01-09

Revision History:

--*/
#pragma once

#include "ast/ast.h"
class sexpr;

namespace algebraic_numbers {
    class anum;
    class manager;
}

enum arith_sort_kind {
    REAL_SORT,
    INT_SORT,
    COMPLEX_SORT
};

enum arith_op_kind {
    OP_NUM, // rational & integers
    OP_IRRATIONAL_ALGEBRAIC_NUM,  // irrationals that are roots of polynomials with integer coefficients
    //
    OP_LE,
    OP_GE,
    OP_LT,
    OP_GT,
    OP_ADD,
    OP_SUB,
    OP_UMINUS,
    OP_MUL,
    OP_DIV,
    OP_IDIV,
    OP_DIV0,
    OP_IDIV0,
    OP_IDIVIDES,
    OP_REM,
    OP_MOD,
    OP_MOD0,
    OP_TO_REAL,
    OP_TO_INT,
    OP_IS_INT,
    OP_ABS,
    OP_POWER,
    OP_POWER0,
    // hyperbolic and trigonometric functions
    OP_SIN,
    OP_COS,
    OP_TAN,
    OP_ASIN,
    OP_ACOS,
    OP_ATAN,
    OP_SINH,
    OP_COSH,
    OP_TANH,
    OP_ASINH,
    OP_ACOSH,
    OP_ATANH,
    OP_EXP,
    OP_ATAN2,
    OP_LOG,
    // Bit-vector functions
    OP_ARITH_BAND,
    OP_ARITH_SHL,
    OP_ARITH_ASHR,
    OP_ARITH_LSHR,
    // constants
    OP_PI,
    OP_E,
    // under-specified symbols
    OP_NEG_ROOT,      // x^n when n is even and x is negative
    OP_U_ASIN,        // asin(x) for x < -1 or x > 1
    OP_U_ACOS,        // acos(x) for x < -1 or x > 1
    OP_COMPLEX,
    OP_REAL_PART,
    OP_IMAG_PART,
    LAST_ARITH_OP
};

class arith_util;

class arith_decl_plugin : public decl_plugin {
protected:
    struct algebraic_numbers_wrapper;
    algebraic_numbers_wrapper * m_aw;
    symbol      m_intv_sym;
    symbol      m_realv_sym;
    symbol      m_rootv_sym;
    sort *      m_real_decl;
    sort *      m_int_decl;
    sort *      m_complex_decl = nullptr;
    func_decl * m_c_add_decl = nullptr;
    func_decl * m_c_sub_decl = nullptr;
    func_decl * m_c_uminus_decl = nullptr;
    func_decl * m_c_mul_decl = nullptr;
    func_decl * m_rc_mul_decl = nullptr;
    func_decl * m_cr_mul_decl = nullptr;
    func_decl * m_c_div_decl = nullptr;
    func_decl * m_complex_ctor = nullptr;
    func_decl * m_real_part_decl = nullptr;
    func_decl * m_imag_part_decl = nullptr;
    func_decl * m_r_le_decl;
    func_decl * m_r_ge_decl;
    func_decl * m_r_lt_decl;
    func_decl * m_r_gt_decl;

    func_decl * m_r_add_decl;
    func_decl * m_r_sub_decl;
    func_decl * m_r_uminus_decl;
    func_decl * m_r_mul_decl;
    func_decl * m_r_div_decl;

    func_decl * m_i_le_decl;
    func_decl * m_i_ge_decl;
    func_decl * m_i_lt_decl;
    func_decl * m_i_gt_decl;

    func_decl * m_i_add_decl;
    func_decl * m_i_sub_decl;
    func_decl * m_i_uminus_decl;
    func_decl * m_i_mul_decl;
    func_decl * m_i_div_decl;
    func_decl * m_i_mod_decl;
    func_decl * m_i_rem_decl;

    func_decl * m_to_real_decl = nullptr;
    func_decl * m_to_int_decl = nullptr;
    func_decl * m_r_to_real_decl = nullptr;
    func_decl * m_i_to_int_decl = nullptr;
    func_decl * m_is_int_decl = nullptr;
    func_decl * m_r_power_decl = nullptr;
    func_decl * m_i_power_decl = nullptr;

    func_decl * m_r_abs_decl;
    func_decl * m_i_abs_decl;

    func_decl * m_sin_decl;
    func_decl * m_cos_decl;
    func_decl * m_tan_decl;
    func_decl * m_asin_decl;
    func_decl * m_acos_decl;
    func_decl * m_atan_decl;
    func_decl * m_sinh_decl;
    func_decl * m_cosh_decl;
    func_decl * m_tanh_decl;
    func_decl * m_asinh_decl;
    func_decl * m_acosh_decl;
    func_decl * m_atanh_decl;
    func_decl * m_exp_decl;
    func_decl * m_atan2_decl;
    func_decl * m_log_decl;

    app       * m_pi;
    app       * m_e;

    func_decl * m_neg_root_decl;
    func_decl * m_u_asin_decl;
    func_decl * m_u_acos_decl;
    ptr_vector<app> m_small_ints;
    ptr_vector<app> m_small_reals;

    bool        m_convert_int_numerals_to_real;

    symbol bv_symbol(decl_kind k) const;

    func_decl * mk_func_decl(decl_kind k, bool is_real);
    func_decl * mk_complex_func_decl(decl_kind k);
    void set_manager(ast_manager * m, family_id id) override;
    decl_kind fix_kind(decl_kind k, unsigned arity);
    void check_arity(unsigned arity, unsigned expected_arity);
    func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);

public:
    arith_decl_plugin();

    ~arith_decl_plugin() override;
    void finalize() override;

    algebraic_numbers::manager & am() const;
    algebraic_numbers_wrapper & aw() const;

    void del(parameter const & p) override;
    parameter translate(parameter const & p, decl_plugin & target) override;

    decl_plugin * mk_fresh() override {
        return alloc(arith_decl_plugin);
    }

    bool convert_int_numerals_to_real() const { return m_convert_int_numerals_to_real; }

    sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;

    func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                             unsigned arity, sort * const * domain, sort * range) override;

    func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                             unsigned num_args, expr * const * args, sort * range) override;

    bool is_value(app * e) const override;

    bool is_unique_value(app * e) const override;

    bool are_equal(app * a, app * b) const override;

    bool are_distinct(app * a, app * b) const override;

    void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;

    void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;

    app * mk_numeral(rational const & n, bool is_int);

    app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int);

    // Create a (real) numeral that is the i-th root of the polynomial encoded using the given sexpr.
    app * mk_numeral(sexpr const * p, unsigned i);

    app * mk_pi() const { return m_pi; }

    app * mk_e() const { return m_e; }

    expr * get_some_value(sort * s) override;

    bool is_considered_uninterpreted(func_decl * f) override {
        if (f->get_family_id() != get_family_id())
            return false;
        switch (f->get_decl_kind())
        {
        case OP_NEG_ROOT:
        case OP_U_ASIN:
        case OP_U_ACOS:
        case OP_DIV0:
        case OP_IDIV0:
        case OP_MOD0:
        case OP_POWER0:
            return true;
        default:
            return false;
        }
        return false;
    }
};

/**
   \brief Procedures for recognizing arithmetic expressions.
   We don't need access to ast_manager, and operations can be simultaneously
   executed in different threads.
*/
class arith_recognizers {
    bool is_arith_op(expr const* n, decl_kind k, unsigned& sz, expr*& x, expr*& y) {
        if (!is_app_of(n, arith_family_id, k))
            return false;
        x = to_app(n)->get_arg(0);
        y = to_app(n)->get_arg(1);
        sz = to_app(n)->get_parameter(0).get_int();
        return true;
    }
public:
    family_id get_family_id() const { return arith_family_id; }

    bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == arith_family_id; }

    bool is_irrational_algebraic_numeral(expr const* n) const;

    bool is_numeral(expr const* n) const { return is_app_of(n, arith_family_id, OP_NUM); }
    bool is_int_expr(expr const * e) const;

    bool is_le(expr const * n) const { return is_app_of(n, arith_family_id, OP_LE); }
    bool is_ge(expr const * n) const { return is_app_of(n, arith_family_id, OP_GE); }
    bool is_lt(expr const * n) const { return is_app_of(n, arith_family_id, OP_LT); }
    bool is_gt(expr const * n) const { return is_app_of(n, arith_family_id, OP_GT); }
    bool is_le(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_LE); }
    bool is_ge(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_GE); }
    bool is_lt(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_LT); }
    bool is_gt(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_GT); }

    bool is_div0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_DIV0); }
    bool is_idiv0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_IDIV0); }
    bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); }
    bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); }
    bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); }
    bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); }
    bool is_add(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_ADD); }
    bool is_mul(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MUL); }
    bool is_sub(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_SUB); }
    bool is_uminus(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_UMINUS); }
    bool is_div(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_DIV); }
    bool is_rem(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_REM); }
    bool is_mod(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MOD); }
    bool is_to_real(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_REAL); }
    bool is_to_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_INT); }
    bool is_is_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_IS_INT); }

    bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); }
    bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); }
    bool is_uminus(expr const * n) const { return is_app_of(n, arith_family_id, OP_UMINUS); }
    bool is_mul(expr const * n) const { return is_app_of(n, arith_family_id, OP_MUL); }
    bool is_div(expr const * n) const { return is_app_of(n, arith_family_id, OP_DIV); }
    bool is_div0(expr const * n) const { return is_app_of(n, arith_family_id, OP_DIV0); }
    bool is_idiv(expr const * n) const { return is_app_of(n, arith_family_id, OP_IDIV); }
    bool is_idiv0(expr const * n) const { return is_app_of(n, arith_family_id, OP_IDIV0); }
    bool is_mod(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD); }
    bool is_rem(expr const * n) const { return is_app_of(n, arith_family_id, OP_REM); }
    bool is_mod0(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD0); }
    bool is_rem0(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD0); }
    bool is_to_real(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_REAL); }
    bool is_to_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_INT); }
    bool is_is_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_IS_INT); }
    bool is_power(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER); }
    bool is_power0(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER0); }
    bool is_abs(expr const* n) const { return is_app_of(n, arith_family_id, OP_ABS); }

    bool is_int(sort const * s) const { return is_sort_of(s, arith_family_id, INT_SORT); }
    bool is_int(expr const * n) const { return is_int(n->get_sort()); }
    bool is_real(sort const * s) const { return is_sort_of(s, arith_family_id, REAL_SORT); }
    bool is_real(expr const * n) const { return is_real(n->get_sort()); }
    bool is_complex(sort const * s) const { return is_sort_of(s, arith_family_id, COMPLEX_SORT); }
    bool is_complex(expr const * n) const { return is_complex(n->get_sort()); }
    bool is_complex_constructor(expr const * n) const { return is_app_of(n, arith_family_id, OP_COMPLEX); }
    bool is_real_part(expr const * n) const { return is_app_of(n, arith_family_id, OP_REAL_PART); }
    bool is_imag_part(expr const * n) const { return is_app_of(n, arith_family_id, OP_IMAG_PART); }
    bool is_int_real(sort const * s) const { return is_int(s) || is_real(s); }
    bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }

    bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); }
    bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_BAND, sz, x, y); }
    bool is_shl(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_SHL); }
    bool is_shl(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_SHL, sz, x, y); }
    bool is_lshr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_LSHR); }
    bool is_lshr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_LSHR, sz, x, y); }
    bool is_ashr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_ASHR); }
    bool is_ashr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_ASHR, sz, x, y); }

    bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); }
    bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); }
    bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); }
    bool is_sinh(expr const* n) const { return is_app_of(n, arith_family_id, OP_SINH); }
    bool is_cosh(expr const* n) const { return is_app_of(n, arith_family_id, OP_COSH); }
    bool is_tanh(expr const* n) const { return is_app_of(n, arith_family_id, OP_TANH); }
    bool is_asin(expr const* n) const { return is_app_of(n, arith_family_id, OP_ASIN); }
    bool is_acos(expr const* n) const { return is_app_of(n, arith_family_id, OP_ACOS); }
    bool is_atan(expr const* n) const { return is_app_of(n, arith_family_id, OP_ATAN); }
    bool is_asinh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ASINH); }
    bool is_acosh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ACOSH); }
    bool is_atanh(expr const* n) const { return is_app_of(n, arith_family_id, OP_ATANH); }
    bool is_exp(expr const* n) const { return is_app_of(n, arith_family_id, OP_EXP); }
    bool is_atan2(expr const* n) const { return is_app_of(n, arith_family_id, OP_ATAN2); }
    bool is_log(expr const* n) const { return is_app_of(n, arith_family_id, OP_LOG); }
    bool is_pi(expr const * arg) const { return is_app_of(arg, arith_family_id, OP_PI); }
    bool is_e(expr const * arg) const { return is_app_of(arg, arith_family_id, OP_E); }
    bool is_non_algebraic(expr const* n) const {
        return is_sin(n) ||
            is_cos(n) ||
            is_tan(n) ||
            is_sinh(n) ||
            is_cosh(n) ||
            is_tanh(n) || 
            is_asin(n) ||
            is_acos(n) ||
            is_atan(n) ||
            is_asinh(n) ||
            is_acosh(n) ||
            is_atanh(n) ||
            is_exp(n) ||
            is_atan2(n) ||
            is_log(n) ||
            is_e(n) ||
            is_pi(n);
    }

    START_DISABLE_EXTRA_SEMI_WARNING;
    MATCH_UNARY(is_uminus);
    MATCH_UNARY(is_to_real);
    MATCH_UNARY(is_to_int);
    MATCH_UNARY(is_is_int);
    MATCH_UNARY(is_abs);
    MATCH_BINARY(is_sub);
    MATCH_BINARY(is_add);
    MATCH_BINARY(is_mul);
    MATCH_BINARY(is_le);
    MATCH_BINARY(is_ge);
    MATCH_BINARY(is_lt);
    MATCH_BINARY(is_gt);
    MATCH_BINARY(is_mod);
    MATCH_BINARY(is_rem);
    MATCH_BINARY(is_div);
    MATCH_BINARY(is_idiv);
    MATCH_BINARY(is_mod0);
    // MATCH_BINARY(is_rem0);
    MATCH_BINARY(is_div0);
    MATCH_BINARY(is_idiv0);
    MATCH_BINARY(is_power);
    MATCH_BINARY(is_power0);

    MATCH_UNARY(is_sin);
    MATCH_UNARY(is_asin);
    MATCH_UNARY(is_asinh);
    MATCH_UNARY(is_cos);
    MATCH_UNARY(is_acos);
    MATCH_UNARY(is_acosh);
    MATCH_UNARY(is_tan);
    MATCH_UNARY(is_atan);
    MATCH_UNARY(is_atanh);
    MATCH_UNARY(is_sinh);
    MATCH_UNARY(is_cosh);
    MATCH_UNARY(is_tanh);
    MATCH_UNARY(is_exp);
    MATCH_BINARY(is_atan2);
    MATCH_UNARY(is_log);
    END_DISABLE_WARNING;

};

class arith_util : public arith_recognizers {
    ast_manager &       m_manager;
    arith_decl_plugin * m_plugin;

    void init_plugin();

public:
    arith_util(ast_manager & m);

    ast_manager & get_manager() const { return m_manager; }

    arith_decl_plugin & plugin() const {
        if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
        SASSERT(m_plugin != 0);
        return *m_plugin;
    }

    algebraic_numbers::manager & am() const {
        return plugin().am();
    }

    // return true if \c n is a term of the form (* -1 r)
    bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
    bool is_one(expr const* n) const{ rational val; return is_numeral(n, val) && val.is_one(); }
    bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
    bool is_times_minus_one(expr* n, expr*& r) const {
        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
            r = to_app(n)->get_arg(1);
            return true;
        }
        return false;
    }
    bool is_unsigned(expr const* n, unsigned& u) const {
        rational val;
        bool is_int = true;
        return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true);
    }
    bool is_numeral(expr const* n) const { return arith_recognizers::is_numeral(n); }
    bool is_numeral(expr const* n, rational& val, bool& is_int) const;
    bool is_numeral(expr const* n, rational& val) const { bool is_int; return is_numeral(n, val, is_int); }

    bool convert_int_numerals_to_real() const { return plugin().convert_int_numerals_to_real(); }
    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const;
    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n) const;

    sort * mk_int() { return m_manager.mk_sort(arith_family_id, INT_SORT); }
    sort * mk_real() { return m_manager.mk_sort(arith_family_id, REAL_SORT); }
    sort * mk_complex() { return m_manager.mk_sort(arith_family_id, COMPLEX_SORT); }
    app * mk_complex(expr * re, expr * im) const { return m_manager.mk_app(arith_family_id, OP_COMPLEX, re, im); }
    app * mk_real_part(expr * z) const { return m_manager.mk_app(arith_family_id, OP_REAL_PART, z); }
    app * mk_imag_part(expr * z) const { return m_manager.mk_app(arith_family_id, OP_IMAG_PART, z); }

    func_decl* mk_rem0();
    func_decl* mk_div0();
    func_decl* mk_idiv0();
    func_decl* mk_mod0();
    func_decl* mk_ipower0();
    func_decl* mk_rpower0();


    app * mk_numeral(rational const & val, bool is_int) const {
        return plugin().mk_numeral(val, is_int);
    }
    app * mk_numeral(rational const & val, sort const * s) const {
        if (is_complex(s)) {
            expr_ref re(mk_numeral(val, false), m_manager);
            expr_ref im(mk_numeral(rational(0), false), m_manager);
            return mk_complex(re, im);
        }
        SASSERT(is_int(s) || is_real(s));
        return mk_numeral(val, is_int(s));
    }
    app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int) {
        return plugin().mk_numeral(m, val, is_int);
    }
    app * mk_numeral(sexpr const * p, unsigned i) {
        return plugin().mk_numeral(p, i);
    }
    app * mk_int(int i) {
        return mk_numeral(rational(i), true);
    }
    app * mk_int(unsigned i) {
        return mk_numeral(rational(i), true);
    }
    app * mk_int(rational const& r) {
        return mk_numeral(r, true);
    }
    app * mk_real(int i) {
        return mk_numeral(rational(i), false);
    }
    app * mk_real(rational const& r) {
        return mk_numeral(r, false);
    }
    app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_LE, arg1, arg2); }
    app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GE, arg1, arg2); }
    app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_LT, arg1, arg2); }
    app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_GT, arg1, arg2); }
    app * mk_divides(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_IDIVIDES, arg1, arg2); }

    app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_ADD, num_args, args); }
    app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2); }
    app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); }
    app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.data()); }
    app * mk_add(expr_ref_buffer const& args) const { return mk_add(args.size(), args.data()); }
    app * mk_add(ptr_buffer<expr> const& args) const { return mk_add(args.size(), args.data()); }
    app * mk_add(ptr_vector<expr> const& args) const { return mk_add(args.size(), args.data()); }

    app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); }
    app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); }
    app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2); }
    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2, arg3); }
    app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_MUL, num_args, args); }
    app * mk_mul(ptr_buffer<expr> const& args) const { return mk_mul(args.size(), args.data()); }
    app * mk_mul(ptr_vector<expr> const& args) const { return mk_mul(args.size(), args.data()); }
    app * mk_mul(expr_ref_vector const& args) const { return mk_mul(args.size(), args.data()); }
    app * mk_uminus(expr * arg) const { return m_manager.mk_app(arith_family_id, OP_UMINUS, arg); }
    app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV, arg1, arg2); }
    app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV, arg1, arg2); }
    app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_REM, arg1, arg2); }
    app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD, arg1, arg2); }
    app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV0, arg1, arg2); }
    app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV0, arg1, arg2); }
    app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD0, arg1, arg2); }
    app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD0, arg1, arg2); }
    app * mk_to_real(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_REAL, arg1); }
    app * mk_to_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_INT, arg1); }
    app * mk_is_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_IS_INT, arg1); }
    app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); }
    app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); }

    app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); }
    app* mk_band(unsigned n, std::initializer_list<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, static_cast<unsigned>(args.size()), args.begin()); }
    app* mk_shl(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, 2, args); }
    app* mk_shl(unsigned n, std::initializer_list<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, static_cast<unsigned>(args.size()), args.begin()); }
    app* mk_ashr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, 2, args); }
    app* mk_ashr(unsigned n, std::initializer_list<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, static_cast<unsigned>(args.size()), args.begin()); }
    app* mk_lshr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, 2, args); }
    app* mk_lshr(unsigned n, std::initializer_list<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, static_cast<unsigned>(args.size()), args.begin()); }

    app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); }
    app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); }
    app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); }
    app * mk_asin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ASIN, arg); }
    app * mk_acos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ACOS, arg); }
    app * mk_atan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ATAN, arg); }

    app * mk_sinh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SINH, arg); }
    app * mk_cosh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COSH, arg); }
    app * mk_tanh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TANH, arg); }
    app * mk_asinh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ASINH, arg); }
    app * mk_acosh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ACOSH, arg); }
    app * mk_atanh(expr * arg) { return m_manager.mk_app(arith_family_id, OP_ATANH, arg); }
    app * mk_exp(expr * arg) { return m_manager.mk_app(arith_family_id, OP_EXP, arg); }
    app * mk_atan2(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_ATAN2, arg1, arg2); }
    app * mk_log(expr * arg) { return m_manager.mk_app(arith_family_id, OP_LOG, arg); }

    app * mk_pi() { return plugin().mk_pi(); }
    app * mk_e()  { return plugin().mk_e(); }

    app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_NEG_ROOT, arg1, arg2); }
    app * mk_u_asin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_U_ASIN, arg); }
    app * mk_u_acos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_U_ACOS, arg); }

    /**
       \brief Return the equality (= lhs rhs), but it makes sure that
       if one of the arguments is a numeral, then it will be in the right-hand-side;
       if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
    */
    app * mk_eq(expr * lhs, expr * rhs) {
        if (arith_recognizers::is_numeral(lhs) || (!arith_recognizers::is_numeral(rhs) && lhs->get_id() > rhs->get_id()))
            std::swap(lhs, rhs);
        if (lhs == rhs)
            return m_manager.mk_true();
        if (arith_recognizers::is_numeral(lhs) && arith_recognizers::is_numeral(rhs)) {
            SASSERT(lhs != rhs);
            return m_manager.mk_false();
        }
        return m_manager.mk_eq(lhs, rhs);
    }

    expr_ref mk_mul_simplify(expr_ref_vector const& args);
    expr_ref mk_mul_simplify(unsigned sz, expr* const* args);

    expr_ref mk_add_simplify(expr_ref_vector const& args);
    expr_ref mk_add_simplify(unsigned sz, expr* const* args);

    bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);

    bool is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);

    bool is_underspecified(expr* e) const;

    bool is_bounded(expr* e) const;

    bool is_extended_numeral(expr* e, rational& r) const;

};


inline app_ref mk_numeral(rational const& r, app_ref const& x) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_numeral(r, r.is_int() && a.is_int(x)), x.get_manager());
}

inline app_ref operator+(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_add(x, y), x.get_manager());
}

inline app_ref operator+(app_ref const& x, rational const& y) {
    return x + mk_numeral(y, x);
}

inline app_ref operator+(app_ref const& x, int y) {
    return x + rational(y);
}

inline app_ref operator+(rational const& x, app_ref const& y) {
    return mk_numeral(x, y) + y;
}

inline app_ref operator+(int x, app_ref const& y) {
    return rational(x) + y;
}

inline app_ref operator-(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_sub(x, y), x.get_manager());
}

inline app_ref operator-(app_ref const& x, rational const& y) {
    return x - mk_numeral(y, x);
}

inline app_ref operator-(app_ref const& x, int y) {
    return x - rational(y);
}

inline app_ref operator-(rational const& x, app_ref const& y) {
    return mk_numeral(x, y) - y;
}

inline app_ref operator-(int x, app_ref const& y) {
    return rational(x) - y;
}


inline app_ref operator*(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_mul(x, y), x.get_manager());
}

inline app_ref operator*(app_ref const& x, rational const& y) {
    return x * mk_numeral(y, x);
}

inline app_ref operator*(rational const& x, app_ref const& y) {
    return mk_numeral(x, y) * y;
}

inline app_ref operator*(app_ref const& x, int y) {
    return x * rational(y);
}

inline app_ref operator*(int x, app_ref const& y) {
    return rational(x) * y;
}

inline app_ref operator<=(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_le(x, y), x.get_manager());
}

inline app_ref operator<=(app_ref const& x, rational const& y) {
    return x <= mk_numeral(y, x);
}

inline app_ref operator<=(app_ref const& x, int y) {
    return x <= rational(y);
}

inline app_ref operator>=(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_ge(x, y), x.get_manager());
}

inline app_ref operator<(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_lt(x, y), x.get_manager());
}

inline app_ref operator>(app_ref const& x, app_ref const& y) {
    arith_util a(x.get_manager());
    return app_ref(a.mk_gt(x, y), x.get_manager());
}