#include <ICPModule.h>

Inheritance diagram for smtrat::ICPModule< Settings >:

[legend]

Collaboration diagram for smtrat::ICPModule< Settings >:

[legend]

Data Structures
struct	comp
	Typedefs: More...

struct	formulaPtrComp

struct	linearVariable

struct	weights

Public Types
typedef carl::FastPointerMap< Poly *, weights >	WeightMap

typedef Settings	SettingsType

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

Public Member Functions
std::string	moduleName () const

	ICPModule (const ModuleInput , Conditionals &, Manager const =NULL)
	Constructors: More...

	~ICPModule ()
	Destructor: More...

bool	informCore (const FormulaT &)

bool	addCore (ModuleInput::const_iterator)

void	removeCore (ModuleInput::const_iterator)

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

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

EvalRationalIntervalMap	getCurrentBoxAsIntervals () const

FormulasT	getCurrentBoxAsFormulas () 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...

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

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

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

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

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

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

unsigned	currentlySatisfiedByBackend (const FormulaT &_formula) const

virtual unsigned	currentlySatisfied (const FormulaT &) const

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

Answer	solverState () const

std::size_t	id () const

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

thread_priority	threadPriority () const

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

const ModuleInput *	pReceivedFormula () const

const ModuleInput &	rReceivedFormula () const

const ModuleInput *	pPassedFormula () const

const ModuleInput &	rPassedFormula () const

const Model &	model () const

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

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

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

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

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

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

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

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

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

ModuleInput::const_iterator	firstUncheckedReceivedSubformula () const

ModuleInput::const_iterator	firstSubformulaToPass () const

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

const smtrat::Conditionals &	answerFound () const

bool	isPreprocessor () const

carl::Variable	objective () const

bool	is_minimizing () const

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

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

void	collectTheoryPropagations ()

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

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

bool	hasValidInfeasibleSubset () const

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

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

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

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

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

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

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

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

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

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

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

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

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

Protected Member Functions
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...

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

void	clearPassedFormula ()

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

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

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

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

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

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

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

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

unsigned	checkModel () const

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

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

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

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

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

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

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

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

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

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

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

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

std::vector< TheoryPropagation >	mTheoryPropagations

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

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

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

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

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

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

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

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

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

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

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

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

Private Types
template<template< typename > class Operator>
using	Contractor = carl::Contraction< Operator, Poly >

Private Member Functions
void	resetHistory (icp::ContractionCandidate *)
	Methods: More...

void	addConstraint (const FormulaT &_formula)

icp::IcpVariable *	getIcpVariable (carl::Variable::Arg _var, bool _original, const icp::LRAVariable *_lraVar)

void	activateNonlinearConstraint (const FormulaT &_formula)

void	activateLinearConstraint (const FormulaT &_formula, const FormulaT &_origin)

bool	initialLinearCheck (Answer &_answer)
	Performs a consistency check on the linearization of the received constraints. More...

bool	checkNotEqualConstraints ()

void	contractCurrentBox ()

Answer	callBackends (bool _final=false, bool _full=true, carl::Variable _objective=carl::Variable::NO_VARIABLE)

Poly	createNonlinearCCs (const ConstraintT &_constraint, const std::vector< Poly > &_tempMonomes)
	Creates the non-linear contraction candidates from all items in mTemporaryMonomes and empties mTemporaryMonomes. More...

void	createLinearCCs (const FormulaT &_constraint, const FormulaT &_original)
	Creates the linear contraction candidates corresponding to the given linear constraint. More...

void	fillCandidates ()
	Fills the IcpRelevantCandidates with all nonlinear and all active linear ContractionCandidates. More...

bool	addCandidateToRelevant (icp::ContractionCandidate *_candidate)
	Adds the specific candidate to IcpRelevantCandidates. More...

bool	removeCandidateFromRelevant (icp::ContractionCandidate *_candidate)
	Removes a candidate from the icpRelevantCandidates. More...

void	updateRelevantCandidates (carl::Variable::Arg _var)
	Update all affected candidates and reinsert them into icpRelevantCandidates. More...

icp::ContractionCandidate *	chooseContractionCandidate ()
	Method to determine the next combination of variable and constraint to be contracted. More...

void	contraction (icp::ContractionCandidate *_selection)
	Calls the actual contraction function and implements threshold functionality. More...

void	setContraction (icp::ContractionCandidate *_selection, icp::IcpVariable &_icpVar, const DoubleInterval &_contractedInterval)

void	setContraction (const FormulaT &_constraint, icp::IcpVariable &_icpVar, const DoubleInterval &_contractedInterval, bool _allCCs)

