#include <ModelConditionalSubstitution.h>

Inheritance diagram for carl::ModelConditionalSubstitution< Rational, Poly >:

Collaboration diagram for carl::ModelConditionalSubstitution< Rational, Poly >:

[legend]

Public Member Functions
	ModelConditionalSubstitution (const std::vector< std::pair< Formula< Poly >, ModelValue< Rational, Poly >>> &values)

	ModelConditionalSubstitution (std::initializer_list< std::pair< Formula< Poly >, ModelValue< Rational, Poly >>> values)

virtual void	multiplyBy (const Rational &n)
	Multiply this model substitution by a rational. More...

virtual void	add (const Rational &n)
	Add a rational to this model substitution. More...

virtual ModelSubstitutionPtr< Rational, Poly >	clone () const
	Create a copy of this model substitution. More...

virtual Formula< Poly >	representingFormula (const ModelVariable &mv)

virtual ModelValue< Rational, Poly >	evaluateSubstitution (const Model< Rational, Poly > &model) const
	Evaluate this substitution with respect to the given model. More...

virtual bool	dependsOn (const ModelVariable &var) const
	Check if this substitution needs the given model variable. More...

virtual void	print (std::ostream &os) const
	Print this substitution to the given output stream. More...

const ModelValue< Rational, Poly > &	evaluate (const Model< Rational, Poly > &model) const

void	resetCache () const

template<typename Iterator >
const ModelValue< Rational, Poly > &	getModelValue (Iterator _mvit, Model< Rational, Poly > &_model)

Private Types
using	Super = ModelSubstitution< Rational, Poly >

Private Attributes
std::vector< std::pair< Formula< Poly >, ModelValue< Rational, Poly > > >	mValues

std::optional< ModelValue< Rational, Poly > >	mCachedValue

Detailed Description

template<typename Rational, typename Poly>
class carl::ModelConditionalSubstitution< Rational, Poly >

Definition at line 8 of file ModelConditionalSubstitution.h.

Member Typedef Documentation

◆ Super

template<typename Rational , typename Poly >

using carl::ModelConditionalSubstitution< Rational, Poly >::Super = ModelSubstitution<Rational,Poly>

private

Definition at line 10 of file ModelConditionalSubstitution.h.

Constructor & Destructor Documentation

◆ ModelConditionalSubstitution() [1/2]

template<typename Rational , typename Poly >

carl::ModelConditionalSubstitution< Rational, Poly >::ModelConditionalSubstitution ( const std::vector< std::pair< Formula< Poly >, ModelValue< Rational, Poly >>> & values )

inline

Definition at line 13 of file ModelConditionalSubstitution.h.

◆ ModelConditionalSubstitution() [2/2]

template<typename Rational , typename Poly >

carl::ModelConditionalSubstitution< Rational, Poly >::ModelConditionalSubstitution ( std::initializer_list< std::pair< Formula< Poly >, ModelValue< Rational, Poly >>> values )

inline

Definition at line 15 of file ModelConditionalSubstitution.h.

Member Function Documentation

◆ add()

template<typename Rational , typename Poly >

virtual void carl::ModelConditionalSubstitution< Rational, Poly >::add ( const Rational & _number )

inlinevirtual

Add a rational to this model substitution.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 20 of file ModelConditionalSubstitution.h.

◆ clone()

template<typename Rational , typename Poly >

virtual ModelSubstitutionPtr<Rational,Poly> carl::ModelConditionalSubstitution< Rational, Poly >::clone ( ) const

inlinevirtual

Create a copy of this model substitution.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 23 of file ModelConditionalSubstitution.h.

◆ dependsOn()

template<typename Rational , typename Poly >

virtual bool carl::ModelConditionalSubstitution< Rational, Poly >::dependsOn ( const ModelVariable & ) const

inlinevirtual

Check if this substitution needs the given model variable.

Reimplemented from carl::ModelSubstitution< Rational, Poly >.

Definition at line 39 of file ModelConditionalSubstitution.h.

Here is the call graph for this function:

◆ evaluate()

template<typename Rational , typename Poly >

const ModelValue<Rational, Poly>& carl::ModelSubstitution< Rational, Poly >::evaluate ( const Model< Rational, Poly > & model ) const

inlineinherited

Definition at line 37 of file ModelSubstitution.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluateSubstitution()

template<typename Rational , typename Poly >

virtual ModelValue<Rational,Poly> carl::ModelConditionalSubstitution< Rational, Poly >::evaluateSubstitution ( const Model< Rational, Poly > & model ) const