#include <ast.hpp>

Public Types
using	allocator_type = Allocator

using	this_type = TFormula<Allocator, ExtendedSig>

using	Sequence = battery::vector<this_type, Allocator>

using	Existential = battery::tuple<LVar<Allocator>, Sort<Allocator>>

using	LogicSet = logic_set<this_type>

using	Formula
	Representation of Booleans.

Public Member Functions
CUDA	TFormula ()

CUDA	TFormula (Formula &&formula)

CUDA	TFormula (AType uid, Formula &&formula)

CUDA	TFormula (const this_type &other)

CUDA	TFormula (this_type &&other)

template<class Alloc2 , class ExtendedSig2 >
CUDA NI	TFormula (const TFormula< Alloc2, ExtendedSig2 > &other, const Allocator &allocator=Allocator())

CUDA void	swap (this_type &other)

CUDA this_type &	operator= (const this_type &rhs)

CUDA this_type &	operator= (this_type &&rhs)

CUDA Formula &	data ()

CUDA const Formula &	data () const

CUDA AType	type () const

CUDA void	type_as (AType ty)

CUDA constexpr bool	is_untyped () const

CUDA NI std::optional< Sort< allocator_type > >	sort () const

CUDA size_t	index () const

CUDA bool	is (size_t kind) const

CUDA bool	is_true () const

CUDA bool	is_false () const

CUDA logic_int	to_z () const

CUDA bool	is_constant () const

CUDA bool	is_variable () const

CUDA bool	is_unary () const

CUDA bool	is_binary () const

CUDA logic_bool	b () const

CUDA logic_int	z () const

CUDA const logic_real &	r () const

CUDA const LogicSet &	s () const

CUDA AVar	v () const

CUDA const LVar< Allocator > &	lv () const

CUDA const Existential &	exists () const

CUDA Sig	sig () const

CUDA NI bool	is_logical () const

CUDA const ExtendedSig &	esig () const

CUDA const Sequence &	seq () const

CUDA const this_type &	seq (size_t i) const

CUDA const Sequence &	eseq () const

CUDA const this_type &	eseq (size_t i) const

CUDA logic_bool &	b ()

CUDA logic_int &	z ()

CUDA logic_real &	r ()

CUDA LogicSet &	s ()

CUDA AVar &	v ()

CUDA Sig &	sig ()

CUDA ExtendedSig &	esig ()

CUDA Sequence &	seq ()

CUDA this_type &	seq (size_t i)

CUDA Sequence &	eseq ()

CUDA this_type &	eseq (size_t i)

CUDA NI this_type	map_sig (Sig sig) const

CUDA NI this_type	map_atype (AType aty) const

template<class Fun >
CUDA NI void	inplace_map (Fun fun)

template<class Fun >
CUDA NI this_type	map (Fun fun)

CUDA void	print (bool print_atype=true) const

Static Public Member Functions
static CUDA this_type	make_true ()

static CUDA this_type	make_false ()

static CUDA this_type	make_bool (logic_bool b, AType atype=UNTYPED)

static CUDA this_type	make_z (logic_int i, AType atype=UNTYPED)

static CUDA this_type	make_real (double lb, double ub, AType atype=UNTYPED)

static CUDA this_type	make_real (logic_real r, AType atype=UNTYPED)

static CUDA this_type	make_set (LogicSet set, AType atype=UNTYPED)

static CUDA this_type	make_avar (AVar v)

static CUDA this_type	make_avar (AType ty, int vid)

static CUDA this_type	make_lvar (AType ty, LVar< Allocator > lvar)

static CUDA this_type	make_exists (AType ty, LVar< Allocator > lvar, Sort< Allocator > ctype)

CUDA static NI this_type	make_nary (Sig sig, Sequence children, AType atype=UNTYPED, bool flatten=true)

static CUDA this_type	make_unary (Sig sig, TFormula child, AType atype=UNTYPED, const Allocator &allocator=Allocator())

static CUDA this_type	make_binary (TFormula lhs, Sig sig, TFormula rhs, AType atype=UNTYPED, const Allocator &allocator=Allocator(), bool flatten=true)

static CUDA this_type	make_nary (ExtendedSig esig, Sequence children, AType atype=UNTYPED)

Static Public Attributes
static constexpr size_t	B = 0

static constexpr size_t	Z = B + 1

static constexpr size_t	R = Z + 1

static constexpr size_t	S = R + 1

static constexpr size_t	V = S + 1

static constexpr size_t	LV = V + 1

static constexpr size_t	E = LV + 1

static constexpr size_t	Seq = E + 1

static constexpr size_t	ESeq = Seq + 1

Friends
template<class Alloc2 , class ExtendedSig2 >
class	TFormula

Detailed Description

