Abbreviations (Averest)

Abbreviations Module

Namespace: Averest.Core
Assembly: Averest.dll

Implements a hash table to abbreviate boolean expressions by new variables so that common sub-expressions can be shared.

Types

Type	Description
Abbrev	An abbreviation is a pair that describes a mapping from a QName to a Boolean expression. Since this mapping is partial (some names may not be bound), the second component is a BoolExpr option.
AbbrevTable	An abbreviation table essentially consists of a map from boolean expressions to QNames. This mapping is viewed as abbreviation of the expression by a new boolean variable whose name is the QName. In contrast to the forward variant, new abbreviations can be created. To this end, the table has to generate new names which is done by storing in integer which is also the maximum number of boolean expressions abbreviated in the table.

Functions and values

Function or value	Description
`AbbrevBoolExpr abrTab boolExpr` Full Usage: `AbbrevBoolExpr abrTab boolExpr` Parameters: abrTab : `AbbrevTable` boolExpr : `BoolExpr` Returns: `BoolExpr`	Inserts a boolean expression in the table. The behavior is similar to StrongAbbrevBoolExpr, except variables, negations and boolean constants and variables phi. They are simply returned without creating a new abbreviation in the table. abrTab : `AbbrevTable` boolExpr : `BoolExpr` Returns: `BoolExpr`
`AbbrevConj abbrevs (t1, t2)` Full Usage: `AbbrevConj abbrevs (t1, t2)` Parameters: abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean conjunction of t1 and t2 with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`AbbrevDisj abbrevs (t1, t2)` Full Usage: `AbbrevDisj abbrevs (t1, t2)` Parameters: abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean disjunction of t1 and t2 with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`AbbrevEqu abbrevs (t1, t2)` Full Usage: `AbbrevEqu abbrevs (t1, t2)` Parameters: abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean equivalence of t1 and t2 with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`AbbrevImpl abbrevs (t1, t2)` Full Usage: `AbbrevImpl abbrevs (t1, t2)` Parameters: abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean implication of t1 and t2 with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`AbbrevIte abbrevs (t1, t2, t3)` Full Usage: `AbbrevIte abbrevs (t1, t2, t3)` Parameters: abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` t3 : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean if-then-else with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t1 : `BoolExpr` t2 : `BoolExpr` t3 : `BoolExpr` Returns: `BoolExpr`
`AbbrevNeg abbrevs t` Full Usage: `AbbrevNeg abbrevs t` Parameters: abbrevs : `AbbrevTable` t : `BoolExpr` Returns: `BoolExpr`	Creates an expression that represents the boolean negation of t with its subterms abbreviated in the abbreviation table. abbrevs : `AbbrevTable` t : `BoolExpr` Returns: `BoolExpr`
`AbbrevUnbound abbrevs` Full Usage: `AbbrevUnbound abbrevs` Parameters: abbrevs : `AbbrevTable` Returns: `QName`	Generates a new qname that is not abbreviated so far in the referenced abbreviation table. abbrevs : `AbbrevTable` Returns: `QName`
`AbbrevsToList abbrevs` Full Usage: `AbbrevsToList abbrevs` Parameters: abbrevs : `(BoolExpr * Action) list` Returns: `(QName * Expr) list`	abbrevs : `(BoolExpr * Action) list` Returns: `(QName * Expr) list`
`AbbrevsToSubst initialRho abbrevs` Full Usage: `AbbrevsToSubst initialRho abbrevs` Parameters: initialRho : `Map<QName, Expr>` abbrevs : `(BoolExpr * Action) list` Returns: `Map<QName, Expr>`	initialRho : `Map<QName, Expr>` abbrevs : `(BoolExpr * Action) list` Returns: `Map<QName, Expr>`
`NewAbbrevTable name` Full Usage: `NewAbbrevTable name` Parameters: name : `string` Returns: `AbbrevTable`	Generates a new abbreviation table where the names of the variables used for the abbreviations start with two underscores and s. Note that the abbreviation tables must have different name stubs s. name : `string` Returns: `AbbrevTable`
`PrnAbbrev (arg1, arg2)` Full Usage: `PrnAbbrev (arg1, arg2)` Parameters: arg0 : `BoolExpr option` arg1 : `QName` Returns: `PrnDrv -> unit`	printer of abbreviation abr arg0 : `BoolExpr option` arg1 : `QName` Returns: `PrnDrv -> unit`
`PrnAbbrevTable abbrevs` Full Usage: `PrnAbbrevTable abbrevs` Parameters: abbrevs : `AbbrevTable` Returns: `PrnDrv -> unit`	Printer function for an abbreviation table abbrevs : `AbbrevTable` Returns: `PrnDrv -> unit`
`QNameOfExpr abbrevs t` Full Usage: `QNameOfExpr abbrevs t` Parameters: abbrevs : `AbbrevTable` t : `BoolExpr` Returns: `QName`	Returns the qname associated with dfn in table given by abrTab If not found there, the parent table will be consulted. An InternalException will be raised if no entry is bound to dfn in any table. abbrevs : `AbbrevTable` t : `BoolExpr` Returns: `QName`
`StrongAbbrevBoolExpr abrTab boolExpr` Full Usage: `StrongAbbrevBoolExpr abrTab boolExpr` Parameters: abrTab : `AbbrevTable` boolExpr : `BoolExpr` Returns: `BoolExpr`	Inserts a boolean expression in the table. If the expression is already associated with a qname, return that qname, otherwise generate a new qname and associate it with the expression. abrTab : `AbbrevTable` boolExpr : `BoolExpr` Returns: `BoolExpr`