Defining terms and formulas of first-order logic

Functions
EXPR	efun (FUNSYM fun, const EXPR *args)
	Variables and applied functions and predicates. More...
EXPR	etrue ()
	The true expression. More...
EXPR	efalse ()
	The false expression. More...
EXPR	enot (EXPR a)
	Negation. More...
EXPR	eand (size_t nb, const EXPR *a)
	N-ary conjunction. More...
EXPR	eor (size_t nb, const EXPR *a)
	N-ary disjunction. More...
EXPR	exor (EXPR a, EXPR b)
	Xor. More...
EXPR	eimp (EXPR a, EXPR b)
	Implication. More...
EXPR	eeq (EXPR a, EXPR b)
	Equality. More...
EXPR	edistinct (size_t nb, const EXPR *d)
	Distinct. More...
EXPR	eint (int i)
	Integer constants. More...
EXPR	eadd (EXPR a, EXPR b)
	Addition. More...
EXPR	eopp (EXPR a)
	Unary minus. More...
EXPR	eminus (EXPR a, EXPR b)
	Binary subtraction. More...
EXPR	emult (EXPR a, EXPR b)
	Binary multiplication. More...
EXPR	elt (EXPR a, EXPR b)
	Less than. More...
EXPR	ele (EXPR a, EXPR b)
	Less or equal. More...
EXPR	egt (EXPR a, EXPR b)
	Greater than. More...
EXPR	ege (EXPR a, EXPR b)
	Greater or equal. More...

Detailed Description

Defining terms and formulas of first-order logic.

Function Documentation

eadd()

EXPR eadd	(	EXPR	a,
		EXPR	b
	)

Addition.

This function creates the addition of the two integer expressions a and b.

Parameters

a	The left-hand side operand of the addition.
b	The right-hand side operand of the addition.

Returns

The corresponding expression.

eand()

EXPR eand	(	size_t	nb,
		const EXPR *	a
	)

N-ary conjunction.

This function creates the conjunction of the nb Boolean expressions in a.

Parameters

nb	The number of expressions.
a	A pointer to the list of expressions.

Returns

The corresponding expression.

edistinct()

EXPR edistinct	(	size_t	nb,
		const EXPR *	d
	)

Distinct.

This function expresses the fact that all the elements in d are pairwise distinct.

Parameters

nb	The number of expressions.
d	A pointer to the list of expressions.

Returns

The corresponding expression.

eeq()

EXPR eeq	(	EXPR	a,
		EXPR	b
	)

Equality.

This function creates the implication of the two expressions (of any type) a and b.

Parameters

a	The left-hand side formula of the equality.
b	The right-hand side formula of the equality.

Returns

The corresponding expression.

efalse()

EXPR efalse

(

)

The false expression.

This function create the false Boolean expression.

Returns

The corresponding expression.

efun()

EXPR efun	(	FUNSYM	fun,
		const EXPR *	args
	)

Variables and applied functions and predicates.

This function applies an uninterpreted function or predicate symbol to 0 or more arguments.

Parameters

fun	The function or predicate symbol
args	The (possibly empty) pointer to the list of arguments. It should be of the same length as the arity of the function or predicate symbol.

Returns

The corresponding expression.

ege()

EXPR ege	(	EXPR	a,
		EXPR	b
	)

Greater or equal.

This function creates the comparison that the integer expressions a is greater or equal than the integer expression b.

Parameters

a	The left-hand side operand of greater or equal.
b	The right-hand side operand of greater or equal.

Returns

The corresponding expression.

egt()

EXPR egt	(	EXPR	a,
		EXPR	b
	)

Greater than.

This function creates the comparison that the integer expressions a is stricly greater than the integer expression b.

Parameters

a	The left-hand side operand of greater than.
b	The right-hand side operand of greater than.

Returns

The corresponding expression.

eimp()

EXPR eimp	(	EXPR	a,
		EXPR	b
	)

Implication.

This function creates the implication of the two Boolean expressions a and b.

Parameters

a	The left-hand side formula of the implication.
b	The right-hand side formula of the implication.

Returns

The corresponding expression.

eint()

EXPR eint

(

int

i

)

Integer constants.

This function injects an integer constant into expressions.

Parameters

i	The constant.

Returns

The corresponding expression.

ele()

EXPR ele	(	EXPR	a,
		EXPR	b
	)

Less or equal.

This function creates the comparison that the integer expressions a is smaller or equal than the integer expression b.

Parameters

a	The left-hand side operand of less or equal.
b	The right-hand side operand of less or equal.

Returns

The corresponding expression.

elt()

EXPR elt	(	EXPR	a,
		EXPR	b
	)

Less than.

This function creates the comparison that the integer expressions a is stricly smaller than the integer expression b.

Parameters

a	The left-hand side operand of less than.
b	The right-hand side operand of less than.

Returns

The corresponding expression.

eminus()

EXPR eminus	(	EXPR	a,
		EXPR	b
	)

Binary subtraction.

This function creates the subtraction of the two integer expressions a and b.

Parameters

a	The left-hand side operand of the subtraction.
b	The right-hand side operand of the subtraction.

Returns

The corresponding expression.

emult()

EXPR emult	(	EXPR	a,
		EXPR	b
	)

Binary multiplication.

This function creates the multiplication of the two integer expressions a and b.

Parameters

a	The left-hand side operand of the multiplication.
b	The right-hand side operand of the multiplication.

Returns

The corresponding expression.

enot()

EXPR enot

(

EXPR

a

)

Negation.

This function negates the Boolean expression a.

Parameters

a	The expression to negate

Returns

The corresponding expression.

eopp()

EXPR eopp

(

EXPR

a

)

Unary minus.

This function creates the opposite of the integer expression a.

Parameters

a	The expression that we take the opposite of.

Returns

The corresponding expression.

eor()

EXPR eor	(	size_t	nb,
		const EXPR *	a
	)

N-ary disjunction.

This function creates the disjunction of the nb Boolean expressions in a.

Parameters

nb	The number of expressions.
a	A pointer to the list of expressions.

Returns

The corresponding expression.

etrue()

EXPR etrue

(

)

The true expression.

This function create the true Boolean expression.

Returns

The corresponding expression.

exor()

EXPR exor	(	EXPR	a,
		EXPR	b
	)

Xor.

This function creates the exclusive or of the two Boolean expressions a and b.

Parameters

a	The left-hand side formula of the exclusive or.
b	The right-hand side formula of the exclusive or.

Returns

The corresponding expression.