The input formula a module has to consider for it's satisfiability check. More...

#include <ModuleInput.h>

Inheritance diagram for smtrat::ModuleInput:

Collaboration diagram for smtrat::ModuleInput:

Data Structures
struct	IteratorCompare

Public Types
typedef super::iterator	iterator
	Passing through the list::iterator. More...

typedef super::const_iterator	const_iterator
	Passing through the list::const_iterator. More...

Public Member Functions
	ModuleInput ()
	Constructs a module input. More...

carl::Condition	properties () const

bool	is_constraint_conjunction () const

bool	isConstraintLiteralConjunction () const

bool	is_real_constraint_conjunction () const

bool	isRealConstraintLiteralConjunction () const

bool	is_integer_constraint_conjunction () const

bool	isIntegerConstraintLiteralConjunction () const

bool	containsBitVectorConstraints () const

bool	containsBooleanVariables () const

bool	containsRealVariables () const

bool	containsIntegerVariables () const

bool	containsUninterpretedEquations () const

bool	is_only_propositional () const

unsigned	satisfiedBy (const Model &_assignment) const

unsigned	satisfiedBy (const RationalAssignment &_assignment) const

const auto &	back () const

iterator	begin ()

iterator	end ()

const_iterator	begin () const

const_iterator	end () const

auto	rbegin () const

auto	rend () const

bool	empty () const

size_t	size () const

iterator	find (const FormulaT &_formula)

const_iterator	find (const FormulaT &_formula) const

iterator	find (const_iterator _hint, const FormulaT &_formula)

const_iterator	find (const_iterator _hint, const FormulaT &_formula) const

bool	contains (const FormulaT &_subformula) const

void	updateProperties ()
	Updates all properties of the formula underlying this module input. More...

void	gatherVariables (carl::carlVariables &vars) const

	operator FormulaT () const

void	addOrigin (iterator _formula, const FormulaT &_origin)

iterator	erase (iterator _formula)

void	clearOrigins (iterator _formula)

bool	removeOrigin (iterator _formula, const FormulaT &_origin)

bool	removeOrigins (iterator _formula, const std::shared_ptr< FormulasT > &_origins)

std::pair< iterator, bool >	add (const FormulaT &_formula, bool _mightBeConjunction=true)

std::pair< iterator, bool >	add (const FormulaT &_formula, const FormulaT &_origins, bool _mightBeConjunction=true)

std::pair< iterator, bool >	add (const FormulaT &_formula, const std::shared_ptr< FormulasT > &_origins, bool _mightBeConjunction=true)

std::pair< iterator, bool >	add (const FormulaT &_formula, bool _hasSingleOrigin, const FormulaT &_origin, const std::shared_ptr< FormulasT > &_origins, bool _mightBeConjunction=true)

Private Types
typedef std::list< FormulaWithOrigins >	super

Private Attributes
carl::Condition	mProperties
	Store some properties about the conjunction of the stored formulas. More...

bool	mPropertiesUpdated
	A flag indicating whether the properties of this module input are updated. More...

carl::FastMap< FormulaT, iterator >	mFormulaPositionMap
	Maps all formulas occurring (in the origins) at pos i in this module input to i. This is for a faster access. More...

T	elements
	STL member. More...

Friends
class	Module

class	Manager

Detailed Description

The input formula a module has to consider for it's satisfiability check.

It is a list of formulas and semantically considered as their conjunction.

Definition at line 130 of file ModuleInput.h.

Member Typedef Documentation

◆ const_iterator

typedef super::const_iterator smtrat::ModuleInput::const_iterator

Passing through the list::const_iterator.

Definition at line 146 of file ModuleInput.h.

◆ iterator

typedef super::iterator smtrat::ModuleInput::iterator

Passing through the list::iterator.

Definition at line 144 of file ModuleInput.h.

◆ super

typedef std::list<FormulaWithOrigins> smtrat::ModuleInput::super

private

Definition at line 138 of file ModuleInput.h.

Constructor & Destructor Documentation

◆ ModuleInput()

smtrat::ModuleInput::ModuleInput ( )

