		Search-engine friendly clone of the ACL2 documentation.

Pfcs

Abstract-syntax

Abstract syntax of PFCSes.

Expressions are built out of constants, variables, and field operations. A basic constraint is an equality between expressions. Constraints may be (conjunctively) grouped into named relations (see definition), which may be conjoined with equality constraints. A system of constraints is a collection of named relations, which are hierarchically organized, and of constraints that may reference the relations.

The abstract syntax is derived from the ABNF grammar in a straightforward way.

Subtopics

Syntax-abstraction: Mapping from concrete to abstract syntax, for PFCS.
Expression: Fixtype of expressions.
Definition: Fixtype of definitions of relations.
Constraint: Fixtype of constraints.
Definition-option: Fixtype of optional definitions of relations.
Abstract-syntax-operations: Operations on the abstract syntax of PFCSes.
System: Fixtype of systems of constraints.
Convenience-constructors: Utilities to convniently construct PFCS abstract syntax.
System-result: Fixtype of errors and PFCS systems.
Expression-result: Fixtype of errors and PFCS expressions.
Expression-list-result: Fixtype of errors and lists of PFCS expressions.
Definition-result: Fixtype of errors and PFCS definitions.
Definition-list-result: Fixtype of errors and lists of PFCS definitions.
Constraint-result: Fixtype of errors and PFCS constraints.
Constraint-list-result: Fixtype of errors and lists of PFCS constraints.
Expression-list: Fixtype of lists of expressions.
Definition-list: Fixtype of lists of definitions of relations.
Constraint-list: Fixtype of lists of constraints.