#include <PPNL.h>

Inheritance diagram for smtrat::MCSAT_PPNL:

Collaboration diagram for smtrat::MCSAT_PPNL:

[legend]

Public Member Functions
	MCSAT_PPNL ()

bool	inform (const FormulaT &_constraint)
	Informs the solver about a constraint. More...

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

bool	add (const FormulaT &_subformula, bool _containsUnknownConstraints=true)
	Adds the given formula to the conjunction of formulas, which will be considered for the next satisfiability check. More...

Answer	check (bool _full=true)
	Checks the so far added formulas for satisfiability. More...

void	push ()
	Pushes a backtrack point to the stack of backtrack points. More...

bool	pop ()
	Pops a backtrack point from the stack of backtrack points. More...

void	pop (size_t _levels)

void	clear ()

void	setObjectiveVariable (carl::Variable var)

const carl::Variable &	objectiveVariable () const

void	reset ()

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

std::list< std::vector< carl::Variable > >	getModelEqualities () const
	Determines variables assigned by the currently found satisfying assignment to an equal value in their domain. More...

const Model &	model () const

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

std::vector< FormulaT >	lemmas ()
	Returns the lemmas/tautologies which were made during the last solving provoked by check(). More...

const ModuleInput &	formula () const

ModuleInput::iterator	formulaBegin ()

ModuleInput::iterator	formulaEnd ()

void	printAssignment () const
	Prints the currently found assignment of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable. More...

void	printAllAssignments (std::ostream &_out=std::cout)
	Prints all assignments of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable. More...

void	printInfeasibleSubset (std::ostream &_out=std::cout) const
	Prints the first found infeasible subset of the set of received formulas. More...

void	printBackTrackStack (std::ostream &_out=std::cout) const
	Prints the stack of backtrack points. More...

void	printStrategyGraph (std::ostream &_out=std::cout) const
	Prints the strategy of the solver maintained by this manager. More...

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

std::ostream &	rDebugOutputChannel ()

auto	logic () const

auto &	rLogic ()

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

void	clearInformationRelevantFormula ()
	Deletes all InformationRelevantFormula. More...

void	setLemmaLevel (LemmaLevel level)
	Sets the current level for lemma generation. More...

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

std::pair< bool, FormulaT >	getInputSimplified ()

ModuleInput::iterator	remove (ModuleInput::iterator _subformula)
	Removes the formula at the given position in the conjunction of formulas, which will be considered for the next satisfiability check. More...

ModuleInput::iterator	remove (const FormulaT &_subformula)
	Temporarily added: (TODO: Discuss with Gereon) Removes the given formula in the conjunction of formulas, which will be considered for the next satisfiability check. More...

Protected Member Functions
void	setStrategy (const std::initializer_list< BackendLink > &backends)

void	setStrategy (const BackendLink &backend)

template<typename Module >
BackendLink	addBackend (const std::initializer_list< BackendLink > &backends={})

template<typename Module >
BackendLink	addBackend (const BackendLink &backend)

BackendLink &	addEdge (std::size_t from, std::size_t to)

std::vector< Module * >	getAllBackends (Module *_module) const
	Gets all backends so far instantiated according the strategy and all previous enquiries of the given module. More...

std::vector< Module * >	getBackends (Module _requiredBy, std::atomic_bool _foundAnswer)
	Get the backends to call for the given problem instance required by the given module. More...

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

Private Attributes
smtrat::Conditionals	mPrimaryBackendFoundAnswer
	a vector of flags, which indicate that an answer has been found of an antecessor module of the primary module More...

ModuleInput *	mpPassedFormula
	the constraints so far passed to the primary backend More...

carl::Condition	mPropositions
	The propositions of the passed formula. More...

std::vector< ModuleInput::iterator >	mBacktrackPoints
	Contains the backtrack points, that are iterators to the last formula to be kept when backtracking to the respective point. More...

std::vector< Module * >	mGeneratedModules
	all generated instances of modules More...

std::map< const Module const, std::vector< Module > >	mBackendsOfModules
	a mapping of each module to its backends More...

Module *	mpPrimaryBackend
	the primary backends More...

bool	mBackendsUptodate
	a Boolean showing whether the manager has received new constraint after the last consistency check More...

