smt_tuple_sym.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_TUPLE_SMT_TUPLE_SYM_H_
#define SOLVERS_SMT_TUPLE_SMT_TUPLE_SYM_H_
 
#include <solvers/smt/smt_solver.h>
#include <util/symtab/namespace.h>
 
class tuple_sym_smt_ast;
typedef const tuple_sym_smt_ast *tuple_sym_smt_astt;
 
class smt_tuple_sym_flattener : public tuple_iface
{
public:
  smt_tuple_sym_flattener(smt_solver_baset *_ctx, const namespacet &_ns)
    : ctx(_ctx), ns(_ns)
  {
  }
 
  virtual ~smt_tuple_sym_flattener() = default;
 
  smt_sortt mk_struct_sort(const type2tc &type) override;
  smt_astt tuple_create(const expr2tc &structdef) override;
  smt_astt tuple_fresh(smt_sortt s, std::string name = "") override;
  smt_astt tuple_array_of(const expr2tc &init_value, unsigned long domain_width)
    override;
  smt_astt mk_tuple_symbol(const std::string &name, smt_sortt s) override;
  smt_astt mk_tuple_array_symbol(const expr2tc &expr) override;
  expr2tc tuple_get(const expr2tc &expr) override;
  expr2tc tuple_get(const type2tc &type, smt_astt a) override;
 
  expr2tc tuple_get_array_elem(
    smt_astt array,
    uint64_t index,
    const type2tc &subtype) override;
 
  expr2tc tuple_get_rec(tuple_sym_smt_astt tuple);
  smt_astt tuple_array_create(
    const type2tc &array_type,
    smt_astt *input_args,
    bool const_array,
    smt_sortt domain) override;
 
  smt_solver_baset *ctx;
  const namespacet &ns;
};
 
#endif