oneshot_process.h File Reference

#include <solvers/smt/smt_result.h>
#include <optional>
#include <string>

Include dependency graph for oneshot_process.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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.
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.