[FR] Mixing compiled NNF formulas with bauhaus statements

[beckydvn]

Willingness to contribute

The Bauhaus Community encourages new feature contributions. Would you be willing to contribute an implementation of this feature?

• Yes. I can contribute this feature independently.
• Yes. I would be willing to contribute this feature with guidance from the Bauhaus community.
• No. I cannot contribute this feature at this time.

Proposal Summary

Ability to use compiled and simplified NNF statements in future constraints.

Motivation

I attempted to use bauhaus in an iterative algorithm, where the formulas needed to be compiled to NNF and simplified each time for use in the next iteration. However, I would run into the issue in the next iteration where I would need to combine a formula with bauhaus propositions with a compiled NNF formula, and as it stands you can only add constraints using bauhaus propositions. Below is a simple example of the error:

a = Bauhaus("a")
b = Bauhaus("b")
e.add_constraint(a | b)
# get NNF
f = e.compile()
# attempt to use it again, results in the error: 'And' object has no attribute 'compile'
e.add_constraint(f & (a | b))
e = e.compile()

Describe the solution you'd like
Ideally, the functionality to use either NNF statements or statements with bauhaus propositions (or both) as needed when adding constraints.

Why is it currently difficult to achieve this with Bauhaus?
Bauhaus currently only allows the user to add constraints using statements with bauhaus propositions.

[haz]

Not exactly sure what the right solution is, but do agree that an issue exists for iterative processing. It's more than just adding constraints dynamically, as this would kind of do the same as what's suggested above (but work now):

a = Bauhaus("a")
b = Bauhaus("b")
e.add_constraint(a | b)
e.add_constraint(a | b)
e = e.compile()

I mean, the example on the line e.add_constraint(f & (a | b)) makes it look a little odd (same constraint twice), but the point is you can iteratively add constraints. Where it runs into trouble is when we want to compile, processing, then augment. Specifically, if you just keep combining things, the theory blows up by the end. So you need to simplify at every iteration:

a = Bauhaus("a")
b = Bauhaus("b")
e.add_constraint(a | b)
theory = e.compile()
theory = theory.simplify()
# ?? add some more constraints to theory using bauhaus ??