smt2_incremental_decision_procedure.h

Go to the documentation of this file.

// Author: Diffblue Ltd.
 
 
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
#include <util/expr.h> // Needed for `exprt` values. IWYU pragma: keep
#include <util/message.h>
 
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/encoding/struct_encoding.h>
#include <solvers/smt2_incremental/object_tracking.h>
#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
#include <solvers/smt2_incremental/smt_object_size.h>
#include <solvers/smt2_incremental/type_size_mapping.h>
#include <solvers/stack_decision_procedure.h>
 
#include <memory>
#include <unordered_map>
 
class namespacet;
class smt_base_solver_processt; // IWYU pragma: keep
class string_constantt;
class union_tag_typet;
 
class smt2_incremental_decision_proceduret final
  : public stack_decision_proceduret
{
public:
  explicit smt2_incremental_decision_proceduret(
    const namespacet &_ns,
    std::unique_ptr<smt_base_solver_processt> solver_process,
    message_handlert &message_handler);
 
  // Implementation of public decision_proceduret member functions.
  exprt handle(const exprt &expr) override;
  exprt get(const exprt &expr) const override;
  void print_assignment(std::ostream &out) const override;
  std::string decision_procedure_text() const override;
  std::size_t get_number_of_solver_calls() const override;
  void set_to(const exprt &expr, bool value) override;
 
  // Implementation of public stack_decision_proceduret member functions.
  void push(const std::vector<exprt> &assumptions) override;
  void push() override;
  void pop() override;
 
  std::optional<exprt>
  get_expr(const smt_termt &descriptor, const typet &type) const;
  std::optional<exprt>
  get_expr(const smt_termt &struct_term, const struct_tag_typet &type) const;
  std::optional<exprt>
  get_expr(const smt_termt &union_term, const union_tag_typet &type) const;
  std::optional<exprt>
  get_expr(const smt_termt &array, const array_typet &type) const;
 
protected:
  // Implementation of protected decision_proceduret member function.
  resultt dec_solve(const exprt &) override;
  template <typename t_exprt>
  void define_array_function(const t_exprt &array);
  void initialize_array_elements(
    const array_exprt &array,
    const smt_identifier_termt &array_identifier);
  void initialize_array_elements(
    const array_of_exprt &array,
    const smt_identifier_termt &array_identifier);
  void initialize_array_elements(
    const string_constantt &string,
    const smt_identifier_termt &array_identifier);
  void define_dependent_functions(const exprt &expr);
  void ensure_handle_for_expr_defined(const exprt &expr);
  smt_termt convert_expr_to_smt(const exprt &expr);
  void define_index_identifiers(const exprt &expr);
  exprt substitute_defined_padding(exprt expr);
  void define_object_properties();
  exprt lower(exprt expression) const;
  std::optional<smt_termt> get_identifier(const exprt &expr) const;
 
  const namespacet &ns;
  size_t number_of_solver_calls;
  std::unique_ptr<smt_base_solver_processt> solver_process;
  messaget log;
  class sequencet
  {
    size_t next_id = 0;
 
  public:
    size_t operator()()
    {
      return next_id++;
    }
  } handle_sequence, array_sequence, index_sequence, padding_sequence;
  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
    expression_handle_identifiers;
  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
    expression_identifiers;
  std::unordered_map<irep_idt, smt_identifier_termt> identifier_table;
  smt_object_mapt object_map;
  std::vector<bool> object_properties_defined;
  smt_object_sizet object_size_function;
  smt_is_dynamic_objectt is_dynamic_object_function;
  type_size_mapt pointer_sizes_map;
  struct_encodingt struct_encoding;
};
 
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H