void	updateRelativeContraction (const DoubleInterval &_interval, const DoubleInterval &_contractedInterval)

void	updateAbsoluteContraction (const DoubleInterval &_interval, const DoubleInterval &_contractedInterval)

std::map< carl::Variable, double >	createModel (bool antipoint=false) const

double	sizeBasedSplittingImpact (std::map< carl::Variable, icp::IcpVariable * >::const_iterator _varIcpVarMapIter) const
	Selects the next splitting direction according to different heuristics. More...

FormulaSetT	createPremiseDeductions ()

std::vector< FormulaT >	createPremise ()

FormulasT	createBoxFormula (bool _onlyOriginalVariables)

bool	performSplit (bool _contractionApplied, bool &_moreContractionFound)

bool	splitToBoundedIntervalsWithoutZero (carl::Variable &_variable, Rational &_value, bool &_leftCaseWeak, bool &_preferLeftCase, std::vector< std::map< carl::Variable, icp::IcpVariable * >::const_iterator > &_suitableVariables)

void	sizeBasedSplitting (carl::Variable &_variable, Rational &_value, bool &_leftCaseWeak, bool &_preferLeftCase)

bool	satBasedSplitting (carl::Variable &_variable, Rational &_value, bool &_leftCaseWeak, bool &_preferLeftCase)

double	satBasedSplittingImpact (icp::IcpVariable &_icpVariable, const EvalDoubleIntervalMap &_intervals, const DoubleInterval &_seperatedPart, bool _calculateImpact)

void	splittingBasedContraction (icp::IcpVariable &_icpVar, const FormulaT &_violatedConstraint, const DoubleInterval &_contractedInterval)

bool	tryTestPoints ()

bool	checkBoxAgainstLinearFeasibleRegion ()
	Checks the actual intervalBox with the LRASolver. More...

void	pushBoundsToPassedFormula ()
	Creates Bounds and passes them to PassedFormula for the Backends. More...

RationalInterval	doubleToRationalInterval (carl::Variable::Arg _var, const DoubleInterval &_interval, EvalRationalIntervalMap::const_iterator _initialIntervalIter) const

FormulaT	intervalBoundToFormula (carl::Variable::Arg _var, const DoubleInterval &_interval, EvalRationalIntervalMap::const_iterator _initialIntervalIter, bool _upper) const

FormulasT	variableReasonHull (icp::set_icpVariable &_reasons)
	Compute hull of defining origins for set of icpVariables. More...

FormulasT	createConstraintsFromBounds (const EvalDoubleIntervalMap &_map, bool _isOriginal=true)
	creates constraints for the actual bounds of the original variables. More...

FormulaT	getReceivedFormulas (const FormulaT &_deduction)
	Parses obtained deductions from the LRA module and maps them to original constraints or introduces new ones. More...

void	remapAndSetLraInfeasibleSubsets ()
	Sets the own infeasible subset according to the infeasible subset of the internal lra module. More...

double	calculateCurrentBoxSize ()

void	addProgress (double _progress)

void	setBox (icp::HistoryNode *_selection)
	Set all parameters of the module according to the selected HistoryNode. More...

bool	intervalsEmpty (const EvalDoubleIntervalMap &_intervals) const

bool	intervalsEmpty (bool _original=false) const

bool	contractionCandidatesHaveLegalOrigins () const

bool	contractionCandidatesHaveLegalOrigins (const ContractionCandidates &_ccs) const

bool	contractionCandidateHasLegalOrigins (const icp::ContractionCandidate &_cc) const

bool	fulfillsTarget (icp::ContractionCandidate &_cc) const

bool	fulfillsTarget (const DoubleInterval &_interval) const

void	debugPrint () const
	Printout of actual tables of linear constraints, active linear constraints, nonlinear constraints and active nonlinear constraints. More...

void	printAffectedCandidates () const
	Prints the mapping from variable to ContractionCandidates which contain this variable. More...

void	printIcpVariables () const
	Prints all icpVariables. More...

void	printIcpRelevantCandidates () const
	Prints all icpRelevant candidates with their weight and id. More...

void	printIntervals (bool _original=false) const
	Prints all intervals from mIntervals, should be the same intervals as in mHistoryActual->intervals(). More...

void	printPreprocessedInput (std::string _init="") const
	Prints all intervals from mIntervals, should be the same intervals as in mHistoryActual->intervals(). More...

