Simple dataclass used to store the configuration of the program. More...

#include <Config.h>

Public Types
enum class	LPSolver { SOPLEX = 0 , QSOPTEX = 1 }
	Underlying LP solver used by the theory solver. More...

enum class	SatSolver { CADICAL = 0 , PICOSAT = 1 }
	Underlying SAT solver used by the abstract SAT solver. More...

enum class	SatDefaultPhase { False = 0 , True = 1 , JeroslowWang = 2 , RandomInitialPhase = 3 }
	Phase for the SAT solver. More...

enum class	Format { AUTO , SMT2 , MPS , VNNLIB }
	Format of the input file. More...

enum class	LPMode { AUTO = 0 , PURE_PRECISION_BOOSTING = 1 , PURE_ITERATIVE_REFINEMENT = 2 , HYBRID = 3 }
	LP mode used by the LP solver. More...

enum class	BoundPropagationType { AUTO = 0 , EQ_BINOMIAL = 1 , EQ_POLYNOMIAL = 2 , BOUND_POLYNOMIAL = 3 }
	Types of bound propagation supported by the bound propagator. More...

enum class	PreprocessingRunningFrequency { AUTO , NEVER , ON_FIXED , ON_ITERATION , ALWAYS }
	Frequency at which the preprocessors will run. More...

Public Member Functions
	Config ()=default
	Construct a new Config object.

	Config (std::string filename)
	Construct a new Config object with the given filename.

	Config (bool read_from_stdin)
	Construct a new Config object that will read the input from the standard input.

std::string	filename () const
	Get read-only access to the `filename` parameter of the configuration.

std::string	filename_extension () const
	Get read-only access to the `filename` extension of the configuration.

OptionValue< std::string > &	m_filename ()
	Get read-write access to the `filename` extension of the configuration.

std::string	onnx_file () const
	Get read-only access to the `onnx_file` parameter of the configuration.

OptionValue< std::string > &	m_onnx_file ()
	Get read-write access to the `onnx_file` parameter of the configuration.

bool	needs_expansion () const

LPMode	actual_lp_mode () const
	Get read-only access to the actual `lp_mode` parameter of the configuration.

Format	actual_format () const
	Get read-only access to the actual `format` parameter of the configuration.

BoundPropagationType	actual_bound_propagation_type () const
	Get read-only access to the actual `actual_bound_propagation_type` parameter of the configuration.

PreprocessingRunningFrequency	actual_bound_propagation_frequency () const
	Get read-only access to the actual `bound_propagation_frequency` parameter of the configuration.

PreprocessingRunningFrequency	actual_bound_implication_frequency () const
	Get read-only access to the actual `bound_implication_frequency` parameter of the configuration.

OptionValue< BoundPropagationType > &	m_bound_propagation_type ()
	Get read-only access to the `bound_propagation_type` parameter of the configuration.

const BoundPropagationType &	bound_propagation_type () const
	Get read-write access to the `bound_propagation_type` parameter of the configuration.

OptionValue< PreprocessingRunningFrequency > &	m_bound_propagation_frequency ()
	Get read-only access to the `bound_propagation_frequency` parameter of the configuration.

const PreprocessingRunningFrequency &	bound_propagation_frequency () const
	Get read-write access to the `bound_propagation_frequency` parameter of the configuration.

OptionValue< PreprocessingRunningFrequency > &	m_bound_implication_frequency ()
	Get read-only access to the `bound_implication_frequency` parameter of the configuration.

const PreprocessingRunningFrequency &	bound_implication_frequency () const
	Get read-write access to the `bound_implication_frequency` parameter of the configuration.

OptionValue< bool > &	m_complete ()
	Get read-only access to the `complete` parameter of the configuration.

const bool &	complete () const
	Get read-write access to the `complete` parameter of the configuration.

OptionValue< bool > &	m_continuous_output ()
	Get read-only access to the `continuous_output` parameter of the configuration.

const bool &	continuous_output () const
	Get read-write access to the `continuous_output` parameter of the configuration.

OptionValue< bool > &	m_csv ()
	Get read-only access to the `csv` parameter of the configuration.

const bool &	csv () const
	Get read-write access to the `csv` parameter of the configuration.

OptionValue< bool > &	m_debug_parsing ()
	Get read-only access to the `debug_parsing` parameter of the configuration.