inline

Constructs a module input.

Definition at line 163 of file ModuleInput.h.

Member Function Documentation

◆ add() [1/4]

std::pair<iterator,bool> smtrat::ModuleInput::add	(	const FormulaT &	_formula,
		bool	_hasSingleOrigin,
		const FormulaT &	_origin,
		const std::shared_ptr< FormulasT > &	_origins,
		bool	_mightBeConjunction = `true`
	)

◆ add() [2/4]

std::pair<iterator,bool> smtrat::ModuleInput::add	(	const FormulaT &	_formula,
		bool	_mightBeConjunction = `true`
	)

inline

Definition at line 430 of file ModuleInput.h.

Here is the caller graph for this function:

◆ add() [3/4]

std::pair<iterator,bool> smtrat::ModuleInput::add	(	const FormulaT &	_formula,
		const FormulaT &	_origins,
		bool	_mightBeConjunction = `true`
	)

inline

Definition at line 435 of file ModuleInput.h.

Here is the call graph for this function:

◆ add() [4/4]

std::pair<iterator,bool> smtrat::ModuleInput::add	(	const FormulaT &	_formula,
		const std::shared_ptr< FormulasT > &	_origins,
		bool	_mightBeConjunction = `true`
	)

inline

Definition at line 440 of file ModuleInput.h.

Here is the call graph for this function:

◆ addOrigin()

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

inline

Definition at line 404 of file ModuleInput.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ back()

const auto& smtrat::ModuleInput::back ( ) const

inline

Definition at line 317 of file ModuleInput.h.

◆ begin() [1/2]

iterator smtrat::ModuleInput::begin ( )

inline

Definition at line 321 of file ModuleInput.h.

Here is the caller graph for this function:

◆ begin() [2/2]

const_iterator smtrat::ModuleInput::begin ( ) const

inline

Definition at line 331 of file ModuleInput.h.

◆ clearOrigins()

void smtrat::ModuleInput::clearOrigins ( iterator _formula )

inline

Definition at line 417 of file ModuleInput.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ contains()

bool smtrat::ModuleInput::contains ( const FormulaT & _subformula ) const

inline

Parameters

_subformula The formula for which to check whether it is one of the stored formulas.

Returns: true, if the given formula is one of the stored formulas; false, otherwise.

Definition at line 372 of file ModuleInput.h.

Here is the caller graph for this function:

◆ containsBitVectorConstraints()

bool smtrat::ModuleInput::containsBitVectorConstraints ( ) const

inline

Returns: true, if this formula contains bit vector constraints; false, otherwise.

Definition at line 245 of file ModuleInput.h.

◆ containsBooleanVariables()

bool smtrat::ModuleInput::containsBooleanVariables ( ) const

inline

Returns: true, if this formula contains Boolean variables; false, otherwise.

Definition at line 254 of file ModuleInput.h.

◆ containsIntegerVariables()

bool smtrat::ModuleInput::containsIntegerVariables ( ) const

inline

Returns: true, if this formula contains Boolean variables; false, otherwise.

Definition at line 272 of file ModuleInput.h.

◆ containsRealVariables()

bool smtrat::ModuleInput::containsRealVariables ( ) const

inline

Returns: true, if this formula contains Boolean variables; false, otherwise.

Definition at line 263 of file ModuleInput.h.

◆ containsUninterpretedEquations()

bool smtrat::ModuleInput::containsUninterpretedEquations ( ) const

inline

Returns: true, if this formula contains uninterpreted equations; false, otherwise.

Definition at line 281 of file ModuleInput.h.

◆ empty()

bool smtrat::ModuleInput::empty ( ) const

inline

Definition at line 349 of file ModuleInput.h.

Here is the caller graph for this function:

◆ end() [1/2]

iterator smtrat::ModuleInput::end ( )

inline

Definition at line 326 of file ModuleInput.h.

Here is the caller graph for this function:

◆ end() [2/2]

const_iterator smtrat::ModuleInput::end ( ) const

inline

Definition at line 336 of file ModuleInput.h.

◆ erase()

