carl  24.04
Computer ARithmetic Library
Public Types | Public Member Functions | Private Attributes
carl::VariableComparison< Poly > Class Template Reference

Represent a sum type/variant of an (in)equality between a variable on the left-hand side and multivariateRoot or algebraic real on the right-hand side. More...

#include <VariableComparison.h>

Collaboration diagram for carl::VariableComparison< Poly >:
Collaboration graph
[legend]

Public Types

using Number = typename UnderlyingNumberType< Poly >::type
 
using MR = MultivariateRoot< Poly >
 
using RAN = typename MultivariateRoot< Poly >::RAN
 

Public Member Functions

 VariableComparison (Variable v, const std::variant< MR, RAN > &value, Relation rel, bool neg)
 
 VariableComparison (Variable v, const MR &value, Relation rel)
 
 VariableComparison (Variable v, const RAN &value, Relation rel)
 
Variable var () const
 
Relation relation () const
 
bool negated () const
 
const std::variant< MR, RAN > & value () const
 
std::variant< MR, RAN > & value ()
 
bool is_equality () const
 
VariableComparison negation () const
 
VariableComparison invert_relation () const
 
VariableComparison resolve_negation () const
 

Private Attributes

Variable m_var
 
std::variant< MR, RAN > m_value
 
Relation m_relation
 
bool m_negated
 

Detailed Description

template<typename Poly>
class carl::VariableComparison< Poly >

Represent a sum type/variant of an (in)equality between a variable on the left-hand side and multivariateRoot or algebraic real on the right-hand side.

This is basically a special purpose atomic SMT formula. The lhs-variable must does not appear on the rhs.

Definition at line 28 of file VariableComparison.h.

Member Typedef Documentation

◆ MR

template<typename Poly >
using carl::VariableComparison< Poly >::MR = MultivariateRoot<Poly>

Definition at line 31 of file VariableComparison.h.

◆ Number

template<typename Poly >
using carl::VariableComparison< Poly >::Number = typename UnderlyingNumberType<Poly>::type

Definition at line 30 of file VariableComparison.h.

◆ RAN

template<typename Poly >
using carl::VariableComparison< Poly >::RAN = typename MultivariateRoot<Poly>::RAN

Definition at line 32 of file VariableComparison.h.

Constructor & Destructor Documentation

◆ VariableComparison() [1/3]

template<typename Poly >
carl::VariableComparison< Poly >::VariableComparison ( Variable  v,
const std::variant< MR, RAN > &  value,
Relation  rel,
bool  neg 
)
inline

Definition at line 39 of file VariableComparison.h.

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

◆ VariableComparison() [2/3]

template<typename Poly >
carl::VariableComparison< Poly >::VariableComparison ( Variable  v,
const MR &  value,
Relation  rel 
)
inline

Definition at line 43 of file VariableComparison.h.

Here is the call graph for this function:

◆ VariableComparison() [3/3]

template<typename Poly >
carl::VariableComparison< Poly >::VariableComparison ( Variable  v,
const RAN &  value,
Relation  rel 
)
inline

Definition at line 57 of file VariableComparison.h.

Member Function Documentation

◆ invert_relation()

template<typename Poly >
VariableComparison carl::VariableComparison< Poly >::invert_relation ( ) const
inline

Definition at line 83 of file VariableComparison.h.

Here is the call graph for this function:

◆ is_equality()

template<typename Poly >
bool carl::VariableComparison< Poly >::is_equality ( ) const
inline

Definition at line 76 of file VariableComparison.h.

Here is the call graph for this function:

◆ negated()

template<typename Poly >
bool carl::VariableComparison< Poly >::negated ( ) const
inline

Definition at line 67 of file VariableComparison.h.

Here is the caller graph for this function:

◆ negation()

template<typename Poly >
VariableComparison carl::VariableComparison< Poly >::negation ( ) const
inline

Definition at line 80 of file VariableComparison.h.

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

◆ relation()

template<typename Poly >
Relation carl::VariableComparison< Poly >::relation ( ) const
inline

Definition at line 64 of file VariableComparison.h.

Here is the caller graph for this function:

◆ resolve_negation()

template<typename Poly >
VariableComparison carl::VariableComparison< Poly >::resolve_negation ( ) const
inline

Definition at line 86 of file VariableComparison.h.

Here is the call graph for this function:

◆ value() [1/2]

template<typename Poly >
std::variant<MR, RAN>& carl::VariableComparison< Poly >::value ( )
inline

Definition at line 73 of file VariableComparison.h.

◆ value() [2/2]

template<typename Poly >
const std::variant<MR, RAN>& carl::VariableComparison< Poly >::value ( ) const
inline

Definition at line 70 of file VariableComparison.h.

Here is the caller graph for this function:

◆ var()

template<typename Poly >
Variable carl::VariableComparison< Poly >::var ( ) const
inline

Definition at line 61 of file VariableComparison.h.

Here is the caller graph for this function:

Field Documentation

◆ m_negated

template<typename Poly >
bool carl::VariableComparison< Poly >::m_negated
private

Definition at line 37 of file VariableComparison.h.

◆ m_relation

template<typename Poly >
Relation carl::VariableComparison< Poly >::m_relation
private

Definition at line 36 of file VariableComparison.h.

◆ m_value

template<typename Poly >
std::variant<MR, RAN> carl::VariableComparison< Poly >::m_value
private

Definition at line 35 of file VariableComparison.h.

◆ m_var

template<typename Poly >
Variable carl::VariableComparison< Poly >::m_var
private

Definition at line 34 of file VariableComparison.h.

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