HAL
Public Member Functions | Public Attributes | Friends | List of all members
hal::SMT::QueryConfig Struct Referencefinal

#include <types.h>

Collaboration diagram for hal::SMT::QueryConfig:
Collaboration graph

Public Member Functions

QueryConfig & with_solver (SolverType solver)
 
QueryConfig & with_call (SolverCall call)
 
QueryConfig & with_local_solver ()
 
QueryConfig & with_remote_solver ()
 
QueryConfig & with_model_generation ()
 
QueryConfig & without_model_generation ()
 
QueryConfig & with_timeout (u64 seconds)
 

Public Attributes

SolverType solver = SolverType::Z3
 The SMT solver identifier. More...
 
SolverCall call = SolverCall::Binary
 The calling format for the SMT solver. More...
 
 bool = true
 Controls whether the SMT query is performed on a local or a remote machine. More...
 
bool generate_model = false
 Controls whether the SMT solver should generate a model in case formula is satisfiable. More...
 
u64 timeout_in_seconds = 10
 The timeout after which the SMT solver is killed in seconds. More...
 

Friends

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

Detailed Description

Represents the data structure to configure an SMT query.

Definition at line 60 of file types.h.

Member Function Documentation

◆ with_call()

QueryConfig & hal::SMT::QueryConfig::with_call ( SolverCall  call)

Sets the solver type to the desired SMT solver.

Parameters
[in]call- The solver call.
Returns
The updated SMT query configuration.

Definition at line 95 of file types.cpp.

References call.

Referenced by hal::smt_init().

◆ with_local_solver()

QueryConfig & hal::SMT::QueryConfig::with_local_solver ( )

Activates local SMT solver execution.

Returns
The updated SMT query configuration.

Definition at line 101 of file types.cpp.

Referenced by hal::smt_init().

◆ with_model_generation()

QueryConfig & hal::SMT::QueryConfig::with_model_generation ( )

Indicates that the SMT solver should generate a model in case the formula is satisfiable.

Returns
The updated SMT query configuration.

Definition at line 113 of file types.cpp.

References generate_model.

Referenced by hal::smt_init(), and hal::solve_fsm::solve_fsm().

◆ with_remote_solver()

QueryConfig & hal::SMT::QueryConfig::with_remote_solver ( )

Indicates that the SMT solver runs on a remote machine.

Returns
The updated SMT query configuration.

Definition at line 107 of file types.cpp.

Referenced by hal::smt_init().

◆ with_solver()

QueryConfig & hal::SMT::QueryConfig::with_solver ( SolverType  solver)

Sets the solver type to the desired SMT solver.

Parameters
[in]solver- The solver type identifier.
Returns
The updated SMT query configuration.

Definition at line 89 of file types.cpp.

References solver.

Referenced by hal::smt_init().

◆ with_timeout()

QueryConfig & hal::SMT::QueryConfig::with_timeout ( u64  seconds)

Sets a timeout in seconds that terminates an SMT query after the specified time has passed.

Parameters
[in]seconds- The timeout in seconds.
Returns
The updated SMT query configuration.

Definition at line 125 of file types.cpp.

References timeout_in_seconds.

Referenced by hal::smt_init(), and hal::solve_fsm::solve_fsm().

◆ without_model_generation()

QueryConfig & hal::SMT::QueryConfig::without_model_generation ( )

Indicates that the SMT solver should not generate a model.

Returns
The updated SMT query configuration.

Definition at line 119 of file types.cpp.

References generate_model.

Referenced by hal::smt_init().

Friends And Related Function Documentation

◆ operator<<

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

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.

Member Data Documentation

◆ bool

hal::SMT::QueryConfig::bool = true

Controls whether the SMT query is performed on a local or a remote machine.

Definition at line 71 of file types.h.

◆ call

SolverCall hal::SMT::QueryConfig::call = SolverCall::Binary

The calling format for the SMT solver.

Definition at line 69 of file types.h.

Referenced by hal::SMT::Solver::query_local_with_smt2(), and with_call().

◆ generate_model

bool hal::SMT::QueryConfig::generate_model = false

Controls whether the SMT solver should generate a model in case formula is satisfiable.

Definition at line 73 of file types.h.

Referenced by hal::SMT::Boolector::query_binary(), hal::SMT::Bitwuzla::query_library(), hal::smt_init(), with_model_generation(), and without_model_generation().

◆ solver

SolverType hal::SMT::QueryConfig::solver = SolverType::Z3

The SMT solver identifier.

Definition at line 67 of file types.h.

Referenced by hal::SMT::Solver::query_local_with_smt2(), hal::smt_init(), and with_solver().

◆ timeout_in_seconds

u64 hal::SMT::QueryConfig::timeout_in_seconds = 10

The timeout after which the SMT solver is killed in seconds.

Definition at line 75 of file types.h.

Referenced by hal::SMT::Z3::query_binary(), hal::SMT::Boolector::query_binary(), hal::smt_init(), and with_timeout().

The documentation for this struct was generated from the following files: