在Z3中得到布尔公式中的原子

Question

我想知道是否有一种方法可以得到布尔公式的原子：

a = Bool('a')
b = Bool('b')
c = Bool('C')
d = Bool('D')
e = Bool('E')
f = Bool('F')

formula = And(Or(a, b), Or(c, d), Or(e, f))

我想知道这样的事情是否存在：

formula.get_atoms() or get_atoms(formula)

给我以下期望的输出：

{A, B, C, D, E, F}

在pySMT中，get_atoms()存在提供原子。然而，出于某种原因，我需要在Z3上进行实验。

Answer 1

您可以遍历children() (文档)的层次结构：

def atoms(expr):
    a = set()
    if not str(expr) in {'True', 'False'}:
        c = expr.children()
        if len(c):
            for child in c:
                a = a.union(atoms(child))  
        else:
            a = {expr}
    return a    

a = Bool('a')
b = Bool('b')
c = Bool('C')
d = Bool('D')
e = Bool('E')
f = Bool('F')

formula = And(Or(a, b), Or(c, d), Or(e, f))

print(atoms(formula))