A module which performs the Simplex method on the linear part of it's received formula. More...

#include <LRAModule.h>

Inheritance diagram for smtrat::LRAModule< Settings >:

[legend]

Collaboration diagram for smtrat::LRAModule< Settings >:

[legend]

Data Structures
struct	Context
	Stores a formula, being part of the received formula of this module, and the position of this formula in the passed formula. More...

Public Types
typedef Settings::BoundType	LRABoundType
	Number type of the underlying value of a bound of a variable within the LRAModule. More...

typedef Settings::EntryType	LRAEntryType
	Type of an entry within the tableau. More...

typedef lra::Bound< LRABoundType, LRAEntryType >	LRABound
	Type of a bound of a variable within the LRAModule. More...

typedef lra::Variable< LRABoundType, LRAEntryType >	LRAVariable
	A variable of the LRAModule, being either a original variable or a slack variable representing a linear polynomial. More...

typedef lra::Value< LRABoundType >	LRAValue
	The type of the assignment of a variable maintained by the LRAModule. It consists of a tuple of two value of the bound type. More...

typedef Settings	SettingsType

typedef carl::FastMap< carl::Variable, LRAVariable * >	VarVariableMap
	Maps an original variable to it's corresponding LRAModule variable. More...

typedef carl::FastPointerMap< typename Poly::PolyType, LRAVariable * >	ExVariableMap
	Maps a linear polynomial to it's corresponding LRAModule variable. More...

typedef carl::FastMap< FormulaT, std::vector< const LRABound * > * >	ConstraintBoundsMap
	Maps constraint to the bounds it represents (e.g., equations represent two bounds) More...

typedef carl::FastMap< FormulaT, Context >	ConstraintContextMap
	Stores the position of a received formula in the passed formula. More...

typedef lra::Tableau< typename Settings::Tableau_settings, LRABoundType, LRAEntryType >	LRATableau
	The tableau which is the main data structure maintained by the LRAModule responsible for the pivoting steps. More...

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

Public Member Functions
std::string	moduleName () const

	LRAModule (const ModuleInput _formula, Conditionals &_conditionals, Manager _manager=NULL)
	Constructs a LRAModule. More...

virtual	~LRAModule ()
	Destructs this LRAModule. More...

bool	informCore (const FormulaT &_constraint)
	Informs this module about the existence of the given constraint, which means that it could be added in future. More...

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

void	init ()
	Initializes the tableau according to all linear constraints, of which this module has been informed. More...

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 everything related to the given sub-formula of the received formula. More...

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

Answer	checkCore_old ()

Answer	processResult (Answer _result)

void	updateModel () const
	Updates the model, if the solver has detected the consistency of the received formula, beforehand. More...

unsigned	currentlySatisfied (const FormulaT &) const

const RationalAssignment &	getRationalModel () const
	Gives a rational model if the received formula is satisfiable. More...

Answer	optimize (Answer _result)

Answer	checkNotEqualConstraints (Answer _result)

void	processLearnedBounds ()

void	createInfeasibleSubsets (lra::EntryID _tableauEntry)

EvalRationalIntervalMap	getVariableBounds () const
	Returns the bounds of the variables as intervals. More...

void	printLinearConstraints (std::ostream &_out=std::cout, const std::string _init="") const
	Prints all linear constraints. More...

void	printNonlinearConstraints (std::ostream &_out=std::cout, const std::string _init="") const
	Prints all non-linear constraints. More...

void	printConstraintToBound (std::ostream &_out=std::cout, const std::string _init="") const
	Prints the mapping of constraints to their corresponding bounds. More...

void	printBoundCandidatesToPass (std::ostream &_out=std::cout, const std::string _init="") const
	Prints the strictest bounds, which have to be passed the backend in case. More...

void	printRationalModel (std::ostream &_out=std::cout, const std::string _init="") const
	Prints the current rational assignment. More...

void	printTableau (std::ostream &_out=std::cout, const std::string _init="") const
	Prints the current tableau. More...

