smtrat::mcsat Namespace Reference

Namespaces
	arithmetic
	constraint_type
	fm
	A Fourier-Motzkin based backend.
	icp
	nlsat
	onecell
	onecellcad
	smtaf
	variableordering
	vs

Data Structures
struct	SequentialAssignment
struct	FastParallelExplanation
	This explanation executes all given explanation in parallel processes and waits for the fastest explanation, returning the fastest delivered explanation, terminating all other parallel processes. More...
struct	FullParallelExplanation
	This explanation executes all given explanation parallel in multiple threads and waits until every single one has finished, returning the result of the first listed explanation. More...
struct	ParallelExplanation
struct	SequentialExplanation
class	Bookkeeping
	Represent the trail, i.e. More...
class	ClauseChain
	An explanation is either a single clause or a chain of clauses, satisfying the following properties: More...
class	MCSATBackend
struct	InformationGetter
struct	TheoryLevel
class	MCSATMixin
struct	Base
struct	MCSATSettingsDefault
struct	MCSATSettingsNL
struct	MCSATSettingsFMICPVSNL
struct	MCSATSettingsOC
struct	MCSATSettingsOCNN
struct	MCSATSettingsOCNNASC
struct	MCSATSettingsOCNNDSC
struct	MCSATSettingsOCLWH11
struct	MCSATSettingsOCLWH12
struct	MCSATSettingsOCLWH13
struct	MCSATSettingsOCLWH21
struct	MCSATSettingsOCLWH22
struct	MCSATSettingsOCLWH23
struct	MCSATSettingsOCLWH31
struct	MCSATSettingsOCLWH32
struct	MCSATSettingsOCLWH33
struct	MCSATSettingsFMICPVSOCLWH11
struct	MCSATSettingsFMICPVSOCLWH12
struct	MCSATSettingsFMICPVSOCLWH13
struct	MCSATSettingsFMICPVSOCNNASC
struct	MCSATSettingsFMICPVSOCNNDSC
struct	MCSATSettingsFMICPVSOCPARALLEL
struct	MCSATSettingsOCPARALLEL
struct	MCSATSettingsOCNew
struct	MCSATSettingsFMICPVSOCNew
struct	MCSATSettingsVSOCNew
struct	MCSATSettingsFMOCNew
struct	MCSATSettingsFMICPVSOCNewOC
struct	MCSATSettingsFMVSOC
struct	MCSATSettingsFMICPVSOC
struct	MCSATSettingsFMICPOC
struct	MCSATSettingsFMNL
struct	MCSATSettingsVSNL
struct	MCSATSettingsFMVSNL
struct	MCSATSettingsICPNL
struct	MCSAT_AF_NL
struct	MCSAT_AF_OCNL
struct	MCSAT_AF_FMOCNL
struct	MCSAT_AF_FMICPOCNL
struct	MCSAT_AF_FMICPVSOCNL
struct	MCSAT_AF_FMVSOCNL
struct	MCSAT_SMT_FMOCNL

Typedefs
typedef allocator< std::optional< Explanation >, managed_shared_memory::segment_manager >	ShmemAllocator
typedef vector< std::optional< Explanation >, ShmemAllocator >	SharedVector
using	ModelValues = std::vector< std::pair< carl::Variable, ModelValue > >
using	AssignmentOrConflict = std::variant< ModelValues, FormulasT >
using	Explanation = std::variant< FormulaT, ClauseChain >

Enumerations
enum class	ConstraintType { Constant , Assigned , Univariate , Unassigned }
	This type categorizes constraints with respect to a given (partial) model and the next variable to be assigned. More...
enum class	VariableOrdering {   GreedyMaxUnivariate , FeatureBased , FeatureBasedZ3 , FeatureBasedBrown ,   FeatureBasedTriangular , FeatureBasedLexicographic , FeatureBasedPickering }

Functions
FormulaT	resolveExplanation (const Explanation &expl)
std::ostream &	operator<< (std::ostream &os, const Bookkeeping &bk)
FormulaT	_transformToImplicationChain (const FormulaT &formula, const Model &model, ClauseChain &chain, bool outermost, bool withEquivalences)
std::ostream &	operator<< (std::ostream &stream, const ClauseChain::Link &link)
std::ostream &	operator<< (std::ostream &stream, const ClauseChain &chain)
std::ostream &	operator<< (std::ostream &os, ConstraintType ct)
template<typename P >
std::vector< carl::BasicConstraint< P > >	constr_from_vc (const carl::VariableComparison< P > &vc, const carl::Assignment< typename P::RootType > assignment, bool tarski=false)
std::string	get_name (VariableOrdering ordering)
std::ostream &	operator<< (std::ostream &os, VariableOrdering ordering)
template<VariableOrdering vot, typename Constraints >
std::vector< carl::Variable >	calculate_variable_order (const Constraints &c)
template<VariableOrdering vot>
std::vector< carl::Variable >	calculate_variable_order (const std::vector< ConstraintT > &constraints)
template<typename Settings >
std::ostream &	operator<< (std::ostream &os, const MCSATBackend< Settings > &backend)

