smt_tuple_node_ast.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_TUPLE_SMT_TUPLE_NODE_AST_H_
#define SOLVERS_SMT_TUPLE_SMT_TUPLE_NODE_AST_H_
 
#include <solvers/smt/smt_solver.h>
 
class tuple_node_smt_ast;
typedef const tuple_node_smt_ast *tuple_node_smt_astt;
 
class smt_tuple_node_flattener;

class tuple_node_smt_ast : public smt_ast
{
public:
  tuple_node_smt_ast(
    smt_tuple_node_flattener &f,
    smt_solver_baset *ctx,
    smt_sortt s,
    std::string _name)
    : smt_ast(ctx, s),
      name(std::move(_name)),
      flat(f),
      creation_ctx_level(ctx->ctx_level)
  {
  }
  ~tuple_node_smt_ast() override = default;

  const std::string name;
 
  smt_tuple_node_flattener &flat;
  std::vector<smt_astt> elements;

  const unsigned int creation_ctx_level;
 
  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;
  void assign(smt_solver_baset *ctx, smt_astt sym) 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
  {
    log_debug("tuple-node", "name {}", name);
    for (auto const &e : elements)
      e->dump();
  }
 
  void make_free(smt_solver_baset *ctx);
  void pre_ite(smt_solver_baset *ctx, smt_astt cond, smt_astt falseop);
};
 
inline tuple_node_smt_astt to_tuple_node_ast(smt_astt a)
{
  tuple_node_smt_astt ta = dynamic_cast<tuple_node_smt_astt>(a);
  assert(ta != nullptr && "Tuple AST mismatch");
  return ta;
}
 
#endif