smt_conv.h

Go to the documentation of this file.

#ifndef _ESBMC_PROP_SMT_SMT_CONV_H_
#define _ESBMC_PROP_SMT_SMT_CONV_H_
 
#include <memory>
#include <string>
#include <unordered_set>
#include <irep2/irep2.h>
#include <util/base/threeval.h>
#include <solvers/smt/smt_result.h>
 
// Forward declaration only: the full solver implementation lives in
// smt_solver.h and is deliberately NOT pulled in here, so that including
// smt_conv.h does not expose smt_astt / smt_sortt / ast_vec or the AST/sort
// construction machinery to the rest of ESBMC.
class smt_solver_baset;

class smt_convt
{
public:
  explicit smt_convt(std::unique_ptr<smt_solver_baset> impl);
  ~smt_convt();
 
  // --- Minimal external API, forwarded to the implementation ---
 
  void push_ctx();
  void pop_ctx();
  smt_resultt dec_solve();
  smt_resultt dec_solve_assuming(const std::vector<expr2tc> &assumptions);
  bool supports_assumptions() const;
  void pre_solve();
  const std::string solver_text();

  void convert_ast(const expr2tc &expr);
  void convert_assign(const expr2tc &expr);
  void define(const expr2tc &expr);

  void renumber_symbol_address(
    const expr2tc &guard,
    const expr2tc &addr_symbol,
    const expr2tc &new_size);

  expr2tc get(const expr2tc &expr);
  expr2tc get_by_type(const expr2tc &expr);
  expr2tc get_by_ast(const expr2tc &expr);

  tvt l_get(const expr2tc &expr);

  bool has_model() const;

  void assert_expr(const expr2tc &e);
  void note_division_operands(
    const expr2tc &expr,
    std::unordered_set<const expr2t *> &seen);
  void begin_step(const expr2tc &guard, const expr2tc &cond);
  void note_assignment(const expr2tc &lhs, const expr2tc &rhs);
  void end_step();

  void dump_expr(const expr2tc &expr);
  std::string dump_smt();
  void print_model();
 
private:
  std::unique_ptr<smt_solver_baset> solver_impl;
};
 
#endif /* _ESBMC_PROP_SMT_SMT_CONV_H_ */