#include <CSplitModule.h>

Inheritance diagram for smtrat::CSplitModule< Settings >:

Collaboration diagram for smtrat::CSplitModule< Settings >:

[legend]

Data Structures
struct	Expansion
	Represents the quotients and remainders of a variable in a positional notation to the basis Settings::expansionBase. More...

struct	LAModule
	Linear arithmetic module to call for the linearized formula. More...

struct	Linearization
	Represents the class of all original constraints with the same left hand side after a normalization. More...

struct	Purification
	Represents the substitution variables of a nonlinear monomial in a positional notation to the basis Settings::expansionBase. More...

Public Types
typedef Settings	SettingsType

enum class	LemmaType : unsigned { NORMAL = 0 , PERMANENT = 1 }

Public Member Functions
std::string	moduleName () const

	CSplitModule (const ModuleInput _formula, Conditionals &_conditionals, Manager _manager=nullptr)

bool	addCore (ModuleInput::const_iterator _subformula)
	The module has to take the given sub-formula of the received formula into account. More...

void	removeCore (ModuleInput::const_iterator _subformula)
	Removes the subformula of the received formula at the given position to the considered ones of this module. More...

void	updateModel () const
	Updates the current assignment into the model. More...

Answer	checkCore ()
	Checks the received formula for consistency. More...

bool	inform (const FormulaT &_constraint)
	Informs the module about the given constraint. More...

void	deinform (const FormulaT &_constraint)
	The inverse of informing about a constraint. More...

virtual void	init ()
	Informs all backends about the so far encountered constraints, which have not yet been communicated. More...

bool	add (ModuleInput::const_iterator _subformula)
	The module has to take the given sub-formula of the received formula into account. More...

virtual Answer	check (bool _final=false, bool _full=true, carl::Variable _objective=carl::Variable::NO_VARIABLE)
	Checks the received formula for consistency. More...

virtual void	remove (ModuleInput::const_iterator _subformula)
	Removes everything related to the given sub-formula of the received formula. More...

virtual void	updateAllModels ()
	Updates all satisfying models, if the solver has detected the consistency of the received formula, beforehand. More...

virtual std::list< std::vector< carl::Variable > >	getModelEqualities () const
	Partition the variables from the current model into equivalence classes according to their assigned value. More...

unsigned	currentlySatisfiedByBackend (const FormulaT &_formula) const

virtual unsigned	currentlySatisfied (const FormulaT &) const

bool	receivedVariable (carl::Variable::Arg _var) const

Answer	solverState () const

std::size_t	id () const

void	setId (std::size_t _id)
	Sets this modules unique ID to identify itself. More...

thread_priority	threadPriority () const

void	setThreadPriority (thread_priority _threadPriority)
	Sets the priority of this module to get a thread for running its check procedure. More...

const ModuleInput *	pReceivedFormula () const

const ModuleInput &	rReceivedFormula () const

const ModuleInput *	pPassedFormula () const

const ModuleInput &	rPassedFormula () const

const Model &	model () const

const std::vector< Model > &	allModels () const

const std::vector< FormulaSetT > &	infeasibleSubsets () const

const std::vector< Module * > &	usedBackends () const

const carl::FastSet< FormulaT > &	constraintsToInform () const

const carl::FastSet< FormulaT > &	informedConstraints () const

void	addLemma (const FormulaT &_lemma, const LemmaType &_lt=LemmaType::NORMAL, const FormulaT &_preferredFormula=FormulaT(carl::FormulaType::TRUE))
	Stores a lemma being a valid formula. More...

bool	hasLemmas ()
	Checks whether this module or any of its backends provides any lemmas. More...

void	clearLemmas ()
	Deletes all yet found lemmas. More...

const std::vector< Lemma > &	lemmas () const

ModuleInput::const_iterator	firstUncheckedReceivedSubformula () const

ModuleInput::const_iterator	firstSubformulaToPass () const

void	receivedFormulaChecked ()
	Notifies that the received formulas has been checked. More...

const smtrat::Conditionals &	answerFound () const

bool	isPreprocessor () const

carl::Variable	objective () const

bool	is_minimizing () const

void	excludeNotReceivedVariablesFromModel () const
	Excludes all variables from the current model, which do not occur in the received formula. More...

void	updateLemmas ()
	Stores all lemmas of any backend of this module in its own lemma vector. More...

void	collectTheoryPropagations ()

void	collectOrigins (const FormulaT &_formula, FormulasT &_origins) const
	Collects the formulas in the given formula, which are part of the received formula. More...

void	collectOrigins (const FormulaT &_formula, FormulaSetT &_origins) const

bool	hasValidInfeasibleSubset () const

void	checkInfSubsetForMinimality (std::vector< FormulaSetT >::const_iterator _infsubset, const std::string &_filename="smaller_muses", unsigned _maxSizeDifference=1) const
	Checks the given infeasible subset for minimality by storing all subsets of it, which have a smaller size which differs from the size of the infeasible subset not more than the given threshold. More...

virtual std::pair< bool, FormulaT >	getReceivedFormulaSimplified ()

void	print (const std::string &_initiation="***") const
	Prints everything relevant of the solver. More...

void	printReceivedFormula (const std::string &_initiation="***") const
	Prints the vector of the received formula. More...

void	printPassedFormula (const std::string &_initiation="***") const
	Prints the vector of passed formula. More...

void	printInfeasibleSubsets (const std::string &_initiation="***") const
	Prints the infeasible subsets. More...

void	printModel (std::ostream &_out=std::cout) const
	Prints the assignment of this module satisfying its received formula if it satisfiable and this module could find an assignment. More...

void	printAllModels (std::ostream &_out=std::cout)
	Prints all assignments of this module satisfying its received formula if it satisfiable and this module could find an assignment. More...

Static Public Member Functions
static void	freeSplittingVariable (const FormulaT &_splittingVariable)

Static Public Attributes
static size_t	mNumOfBranchVarsToStore = 5
	The number of different variables to consider for a probable infinite loop of branchings. More...

static std::vector< Branching >	mLastBranches = std::vector<Branching>(mNumOfBranchVarsToStore, Branching(typename Poly::PolyType(), 0))
	Stores the last branches in a cycle buffer. More...

static size_t	mFirstPosInLastBranches = 0
	The beginning of the cyclic buffer storing the last branches. More...

static std::vector< FormulaT >	mOldSplittingVariables
	Reusable splitting variables. More...

Protected Member Functions
virtual bool	informCore ([[maybe_unused]] const FormulaT &_constraint)
	Informs the module about the given constraint. More...

virtual void	deinformCore ([[maybe_unused]] const FormulaT &_constraint)
	The inverse of informing about a constraint. More...

virtual bool	addCore ([[maybe_unused]] ModuleInput::const_iterator formula)
	The module has to take the given sub-formula of the received formula into account. More...

virtual void	removeCore ([[maybe_unused]] ModuleInput::const_iterator formula)
	Removes everything related to the given sub-formula of the received formula. More...

bool	anAnswerFound () const
	Checks for all antecedent modules and those which run in parallel with the same antecedent modules, whether one of them has determined a result. More...

void	clearModel () const
	Clears the assignment, if any was found. More...

void	clearModels () const
	Clears all assignments, if any was found. More...

void	cleanModel () const
	Substitutes variable occurrences by its model value in the model values of other variables. More...

ModuleInput::iterator	passedFormulaBegin ()

ModuleInput::iterator	passedFormulaEnd ()

void	addOrigin (ModuleInput::iterator _formula, const FormulaT &_origin)
	Adds the given set of formulas in the received formula to the origins of the given passed formula. More...

const FormulaT &	getOrigins (ModuleInput::const_iterator _formula) const
	Gets the origins of the passed formula at the given position. More...

void	getOrigins (const FormulaT &_formula, FormulasT &_origins) const

void	getOrigins (const FormulaT &_formula, FormulaSetT &_origins) const

std::pair< ModuleInput::iterator, bool >	removeOrigin (ModuleInput::iterator _formula, const FormulaT &_origin)

std::pair< ModuleInput::iterator, bool >	removeOrigins (ModuleInput::iterator _formula, const std::shared_ptr< std::vector< FormulaT >> &_origins)

void	informBackends (const FormulaT &_constraint)
	Informs all backends of this module about the given constraint. More...

