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)
