This module implements a simple BDD package where nodes of the BDD directly refer to boolean Quartz expressions. For using the package, one first has to initialize the BDD manager which is done by the function Initialize. To this end, the maximal number of available nodes has to be specified as well as a list of boolean Quartz expressions that are mapped in the given order to BDD variables (of type BDDIndex). After that, one may use the typical BDD functions that will then create new nodes when necessary (unless the desired node does not yet exist). The user should invoke from time to time function GarbageCollect to allow the BDD package to reuse nodes that are no longer variable needed. The ordering is stored in Index2BoolExpr and can be modified with function SwapVar.

Functions of this model deal with the theory of equality of uninterpreted functions (EUF). To this end, reductions are provided that endow given EUF formulas with additional constraints so that the satisfiability or validity can be decided by means of a propositional SAT solver. In particular, constraints are added to ensure the congruence of functions, i.e. x1=x2 must imply f(x1)=f(x2), and the transitivity of equations. The generated assumptions are added as conjunctions asm&phi for checking the satisfiability, and as an implication asm->phi for checking the validity of an EUF formula phi.

This module implements algorithms for matrices on rational numbers. To this end, it first implements a type for rational and complex numbers, and based on these, algorithms for inverting a matrix, for solving linear (in)equation systems, and for computing eigenvalues (e.g. to solve linear differential equation systems) are provided.

This module implements functions for checking the satisfiability of boolean expressions. The SAT checking procedures are based on Shannon graphs which are unreduced unordered binary decision diagrams. This has the advantage that one can construct an equivalent Shannon graph for a given BoolExpr in linear time.

The functions of this module provide translations from temporal logics to symbolically encoded omega automata. In general, these translations replace an elementary subformula (one that starts with a temporal operator) by a new state variable of the automaton and according state transitions and contraints so that the new state variable becomes equivalent to the elementary subformula it abbreviates. To this end, one usually makes use of GF-constraints which however are harder to check than others. They cannot always be avoided, but the translators presented here may try to use F-constraints whenever possible which then usually generates a cascade of F-constraints, i.e. formulas of the following form where phi is propositional: CF ::= F phi | F(phi&CF) | X CF | CF & CF. The use of F or CF-constraints is controlled with option tryConstrF of the translators. In addition to the use of GF or F-constraints, the translators differ also in the acceptance condition they finally produce: LTL2Omega will just have these constraints while LTL2OmegaCTL will rather use a CTL formula (equivalent to an LeftCTL*-LTL formula) with potential GF-constraints. In case F-constraints should be used LTL2OmegaCTL incorporates them to the CTL formula.