I suggest adding some functionality that allows you to cleanly create custom constraints using the annotated objects. The functions provided with the library are incredibly useful, but trying to create custom constraints (even something as simple as negating a proposition) is clunky. Currently it seems like the only way to do it is to take care of the "abstract" annotated constraints first, then convert the theory to an NNF object and add extra constraints manually with an endless string of "&"s. Every proposition also has to be casted to an NNF variable, leading to a lot of verbose syntax for relatively simple statements.
I suggest adding some functionality that allows you to cleanly create custom constraints using the annotated objects. The functions provided with the library are incredibly useful, but trying to create custom constraints (even something as simple as negating a proposition) is clunky. Currently it seems like the only way to do it is to take care of the "abstract" annotated constraints first, then convert the theory to an NNF object and add extra constraints manually with an endless string of "&"s. Every proposition also has to be casted to an NNF variable, leading to a lot of verbose syntax for relatively simple statements.