#include <ModelFormulaSubstitution.h>

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

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

[legend]

Public Member Functions
	ModelFormulaSubstitution (const Formula< Poly > &f)

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

virtual void	add (const Rational &)
	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 > &m) 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 Formula< Poly > &	getFormula () const

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
Formula< Poly >	mFormula

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

Detailed Description

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

Definition at line 8 of file ModelFormulaSubstitution.h.

Member Typedef Documentation

◆ Super

template<typename Rational , typename Poly >

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

private

Definition at line 10 of file ModelFormulaSubstitution.h.

Constructor & Destructor Documentation

◆ ModelFormulaSubstitution()

template<typename Rational , typename Poly >

carl::ModelFormulaSubstitution< Rational, Poly >::ModelFormulaSubstitution ( const Formula< Poly > & f )

inline

Definition at line 13 of file ModelFormulaSubstitution.h.

Member Function Documentation

◆ add()

template<typename Rational , typename Poly >

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

inlinevirtual

Add a rational to this model substitution.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 16 of file ModelFormulaSubstitution.h.

◆ clone()

template<typename Rational , typename Poly >

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

inlinevirtual

Create a copy of this model substitution.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 17 of file ModelFormulaSubstitution.h.

◆ dependsOn()

template<typename Rational , typename Poly >

virtual bool carl::ModelFormulaSubstitution< 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 27 of file ModelFormulaSubstitution.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::ModelFormulaSubstitution< Rational, Poly >::evaluateSubstitution ( const Model< Rational, Poly > & model ) const

inlinevirtual

Evaluate this substitution with respect to the given model.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 24 of file ModelFormulaSubstitution.h.

Here is the call graph for this function:

◆ getFormula()

template<typename Rational , typename Poly >

const Formula<Poly>& carl::ModelFormulaSubstitution< Rational, Poly >::getFormula ( ) const

inline

Definition at line 43 of file ModelFormulaSubstitution.h.

◆ getModelValue()

template<typename Rational , typename Poly >

template<typename Iterator >

const ModelValue<Rational,Poly>& carl::ModelSubstitution< Rational, Poly >::getModelValue	(	Iterator	_mvit,
		Model< Rational, Poly > &	_model
	)

inlineinherited

Definition at line 66 of file ModelSubstitution.h.

Here is the call graph for this function:

◆ multiplyBy()

template<typename Rational , typename Poly >

virtual void carl::ModelFormulaSubstitution< Rational, Poly >::multiplyBy ( const Rational & _number )

inlinevirtual

Multiply this model substitution by a rational.

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 15 of file ModelFormulaSubstitution.h.

◆ print()

template<typename Rational , typename Poly >

virtual void carl::ModelFormulaSubstitution< Rational, Poly >::print ( std::ostream & os ) const

inlinevirtual

Print this substitution to the given output stream.

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

Definition at line 39 of file ModelFormulaSubstitution.h.

◆ representingFormula()

template<typename Rational , typename Poly >

virtual Formula<Poly> carl::ModelFormulaSubstitution< Rational, Poly >::representingFormula ( const ModelVariable & mv )

inlinevirtual

Implements carl::ModelSubstitution< Rational, Poly >.

Definition at line 20 of file ModelFormulaSubstitution.h.

Here is the call graph for this function:

◆ resetCache()

template<typename Rational , typename Poly >

void carl::ModelSubstitution< Rational, Poly >::resetCache ( ) const

inlineinherited

Definition at line 43 of file ModelSubstitution.h.

Field Documentation

◆ mCachedValue

template<typename Rational , typename Poly >

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

mutableprivateinherited

Definition at line 28 of file ModelSubstitution.h.

◆ mFormula

template<typename Rational , typename Poly >

Formula<Poly> carl::ModelFormulaSubstitution< Rational, Poly >::mFormula

private

Definition at line 11 of file ModelFormulaSubstitution.h.

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

carl-formula/model/ModelSubstitution.h
carl-formula/model/substitutions/ModelFormulaSubstitution.h

Public Member Functions

Private Types

Private Attributes

Detailed Description

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

Member Typedef Documentation

◆ Super

Constructor & Destructor Documentation

◆ ModelFormulaSubstitution()

Member Function Documentation

◆ add()

◆ clone()

◆ dependsOn()

◆ evaluate()

◆ evaluateSubstitution()

◆ getFormula()

◆ getModelValue()

◆ multiplyBy()

◆ print()

◆ representingFormula()

◆ resetCache()

Field Documentation

◆ mCachedValue

◆ mFormula

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