const bool &	debug_parsing () const
	Get read-write access to the `debug_parsing` parameter of the configuration.

OptionValue< bool > &	m_debug_scanning ()
	Get read-only access to the `debug_scanning` parameter of the configuration.

const bool &	debug_scanning () const
	Get read-write access to the `debug_scanning` parameter of the configuration.

OptionValue< bool > &	m_disable_expansion ()
	Get read-only access to the `disable_expansion` parameter of the configuration.

const bool &	disable_expansion () const
	Get read-write access to the `disable_expansion` parameter of the configuration.

OptionValue< bool > &	m_enforce_check_sat ()
	Get read-only access to the `enforce_check_sat` parameter of the configuration.

const bool &	enforce_check_sat () const
	Get read-write access to the `enforce_check_sat` parameter of the configuration.

OptionValue< Format > &	m_format ()
	Get read-only access to the `format` parameter of the configuration.

const Format &	format () const
	Get read-write access to the `format` parameter of the configuration.

OptionValue< LPMode > &	m_lp_mode ()
	Get read-only access to the `lp_mode` parameter of the configuration.

const LPMode &	lp_mode () const
	Get read-write access to the `lp_mode` parameter of the configuration.

OptionValue< LPSolver > &	m_lp_solver ()
	Get read-only access to the `lp_solver` parameter of the configuration.

const LPSolver &	lp_solver () const
	Get read-write access to the `lp_solver` parameter of the configuration.

OptionValue< unsigned int > &	m_number_of_jobs ()
	Get read-only access to the `number_of_jobs` parameter of the configuration.

const unsigned int &	number_of_jobs () const
	Get read-write access to the `number_of_jobs` parameter of the configuration.

OptionValue< bool > &	m_optimize ()
	Get read-only access to the `optimize` parameter of the configuration.

const bool &	optimize () const
	Get read-write access to the `optimize` parameter of the configuration.

OptionValue< double > &	m_precision ()
	Get read-only access to the `precision` parameter of the configuration.

const double &	precision () const
	Get read-write access to the `precision` parameter of the configuration.

OptionValue< bool > &	m_produce_models ()
	Get read-only access to the `produce_models` parameter of the configuration.

const bool &	produce_models () const
	Get read-write access to the `produce_models` parameter of the configuration.

OptionValue< unsigned int > &	m_random_seed ()
	Get read-only access to the `random_seed` parameter of the configuration.

const unsigned int &	random_seed () const
	Get read-write access to the `random_seed` parameter of the configuration.

OptionValue< bool > &	m_read_from_stdin ()
	Get read-only access to the `read_from_stdin` parameter of the configuration.

const bool &	read_from_stdin () const
	Get read-write access to the `read_from_stdin` parameter of the configuration.

OptionValue< SatDefaultPhase > &	m_sat_default_phase ()
	Get read-only access to the `sat_default_phase` parameter of the configuration.

const SatDefaultPhase &	sat_default_phase () const
	Get read-write access to the `sat_default_phase` parameter of the configuration.

OptionValue< SatSolver > &	m_sat_solver ()
	Get read-only access to the `sat_solver` parameter of the configuration.

const SatSolver &	sat_solver () const
	Get read-write access to the `sat_solver` parameter of the configuration.

OptionValue< bool > &	m_silent ()
	Get read-only access to the `silent` parameter of the configuration.

const bool &	silent () const
	Get read-write access to the `silent` parameter of the configuration.

OptionValue< int > &	m_simplex_sat_phase ()
	Get read-only access to the `simplex_sat_phase` parameter of the configuration.

const int &	simplex_sat_phase () const
	Get read-write access to the `simplex_sat_phase` parameter of the configuration.

OptionValue< bool > &	m_skip_check_sat ()
	Get read-only access to the `skip_check_sat` parameter of the configuration.

const bool &	skip_check_sat () const
	Get read-write access to the `skip_check_sat` parameter of the configuration.

OptionValue< int > &	m_verbose_dlinear ()
	Get read-only access to the `verbose_dlinear` parameter of the configuration.

const int &	verbose_dlinear () const
	Get read-write access to the `verbose_dlinear` parameter of the configuration.

OptionValue< int > &	m_verbose_simplex ()
	Get read-only access to the `verbose_simplex` parameter of the configuration.

const int &	verbose_simplex () const
	Get read-write access to the `verbose_simplex` parameter of the configuration.

