HAL
Public Member Functions | Static Public Member Functions | List of all members
hal::SMT::Solver Class Referencefinal

#include <solver.h>

Collaboration diagram for hal::SMT::Solver:
Collaboration graph

Public Member Functions

 Solver (const std::vector< Constraint > &constraints={})
 
const std::vector< Constraint > & get_constraints () const
 
Solver & with_constraint (const Constraint &constraint)
 
Solver & with_constraints (const std::vector< Constraint > &constraints)
 
Result< SolverResult > query (const QueryConfig &config=QueryConfig()) const
 
Result< SolverResult > query_local (const QueryConfig &config) const
 
Result< SolverResult > query_remote (const QueryConfig &config) const
 
Result< std::string > to_smt2 (const QueryConfig &config) const
 

Static Public Member Functions

static bool has_local_solver_for (SolverType type, SolverCall call)
 
static Result< SolverResult > query_local_with_smt2 (const QueryConfig &config, const std::string &smt2)
 

Detailed Description

Provides an interface to query SMT solvers for a list of constraints, i.e. statements that have to be equal. To this end, we translate constraints to a SMT-LIB v2 string representation and query solvers with a defined configuration, i.e., chosen solver, model generation etc.

Definition at line 40 of file solver.h.

Constructor & Destructor Documentation

◆ Solver()

hal::SMT::Solver::Solver ( const std::vector< Constraint > &  constraints = {})

Constructs an solver with an optional list of constraints.

Parameters
[in]constraints- The (optional) list of constraints.

Definition at line 352 of file solver.cpp.

Member Function Documentation

◆ get_constraints()

const std::vector< Constraint > & hal::SMT::Solver::get_constraints ( ) const

Returns the vector of constraints.

Returns
The vector of constraints.

Definition at line 371 of file solver.cpp.

Referenced by hal::smt_init().

◆ has_local_solver_for()

bool hal::SMT::Solver::has_local_solver_for ( SolverType  type,
SolverCall  call 
)
static

Checks whether a SMT solver of the given type is available on the local machine.

Parameters
[in]type- The SMT solver type.
[in]call- The solver call.
Returns
true if an SMT solver of the requested type is available, false otherwise.

Definition at line 376 of file solver.cpp.

References hal::SMT::Binary, and type.

Referenced by hal::smt_init().

◆ query()

Result< SolverResult > hal::SMT::Solver::query ( const QueryConfig &  config = QueryConfig()) const

Queries an SMT solver with the specified query configuration.

Parameters
[in]config- The SMT solver query configuration.
Returns
OK() and the result on success, Err() otherwise.

Definition at line 402 of file solver.cpp.

References ERR_APPEND, query_local(), and query_remote().

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

◆ query_local()

Result< SolverResult > hal::SMT::Solver::query_local ( const QueryConfig &  config) const

Queries a local SMT solver with the specified query configuration.

Parameters
[in]config- The SMT solver query configuration.
Returns
OK() and the result on success, Err() otherwise.

Definition at line 428 of file solver.cpp.

References ERR_APPEND, hal::input, and query_local_with_smt2().

Referenced by query().

◆ query_local_with_smt2()

Result< SolverResult > hal::SMT::Solver::query_local_with_smt2 ( const QueryConfig &  config,
const std::string &  smt2 
)
static

Queries a local SMT solver with the specified query configuration and the provided smt2 representation of the query.

Parameters
[in]config- The SMT solver query configuration.
[in]smt2- The SMT solver query as smt2 string.
Returns
OK() and the result on success, Err() otherwise.

Definition at line 440 of file solver.cpp.

References hal::SMT::QueryConfig::call, ERR_APPEND, hal::output, query(), and hal::SMT::QueryConfig::solver.

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

◆ query_remote()

Result< SolverResult > hal::SMT::Solver::query_remote ( const QueryConfig &  config) const

Queries a remote SMT solver with the specified query configuration.

Warning
This function is not yet implemented.
Parameters
[in]config- The SMT solver query configuration.
Returns
Ok() and the result on success, Err() otherwise.

Definition at line 451 of file solver.cpp.

References ERR.

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

◆ to_smt2()

Result< std::string > hal::SMT::Solver::to_smt2 ( const QueryConfig &  config) const

Translate the solver into an SMT-LIB v2 string representation

Parameters
[in]config- The SMT solver query configuration.
Returns
Ok() and the SMT-LIB v2 string representation, Err() otherwise.

Definition at line 457 of file solver.cpp.

◆ with_constraint()

Solver & hal::SMT::Solver::with_constraint ( const Constraint &  constraint)

Adds a constraint to the SMT solver.

Parameters
[in]constraint- The constraint.
Returns
The updated SMT solver.

Definition at line 356 of file solver.cpp.

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

◆ with_constraints()

Solver & hal::SMT::Solver::with_constraints ( const std::vector< Constraint > &  constraints)

Adds a vector of constraints to the SMT solver.

Parameters
[in]constraints- the constraints.
Returns
The updated SMT solver.

Definition at line 362 of file solver.cpp.

Referenced by hal::smt_init().

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