Represent a sum type/variant over the different kinds of values that can be assigned to the different kinds of variables that exist in CARL and to use them in a more uniform way, e.g. More...

#include <ModelValue.h>

Public Member Functions
	ModelValue ()=default
	Default constructor. More...

	ModelValue (const ModelValue &mv)

	ModelValue (ModelValue &&mv)=default

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Super>::value, T>::type>
	ModelValue (const T &_t)
	Initialize the Assignment from some valid type of the underlying variant. More...

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Super>::value, T>::type>
	ModelValue (T &&_t)

template<typename ... Args>
	ModelValue (const std::variant< Args... > &variant)

	ModelValue (const MultivariateRoot< Poly > &mr)

ModelValue &	operator= (const ModelValue &mv)

ModelValue &	operator= (ModelValue &&mv)=default

template<typename T >
ModelValue &	operator= (const T &t)
	Assign some value to the underlying variant. More...

template<typename ... Args>
ModelValue &	operator= (const std::variant< Args... > &variant)

ModelValue &	operator= (const MultivariateRoot< Poly > &mr)

template<typename F >
auto	visit (F &&f) const

bool	isBool () const

bool	isRational () const

bool	isSqrtEx () const

bool	isRAN () const

bool	isBVValue () const

bool	isSortValue () const

bool	isUFModel () const

bool	isPlusInfinity () const

bool	isMinusInfinity () const

bool	isSubstitution () const

bool	asBool () const

const Rational &	asRational () const

const SqrtEx< Poly > &	asSqrtEx () const

const Poly::RootType &	asRAN () const

const carl::BVValue &	asBVValue () const

const SortValue &	asSortValue () const

const UFModel &	asUFModel () const

UFModel &	asUFModel ()

const InfinityValue &	asInfinity () const

const ModelSubstitutionPtr< Rational, Poly > &	asSubstitution () const

ModelSubstitutionPtr< Rational, Poly > &	asSubstitution ()

Private Types
using	Super = std::variant< bool, Rational, SqrtEx< Poly >, typename Poly::RootType, BVValue, SortValue, UFModel, InfinityValue, ModelSubstitutionPtr< Rational, Poly > >
	Base type we are deriving from. More...

Private Member Functions
template<typename Variant >
Super	clone (const Variant &v) const

Private Attributes
Super	mData

Friends
template<typename R , typename P >
std::ostream &	operator<< (std::ostream &os, const ModelValue< R, P > &mv)

template<typename R , typename P >
bool	operator== (const ModelValue< R, P > &lhs, const ModelValue< R, P > &rhs)

template<typename R , typename P >
bool	operator< (const ModelValue< R, P > &lhs, const ModelValue< R, P > &rhs)

Detailed Description

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

Represent a sum type/variant over the different kinds of values that can be assigned to the different kinds of variables that exist in CARL and to use them in a more uniform way, e.g.

a plain "bool", "infinity", a "carl::RealAlgebraicNumber", a (bitvector) "carl::BVValue" etc.

Definition at line 56 of file ModelValue.h.

Member Typedef Documentation

◆ Super

template<typename Rational , typename Poly >

using carl::ModelValue< Rational, Poly >::Super = std::variant<bool, Rational, SqrtEx<Poly>, typename Poly::RootType, BVValue, SortValue, UFModel, InfinityValue, ModelSubstitutionPtr<Rational,Poly> >

private

Base type we are deriving from.

Definition at line 66 of file ModelValue.h.

Constructor & Destructor Documentation

◆ ModelValue() [1/7]

template<typename Rational , typename Poly >

carl::ModelValue< Rational, Poly >::ModelValue ( )

default

Default constructor.

◆ ModelValue() [2/7]

template<typename Rational , typename Poly >

carl::ModelValue< Rational, Poly >::ModelValue ( const ModelValue< Rational, Poly > & mv )

inline

Definition at line 87 of file ModelValue.h.

◆ ModelValue() [3/7]

template<typename Rational , typename Poly >

carl::ModelValue< Rational, Poly >::ModelValue ( ModelValue< Rational, Poly > && mv )

default

◆ ModelValue() [4/7]

template<typename Rational , typename Poly >

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Super>::value, T>::type>

carl::ModelValue< Rational, Poly >::ModelValue ( const T & _t )

inline

Initialize the Assignment from some valid type of the underlying variant.

Definition at line 96 of file ModelValue.h.

◆ ModelValue() [5/7]

template<typename Rational , typename Poly >

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Super>::value, T>::type>

carl::ModelValue< Rational, Poly >::ModelValue ( T && _t )