OptionValue< bool > &	m_verify ()
	Get read-only access to the `verify` parameter of the configuration.

const bool &	verify () const
	Get read-write access to the `verify` parameter of the configuration.

OptionValue< bool > &	m_with_timings ()
	Get read-only access to the `with_timings` parameter of the configuration.

const bool &	with_timings () const
	Get read-write access to the `with_timings` parameter of the configuration.

Detailed Description

Simple dataclass used to store the configuration of the program.

It is usually generated by the ArgParser using the command line arguments.

Definition at line 38 of file Config.h.

Member Enumeration Documentation

◆ BoundPropagationType

enum class dlinear::Config::BoundPropagationType

strong

Types of bound propagation supported by the bound propagator.

Enumerator
AUTO	Automatically select the best configuration based on expected performance. Default option.
EQ_BINOMIAL	Only propagate bounds in theory formulas in the form \( a x_1 + b x_2 = c \).
EQ_POLYNOMIAL	Only propagate bound in theory formulae in the form \( \sum a_i x_i = c \).
BOUND_POLYNOMIAL	Propagate all possible constraints.

Definition at line 72 of file Config.h.

◆ Format

enum class dlinear::Config::Format

strong

Format of the input file.

Enumerator
AUTO	Automatically detect the input format based on the file extension. Default option.
SMT2	SMT2 format.
MPS	MPS format.
VNNLIB	VNNLIB format.

Definition at line 58 of file Config.h.

◆ LPMode

enum class dlinear::Config::LPMode

strong

LP mode used by the LP solver.

Enumerator
AUTO	Let the LP solver choose the mode. Default option.
PURE_PRECISION_BOOSTING	Use the precision boosting mode, if available.
PURE_ITERATIVE_REFINEMENT	Use the iterative refinement mode, if available.
HYBRID	Use both modes, if available.

Definition at line 65 of file Config.h.

◆ LPSolver

enum class dlinear::Config::LPSolver

strong

Underlying LP solver used by the theory solver.

Enumerator
SOPLEX	Soplex Solver. Default option.
QSOPTEX	Qsoptex Solver.

Definition at line 41 of file Config.h.

◆ PreprocessingRunningFrequency

enum class dlinear::Config::PreprocessingRunningFrequency

strong

Frequency at which the preprocessors will run.

Enumerator
AUTO	Automatically select the best configuration based on expected performance. Default option.
NEVER	Never run this preprocess, effectively disabling it.
ON_FIXED	Run this preprocess only once, on fixed literals, before all iterations.
ON_ITERATION	Run this preprocess only at every iteration.
ALWAYS	Run this preprocess at every chance it gets. Usually combines ON_FIXED and ON_ITERATION.

Definition at line 79 of file Config.h.

◆ SatDefaultPhase

enum class dlinear::Config::SatDefaultPhase

strong

Phase for the SAT solver.

Enumerator
False	Assign false to non fixed decision literals.
True	Assign true to non fixed decision literals.
JeroslowWang	Default option.
RandomInitialPhase	Randomly assign a value to non fixed decision literals.

Definition at line 51 of file Config.h.

◆ SatSolver

enum class dlinear::Config::SatSolver

strong

Underlying SAT solver used by the abstract SAT solver.

Enumerator
CADICAL	Cadical Solver. Default option.
PICOSAT	Picosat Solver.

Definition at line 46 of file Config.h.

Constructor & Destructor Documentation

◆ Config() [1/2]

dlinear::Config::Config ( std::string filename )

explicit

Construct a new Config object with the given filename.

Parameters

filename name of the input file

Definition at line 15 of file Config.cpp.

◆ Config() [2/2]

dlinear::Config::Config ( bool read_from_stdin )

explicit

Construct a new Config object that will read the input from the standard input.

Parameters

read_from_stdin whether to read the input from the standard input

Definition at line 16 of file Config.cpp.

Member Function Documentation

◆ actual_bound_implication_frequency()

Config::PreprocessingRunningFrequency dlinear::Config::actual_bound_implication_frequency ( ) const

nodiscard

Get read-only access to the actual bound_implication_frequency parameter of the configuration.

If the bound_implication_frequency is PreprocessingRunningFrequency::AUTO, it will return the appropriate preprocessing running frequency based on the actual format

Returns: actual bound_implication_frequency parameter of the configuration

