BDD test if an expression is true using PyEDA

Question

I am trying to use the PyEDA package BDD implementation, and feed "True/False" data to construct a functional BDD. Then test as my data get updated if new expression is "True" in the constructed BDD.

However, I could not utilize the "equivalent" method and get a "True". Maybe, the expression construction is wrong, or something else.

I did not come for an electronics background, thus I couldn't fully understand some of the techniques presented in the documentation.

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

I found a workaround, by constructing a BDD from the test expression, then test if it is present in the original BDD.

test_bdd.satisfy_one() in src_bdd.satisfy_all()

Answer 2

The previous answer has worked, however, it checks for an expression linearly: Previous answer

test_bdd.satisfy_one() in src_bdd.satisfy_all()

Here is my new one, which checks if the conjoint expression and provided tree arrive to the terminal node zero, which means the expression is not presented in the tree: Full Example:

# import
from pyeda.inter import *
from pyeda.boolalg.bdd import BDDZERO, BDDONE

# define BDD variables
x1, x2, x3 = map(bddvar, 'x1 x2 x3'.split())

# build the BDD
dd = BDDZERO # root

# add couple of expressions
f1 = x1 & ~x2 & x3
dd |= f1

f2 = ~x1 & x2 & x3
dd |= f2

# check expression (true = not found)
f3 = ~x1 & x2 & ~x3
(dd & f3) == BDDZERO

# check expression (false = found)
f4 = ~x1 & x2 & x3
(dd & f4) == BDDZERO