YosysHQ / imctk

Incremental Model Checking Toolkit
Other
5 stars 2 forks source link

Traits for Boolean negation #7

Closed jix closed 1 month ago

jix commented 2 months ago

Currently the little code that generically handles Boolean negation does so by using std::ops::BitXor<Pol> instances. While such types should implement various std::ops trait to support using operators for (conditional) Boolean negation, having specific imctk provided traits for this would make generic code quite a bit simpler than with only the std::ops traits.

There are some unresolved questions on how to best design the trait or the traits to handle all of:

Reducing the number of traits that cover these operations would be nice, but having the traits too coarse grained may have us ending up with types can only support part of the operations of one of the involved traits. We should be able to use the fact that obtaining a negated copy only makes sense for types implementing Clone and conversely that having a Clone implementation available allows implementing some of these operations in terms of others.

Another aspect to take into consideration is to make sure that negation can be lifted to reference types, collections or other generic types without running into overlap or coherence issues that would prevent those trait implementations.