virtual void	addConstraintToInform (const FormulaT &_constraint)
	Adds a constraint to the collection of constraints of this module, which are informed to a freshly generated backend. More...

std::pair< ModuleInput::iterator, bool >	addReceivedSubformulaToPassedFormula (ModuleInput::const_iterator _subformula)
	Copies the given sub-formula of the received formula to the passed formula. More...

bool	originInReceivedFormula (const FormulaT &_origin) const

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula)
	Adds the given formula to the passed formula with no origin. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, const std::shared_ptr< std::vector< FormulaT >> &_origins)
	Adds the given formula to the passed formula. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, const FormulaT &_origin)
	Adds the given formula to the passed formula. More...

void	generateTrivialInfeasibleSubset ()
	Stores the trivial infeasible subset being the set of received formulas. More...

void	receivedFormulasAsInfeasibleSubset (ModuleInput::const_iterator _subformula)
	Stores an infeasible subset consisting only of the given received formula. More...

std::vector< FormulaT >::const_iterator	findBestOrigin (const std::vector< FormulaT > &_origins) const

void	getInfeasibleSubsets ()
	Copies the infeasible subsets of the passed formula. More...

std::vector< FormulaSetT >	getInfeasibleSubsets (const Module &_backend) const
	Get the infeasible subsets the given backend provides. More...

const Model &	backendsModel () const
	Stores the model of a backend which determined satisfiability of the passed formula in the model of this module. More...

void	getBackendsModel () const

void	getBackendsAllModels () const
	Stores all models of a backend in the list of all models of this module. More...

virtual Answer	runBackends (bool _final, bool _full, carl::Variable _objective)
	Runs the backend solvers on the passed formula. More...

virtual Answer	runBackends ()

virtual ModuleInput::iterator	eraseSubformulaFromPassedFormula (ModuleInput::iterator _subformula, bool _ignoreOrigins=false)
	Removes everything related to the sub-formula to remove from the passed formula in the backends of this module. More...

void	clearPassedFormula ()

std::vector< FormulaT >	merge (const std::vector< FormulaT > &, const std::vector< FormulaT > &) const
	Merges the two vectors of sets into the first one. More...

size_t	determine_smallest_origin (const std::vector< FormulaT > &origins) const

bool	probablyLooping (const typename Poly::PolyType &_branchingPolynomial, const Rational &_branchingValue) const
	Checks whether given the current branching value and branching variable/polynomial it is (highly) probable that this branching is part of an infinite loop of branchings. More...

bool	branchAt (const Poly &_polynomial, bool _integral, const Rational &_value, std::vector< FormulaT > &&_premise, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false)
	Adds a lemmas which provoke a branching for the given variable at the given value, if this module returns Unknown and there exists a preceding SATModule. More...

bool	branchAt (const Poly &_polynomial, bool _integral, const Rational &_value, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false, const std::vector< FormulaT > &_premise=std::vector< FormulaT >())

bool	branchAt (carl::Variable::Arg _var, const Rational &_value, std::vector< FormulaT > &&_premise, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false)

bool	branchAt (carl::Variable::Arg _var, const Rational &_value, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false, const std::vector< FormulaT > &_premise=std::vector< FormulaT >())

void	splitUnequalConstraint (const FormulaT &)
	Adds the following lemmas for the given constraint p!=0. More...

unsigned	checkModel () const

void	addInformationRelevantFormula (const FormulaT &formula)
	Adds a formula to the InformationRelevantFormula. More...

const std::set< FormulaT > &	getInformationRelevantFormulas ()
	Gets all InformationRelevantFormulas. More...

bool	isLemmaLevel (LemmaLevel level)
	Checks if current lemma level is greater or equal to given level. More...

Static Protected Member Functions
static bool	modelsDisjoint (const Model &_modelA, const Model &_modelB)
	Checks whether there is no variable assigned by both models. More...

Protected Attributes
std::vector< FormulaSetT >	mInfeasibleSubsets
	Stores the infeasible subsets. More...

Manager *const	mpManager
	A reference to the manager. More...

Model	mModel
	Stores the assignment of the current satisfiable result, if existent. More...

std::vector< Model >	mAllModels
	Stores all satisfying assignments. More...

bool	mModelComputed
	True, if the model has already been computed. More...

bool	mFinalCheck
	true, if the check procedure should perform a final check which especially means not to postpone splitting decisions More...

bool	mFullCheck
	false, if this module should avoid too expensive procedures and rather return unknown instead. More...

carl::Variable	mObjectiveVariable
	Objective variable to be minimized. If set to NO_VARIABLE, a normal sat check should be performed. More...

std::vector< TheoryPropagation >	mTheoryPropagations

std::atomic< Answer >	mSolverState
	States whether the received formula is known to be satisfiable or unsatisfiable otherwise it is set to unknown. More...

std::atomic_bool *	mBackendsFoundAnswer
	This flag is passed to any backend and if it determines an answer to a prior check call, this flag is fired. More...

Conditionals	mFoundAnswer
	Vector of Booleans: If any of them is true, we have to terminate a running check procedure. More...

std::vector< Module * >	mUsedBackends
	The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula). More...

std::vector< Module * >	mAllBackends
	The backends of this module which have been used. More...

std::vector< Lemma >	mLemmas
	Stores the lemmas being valid formulas this module or its backends made. More...

ModuleInput::iterator	mFirstSubformulaToPass
	Stores the position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends. More...

carl::FastSet< FormulaT >	mConstraintsToInform
	Stores the constraints which the backends must be informed about. More...

carl::FastSet< FormulaT >	mInformedConstraints
	Stores the position of the first constraint of which no backend has been informed about. More...

ModuleInput::const_iterator	mFirstUncheckedReceivedSubformula
	Stores the position of the first (by this module) unchecked sub-formula of the received formula. More...

unsigned	mSmallerMusesCheckCounter
	Counter used for the generation of the smt2 files to check for smaller muses. More...

std::vector< std::size_t >	mVariableCounters
	Maps variables to the number of their occurrences. More...

Private Types
enum class	DomainSize { SMALL = 0 , LARGE = 1 , UNBOUNDED = 2 }
	Subdivides the size of a variable domain into three classes: More...

Private Member Functions
bool	resetExpansions ()
	Resets all expansions to the center points of the variable domains and constructs a new tree of reductions for the currently active monomials. More...

bool	bloatDomains (const FormulaSetT &LRAConflict)
	Bloats the active domains of a subset of variables that are part of the LRA solvers infeasible subset, and indicates if no active domain could be bloated, because the maximal domain of all variables were reached. More...

Answer	analyzeConflict (const FormulaSetT &LRAConflict)
	Analyzes the infeasible subset of the LRA solver and constructs an infeasible subset of the received constraints. More...

void	changeActiveDomain (Expansion &expansion, RationalInterval &&domain)
	Changes the active domain of a variable and adapts its positional notation to the basis Settings::expansionBase. More...

void	propagateFormula (const FormulaT &formula, bool assert)
	Asserts/Removes the given formula to/from the LRA solver. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, bool _hasSingleOrigin, const FormulaT &_origin, const std::shared_ptr< std::vector< FormulaT >> &_origins, bool _mightBeConjunction)
	This method actually implements the adding of a formula to the passed formula. More...

Answer	foundAnswer (Answer _answer)
	Sets the solver state to the given answer value. More...

Private Attributes
std::map< carl::Monomial::Arg, Purification >	mPurifications
	Maps a monomial to its purification information. More...

Bimap< Expansion, const carl::Variable, &Expansion::mRationalization, const carl::Variable, &Expansion::mDiscretization >	mExpansions

Bimap< Linearization, const Poly, &Linearization::mNormalization, const Poly, &Linearization::mLinearization >	mLinearizations

vb::VariableBounds< FormulaT >	mVariableBounds
	Helper class that extracts the variable domains. More...

Model	mLRAModel
	Stores the last model for the linearization that was found by the LRA solver. More...

bool	mCheckedWithBackends
	Stores whether the last consistency check was done by the backends. More...

LAModule	mLRAModule
	Handle to the linear arithmetic module. More...

friend	Manager

std::size_t	mId
	A unique ID to identify this module instance. (Could be useful but currently nowhere used) More...

