smt_ast.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_SMT_AST_H_
#define SOLVERS_SMT_SMT_AST_H_
 
#include <solvers/smt/smt_sort.h>
 
#include <irep2/irep2_expr.h>
#include <util/message/message.h>
 
class smt_solver_baset;

 
class smt_ast;
typedef const smt_ast *smt_astt;
 
class smt_ast
{
public:
  smt_sortt sort;

  const smt_solver_baset *context;
 
  smt_ast(smt_solver_baset *ctx, smt_sortt s);
  virtual ~smt_ast() = default;

  virtual smt_astt with_sort(smt_solver_baset *ctx, smt_sortt s) const;
 
  // "this" is the true operand.
  virtual smt_astt
  ite(smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const;

  virtual smt_astt eq(smt_solver_baset *ctx, smt_astt other) const;

  virtual void assign(smt_solver_baset *ctx, smt_astt sym) const;

  virtual smt_astt update(
    smt_solver_baset *ctx,
    smt_astt value,
    unsigned int idx,
    const expr2tc &idx_expr = expr2tc()) const;

  virtual smt_astt select(smt_solver_baset *ctx, const expr2tc &idx) const;

  virtual smt_astt project(smt_solver_baset *ctx, unsigned int elem) const;
 
  virtual void dump() const
  {
    log_status("Chosen solver doesn't support printing the AST\n");
  }
};
 
template <typename solver_ast>
class solver_smt_ast : public smt_ast
{
public:
  solver_smt_ast(smt_solver_baset *ctx, solver_ast _a, smt_sortt s)
    : smt_ast(ctx, s), a(_a)
  {
  }
 
  typedef solver_ast solver_ast_type;
  solver_ast_type a;
};
 
#ifdef NDEBUG
#  define dynamic_cast static_cast
#endif
template <typename derived_class>
const derived_class *to_solver_smt_ast(smt_astt s)
{
  const derived_class *r = dynamic_cast<const derived_class *>(s);
  assert(r);
  return r;
}
#ifdef dynamic_cast
#  undef dynamic_cast
#endif
 
#endif /* SOLVERS_SMT_SMT_AST_H_ */