Typedef Documentation

AssignmentOrConflict

using smtrat::mcsat::AssignmentOrConflict = typedef std::variant<ModelValues,FormulasT>

Definition at line 13 of file smtrat-mcsat.h.

Explanation

using smtrat::mcsat::Explanation = typedef std::variant<FormulaT, ClauseChain>

Definition at line 14 of file smtrat-mcsat.h.

ModelValues

using smtrat::mcsat::ModelValues = typedef std::vector<std::pair<carl::Variable, ModelValue> >

Definition at line 12 of file smtrat-mcsat.h.

SharedVector

typedef vector<std::optional<Explanation> , ShmemAllocator> smtrat::mcsat::SharedVector

Definition at line 17 of file FastParallelExplanation.h.

ShmemAllocator

typedef allocator<std::optional<Explanation> , managed_shared_memory::segment_manager> smtrat::mcsat::ShmemAllocator

Definition at line 16 of file FastParallelExplanation.h.

Enumeration Type Documentation

ConstraintType

enum smtrat::mcsat::ConstraintType

strong

This type categorizes constraints with respect to a given (partial) model and the next variable to be assigned.

Note that Constant implies Assigned.

Enumerator
Constant
Assigned	The constraint contains no variables.
Univariate	The constraint is fully assigned.
Unassigned	The constraint has a single unassigned variable being the next one. The constraint has an unassigned variable that is not the next one.

Definition at line 17 of file ConstraintCategorization.h.

VariableOrdering

enum smtrat::mcsat::VariableOrdering

strong

Enumerator
GreedyMaxUnivariate
FeatureBased
FeatureBasedZ3
FeatureBasedBrown
FeatureBasedTriangular
FeatureBasedLexicographic
FeatureBasedPickering

Definition at line 9 of file VariableOrdering.h.

Function Documentation

_transformToImplicationChain()

FormulaT smtrat::mcsat::_transformToImplicationChain	(	const FormulaT &	formula,
		const Model &	model,
		ClauseChain &	chain,
		bool	outermost,
		bool	withEquivalences
	)

Definition at line 70 of file ClauseChain.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

calculate_variable_order() [1/2]

template<VariableOrdering vot, typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::calculate_variable_order

(

const Constraints &

c

)

Definition at line 36 of file VariableOrdering.h.

calculate_variable_order() [2/2]

template<VariableOrdering vot>

std::vector<carl::Variable> smtrat::mcsat::calculate_variable_order

(

const std::vector< ConstraintT > &

constraints

)

Definition at line 49 of file VariableOrdering.h.

Here is the call graph for this function:

constr_from_vc()

template<typename P >

std::vector<carl::BasicConstraint<P> > smtrat::mcsat::constr_from_vc ( const carl::VariableComparison< P > &  vc, const carl::Assignment< typename P::RootType >  assignment, bool  tarski = false  )

inline

Definition at line 6 of file RootExpr.h.

Here is the call graph for this function:

Here is the caller graph for this function:

get_name()

std::string smtrat::mcsat::get_name ( VariableOrdering  ordering )

inline

Definition at line 19 of file VariableOrdering.h.

Here is the caller graph for this function:

operator<<() [1/6]

std::ostream& smtrat::mcsat::operator<< ( std::ostream &  os, const Bookkeeping &  bk  )

inline

Definition at line 107 of file Bookkeeping.h.

Here is the call graph for this function:

operator<<() [2/6]

template<typename Settings >

std::ostream& smtrat::mcsat::operator<<	(	std::ostream &	os,
		const MCSATBackend< Settings > &	backend
	)

Definition at line 149 of file BaseBackend.h.

Here is the call graph for this function:

operator<<() [3/6]

std::ostream& smtrat::mcsat::operator<< ( std::ostream &  os, ConstraintType  ct  )

inline

Definition at line 23 of file ConstraintCategorization.h.

operator<<() [4/6]

std::ostream& smtrat::mcsat::operator<< ( std::ostream &  os, VariableOrdering  ordering  )

inline

Definition at line 31 of file VariableOrdering.h.

Here is the call graph for this function:

operator<<() [5/6]

std::ostream& smtrat::mcsat::operator<< ( std::ostream &  stream, const ClauseChain &  chain  )

inline

Definition at line 153 of file ClauseChain.h.

operator<<() [6/6]

std::ostream& smtrat::mcsat::operator<< ( std::ostream &  stream, const ClauseChain::Link &  link  )

inline

Definition at line 142 of file ClauseChain.h.

resolveExplanation()

FormulaT smtrat::mcsat::resolveExplanation ( const Explanation &  expl )

inline

Definition at line 16 of file smtrat-mcsat.h.