template<class Allocator, class ExtendedSig = battery::string<Allocator>>
class lala::TFormula< Allocator, ExtendedSig >

TFormula represents the AST of a typed first-order logical formula. In our context, the type of a formula is an integer representing the UID of an abstract domain in which the formula should to be interpreted. It defaults to the value UNTYPED if the formula is not (yet) typed. By default, the types of integer and real number are supported. The supported symbols can be extended with the template parameter ExtendedSig. This extended signature can also be used for representing exactly constant such as real numbers using a string. The AST of a formula is represented by a variant, where each alternative is described below. We represent everything at the same level (term, formula, predicate, variable, constant). This is generally convenient when modelling to avoid creating intermediate boolean variables when reifying. We can have x + (x > y \/ y > x + 4) >= 1.

Differently from first-order logic, the existential quantifier does not have a subformula, i.e., we write \( \exists{x:Int} \land \exists{y:Int} \land x < y\). This semantics comes from "dynamic predicate logic" where a formula is interpreted in a context (here the abstract element). (The exact connection of our framework to dynamic predicate logic is not yet perfectly clear.)

Member Typedef Documentation

◆ allocator_type

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::allocator_type = Allocator

◆ this_type

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::this_type = TFormula<Allocator, ExtendedSig>

◆ Sequence

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::Sequence = battery::vector<this_type, Allocator>

◆ Existential

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::Existential = battery::tuple<LVar<Allocator>, Sort<Allocator>>

◆ LogicSet

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::LogicSet = logic_set<this_type>

◆ Formula

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

using lala::TFormula< Allocator, ExtendedSig >::Formula

Initial value:

 battery::variant<
    logic_bool,
    logic_int,
    logic_real,
    LogicSet,
    AVar,
    LVar<Allocator>,
    Existential,
    battery::tuple<Sig, Sequence>,
    battery::tuple<ExtendedSig, Sequence>
  >

Representation of Booleans.

Representation of integers. Approximation of real numbers. Set of Booleans, integers, reals or sets. Abstract variable Logical variable Existential quantifier ADD, SUB, ..., EQ, ..., AND, .., NOT see above

Constructor & Destructor Documentation

