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. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

翻译：决策图（DDs）是有效表示命题公式的强大工具，在众多领域尤其在形式化验证和知识编译中得到广泛应用。某些形式的决策图（如OBDD、SDD）具有规范性，即在给定原子列表条件下，能唯一表示公式的等价类。鉴于命题逻辑表达能力的局限性，已有文献提出将DDs扩展到SMT层次的一些尝试。然而，这些技术仍存在若干局限：多数过程具有理论特异性；部分方法生成的理论决策图（T-DDs）无法唯一表示理论有效公式或理论不一致公式；尚无技术能可证明地生成理论规范型T-DDs（即在给定理论原子列表条件下唯一表示理论等价类公式）。此外，这些过程实现困难，实际可用的实现极少。本文提出一种新颖且高度通用的技术，将DDs扩展到SMT层次，具有多项优势：可基于AllSMT求解器和DD包（作为黑箱使用）轻松实现；适用于任何形式的DDs及AllSMT求解器支持的任何理论或其组合；当命题DD具备规范性时，能生成理论规范型T-DDs。我们在OBDD和SDD包以及MathSAT SMT求解器基础上，实现了同时支持T-OBDD和T-SDD的原型工具。初步实证评估验证了该方法的有效性。