Definition at line 82 of file Config.cpp.

◆ actual_bound_propagation_frequency()

Config::PreprocessingRunningFrequency dlinear::Config::actual_bound_propagation_frequency ( ) const

nodiscard

Get read-only access to the actual bound_propagation_frequency parameter of the configuration.

If the bound_propagation_frequency is PreprocessingRunningFrequency::AUTO, it will return the appropriate preprocessing running frequency based on the actual format

Returns: actual bound_propagation_frequency parameter of the configuration

Definition at line 65 of file Config.cpp.

◆ actual_bound_propagation_type()

Config::BoundPropagationType dlinear::Config::actual_bound_propagation_type ( ) const

nodiscard

Get read-only access to the actual actual_bound_propagation_type parameter of the configuration.

If the actual_bound_propagation_type is BoundPropagationType::AUTO, it will return the appropriate bound propagation type based on the actual format

Returns: actual actual_bound_propagation_type parameter of the configuration

Definition at line 48 of file Config.cpp.

◆ actual_format()

Config::Format dlinear::Config::actual_format ( ) const

nodiscard

Get read-only access to the actual format parameter of the configuration.

If the format is Format::AUTO, it will return the appropriate format based on the filename extension

Returns: actual format parameter of the configuration

Definition at line 33 of file Config.cpp.

◆ actual_lp_mode()

Config::LPMode dlinear::Config::actual_lp_mode ( ) const

nodiscard

Get read-only access to the actual lp_mode parameter of the configuration.

If the lp_mode is LPMode::AUTO, it will return the appropriate mode based on the lp_solver

Returns: actual lp_mode parameter of the configuration

Definition at line 25 of file Config.cpp.

◆ bound_implication_frequency()

const PreprocessingRunningFrequency & dlinear::Config::bound_implication_frequency ( ) const

inlinenodiscard

Get read-write access to the bound_implication_frequency parameter of the configuration.

Default to PreprocessingRunningFrequency::AUTO

Returns: bound_implication_frequency parameter of the configuration

Definition at line 161 of file Config.h.

◆ bound_propagation_frequency()

const PreprocessingRunningFrequency & dlinear::Config::bound_propagation_frequency ( ) const

inlinenodiscard

Get read-write access to the bound_propagation_frequency parameter of the configuration.

Default to PreprocessingRunningFrequency::AUTO

Returns: bound_propagation_frequency parameter of the configuration

Definition at line 158 of file Config.h.

◆ bound_propagation_type()

const BoundPropagationType & dlinear::Config::bound_propagation_type ( ) const

inlinenodiscard

Get read-write access to the bound_propagation_type parameter of the configuration.

Default to BoundPropagationType::AUTO

Returns: bound_propagation_type parameter of the configuration

Definition at line 155 of file Config.h.

◆ complete()

const bool & dlinear::Config::complete ( ) const

inlinenodiscard

Get read-write access to the complete parameter of the configuration.

Default to false

Returns: complete parameter of the configuration

Definition at line 164 of file Config.h.

◆ continuous_output()

const bool & dlinear::Config::continuous_output ( ) const

inlinenodiscard

Get read-write access to the continuous_output parameter of the configuration.

Default to false

Returns: continuous_output parameter of the configuration

Definition at line 165 of file Config.h.

◆ csv()

const bool & dlinear::Config::csv ( ) const

inlinenodiscard

Get read-write access to the csv parameter of the configuration.

Default to false

Returns: csv parameter of the configuration

Definition at line 166 of file Config.h.

◆ debug_parsing()

const bool & dlinear::Config::debug_parsing ( ) const

inlinenodiscard

Get read-write access to the debug_parsing parameter of the configuration.

Default to false

Returns: debug_parsing parameter of the configuration

Definition at line 167 of file Config.h.

◆ debug_scanning()

const bool & dlinear::Config::debug_scanning ( ) const

inlinenodiscard

Get read-write access to the debug_scanning parameter of the configuration.

Default to false

Returns: debug_scanning parameter of the configuration

Definition at line 168 of file Config.h.

◆ disable_expansion()

const bool & dlinear::Config::disable_expansion ( ) const

inlinenodiscard

Get read-write access to the disable_expansion parameter of the configuration.

Default to false

Returns: disable_expansion parameter of the configuration

Definition at line 172 of file Config.h.

