Expressions (Averest)

Expressions Module

Namespace: Averest.Core
Assembly: Averest.dll

This module implements the data type of Quartz expressions together with many functions. Expressions are split into expressions having different Quartz types as well as left-hand side expressions LhsExpr that may have any type, but whose operators are restricted to those that can appear on left-hand sides of assignments. Certain operators like *Var,*Ite,*Case,*ArrAcc, and *TupAcc are defined for all types and these generate variables, if-then-else expressions, case expressions, array element access, and tuple access. The other operators should be rather self-explaining (see Module StaticEvaluation for further explanation of these operations and note that boolean lists are usually bitvector constants, radix-2 numbers or 2-complement numbers).

Types

Type	Description
ArrExpr
BoolExpr
BtvExpr
Expr
IntExpr
LhsExpr
NatExpr
RealExpr
Substitution	type abbreviation for substitutions
TupExpr

Functions and values

Function or value	Description
`AtomsOfBoolExpr eL` Full Usage: `AtomsOfBoolExpr eL` Parameters: eL : `BoolExpr list` Returns: `Set<BoolExpr>`	Computes the set of atoms of a list of BoolExpr. This is required for a boolean abstraction as used by BDDs and SAT solvers like ShannonGraphs. eL : `BoolExpr list` Returns: `Set<BoolExpr>`
`CellsOfDecl (xn, decl)` Full Usage: `CellsOfDecl (xn, decl)` Parameters: xn : `QName` decl : `Decl` Returns: `LhsExpr list`	compute the cells of a declaration xn : `QName` decl : `Decl` Returns: `LhsExpr list`
`CellsOfExpr e` Full Usage: `CellsOfExpr e` Parameters: e : `Expr` Returns: `Set<LhsExpr>`	e : `Expr` Returns: `Set<LhsExpr>`
`CellsOfInterface iface` Full Usage: `CellsOfInterface iface` Parameters: iface : `(QName * Decl) list` Returns: `LhsExpr list`	compute the cells of an interface iface : `(QName * Decl) list` Returns: `LhsExpr list`
`DefaultVal qtype` Full Usage: `DefaultVal qtype` Parameters: qtype : `QType` Returns: `Expr`	returns a default value (e.g. used as initial value in Quartz) for a given type; for Qarr types, the default value of the base type is returned. qtype : `QType` Returns: `Expr`
`EnumLhsOfName xn qty` Full Usage: `EnumLhsOfName xn qty` Parameters: xn : `QName` qty : `QType` Returns: `(LhsExpr * QType) list`	xn : `QName` qty : `QType` Returns: `(LhsExpr * QType) list`
`FVarsArrExpr expr` Full Usage: `FVarsArrExpr expr` Parameters: expr : `ArrExpr` Returns: `Set<QName * QType>`	expr : `ArrExpr` Returns: `Set<QName * QType>`
`FVarsBoolExpr expr` Full Usage: `FVarsBoolExpr expr` Parameters: expr : `BoolExpr` Returns: `Set<QName * QType>`	expr : `BoolExpr` Returns: `Set<QName * QType>`
`FVarsBtvExpr expr` Full Usage: `FVarsBtvExpr expr` Parameters: expr : `BtvExpr` Returns: `Set<QName * QType>`	expr : `BtvExpr` Returns: `Set<QName * QType>`
`FVarsExpr expr` Full Usage: `FVarsExpr expr` Parameters: expr : `Expr` Returns: `Set<QName * QType>`	expr : `Expr` Returns: `Set<QName * QType>`
`FVarsIntExpr expr` Full Usage: `FVarsIntExpr expr` Parameters: expr : `IntExpr` Returns: `Set<QName * QType>`	expr : `IntExpr` Returns: `Set<QName * QType>`
`FVarsLhsExpr lhsExpr` Full Usage: `FVarsLhsExpr lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `Set<QName * QType>`	lhsExpr : `LhsExpr` Returns: `Set<QName * QType>`
`FVarsNatExpr expr` Full Usage: `FVarsNatExpr expr` Parameters: expr : `NatExpr` Returns: `Set<QName * QType>`	expr : `NatExpr` Returns: `Set<QName * QType>`
`FVarsRealExpr expr` Full Usage: `FVarsRealExpr expr` Parameters: expr : `RealExpr` Returns: `Set<QName * QType>`	expr : `RealExpr` Returns: `Set<QName * QType>`
`FVarsTupExpr expr` Full Usage: `FVarsTupExpr expr` Parameters: expr : `TupExpr` Returns: `Set<QName * QType>`	expr : `TupExpr` Returns: `Set<QName * QType>`
`GetArr expr` Full Usage: `GetArr expr` Parameters: expr : `Expr` Returns: `ArrExpr`	GetArr(Earr t)=t and fails for other expressions expr : `Expr` Returns: `ArrExpr`
`GetBool expr` Full Usage: `GetBool expr` Parameters: expr : `Expr` Returns: `BoolExpr`	GetBool(Ebool t)=t and fails for other expressions expr : `Expr` Returns: `BoolExpr`
`GetBtv expr` Full Usage: `GetBtv expr` Parameters: expr : `Expr` Returns: `BtvExpr`	GetBtv(Ebtv t)=t and fails for other expressions expr : `Expr` Returns: `BtvExpr`
`GetInt expr` Full Usage: `GetInt expr` Parameters: expr : `Expr` Returns: `IntExpr`	GetInt(Eint t)=t and fails for other expressions expr : `Expr` Returns: `IntExpr`
`GetLhs expr` Full Usage: `GetLhs expr` Parameters: expr : `Expr` Returns: `LhsExpr`	GetLhs(Elhs t)=t and fails for other expressions expr : `Expr` Returns: `LhsExpr`
`GetNat expr` Full Usage: `GetNat expr` Parameters: expr : `Expr` Returns: `NatExpr`	GetNat(Enat t)=t and fails for other expressions expr : `Expr` Returns: `NatExpr`
`GetReal expr` Full Usage: `GetReal expr` Parameters: expr : `Expr` Returns: `RealExpr`	GetReal(Ereal t)=t and fails for other expressions expr : `Expr` Returns: `RealExpr`
`GetTup expr` Full Usage: `GetTup expr` Parameters: expr : `Expr` Returns: `TupExpr`	GetTup(Etup t)=t and fails for other expressions expr : `Expr` Returns: `TupExpr`
`LengthOfBtvExpr btvExpr` Full Usage: `LengthOfBtvExpr btvExpr` Parameters: btvExpr : `BtvExpr` Returns: `int option`	btvExpr : `BtvExpr` Returns: `int option`
`Lhs2Rhs lhs` Full Usage: `Lhs2Rhs lhs` Parameters: lhs : `LhsExpr` Returns: `Expr`	lhs : `LhsExpr` Returns: `Expr`
`Lhs2TypeRhs expr` Full Usage: `Lhs2TypeRhs expr` Parameters: expr : `LhsExpr` Returns: `QType * Expr`	expr : `LhsExpr` Returns: `QType * Expr`
`LhsEquCond lhsExpr1 lhsExpr2` Full Usage: `LhsEquCond lhsExpr1 lhsExpr2` Parameters: lhsExpr1 : `LhsExpr` lhsExpr2 : `LhsExpr` Returns: `BoolExpr`	generate a BoolExpr that states that lhsExpr1 and lhsExpr2 are equal lhsExpr1 : `LhsExpr` lhsExpr2 : `LhsExpr` Returns: `BoolExpr`
`LhsWriteCells lhsExpr` Full Usage: `LhsWriteCells lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `Set<LhsExpr>`	LhsWriteCells lhs computes the writeable cells of a lhsExpr. lhsExpr : `LhsExpr` Returns: `Set<LhsExpr>`
`MkArrAccExpr qty (ar, e)` Full Usage: `MkArrAccExpr qty (ar, e)` Parameters: qty : `QType` ar : `ArrExpr` e : `NatExpr` Returns: `Expr`	qty : `QType` ar : `ArrExpr` e : `NatExpr` Returns: `Expr`
`MkBoolBitOfBtv (expr, n)` Full Usage: `MkBoolBitOfBtv (expr, n)` Parameters: expr : `BtvExpr` n : `int` Returns: `BoolExpr`	expr : `BtvExpr` n : `int` Returns: `BoolExpr`
`MkBoolCase (arg1, arg2)` Full Usage: `MkBoolCase (arg1, arg2)` Parameters: arg0 : `(BoolExpr * BoolExpr) list` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `(BoolExpr * BoolExpr) list` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBoolConj (arg1, arg2)` Full Usage: `MkBoolConj (arg1, arg2)` Parameters: arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBoolCont expr` Full Usage: `MkBoolCont expr` Parameters: expr : `BoolExpr` Returns: `BoolExpr`	expr : `BoolExpr` Returns: `BoolExpr`
`MkBoolDisj (arg1, arg2)` Full Usage: `MkBoolDisj (arg1, arg2)` Parameters: arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBoolEqu (arg1, arg2)` Full Usage: `MkBoolEqu (arg1, arg2)` Parameters: arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBoolImpl (arg1, arg2)` Full Usage: `MkBoolImpl (arg1, arg2)` Parameters: arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBoolIte (c, t1, t2)` Full Usage: `MkBoolIte (c, t1, t2)` Parameters: c : `BoolExpr` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	c : `BoolExpr` t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`MkBoolNeg expr` Full Usage: `MkBoolNeg expr` Parameters: expr : `BoolExpr` Returns: `BoolExpr`	expr : `BoolExpr` Returns: `BoolExpr`
`MkBoolNext expr` Full Usage: `MkBoolNext expr` Parameters: expr : `BoolExpr` Returns: `BoolExpr`	expr : `BoolExpr` Returns: `BoolExpr`
`MkBoolXor (arg1, arg2)` Full Usage: `MkBoolXor (arg1, arg2)` Parameters: arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`	arg0 : `BoolExpr` arg1 : `BoolExpr` Returns: `BoolExpr`
`MkBtvAppend (arg1, arg2)` Full Usage: `MkBtvAppend (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvConj (arg1, arg2)` Full Usage: `MkBtvConj (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvDisj (arg1, arg2)` Full Usage: `MkBtvDisj (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvEqu (arg1, arg2)` Full Usage: `MkBtvEqu (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BoolExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BoolExpr`
`MkBtvEqv (arg1, arg2)` Full Usage: `MkBtvEqv (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvImpl (arg1, arg2)` Full Usage: `MkBtvImpl (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvNeg expr` Full Usage: `MkBtvNeg expr` Parameters: expr : `BtvExpr` Returns: `BtvExpr`	expr : `BtvExpr` Returns: `BtvExpr`
`MkBtvOfBoolTup bl` Full Usage: `MkBtvOfBoolTup bl` Parameters: bl : `BoolExpr list` Returns: `BtvExpr`	bl : `BoolExpr list` Returns: `BtvExpr`
`MkBtvOfInt (expr, len)` Full Usage: `MkBtvOfInt (expr, len)` Parameters: expr : `IntExpr` len : `int` Returns: `BtvExpr`	expr : `IntExpr` len : `int` Returns: `BtvExpr`
`MkBtvOfNat (expr, len)` Full Usage: `MkBtvOfNat (expr, len)` Parameters: expr : `NatExpr` len : `int` Returns: `BtvExpr`	expr : `NatExpr` len : `int` Returns: `BtvExpr`
`MkBtvReplicate (expr, n)` Full Usage: `MkBtvReplicate (expr, n)` Parameters: expr : `BoolExpr` n : `int` Returns: `BtvExpr`	expr : `BoolExpr` n : `int` Returns: `BtvExpr`
`MkBtvReverse expr` Full Usage: `MkBtvReverse expr` Parameters: expr : `BtvExpr` Returns: `BtvExpr`	expr : `BtvExpr` Returns: `BtvExpr`
`MkBtvSegment (expr, n2, n1)` Full Usage: `MkBtvSegment (expr, n2, n1)` Parameters: expr : `BtvExpr` n2 : `int` n1 : `int` Returns: `BtvExpr`	expr : `BtvExpr` n2 : `int` n1 : `int` Returns: `BtvExpr`
`MkBtvSignAdjust (len, expr)` Full Usage: `MkBtvSignAdjust (len, expr)` Parameters: len : `int` expr : `BtvExpr` Returns: `BtvExpr`	len : `int` expr : `BtvExpr` Returns: `BtvExpr`
`MkBtvXor (arg1, arg2)` Full Usage: `MkBtvXor (arg1, arg2)` Parameters: arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`	arg0 : `BtvExpr` arg1 : `BtvExpr` Returns: `BtvExpr`
`MkBtvZeroAdjust (len, expr)` Full Usage: `MkBtvZeroAdjust (len, expr)` Parameters: len : `int` expr : `BtvExpr` Returns: `BtvExpr`	len : `int` expr : `BtvExpr` Returns: `BtvExpr`
`MkCaseExpr (CL, expr)` Full Usage: `MkCaseExpr (CL, expr)` Parameters: CL : `(BoolExpr * Expr) list` expr : `Expr` Returns: `Expr`	MkCaseExpr(CL,expr) generates a case-expression using one of the constructors BoolCase,BtvCase,NatCase,IntCase,RealCase,ArrCase,TupCase depending on expr. CL : `(BoolExpr * Expr) list` expr : `Expr` Returns: `Expr`
`MkEquExpr qty (e1, e2)` Full Usage: `MkEquExpr qty (e1, e2)` Parameters: qty : `QType` e1 : `Expr` e2 : `Expr` Returns: `BoolExpr`	qty : `QType` e1 : `Expr` e2 : `Expr` Returns: `BoolExpr`
`MkIntAbs expr` Full Usage: `MkIntAbs expr` Parameters: expr : `IntExpr` Returns: `NatExpr`	expr : `IntExpr` Returns: `NatExpr`
`MkIntAdd (arg1, arg2)` Full Usage: `MkIntAdd (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`
`MkIntDiv (arg1, arg2)` Full Usage: `MkIntDiv (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`
`MkIntEqu (arg1, arg2)` Full Usage: `MkIntEqu (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`
`MkIntLeq (arg1, arg2)` Full Usage: `MkIntLeq (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`
`MkIntLes (arg1, arg2)` Full Usage: `MkIntLes (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `BoolExpr`
`MkIntMod (arg1, arg2)` Full Usage: `MkIntMod (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`
`MkIntMul (arg1, arg2)` Full Usage: `MkIntMul (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`
`MkIntOfBtv expr` Full Usage: `MkIntOfBtv expr` Parameters: expr : `BtvExpr` Returns: `IntExpr`	expr : `BtvExpr` Returns: `IntExpr`
`MkIntOfNat expr` Full Usage: `MkIntOfNat expr` Parameters: expr : `NatExpr` Returns: `IntExpr`	expr : `NatExpr` Returns: `IntExpr`
`MkIntSat (blm, expr)` Full Usage: `MkIntSat (blm, expr)` Parameters: blm : `bool list` expr : `IntExpr` Returns: `IntExpr`	blm : `bool list` expr : `IntExpr` Returns: `IntExpr`
`MkIntSub (arg1, arg2)` Full Usage: `MkIntSub (arg1, arg2)` Parameters: arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`	arg0 : `IntExpr` arg1 : `IntExpr` Returns: `IntExpr`
`MkIteExpr (arg1, arg2, arg3)` Full Usage: `MkIteExpr (arg1, arg2, arg3)` Parameters: arg0 : `BoolExpr` arg1 : `Expr` arg2 : `Expr` Returns: `Expr`	MkIteExpr(b,e1,e2) generates an if-then-else expression using one of the constructors BoolIte,BtvIte,NatIte,IntIte,RealIte,ArrIte,TupIte depending on the "types" of e1 and e2 (that should be the same). The result may however not be an Ite-expression since some simplication rules are used. arg0 : `BoolExpr` arg1 : `Expr` arg2 : `Expr` Returns: `Expr`
`MkListConj eL` Full Usage: `MkListConj eL` Parameters: eL : `seq<BoolExpr>` Returns: `BoolExpr`	eL : `seq<BoolExpr>` Returns: `BoolExpr`
`MkListDisj eL` Full Usage: `MkListDisj eL` Parameters: eL : `seq<BoolExpr>` Returns: `BoolExpr`	eL : `seq<BoolExpr>` Returns: `BoolExpr`
`MkListExists t ityL` Full Usage: `MkListExists t ityL` Parameters: t : `BoolExpr` ityL : `(QName * QType) list` Returns: `BoolExpr`	t : `BoolExpr` ityL : `(QName * QType) list` Returns: `BoolExpr`
`MkListForall t ityL` Full Usage: `MkListForall t ityL` Parameters: t : `BoolExpr` ityL : `(QName * QType) list` Returns: `BoolExpr`	t : `BoolExpr` ityL : `(QName * QType) list` Returns: `BoolExpr`
`MkNatAdd (arg1, arg2)` Full Usage: `MkNatAdd (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkNatDiv (arg1, arg2)` Full Usage: `MkNatDiv (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkNatEqu (arg1, arg2)` Full Usage: `MkNatEqu (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`
`MkNatExp (arg1, arg2)` Full Usage: `MkNatExp (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkNatLeq (arg1, arg2)` Full Usage: `MkNatLeq (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`
`MkNatLes (arg1, arg2)` Full Usage: `MkNatLes (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `BoolExpr`
`MkNatLog2 expr` Full Usage: `MkNatLog2 expr` Parameters: expr : `NatExpr` Returns: `NatExpr`	expr : `NatExpr` Returns: `NatExpr`
`MkNatMod (arg1, arg2)` Full Usage: `MkNatMod (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkNatMul (arg1, arg2)` Full Usage: `MkNatMul (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkNatOfBtv expr` Full Usage: `MkNatOfBtv expr` Parameters: expr : `BtvExpr` Returns: `NatExpr`	expr : `BtvExpr` Returns: `NatExpr`
`MkNatSat (blm, expr)` Full Usage: `MkNatSat (blm, expr)` Parameters: blm : `bool list` expr : `NatExpr` Returns: `NatExpr`	blm : `bool list` expr : `NatExpr` Returns: `NatExpr`
`MkNatSub (arg1, arg2)` Full Usage: `MkNatSub (arg1, arg2)` Parameters: arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`	arg0 : `NatExpr` arg1 : `NatExpr` Returns: `NatExpr`
`MkRealAdd (arg1, arg2)` Full Usage: `MkRealAdd (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`
`MkRealCos expr` Full Usage: `MkRealCos expr` Parameters: expr : `RealExpr` Returns: `RealExpr`	expr : `RealExpr` Returns: `RealExpr`
`MkRealDiv (arg1, arg2)` Full Usage: `MkRealDiv (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`
`MkRealDrv e` Full Usage: `MkRealDrv e` Parameters: e : `RealExpr` Returns: `RealExpr`	e : `RealExpr` Returns: `RealExpr`
`MkRealEqu (arg1, arg2)` Full Usage: `MkRealEqu (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`
`MkRealExp (arg1, arg2)` Full Usage: `MkRealExp (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`
`MkRealLeq (arg1, arg2)` Full Usage: `MkRealLeq (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`
`MkRealLes (arg1, arg2)` Full Usage: `MkRealLes (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `BoolExpr`
`MkRealLog2 expr` Full Usage: `MkRealLog2 expr` Parameters: expr : `RealExpr` Returns: `RealExpr`	expr : `RealExpr` Returns: `RealExpr`
`MkRealMul (arg1, arg2)` Full Usage: `MkRealMul (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`
`MkRealOfInt expr` Full Usage: `MkRealOfInt expr` Parameters: expr : `IntExpr` Returns: `RealExpr`	expr : `IntExpr` Returns: `RealExpr`
`MkRealOfNat expr` Full Usage: `MkRealOfNat expr` Parameters: expr : `NatExpr` Returns: `RealExpr`	expr : `NatExpr` Returns: `RealExpr`
`MkRealSin expr` Full Usage: `MkRealSin expr` Parameters: expr : `RealExpr` Returns: `RealExpr`	expr : `RealExpr` Returns: `RealExpr`
`MkRealSub (arg1, arg2)` Full Usage: `MkRealSub (arg1, arg2)` Parameters: arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`	arg0 : `RealExpr` arg1 : `RealExpr` Returns: `RealExpr`
`MkTupAccExpr qty (t, i)` Full Usage: `MkTupAccExpr qty (t, i)` Parameters: qty : `QType` t : `TupExpr` i : `int` Returns: `Expr`	MkTupAccExpr qty (t,i) generates a tuple selection using one of the constructors BoolTupAcc,BtvTupAcc,NatTupAcc,IntTupAcc,RealTupAcc,ArrTupAcc,TupTupAcc depending on qty. qty : `QType` t : `TupExpr` i : `int` Returns: `Expr`
`MkTupEqu (arg1, arg2)` Full Usage: `MkTupEqu (arg1, arg2)` Parameters: arg0 : `TupExpr` arg1 : `TupExpr` Returns: `BoolExpr`	arg0 : `TupExpr` arg1 : `TupExpr` Returns: `BoolExpr`
`MkVarExpr qn qtype` Full Usage: `MkVarExpr qn qtype` Parameters: qn : `QName` qtype : `QType` Returns: `Expr`	generates a variable with name qn and type qtype as an expression qn : `QName` qtype : `QType` Returns: `Expr`
`NoNextInArrExpr expr` Full Usage: `NoNextInArrExpr expr` Parameters: expr : `ArrExpr` Returns: `bool`	expr : `ArrExpr` Returns: `bool`
`NoNextInBoolExpr expr` Full Usage: `NoNextInBoolExpr expr` Parameters: expr : `BoolExpr` Returns: `bool`	expr : `BoolExpr` Returns: `bool`
`NoNextInBtvExpr expr` Full Usage: `NoNextInBtvExpr expr` Parameters: expr : `BtvExpr` Returns: `bool`	expr : `BtvExpr` Returns: `bool`
`NoNextInExpr expr` Full Usage: `NoNextInExpr expr` Parameters: expr : `Expr` Returns: `bool`	expr : `Expr` Returns: `bool`
`NoNextInIntExpr expr` Full Usage: `NoNextInIntExpr expr` Parameters: expr : `IntExpr` Returns: `bool`	expr : `IntExpr` Returns: `bool`
`NoNextInNatExpr expr` Full Usage: `NoNextInNatExpr expr` Parameters: expr : `NatExpr` Returns: `bool`	expr : `NatExpr` Returns: `bool`
`NoNextInRealExpr expr` Full Usage: `NoNextInRealExpr expr` Parameters: expr : `RealExpr` Returns: `bool`	expr : `RealExpr` Returns: `bool`
`NoNextInTupExpr expr` Full Usage: `NoNextInTupExpr expr` Parameters: expr : `TupExpr` Returns: `bool`	expr : `TupExpr` Returns: `bool`
`PrnArrExpr e` Full Usage: `PrnArrExpr e` Parameters: e : `ArrExpr` Returns: `PrnDrv -> unit`	e : `ArrExpr` Returns: `PrnDrv -> unit`
`PrnBoolExpr e` Full Usage: `PrnBoolExpr e` Parameters: e : `BoolExpr` Returns: `PrnDrv -> unit`	e : `BoolExpr` Returns: `PrnDrv -> unit`
`PrnBtvExpr e` Full Usage: `PrnBtvExpr e` Parameters: e : `BtvExpr` Returns: `PrnDrv -> unit`	e : `BtvExpr` Returns: `PrnDrv -> unit`
`PrnExpr e` Full Usage: `PrnExpr e` Parameters: e : `Expr` Returns: `PrnDrv -> unit`	e : `Expr` Returns: `PrnDrv -> unit`
`PrnIntExpr e` Full Usage: `PrnIntExpr e` Parameters: e : `IntExpr` Returns: `PrnDrv -> unit`	e : `IntExpr` Returns: `PrnDrv -> unit`
`PrnLhsExpr e` Full Usage: `PrnLhsExpr e` Parameters: e : `LhsExpr` Returns: `Printer`	e : `LhsExpr` Returns: `Printer`
`PrnNatExpr e` Full Usage: `PrnNatExpr e` Parameters: e : `NatExpr` Returns: `PrnDrv -> unit`	e : `NatExpr` Returns: `PrnDrv -> unit`
`PrnRealExpr e` Full Usage: `PrnRealExpr e` Parameters: e : `RealExpr` Returns: `PrnDrv -> unit`	e : `RealExpr` Returns: `PrnDrv -> unit`
`PrnSubst rho` Full Usage: `PrnSubst rho` Parameters: rho : `Map<QName, Expr>` Returns: `PrnDrv -> unit`	Prints a substitution rho : `Map<QName, Expr>` Returns: `PrnDrv -> unit`
`PrnTupExpr e` Full Usage: `PrnTupExpr e` Parameters: e : `TupExpr` Returns: `PrnDrv -> unit`	e : `TupExpr` Returns: `PrnDrv -> unit`
`QNameOfVarExpr expr` Full Usage: `QNameOfVarExpr expr` Parameters: expr : `Expr` Returns: `QName`	QNameOfVarExpr extracts the qualified name of an expression variable, e.g. QNameOfVarExpr(Ebool(BoolVar qn))=qn expr : `Expr` Returns: `QName`
`RangeOfIntExpr intExpr` Full Usage: `RangeOfIntExpr intExpr` Parameters: intExpr : `IntExpr` Returns: `bool list option`	intExpr : `IntExpr` Returns: `bool list option`
`RangeOfNatExpr natExpr` Full Usage: `RangeOfNatExpr natExpr` Parameters: natExpr : `NatExpr` Returns: `bool list option`	natExpr : `NatExpr` Returns: `bool list option`
`ReadSubstLhs rho lhsExpr` Full Usage: `ReadSubstLhs rho lhsExpr` Parameters: rho : `Map<QName, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`	rho : `Map<QName, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`
`ReadVarsArrExpr` Full Usage: `ReadVarsArrExpr` Returns: `ArrExpr -> Set<QName * QType>`	Returns: `ArrExpr -> Set<QName * QType>`
`ReadVarsBoolExpr` Full Usage: `ReadVarsBoolExpr` Returns: `BoolExpr -> Set<QName * QType>`	Returns: `BoolExpr -> Set<QName * QType>`
`ReadVarsBtvExpr` Full Usage: `ReadVarsBtvExpr` Returns: `BtvExpr -> Set<QName * QType>`	Returns: `BtvExpr -> Set<QName * QType>`
`ReadVarsExpr expr` Full Usage: `ReadVarsExpr expr` Parameters: expr : `Expr` Returns: `Set<QName * QType>`	expr : `Expr` Returns: `Set<QName * QType>`
`ReadVarsIntExpr` Full Usage: `ReadVarsIntExpr` Returns: `IntExpr -> Set<QName * QType>`	Returns: `IntExpr -> Set<QName * QType>`
`ReadVarsLhsExpr expr` Full Usage: `ReadVarsLhsExpr expr` Parameters: expr : `LhsExpr` Returns: `Set<QName * QType>`	expr : `LhsExpr` Returns: `Set<QName * QType>`
`ReadVarsNatExpr` Full Usage: `ReadVarsNatExpr` Returns: `NatExpr -> Set<QName * QType>`	Returns: `NatExpr -> Set<QName * QType>`
`ReadVarsRealExpr` Full Usage: `ReadVarsRealExpr` Returns: `RealExpr -> Set<QName * QType>`	Returns: `RealExpr -> Set<QName * QType>`
`ReadVarsTupExpr` Full Usage: `ReadVarsTupExpr` Returns: `TupExpr -> Set<QName * QType>`	Returns: `TupExpr -> Set<QName * QType>`
`RewriteArr eqs arrExpr` Full Usage: `RewriteArr eqs arrExpr` Parameters: eqs : `Map<LhsExpr, Expr>` arrExpr : `ArrExpr` Returns: `ArrExpr`	eqs : `Map<LhsExpr, Expr>` arrExpr : `ArrExpr` Returns: `ArrExpr`
`RewriteBool eqs boolExpr` Full Usage: `RewriteBool eqs boolExpr` Parameters: eqs : `Map<LhsExpr, Expr>` boolExpr : `BoolExpr` Returns: `BoolExpr`	eqs : `Map<LhsExpr, Expr>` boolExpr : `BoolExpr` Returns: `BoolExpr`
`RewriteBtv eqs btvExpr` Full Usage: `RewriteBtv eqs btvExpr` Parameters: eqs : `Map<LhsExpr, Expr>` btvExpr : `BtvExpr` Returns: `BtvExpr`	eqs : `Map<LhsExpr, Expr>` btvExpr : `BtvExpr` Returns: `BtvExpr`
`RewriteExpr eqs expr` Full Usage: `RewriteExpr eqs expr` Parameters: eqs : `Map<LhsExpr, Expr>` expr : `Expr` Returns: `Expr`	eqs : `Map<LhsExpr, Expr>` expr : `Expr` Returns: `Expr`
`RewriteInt eqs intExpr` Full Usage: `RewriteInt eqs intExpr` Parameters: eqs : `Map<LhsExpr, Expr>` intExpr : `IntExpr` Returns: `IntExpr`	eqs : `Map<LhsExpr, Expr>` intExpr : `IntExpr` Returns: `IntExpr`
`RewriteLhs eqs lhsExpr` Full Usage: `RewriteLhs eqs lhsExpr` Parameters: eqs : `Map<LhsExpr, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`	eqs : `Map<LhsExpr, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`
`RewriteNat eqs natExpr` Full Usage: `RewriteNat eqs natExpr` Parameters: eqs : `Map<LhsExpr, Expr>` natExpr : `NatExpr` Returns: `NatExpr`	eqs : `Map<LhsExpr, Expr>` natExpr : `NatExpr` Returns: `NatExpr`
`RewriteReal eqs realExpr` Full Usage: `RewriteReal eqs realExpr` Parameters: eqs : `Map<LhsExpr, Expr>` realExpr : `RealExpr` Returns: `RealExpr`	eqs : `Map<LhsExpr, Expr>` realExpr : `RealExpr` Returns: `RealExpr`
`RewriteTup eqs tupExpr` Full Usage: `RewriteTup eqs tupExpr` Parameters: eqs : `Map<LhsExpr, Expr>` tupExpr : `TupExpr` Returns: `TupExpr`	eqs : `Map<LhsExpr, Expr>` tupExpr : `TupExpr` Returns: `TupExpr`
`Rhs2Lhs expr` Full Usage: `Rhs2Lhs expr` Parameters: expr : `Expr` Returns: `LhsExpr`	expr : `Expr` Returns: `LhsExpr`
`StripConj t` Full Usage: `StripConj t` Parameters: t : `BoolExpr` Returns: `Set<BoolExpr>`	t : `BoolExpr` Returns: `Set<BoolExpr>`
`StripDisj t` Full Usage: `StripDisj t` Parameters: t : `BoolExpr` Returns: `Set<BoolExpr>`	t : `BoolExpr` Returns: `Set<BoolExpr>`
`SubstArr rho arrExpr` Full Usage: `SubstArr rho arrExpr` Parameters: rho : `Map<QName, Expr>` arrExpr : `ArrExpr` Returns: `ArrExpr`	rho : `Map<QName, Expr>` arrExpr : `ArrExpr` Returns: `ArrExpr`
`SubstBool rho boolExpr` Full Usage: `SubstBool rho boolExpr` Parameters: rho : `Map<QName, Expr>` boolExpr : `BoolExpr` Returns: `BoolExpr`	rho : `Map<QName, Expr>` boolExpr : `BoolExpr` Returns: `BoolExpr`
`SubstBtv rho btvExpr` Full Usage: `SubstBtv rho btvExpr` Parameters: rho : `Map<QName, Expr>` btvExpr : `BtvExpr` Returns: `BtvExpr`	rho : `Map<QName, Expr>` btvExpr : `BtvExpr` Returns: `BtvExpr`
`SubstExpr rho expr` Full Usage: `SubstExpr rho expr` Parameters: rho : `Map<QName, Expr>` expr : `Expr` Returns: `Expr`	rho : `Map<QName, Expr>` expr : `Expr` Returns: `Expr`
`SubstInt rho intExpr` Full Usage: `SubstInt rho intExpr` Parameters: rho : `Map<QName, Expr>` intExpr : `IntExpr` Returns: `IntExpr`	rho : `Map<QName, Expr>` intExpr : `IntExpr` Returns: `IntExpr`
`SubstLhs rho lhsExpr` Full Usage: `SubstLhs rho lhsExpr` Parameters: rho : `Map<QName, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`	rho : `Map<QName, Expr>` lhsExpr : `LhsExpr` Returns: `LhsExpr`
`SubstNat rho natExpr` Full Usage: `SubstNat rho natExpr` Parameters: rho : `Map<QName, Expr>` natExpr : `NatExpr` Returns: `NatExpr`	rho : `Map<QName, Expr>` natExpr : `NatExpr` Returns: `NatExpr`
`SubstQName rho qn` Full Usage: `SubstQName rho qn` Parameters: rho : `Map<QName, Expr>` qn : `QName` Returns: `QName`	rho : `Map<QName, Expr>` qn : `QName` Returns: `QName`
`SubstReal rho realExpr` Full Usage: `SubstReal rho realExpr` Parameters: rho : `Map<QName, Expr>` realExpr : `RealExpr` Returns: `RealExpr`	rho : `Map<QName, Expr>` realExpr : `RealExpr` Returns: `RealExpr`
`SubstTup rho tupExpr` Full Usage: `SubstTup rho tupExpr` Parameters: rho : `Map<QName, Expr>` tupExpr : `TupExpr` Returns: `TupExpr`	rho : `Map<QName, Expr>` tupExpr : `TupExpr` Returns: `TupExpr`
`TargetOfLhs expr` Full Usage: `TargetOfLhs expr` Parameters: expr : `LhsExpr` Returns: `QName`	TargetOfLhs extracts the name of the variable that is written by the given LhsExpr expr, e.g. TargetOfLhs(LhsVar(qn,qty))=qn expr : `LhsExpr` Returns: `QName`
`TypeOfArrExpr arrExpr` Full Usage: `TypeOfArrExpr arrExpr` Parameters: arrExpr : `ArrExpr` Returns: `QType`	arrExpr : `ArrExpr` Returns: `QType`
`TypeOfExpr expr` Full Usage: `TypeOfExpr expr` Parameters: expr : `Expr` Returns: `QType`	expr : `Expr` Returns: `QType`
`TypeOfLhsExpr lhsExpr` Full Usage: `TypeOfLhsExpr lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `QType`	lhsExpr : `LhsExpr` Returns: `QType`
`TypeOfTupExpr tupExpr` Full Usage: `TypeOfTupExpr tupExpr` Parameters: tupExpr : `TupExpr` Returns: `QType`	tupExpr : `TupExpr` Returns: `QType`