StrategyGraph	mStrategyGraph
	primary strategy More...

std::ostream	mDebugOutputChannel
	channel to write debug output More...

carl::Logic	mLogic
	the logic this solver considers More...

std::set< FormulaT >	mInformationRelevantFormula
	List of formula which are relevant for certain tasks. More...

LemmaLevel	mLemmaLevel
	Level of lemma generation. More...

carl::Variable	mObjectiveVariable
	objective variable More...

Detailed Description

Definition at line 10 of file PPNL.h.

Constructor & Destructor Documentation

◆ MCSAT_PPNL()

smtrat::MCSAT_PPNL::MCSAT_PPNL ( )

inline

Definition at line 13 of file PPNL.h.

Here is the call graph for this function:

Member Function Documentation

◆ add()

bool smtrat::Manager::add	(	const FormulaT &	_subformula,
		bool	_containsUnknownConstraints = `true`
	)

inherited

Adds the given formula to the conjunction of formulas, which will be considered for the next satisfiability check.

Parameters

_subformula	The formula to add.
_containsUnknownConstraints	true, if the formula to add contains constraints, about which this solver was not yet informed.

Returns: false, if it is easy to decide whether adding this formula creates a conflict; true, otherwise.

Definition at line 86 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addBackend() [1/2]

template<typename Module >

BackendLink smtrat::Manager::addBackend ( const BackendLink & backend )

inlineprotectedinherited

Definition at line 400 of file Manager.h.

Here is the call graph for this function:

◆ addBackend() [2/2]

template<typename Module >

BackendLink smtrat::Manager::addBackend ( const std::initializer_list< BackendLink > & backends = {} )

inlineprotectedinherited

Definition at line 396 of file Manager.h.

◆ addEdge()

BackendLink& smtrat::Manager::addEdge	(	std::size_t	from,
		std::size_t	to
	)

inlineprotectedinherited

Definition at line 403 of file Manager.h.

Here is the call graph for this function:

◆ addInformationRelevantFormula()

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

inlineinherited

Adds formula to InformationRelevantFormula.

Parameters

formula Formula to add

Definition at line 319 of file Manager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ allModels()

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

inlineinherited

Returns: A list of all assignments, such that they satisfy the conjunction of the so far added formulas.

Note, that an assignment is only provided if the conjunction of so far added formulas is satisfiable. Furthermore, when solving non-linear real arithmetic formulas the assignment could contain other variables or freshly introduced variables.

Definition at line 213 of file Manager.h.

Here is the call graph for this function:

◆ check()

Answer smtrat::Manager::check ( bool _full = true )

inherited

Checks the so far added formulas for satisfiability.

Returns: True, if the conjunction of the so far added formulas is satisfiable; False, if it not satisfiable; Unknown, if this solver cannot decide whether it is satisfiable or not.

Definition at line 115 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ clear()

void smtrat::Manager::clear ( )

inlineinherited

Definition at line 163 of file Manager.h.

Here is the call graph for this function:

◆ clearInformationRelevantFormula()

void smtrat::Manager::clearInformationRelevantFormula ( )

inlineinherited

Deletes all InformationRelevantFormula.

Definition at line 327 of file Manager.h.

◆ deinform()

void smtrat::Manager::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 81 of file Manager.cpp.

Here is the call graph for this function:

◆ formula()

const ModuleInput& smtrat::Manager::formula ( ) const

inlineinherited

Returns: The conjunction of so far added formulas.

Definition at line 229 of file Manager.h.

Here is the caller graph for this function:

◆ formulaBegin()

ModuleInput::iterator smtrat::Manager::formulaBegin ( )

inlineinherited

Definition at line 235 of file Manager.h.

Here is the call graph for this function:

◆ formulaEnd()

ModuleInput::iterator smtrat::Manager::formulaEnd ( )

inlineinherited

Definition at line 239 of file Manager.h.

Here is the call graph for this function:

◆ getAllBackends()

std::vector<Module*> smtrat::Manager::getAllBackends ( Module * _module ) const

inlineprotectedinherited

Gets all backends so far instantiated according the strategy and all previous enquiries of the given module.

Parameters

_module The module to get all backends so far instantiated according the strategy and all previous enquiries of this module.

Returns: All backends so far instantiated according the strategy and all previous enquiries of the given module.

