python_set.h

Go to the documentation of this file.

#pragma once
 
#include <nlohmann/json.hpp>
#include <util/irep/type.h>
#include <util/irep/expr.h>
#include <util/symtab/symbol.h>
 
class python_converter;

class python_set
{
public:
  python_set(python_converter &converter, const nlohmann::json &set_node)
    : converter_(converter), set_value_(set_node)
  {
  }

  exprt get();

  exprt get_empty_set();

  exprt get_from_iterable(const exprt &iterable, const nlohmann::json &element);

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

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

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

  exprt build_set_copy(const symbolt &self, const nlohmann::json &element);

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

  exprt build_set_method_call(
    const symbolt &self,
    const exprt &other,
    const nlohmann::json &element,
    const std::string &method_name);

  exprt build_set_relation_call(
    const exprt &self,
    const exprt &other,
    const nlohmann::json &element,
    const std::string &method_name);

  static exprt handle_operations(
    python_converter &converter,
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element);
 
private:
  symbolt &create_set_list();

  static void emit_filtered_extend(
    python_converter &converter,
    const exprt &source_expr,
    const exprt &ref_expr,
    const symbolt &sink,
    bool want_in_ref,
    const nlohmann::json &element);
 
  python_converter &converter_;
  const nlohmann::json &set_value_;
};