void	printVariables (std::ostream &_out=std::cout, const std::string _init="") const
	Prints all lra variables and their assignments. More...

const VarVariableMap &	originalVariables () const

const ExVariableMap &	slackVariables () const

const LRAVariable *	getSlackVariable (const FormulaT &_constraint) const

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...

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

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 Member Functions
void	learnRefinements ()
	Adds the refinements learned during pivoting to the deductions. More...

void	learnRefinement (const typename LRATableau::LearnedBound &_learnedBound, bool _upperBound)

FormulasT	createPremise (const std::vector< const LRABound * > &_premiseBounds, bool &_premiseOnlyEqualities) const

void	adaptPassedFormula ()
	Adapt the passed formula, such that it consists of the finite infimums and supremums of all variables and the non linear constraints. More...

bool	checkAssignmentForNonlinearConstraint ()
	Checks whether the current assignment of the linear constraints fulfills the non linear constraints. More...

void	activateBound (const LRABound *_bound, const FormulaT &_formula)
	Activate the given bound and update the supremum, the infimum and the assignment of variable to which the bound belongs. More...

void	activateStrictBound (const FormulaT &_neqOrigin, const LRABound &_weakBound, const LRABound *_strictBound)
	Activates a strict bound as a result of the two constraints p!=0 and p<=0 resp. More...

void	setBound (const FormulaT &_constraint)
	Creates a bound corresponding to the given constraint. More...

void	simpleTheoryPropagation ()
	Adds simple deduction being lemmas of the form (=> c_1 c_2) with, e.g. More...

void	simpleTheoryPropagation (const LRABound *_bound)

void	propagate (const LRABound *_premise, const FormulaT &_conclusion)

void	propagateLowerBound (const LRABound *_bound)

void	propagateUpperBound (const LRABound *_bound)

void	propagateEqualBound (const LRABound *_bound)

bool	gomoryCut ()

bool	mostInfeasibleVar (bool _tryGomoryCut, carl::Variables &_varsToExclude)

bool	branch_and_bound ()
	Creates a branch and bound lemma. More...

bool	assignmentConsistentWithTableau (const RationalAssignment &_assignment, const LRABoundType &_delta) const
	Checks whether the found assignment is consistent with the tableau, hence replacing the original variables in the expressions represented by the slack variables equals their assignment. More...

bool	assignmentCorrect () const

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
bool	mInitialized
	A flag, which is true if this module has already set all bounds corresponding to the constraint, of which this module has been informed. More...

bool	mAssignmentFullfilsNonlinearConstraints
	A flag which is true, if the non-linear constraints fulfill the current assignment. More...

bool	mStrongestBoundsRemoved
	A flag which is set, if a supremum or infimum of a LRAModule variable has been changed. More...

bool	mOptimumComputed

bool	mRationalModelComputed

bool	mCheckedWithBackends

LRATableau	mTableau
	Contains the main data structures of this module. More...

carl::FastSet< FormulaT >	mLinearConstraints
	Stores all linear constraints of which this module has been once informed. More...

carl::FastSet< FormulaT >	mNonlinearConstraints
	Stores all non-linear constraints which are currently added (by assertSubformula) to this module. More...

ConstraintContextMap	mActiveResolvedNEQConstraints
	Those constraints p!=0, which are added to this module (part of the received formula), which are resolved by a constraints as p<0, p<=0, p>=0 or p>0. More...

ConstraintContextMap	mActiveUnresolvedNEQConstraints
	Those constraints p!=0, which are added to this module (part of the received formula), which are not yet resolved by a constraints as p<0, p<=0, p>=0 or p>0. More...

