#include <formula.hpp>

Public Types
using	A = AD

using	allocator_type = Allocator

using	this_type = Formula<A, allocator_type>

using	U = typename A::local_universe

using	term_type = Term<A, allocator_type>

using	this_ptr = battery::unique_ptr<this_type, allocator_type>

using	PVarLit = VariableLiteral<A, false>

using	NVarLit = VariableLiteral<A, true>

using	Leq = InequalityLEQ<A, allocator_type>

using	Gt = InequalityGT<A, allocator_type>

using	Eq = Equality<A, allocator_type>

using	Neq = Disequality<A, allocator_type>

using	Conj = Conjunction<A, allocator_type>

using	Disj = Disjunction<A, allocator_type>

using	Bicond = Biconditional<A, allocator_type>

using	Imply = Implication<A, allocator_type>

using	Xor = ExclusiveDisjunction<A, allocator_type>

using	AE = AbstractElement<A, allocator_type>

using	tell_type = typename A::template tell_type<allocator_type>

using	ask_type = typename A::template ask_type<allocator_type>

Public Member Functions
	Formula ()=default

	Formula (this_type &&)=default

this_type &	operator= (this_type &&)=default

template<class A2 , class Alloc2 >
CUDA	Formula (const Formula< A2, Alloc2 > &other, const Allocator &allocator=Allocator())

CUDA bool	is (size_t kind) const

CUDA size_t	kind () const

CUDA bool	embed (A &a, const U &u) const

CUDA void	project (const A &a, U &r) const

CUDA void	print (const A &a) const

template<class Env , class Allocator2 = typename Env::allocator_type>
CUDA TFormula< Allocator2 >	deinterpret (const A &a, const Env &env, AType apc, Allocator2 allocator=Allocator2()) const

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 size_t	length () const

Static Public Member Functions
template<size_t I, class SubFormula >
static CUDA this_type	make (SubFormula &&sub_formula)

static CUDA this_type	make_pvarlit (const AVar &avar)

static CUDA this_type	make_nvarlit (const AVar &avar)

static CUDA this_type	make_true ()

static CUDA this_type	make_false ()

static CUDA this_type	make_leq (term_type &&left, term_type &&right)

static CUDA this_type	make_gt (term_type &&left, term_type &&right)

static CUDA this_type	make_eq (term_type &&left, term_type &&right)

static CUDA this_type	make_neq (term_type &&left, term_type &&right)

static CUDA this_type	make_conj (this_ptr &&left, this_ptr &&right)

static CUDA this_type	make_disj (this_ptr &&left, this_ptr &&right)

static CUDA this_type	make_bicond (this_ptr &&left, this_ptr &&right)

static CUDA this_type	make_imply (this_ptr &&left, this_ptr &&right)

static CUDA this_type	make_xor (this_ptr &&left, this_ptr &&right)

static CUDA this_type	make_abstract_element (tell_type &&tellv, tell_type &&not_tellv, ask_type &&askv, ask_type &&not_askv)

Static Public Attributes
static constexpr size_t	IPVarLit = 0

static constexpr size_t	INVarLit = IPVarLit + 1

static constexpr size_t	ITrue = INVarLit + 1

static constexpr size_t	IFalse = ITrue + 1

static constexpr size_t	ILeq = IFalse + 1

static constexpr size_t	IGt = ILeq + 1

static constexpr size_t	IEq = IGt + 1

static constexpr size_t	INeq = IEq + 1

static constexpr size_t	IConj = INeq + 1

static constexpr size_t	IDisj = IConj + 1

static constexpr size_t	IBicond = IDisj + 1

static constexpr size_t	IImply = IBicond + 1

static constexpr size_t	IXor = IImply + 1

static constexpr size_t	IAE = IXor + 1

Friends
template<class A2 , class Alloc2 >
class	Formula

Detailed Description

template<class AD, class Allocator>
class lala::pc::Formula< AD, Allocator >

A formula can occur in a term, e.g., (x = 2) + (y = 2) + (z = 2) >= 2 In that case, the entailment of the formula is mapped onto a sublattice of U supporting initialization from 0 and 1. A term can occur in a formula, as it is usually done. Therefore, a formula is both a formula and a term.

A logical formula is turned into a term by mapping their satisfiability to and from a sublattice of U representing Boolean values:

Consists of four distinct values \(\{[\![x = 0]\!]_U \sqcap [\![x = 1]\!]_U, [\![x = 0]\!]_U, [\![x = 1]\!]_U, \top_U \}\).
With \(\{[\![x = 0]\!]_U \sqcap [\![x = 1]\!]_U \) meaning neither true or false yet (e.g., unknown), \(\{[\![x = 0]\!]_U \) modelling falsity, \( [\![x = 1]\!]_U \) modelling truth, and \( \top_U \) a logical statement both true and false (i.e., one of the variable is top).