smt_object_size.h

Go to the documentation of this file.

// Author: Diffblue Ltd.
 
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OBJECT_SIZE_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OBJECT_SIZE_H
 
#include <solvers/smt2_incremental/ast/smt_commands.h> // IWYU pragma: keep
#include <solvers/smt2_incremental/ast/smt_terms.h>    // IWYU pragma: keep
 
struct smt_object_sizet final
{
  smt_object_sizet();
  smt_declare_function_commandt declaration;
  using make_applicationt =
    smt_function_application_termt::factoryt<smt_command_functiont>;
  make_applicationt make_application;
  smt_commandt make_definition(std::size_t unique_id, smt_termt size) const;
};
 
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OBJECT_SIZE_H