carl  24.04
Computer ARithmetic Library
Public Member Functions | Private Types | Private Attributes | Friends
carl::ModelVariable Class Reference

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

#include <ModelVariable.h>

Public Member Functions

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Base>::value, T>::type>
 ModelVariable (const T &_t)
 Initialize the ModelVariable from some valid type of the underlying variant. More...
 
bool is_variable () const
 
bool isBVVariable () const
 
bool isUVariable () const
 
bool isFunction () const
 
carl::Variable asVariable () const
 
const carl::BVVariable & asBVVariable () const
 
const carl::UVariable & asUVariable () const
 
const carl::UninterpretedFunction & asFunction () const
 

Private Types

using Base = std::variant< Variable, BVVariable, UVariable, UninterpretedFunction >
 Base type for the content. More...
 

Private Attributes

Base mData
 

Friends

bool operator== (const ModelVariable &lhs, const ModelVariable &rhs)
 Return true if lhs is equal to rhs. More...
 
bool operator< (const ModelVariable &lhs, const ModelVariable &rhs)
 Return true if lhs is smaller than rhs. More...
 
std::ostream & operator<< (std::ostream &os, const ModelVariable &mv)
 

Detailed Description

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

an (algebraic) "carl::Variable", an (uninterpreted) "carl::UVariable", an "carl::UninterpretedFunction" etc.

Definition at line 20 of file ModelVariable.h.

Member Typedef Documentation

◆ Base

using carl::ModelVariable::Base = std::variant<Variable, BVVariable, UVariable, UninterpretedFunction>
private

Base type for the content.

Definition at line 24 of file ModelVariable.h.

Constructor & Destructor Documentation

◆ ModelVariable()

template<typename T , typename T2 = typename std::enable_if<convertible_to_variant<T, Base>::value, T>::type>
carl::ModelVariable::ModelVariable ( const T &  _t)
inline

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

Definition at line 38 of file ModelVariable.h.

Member Function Documentation

◆ asBVVariable()

const carl::BVVariable& carl::ModelVariable::asBVVariable ( ) const
inline
Returns
The stored value as a bitvector variable.

Definition at line 80 of file ModelVariable.h.

Here is the call graph for this function:

◆ asFunction()

const carl::UninterpretedFunction& carl::ModelVariable::asFunction ( ) const
inline
Returns
The stored value as a function.

Definition at line 96 of file ModelVariable.h.

Here is the call graph for this function:

◆ asUVariable()

const carl::UVariable& carl::ModelVariable::asUVariable ( ) const
inline
Returns
The stored value as an uninterpreted variable.

Definition at line 88 of file ModelVariable.h.

Here is the call graph for this function:

◆ asVariable()

carl::Variable carl::ModelVariable::asVariable ( ) const
inline
Returns
The stored value as a variable.

Definition at line 72 of file ModelVariable.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ is_variable()

bool carl::ModelVariable::is_variable ( ) const
inline
Returns
true, if the stored value is a variable.

Definition at line 44 of file ModelVariable.h.

Here is the caller graph for this function:

◆ isBVVariable()

bool carl::ModelVariable::isBVVariable ( ) const
inline
Returns
true, if the stored value is a bitvector variable.

Definition at line 51 of file ModelVariable.h.

Here is the caller graph for this function:

◆ isFunction()

bool carl::ModelVariable::isFunction ( ) const
inline
Returns
true, if the stored value is a function.

Definition at line 65 of file ModelVariable.h.

Here is the caller graph for this function:

◆ isUVariable()

bool carl::ModelVariable::isUVariable ( ) const
inline
Returns
true, if the stored value is an uninterpreted variable.

Definition at line 58 of file ModelVariable.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<

bool operator< ( const ModelVariable &  lhs,
const ModelVariable &  rhs 
)
friend

Return true if lhs is smaller than rhs.

Definition at line 112 of file ModelVariable.h.

◆ operator<<

std::ostream& operator<< ( std::ostream &  os,
const ModelVariable &  mv 
)
friend

Definition at line 116 of file ModelVariable.h.

◆ operator==

bool operator== ( const ModelVariable &  lhs,
const ModelVariable &  rhs 
)
friend

Return true if lhs is equal to rhs.

Definition at line 105 of file ModelVariable.h.

Field Documentation

◆ mData

Base carl::ModelVariable::mData
private

Definition at line 26 of file ModelVariable.h.

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