Definition at line 411 of file Manager.h.

Here is the caller graph for this function:

◆ getAllGeneratedModules()

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

inlineinherited

Returns: All instantiated modules of the solver belonging to this manager.

Definition at line 288 of file Manager.h.

◆ getBackends()

std::vector< Module * > smtrat::Manager::getBackends	(	Module *	_requiredBy,
		std::atomic_bool *	_foundAnswer
	)

protectedinherited

Get the backends to call for the given problem instance required by the given module.

Parameters

_requiredBy	The module asking for a backend.
_foundAnswer	A conditional

Returns: A vector of modules, which the module defined by _requiredBy calls in parallel to achieve an answer to the given instance.

Definition at line 279 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getInformationRelevantFormulas()

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

inlineprotectedinherited

Gets all InformationRelevantFormulas.

Returns: Set of all formulas

Definition at line 460 of file Manager.h.

Here is the caller graph for this function:

◆ getInputSimplified()

std::pair< bool, FormulaT > smtrat::Manager::getInputSimplified ( )

inherited

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

Definition at line 149 of file Manager.cpp.

Here is the call graph for this function:

◆ getModelEqualities()

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

inherited

Determines variables assigned by the currently found satisfying assignment to an equal value in their domain.

Returns: A list of vectors of variables, stating that the variables in one vector are assigned to equal values.

Definition at line 127 of file Manager.cpp.

Here is the call graph for this function:

◆ infeasibleSubsets()

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

inherited

Returns: All infeasible subsets of the set so far added formulas.

Note, that the conjunction of the so far added formulas must be inconsistent to receive an infeasible subset.

Definition at line 122 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ inform()

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

inherited

Informs the solver about a constraint.

Optimally, it should be informed about all constraints, which it will receive eventually, before any of them is added as part of a formula with the interface add(..).

Parameters

_constraint The constraint to inform about.

Returns: false, if it is easy to decide (for any module used of this solver), whether the constraint itself is inconsistent; true, otherwise.

Definition at line 76 of file Manager.cpp.

Here is the call graph for this function:

◆ isLemmaLevel()

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

inlineinherited

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

Parameters

level Level to check.

Definition at line 345 of file Manager.h.

Here is the caller graph for this function:

◆ lemmas()

std::vector< FormulaT > smtrat::Manager::lemmas ( )

inherited

Returns the lemmas/tautologies which were made during the last solving provoked by check().

These lemmas can be used in the same manner as infeasible subsets are used.

Returns: The lemmas/tautologies made during solving.

Definition at line 138 of file Manager.cpp.

Here is the call graph for this function:

◆ logic()

auto smtrat::Manager::logic ( ) const

inlineinherited

Returns: A constant reference to the logic this solver considers.

Definition at line 304 of file Manager.h.

Here is the caller graph for this function:

◆ model()

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

inherited

Returns: An assignment of the variables, which occur in the so far added formulas, to values of their domains, such that it satisfies the conjunction of these formulas.

Note, that an assignment is only provided if the conjunction of so far added formulas is satisfiable. Furthermore, when solving non-linear real arithmetic formulas the assignment could contain other variables or freshly introduced variables.

Definition at line 132 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ objectiveVariable()

const carl::Variable& smtrat::Manager::objectiveVariable ( ) const

inlineinherited

Definition at line 172 of file Manager.h.

Here is the caller graph for this function:

◆ pop() [1/2]

bool smtrat::Manager::pop ( void )

inherited

Pops a backtrack point from the stack of backtrack points.

This provokes, that all formulas which have been added after that backtrack point are removed.

Note, that this interface has not necessarily be used to apply a solver constructed with SMT-RAT, but is often required by state-of-the-art SMT solvers when embedding a theory solver constructed with SMT-RAT into them.

Definition at line 166 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pop() [2/2]

void smtrat::Manager::pop ( size_t _levels )

inherited

Definition at line 180 of file Manager.cpp.

Here is the call graph for this function:

◆ printAllAssignments()

void smtrat::Manager::printAllAssignments ( std::ostream & _out = std::cout )

inlineinherited

Prints all assignments of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable.

Parameters

_out	The stream to print on.

Definition at line 257 of file Manager.h.