void	printContraction (const icp::ContractionCandidate &_cc, const DoubleInterval &_before, const DoubleInterval &_afterA, const DoubleInterval &_afterB=DoubleInterval::empty_interval(), std::ostream &_out=std::cout) 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
carl::FastMap< Poly, Contractor< carl::SimpleNewton > >	mContractors
	Members: More...

icp::ContractionCandidateManager	mCandidateManager

std::set< icp::ContractionCandidate *, icp::contractionCandidateComp >	mActiveNonlinearConstraints

std::set< icp::ContractionCandidate *, icp::contractionCandidateComp >	mActiveLinearConstraints

std::map< const icp::LRAVariable *, ContractionCandidates >	mLinearConstraints

std::map< ConstraintT, ContractionCandidates >	mNonlinearConstraints

FormulaSetT	mNotEqualConstraints

std::map< carl::Variable, icp::IcpVariable * >	mVariables

EvalDoubleIntervalMap	mIntervals

EvalRationalIntervalMap	mInitialIntervals

Model	mFoundSolution

std::set< std::pair< double, unsigned >, comp >	mIcpRelevantCandidates

carl::FastMap< FormulaT, FormulaT >	mLinearizations

carl::FastMap< FormulaT, FormulaT >	mDeLinearizations

carl::FastMap< Poly, carl::Variable >	mVariableLinearizations

std::map< carl::Variable, Poly >	mSubstitutions

icp::HistoryNode *	mHistoryRoot

icp::HistoryNode *	mHistoryActual

ModuleInput *	mValidationFormula

smtrat::Conditionals	mLRAFoundAnswer

LRAModule< LRASettingsICP >	mLRA

std::queue< FormulasT >	mBoxStorage

bool	mIsIcpInitialized

bool	mSplitOccurred

bool	mInvalidBox

bool	mOriginalVariableIntervalContracted

bool	mLRAFoundSolution

double	mTargetDiameter

double	mContractionThreshold

double	mDefaultSplittingSize

SplittingHeuristic	mSplittingHeuristic

unsigned	mNumberOfReusagesAfterTargetDiameterReached

double	mRelativeContraction

double	mAbsoluteContraction

int	mCountBackendCalls

double	mGlobalBoxSize

double	mInitialBoxSize

double	mCovererdRegionSize

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

Static Private Attributes
static const unsigned	mSplittingStrategy = 0

Detailed Description

template<class Settings>
class smtrat::ICPModule< Settings >

Definition at line 32 of file ICPModule.h.

Member Typedef Documentation

◆ Contractor

template<class Settings >

template<template< typename > class Operator>

using smtrat::ICPModule< Settings >::Contractor = carl::Contraction<Operator, Poly>

private

Definition at line 36 of file ICPModule.h.

◆ SettingsType

template<class Settings >

typedef Settings smtrat::ICPModule< Settings >::SettingsType

Definition at line 134 of file ICPModule.h.

◆ WeightMap

template<class Settings >

typedef carl::FastPointerMap<Poly*, weights> smtrat::ICPModule< Settings >::WeightMap

Definition at line 74 of file ICPModule.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

◆ ICPModule()

template<class Settings >

smtrat::ICPModule< Settings >::ICPModule	(	const ModuleInput *	,
		Conditionals &	,
		Manager * const	= `NULL`
	)

Constructors:

◆ ~ICPModule()

template<class Settings >

smtrat::ICPModule< Settings >::~ICPModule ( )

Destructor:

Member Function Documentation

◆ activateLinearConstraint()

template<class Settings >

void smtrat::ICPModule< Settings >::activateLinearConstraint	(	const FormulaT &	_formula,
		const FormulaT &	_origin
	)

private

Parameters

_formula

◆ activateNonlinearConstraint()

template<class Settings >

void smtrat::ICPModule< Settings >::activateNonlinearConstraint ( const FormulaT & _formula )

private

Parameters

_formula

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

◆ addCandidateToRelevant()

template<class Settings >

bool smtrat::ICPModule< Settings >::addCandidateToRelevant ( icp::ContractionCandidate * _candidate )

private

Adds the specific candidate to IcpRelevantCandidates.

Parameters

_candidate

◆ addConstraint()

template<class Settings >

void smtrat::ICPModule< Settings >::addConstraint ( const FormulaT & _formula )

private

Parameters

_splitOccurred

Returns

◆ 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::ICPModule< Settings >::addCore ( ModuleInput::const_iterator )

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

◆ addProgress()

template<class Settings >

void smtrat::ICPModule< Settings >::addProgress ( double _progress )

private

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

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

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

◆ calculateCurrentBoxSize()

template<class Settings >

double smtrat::ICPModule< Settings >::calculateCurrentBoxSize ( )

