使用PyEDA测试表达式是否为真

Question

我试图使用PyEDA包BDD实现，并输入“真/假”数据来构造一个功能性BDD。然后，当我的数据被更新时，测试是否在构造的BDD中的新表达式是"True“。

但是，我不能用“等价”的方法来得到一个“真”。也许，表达式的构造是错误的，或者别的什么。

我来这里不是为了电子背景，因此我不能完全理解文档中提出的一些技术。

from pyeda.inter import *
import random

str_binary = [format(i, '04b') for i in range(1, 5)]

# 0001 = ~x4 & ~x3 & ~x2 & x1
def convert_binary_str_to_expr(str_binary):
    expr = ['~'*abs(int(str_binary[i])-1) + f'x{i}' for i in range(len(str_binary))]
    return ' & '.join(expr)

# ~x4 & ~x3 & ~x2 & x1 | ~x4 & ~x3 & x2 & ~x1
def join_exprs(str_binary):
    formulas = []

    for e in str_binary:
        formulas.append( convert_binary_str_to_expr(e) )

    return ' | '.join(formulas)

expression = join_exprs(str_binary)

# construct BDD
bdd_exprs = expr(expression)
bdd = expr2bdd(bdd_exprs)

# {x3: 1, x2: 0, x1: 0, x0: 0}
true_expr= bdd_exprs.satisfy_one()

# the idea is to construct like 'x3 & ~x2 & ~x1 & ~x0'
# where the x variables are read from BDD.inputs

# first attempt
test_true_1 = [inp if val==1 else ~inp for inp, val in  zip(bdd.inputs, true_expr.values())]

# False, should be True
bdd.equivalent(test_true_1)

# seconde attempt
# And(~x0, ~x1, ~x2, x3)
test_true_2 = expr('x3 & ~x2 & ~x1 & ~x0')

# False, should be True
bdd.equivalent(test_true_2)

Answer 1

我找到了一个解决办法，通过从测试表达式构建一个BDD，然后测试它是否存在于原始BDD中。

test_bdd.satisfy_one() in src_bdd.satisfy_all()