◆ enforce_check_sat()

const bool & dlinear::Config::enforce_check_sat ( ) const

inlinenodiscard

Get read-write access to the enforce_check_sat parameter of the configuration.

Default to false

Returns: enforce_check_sat parameter of the configuration

Definition at line 175 of file Config.h.

◆ filename()

std::string dlinear::Config::filename ( ) const

inlinenodiscard

Get read-only access to the filename parameter of the configuration.

Default to ""

Returns: filename parameter of the configuration

Definition at line 105 of file Config.h.

◆ filename_extension()

std::string dlinear::Config::filename_extension ( ) const

nodiscard

Get read-only access to the filename extension of the configuration.

Contains the filename substring after the dot.

Returns: filename extension of the configuration

Definition at line 18 of file Config.cpp.

◆ format()

const Format & dlinear::Config::format ( ) const

inlinenodiscard

Get read-write access to the format parameter of the configuration.

Default to dlinear::Config::Format::AUTO

Returns: format parameter of the configuration

Definition at line 178 of file Config.h.

◆ lp_mode()

const LPMode & dlinear::Config::lp_mode ( ) const

inlinenodiscard

Get read-write access to the lp_mode parameter of the configuration.

Default to dlinear::Config::LPMode::AUTO

Returns: lp_mode parameter of the configuration

Definition at line 181 of file Config.h.

◆ lp_solver()

const LPSolver & dlinear::Config::lp_solver ( ) const

inlinenodiscard

Get read-write access to the lp_solver parameter of the configuration.

Default to dlinear::Config::LPSolver::SOPLEX

Returns: lp_solver parameter of the configuration

Definition at line 184 of file Config.h.

◆ m_bound_implication_frequency()

OptionValue< PreprocessingRunningFrequency > & dlinear::Config::m_bound_implication_frequency ( )

inline

Get read-only access to the bound_implication_frequency parameter of the configuration.

Default to PreprocessingRunningFrequency::AUTO

Returns: bound_implication_frequency parameter of the configuration

Definition at line 161 of file Config.h.

◆ m_bound_propagation_frequency()

OptionValue< PreprocessingRunningFrequency > & dlinear::Config::m_bound_propagation_frequency ( )

inline

Get read-only access to the bound_propagation_frequency parameter of the configuration.

Default to PreprocessingRunningFrequency::AUTO

Returns: bound_propagation_frequency parameter of the configuration

Definition at line 158 of file Config.h.

◆ m_bound_propagation_type()

OptionValue< BoundPropagationType > & dlinear::Config::m_bound_propagation_type ( )

inline

Get read-only access to the bound_propagation_type parameter of the configuration.

Default to BoundPropagationType::AUTO

Returns: bound_propagation_type parameter of the configuration

Definition at line 155 of file Config.h.

◆ m_complete()

OptionValue< bool > & dlinear::Config::m_complete ( )

inline

Get read-only access to the complete parameter of the configuration.

Default to false

Returns: complete parameter of the configuration

Definition at line 164 of file Config.h.

◆ m_continuous_output()

OptionValue< bool > & dlinear::Config::m_continuous_output ( )

inline

Get read-only access to the continuous_output parameter of the configuration.

Default to false

Returns: continuous_output parameter of the configuration

Definition at line 165 of file Config.h.

◆ m_csv()

OptionValue< bool > & dlinear::Config::m_csv ( )

inline

Get read-only access to the csv parameter of the configuration.

Default to false

Returns: csv parameter of the configuration

Definition at line 166 of file Config.h.

◆ m_debug_parsing()

OptionValue< bool > & dlinear::Config::m_debug_parsing ( )

inline

Get read-only access to the debug_parsing parameter of the configuration.

Default to false

Returns: debug_parsing parameter of the configuration

Definition at line 167 of file Config.h.

◆ m_debug_scanning()

OptionValue< bool > & dlinear::Config::m_debug_scanning ( )

inline

Get read-only access to the debug_scanning parameter of the configuration.

Default to false

Returns: debug_scanning parameter of the configuration

Definition at line 168 of file Config.h.

◆ m_disable_expansion()

OptionValue< bool > & dlinear::Config::m_disable_expansion ( )

inline

Get read-only access to the disable_expansion parameter of the configuration.

Default to false

Returns: disable_expansion parameter of the configuration

Definition at line 172 of file Config.h.

