Bitvectorizer (Averest)

Bitvectorizer Module

Namespace: Averest.Transform
Assembly: Averest.dll

Functions and values

Function or value	Description
`Arr2BitVec arrayExpr` Full Usage: `Arr2BitVec arrayExpr` Parameters: arrayExpr : `ArrExpr` Returns: `ArrExpr`	arrayExpr : `ArrExpr` Returns: `ArrExpr`
`BitDefAbbrevs` Full Usage: `BitDefAbbrevs` Returns: `AbbrevTable ref`	Returns: `AbbrevTable ref`
`Bitvectorize` Full Usage: `Bitvectorize` Returns: `SystemTrans`	Returns: `SystemTrans`
`Bool2BitVec boolExpr` Full Usage: `Bool2BitVec boolExpr` Parameters: boolExpr : `BoolExpr` Returns: `BoolExpr`	boolExpr : `BoolExpr` Returns: `BoolExpr`
`Boolify` Full Usage: `Boolify` Returns: `SystemTrans`	scalarize Returns: `SystemTrans`
`Btv2BitVec btvExpr` Full Usage: `Btv2BitVec btvExpr` Parameters: btvExpr : `BtvExpr` Returns: `BtvExpr`	btvExpr : `BtvExpr` Returns: `BtvExpr`
`DestBtvBL btvExpr` Full Usage: `DestBtvBL btvExpr` Parameters: btvExpr : `BtvExpr` Returns: `BoolExpr list`	btvExpr : `BtvExpr` Returns: `BoolExpr list`
`DestIntBtvBL intExpr` Full Usage: `DestIntBtvBL intExpr` Parameters: intExpr : `IntExpr` Returns: `BoolExpr list`	intExpr : `IntExpr` Returns: `BoolExpr list`
`DestNatBtvBL natExpr` Full Usage: `DestNatBtvBL natExpr` Parameters: natExpr : `NatExpr` Returns: `BoolExpr list`	natExpr : `NatExpr` Returns: `BoolExpr list`
`Expr2BitVec expr` Full Usage: `Expr2BitVec expr` Parameters: expr : `Expr` Returns: `Expr`	expr : `Expr` Returns: `Expr`
`Int2BitVec intExpr` Full Usage: `Int2BitVec intExpr` Parameters: intExpr : `IntExpr` Returns: `IntExpr`	intExpr : `IntExpr` Returns: `IntExpr`
`Lhs2BitVec lhsExpr` Full Usage: `Lhs2BitVec lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `LhsExpr`	lhsExpr : `LhsExpr` Returns: `LhsExpr`
`Nat2BitVec natExpr` Full Usage: `Nat2BitVec natExpr` Parameters: natExpr : `NatExpr` Returns: `NatExpr`	natExpr : `NatExpr` Returns: `NatExpr`
`NewBitDef t` Full Usage: `NewBitDef t` Parameters: t : `BoolExpr` Returns: `BoolExpr`	t : `BoolExpr` Returns: `BoolExpr`
`NewBitVar ()` Full Usage: `NewBitVar ()` Parameters: () : `unit` Returns: `QName`	() : `unit` Returns: `QName`
`NewConj (t1, t2)` Full Usage: `NewConj (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`NewDisj (t1, t2)` Full Usage: `NewDisj (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`NewEqu (t1, t2)` Full Usage: `NewEqu (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`NewImpl (t1, t2)` Full Usage: `NewImpl (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`NewIte (t1, t2, t3)` Full Usage: `NewIte (t1, t2, t3)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` t3 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` t3 : `BoolExpr` Returns: `BoolExpr`
`NewListConj eList` Full Usage: `NewListConj eList` Parameters: eList : `BoolExpr list` Returns: `BoolExpr`	eList : `BoolExpr list` Returns: `BoolExpr`
`NewListDisj eList` Full Usage: `NewListDisj eList` Parameters: eList : `BoolExpr list` Returns: `BoolExpr`	eList : `BoolExpr list` Returns: `BoolExpr`
`NewNeg t` Full Usage: `NewNeg t` Parameters: t : `BoolExpr` Returns: `BoolExpr`	t : `BoolExpr` Returns: `BoolExpr`
`NewXor (t1, t2)` Full Usage: `NewXor (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `BoolExpr`
`Real2BitVec realExpr` Full Usage: `Real2BitVec realExpr` Parameters: realExpr : `RealExpr` Returns: `RealExpr`	realExpr : `RealExpr` Returns: `RealExpr`
`Spec2BitVec specExpr` Full Usage: `Spec2BitVec specExpr` Parameters: specExpr : `SpecExpr` Returns: `SpecExpr`	specExpr : `SpecExpr` Returns: `SpecExpr`
`StrongNewBitDef t` Full Usage: `StrongNewBitDef t` Parameters: t : `BoolExpr` Returns: `BoolExpr`	t : `BoolExpr` Returns: `BoolExpr`
`Tup2BitVec tupExpr` Full Usage: `Tup2BitVec tupExpr` Parameters: tupExpr : `TupExpr` Returns: `TupExpr`	tupExpr : `TupExpr` Returns: `TupExpr`
`TupelizeBitvectors` Full Usage: `TupelizeBitvectors` Returns: `SystemTrans`	Returns: `SystemTrans`