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 e` Full Usage: `AtomsOfBoolExpr e` Parameters: e : `BoolExpr` Returns: `Set<BoolExpr>`	compute atoms of a BoolExpr in some random order e : `BoolExpr` Returns: `Set<BoolExpr>`
`BoolExpr2Latex e` Full Usage: `BoolExpr2Latex e` Parameters: e : `BoolExpr` Returns: `string`	print a propositional formula in Latex e : `BoolExpr` Returns: `string`
`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`
`ComputeAllAssignments atomL` Full Usage: `ComputeAllAssignments atomL` Parameters: atomL : `BoolExpr list` Returns: `Map<BoolExpr, bool> list`	Enumerate all assignments for the given list of atoms; an assignment is thereby a map that maps an atom of the given boolean expression to a boolean value. atomL : `BoolExpr list` Returns: `Map<BoolExpr, bool> 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`
`EvalBoolExpr rho e` Full Usage: `EvalBoolExpr rho e` Parameters: rho : `Map<BoolExpr, bool>` e : `BoolExpr` Returns: `bool`	Evaluate a formula with respect to a given assignment of its atoms. It is expected that the given assignment is complete, i.e., that every atom of the given boolean expression is mapped to either true or false. rho : `Map<BoolExpr, bool>` e : `BoolExpr` Returns: `bool`
`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`
`PartialEval rho e` Full Usage: `PartialEval rho e` Parameters: rho : `Map<BoolExpr, bool>` e : `BoolExpr` Returns: `BoolExpr`	Partial evaluation of a formula wrt. a partial variable assignment: Since the given assignment rho may not map every atom of the boolean expression to a boolean value, the result is just another boolean formula where the mapped atoms are replaced by constants and where simplifications were applied to propagate these constants. rho : `Map<BoolExpr, bool>` e : `BoolExpr` Returns: `BoolExpr`
`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`