Canonical Decision Diagrams Modulo Theories

Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T -DDs) which do not univocally represent T -valid formulas or T -inconsistent formulas; none of these techniques provably produces theory-canonical T -DDs, which (under given conditions on the T -atom list) univocally represent T - equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available....