thread_priority	mThreadPriority
	The priority of this module to get a thread for running its check procedure. More...

const ModuleInput *	mpReceivedFormula
	The formula passed to this module. More...

ModuleInput *	mpPassedFormula
	The formula passed to the backends of this module. More...

std::string	mModuleName

ModuleStatistics &	mStatistics = statistics_get<ModuleStatistics>(moduleName())

Detailed Description

template<typename Settings>
class smtrat::CSplitModule< Settings >

Definition at line 23 of file CSplitModule.h.

Member Typedef Documentation

◆ SettingsType

template<typename Settings >

typedef Settings smtrat::CSplitModule< Settings >::SettingsType

Definition at line 148 of file CSplitModule.h.

Member Enumeration Documentation

◆ DomainSize

template<typename Settings >

enum smtrat::CSplitModule::DomainSize

strongprivate

Subdivides the size of a variable domain into three classes:

SMALL, if domain size <= Settings::maxDomainSize
LARGE, if Settings::maxDomainSize < domain size < infinity
UNBOUNDED, if domain size = infinity

Enumerator
SMALL
LARGE
UNBOUNDED

Definition at line 58 of file CSplitModule.h.

◆ LemmaType

enum smtrat::Module::LemmaType : unsigned

stronginherited

Enumerator
NORMAL
PERMANENT

Definition at line 123 of file Module.h.

Constructor & Destructor Documentation

◆ CSplitModule()

template<typename Settings >

smtrat::CSplitModule< Settings >::CSplitModule	(	const ModuleInput *	_formula,
		Conditionals &	_conditionals,
		Manager *	_manager = `nullptr`
	)

Member Function Documentation

◆ add()

bool smtrat::Module::add ( ModuleInput::const_iterator _subformula )

inherited

The module has to take the given sub-formula of the received formula into account.

Parameters

_subformula The sub-formula to take additionally into account.

Returns: false, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; true, otherwise.

Definition at line 138 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addConstraintToInform()

void smtrat::Module::addConstraintToInform ( const FormulaT & _constraint )

protectedvirtualinherited

Adds a constraint to the collection of constraints of this module, which are informed to a freshly generated backend.

Parameters

_constraint The constraint to add.

Reimplemented in smtrat::SATModule< Settings >.

Definition at line 877 of file Module.cpp.

Here is the caller graph for this function:

◆ addCore() [1/2]

virtual bool smtrat::Module::addCore ( [[maybe_unused] ] ModuleInput::const_iterator formula )

inlineprotectedvirtualinherited

The module has to take the given sub-formula of the received formula into account.

Parameters

formula The sub-formula to take additionally into account.

Returns: false, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; true, otherwise.

Definition at line 706 of file Module.h.

Here is the caller graph for this function:

◆ addCore() [2/2]

template<typename Settings >

bool smtrat::CSplitModule< Settings >::addCore ( ModuleInput::const_iterator _subformula )

The module has to take the given sub-formula of the received formula into account.

Parameters

_subformula The sub-formula to take additionally into account.

Returns: False, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; True, otherwise.

◆ addInformationRelevantFormula()

void smtrat::Module::addInformationRelevantFormula ( const FormulaT & formula )

protectedinherited

Adds a formula to the InformationRelevantFormula.

Parameters

formula Formula to add

Definition at line 1068 of file Module.cpp.

Here is the call graph for this function:

◆ addLemma()

void smtrat::Module::addLemma	(	const FormulaT &	_lemma,
		const LemmaType &	_lt = `LemmaType::NORMAL`,
		const FormulaT &	_preferredFormula = `FormulaT( carl::FormulaType::TRUE )`
	)

inlineinherited

Stores a lemma being a valid formula.

Parameters

_lemma	The eduction/lemma to store.
_lt	The type of the lemma.
_preferredFormula	Hint for the next decision, which formula should be assigned to true.

Definition at line 521 of file Module.h.

Here is the call graph for this function:

◆ addOrigin()