inline

Definition at line 99 of file ModelValue.h.

◆ ModelValue() [6/7]

template<typename Rational , typename Poly >

template<typename ... Args>

carl::ModelValue< Rational, Poly >::ModelValue ( const std::variant< Args... > & variant )

inline

Definition at line 102 of file ModelValue.h.

◆ ModelValue() [7/7]

template<typename Rational , typename Poly >

carl::ModelValue< Rational, Poly >::ModelValue ( const MultivariateRoot< Poly > & mr )

inline

Definition at line 104 of file ModelValue.h.

Member Function Documentation

◆ asBool()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::asBool ( ) const

inline

Returns: The stored value as a bool.

Definition at line 209 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asBVValue()

template<typename Rational , typename Poly >

const carl::BVValue& carl::ModelValue< Rational, Poly >::asBVValue ( ) const

inline

Returns: The stored value as a real algebraic number.

Definition at line 241 of file ModelValue.h.

Here is the call graph for this function:

◆ asInfinity()

template<typename Rational , typename Poly >

const InfinityValue& carl::ModelValue< Rational, Poly >::asInfinity ( ) const

inline

Returns: The stored value as a infinity value.

Definition at line 268 of file ModelValue.h.

Here is the call graph for this function:

◆ asRAN()

template<typename Rational , typename Poly >

const Poly::RootType& carl::ModelValue< Rational, Poly >::asRAN ( ) const

inline

Returns: The stored value as a real algebraic number.

Definition at line 233 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asRational()

template<typename Rational , typename Poly >

const Rational& carl::ModelValue< Rational, Poly >::asRational ( ) const

inline

Returns: The stored value as a rational.

Definition at line 217 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asSortValue()

template<typename Rational , typename Poly >

const SortValue& carl::ModelValue< Rational, Poly >::asSortValue ( ) const

inline

Returns: The stored value as a sort value.

Definition at line 249 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asSqrtEx()

template<typename Rational , typename Poly >

const SqrtEx<Poly>& carl::ModelValue< Rational, Poly >::asSqrtEx ( ) const

inline

Returns: The stored value as a square root expression.

Definition at line 225 of file ModelValue.h.

Here is the call graph for this function:

◆ asSubstitution() [1/2]

template<typename Rational , typename Poly >

ModelSubstitutionPtr<Rational,Poly>& carl::ModelValue< Rational, Poly >::asSubstitution ( )

inline

Definition at line 277 of file ModelValue.h.

Here is the call graph for this function:

◆ asSubstitution() [2/2]

template<typename Rational , typename Poly >

const ModelSubstitutionPtr<Rational,Poly>& carl::ModelValue< Rational, Poly >::asSubstitution ( ) const

inline

Definition at line 273 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asUFModel() [1/2]

template<typename Rational , typename Poly >

UFModel& carl::ModelValue< Rational, Poly >::asUFModel ( )

inline

Definition at line 261 of file ModelValue.h.

Here is the call graph for this function:

◆ asUFModel() [2/2]

template<typename Rational , typename Poly >

const UFModel& carl::ModelValue< Rational, Poly >::asUFModel ( ) const

inline

Returns: The stored value as a uninterpreted function model.

Definition at line 257 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ clone()

template<typename Rational , typename Poly >

template<typename Variant >

Super carl::ModelValue< Rational, Poly >::clone ( const Variant & v ) const

inlineprivate

Definition at line 71 of file ModelValue.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isBool()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isBool ( ) const

inline

Returns: true, if the stored value is a bool.

Definition at line 143 of file ModelValue.h.

Here is the caller graph for this function:

◆ isBVValue()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isBVValue ( ) const

inline

Returns: true, if the stored value is a bitvector literal.

Definition at line 171 of file ModelValue.h.

Here is the caller graph for this function:

◆ isMinusInfinity()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isMinusInfinity ( ) const

inline

Returns: true, if the stored value is -infinity.

Definition at line 198 of file ModelValue.h.

Here is the caller graph for this function:

◆ isPlusInfinity()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isPlusInfinity ( ) const

inline

Returns: true, if the stored value is +infinity.

Definition at line 192 of file ModelValue.h.

Here is the caller graph for this function:

◆ isRAN()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isRAN ( ) const

inline

Returns: true, if the stored value is a real algebraic number.

Definition at line 164 of file ModelValue.h.

Here is the caller graph for this function:

◆ isRational()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isRational ( ) const

inline

Returns: true, if the stored value is a rational.

Definition at line 150 of file ModelValue.h.

Here is the caller graph for this function:

◆ isSortValue()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isSortValue ( ) const

