Module razor_fol::syntax

Defines an abstract syntax tree (AST) for first-order terms and formulae with equality.

Structs

C	Represents a constant symbol with a given name.
F	Represents an uninterpreted function symbol with a given name.
Pred	Represents a predicate symbol with a given name.
Theory	Is a first-order theory, containing a set of first-order formulae.
V	Represents a variable symbol with a given name.

Enums

Formula	Is an abstract syntax tree (AST) for first-order formulae.
Term	Represents a first-order term and consists of variables, constants and function applications.

Traits

FApp	Is the trait for types that can be passed to a function of type F as arguments.

Functions

exists	Returns an existentially quantified formula with the given variables and formula.
exists1	Returns an existentially quantified formula on one variable.
exists2	Returns an existentially quantified formula on two variables.
exists3	Returns an existentially quantified formula on three variables.
exists4	Returns an existentially quantified formula on four variables.
exists5	Returns an existentially quantified formula on five variables.
forall	Returns a universally quantified formula with the given variables and formula.
forall1	Returns a universally quantified formula on one variable.
forall2	Returns a universally quantified formula on two variables.
forall3	Returns a universally quantified formula on three variables.
forall4	Returns a universally quantified formula on four variables.
forall5	Returns a universally quantified formula on five variables.
not	Returns the negation of formula.