Class expr

smt/expr.h:25–414

class AndExpr;

class expr {
  uintptr_t ptr = 0;

  expr(Z3_ast ast) noexcept;
  bool isZ3Ast() const;
  Z3_ast ast() const;
  Z3_ast operator()() const { return ast(); }
  void incRef();
  void decRef();

  Z3_sort sort() const;
  Z3_decl decl() const;
  Z3_app isApp() const;
  Z3_app isAppOf(int app_type) const;

  expr binop_commutative(const expr &rhs,
                         Z3_ast(*op)(Z3_context, Z3_ast, Z3_ast),
                         expr (expr::*expr_op)(const expr &) const,
                         bool (expr::*identity)() const,
                         bool (expr::*absorvent)() const,
                         int z3_app = 0) const;
  expr binop_commutative(const expr &rhs,
                         Z3_ast(*op)(Z3_context, Z3_ast, Z3_ast)) const;

  expr unop_fold(Z3_ast(*op)(Z3_context, Z3_ast)) const;
  expr binop_fold(const expr &rhs,
                  Z3_ast(*op)(Z3_context, Z3_ast, Z3_ast)) const;

  bool alwaysFalse() const { return false; }

  static Z3_ast mkTrue();
  static Z3_ast mkFalse();
  static expr mkUInt(uint64_t n, Z3_sort sort);
  static expr mkInt(int64_t n, Z3_sort sort);
  static expr mkConst(Z3_decl decl);

  bool isUnOp(expr &a, int z3op) const;
  bool isBinOp(expr &a, expr &b, int z3op) const;
  bool isTernaryOp(expr &a, expr &b, expr &c, int z3op) const;

public:
  expr() = default;

  expr(expr &&other) noexcept {
    std::swap(ptr, other.ptr);
  }

  expr(const expr &other) noexcept;
  expr(bool val) noexcept : expr(val ? mkTrue() : mkFalse()) {}
  ~expr() noexcept;

  void operator=(expr &&other);
  void operator=(const expr &other);

  static expr mkUInt(uint64_t n, unsigned bits);
  static expr mkUInt(uint64_t n, const expr &type);
  static expr mkInt(int64_t n, unsigned bits);
  static expr mkInt(int64_t n, const expr &type);