◆ m_enforce_check_sat()

OptionValue< bool > & dlinear::Config::m_enforce_check_sat ( )

inline

Get read-only access to the enforce_check_sat parameter of the configuration.

Default to false

Returns: enforce_check_sat parameter of the configuration

Definition at line 175 of file Config.h.

◆ m_filename()

OptionValue< std::string > & dlinear::Config::m_filename ( )

inline

Get read-write access to the filename extension of the configuration.

Contains the filename substring after the dot.

Returns: filename extension of the configuration

Definition at line 109 of file Config.h.

◆ m_format()

OptionValue< Format > & dlinear::Config::m_format ( )

inline

Get read-only access to the format parameter of the configuration.

Default to dlinear::Config::Format::AUTO

Returns: format parameter of the configuration

Definition at line 178 of file Config.h.

◆ m_lp_mode()

OptionValue< LPMode > & dlinear::Config::m_lp_mode ( )

inline

Get read-only access to the lp_mode parameter of the configuration.

Default to dlinear::Config::LPMode::AUTO

Returns: lp_mode parameter of the configuration

Definition at line 181 of file Config.h.

◆ m_lp_solver()

OptionValue< LPSolver > & dlinear::Config::m_lp_solver ( )

inline

Get read-only access to the lp_solver parameter of the configuration.

Default to dlinear::Config::LPSolver::SOPLEX

Returns: lp_solver parameter of the configuration

Definition at line 184 of file Config.h.

◆ m_number_of_jobs()

OptionValue< unsigned int > & dlinear::Config::m_number_of_jobs ( )

inline

Get read-only access to the number_of_jobs parameter of the configuration.

Default to 1u

Returns: number_of_jobs parameter of the configuration

Definition at line 185 of file Config.h.

◆ m_onnx_file()

OptionValue< std::string > & dlinear::Config::m_onnx_file ( )

inline

Get read-write access to the onnx_file parameter of the configuration.

Default to ""

Returns: onnx_file parameter of the configuration

Definition at line 113 of file Config.h.

◆ m_optimize()

OptionValue< bool > & dlinear::Config::m_optimize ( )

inline

Get read-only access to the optimize parameter of the configuration.

Default to false

Returns: optimize parameter of the configuration

Definition at line 186 of file Config.h.

◆ m_precision()

OptionValue< double > & dlinear::Config::m_precision ( )

inline

Get read-only access to the precision parameter of the configuration.

Default to 9.999999999999996e-4

Returns: precision parameter of the configuration

Definition at line 191 of file Config.h.

◆ m_produce_models()

OptionValue< bool > & dlinear::Config::m_produce_models ( )

inline

Get read-only access to the produce_models parameter of the configuration.

Default to false

Returns: produce_models parameter of the configuration

Definition at line 194 of file Config.h.

◆ m_random_seed()

OptionValue< unsigned int > & dlinear::Config::m_random_seed ( )

inline

Get read-only access to the random_seed parameter of the configuration.

Default to 0u

Returns: random_seed parameter of the configuration

Definition at line 196 of file Config.h.

◆ m_read_from_stdin()

OptionValue< bool > & dlinear::Config::m_read_from_stdin ( )

inline

Get read-only access to the read_from_stdin parameter of the configuration.

Default to false

Returns: read_from_stdin parameter of the configuration

Definition at line 197 of file Config.h.

◆ m_sat_default_phase()

OptionValue< SatDefaultPhase > & dlinear::Config::m_sat_default_phase ( )

inline

Get read-only access to the sat_default_phase parameter of the configuration.

Default to dlinear::Config::SatDefaultPhase::JeroslowWang

Returns: sat_default_phase parameter of the configuration

Definition at line 200 of file Config.h.

◆ m_sat_solver()

OptionValue< SatSolver > & dlinear::Config::m_sat_solver ( )

inline

Get read-only access to the sat_solver parameter of the configuration.

Default to dlinear::Config::SatSolver::PICOSAT

Returns: sat_solver parameter of the configuration

Definition at line 203 of file Config.h.

◆ m_silent()

OptionValue< bool > & dlinear::Config::m_silent ( )

inline

Get read-only access to the silent parameter of the configuration.

Default to false

Returns: silent parameter of the configuration

Definition at line 204 of file Config.h.

◆ m_simplex_sat_phase()

OptionValue< int > & dlinear::Config::m_simplex_sat_phase ( )

