Fobdds, functions, equality and derived symbols don't really work well together

Currently, fobdds can represent formulas, either over the original vocabulary or over the derived vocabulary. As long as the formulas contain only predicates, this works find. But for functions, this is more difficult.

For example the constraint

(f(x) = y) <ct>

should be transformed to a correct bdd, preferably referring to the ct table of f.

But the only way to transform this now would be.

f(x) =<ct> y

And this doesn't work well. Allowing derived variants of equality in BDDs (which is not possible now) results in serious segfaulting...

This can be avoided by always graphing partially known functions, but... we don't want to graph everything.

In the future, we should think how function should be used in BDDs.

(this behaviour was the cause of issue https://bitbucket.org/krr/idp/issue/495)

Comments (1)