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）具有典范性，即（在给定原子列表的条件下）它们能唯一表示公式的等价类。鉴于命题逻辑表达能力有限，文献中已提出一些尝试将决策图提升到SMT层面的方法。遗憾的是，这些技术仍存在局限性：多数方法针对特定理论；部分生成的理论决策图（T-DDs）无法唯一表示T-有效公式或T-不一致公式；没有一种方法可证明能产生理论典范的T-DDs，即（在给定T-原子列表的条件下）唯一表示公式T-等价类的决策图。此外，这些方法实现困难，实际可用的实现极少。本文提出一种新颖且通用的技术，将决策图提升到SMT层面，具有多项优势：它可轻松基于AllSMT求解器和决策图包（作为黑盒使用）实现；适用于AllSMT求解器支持的任何决策图形式、任意理论或其组合；若命题决策图具有典范性，则生成的T-DDs具有理论典范性。我们基于OBDD和SDD包以及MathSAT SMT求解器，实现了针对T-OBDD和T-SDD的原型工具。初步实验评估支持了该方法的有效性。