Here is the call graph for this function:

◆ printAssignment()

void smtrat::Manager::printAssignment ( ) const

inherited

Prints the currently found assignment of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable.

Definition at line 154 of file Manager.cpp.

Here is the call graph for this function:

◆ printBackTrackStack()

void smtrat::Manager::printBackTrackStack ( std::ostream & _out = std::cout ) const

inherited

Prints the stack of backtrack points.

Parameters

_out	The stream to print on.

Definition at line 258 of file Manager.cpp.

Here is the call graph for this function:

◆ printInfeasibleSubset()

void smtrat::Manager::printInfeasibleSubset ( std::ostream & _out = std::cout ) const

inherited

Prints the first found infeasible subset of the set of received formulas.

Parameters

_out	The stream to print on.

Definition at line 237 of file Manager.cpp.

Here is the call graph for this function:

◆ printStrategyGraph()

void smtrat::Manager::printStrategyGraph ( std::ostream & _out = std::cout ) const

inlineinherited

Prints the strategy of the solver maintained by this manager.

Parameters

_out	The stream to print on.

Definition at line 278 of file Manager.h.

◆ push()

void smtrat::Manager::push ( void )

inlineinherited

Pushes a backtrack point to the stack of backtrack points.

Note, that this interface has not necessarily be used to apply a solver constructed with SMT-RAT, but is often required by state-of-the-art SMT solvers when embedding a theory solver constructed with SMT-RAT into them.

Definition at line 142 of file Manager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rDebugOutputChannel()

std::ostream& smtrat::Manager::rDebugOutputChannel ( )

inlineinherited

Returns: The stream to print the debug information on.

Definition at line 296 of file Manager.h.

◆ remove() [1/2]

ModuleInput::iterator smtrat::Manager::remove ( const FormulaT & _subformula )

inlineinherited

Temporarily added: (TODO: Discuss with Gereon) Removes the given formula in the conjunction of formulas, which will be considered for the next satisfiability check.

Parameters

_subformula The formula to remove.

Returns: An iterator to the formula after the position of the just removed formula. If the removed formula has been the last element, the end of the conjunction of formulas, which will be considered for the next satisfiability check is returned.

Definition at line 378 of file Manager.h.

Here is the call graph for this function:

◆ remove() [2/2]

ModuleInput::iterator smtrat::Manager::remove ( ModuleInput::iterator _subformula )

inherited

Removes the formula at the given position in the conjunction of formulas, which will be considered for the next satisfiability check.

Parameters

_subformula The position of the formula to remove.

Returns: An iterator to the formula after the position of the just removed formula. If the removed formula has been the last element, the end of the conjunction of formulas, which will be considered for the next satisfiability check is returned.

Definition at line 159 of file Manager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset()

void smtrat::Manager::reset ( )

inherited

Definition at line 186 of file Manager.cpp.

Here is the call graph for this function:

◆ rLogic()

auto& smtrat::Manager::rLogic ( )

inlineinherited

Returns: A reference to the logic this solver considers.

Definition at line 311 of file Manager.h.

◆ setLemmaLevel()

void smtrat::Manager::setLemmaLevel ( LemmaLevel level )

inlineinherited

Sets the current level for lemma generation.

Parameters

level Level

Definition at line 336 of file Manager.h.

◆ setObjectiveVariable()

void smtrat::Manager::setObjectiveVariable ( carl::Variable var )

inlineinherited

Definition at line 168 of file Manager.h.

Here is the call graph for this function:

◆ setStrategy() [1/2]

void smtrat::Manager::setStrategy ( const BackendLink & backend )

inlineprotectedinherited

Definition at line 392 of file Manager.h.

Here is the call graph for this function:

◆ setStrategy() [2/2]

void smtrat::Manager::setStrategy ( const std::initializer_list< BackendLink > & backends )

inlineprotectedinherited

Definition at line 385 of file Manager.h.

Here is the call graph for this function:

Field Documentation

◆ mBackendsOfModules

std::map<const Module* const, std::vector<Module*> > smtrat::Manager::mBackendsOfModules

privateinherited

a mapping of each module to its backends

Definition at line 49 of file Manager.h.

◆ mBackendsUptodate

bool smtrat::Manager::mBackendsUptodate

privateinherited

