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

Functions
std::optional< smt_resultt >	parse_verdict_line (const std::string &line)
	Recognize a verdict on one output line, tolerating surrounding whitespace.
bool	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	choose_formula_path (const optionst &options, const char *name)
	The formula file the external solver is pointed at.
std::string	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	describe_exit_status (int status)
static std::string	substitute_formula_path (const std::string &cmd_template, const std::string &formula_path)
smt_resultt	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.

Detailed Description

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

name is the backend's option prefix: options are looked up as <name>-model-prog etc. and log messages are prefixed with it.

Function Documentation

◆ choose_formula_path()

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

The formula file the external solver is pointed at.

Honour –output so the user can keep the formula; otherwise use a self-cleaning temporary. With –smt-formula-only no solver runs, so honour –output including stdout via "-" (the default when no file is given).

◆ describe_exit_status()

std::string oneshot_process::describe_exit_status ( int status )

static

◆ model_prog()

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.

With –result-only no counterexample is ever built (bmc.cpp skips trace construction), so feeding the formula to a local model solver would only start a solve whose answer is never read; the option is ignored with a warning in that case.

◆ parse_verdict_line()

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

Recognize a verdict on one output line, tolerating surrounding whitespace.

Accepts the bare SMT-LIB verdicts as well as SAT-competition-style "s ..." lines, amid arbitrary log noise. unknown maps to P_ERROR.

◆ run_solver()

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.

Every f in cmd is replaced by the (shell-quoted) formula path; if no f is present, the path is appended.

A non-null captured_output collects the solver's entire stdout, not just the diagnostic tail, so a caller can parse a model straight out of it (see neurosym_conv.cpp). Left null, behaviour is unchanged.

◆ substitute_formula_path()

std::string oneshot_process::substitute_formula_path	(	const std::string &	cmd_template,
		const std::string &	formula_path )