inline

Get read-only access to the simplex_sat_phase parameter of the configuration.

Default to 1

Returns: simplex_sat_phase parameter of the configuration

Definition at line 205 of file Config.h.

◆ m_skip_check_sat()

OptionValue< bool > & dlinear::Config::m_skip_check_sat ( )

inline

Get read-only access to the skip_check_sat parameter of the configuration.

Default to false

Returns: skip_check_sat parameter of the configuration

Definition at line 206 of file Config.h.

◆ m_verbose_dlinear()

OptionValue< int > & dlinear::Config::m_verbose_dlinear ( )

inline

Get read-only access to the verbose_dlinear parameter of the configuration.

Default to 2

Returns: verbose_dlinear parameter of the configuration

Definition at line 207 of file Config.h.

◆ m_verbose_simplex()

OptionValue< int > & dlinear::Config::m_verbose_simplex ( )

inline

Get read-only access to the verbose_simplex parameter of the configuration.

Default to 0

Returns: verbose_simplex parameter of the configuration

Definition at line 208 of file Config.h.

◆ m_verify()

OptionValue< bool > & dlinear::Config::m_verify ( )

inline

Get read-only access to the verify parameter of the configuration.

Default to false

Returns: verify parameter of the configuration

Definition at line 209 of file Config.h.

◆ m_with_timings()

OptionValue< bool > & dlinear::Config::m_with_timings ( )

inline

Get read-only access to the with_timings parameter of the configuration.

Default to false

Returns: with_timings parameter of the configuration

Definition at line 210 of file Config.h.

◆ needs_expansion()

bool dlinear::Config::needs_expansion ( ) const

nodiscard

Get read-only access to the need for input expansion of the  configuration.

It is true when the input format is Format::SMT2 or Format::VNNLIB, false if Format::MPS

Returns: need for input expansion of the configuration

Definition at line 20 of file Config.cpp.

◆ number_of_jobs()

const unsigned int & dlinear::Config::number_of_jobs ( ) const

inlinenodiscard

Get read-write access to the number_of_jobs parameter of the configuration.

Default to 1u

Returns: number_of_jobs parameter of the configuration

Definition at line 185 of file Config.h.

◆ onnx_file()

std::string dlinear::Config::onnx_file ( ) const

inlinenodiscard

Get read-only access to the onnx_file parameter of the configuration.

Default to ""

Returns: onnx_file parameter of the configuration

Definition at line 111 of file Config.h.

◆ optimize()

const bool & dlinear::Config::optimize ( ) const

inlinenodiscard

Get read-write access to the optimize parameter of the configuration.

Default to false

Returns: optimize parameter of the configuration

Definition at line 186 of file Config.h.

◆ precision()

const double & dlinear::Config::precision ( ) const

inlinenodiscard

Get read-write access to the precision parameter of the configuration.

Default to 9.999999999999996e-4

Returns: precision parameter of the configuration

Definition at line 191 of file Config.h.

◆ produce_models()

const bool & dlinear::Config::produce_models ( ) const

inlinenodiscard

Get read-write access to the produce_models parameter of the configuration.

Default to false

Returns: produce_models parameter of the configuration

Definition at line 194 of file Config.h.

◆ random_seed()

const unsigned int & dlinear::Config::random_seed ( ) const

inlinenodiscard

Get read-write access to the random_seed parameter of the configuration.

Default to 0u

Returns: random_seed parameter of the configuration

Definition at line 196 of file Config.h.

◆ read_from_stdin()

const bool & dlinear::Config::read_from_stdin ( ) const

inlinenodiscard

Get read-write access to the read_from_stdin parameter of the configuration.

Default to false

Returns: read_from_stdin parameter of the configuration

Definition at line 197 of file Config.h.

◆ sat_default_phase()

const SatDefaultPhase & dlinear::Config::sat_default_phase ( ) const

inlinenodiscard

Get read-write access to the sat_default_phase parameter of the configuration.

Default to dlinear::Config::SatDefaultPhase::JeroslowWang

Returns: sat_default_phase parameter of the configuration

Definition at line 200 of file Config.h.

◆ sat_solver()

const SatSolver & dlinear::Config::sat_solver ( ) const

inlinenodiscard

Get read-write access to the sat_solver parameter of the configuration.

Default to dlinear::Config::SatSolver::PICOSAT