void smtrat::Module::addOrigin	(	ModuleInput::iterator	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Adds the given set of formulas in the received formula to the origins of the given passed formula.

Parameters

_formula	The passed formula to set the origins for.
_origin	A set of formulas in the received formula of this module.

Definition at line 798 of file Module.h.

Here is the call graph for this function:

◆ addReceivedSubformulaToPassedFormula()

std::pair<ModuleInput::iterator,bool> smtrat::Module::addReceivedSubformulaToPassedFormula ( ModuleInput::const_iterator _subformula )

inlineprotectedinherited

Copies the given sub-formula of the received formula to the passed formula.

Note, that there is always a link between sub-formulas of the passed formulas to sub-formulas of the received formulas, which are responsible for its occurrence.

Parameters

_subformula The sub-formula of the received formula to copy.

Definition at line 857 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addSubformulaToPassedFormula() [1/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula ( const FormulaT & _formula )

inlineprotectedinherited

Adds the given formula to the passed formula with no origin.

Note that in the next call of this module's removeSubformula, all formulas in the passed formula without origins will be removed.

Parameters

_formula The formula to add to the passed formula.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 873 of file Module.h.

Here is the caller graph for this function:

◆ addSubformulaToPassedFormula() [2/4]

std::pair< ModuleInput::iterator, bool > smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		bool	_hasSingleOrigin,
		const FormulaT &	_origin,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins,
		bool	_mightBeConjunction
	)

privateinherited

This method actually implements the adding of a formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_hasSingleOrigin	true, if the next argument contains the formula being the single origin.
_origin	The sub-formula of the received formula being responsible for the occurrence of the formula to add to the passed formula.
_origins	The link of the formula to add to the passed formula to sub-formulas of the received formulas, which are responsible for its occurrence
_mightBeConjunction	true, if the formula to add might be a conjunction.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 341 of file Module.cpp.

Here is the call graph for this function:

◆ addSubformulaToPassedFormula() [3/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Adds the given formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_origin	The sub-formula of the received formula being responsible for the occurrence of the formula to add to the passed formula.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 901 of file Module.h.

Here is the call graph for this function:

◆ addSubformulaToPassedFormula() [4/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins
	)

inlineprotectedinherited

Adds the given formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_origins	The link of the formula to add to the passed formula to sub-formulas of the received formulas, which are responsible for its occurrence

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 887 of file Module.h.

Here is the call graph for this function:

◆ allModels()

const std::vector<Model>& smtrat::Module::allModels ( ) const

inlineinherited

Returns: All satisfying assignments, if existent.

Definition at line 471 of file Module.h.

Here is the caller graph for this function:

◆ analyzeConflict()

template<typename Settings >

Answer smtrat::CSplitModule< Settings >::analyzeConflict ( const FormulaSetT & LRAConflict )

private

Analyzes the infeasible subset of the LRA solver and constructs an infeasible subset of the received constraints.

The unsatisfiability cannot be deduced if the corresponding original constraints contain real valued variables.

Parameters

LRAConflict Infeasible subset of the LRA solver

Returns: UNSAT, if an infeasible subset of the received constraints could be constructed; UNKNOWN, otherwise.

◆ anAnswerFound()

bool smtrat::Module::anAnswerFound ( ) const

inlineprotectedinherited

Checks for all antecedent modules and those which run in parallel with the same antecedent modules, whether one of them has determined a result.

Returns: True, if one of them has determined a result.

Definition at line 737 of file Module.h.

Here is the caller graph for this function:

◆ answerFound()

const smtrat::Conditionals& smtrat::Module::answerFound ( ) const

inlineinherited

Returns: A vector of Booleans: If any of them is true, we have to terminate a running check procedure.

Definition at line 597 of file Module.h.

Here is the caller graph for this function:

◆ backendsModel()

const Model & smtrat::Module::backendsModel ( ) const

protectedinherited

Stores the model of a backend which determined satisfiability of the passed formula in the model of this module.

Definition at line 630 of file Module.cpp.

Here is the call graph for this function:

◆ bloatDomains()

template<typename Settings >

bool smtrat::CSplitModule< Settings >::bloatDomains ( const FormulaSetT & LRAConflict )

private

Bloats the active domains of a subset of variables that are part of the LRA solvers infeasible subset, and indicates if no active domain could be bloated, because the maximal domain of all variables were reached.

Parameters

LRAConflict Infeasible subset of the LRA solver

Returns: True, if no active domain was bloated; False, otherwise.

◆ branchAt() [1/4]

bool smtrat::Module::branchAt	(	carl::Variable::Arg	_var,
		const Rational &	_value,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`,
		const std::vector< FormulaT > &	_premise = `std::vector<FormulaT>()`
	)

inlineprotectedinherited

Definition at line 1098 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [2/4]

bool smtrat::Module::branchAt	(	carl::Variable::Arg	_var,
		const Rational &	_value,
		std::vector< FormulaT > &&	_premise,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`
	)

inlineprotectedinherited

Definition at line 1093 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [3/4]

bool smtrat::Module::branchAt	(	const Poly &	_polynomial,
		bool	_integral,
		const Rational &	_value,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`,
		const std::vector< FormulaT > &	_premise = `std::vector<FormulaT>()`
	)

inlineprotectedinherited

Definition at line 1088 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [4/4]

bool smtrat::Module::branchAt	(	const Poly &	_polynomial,
		bool	_integral,
		const Rational &	_value,
		std::vector< FormulaT > &&	_premise,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`
	)

protectedinherited

Adds a lemmas which provoke a branching for the given variable at the given value, if this module returns Unknown and there exists a preceding SATModule.

Note that the given value is rounded down and up, if the given variable is integer-valued.

Parameters

_polynomial	The variable to branch for.
_integral	A flag being true, if all variables in the polynomial to branch for are integral.
_value	The value to branch at.
_premise	The sub-formulas of the received formula from which the branch is followed. Note, that a premise is not necessary, as every branch is a valid formula. But a premise can prevent from branching unnecessarily.
_leftCaseWeak	true, if a branching in the form of (or (<= p b) (> p b)) is desired. false, if a branching in the form of (or (< p b) (>= p b)) is desired.
_preferLeftCase	true, if the left case (polynomial less(or equal) 0 shall be chosen first. false, otherwise.
_useReceivedFormulaAsPremise	true, if the whole received formula should be used as premise

Definition at line 478 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ changeActiveDomain()

template<typename Settings >

void smtrat::CSplitModule< Settings >::changeActiveDomain	(	Expansion &	expansion,
		RationalInterval &&	domain
	)

private

Changes the active domain of a variable and adapts its positional notation to the basis Settings::expansionBase.

Parameters

expansion	Expansion data structure thats keeps all needed informations.
domain	The new domain that shall be active afterwards. Note, that the new domain has to contain the currently active interval.

◆ check()

Answer smtrat::Module::check	(	bool	_final = `false`,
		bool	_full = `true`,
		carl::Variable	_objective = `carl::Variable::NO_VARIABLE`
	)

virtualinherited

Checks the received formula for consistency.

Note, that this is an implementation of the satisfiability check of the conjunction of the so far received formulas, which does actually nothing but passing the problem to its backends. This implementation is only used internally and must be overwritten by any derived module.

Parameters

_final	true, if this satisfiability check will be the last one (for a global sat-check), if its result is SAT
_full	false, if this module should avoid too expensive procedures and rather return unknown instead.
_objective	if not set to NO_VARIABLE, the module should find an assignment minimizing this objective variable; otherwise any assignment is good.

Returns: True, if the received formula is satisfiable; False, if the received formula is not satisfiable; Unknown, otherwise.

Reimplemented in smtrat::PModule.

Definition at line 86 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkCore()

template<typename Settings >

Answer smtrat::CSplitModule< Settings >::checkCore ( )

virtual

Checks the received formula for consistency.

Returns: SAT, if the received formula is satisfiable; UNSAT, if the received formula is not satisfiable; UNKNOWN, otherwise.

Reimplemented from smtrat::Module.

◆ checkInfSubsetForMinimality()

void smtrat::Module::checkInfSubsetForMinimality	(	std::vector< FormulaSetT >::const_iterator	_infsubset,
		const std::string &	_filename = `"smaller_muses"`,
		unsigned	_maxSizeDifference = `1`
	)		const

inherited

Checks the given infeasible subset for minimality by storing all subsets of it, which have a smaller size which differs from the size of the infeasible subset not more than the given threshold.

Parameters

_infsubset	The infeasible subset to check for minimality.
_filename	The name of the file to store the infeasible subsets in order to be able to check their infeasibility.
_maxSizeDifference	The maximal difference between the sizes of the subsets compared to the size of the infeasible subset.

Definition at line 1018 of file Module.cpp.

Here is the call graph for this function:

◆ checkModel()

unsigned smtrat::Module::checkModel ( ) const

protectedinherited

Returns: false, if the current model of this module does not satisfy the current given formula; true, if it cannot be said whether the model satisfies the given formula.

Definition at line 588 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cleanModel()

void smtrat::Module::cleanModel ( ) const

inlineprotectedinherited

Substitutes variable occurrences by its model value in the model values of other variables.

Definition at line 771 of file Module.h.

◆ clearLemmas()

void smtrat::Module::clearLemmas ( )

inlineinherited

Deletes all yet found lemmas.

Definition at line 550 of file Module.h.

Here is the caller graph for this function:

◆ clearModel()

void smtrat::Module::clearModel ( ) const

inlineprotectedinherited

Clears the assignment, if any was found.

Definition at line 749 of file Module.h.

Here is the caller graph for this function:

◆ clearModels()

void smtrat::Module::clearModels ( ) const

inlineprotectedinherited

Clears all assignments, if any was found.

Definition at line 758 of file Module.h.

Here is the call graph for this function:

◆ clearPassedFormula()

void smtrat::Module::clearPassedFormula ( )

protectedinherited

Definition at line 850 of file Module.cpp.

Here is the call graph for this function:

◆ collectOrigins() [1/2]

void smtrat::Module::collectOrigins	(	const FormulaT &	_formula,
		FormulaSetT &	_origins
	)		const

inherited

Definition at line 980 of file Module.cpp.

Here is the call graph for this function:

◆ collectOrigins() [2/2]

void smtrat::Module::collectOrigins	(	const FormulaT &	_formula,
		FormulasT &	_origins
	)		const

inherited

Collects the formulas in the given formula, which are part of the received formula.

If the given formula directly occurs in the received formula, it is inserted into the given set. Otherwise, the given formula must be of type AND and all its sub-formulas part of the received formula. Hence, they will be added to the given set.

Parameters

_formula	The formula from which to collect the formulas being sub-formulas of the received formula (origins).
_origins	The set in which to store the origins.

Definition at line 960 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ collectTheoryPropagations()

void smtrat::Module::collectTheoryPropagations ( )

inherited

Definition at line 928 of file Module.cpp.

◆ constraintsToInform()

const carl::FastSet<FormulaT>& smtrat::Module::constraintsToInform ( ) const

inlineinherited

Returns: The constraints which the backends must be informed about.

Definition at line 496 of file Module.h.

◆ currentlySatisfied()

virtual unsigned smtrat::Module::currentlySatisfied ( const FormulaT & ) const

inlinevirtualinherited

Returns: 0, if the given formula is conflicted by the current model; 1, if the given formula is satisfied by the current model; 2, otherwise; 3, if we do not know anything (default)

Reimplemented in smtrat::LRAModule< Settings >, smtrat::LRAModule< smtrat::LRASettings1 >, and smtrat::LRAModule< smtrat::LRASettingsICP >.

Definition at line 372 of file Module.h.

◆ currentlySatisfiedByBackend()

unsigned smtrat::Module::currentlySatisfiedByBackend ( const FormulaT & _formula ) const

inherited

Returns: 0, if the given formula is conflicted by the current model; 1, if the given formula is satisfied by the current model; 2, otherwise 3, if we do not know anything (default)

Definition at line 296 of file Module.cpp.

◆ deinform()

void smtrat::Module::deinform ( const FormulaT & _constraint )

inherited

The inverse of informing about a constraint.

All data structures which were kept regarding this constraint are going to be removed. Note, that this makes only sense if it is not likely enough that a formula with this constraint must be solved again.

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 124 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deinformCore()

virtual void smtrat::Module::deinformCore ( [[maybe_unused] ] const FormulaT & _constraint )

inlineprotectedvirtualinherited

The inverse of informing about a constraint.

All data structures which were kept regarding this constraint are going to be removed. Note, that this makes only sense if it is not likely enough that a formula with this constraint must be solved again.

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 695 of file Module.h.

Here is the caller graph for this function:

◆ determine_smallest_origin()

size_t smtrat::Module::determine_smallest_origin ( const std::vector< FormulaT > & origins ) const

protectedinherited

Parameters

origins A vector of sets of origins.

Returns: The index of the smallest (regarding the size of the sets) element of origins

Definition at line 403 of file Module.cpp.

◆ eraseSubformulaFromPassedFormula()

ModuleInput::iterator smtrat::Module::eraseSubformulaFromPassedFormula	(	ModuleInput::iterator	_subformula,
		bool	_ignoreOrigins = `false`
	)

protectedvirtualinherited

Removes everything related to the sub-formula to remove from the passed formula in the backends of this module.

Afterwards the sub-formula is removed from the passed formula.

Parameters

_subformula	The sub-formula to remove from the passed formula.
_ignoreOrigins	True, if the sub-formula shall be removed regardless of its origins (should only be applied with expertise).

Returns

Reimplemented in smtrat::ICPModule< Settings >, smtrat::ICPModule< smtrat::ICPSettings1 >, and smtrat::ICPModule< smtrat::ICPSettings4 >.

Definition at line 807 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ excludeNotReceivedVariablesFromModel()

void smtrat::Module::excludeNotReceivedVariablesFromModel ( ) const

inherited

Excludes all variables from the current model, which do not occur in the received formula.

Definition at line 884 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ findBestOrigin()

std::vector< FormulaT >::const_iterator smtrat::Module::findBestOrigin ( const std::vector< FormulaT > & _origins ) const

protectedinherited

Parameters

_origins

Returns

Definition at line 691 of file Module.cpp.

Here is the caller graph for this function:

◆ firstSubformulaToPass()

ModuleInput::const_iterator smtrat::Module::firstSubformulaToPass ( ) const

inlineinherited

Returns: The position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends.

Definition at line 581 of file Module.h.

Here is the caller graph for this function:

◆ firstUncheckedReceivedSubformula()

ModuleInput::const_iterator smtrat::Module::firstUncheckedReceivedSubformula ( ) const

inlineinherited

Returns: The position of the first (by this module) unchecked sub-formula of the received formula.

Definition at line 573 of file Module.h.

◆ foundAnswer()

Answer smtrat::Module::foundAnswer ( Answer _answer )

privateinherited

Sets the solver state to the given answer value.

This method also fires the flag given by the antecessor module of this module to true, if the given answer value is not Unknown.

Parameters

_answer The found answer.

Definition at line 856 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ freeSplittingVariable()

static void smtrat::Module::freeSplittingVariable ( const FormulaT & _splittingVariable )

inlinestaticinherited

Definition at line 509 of file Module.h.

◆ generateTrivialInfeasibleSubset()

void smtrat::Module::generateTrivialInfeasibleSubset ( )

inlineprotectedinherited

Stores the trivial infeasible subset being the set of received formulas.

Definition at line 909 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getBackendsAllModels()

void smtrat::Module::getBackendsAllModels ( ) const

protectedinherited

Stores all models of a backend in the list of all models of this module.

Definition at line 669 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getBackendsModel()

void smtrat::Module::getBackendsModel ( ) const

protectedinherited

Definition at line 652 of file Module.cpp.

Here is the caller graph for this function:

◆ getInfeasibleSubsets() [1/2]

void smtrat::Module::getInfeasibleSubsets ( )

protectedinherited

Copies the infeasible subsets of the passed formula.

Definition at line 596 of file Module.cpp.

Here is the caller graph for this function:

◆ getInfeasibleSubsets() [2/2]

std::vector< FormulaSetT > smtrat::Module::getInfeasibleSubsets ( const Module & _backend ) const

protectedinherited

Get the infeasible subsets the given backend provides.

Note, that an infeasible subset in a backend contains sub formulas of the passed formula and an infeasible subset of this module contains sub formulas of the received formula. In this method the LATTER is returned.

Parameters

_backend The backend from which to obtain the infeasible subsets.

Returns: The infeasible subsets the given backend provides.

Definition at line 709 of file Module.cpp.

Here is the call graph for this function:

◆ getInformationRelevantFormulas()

const std::set< FormulaT > & smtrat::Module::getInformationRelevantFormulas ( )

protectedinherited

Gets all InformationRelevantFormulas.

Returns: Set of all formulas

Definition at line 1074 of file Module.cpp.

Here is the call graph for this function:

◆ getModelEqualities()

std::list< std::vector< carl::Variable > > smtrat::Module::getModelEqualities ( ) const

virtualinherited

Partition the variables from the current model into equivalence classes according to their assigned value.

The result is a set of equivalence classes of variables where all variables within one class are assigned the same value. Note that the number of classes may not be minimal, i.e. two classes may actually be equivalent.

Returns: Equivalence classes.

Definition at line 308 of file Module.cpp.

Here is the caller graph for this function:

◆ getOrigins() [1/3]

void smtrat::Module::getOrigins	(	const FormulaT &	_formula,
		FormulaSetT &	_origins
	)		const

inlineprotectedinherited

Parameters

_formula
_origins

Definition at line 968 of file Module.h.

Here is the call graph for this function:

◆ getOrigins() [2/3]

void smtrat::Module::getOrigins	(	const FormulaT &	_formula,
		FormulasT &	_origins
	)		const

inlineprotectedinherited

Parameters

_formula
_origins

Definition at line 955 of file Module.h.

Here is the call graph for this function:

◆ getOrigins() [3/3]

const FormulaT& smtrat::Module::getOrigins ( ModuleInput::const_iterator _formula ) const

inlineprotectedinherited

Gets the origins of the passed formula at the given position.

Parameters

_formula The position of a formula in the passed formulas.

Returns: The origins of the passed formula at the given position.

Definition at line 808 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getReceivedFormulaSimplified()

std::pair< bool, FormulaT > smtrat::Module::getReceivedFormulaSimplified ( )

virtualinherited

Returns: A pair of a Boolean and a formula, where the Boolean is true, if the received formula could be simplified to an equisatisfiable formula. The formula is equisatisfiable to this module's reveived formula, if the Boolean is true.

Reimplemented in smtrat::PModule.

Definition at line 945 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ hasLemmas()

bool smtrat::Module::hasLemmas ( )

inlineinherited

Checks whether this module or any of its backends provides any lemmas.

Definition at line 532 of file Module.h.

◆ hasValidInfeasibleSubset()

bool smtrat::Module::hasValidInfeasibleSubset ( ) const

inherited

Returns: true, if the module has at least one valid infeasible subset, that is all its elements are sub-formulas of the received formula (pointer must be equal).

Definition at line 1000 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ id()

std::size_t smtrat::Module::id ( ) const

inlineinherited

Returns: A unique ID to identify this module instance.

Definition at line 396 of file Module.h.

◆ infeasibleSubsets()

const std::vector<FormulaSetT>& smtrat::Module::infeasibleSubsets ( ) const

inlineinherited

Returns: The infeasible subsets of the set of received formulas (empty, if this module has not detected unsatisfiability of the conjunction of received formulas.

Definition at line 480 of file Module.h.

Here is the caller graph for this function:

◆ inform()

bool smtrat::Module::inform ( const FormulaT & _constraint )

inherited

Informs the module about the given constraint.

It should be tried to inform this module about any constraint it could receive eventually before assertSubformula is called (preferably for the first time, but at least before adding a formula containing that constraint).

Parameters

_constraint The constraint to inform about.

Returns: false, if it can be easily decided whether the given constraint is inconsistent; true, otherwise.

Definition at line 117 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ informBackends()

void smtrat::Module::informBackends ( const FormulaT & _constraint )

inlineprotectedinherited

Informs all backends of this module about the given constraint.

Parameters

_constraint The constraint to inform about.

Definition at line 836 of file Module.h.

◆ informCore()

virtual bool smtrat::Module::informCore ( [[maybe_unused] ] const FormulaT & _constraint )

inlineprotectedvirtualinherited

Informs the module about the given constraint.

It should be tried to inform this module about any constraint it could receive eventually before assertSubformula is called (preferably for the first time, but at least before adding a formula containing that constraint).

Parameters

_constraint The constraint to inform about.

Returns: false, if it can be easily decided whether the given constraint is inconsistent; true, otherwise.

Definition at line 684 of file Module.h.

Here is the caller graph for this function:

◆ informedConstraints()

const carl::FastSet<FormulaT>& smtrat::Module::informedConstraints ( ) const

inlineinherited

Returns: The position of the first constraint of which no backend has been informed about.

Definition at line 504 of file Module.h.

Here is the caller graph for this function:

◆ init()

void smtrat::Module::init ( )

virtualinherited

Informs all backends about the so far encountered constraints, which have not yet been communicated.

This method must not be called twice and only before the first runBackends call.

Reimplemented in smtrat::PBPPModule< Settings >, smtrat::PBGaussModule< Settings >, smtrat::NRAILModule< Settings >, smtrat::NewCoveringModule< Settings >, smtrat::NewCADModule< Settings >, smtrat::LRAModule< Settings >, smtrat::LRAModule< smtrat::LRASettings1 >, smtrat::LRAModule< smtrat::LRASettingsICP >, smtrat::IntBlastModule< Settings >, smtrat::FPPModule< Settings >, smtrat::CurryModule< Settings >, and smtrat::BVModule< Settings >.

Definition at line 234 of file Module.cpp.

Here is the call graph for this function:

◆ is_minimizing()

bool smtrat::Module::is_minimizing ( ) const

inlineinherited

Definition at line 623 of file Module.h.

◆ isLemmaLevel()

bool smtrat::Module::isLemmaLevel ( LemmaLevel level )

protectedinherited

Checks if current lemma level is greater or equal to given level.

Parameters

level Level to check.

Definition at line 1079 of file Module.cpp.

Here is the call graph for this function:

◆ isPreprocessor()

bool smtrat::Module::isPreprocessor ( ) const

inlineinherited

Returns: true, if this module is a preprocessor that is a module, which simplifies its received formula to an equisatisfiable formula being passed to its backends. The simplified formula can be obtained with getReceivedFormulaSimplified().

Definition at line 607 of file Module.h.

◆ lemmas()

const std::vector<Lemma>& smtrat::Module::lemmas ( ) const

inlineinherited

Returns: A constant reference to the lemmas being valid formulas this module or its backends made.

Definition at line 565 of file Module.h.

Here is the caller graph for this function:

◆ merge()

std::vector< FormulaT > smtrat::Module::merge	(	const std::vector< FormulaT > &	_vecSetA,
		const std::vector< FormulaT > &	_vecSetB
	)		const

protectedinherited

Merges the two vectors of sets into the first one.

({a,b},{a,c}) and ({b,d},{b}) -> ({a,b,d},{a,b},{a,b,c,d},{a,b,c})

Parameters

_vecSetA	A vector of sets of constraints.
_vecSetB	A vector of sets of constraints.

Returns: The vector being the two given vectors merged.

Definition at line 377 of file Module.cpp.

◆ model()

const Model& smtrat::Module::model ( ) const

inlineinherited

Returns: The assignment of the current satisfiable result, if existent.

Definition at line 463 of file Module.h.

Here is the caller graph for this function:

◆ modelsDisjoint()

bool smtrat::Module::modelsDisjoint	(	const Model &	_modelA,
		const Model &	_modelB
	)

staticprotectedinherited

Checks whether there is no variable assigned by both models.

Parameters

_modelA	The first model to check for.
_modelB	The second model to check for.

Returns: true, if there is no variable assigned by both models; false, otherwise.

Definition at line 611 of file Module.cpp.

◆ moduleName()

template<typename Settings >

std::string smtrat::CSplitModule< Settings >::moduleName ( ) const

inlinevirtual

Returns: The name of the given module type as name.

Reimplemented from smtrat::Module.

Definition at line 150 of file CSplitModule.h.

◆ objective()

carl::Variable smtrat::Module::objective ( ) const

inlineinherited

Definition at line 619 of file Module.h.

◆ originInReceivedFormula()

bool smtrat::Module::originInReceivedFormula ( const FormulaT & _origin ) const

protectedinherited

Definition at line 352 of file Module.cpp.

Here is the call graph for this function:

◆ passedFormulaBegin()

ModuleInput::iterator smtrat::Module::passedFormulaBegin ( )

inlineprotectedinherited

Returns: An iterator to the end of the passed formula. TODO: disable this method

Definition at line 780 of file Module.h.

Here is the call graph for this function:

◆ passedFormulaEnd()

ModuleInput::iterator smtrat::Module::passedFormulaEnd ( )

inlineprotectedinherited

Returns: An iterator to the end of the passed formula.

Definition at line 788 of file Module.h.

Here is the call graph for this function:

◆ pPassedFormula()

const ModuleInput* smtrat::Module::pPassedFormula ( ) const

inlineinherited

Returns: A pointer to the formula passed to the backends of this module.

Definition at line 447 of file Module.h.

Here is the caller graph for this function:

◆ pReceivedFormula()

const ModuleInput* smtrat::Module::pReceivedFormula ( ) const

inlineinherited

Returns: A pointer to the formula passed to this module.

Definition at line 431 of file Module.h.

◆ print()

void smtrat::Module::print ( const std::string & _initiation = "***" ) const

inherited

Prints everything relevant of the solver.

Parameters

_initiation The line initiation.

Definition at line 1085 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printAllModels()

void smtrat::Module::printAllModels ( std::ostream & _out = std::cout )

inherited

Prints all assignments of this module satisfying its received formula if it satisfiable and this module could find an assignment.

Parameters

_out	The stream to print the assignment on.

Definition at line 1161 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printInfeasibleSubsets()

void smtrat::Module::printInfeasibleSubsets ( const std::string & _initiation = "***" ) const

inherited

Prints the infeasible subsets.

Parameters

_initiation The line initiation.

Definition at line 1136 of file Module.cpp.

Here is the caller graph for this function:

◆ printModel()

void smtrat::Module::printModel ( std::ostream & _out = std::cout ) const

inherited

Prints the assignment of this module satisfying its received formula if it satisfiable and this module could find an assignment.

Parameters

_out	The stream to print the assignment on.

Definition at line 1151 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printPassedFormula()

void smtrat::Module::printPassedFormula ( const std::string & _initiation = "***" ) const

inherited

Prints the vector of passed formula.

Parameters

_initiation The line initiation.

Definition at line 1118 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printReceivedFormula()

void smtrat::Module::printReceivedFormula ( const std::string & _initiation = "***" ) const

inherited

Prints the vector of the received formula.

Parameters

_initiation The line initiation.

Definition at line 1105 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ probablyLooping()

bool smtrat::Module::probablyLooping	(	const typename Poly::PolyType &	_branchingPolynomial,
		const Rational &	_branchingValue
	)		const

protectedinherited

Checks whether given the current branching value and branching variable/polynomial it is (highly) probable that this branching is part of an infinite loop of branchings.

Parameters

_branchingPolynomial	The polynomial to branch at (in most branching strategies this is just a variable).
_branchingValue	The value to branch at.

Returns: true, if this branching is probably part of an infinite loop of branchings; false, otherwise.

Definition at line 426 of file Module.cpp.

◆ propagateFormula()

template<typename Settings >

void smtrat::CSplitModule< Settings >::propagateFormula	(	const FormulaT &	formula,
		bool	assert
	)

inlineprivate

Asserts/Removes the given formula to/from the LRA solver.

Parameters

formula	The formula to assert/remove to the LRA solver.
assert	True, if formula shall be asserted; False, if formula shall be removed.

◆ receivedFormulaChecked()

void smtrat::Module::receivedFormulaChecked ( )

inlineinherited

Notifies that the received formulas has been checked.

Definition at line 589 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ receivedFormulasAsInfeasibleSubset()

void smtrat::Module::receivedFormulasAsInfeasibleSubset ( ModuleInput::const_iterator _subformula )

inlineprotectedinherited

Stores an infeasible subset consisting only of the given received formula.

Definition at line 920 of file Module.h.

◆ receivedVariable()

bool smtrat::Module::receivedVariable ( carl::Variable::Arg _var ) const

inlineinherited

Definition at line 377 of file Module.h.

◆ remove()

void smtrat::Module::remove ( ModuleInput::const_iterator _subformula )

virtualinherited

Removes everything related to the given sub-formula of the received formula.

However, it is desired not to lose track of search spaces where no satisfying assignment can be found for the remaining sub-formulas.

Parameters

_subformula The sub formula of the received formula to remove.

Reimplemented in smtrat::PModule.

Definition at line 159 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeCore() [1/2]

virtual void smtrat::Module::removeCore ( [[maybe_unused] ] ModuleInput::const_iterator formula )

inlineprotectedvirtualinherited

Removes everything related to the given sub-formula of the received formula.

However, it is desired not to lose track of search spaces where no satisfying assignment can be found for the remaining sub-formulas.

Parameters

formula The sub formula of the received formula to remove.

Definition at line 729 of file Module.h.

Here is the caller graph for this function:

◆ removeCore() [2/2]

template<typename Settings >

void smtrat::CSplitModule< Settings >::removeCore ( ModuleInput::const_iterator _subformula )

Removes the subformula of the received formula at the given position to the considered ones of this module.

Note that this includes every stored calculation which depended on this subformula, but should keep the other stored calculation, if possible, untouched.

Parameters

_subformula The position of the subformula to remove.

◆ removeOrigin()

std::pair<ModuleInput::iterator,bool> smtrat::Module::removeOrigin	(	ModuleInput::iterator	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Definition at line 814 of file Module.h.

Here is the call graph for this function:

◆ removeOrigins()

std::pair<ModuleInput::iterator,bool> smtrat::Module::removeOrigins	(	ModuleInput::iterator	_formula,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins
	)

inlineprotectedinherited

Definition at line 823 of file Module.h.

Here is the call graph for this function:

◆ resetExpansions()

template<typename Settings >

bool smtrat::CSplitModule< Settings >::resetExpansions ( )

private

Resets all expansions to the center points of the variable domains and constructs a new tree of reductions for the currently active monomials.

Returns: True, if there exists a maximal domain with no integral points; False, otherwise.

◆ rPassedFormula()

const ModuleInput& smtrat::Module::rPassedFormula ( ) const

inlineinherited

Returns: A reference to the formula passed to the backends of this module.

Definition at line 455 of file Module.h.

Here is the caller graph for this function:

◆ rReceivedFormula()

const ModuleInput& smtrat::Module::rReceivedFormula ( ) const

inlineinherited

Returns: A reference to the formula passed to this module.

Definition at line 439 of file Module.h.

Here is the caller graph for this function:

◆ runBackends() [1/2]

virtual Answer smtrat::Module::runBackends ( )

inlineprotectedvirtualinherited

Reimplemented in smtrat::PModule.

Definition at line 1012 of file Module.h.

Here is the caller graph for this function:

◆ runBackends() [2/2]

Answer smtrat::Module::runBackends	(	bool	_final,
		bool	_full,
		carl::Variable	_objective
	)

protectedvirtualinherited

Runs the backend solvers on the passed formula.

Parameters

_final	true, if this satisfiability check will be the last one (for a global sat-check), if its result is SAT
_full	false, if this module should avoid too expensive procedures and rather return unknown instead.
_objective	if not set to NO_VARIABLE, the module should find an assignment minimizing this objective variable; otherwise any assignment is good.

Returns: True, if the passed formula is consistent; False, if the passed formula is inconsistent; Unknown, otherwise.

Reimplemented in smtrat::PModule.

Definition at line 727 of file Module.cpp.

Here is the call graph for this function:

◆ setId()

void smtrat::Module::setId ( std::size_t _id )

inlineinherited

Sets this modules unique ID to identify itself.

Parameters

_id	The id to set this module's id to.

Definition at line 405 of file Module.h.

Here is the caller graph for this function:

◆ setThreadPriority()

void smtrat::Module::setThreadPriority ( thread_priority _threadPriority )

inlineinherited

Sets the priority of this module to get a thread for running its check procedure.

Parameters

_threadPriority The priority to set this module's thread priority to.

Definition at line 423 of file Module.h.

Here is the caller graph for this function:

◆ solverState()

Answer smtrat::Module::solverState ( ) const

inlineinherited

Returns: True, if this module is in a state, such that it has found a solution for its received formula; False, if this module is in a state, such that it has determined that there is no solution for its received formula; Unknown, otherwise.

Definition at line 388 of file Module.h.

Here is the caller graph for this function:

◆ splitUnequalConstraint()

void smtrat::Module::splitUnequalConstraint ( const FormulaT & _unequalConstraint )

protectedinherited

Adds the following lemmas for the given constraint p!=0.

 (p!=0 <-> (p<0 or p>0))

and not(p<0 and p>0)

Parameters

_unequalConstraint A constraint having the relation symbol !=.

Definition at line 565 of file Module.cpp.

◆ threadPriority()

thread_priority smtrat::Module::threadPriority ( ) const

inlineinherited

Returns: The priority of this module to get a thread for running its check procedure.

Definition at line 414 of file Module.h.

Here is the caller graph for this function:

◆ updateAllModels()

void smtrat::Module::updateAllModels ( )

virtualinherited

Updates all satisfying models, if the solver has detected the consistency of the received formula, beforehand.

Reimplemented in smtrat::SATModule< Settings >.

Definition at line 261 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ updateLemmas()

void smtrat::Module::updateLemmas ( )

inherited

Stores all lemmas of any backend of this module in its own lemma vector.

Definition at line 919 of file Module.cpp.

Here is the caller graph for this function:

◆ updateModel()

template<typename Settings >

void smtrat::CSplitModule< Settings >::updateModel ( ) const

virtual

Updates the current assignment into the model.

Note, that this is a unique but possibly symbolic assignment maybe containing newly introduced variables.

Reimplemented from smtrat::Module.

◆ usedBackends()

const std::vector<Module*>& smtrat::Module::usedBackends ( ) const

inlineinherited

Returns: The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula).

Definition at line 488 of file Module.h.

Here is the caller graph for this function:

Field Documentation

◆ mAllBackends

std::vector<Module*> smtrat::Module::mAllBackends

protectedinherited

The backends of this module which have been used.

Definition at line 227 of file Module.h.

◆ mAllModels

std::vector<Model> smtrat::Module::mAllModels

mutableprotectedinherited

Stores all satisfying assignments.

Definition at line 201 of file Module.h.

◆ Manager

friend smtrat::Module::Manager

privateinherited

Definition at line 71 of file Module.h.

◆ mBackendsFoundAnswer

std::atomic_bool* smtrat::Module::mBackendsFoundAnswer

protectedinherited

This flag is passed to any backend and if it determines an answer to a prior check call, this flag is fired.

Definition at line 220 of file Module.h.

◆ mCheckedWithBackends

template<typename Settings >

bool smtrat::CSplitModule< Settings >::mCheckedWithBackends

private

Stores whether the last consistency check was done by the backends.

Definition at line 127 of file CSplitModule.h.

◆ mConstraintsToInform

carl::FastSet<FormulaT> smtrat::Module::mConstraintsToInform

protectedinherited

Stores the constraints which the backends must be informed about.

Definition at line 233 of file Module.h.

◆ mExpansions

template<typename Settings >

Bimap<Expansion, const carl::Variable, &Expansion::mRationalization, const carl::Variable, &Expansion::mDiscretization> smtrat::CSplitModule< Settings >::mExpansions

private

Definition at line 94 of file CSplitModule.h.

◆ mFinalCheck

bool smtrat::Module::mFinalCheck

protectedinherited

true, if the check procedure should perform a final check which especially means not to postpone splitting decisions

Definition at line 205 of file Module.h.

◆ mFirstPosInLastBranches

std::size_t smtrat::Module::mFirstPosInLastBranches = 0

staticinherited

The beginning of the cyclic buffer storing the last branches.

Definition at line 275 of file Module.h.

◆ mFirstSubformulaToPass

ModuleInput::iterator smtrat::Module::mFirstSubformulaToPass

protectedinherited

Stores the position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends.

Definition at line 231 of file Module.h.

◆ mFirstUncheckedReceivedSubformula

ModuleInput::const_iterator smtrat::Module::mFirstUncheckedReceivedSubformula

protectedinherited

Stores the position of the first (by this module) unchecked sub-formula of the received formula.

Definition at line 237 of file Module.h.

◆ mFoundAnswer

Conditionals smtrat::Module::mFoundAnswer

protectedinherited

Vector of Booleans: If any of them is true, we have to terminate a running check procedure.

Definition at line 223 of file Module.h.

◆ mFullCheck

bool smtrat::Module::mFullCheck

protectedinherited

false, if this module should avoid too expensive procedures and rather return unknown instead.

Definition at line 207 of file Module.h.

◆ mId

std::size_t smtrat::Module::mId

privateinherited

A unique ID to identify this module instance. (Could be useful but currently nowhere used)

Definition at line 184 of file Module.h.

◆ mInfeasibleSubsets

std::vector<FormulaSetT> smtrat::Module::mInfeasibleSubsets

protectedinherited

Stores the infeasible subsets.

Definition at line 195 of file Module.h.

◆ mInformedConstraints

carl::FastSet<FormulaT> smtrat::Module::mInformedConstraints

protectedinherited

Stores the position of the first constraint of which no backend has been informed about.

Definition at line 235 of file Module.h.

◆ mLastBranches

std::vector< Branching > smtrat::Module::mLastBranches = std::vector<Branching>(mNumOfBranchVarsToStore, Branching(typename Poly::PolyType(), 0))

staticinherited

Stores the last branches in a cycle buffer.

Definition at line 273 of file Module.h.

◆ mLemmas

std::vector<Lemma> smtrat::Module::mLemmas

protectedinherited

Stores the lemmas being valid formulas this module or its backends made.

Definition at line 229 of file Module.h.

◆ mLinearizations

template<typename Settings >

Bimap<Linearization, const Poly, &Linearization::mNormalization, const Poly, &Linearization::mLinearization> smtrat::CSplitModule< Settings >::mLinearizations

private

Definition at line 120 of file CSplitModule.h.

◆ mLRAModel

template<typename Settings >

Model smtrat::CSplitModule< Settings >::mLRAModel

private

Stores the last model for the linearization that was found by the LRA solver.

Definition at line 125 of file CSplitModule.h.

◆ mLRAModule

template<typename Settings >

LAModule smtrat::CSplitModule< Settings >::mLRAModule

private

Handle to the linear arithmetic module.

Definition at line 145 of file CSplitModule.h.

◆ mModel

Model smtrat::Module::mModel

mutableprotectedinherited

Stores the assignment of the current satisfiable result, if existent.

Definition at line 199 of file Module.h.

◆ mModelComputed

bool smtrat::Module::mModelComputed

mutableprotectedinherited

True, if the model has already been computed.

Definition at line 203 of file Module.h.

◆ mModuleName

std::string smtrat::Module::mModuleName

privateinherited

Definition at line 191 of file Module.h.

◆ mNumOfBranchVarsToStore

std::size_t smtrat::Module::mNumOfBranchVarsToStore = 5

staticinherited

The number of different variables to consider for a probable infinite loop of branchings.

Definition at line 271 of file Module.h.

◆ mObjectiveVariable

carl::Variable smtrat::Module::mObjectiveVariable

protectedinherited

Objective variable to be minimized. If set to NO_VARIABLE, a normal sat check should be performed.

Definition at line 209 of file Module.h.

◆ mOldSplittingVariables

std::vector< FormulaT > smtrat::Module::mOldSplittingVariables

staticinherited

Reusable splitting variables.

Definition at line 277 of file Module.h.

◆ mpManager

Manager* const smtrat::Module::mpManager

protectedinherited

A reference to the manager.

Definition at line 197 of file Module.h.

◆ mpPassedFormula

ModuleInput* smtrat::Module::mpPassedFormula

privateinherited

The formula passed to the backends of this module.

Definition at line 190 of file Module.h.

◆ mpReceivedFormula

const ModuleInput* smtrat::Module::mpReceivedFormula

privateinherited

The formula passed to this module.

Definition at line 188 of file Module.h.

◆ mPurifications

template<typename Settings >

std::map<carl::Monomial::Arg, Purification> smtrat::CSplitModule< Settings >::mPurifications

private

Maps a monomial to its purification information.

Definition at line 52 of file CSplitModule.h.

◆ mSmallerMusesCheckCounter

unsigned smtrat::Module::mSmallerMusesCheckCounter

mutableprotectedinherited

Counter used for the generation of the smt2 files to check for smaller muses.

Definition at line 239 of file Module.h.

◆ mSolverState

std::atomic<Answer> smtrat::Module::mSolverState

protectedinherited

States whether the received formula is known to be satisfiable or unsatisfiable otherwise it is set to unknown.

Definition at line 215 of file Module.h.

◆ mStatistics

ModuleStatistics& smtrat::Module::mStatistics = statistics_get<ModuleStatistics>(moduleName())

privateinherited

Definition at line 192 of file Module.h.

◆ mTheoryPropagations

std::vector<TheoryPropagation> smtrat::Module::mTheoryPropagations

protectedinherited

Definition at line 211 of file Module.h.

◆ mThreadPriority

thread_priority smtrat::Module::mThreadPriority

privateinherited

The priority of this module to get a thread for running its check procedure.

Definition at line 186 of file Module.h.

◆ mUsedBackends

std::vector<Module*> smtrat::Module::mUsedBackends

protectedinherited

The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula).

Definition at line 225 of file Module.h.

◆ mVariableBounds

template<typename Settings >

vb::VariableBounds<FormulaT> smtrat::CSplitModule< Settings >::mVariableBounds

private

Helper class that extracts the variable domains.

Definition at line 123 of file CSplitModule.h.

◆ mVariableCounters

std::vector<std::size_t> smtrat::Module::mVariableCounters

protectedinherited

Maps variables to the number of their occurrences.

Definition at line 241 of file Module.h.

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

smtrat-modules/CSplitModule/CSplitModule.h

Data Structures

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Private Types

Private Member Functions

Private Attributes

Detailed Description

template<typename Settings> class smtrat::CSplitModule< Settings >

Member Typedef Documentation

◆ SettingsType

Member Enumeration Documentation

◆ DomainSize

◆ LemmaType

Constructor & Destructor Documentation

◆ CSplitModule()

Member Function Documentation

◆ add()

◆ addConstraintToInform()

◆ addCore() [1/2]

◆ addCore() [2/2]

◆ addInformationRelevantFormula()

◆ addLemma()

◆ addOrigin()

◆ addReceivedSubformulaToPassedFormula()

◆ addSubformulaToPassedFormula() [1/4]

◆ addSubformulaToPassedFormula() [2/4]

◆ addSubformulaToPassedFormula() [3/4]

◆ addSubformulaToPassedFormula() [4/4]

◆ allModels()

◆ analyzeConflict()

◆ anAnswerFound()

◆ answerFound()

◆ backendsModel()

◆ bloatDomains()

◆ branchAt() [1/4]

◆ branchAt() [2/4]

◆ branchAt() [3/4]

◆ branchAt() [4/4]

◆ changeActiveDomain()

◆ check()

◆ checkCore()

◆ checkInfSubsetForMinimality()

◆ checkModel()

◆ cleanModel()

◆ clearLemmas()

◆ clearModel()

◆ clearModels()

◆ clearPassedFormula()

◆ collectOrigins() [1/2]

◆ collectOrigins() [2/2]

◆ collectTheoryPropagations()

◆ constraintsToInform()

◆ currentlySatisfied()

◆ currentlySatisfiedByBackend()

◆ deinform()

◆ deinformCore()

◆ determine_smallest_origin()

◆ eraseSubformulaFromPassedFormula()

◆ excludeNotReceivedVariablesFromModel()

◆ findBestOrigin()

◆ firstSubformulaToPass()

◆ firstUncheckedReceivedSubformula()

◆ foundAnswer()

◆ freeSplittingVariable()

◆ generateTrivialInfeasibleSubset()

◆ getBackendsAllModels()

◆ getBackendsModel()

◆ getInfeasibleSubsets() [1/2]

◆ getInfeasibleSubsets() [2/2]

◆ getInformationRelevantFormulas()

◆ getModelEqualities()

◆ getOrigins() [1/3]

◆ getOrigins() [2/3]

◆ getOrigins() [3/3]

◆ getReceivedFormulaSimplified()

template<typename Settings>
class smtrat::CSplitModule< Settings >