oneshot_process.h

Go to the documentation of this file.

#ifndef _ESBMC_SOLVERS_SMTLIB_ONESHOT_PROCESS_H
#define _ESBMC_SOLVERS_SMTLIB_ONESHOT_PROCESS_H
 
#include <solvers/smt/smt_result.h>
 
#include <optional>
#include <string>
 
class optionst;

namespace oneshot_process
{
std::optional<smt_resultt> parse_verdict_line(const std::string &line);

bool uses_temp_formula(const optionst &options);

std::string choose_formula_path(const optionst &options, const char *name);

std::string model_prog(const optionst &options, const char *name);

smt_resultt run_solver(
  const std::string &cmd,
  const std::string &formula_path,
  const char *name,
  std::string *captured_output = nullptr);
} // namespace oneshot_process
 
#endif /* _ESBMC_SOLVERS_SMTLIB_ONESHOT_PROCESS_H */