Returns: sat_solver parameter of the configuration

Definition at line 203 of file Config.h.

◆ silent()

const bool & dlinear::Config::silent ( ) const

inlinenodiscard

Get read-write access to the silent parameter of the configuration.

Default to false

Returns: silent parameter of the configuration

Definition at line 204 of file Config.h.

◆ simplex_sat_phase()

const int & dlinear::Config::simplex_sat_phase ( ) const

inlinenodiscard

Get read-write access to the simplex_sat_phase parameter of the configuration.

Default to 1

Returns: simplex_sat_phase parameter of the configuration

Definition at line 205 of file Config.h.

◆ skip_check_sat()

const bool & dlinear::Config::skip_check_sat ( ) const

inlinenodiscard

Get read-write access to the skip_check_sat parameter of the configuration.

Default to false

Returns: skip_check_sat parameter of the configuration

Definition at line 206 of file Config.h.

◆ verbose_dlinear()

const int & dlinear::Config::verbose_dlinear ( ) const

inlinenodiscard

Get read-write access to the verbose_dlinear parameter of the configuration.

Default to 2

Returns: verbose_dlinear parameter of the configuration

Definition at line 207 of file Config.h.

◆ verbose_simplex()

const int & dlinear::Config::verbose_simplex ( ) const

inlinenodiscard

Get read-write access to the verbose_simplex parameter of the configuration.

Default to 0

Returns: verbose_simplex parameter of the configuration

Definition at line 208 of file Config.h.

◆ verify()

const bool & dlinear::Config::verify ( ) const

inlinenodiscard

Get read-write access to the verify parameter of the configuration.

Default to false

Returns: verify parameter of the configuration

Definition at line 209 of file Config.h.

◆ with_timings()

const bool & dlinear::Config::with_timings ( ) const

inlinenodiscard

Get read-write access to the with_timings parameter of the configuration.

Default to false

Returns: with_timings parameter of the configuration

Definition at line 210 of file Config.h.

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

dlinear/util/Config.h
dlinear/util/Config.cpp

Public Types

Public Member Functions

Detailed Description

Member Enumeration Documentation

◆ BoundPropagationType

◆ Format

◆ LPMode

◆ LPSolver

◆ PreprocessingRunningFrequency

◆ SatDefaultPhase

◆ SatSolver

Constructor & Destructor Documentation

◆ Config() [1/2]

◆ Config() [2/2]

Member Function Documentation

◆ actual_bound_implication_frequency()

◆ actual_bound_propagation_frequency()

◆ actual_bound_propagation_type()

◆ actual_format()

◆ actual_lp_mode()

◆ bound_implication_frequency()

◆ bound_propagation_frequency()

◆ bound_propagation_type()

◆ complete()

◆ continuous_output()

◆ csv()

◆ debug_parsing()

◆ debug_scanning()

◆ disable_expansion()

◆ enforce_check_sat()

◆ filename()

◆ filename_extension()

◆ format()

◆ lp_mode()

◆ lp_solver()

◆ m_bound_implication_frequency()

◆ m_bound_propagation_frequency()

◆ m_bound_propagation_type()

◆ m_complete()

◆ m_continuous_output()

◆ m_csv()

◆ m_debug_parsing()

◆ m_debug_scanning()

◆ m_disable_expansion()

◆ m_enforce_check_sat()

◆ m_filename()

◆ m_format()

◆ m_lp_mode()

◆ m_lp_solver()

◆ m_number_of_jobs()

◆ m_onnx_file()

◆ m_optimize()

◆ m_precision()

◆ m_produce_models()

◆ m_random_seed()

◆ m_read_from_stdin()

◆ m_sat_default_phase()

◆ m_sat_solver()

◆ m_silent()

◆ m_simplex_sat_phase()

◆ m_skip_check_sat()

◆ m_verbose_dlinear()

◆ m_verbose_simplex()

◆ m_verify()

◆ m_with_timings()

◆ needs_expansion()

◆ number_of_jobs()

◆ onnx_file()

◆ optimize()

◆ precision()

◆ produce_models()

◆ random_seed()

◆ read_from_stdin()

◆ sat_default_phase()

◆ sat_solver()

◆ silent()

◆ simplex_sat_phase()

◆ skip_check_sat()

◆ verbose_dlinear()

◆ verbose_simplex()