lala::pc::VariableLiteral< AD, neg > Class Template Reference

#include <formula.hpp>

Public Types
using	A = AD
using	U = typename A::local_universe

Public Member Functions
	VariableLiteral ()=default
CUDA	VariableLiteral (AVar avar)
template<class A2 , class Alloc >
CUDA	VariableLiteral (const VariableLiteral< A2, neg > &other, const Alloc &)
CUDA local::B	ask (const A &a) const
CUDA local::B	nask (const A &a) const
CUDA bool	deduce (A &a) const
CUDA bool	contradeduce (A &a) const
CUDA NI void	print (const A &a) const
template<class Env , class Allocator = typename Env::allocator_type>
CUDA NI TFormula< Allocator >	deinterpret (const A &, const Env &env, AType apc, Allocator allocator=Allocator()) const
CUDA size_t	length () const

Friends
template<class A2 , bool neg2>
class	VariableLiteral

Detailed Description

template<class AD, bool neg>
class lala::pc::VariableLiteral< AD, neg >

A Boolean variable defined on a universe of discourse supporting 0 for false and 1 for true.

Member Typedef Documentation

A

template<class AD , bool neg>

using lala::pc::VariableLiteral< AD, neg >::A = AD

U

template<class AD , bool neg>

using lala::pc::VariableLiteral< AD, neg >::U = typename A::local_universe

Constructor & Destructor Documentation

VariableLiteral() [1/3]

template<class AD , bool neg>

lala::pc::VariableLiteral< AD, neg >::VariableLiteral ( )

default

VariableLiteral() [2/3]

template<class AD , bool neg>

CUDA lala::pc::VariableLiteral< AD, neg >::VariableLiteral ( AVar  avar )

inline

VariableLiteral() [3/3]

template<class AD , bool neg>

template<class A2 , class Alloc >

CUDA lala::pc::VariableLiteral< AD, neg >::VariableLiteral ( const VariableLiteral< A2, neg > &  other, const Alloc &    )

inline

Member Function Documentation

ask()

template<class AD , bool neg>

CUDA local::B lala::pc::VariableLiteral< AD, neg >::ask ( const A &  a ) const

inline

Given a variable x taking a value in a universe U denoted by \( a(x) \).

• \( a \vDash x \) holds iff \( \lnot (a(x) \leq [\![x = 0]\!]_U) \).
• \( a \vDash \lnot{x} \) holds iff \( a(x) \geq [\![x = 0]\!]_U \).

nask()

template<class AD , bool neg>

CUDA local::B lala::pc::VariableLiteral< AD, neg >::nask ( const A &  a ) const

inline

Given a variable x taking a value in a universe U denoted by \( a(x) \).

• \( a \nvDash x \) holds iff \( a(x) \geq [\![x = 0]\!]_U \).
• \( a \nvDash \lnot{x} \) holds iff \( \lnot (a(x) \leq [\![x = 0]\!]_U) \).

deduce()

template<class AD , bool neg>

CUDA bool lala::pc::VariableLiteral< AD, neg >::deduce ( A &  a ) const

inline

Perform:

• Positive literal: \( x = a(x) \sqcup [\![x = 1]\!]_U \)
• Negative literal: \( x = a(x) \sqcup [\![x = 0]\!]_U \).

contradeduce()

template<class AD , bool neg>

CUDA bool lala::pc::VariableLiteral< AD, neg >::contradeduce ( A &  a ) const

inline

Perform:

• Positive literal: \( x = a(x) \sqcup [\![x = 0]\!]_U \)
• Negative literal: \( x = a(x) \sqcup [\![x = 1]\!]_U \).

print()

template<class AD , bool neg>

CUDA NI void lala::pc::VariableLiteral< AD, neg >::print ( const A &  a ) const

inline

deinterpret()

template<class AD , bool neg>

template<class Env , class Allocator = typename Env::allocator_type>

CUDA NI TFormula< Allocator > lala::pc::VariableLiteral< AD, neg >::deinterpret ( const A &  , const Env &  env, AType  apc, Allocator  allocator = Allocator()  ) const

inline

length()

template<class AD , bool neg>

CUDA size_t lala::pc::VariableLiteral< AD, neg >::length ( ) const

inline

Friends And Related Symbol Documentation

VariableLiteral

template<class AD , bool neg>

template<class A2 , bool neg2>

friend class VariableLiteral

friend

---

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

• include/lala/formula.hpp