smt_tuple.h

Go to the documentation of this file.

#ifndef _ESBMC_SOLVERS_SMT_TUPLE_SMT_TUPLE_H_
#define _ESBMC_SOLVERS_SMT_TUPLE_SMT_TUPLE_H_
 
#include <solvers/smt/smt_ast.h>
#include <solvers/smt/tuple/smt_tuple_sort.h>

void check_tuple_field(
  unsigned int idx,
  std::size_t size,
  const type2tc &tuple_type);
 
// Abstract class defining the interface required for creating tuples.
class tuple_iface
{
public:
  virtual smt_sortt mk_struct_sort(const type2tc &type) = 0;

  virtual smt_astt tuple_create(const expr2tc &structdef) = 0;

  virtual smt_astt tuple_fresh(smt_sortt s, std::string name = "") = 0;
 
  // XXX XXX XXX docs gap
  virtual smt_astt tuple_array_create(
    const type2tc &array_type,
    smt_astt *inputargs,
    bool const_array,
    smt_sortt domain) = 0;

  virtual smt_astt
  tuple_array_of(const expr2tc &init_value, unsigned long domain_width) = 0;

  virtual smt_astt mk_tuple_symbol(const std::string &name, smt_sortt s) = 0;

  virtual smt_astt mk_tuple_array_symbol(const expr2tc &expr) = 0;

  virtual expr2tc tuple_get(const expr2tc &expr) = 0;
  virtual expr2tc tuple_get(const type2tc &type, smt_astt a) = 0;
 
  virtual expr2tc tuple_get_array_elem(
    smt_astt array,
    uint64_t index,
    const type2tc &subtype) = 0;
 
  virtual void add_tuple_constraints_for_solving() {};
  virtual void push_tuple_ctx() {};
  virtual void pop_tuple_ctx() {};
 
  virtual ~tuple_iface() = default;
};
 
#endif /* _ESBMC_SOLVERS_SMT_TUPLE_SMT_TUPLE_H_ */