Modules  Description 
Implements a hash table to abbreviate boolean expressions by new variables so that common subexpressions can be shared. 



support for debug messages and conditional checks, debug levels are: 1: general messages about progress, 2: messages about internal state, 3: runtime checks 



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 lefthand side expressions LhsExpr that may have any type, but whose operators are restricted to those that can appear on lefthand sides of assignments. Certain operators like *Var,*Ite,*Case,*ArrAcc, and *TupAcc are defined for all types and these generate variables, ifthenelse expressions, case expressions, array element access, and tuple access. The other operators should be rather selfexplaining (see Module StaticEvaluation for further explanation of these operations and note that boolean lists are usually bitvector constants, radix2 numbers or 2complement numbers). 

Module Global contains some general definitions. 

This module provides some generel algorithms on (directed) graphs, where the graphs are usually represented as maps where a node is mapped to the set of its successor nodes. In case of directed acyclic graphs, one may optionally specify the set of root nodes to avoid that computation. 



This module implements functions for structured pretty printing. In general, the functions obtain a value to be printed, and a printer driver and will then generates a printer. A printer driver is thereby a function of type PrnDrv : (string > unit) that will later on consume a string to print it. Such a printer driver is given to a printer which has consequently type PrnDrv > unit to finally print the value. Hence, given a printer driver p:PrnDrv, and a printer P:Printer, the function application (P p) finally prints the value that was used to generate the printer P. A pretty printer is function that maps a given precedence to a Printer. This concept allows one to easily print all kinds of values into files, strings, and output streams. 



Module StaticEvaluation implements static evaluation of constant expressions of scalar types. To this end, all scalar types are assumed to be reduced to boolean lists, and depending on the operator, these boolean lists may simply be bitvectors, radix2 numbers or 2complement numbers. It is always assumed that radix2 numbers have no redundant leading zeros, and that 2complement numbers do not have redundant signs. In addition to the static evaluation functions, the module also provides translations of constants of Quartz expressions given as strings to boolean lists as given by functions NatConstStr2BL for natconstants, BinBitConst2BL for binary bvconstants, OctBitConst2BL for octal bvconstants, and HexBitConst2BL for hexadecimal bvconstants. Functions NatDecStr2BL, BL2NatDecStr, Nat2BL, BL2Nat convert between natural numbers and their radix2 representations (as boolean lists) and analogously IntDecStr2BL, BL2IntDecStr, Int2BL, BL2Int convert between integers and their 2complement representations (as boolean lists) Finally, the module provides some additional arithmetic operators like Div, Mod, FloorLog2, and CeilLog2. 

Module Types implements the data types of the Quartz language. 