◆ TFormula() [1/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA lala::TFormula< Allocator, ExtendedSig >::TFormula ( )

inline

By default, we initialize the formula to true.

◆ TFormula() [2/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA lala::TFormula< Allocator, ExtendedSig >::TFormula ( Formula && formula )

inline

◆ TFormula() [3/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA lala::TFormula< Allocator, ExtendedSig >::TFormula	(	AType	uid,
		Formula &&	formula )

inline

◆ TFormula() [4/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA lala::TFormula< Allocator, ExtendedSig >::TFormula ( const this_type & other )

inline

◆ TFormula() [5/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA lala::TFormula< Allocator, ExtendedSig >::TFormula ( this_type && other )

inline

◆ TFormula() [6/6]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

template<class Alloc2 , class ExtendedSig2 >

CUDA NI lala::TFormula< Allocator, ExtendedSig >::TFormula	(	const TFormula< Alloc2, ExtendedSig2 > &	other,
		const Allocator &	allocator = Allocator() )

inline

Member Function Documentation

◆ swap()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA void lala::TFormula< Allocator, ExtendedSig >::swap ( this_type & other )

inline

◆ operator=() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA this_type & lala::TFormula< Allocator, ExtendedSig >::operator= ( const this_type & rhs )

inline

◆ operator=() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA this_type & lala::TFormula< Allocator, ExtendedSig >::operator= ( this_type && rhs )

inline

◆ data() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA Formula & lala::TFormula< Allocator, ExtendedSig >::data ( )

inline

◆ data() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const Formula & lala::TFormula< Allocator, ExtendedSig >::data ( ) const

inline

◆ type()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA AType lala::TFormula< Allocator, ExtendedSig >::type ( ) const

inline

◆ type_as()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA void lala::TFormula< Allocator, ExtendedSig >::type_as ( AType ty )

inline

◆ is_untyped()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA constexpr bool lala::TFormula< Allocator, ExtendedSig >::is_untyped ( ) const

inlineconstexpr

◆ sort()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA NI std::optional< Sort< allocator_type > > lala::TFormula< Allocator, ExtendedSig >::sort ( ) const

inline

◆ make_true()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_true ( )

inlinestatic

◆ make_false()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_false ( )

inlinestatic

◆ make_bool()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_bool	(	logic_bool	b,
		AType	atype = UNTYPED )

inlinestatic

◆ make_z()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_z	(	logic_int	i,
		AType	atype = UNTYPED )

inlinestatic

◆ make_real() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_real	(	double	lb,
		double	ub,
		AType	atype = UNTYPED )

inlinestatic

Create a term representing a real number which is approximated by interval [lb..ub]. By default the real number is supposedly over-approximated.

◆ make_real() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_real	(	logic_real	r,
		AType	atype = UNTYPED )

inlinestatic

◆ make_set()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_set	(	LogicSet	set,
		AType	atype = UNTYPED )

inlinestatic

◆ make_avar() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_avar ( AVar v )

inlinestatic

The type of the formula is embedded in v.

◆ make_avar() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_avar	(	AType	ty,
		int	vid )

inlinestatic

◆ make_lvar()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_lvar	(	AType	ty,
		LVar< Allocator >	lvar )

inlinestatic

◆ make_exists()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_exists	(	AType	ty,
		LVar< Allocator >	lvar,
		Sort< Allocator >	ctype )

inlinestatic

◆ make_nary() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA static NI this_type lala::TFormula< Allocator, ExtendedSig >::make_nary	(	Sig	sig,
		Sequence	children,
		AType	atype = UNTYPED,
		bool	flatten = true )

inlinestatic

If flatten is true it will try to merge the children together to avoid nested formula.

◆ make_unary()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_unary	(	Sig	sig,
		TFormula< Allocator, ExtendedSig >	child,
		AType	atype = UNTYPED,
		const Allocator &	allocator = Allocator() )

inlinestatic

◆ make_binary()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_binary	(	TFormula< Allocator, ExtendedSig >	lhs,
		Sig	sig,
		TFormula< Allocator, ExtendedSig >	rhs,
		AType	atype = UNTYPED,
		const Allocator &	allocator = Allocator(),
		bool	flatten = true )

inlinestatic

◆ make_nary() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

static CUDA this_type lala::TFormula< Allocator, ExtendedSig >::make_nary	(	ExtendedSig	esig,
		Sequence	children,
		AType	atype = UNTYPED )

inlinestatic

◆ index()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA size_t lala::TFormula< Allocator, ExtendedSig >::index ( ) const

inline

◆ is()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is ( size_t kind ) const

inline

◆ is_true()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_true ( ) const

inline

◆ is_false()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_false ( ) const

inline

◆ to_z()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_int lala::TFormula< Allocator, ExtendedSig >::to_z ( ) const

inline

◆ is_constant()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_constant ( ) const

inline

◆ is_variable()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_variable ( ) const

inline

◆ is_unary()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_unary ( ) const

inline

◆ is_binary()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA bool lala::TFormula< Allocator, ExtendedSig >::is_binary ( ) const

inline

◆ b() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_bool lala::TFormula< Allocator, ExtendedSig >::b ( ) const

inline

◆ z() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_int lala::TFormula< Allocator, ExtendedSig >::z ( ) const

inline

◆ r() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const logic_real & lala::TFormula< Allocator, ExtendedSig >::r ( ) const

inline

◆ s() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const LogicSet & lala::TFormula< Allocator, ExtendedSig >::s ( ) const

inline

◆ v() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA AVar lala::TFormula< Allocator, ExtendedSig >::v ( ) const

inline

◆ lv()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const LVar< Allocator > & lala::TFormula< Allocator, ExtendedSig >::lv ( ) const

inline

◆ exists()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const Existential & lala::TFormula< Allocator, ExtendedSig >::exists ( ) const

inline

◆ sig() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA Sig lala::TFormula< Allocator, ExtendedSig >::sig ( ) const

inline

◆ is_logical()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA NI bool lala::TFormula< Allocator, ExtendedSig >::is_logical ( ) const

inline

◆ esig() [1/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const ExtendedSig & lala::TFormula< Allocator, ExtendedSig >::esig ( ) const

inline

◆ seq() [1/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const Sequence & lala::TFormula< Allocator, ExtendedSig >::seq ( ) const

inline

◆ seq() [2/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const this_type & lala::TFormula< Allocator, ExtendedSig >::seq ( size_t i ) const

inline

◆ eseq() [1/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const Sequence & lala::TFormula< Allocator, ExtendedSig >::eseq ( ) const

inline

◆ eseq() [2/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA const this_type & lala::TFormula< Allocator, ExtendedSig >::eseq ( size_t i ) const

inline

◆ b() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_bool & lala::TFormula< Allocator, ExtendedSig >::b ( )

inline

◆ z() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_int & lala::TFormula< Allocator, ExtendedSig >::z ( )

inline

◆ r() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA logic_real & lala::TFormula< Allocator, ExtendedSig >::r ( )

inline

◆ s() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA LogicSet & lala::TFormula< Allocator, ExtendedSig >::s ( )

inline

◆ v() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA AVar & lala::TFormula< Allocator, ExtendedSig >::v ( )

inline

◆ sig() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA Sig & lala::TFormula< Allocator, ExtendedSig >::sig ( )

inline

◆ esig() [2/2]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA ExtendedSig & lala::TFormula< Allocator, ExtendedSig >::esig ( )

inline

◆ seq() [3/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA Sequence & lala::TFormula< Allocator, ExtendedSig >::seq ( )

inline

◆ seq() [4/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA this_type & lala::TFormula< Allocator, ExtendedSig >::seq ( size_t i )

inline

◆ eseq() [3/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA Sequence & lala::TFormula< Allocator, ExtendedSig >::eseq ( )

inline

◆ eseq() [4/4]

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA this_type & lala::TFormula< Allocator, ExtendedSig >::eseq ( size_t i )

inline

◆ map_sig()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA NI this_type lala::TFormula< Allocator, ExtendedSig >::map_sig ( Sig sig ) const

inline

◆ map_atype()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA NI this_type lala::TFormula< Allocator, ExtendedSig >::map_atype ( AType aty ) const

inline

◆ inplace_map()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

template<class Fun >

CUDA NI void lala::TFormula< Allocator, ExtendedSig >::inplace_map ( Fun fun )

inline

In-place map of each leaf of the formula to a new leaf according to fun.

◆ map()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

template<class Fun >

CUDA NI this_type lala::TFormula< Allocator, ExtendedSig >::map ( Fun fun )

inline

Map of each leaf of the formula to a new leaf according to fun.

◆ print()

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

CUDA void lala::TFormula< Allocator, ExtendedSig >::print ( bool print_atype = true ) const

inline

Friends And Related Symbol Documentation

◆ TFormula

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

template<class Alloc2 , class ExtendedSig2 >

friend class TFormula

friend

Member Data Documentation

◆ B

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::B = 0

staticconstexpr

Index of Booleans in the variant type Formula (called kind below).

◆ Z

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::Z = B + 1

staticconstexpr

Index of integers in the variant type Formula (called kind below).

◆ R

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::R = Z + 1

staticconstexpr

Index of real numbers in the variant type Formula (called kind below).

◆ S

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::S = R + 1

staticconstexpr

Index of sets in the variant type Formula (called kind below).

◆ V

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::V = S + 1

staticconstexpr

Index of abstract variables in the variant type Formula (called kind below).

◆ LV

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::LV = V + 1

staticconstexpr

Index of logical variables in the variant type Formula (called kind below).

◆ E

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::E = LV + 1

staticconstexpr

Index of existential quantifier in the variant type Formula (called kind below).

◆ Seq

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::Seq = E + 1

staticconstexpr

Index of n-ary operators in the variant type Formula (called kind below).

◆ ESeq

template<class Allocator , class ExtendedSig = battery::string<Allocator>>

size_t lala::TFormula< Allocator, ExtendedSig >::ESeq = Seq + 1

staticconstexpr

Index of n-ary operators where the operator is an extended signature in the variant type Formula (called kind below).

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

include/lala/logic/ast.hpp

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ allocator_type

◆ this_type

◆ Sequence

◆ Existential

◆ LogicSet

◆ Formula

Constructor & Destructor Documentation

◆ TFormula() [1/6]

◆ TFormula() [2/6]

◆ TFormula() [3/6]

◆ TFormula() [4/6]

◆ TFormula() [5/6]

◆ TFormula() [6/6]

Member Function Documentation

◆ swap()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ data() [1/2]

◆ data() [2/2]

◆ type()

◆ type_as()

◆ is_untyped()

◆ sort()

◆ make_true()

◆ make_false()

◆ make_bool()

◆ make_z()

◆ make_real() [1/2]

◆ make_real() [2/2]

◆ make_set()

◆ make_avar() [1/2]

◆ make_avar() [2/2]

◆ make_lvar()

◆ make_exists()

◆ make_nary() [1/2]

◆ make_unary()

◆ make_binary()

◆ make_nary() [2/2]

◆ index()

◆ is()

◆ is_true()

◆ is_false()

◆ to_z()

◆ is_constant()

◆ is_variable()

◆ is_unary()

◆ is_binary()

◆ b() [1/2]

◆ z() [1/2]

◆ r() [1/2]

◆ s() [1/2]

◆ v() [1/2]

◆ lv()

◆ exists()

◆ sig() [1/2]

◆ is_logical()

◆ esig() [1/2]

◆ seq() [1/4]

◆ seq() [2/4]

◆ eseq() [1/4]

◆ eseq() [2/4]

◆ b() [2/2]

◆ z() [2/2]

◆ r() [2/2]

◆ s() [2/2]

◆ v() [2/2]

◆ sig() [2/2]

◆ esig() [2/2]

◆ seq() [3/4]

◆ seq() [4/4]

◆ eseq() [3/4]

◆ eseq() [4/4]

◆ map_sig()