EqualityTheory Module
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.
Functions and values
| Function or value | Description |
|
AckermannSatReduce phi adds conjuncts to phi that guarantee that models computed by propositional decision procedures satisfy transitivity of the contained equations as well as the functional consistency of equations of the same functions.
|
|
AckermannValidReduce phi generates an implication asm->phi such that asm contains the assumptions about transitivity of equality and the congruence of functions used in phi. Thus, the search of counterexamples is reduced to models of asm.
|
|
Given an undirected graph, this function computes a pair (tc,graph1) where graph1 is a chordal extension of the given graph where the triangles given in set tc cover each cycle of the given graph. The undirected graphs are represented as maps where each node is mapped to the set of its neighbors. |
|
|
Given an equality logic formula phi, this function computes the nonpolar equality graph as defined in Chapter 4.4. of [KrSt08], and extends it to a chordal graph using function Chordalize so that transitivity constraints are derived from the triangles of the chordal graph. The function returns a set of BoolExpr where each expression of that set is a transitivity constraints (three of them are generated per triangle).
|