inline

Returns: true, if the stored value is a sort value.

Definition at line 178 of file ModelValue.h.

Here is the caller graph for this function:

◆ isSqrtEx()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isSqrtEx ( ) const

inline

Returns: true, if the stored value is a square root expression.

Definition at line 157 of file ModelValue.h.

Here is the caller graph for this function:

◆ isSubstitution()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isSubstitution ( ) const

inline

Definition at line 202 of file ModelValue.h.

Here is the caller graph for this function:

◆ isUFModel()

template<typename Rational , typename Poly >

bool carl::ModelValue< Rational, Poly >::isUFModel ( ) const

inline

Returns: true, if the stored value is a uninterpreted function model.

Definition at line 185 of file ModelValue.h.

Here is the caller graph for this function:

◆ operator=() [1/5]

template<typename Rational , typename Poly >

ModelValue& carl::ModelValue< Rational, Poly >::operator= ( const ModelValue< Rational, Poly > & mv )

inline

Definition at line 106 of file ModelValue.h.

Here is the call graph for this function:

◆ operator=() [2/5]

template<typename Rational , typename Poly >

ModelValue& carl::ModelValue< Rational, Poly >::operator= ( const MultivariateRoot< Poly > & mr )

inline

Definition at line 130 of file ModelValue.h.

◆ operator=() [3/5]

template<typename Rational , typename Poly >

template<typename ... Args>

ModelValue& carl::ModelValue< Rational, Poly >::operator= ( const std::variant< Args... > & variant )

inline

Definition at line 125 of file ModelValue.h.

Here is the call graph for this function:

◆ operator=() [4/5]

template<typename Rational , typename Poly >

template<typename T >

ModelValue& carl::ModelValue< Rational, Poly >::operator= ( const T & t )

inline

Assign some value to the underlying variant.

Parameters

t	Some value.

Returns: *this.

Definition at line 119 of file ModelValue.h.

◆ operator=() [5/5]

template<typename Rational , typename Poly >

ModelValue& carl::ModelValue< Rational, Poly >::operator= ( ModelValue< Rational, Poly > && mv )

default

◆ visit()

template<typename Rational , typename Poly >

template<typename F >

auto carl::ModelValue< Rational, Poly >::visit ( F && f ) const

inline

Definition at line 136 of file ModelValue.h.

Here is the call graph for this function:

Friends And Related Function Documentation

◆ operator<

template<typename Rational , typename Poly >

template<typename R , typename P >

bool operator<	(	const ModelValue< R, P > &	lhs,
		const ModelValue< R, P > &	rhs
	)

friend

◆ operator<<

template<typename Rational , typename Poly >

template<typename R , typename P >

std::ostream& operator<<	(	std::ostream &	os,
		const ModelValue< R, P > &	mv
	)

friend

Definition at line 305 of file ModelValue.h.

◆ operator==

template<typename Rational , typename Poly >

template<typename R , typename P >

bool operator==	(	const ModelValue< R, P > &	lhs,
		const ModelValue< R, P > &	rhs
	)

friend

Field Documentation

◆ mData

template<typename Rational , typename Poly >

Super carl::ModelValue< Rational, Poly >::mData

private

Definition at line 68 of file ModelValue.h.

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

carl-formula/model/ModelValue.h

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Detailed Description

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

Member Typedef Documentation

◆ Super

Constructor & Destructor Documentation

◆ ModelValue() [1/7]

◆ ModelValue() [2/7]

◆ ModelValue() [3/7]

◆ ModelValue() [4/7]

◆ ModelValue() [5/7]

◆ ModelValue() [6/7]

◆ ModelValue() [7/7]

Member Function Documentation

◆ asBool()

◆ asBVValue()

◆ asInfinity()

◆ asRAN()

◆ asRational()

◆ asSortValue()

◆ asSqrtEx()

◆ asSubstitution() [1/2]

◆ asSubstitution() [2/2]

◆ asUFModel() [1/2]

◆ asUFModel() [2/2]

◆ clone()

◆ isBool()

◆ isBVValue()

◆ isMinusInfinity()

◆ isPlusInfinity()

◆ isRAN()

◆ isRational()

◆ isSortValue()

◆ isSqrtEx()

◆ isSubstitution()

◆ isUFModel()

◆ operator=() [1/5]

◆ operator=() [2/5]

◆ operator=() [3/5]

◆ operator=() [4/5]

◆ operator=() [5/5]

◆ visit()

Friends And Related Function Documentation

◆ operator<

◆ operator<<

◆ operator==

Field Documentation

◆ mData

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