ModuleInput::iterator smtrat::ModuleInput::erase ( iterator _formula )

Definition at line 98 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ find() [1/4]

ModuleInput::iterator smtrat::ModuleInput::find ( const FormulaT & _formula )

Definition at line 46 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ find() [2/4]

ModuleInput::const_iterator smtrat::ModuleInput::find ( const FormulaT & _formula ) const

Definition at line 59 of file ModuleInput.cpp.

Here is the call graph for this function:

◆ find() [3/4]

ModuleInput::iterator smtrat::ModuleInput::find	(	const_iterator	_hint,
		const FormulaT &	_formula
	)

Definition at line 72 of file ModuleInput.cpp.

Here is the call graph for this function:

◆ find() [4/4]

ModuleInput::const_iterator smtrat::ModuleInput::find	(	const_iterator	_hint,
		const FormulaT &	_formula
	)		const

Definition at line 85 of file ModuleInput.cpp.

Here is the call graph for this function:

◆ gatherVariables()

void smtrat::ModuleInput::gatherVariables ( carl::carlVariables & vars ) const

inline

Definition at line 382 of file ModuleInput.h.

Here is the call graph for this function:

◆ is_constraint_conjunction()

bool smtrat::ModuleInput::is_constraint_conjunction ( ) const

inline

Returns: true, if this formula is a conjunction of constraints; false, otherwise.

Definition at line 185 of file ModuleInput.h.

Here is the caller graph for this function:

◆ is_integer_constraint_conjunction()

bool smtrat::ModuleInput::is_integer_constraint_conjunction ( ) const

inline

Returns: true, if this formula is a conjunction of integer constraints; false, otherwise.

Definition at line 227 of file ModuleInput.h.

Here is the call graph for this function:

◆ is_only_propositional()

bool smtrat::ModuleInput::is_only_propositional ( ) const

inline

Returns: true, if this formula is propositional; false, otherwise.

Definition at line 290 of file ModuleInput.h.

Here is the call graph for this function:

◆ is_real_constraint_conjunction()

bool smtrat::ModuleInput::is_real_constraint_conjunction ( ) const

inline

Returns: true, if this formula is a conjunction of real constraints; false, otherwise.

Definition at line 209 of file ModuleInput.h.

Here is the call graph for this function:

◆ isConstraintLiteralConjunction()

bool smtrat::ModuleInput::isConstraintLiteralConjunction ( ) const

inline

Returns: true, if this formula is a conjunction of literals of constraints; false, otherwise.

Definition at line 197 of file ModuleInput.h.

Here is the caller graph for this function:

◆ isIntegerConstraintLiteralConjunction()

bool smtrat::ModuleInput::isIntegerConstraintLiteralConjunction ( ) const

inline

Returns: true, if this formula is a conjunction of literals of integer constraints; false, otherwise.

Definition at line 236 of file ModuleInput.h.

Here is the call graph for this function:

◆ isRealConstraintLiteralConjunction()

bool smtrat::ModuleInput::isRealConstraintLiteralConjunction ( ) const

inline

Returns: true, if this formula is a conjunction of literals of real constraints; false, otherwise.

Definition at line 218 of file ModuleInput.h.

Here is the call graph for this function:

◆ operator FormulaT()

smtrat::ModuleInput::operator FormulaT ( ) const

inlineexplicit

Definition at line 396 of file ModuleInput.h.

◆ properties()

carl::Condition smtrat::ModuleInput::properties ( ) const

inline

Returns: All known properties of the underlying formula of this module input.

Definition at line 175 of file ModuleInput.h.

Here is the caller graph for this function:

◆ rbegin()

auto smtrat::ModuleInput::rbegin ( ) const

inline

Definition at line 341 of file ModuleInput.h.

◆ removeOrigin()

bool smtrat::ModuleInput::removeOrigin	(	iterator	_formula,
		const FormulaT &	_origin
	)

Definition at line 106 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeOrigins()

bool smtrat::ModuleInput::removeOrigins	(	iterator	_formula,
		const std::shared_ptr< FormulasT > &	_origins
	)

Definition at line 140 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rend()

