smt_array.h

Go to the documentation of this file.

#ifndef _ESBMC_SOLVERS_SMT_SMT_ARRAY_H_
#define _ESBMC_SOLVERS_SMT_SMT_ARRAY_H_
 
#include <solvers/smt/smt_ast.h>
#include <solvers/smt/smt_sort.h>
 
// Interface definition for array manipulation
 
class array_iface
{
public:
  // This constructor makes this not qualify as an abstract interface according
  // to strict definitions.
  array_iface(bool _b, bool inf)
    : supports_bools_in_arrays(_b), can_init_infinite_arrays(inf)
  {
  }
 
  virtual smt_astt mk_array_symbol(
    const std::string &name,
    smt_sortt sort,
    smt_sortt subtype) = 0;

  virtual expr2tc
  get_array_elem(smt_astt a, uint64_t idx, const type2tc &subtype) = 0;

  virtual smt_astt
  convert_array_of(smt_astt init_val, unsigned long domain_width) = 0;
 
  smt_astt default_convert_array_of(
    smt_astt init_val,
    unsigned long domain_width,
    smt_solver_baset *ctx);
 
  virtual void add_array_constraints_for_solving() {};
 
  virtual void push_array_ctx() {};
  virtual void pop_array_ctx() {};
 
  // And everything else goes through the ast methods!
 
  // Small piece of internal munging:
  bool supports_bools_in_arrays;
  bool can_init_infinite_arrays;
};
 
#endif /* _ESBMC_SOLVERS_SMT_SMT_ARRAY_H_ */