private

◆ callBackends()

template<class Settings >

Answer smtrat::ICPModule< Settings >::callBackends	(	bool	_final = `false`,
		bool	_full = `true`,
		carl::Variable	_objective = `carl::Variable::NO_VARIABLE`
	)

private

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

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

◆ checkBoxAgainstLinearFeasibleRegion()

template<class Settings >

bool smtrat::ICPModule< Settings >::checkBoxAgainstLinearFeasibleRegion ( )

private

Checks the actual intervalBox with the LRASolver.

Returns

◆ checkCore()

template<class Settings >

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

virtual

Checks the received formula for consistency.

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: SAT, if the received formula is satisfiable; UNSAT, if the received formula is not satisfiable; Unknown, otherwise.

Reimplemented from smtrat::Module.

◆ checkInfSubsetForMinimality()

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

inherited

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

Parameters

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

Definition at line 1018 of file Module.cpp.

Here is the call graph for this function:

◆ checkModel()

unsigned smtrat::Module::checkModel ( ) const

protectedinherited

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

Definition at line 588 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkNotEqualConstraints()

template<class Settings >

bool smtrat::ICPModule< Settings >::checkNotEqualConstraints ( )

private

Returns

◆ chooseContractionCandidate()

template<class Settings >

icp::ContractionCandidate* smtrat::ICPModule< Settings >::chooseContractionCandidate ( )

private

Method to determine the next combination of variable and constraint to be contracted.

Parameters

_it

Returns: a pair of variable and constraint

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

◆ contractCurrentBox()

template<class Settings >

void smtrat::ICPModule< Settings >::contractCurrentBox ( )

private

Parameters

_splitOccurred

◆ contraction()

template<class Settings >

void smtrat::ICPModule< Settings >::contraction ( icp::ContractionCandidate * _selection )

private

Calls the actual contraction function and implements threshold functionality.

Parameters

_selection

◆ contractionCandidateHasLegalOrigins()

template<class Settings >

bool smtrat::ICPModule< Settings >::contractionCandidateHasLegalOrigins ( const icp::ContractionCandidate & _cc ) const

inlineprivate

