cprover
Loading...
Searching...
No Matches
solver_factory.cpp File Reference

Solver Factory. More...

+ Include dependency graph for solver_factory.cpp:

Go to the source code of this file.

Functions

static void emit_solver_warning (message_handlert &message_handler, const std::string &solver)
 Emit a warning for non-existent solver solver via message_handler.
 
template<typename SatcheckT >
static std::unique_ptr< SatcheckT > make_satcheck_prop (message_handlert &message_handler, const optionst &options)
 
static std::unique_ptr< proptget_sat_solver (message_handlert &message_handler, const optionst &options)
 
std::unique_ptr< std::ofstream > open_outfile_and_check (const std::string &filename, message_handlert &message_handler, const std::string &arg_name)
 
static void parse_sat_options (const cmdlinet &cmdline, optionst &options)
 
static void parse_smt2_options (const cmdlinet &cmdline, optionst &options)
 
void parse_solver_options (const cmdlinet &cmdline, optionst &options)
 Parse solver-related command-line parameters in cmdline and set corresponding values in options.
 

Detailed Description

Solver Factory.

Definition in file solver_factory.cpp.

Function Documentation

◆ emit_solver_warning()

static void emit_solver_warning ( message_handlert & message_handler,
const std::string & solver )
static

Emit a warning for non-existent solver solver via message_handler.

Definition at line 181 of file solver_factory.cpp.

◆ get_sat_solver()

static std::unique_ptr< propt > get_sat_solver ( message_handlert & message_handler,
const optionst & options )
static

Definition at line 218 of file solver_factory.cpp.

◆ make_satcheck_prop()

template<typename SatcheckT >
static std::unique_ptr< SatcheckT > make_satcheck_prop ( message_handlert & message_handler,
const optionst & options )
static

Definition at line 193 of file solver_factory.cpp.

◆ open_outfile_and_check()

std::unique_ptr< std::ofstream > open_outfile_and_check ( const std::string & filename,
message_handlert & message_handler,
const std::string & arg_name )

Definition at line 440 of file solver_factory.cpp.

◆ parse_sat_options()

static void parse_sat_options ( const cmdlinet & cmdline,
optionst & options )
static

Definition at line 608 of file solver_factory.cpp.

◆ parse_smt2_options()

static void parse_smt2_options ( const cmdlinet & cmdline,
optionst & options )
static

Definition at line 625 of file solver_factory.cpp.

◆ parse_solver_options()

void parse_solver_options ( const cmdlinet & cmdline,
optionst & options )

Parse solver-related command-line parameters in cmdline and set corresponding values in options.

Definition at line 705 of file solver_factory.cpp.