a Boolean showing whether the manager has received new constraint after the last consistency check

Definition at line 53 of file Manager.h.

◆ mBacktrackPoints

std::vector<ModuleInput::iterator> smtrat::Manager::mBacktrackPoints

privateinherited

Contains the backtrack points, that are iterators to the last formula to be kept when backtracking to the respective point.

Definition at line 45 of file Manager.h.

◆ mDebugOutputChannel

std::ostream smtrat::Manager::mDebugOutputChannel

privateinherited

channel to write debug output

Definition at line 57 of file Manager.h.

◆ mGeneratedModules

std::vector<Module*> smtrat::Manager::mGeneratedModules

privateinherited

all generated instances of modules

Definition at line 47 of file Manager.h.

◆ mInformationRelevantFormula

std::set<FormulaT> smtrat::Manager::mInformationRelevantFormula

privateinherited

List of formula which are relevant for certain tasks.

Definition at line 61 of file Manager.h.

◆ mLemmaLevel

LemmaLevel smtrat::Manager::mLemmaLevel

privateinherited

Level of lemma generation.

Definition at line 63 of file Manager.h.

◆ mLogic

carl::Logic smtrat::Manager::mLogic

privateinherited

the logic this solver considers

Definition at line 59 of file Manager.h.

◆ mObjectiveVariable

carl::Variable smtrat::Manager::mObjectiveVariable

privateinherited

objective variable

Definition at line 65 of file Manager.h.

◆ mpPassedFormula

ModuleInput* smtrat::Manager::mpPassedFormula

privateinherited

the constraints so far passed to the primary backend

Definition at line 41 of file Manager.h.

◆ mpPrimaryBackend

Module* smtrat::Manager::mpPrimaryBackend

privateinherited

the primary backends

Definition at line 51 of file Manager.h.

◆ mPrimaryBackendFoundAnswer

smtrat::Conditionals smtrat::Manager::mPrimaryBackendFoundAnswer

privateinherited

a vector of flags, which indicate that an answer has been found of an antecessor module of the primary module

Definition at line 39 of file Manager.h.

◆ mPropositions

carl::Condition smtrat::Manager::mPropositions

privateinherited

The propositions of the passed formula.

Definition at line 43 of file Manager.h.

◆ mStrategyGraph

StrategyGraph smtrat::Manager::mStrategyGraph

privateinherited

primary strategy

Definition at line 55 of file Manager.h.

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

smtrat-strategies/strategies/MCSAT/PPNL.h

Public Member Functions

Protected Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ MCSAT_PPNL()

Member Function Documentation

◆ add()

◆ addBackend() [1/2]

◆ addBackend() [2/2]

◆ addEdge()

◆ addInformationRelevantFormula()

◆ allModels()

◆ check()

◆ clear()

◆ clearInformationRelevantFormula()

◆ deinform()

◆ formula()

◆ formulaBegin()

◆ formulaEnd()

◆ getAllBackends()

◆ getAllGeneratedModules()

◆ getBackends()

◆ getInformationRelevantFormulas()

◆ getInputSimplified()

◆ getModelEqualities()

◆ infeasibleSubsets()

◆ inform()

◆ isLemmaLevel()

◆ lemmas()

◆ logic()

◆ model()

◆ objectiveVariable()

◆ pop() [1/2]

◆ pop() [2/2]

◆ printAllAssignments()

◆ printAssignment()

◆ printBackTrackStack()

◆ printInfeasibleSubset()

◆ printStrategyGraph()

◆ push()

◆ rDebugOutputChannel()

◆ remove() [1/2]

◆ remove() [2/2]

◆ reset()

◆ rLogic()

◆ setLemmaLevel()

◆ setObjectiveVariable()

◆ setStrategy() [1/2]

◆ setStrategy() [2/2]

Field Documentation

◆ mBackendsOfModules

◆ mBackendsUptodate

◆ mBacktrackPoints

◆ mDebugOutputChannel

◆ mGeneratedModules

◆ mInformationRelevantFormula

◆ mLemmaLevel

◆ mLogic

◆ mObjectiveVariable

◆ mpPassedFormula

◆ mpPrimaryBackend

◆ mPrimaryBackendFoundAnswer

◆ mPropositions

◆ mStrategyGraph