hal::SMT Namespace Reference

Namespaces
	Bitwuzla
	Boolector
	ConstantPropagation
	ModelParser
	Translator
	Z3

Classes
class	Solver
class	SymbolicExecution
class	SymbolicState
struct	QueryConfig
struct	Constraint
struct	Model
struct	SolverResult

Enumerations
enum class	SolverType : int { Z3 = 0 , Boolector , Bitwuzla , Unknown }
enum class	SolverCall : int { Binary , Library }
enum class	SolverResultType { Sat , UnSat , Unknown }

Functions
std::ostream &	operator<< (std::ostream &out, const QueryConfig &config)
std::ostream &	operator<< (std::ostream &out, const Constraint &constraint)
std::ostream &	operator<< (std::ostream &out, const Model &model)
std::ostream &	operator<< (std::ostream &out, const SolverResult &result)

Enumeration Type Documentation

SolverCall

enum hal::SMT::SolverCall : int

strong

Enumerator
Binary	Call binary in subprocess
Library	Call linked library

Definition at line 51 of file types.h.

SolverResultType

enum hal::SMT::SolverResultType

strong

Result type of an SMT solver query.

Enumerator
Sat	The list of constraints is satisfiable.
UnSat	The list of constraints is not satisfiable.
Unknown	A result could not be obtained, e.g., due to a time-out.

Definition at line 216 of file types.h.

SolverType

enum hal::SMT::SolverType : int

strong

Identifier for the SMT solver type.

Enumerator
Z3	Z3 SMT solver.
Boolector	Boolector SMT solver.
Bitwuzla	Bitwuzla SMT solver.
Unknown	Unknown (unsupported) SMT solver.

Definition at line 43 of file types.h.

Function Documentation

operator<<() [1/4]

std::ostream& hal::SMT::operator<<	(	std::ostream &	out,
		const Constraint &	constraint
	)

Passes a human-readable description of the SMT constraint to the output stream.

Parameters

[in]	out	- The output stream to write to.
[in]	constraint	- The SMT constraint.

Returns

A reference to the output stream.

Definition at line 151 of file types.cpp.

operator<<() [2/4]

std::ostream& hal::SMT::operator<<	(	std::ostream &	out,
		const Model &	model
	)

Passes a human-readable description of the SMT model to the output stream.

Parameters

[in]	out	- The output stream to write to.
[in]	model	- The SMT model.

Returns

A reference to the output stream.

Definition at line 210 of file types.cpp.

operator<<() [3/4]

std::ostream& hal::SMT::operator<<	(	std::ostream &	out,
		const QueryConfig &	config
	)

Passes a human-readable description of the SMT query configuration to the output stream.

Parameters

[in]	out	- The output stream to write to.
[in]	config	- The SMT query configuration.

Returns

A reference to the output stream.

Definition at line 131 of file types.cpp.

operator<<() [4/4]

std::ostream& hal::SMT::operator<<	(	std::ostream &	out,
		const SolverResult &	result
	)

Human-readable description of SMT result.

Parameters

[in]	out	- Stream to write to.
[in]	result	- SMT result.

Returns

A reference to output stream.

Definition at line 334 of file types.cpp.