Implements a hash table to abbreviate boolean expressions by new variables so that common sub-expressions 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 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).

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, radix-2 numbers or 2-complement numbers. It is always assumed that radix-2 numbers have no redundant leading zeros, and that 2-complement 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 nat-constants, BinBitConst2BL for binary bv-constants, OctBitConst2BL for octal bv-constants, and HexBitConst2BL for hexadecimal bv-constants. Functions NatDecStr2BL, BL2NatDecStr, Nat2BL, BL2Nat convert between natural numbers and their radix-2 representations (as boolean lists) and analogously IntDecStr2BL, BL2IntDecStr, Int2BL, BL2Int convert between integers and their 2-complement 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.