oneshot_process.cpp File Reference

#include <solvers/smtlib/oneshot_process.h>
#include <util/base/filesystem.h>
#include <util/message/message.h>
#include <util/config/options.h>
#include <cctype>
#include <cerrno>
#include <cstdio>
#include <cstring>
#include <list>
#include <sys/wait.h>
#include <unistd.h>

Include dependency graph for oneshot_process.cpp:

Namespaces
namespace	oneshot_process
	Helpers shared by backends that render the formula into a file via the smtlib serializer and run an external one-shot solver command on it (bitwuzllob, neurosym).

Functions
std::optional< smt_resultt >	oneshot_process::parse_verdict_line (const std::string &line)
	Recognize a verdict on one output line, tolerating surrounding whitespace.
bool	oneshot_process::uses_temp_formula (const optionst &options)
	Whether the formula file is a temporary the backend creates, as opposed to a user-supplied –output path (or stdout under –smt-formula-only).
std::string	oneshot_process::choose_formula_path (const optionst &options, const char *name)
	The formula file the external solver is pointed at.
std::string	oneshot_process::model_prog (const optionst &options, const char *name)
	The local interactive model solver command (<name>-model-prog), or "" when none is configured.
static std::string	oneshot_process::describe_exit_status (int status)
static std::string	oneshot_process::substitute_formula_path (const std::string &cmd_template, const std::string &formula_path)
smt_resultt	oneshot_process::run_solver (const std::string &cmd, const std::string &formula_path, const char *name, std::string *captured_output=nullptr)
	Run the one-shot solver command on formula_path and parse the verdict from its standard output.