carl::Variable	mDelta
	The delta value, which influencing the assignment such that it also fulfills all strict inequalities (cf. More...

std::vector< const LRABound * >	mBoundCandidatesToPass
	Stores the bounds, which would influence a backend call because of recent changes. More...

RationalAssignment	mRationalAssignment

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<class Settings>
class smtrat::LRAModule< Settings >

A module which performs the Simplex method on the linear part of it's received formula.

Definition at line 28 of file LRAModule.h.

Member Typedef Documentation

◆ ConstraintBoundsMap

template<class Settings >

typedef carl::FastMap<FormulaT, std::vector<const LRABound*>*> smtrat::LRAModule< Settings >::ConstraintBoundsMap

Maps constraint to the bounds it represents (e.g., equations represent two bounds)

Definition at line 69 of file LRAModule.h.

◆ ConstraintContextMap

template<class Settings >

typedef carl::FastMap<FormulaT, Context> smtrat::LRAModule< Settings >::ConstraintContextMap

Stores the position of a received formula in the passed formula.

Definition at line 71 of file LRAModule.h.

◆ ExVariableMap

template<class Settings >

typedef carl::FastPointerMap<typename Poly::PolyType, LRAVariable*> smtrat::LRAModule< Settings >::ExVariableMap

Maps a linear polynomial to it's corresponding LRAModule variable.

Definition at line 67 of file LRAModule.h.

◆ LRABound

template<class Settings >

typedef lra::Bound<LRABoundType, LRAEntryType> smtrat::LRAModule< Settings >::LRABound

Type of a bound of a variable within the LRAModule.

Definition at line 37 of file LRAModule.h.

◆ LRABoundType

template<class Settings >

typedef Settings::BoundType smtrat::LRAModule< Settings >::LRABoundType

Number type of the underlying value of a bound of a variable within the LRAModule.

Definition at line 33 of file LRAModule.h.

◆ LRAEntryType

template<class Settings >

typedef Settings::EntryType smtrat::LRAModule< Settings >::LRAEntryType

Type of an entry within the tableau.

Definition at line 35 of file LRAModule.h.

◆ LRATableau

template<class Settings >

typedef lra::Tableau<typename Settings::Tableau_settings, LRABoundType, LRAEntryType> smtrat::LRAModule< Settings >::LRATableau

The tableau which is the main data structure maintained by the LRAModule responsible for the pivoting steps.

Definition at line 73 of file LRAModule.h.

◆ LRAValue

template<class Settings >

typedef lra::Value<LRABoundType> smtrat::LRAModule< Settings >::LRAValue

The type of the assignment of a variable maintained by the LRAModule. It consists of a tuple of two value of the bound type.

Definition at line 41 of file LRAModule.h.

◆ LRAVariable

template<class Settings >

typedef lra::Variable<LRABoundType, LRAEntryType> smtrat::LRAModule< Settings >::LRAVariable

A variable of the LRAModule, being either a original variable or a slack variable representing a linear polynomial.

Definition at line 39 of file LRAModule.h.

◆ SettingsType

template<class Settings >

typedef Settings smtrat::LRAModule< Settings >::SettingsType

Definition at line 42 of file LRAModule.h.

◆ VarVariableMap

template<class Settings >

typedef carl::FastMap<carl::Variable, LRAVariable*> smtrat::LRAModule< Settings >::VarVariableMap

Maps an original variable to it's corresponding LRAModule variable.

Definition at line 65 of file LRAModule.h.

Member Enumeration Documentation

◆ LemmaType

enum smtrat::Module::LemmaType : unsigned

stronginherited

Enumerator
NORMAL
PERMANENT

Definition at line 123 of file Module.h.

Constructor & Destructor Documentation

◆ LRAModule()

template<class Settings >

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

Constructs a LRAModule.

Parameters

_type	The type of this module being LRAModule.
_formula	The formula passed to this module, called received formula.
_settings	[Not yet used.]
_conditionals	Vector of Booleans: If any of them is true, we have to terminate a running check procedure.
_manager	A reference to the manager of the solver using this module.

◆ ~LRAModule()

template<class Settings >

virtual smtrat::LRAModule< Settings >::~LRAModule ( )

virtual

Destructs this LRAModule.

Member Function Documentation

◆ activateBound()

template<class Settings >

void smtrat::LRAModule< Settings >::activateBound	(	const LRABound *	_bound,
		const FormulaT &	_formula
	)

private

Activate the given bound and update the supremum, the infimum and the assignment of variable to which the bound belongs.

Parameters

_bound	The bound to activate.
_formula	The constraints which form this bound.

◆ activateStrictBound()

template<class Settings >

void smtrat::LRAModule< Settings >::activateStrictBound	(	const FormulaT &	_neqOrigin,
		const LRABound &	_weakBound,
		const LRABound *	_strictBound
	)

private

Activates a strict bound as a result of the two constraints p!=0 and p<=0 resp.

p>=0.

Parameters

_neqOrigin	The constraint with != as relation symbol.
_weakBound	The bound corresponding to either a constraint with <= resp. >= as relation symbol.
_strictBound	The bound to activate corresponding to either a constraint with < or > as relation symbol.

◆ adaptPassedFormula()

template<class Settings >

void smtrat::LRAModule< Settings >::adaptPassedFormula ( )

private

Adapt the passed formula, such that it consists of the finite infimums and supremums of all variables and the non linear constraints.

◆ 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<class Settings >

bool smtrat::LRAModule< 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:

◆ 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:

◆ assignmentConsistentWithTableau()

template<class Settings >

bool smtrat::LRAModule< Settings >::assignmentConsistentWithTableau	(	const RationalAssignment &	_assignment,
		const LRABoundType &	_delta
	)		const

private

Checks whether the found assignment is consistent with the tableau, hence replacing the original variables in the expressions represented by the slack variables equals their assignment.

Parameters

_assignment	The assignment of the original variables.
_delta	The calculated delta for the given assignment.

Returns: true, if the found assignment is consistent with the tableau; false, otherwise.

◆ assignmentCorrect()

template<class Settings >

bool smtrat::LRAModule< Settings >::assignmentCorrect ( ) const

private

Returns: true, if the encountered satisfying assignment for the received formula indeed satisfies it; false, otherwise.

◆ 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:

◆ branch_and_bound()

template<class Settings >

bool smtrat::LRAModule< Settings >::branch_and_bound ( )

private

Creates a branch and bound lemma.

Returns: true, if the solution is not in the domain, 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:

◆ 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:

◆ checkAssignmentForNonlinearConstraint()

template<class Settings >

bool smtrat::LRAModule< Settings >::checkAssignmentForNonlinearConstraint ( )

private

Checks whether the current assignment of the linear constraints fulfills the non linear constraints.

Returns: true, if the current assignment of the linear constraints fulfills the non linear constraints; false, otherwise.

◆ checkCore()

template<class Settings >

Answer smtrat::LRAModule< 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.

◆ checkCore_old()

template<class Settings >

Answer smtrat::LRAModule< Settings >::checkCore_old ( )

◆ 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:

◆ checkNotEqualConstraints()

template<class Settings >

Answer smtrat::LRAModule< Settings >::checkNotEqualConstraints ( Answer _result )

◆ 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.

◆ createInfeasibleSubsets()

template<class Settings >

void smtrat::LRAModule< Settings >::createInfeasibleSubsets ( lra::EntryID _tableauEntry )

◆ createPremise()

template<class Settings >

FormulasT smtrat::LRAModule< Settings >::createPremise	(	const std::vector< const LRABound * > &	_premiseBounds,
		bool &	_premiseOnlyEqualities
	)		const

private

◆ currentlySatisfied()

template<class Settings >

unsigned smtrat::LRAModule< Settings >::currentlySatisfied ( const FormulaT & ) const

virtual

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

Reimplemented from smtrat::Module.

◆ 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() [1/2]

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:

◆ deinformCore() [2/2]

template<class Settings >

void smtrat::LRAModule< Settings >::deinformCore ( const FormulaT & _constraint )

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.

◆ 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:

◆ getRationalModel()

template<class Settings >

const RationalAssignment& smtrat::LRAModule< Settings >::getRationalModel ( ) const

Gives a rational model if the received formula is satisfiable.

Note, that it is calculated from scratch every time you call this method.

Returns: The rational model.

◆ 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:

◆ getSlackVariable()

template<class Settings >

const LRAVariable* smtrat::LRAModule< Settings >::getSlackVariable ( const FormulaT & _constraint ) const

inline

Parameters

_constraint The constraint to get the slack variable for.

Returns: The slack variable constructed for the linear polynomial without the constant part in the given constraint.

Definition at line 298 of file LRAModule.h.

Here is the call graph for this function:

◆ getVariableBounds()

template<class Settings >

EvalRationalIntervalMap smtrat::LRAModule< Settings >::getVariableBounds ( ) const

Returns the bounds of the variables as intervals.

Returns: The bounds of the variables as intervals.

◆ gomoryCut()

template<class Settings >

bool smtrat::LRAModule< Settings >::gomoryCut ( )

private

Returns: true, if a branching occurred. false, otherwise.

◆ 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() [1/2]

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:

◆ informCore() [2/2]

template<class Settings >

bool smtrat::LRAModule< Settings >::informCore ( const FormulaT & _constraint )

Informs this module about the existence of the given constraint, which means that it could be added in future.

Parameters

_constraint The constraint to inform about.

Returns: false, if the it can be determined that the constraint itself is conflicting; true, otherwise.

◆ 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()

template<class Settings >

void smtrat::LRAModule< Settings >::init ( )

virtual

Initializes the tableau according to all linear constraints, of which this module has been informed.

Reimplemented from smtrat::Module.

◆ 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.

◆ learnRefinement()

template<class Settings >

void smtrat::LRAModule< Settings >::learnRefinement	(	const typename LRATableau::LearnedBound &	_learnedBound,
		bool	_upperBound
	)

private

◆ learnRefinements()

template<class Settings >

void smtrat::LRAModule< Settings >::learnRefinements ( )

private

Adds the refinements learned during pivoting to the deductions.

◆ 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<class Settings >

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

inlinevirtual

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

Reimplemented from smtrat::Module.

Definition at line 43 of file LRAModule.h.

◆ mostInfeasibleVar()

template<class Settings >

bool smtrat::LRAModule< Settings >::mostInfeasibleVar	(	bool	_tryGomoryCut,
		carl::Variables &	_varsToExclude
	)

private

Parameters

_varsToExclude The variable on which we do not want to branch.

Returns: true, if the solution is not in the domain, false, otherwise.

◆ objective()

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

inlineinherited

Definition at line 619 of file Module.h.

◆ optimize()

template<class Settings >

Answer smtrat::LRAModule< Settings >::optimize ( Answer _result )

◆ originalVariables()

template<class Settings >

const VarVariableMap& smtrat::LRAModule< Settings >::originalVariables ( ) const

inline

Returns: A constant reference to the original variables.

Definition at line 281 of file LRAModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ 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:

◆ printBoundCandidatesToPass()

template<class Settings >

void smtrat::LRAModule< Settings >::printBoundCandidatesToPass	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints the strictest bounds, which have to be passed the backend in case.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ printConstraintToBound()

template<class Settings >

void smtrat::LRAModule< Settings >::printConstraintToBound	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints the mapping of constraints to their corresponding bounds.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ 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:

◆ printLinearConstraints()

template<class Settings >

void smtrat::LRAModule< Settings >::printLinearConstraints	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints all linear constraints.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ 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:

◆ printNonlinearConstraints()

template<class Settings >

void smtrat::LRAModule< Settings >::printNonlinearConstraints	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints all non-linear constraints.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ 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:

◆ printRationalModel()

template<class Settings >

void smtrat::LRAModule< Settings >::printRationalModel	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints the current rational assignment.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ 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:

◆ printTableau()

template<class Settings >

void smtrat::LRAModule< Settings >::printTableau	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints the current tableau.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ printVariables()

template<class Settings >

void smtrat::LRAModule< Settings >::printVariables	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Prints all lra variables and their assignments.

Parameters

_out	The output stream to print on.
_init	The beginning of each line to print.

◆ 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.

◆ processLearnedBounds()

template<class Settings >

void smtrat::LRAModule< Settings >::processLearnedBounds ( )

◆ processResult()

template<class Settings >

Answer smtrat::LRAModule< Settings >::processResult ( Answer _result )

◆ propagate()

template<class Settings >

void smtrat::LRAModule< Settings >::propagate	(	const LRABound *	_premise,
		const FormulaT &	_conclusion
	)

private

◆ propagateEqualBound()

template<class Settings >

void smtrat::LRAModule< Settings >::propagateEqualBound ( const LRABound * _bound )

private

◆ propagateLowerBound()

template<class Settings >

void smtrat::LRAModule< Settings >::propagateLowerBound ( const LRABound * _bound )

private

◆ propagateUpperBound()

template<class Settings >

void smtrat::LRAModule< Settings >::propagateUpperBound ( const LRABound * _bound )

private

◆ 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<class Settings >

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

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

Parameters

_subformula The sub formula of the received formula 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:

◆ 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:

◆ setBound()

template<class Settings >

void smtrat::LRAModule< Settings >::setBound ( const FormulaT & _constraint )

private

Creates a bound corresponding to the given constraint.

Parameters

_constraint The constraint corresponding to the bound to create.

◆ 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:

◆ simpleTheoryPropagation() [1/2]

template<class Settings >

void smtrat::LRAModule< Settings >::simpleTheoryPropagation ( )

private

Adds simple deduction being lemmas of the form (=> c_1 c_2) with, e.g.

c_1 being p>=1 and c_2 being p>0.

◆ simpleTheoryPropagation() [2/2]

template<class Settings >

void smtrat::LRAModule< Settings >::simpleTheoryPropagation ( const LRABound * _bound )

private

◆ slackVariables()

template<class Settings >

const ExVariableMap& smtrat::LRAModule< Settings >::slackVariables ( ) const

inline

Returns: A constant reference to the slack variables.

Definition at line 289 of file LRAModule.h.

Here is the call 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<class Settings >

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

virtual

Updates the model, if the solver has detected the consistency of the received formula, beforehand.

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

◆ mActiveResolvedNEQConstraints

template<class Settings >

ConstraintContextMap smtrat::LRAModule< Settings >::mActiveResolvedNEQConstraints

private

Those constraints p!=0, which are added to this module (part of the received formula), which are resolved by a constraints as p<0, p<=0, p>=0 or p>0.

Definition at line 105 of file LRAModule.h.

◆ mActiveUnresolvedNEQConstraints

template<class Settings >

ConstraintContextMap smtrat::LRAModule< Settings >::mActiveUnresolvedNEQConstraints

private

Those constraints p!=0, which are added to this module (part of the received formula), which are not yet resolved by a constraints as p<0, p<=0, p>=0 or p>0.

Definition at line 110 of file LRAModule.h.

◆ 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.

◆ mAssignmentFullfilsNonlinearConstraints

template<class Settings >

bool smtrat::LRAModule< Settings >::mAssignmentFullfilsNonlinearConstraints

private

A flag which is true, if the non-linear constraints fulfill the current assignment.

Definition at line 83 of file LRAModule.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.

◆ mBoundCandidatesToPass

template<class Settings >

std::vector<const LRABound* > smtrat::LRAModule< Settings >::mBoundCandidatesToPass

private

Stores the bounds, which would influence a backend call because of recent changes.

Definition at line 117 of file LRAModule.h.

◆ mCheckedWithBackends

template<class Settings >

bool smtrat::LRAModule< Settings >::mCheckedWithBackends

private

Definition at line 91 of file LRAModule.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.

◆ mDelta

template<class Settings >

carl::Variable smtrat::LRAModule< Settings >::mDelta

private

The delta value, which influencing the assignment such that it also fulfills all strict inequalities (cf.

Integrating Simplex with DPLL(T ) by B. Dutertre and L. de Moura).

Definition at line 115 of file LRAModule.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.

◆ mInitialized

template<class Settings >

bool smtrat::LRAModule< Settings >::mInitialized

private

A flag, which is true if this module has already set all bounds corresponding to the constraint, of which this module has been informed.

Definition at line 81 of file LRAModule.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.

◆ mLinearConstraints

template<class Settings >

carl::FastSet<FormulaT> smtrat::LRAModule< Settings >::mLinearConstraints

private

Stores all linear constraints of which this module has been once informed.

Definition at line 98 of file LRAModule.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.

◆ mNonlinearConstraints

template<class Settings >

carl::FastSet<FormulaT> smtrat::LRAModule< Settings >::mNonlinearConstraints

private

Stores all non-linear constraints which are currently added (by assertSubformula) to this module.

Definition at line 100 of file LRAModule.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.

◆ mOptimumComputed

template<class Settings >

bool smtrat::LRAModule< Settings >::mOptimumComputed

private

Definition at line 87 of file LRAModule.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.

◆ mRationalAssignment

template<class Settings >

RationalAssignment smtrat::LRAModule< Settings >::mRationalAssignment

mutableprivate

Definition at line 119 of file LRAModule.h.

◆ mRationalModelComputed

template<class Settings >

bool smtrat::LRAModule< Settings >::mRationalModelComputed

mutableprivate

Definition at line 89 of file LRAModule.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.

◆ mStrongestBoundsRemoved

template<class Settings >

bool smtrat::LRAModule< Settings >::mStrongestBoundsRemoved

private

A flag which is set, if a supremum or infimum of a LRAModule variable has been changed.

Definition at line 85 of file LRAModule.h.

◆ mTableau

template<class Settings >

LRATableau smtrat::LRAModule< Settings >::mTableau

private

Contains the main data structures of this module.

It maintains for each LRAModule variable a row or a column. On this tableau pivoting can be performed as the well known Simplex method performs.

Definition at line 96 of file LRAModule.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.

◆ 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/LRAModule/LRAModule.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 Member Functions

Private Attributes

Detailed Description

template<class Settings> class smtrat::LRAModule< Settings >

Member Typedef Documentation

◆ ConstraintBoundsMap

◆ ConstraintContextMap

◆ ExVariableMap

◆ LRABound

◆ LRABoundType

◆ LRAEntryType

◆ LRATableau

◆ LRAValue

◆ LRAVariable

◆ SettingsType

◆ VarVariableMap

Member Enumeration Documentation

◆ LemmaType

Constructor & Destructor Documentation

◆ LRAModule()

◆ ~LRAModule()

Member Function Documentation

◆ activateBound()

◆ activateStrictBound()

◆ adaptPassedFormula()

◆ 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()

◆ anAnswerFound()

◆ answerFound()

◆ assignmentConsistentWithTableau()

◆ assignmentCorrect()

◆ backendsModel()

◆ branch_and_bound()

◆ branchAt() [1/4]

◆ branchAt() [2/4]

◆ branchAt() [3/4]

◆ branchAt() [4/4]

◆ check()

◆ checkAssignmentForNonlinearConstraint()

◆ checkCore()

◆ checkCore_old()

◆ checkInfSubsetForMinimality()

◆ checkModel()

◆ checkNotEqualConstraints()

◆ cleanModel()

◆ clearLemmas()

◆ clearModel()

◆ clearModels()

◆ clearPassedFormula()

◆ collectOrigins() [1/2]

◆ collectOrigins() [2/2]

◆ collectTheoryPropagations()

◆ constraintsToInform()

◆ createInfeasibleSubsets()

◆ createPremise()

◆ currentlySatisfied()

◆ currentlySatisfiedByBackend()

◆ deinform()

◆ deinformCore() [1/2]

◆ deinformCore() [2/2]

◆ determine_smallest_origin()

template<class Settings>
class smtrat::LRAModule< Settings >