smt_tuple_sym_ast.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_TUPLE_SMT_TUPLE_SYM_AST_H_
#define SOLVERS_SMT_TUPLE_SMT_TUPLE_SYM_AST_H_
 
#include <solvers/smt/smt_conv.h>
 
class tuple_sym_smt_ast;
typedef const tuple_sym_smt_ast *tuple_sym_smt_astt;
 
class smt_tuple_node_flattener;
 
class tuple_sym_smt_ast : public smt_ast
{
public:
  tuple_sym_smt_ast(smt_solver_baset *ctx, smt_sortt s, std::string _name)
    : smt_ast(ctx, s), name(std::move(_name))
  {
  }
  ~tuple_sym_smt_ast() override = default;

  const std::string name;
 
  smt_astt
  ite(smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const override;
  smt_astt eq(smt_solver_baset *ctx, smt_astt other) const override;
  smt_astt update(
    smt_solver_baset *ctx,
    smt_astt value,
    unsigned int idx,
    const expr2tc &idx_expr = expr2tc()) const override;
  smt_astt select(smt_solver_baset *ctx, const expr2tc &idx) const override;
  smt_astt project(smt_solver_baset *ctx, unsigned int elem) const override;
 
  void dump() const override
  {
  }
};
 
inline tuple_sym_smt_astt to_tuple_sym_ast(smt_astt a)
{
  tuple_sym_smt_astt ta = dynamic_cast<tuple_sym_smt_astt>(a);
  assert(ta != nullptr && "Tuple AST mismatch");
  return ta;
}
 
#endif