auto smtrat::ModuleInput::rend ( ) const

inline

Definition at line 345 of file ModuleInput.h.

◆ satisfiedBy() [1/2]

unsigned smtrat::ModuleInput::satisfiedBy ( const Model & _assignment ) const

Parameters

_assignment The model to check conjunction of the stored formulas against.

Returns: 1, if the conjunction of the stored formulas is satisfied by the given model; 0, if the given model conflicts the conjunction of the stored formulas; 2, if it cannot be determined cheaply, whether the given model conflicts or satisfies the conjunction of the stored formulas.

Definition at line 33 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ satisfiedBy() [2/2]

unsigned smtrat::ModuleInput::satisfiedBy ( const RationalAssignment & _assignment ) const

Parameters

_assignment The assignment to check conjunction of the stored formulas against.

Returns: 1, if the conjunction of the stored formulas is satisfied by the given assignment; 0, if the given assignment conflicts the conjunction of the stored formulas; 2, if it cannot be determined cheaply, whether the given assignment conflicts or satisfies the conjunction of the stored formulas.

Definition at line 15 of file ModuleInput.cpp.

Here is the call graph for this function:

◆ size()

size_t smtrat::ModuleInput::size ( void ) const

inline

Definition at line 354 of file ModuleInput.h.

◆ updateProperties()

void smtrat::ModuleInput::updateProperties ( )

Updates all properties of the formula underlying this module input.

Definition at line 167 of file ModuleInput.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ Manager

friend class Manager

friend

Definition at line 134 of file ModuleInput.h.

◆ Module

friend class Module

friend

Definition at line 132 of file ModuleInput.h.

Field Documentation

◆ elements

T std::list< T >::elements

inherited

STL member.

◆ mFormulaPositionMap

carl::FastMap<FormulaT,iterator> smtrat::ModuleInput::mFormulaPositionMap

private

Maps all formulas occurring (in the origins) at pos i in this module input to i. This is for a faster access.

Definition at line 156 of file ModuleInput.h.

◆ mProperties

carl::Condition smtrat::ModuleInput::mProperties

private

Store some properties about the conjunction of the stored formulas.

Definition at line 152 of file ModuleInput.h.

◆ mPropertiesUpdated

bool smtrat::ModuleInput::mPropertiesUpdated

private

A flag indicating whether the properties of this module input are updated.

Definition at line 154 of file ModuleInput.h.

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

smtrat-solver/ModuleInput.h
smtrat-solver/ModuleInput.cpp

Data Structures

Public Types

Public Member Functions

Private Types

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ iterator

◆ super

Constructor & Destructor Documentation

◆ ModuleInput()

Member Function Documentation

◆ add() [1/4]

◆ add() [2/4]

◆ add() [3/4]

◆ add() [4/4]

◆ addOrigin()

◆ back()

◆ begin() [1/2]

◆ begin() [2/2]

◆ clearOrigins()

◆ contains()

◆ containsBitVectorConstraints()

◆ containsBooleanVariables()

◆ containsIntegerVariables()

◆ containsRealVariables()

◆ containsUninterpretedEquations()

◆ empty()

◆ end() [1/2]

◆ end() [2/2]

◆ erase()

◆ find() [1/4]

◆ find() [2/4]

◆ find() [3/4]

◆ find() [4/4]

◆ gatherVariables()

◆ is_constraint_conjunction()

◆ is_integer_constraint_conjunction()

◆ is_only_propositional()

◆ is_real_constraint_conjunction()

◆ isConstraintLiteralConjunction()

◆ isIntegerConstraintLiteralConjunction()

◆ isRealConstraintLiteralConjunction()

◆ operator FormulaT()

◆ properties()

◆ rbegin()

◆ removeOrigin()

◆ removeOrigins()

◆ rend()

◆ satisfiedBy() [1/2]

◆ satisfiedBy() [2/2]

◆ size()

◆ updateProperties()

Friends And Related Function Documentation

◆ Manager

◆ Module

Field Documentation

◆ elements

◆ mFormulaPositionMap

◆ mProperties

◆ mPropertiesUpdated