python_math.h

Go to the documentation of this file.

#ifndef CPROVER_PYTHON_FRONTEND_PYTHON_MATH_H
#define CPROVER_PYTHON_FRONTEND_PYTHON_MATH_H
 
#include <util/arith/arith_tools.h>
#include <util/irep/expr.h>
#include <util/irep/std_code.h>
#include <nlohmann/json.hpp>
#include <optional>
#include <string>
#include <string_view>
#include <unordered_map>
 
class python_converter;
class type_handler;
class contextt;
class symbolt;

class python_math
{
private:
  python_converter &converter;
  contextt &symbol_table;
  type_handler &type_handler_;
  mutable std::unordered_map<std::string_view, const symbolt *>
    c_math_symbol_cache_;

  exprt resolve_symbol(const exprt &operand) const;

  std::optional<BigInt> try_fold_int_constant(const exprt &expr) const;

  exprt promote_to_double_if_needed(exprt operand) const;

  exprt build_unary_c_math_call(
    const char *symbol_id,
    const char *display_name,
    exprt operand,
    const nlohmann::json &element);

  const symbolt &
  get_c_math_symbol_cached(const char *symbol_id, const char *display_name);
 
public:
  std::optional<double> try_resolve_constant_double(const exprt &operand) const;

  python_math(python_converter &conv, contextt &ctx, type_handler &th);
 
  static BigInt pow_bigint_non_negative(BigInt base, BigInt exp);
 
  static bool
  fits_in_width(const BigInt &value, unsigned width, bool is_signed);
 
  static const BigInt kMaxConstantFoldExponent;

  bool is_math_dispatch_target(
    const std::string &caller,
    const std::string &func_name) const;

  bool is_math_dispatch_target_cached(
    const std::string &caller,
    const std::string &func_name);

  bool is_unary_dispatch_function(std::string_view func_name) const;

  bool is_binary_dispatch_function(std::string_view func_name) const;

  exprt handle(
    std::string_view func_name,
    exprt operand,
    const nlohmann::json &element);

  exprt handle(
    std::string_view func_name,
    exprt lhs,
    exprt rhs,
    const nlohmann::json &element);

  exprt compute_expr(const exprt &expr) const;

  exprt handle_power(exprt lhs, exprt rhs);

  exprt handle_power_symbolic(exprt base, exprt exp);
  exprt handle_power_symbolic_exponent(exprt lhs, exprt rhs);

  exprt build_power_expression(const exprt &base, const BigInt &exp);

  exprt handle_modulo(exprt lhs, exprt rhs, const nlohmann::json &element);

  exprt
  handle_int_modulo(const exprt &lhs, const exprt &rhs, const exprt &bin_expr);

  exprt handle_floor_division(
    const exprt &lhs,
    const exprt &rhs,
    const exprt &bin_expr);

  void handle_float_division(exprt &lhs, exprt &rhs, exprt &bin_expr) const;

  void promote_int_to_float(exprt &op, const typet &target_type) const;

  exprt handle_sqrt(exprt operand, const nlohmann::json &element);

  exprt handle_sin(exprt operand, const nlohmann::json &element);

  exprt handle_cos(exprt operand, const nlohmann::json &element);

  exprt
  handle_divmod(exprt dividend, exprt divisor, const nlohmann::json &element);
  exprt handle_numeric_divmod(
    exprt dividend,
    exprt divisor,
    const nlohmann::json &element);
  exprt raise_divmod_type_error(
    const typet &dividend_type,
    const typet &divisor_type,
    const nlohmann::json &element);

  exprt handle_exp(exprt operand, const nlohmann::json &element);

  exprt handle_log(exprt operand, const nlohmann::json &element);

  exprt handle_acos(exprt operand, const nlohmann::json &element);

  exprt handle_atan(exprt operand, const nlohmann::json &element);

  exprt
  handle_atan2(exprt y_operand, exprt x_operand, const nlohmann::json &element);

  exprt handle_log2(exprt operand, const nlohmann::json &element);

  exprt handle_pow(exprt base, exprt exp, const nlohmann::json &element);

  exprt handle_fabs(exprt operand, const nlohmann::json &element);

  exprt handle_trunc(exprt operand, const nlohmann::json &element);

  exprt handle_fmod(exprt lhs, exprt rhs, const nlohmann::json &element);

  exprt handle_copysign(exprt lhs, exprt rhs, const nlohmann::json &element);

  exprt handle_tan(exprt operand, const nlohmann::json &element);

  exprt handle_asin(exprt operand, const nlohmann::json &element);

  exprt handle_sinh(exprt operand, const nlohmann::json &element);

  exprt handle_cosh(exprt operand, const nlohmann::json &element);

  exprt handle_tanh(exprt operand, const nlohmann::json &element);

  exprt handle_log10(exprt operand, const nlohmann::json &element);

  exprt handle_expm1(exprt operand, const nlohmann::json &element);

  exprt handle_log1p(exprt operand, const nlohmann::json &element);

  exprt handle_exp2(exprt operand, const nlohmann::json &element);

  exprt handle_asinh(exprt operand, const nlohmann::json &element);

  exprt handle_acosh(exprt operand, const nlohmann::json &element);

  exprt handle_atanh(exprt operand, const nlohmann::json &element);

  exprt handle_hypot(exprt lhs, exprt rhs, const nlohmann::json &element);

  exprt handle_dist(exprt p, exprt q, const nlohmann::json &element);
};
 
#endif