Definition at line 464 of file ICPModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ contractionCandidatesHaveLegalOrigins() [1/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::contractionCandidatesHaveLegalOrigins ( ) const

inlineprivate

Definition at line 439 of file ICPModule.h.

◆ contractionCandidatesHaveLegalOrigins() [2/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::contractionCandidatesHaveLegalOrigins ( const ContractionCandidates & _ccs ) const

inlineprivate

Definition at line 454 of file ICPModule.h.

Here is the call graph for this function:

◆ createBoxFormula()

template<class Settings >

FormulasT smtrat::ICPModule< Settings >::createBoxFormula ( bool _onlyOriginalVariables )

private

Parameters

_onlyOriginalVariables

Returns

◆ createConstraintsFromBounds()

template<class Settings >

FormulasT smtrat::ICPModule< Settings >::createConstraintsFromBounds	(	const EvalDoubleIntervalMap &	_map,
		bool	_isOriginal = `true`
	)

private

creates constraints for the actual bounds of the original variables.

Returns

◆ createLinearCCs()

template<class Settings >

void smtrat::ICPModule< Settings >::createLinearCCs	(	const FormulaT &	_constraint,
		const FormulaT &	_original
	)

private

Creates the linear contraction candidates corresponding to the given linear constraint.

Parameters

_constraint
_origin

◆ createModel()

template<class Settings >

std::map<carl::Variable, double> smtrat::ICPModule< Settings >::createModel ( bool antipoint = false ) const

private

Parameters

antipoint

Returns

◆ createNonlinearCCs()

template<class Settings >

Poly smtrat::ICPModule< Settings >::createNonlinearCCs	(	const ConstraintT &	_constraint,
		const std::vector< Poly > &	_tempMonomes
	)

private

Creates the non-linear contraction candidates from all items in mTemporaryMonomes and empties mTemporaryMonomes.

◆ createPremise()

template<class Settings >

std::vector<FormulaT> smtrat::ICPModule< Settings >::createPremise ( )

private

◆ createPremiseDeductions()

template<class Settings >

FormulaSetT smtrat::ICPModule< Settings >::createPremiseDeductions ( )

private

Returns

◆ currentlySatisfied()

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

inlinevirtualinherited

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

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

Definition at line 372 of file Module.h.

◆ currentlySatisfiedByBackend()

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

inherited

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

Definition at line 296 of file Module.cpp.

◆ debugPrint()

template<class Settings >

void smtrat::ICPModule< Settings >::debugPrint ( ) const

private

Printout of actual tables of linear constraints, active linear constraints, nonlinear constraints and active nonlinear constraints.

◆ deinform()

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

inherited

The inverse of informing about a constraint.

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

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 124 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deinformCore()

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

inlineprotectedvirtualinherited

The inverse of informing about a constraint.

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

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 695 of file Module.h.

Here is the caller graph for this function:

◆ determine_smallest_origin()

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

protectedinherited

Parameters

origins A vector of sets of origins.

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

Definition at line 403 of file Module.cpp.

◆ doubleToRationalInterval()

template<class Settings >

RationalInterval smtrat::ICPModule< Settings >::doubleToRationalInterval	(	carl::Variable::Arg	_var,
		const DoubleInterval &	_interval,
		EvalRationalIntervalMap::const_iterator	_initialIntervalIter
	)		const

private

◆ eraseSubformulaFromPassedFormula()

template<class Settings >

ModuleInput::iterator smtrat::ICPModule< Settings >::eraseSubformulaFromPassedFormula	(	ModuleInput::iterator	_subformula,
		bool	_ignoreOrigins = `false`
	)

protectedvirtual

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	SAT, if the sub-formula shall be removed regardless of its origins (should only be applied with expertise).

Returns

Reimplemented from smtrat::Module.

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

◆ fillCandidates()

template<class Settings >

void smtrat::ICPModule< Settings >::fillCandidates ( )

private

Fills the IcpRelevantCandidates with all nonlinear and all active linear ContractionCandidates.

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

◆ fulfillsTarget() [1/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::fulfillsTarget ( const DoubleInterval & _interval ) const

inlineprivate

Definition at line 491 of file ICPModule.h.

◆ fulfillsTarget() [2/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::fulfillsTarget ( icp::ContractionCandidate & _cc ) const

inlineprivate

Definition at line 477 of file ICPModule.h.

Here is the call graph for this function:

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

◆ getCurrentBoxAsFormulas()

template<class Settings >

FormulasT smtrat::ICPModule< Settings >::getCurrentBoxAsFormulas ( ) const

◆ getCurrentBoxAsIntervals()

template<class Settings >

EvalRationalIntervalMap smtrat::ICPModule< Settings >::getCurrentBoxAsIntervals ( ) const

◆ getIcpVariable()

template<class Settings >

icp::IcpVariable* smtrat::ICPModule< Settings >::getIcpVariable	(	carl::Variable::Arg	_var,
		bool	_original,
		const icp::LRAVariable *	_lraVar
	)

private

Parameters

_var
_original
_lraVar

Returns

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

◆ getReceivedFormulas()

template<class Settings >

FormulaT smtrat::ICPModule< Settings >::getReceivedFormulas ( const FormulaT & _deduction )

private

Parses obtained deductions from the LRA module and maps them to original constraints or introduces new ones.

◆ getReceivedFormulaSimplified()

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

virtualinherited

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

Reimplemented in smtrat::PModule.

Definition at line 945 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ hasLemmas()

bool smtrat::Module::hasLemmas ( )

inlineinherited

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

Definition at line 532 of file Module.h.

◆ hasValidInfeasibleSubset()

bool smtrat::Module::hasValidInfeasibleSubset ( ) const

inherited

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

Definition at line 1000 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ id()

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

inlineinherited

Returns: A unique ID to identify this module instance.

Definition at line 396 of file Module.h.

◆ infeasibleSubsets()

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

inlineinherited

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

Definition at line 480 of file Module.h.

Here is the caller graph for this function:

◆ inform()

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

inherited

Informs the module about the given constraint.

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

Parameters

_constraint The constraint to inform about.

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

Definition at line 117 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ informBackends()

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

inlineprotectedinherited

Informs all backends of this module about the given constraint.

Parameters

_constraint The constraint to inform about.

Definition at line 836 of file Module.h.

◆ informCore() [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::ICPModule< Settings >::informCore ( const FormulaT & )

◆ informedConstraints()

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

inlineinherited

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

Definition at line 504 of file Module.h.

Here is the caller graph for this function:

◆ init()

void smtrat::Module::init ( )

virtualinherited

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

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

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

Definition at line 234 of file Module.cpp.

Here is the call graph for this function:

◆ initialLinearCheck()

template<class Settings >

bool smtrat::ICPModule< Settings >::initialLinearCheck ( Answer & _answer )

private

Performs a consistency check on the linearization of the received constraints.

Parameters

_answer The answer of the consistency check on the linearization of the received constraints.

Returns: true, if the linear check led to a conclusive answer which should be returned by this module; false, otherwise.

◆ intervalBoundToFormula()

template<class Settings >

FormulaT smtrat::ICPModule< Settings >::intervalBoundToFormula	(	carl::Variable::Arg	_var,
		const DoubleInterval &	_interval,
		EvalRationalIntervalMap::const_iterator	_initialIntervalIter,
		bool	_upper
	)		const

private

◆ intervalsEmpty() [1/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::intervalsEmpty ( bool _original = false ) const

private

◆ intervalsEmpty() [2/2]

template<class Settings >

bool smtrat::ICPModule< Settings >::intervalsEmpty ( const EvalDoubleIntervalMap & _intervals ) const

private

◆ is_minimizing()

bool smtrat::Module::is_minimizing ( ) const

inlineinherited

Definition at line 623 of file Module.h.

◆ isLemmaLevel()

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

protectedinherited

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

Parameters

level Level to check.

Definition at line 1079 of file Module.cpp.

Here is the call graph for this function:

◆ isPreprocessor()

bool smtrat::Module::isPreprocessor ( ) const

inlineinherited

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

Definition at line 607 of file Module.h.

◆ lemmas()

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

inlineinherited

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

Definition at line 565 of file Module.h.

Here is the caller graph for this function:

◆ merge()

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

protectedinherited

Merges the two vectors of sets into the first one.

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

Parameters

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

Returns: The vector being the two given vectors merged.

Definition at line 377 of file Module.cpp.

◆ model()

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

inlineinherited

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

Definition at line 463 of file Module.h.

Here is the caller graph for this function:

◆ modelsDisjoint()

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

staticprotectedinherited

Checks whether there is no variable assigned by both models.

Parameters

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

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

Definition at line 611 of file Module.cpp.

◆ moduleName()

template<class Settings >

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

inlinevirtual

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

Reimplemented from smtrat::Module.

Definition at line 135 of file ICPModule.h.

◆ objective()

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

inlineinherited

Definition at line 619 of file Module.h.

◆ originInReceivedFormula()

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

protectedinherited

Definition at line 352 of file Module.cpp.

Here is the call graph for this function:

◆ passedFormulaBegin()

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

inlineprotectedinherited

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

Definition at line 780 of file Module.h.

Here is the call graph for this function:

◆ passedFormulaEnd()

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

inlineprotectedinherited

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

Definition at line 788 of file Module.h.

Here is the call graph for this function:

◆ performSplit()

template<class Settings >

bool smtrat::ICPModule< Settings >::performSplit	(	bool	_contractionApplied,
		bool &	_moreContractionFound
	)

private

Parameters

_contractionApplied
_moreConstactionFound

Returns: If a split has happened.

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

◆ printAffectedCandidates()

template<class Settings >

void smtrat::ICPModule< Settings >::printAffectedCandidates ( ) const

private

Prints the mapping from variable to ContractionCandidates which contain this variable.

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

◆ printContraction()

template<class Settings >

void smtrat::ICPModule< Settings >::printContraction	(	const icp::ContractionCandidate &	_cc,
		const DoubleInterval &	_before,
		const DoubleInterval &	_afterA,
		const DoubleInterval &	_afterB = `DoubleInterval::empty_interval()`,
		std::ostream &	_out = `std::cout`
	)		const

private

◆ printIcpRelevantCandidates()

template<class Settings >

void smtrat::ICPModule< Settings >::printIcpRelevantCandidates ( ) const

private

Prints all icpRelevant candidates with their weight and id.

◆ printIcpVariables()

template<class Settings >

void smtrat::ICPModule< Settings >::printIcpVariables ( ) const

private

Prints all icpVariables.

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

◆ printIntervals()

template<class Settings >

void smtrat::ICPModule< Settings >::printIntervals ( bool _original = false ) const

private

Prints all intervals from mIntervals, should be the same intervals as in mHistoryActual->intervals().

◆ printModel()

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

inherited

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

Parameters

_out	The stream to print the assignment on.

Definition at line 1151 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printPassedFormula()

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

inherited

Prints the vector of passed formula.

Parameters

_initiation The line initiation.

Definition at line 1118 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printPreprocessedInput()

template<class Settings >

void smtrat::ICPModule< Settings >::printPreprocessedInput ( std::string _init = "" ) const

private

Prints all intervals from mIntervals, should be the same intervals as in mHistoryActual->intervals().

◆ printReceivedFormula()

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

inherited

Prints the vector of the received formula.

Parameters

_initiation The line initiation.

Definition at line 1105 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ probablyLooping()

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

protectedinherited

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

Parameters

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

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

Definition at line 426 of file Module.cpp.

◆ pushBoundsToPassedFormula()

template<class Settings >

void smtrat::ICPModule< Settings >::pushBoundsToPassedFormula ( )

private

Creates Bounds and passes them to PassedFormula for the Backends.

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

◆ remapAndSetLraInfeasibleSubsets()

template<class Settings >

void smtrat::ICPModule< Settings >::remapAndSetLraInfeasibleSubsets ( )

private

Sets the own infeasible subset according to the infeasible subset of the internal lra module.

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

◆ removeCandidateFromRelevant()

template<class Settings >

bool smtrat::ICPModule< Settings >::removeCandidateFromRelevant ( icp::ContractionCandidate * _candidate )

private

Removes a candidate from the icpRelevantCandidates.

Parameters

_candidate

◆ 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::ICPModule< Settings >::removeCore ( ModuleInput::const_iterator )

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

◆ resetHistory()

template<class Settings >

void smtrat::ICPModule< Settings >::resetHistory ( icp::ContractionCandidate * )

private

Methods:

Reset to state before application of this cc.

Reset the current state to a state before this contraction was applied. As we only have two states, we check, if this cc has been used yet and if so, we reset the state, else the state remains unchanged.

Parameters

_cc	[description]

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

◆ satBasedSplitting()

template<class Settings >

bool smtrat::ICPModule< Settings >::satBasedSplitting	(	carl::Variable &	_variable,
		Rational &	_value,
		bool &	_leftCaseWeak,
		bool &	_preferLeftCase
	)

private

Parameters

_variable
_value
_leftCaseWeak
_preferLeftCase

Returns

◆ satBasedSplittingImpact()

template<class Settings >

double smtrat::ICPModule< Settings >::satBasedSplittingImpact	(	icp::IcpVariable &	_icpVariable,
		const EvalDoubleIntervalMap &	_intervals,
		const DoubleInterval &	_seperatedPart,
		bool	_calculateImpact
	)

private

◆ setBox()

template<class Settings >

void smtrat::ICPModule< Settings >::setBox ( icp::HistoryNode * _selection )

private

Set all parameters of the module according to the selected HistoryNode.

Parameters

_selection the Node which contains the new context

◆ setContraction() [1/2]

template<class Settings >

void smtrat::ICPModule< Settings >::setContraction	(	const FormulaT &	_constraint,
		icp::IcpVariable &	_icpVar,
		const DoubleInterval &	_contractedInterval,
		bool	_allCCs
	)

private

◆ setContraction() [2/2]

template<class Settings >

void smtrat::ICPModule< Settings >::setContraction	(	icp::ContractionCandidate *	_selection,
		icp::IcpVariable &	_icpVar,
		const DoubleInterval &	_contractedInterval
	)

private

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

◆ sizeBasedSplitting()

template<class Settings >

void smtrat::ICPModule< Settings >::sizeBasedSplitting	(	carl::Variable &	_variable,
		Rational &	_value,
		bool &	_leftCaseWeak,
		bool &	_preferLeftCase
	)

private

Parameters

_variable
_value
_leftCaseWeak
_preferLeftCase

◆ sizeBasedSplittingImpact()

template<class Settings >

double smtrat::ICPModule< Settings >::sizeBasedSplittingImpact ( std::map< carl::Variable, icp::IcpVariable * >::const_iterator _varIcpVarMapIter ) const

private

Selects the next splitting direction according to different heuristics.

Parameters

_targetDiameter

Returns

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

◆ splittingBasedContraction()

template<class Settings >

void smtrat::ICPModule< Settings >::splittingBasedContraction	(	icp::IcpVariable &	_icpVar,
		const FormulaT &	_violatedConstraint,
		const DoubleInterval &	_contractedInterval
	)

private

◆ splitToBoundedIntervalsWithoutZero()

template<class Settings >

bool smtrat::ICPModule< Settings >::splitToBoundedIntervalsWithoutZero	(	carl::Variable &	_variable,
		Rational &	_value,
		bool &	_leftCaseWeak,
		bool &	_preferLeftCase,
		std::vector< std::map< carl::Variable, icp::IcpVariable * >::const_iterator > &	_suitableVariables
	)

private

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

◆ tryTestPoints()

template<class Settings >

bool smtrat::ICPModule< Settings >::tryTestPoints ( )

private

Parameters

_solution

Returns

◆ updateAbsoluteContraction()

template<class Settings >

void smtrat::ICPModule< Settings >::updateAbsoluteContraction	(	const DoubleInterval &	_interval,
		const DoubleInterval &	_contractedInterval
	)

private

Parameters

_interval
_contractedInterval

◆ 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::ICPModule< Settings >::updateModel ( ) const

virtual

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

Reimplemented from smtrat::Module.

◆ updateRelativeContraction()

template<class Settings >

void smtrat::ICPModule< Settings >::updateRelativeContraction	(	const DoubleInterval &	_interval,
		const DoubleInterval &	_contractedInterval
	)

private

Parameters

_interval
_contractedInterval

◆ updateRelevantCandidates()

template<class Settings >

void smtrat::ICPModule< Settings >::updateRelevantCandidates ( carl::Variable::Arg _var )

private

Update all affected candidates and reinsert them into icpRelevantCandidates.

Parameters

_var

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

◆ variableReasonHull()

template<class Settings >

FormulasT smtrat::ICPModule< Settings >::variableReasonHull ( icp::set_icpVariable & _reasons )

private

Compute hull of defining origins for set of icpVariables.

Parameters

_reasons

Returns

bool smtrat::Module::mModelComputed

mutableprotectedinherited

True, if the model has already been computed.

Definition at line 203 of file Module.h.

template<class Settings >

const unsigned smtrat::ICPModule< Settings >::mSplittingStrategy = 0

staticprivate

Definition at line 131 of file ICPModule.h.

◆ mStatistics

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

privateinherited

Definition at line 192 of file Module.h.

◆ mSubstitutions

template<class Settings >

std::map<carl::Variable, Poly> smtrat::ICPModule< Settings >::mSubstitutions

private

Definition at line 98 of file ICPModule.h.

◆ mTargetDiameter

template<class Settings >

double smtrat::ICPModule< Settings >::mTargetDiameter

private

Definition at line 113 of file ICPModule.h.

template<class Settings >

std::map<carl::Variable, icp::IcpVariable*> smtrat::ICPModule< Settings >::mVariables

private

Definition at line 89 of file ICPModule.h.

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

smtrat-modules/ICPModule/ICPModule.h

Data Structures

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Private Types

Private Member Functions

Private Attributes

Static Private Attributes

Detailed Description

template<class Settings> class smtrat::ICPModule< Settings >

Member Typedef Documentation

◆ Contractor

◆ SettingsType

◆ WeightMap

Member Enumeration Documentation

◆ LemmaType

Constructor & Destructor Documentation

◆ ICPModule()

◆ ~ICPModule()

Member Function Documentation

◆ activateLinearConstraint()

◆ activateNonlinearConstraint()

◆ add()

◆ addCandidateToRelevant()

◆ addConstraint()

◆ addConstraintToInform()

◆ addCore() [1/2]

◆ addCore() [2/2]

◆ addInformationRelevantFormula()

◆ addLemma()

◆ addOrigin()

◆ addProgress()

◆ addReceivedSubformulaToPassedFormula()

◆ addSubformulaToPassedFormula() [1/4]

◆ addSubformulaToPassedFormula() [2/4]

◆ addSubformulaToPassedFormula() [3/4]

◆ addSubformulaToPassedFormula() [4/4]

◆ allModels()

◆ anAnswerFound()

◆ answerFound()

◆ backendsModel()

◆ branchAt() [1/4]

◆ branchAt() [2/4]

◆ branchAt() [3/4]

◆ branchAt() [4/4]

◆ calculateCurrentBoxSize()

◆ callBackends()

◆ check()

◆ checkBoxAgainstLinearFeasibleRegion()

◆ checkCore()

◆ checkInfSubsetForMinimality()

◆ checkModel()

◆ checkNotEqualConstraints()

◆ chooseContractionCandidate()

◆ cleanModel()

◆ clearLemmas()

◆ clearModel()

◆ clearModels()

◆ clearPassedFormula()

◆ collectOrigins() [1/2]

◆ collectOrigins() [2/2]

◆ collectTheoryPropagations()

◆ constraintsToInform()

◆ contractCurrentBox()

◆ contraction()

◆ contractionCandidateHasLegalOrigins()

◆ contractionCandidatesHaveLegalOrigins() [1/2]

◆ contractionCandidatesHaveLegalOrigins() [2/2]

◆ createBoxFormula()

◆ createConstraintsFromBounds()

◆ createLinearCCs()

◆ createModel()

◆ createNonlinearCCs()

◆ createPremise()

◆ createPremiseDeductions()

◆ currentlySatisfied()

template<class Settings>
class smtrat::ICPModule< Settings >