Henrik Böving 5a5e83c26c refactor: the AIG framework to track negations in a more efficient way (#7381) ... This PR refactors the AIG datastructures that underly bv_decide in order to allow a better tracking of negations in the circuit. This refactor has two effects, for one adding full constant folding to the AIG framework and secondly enabling us to add further simplifications from the Brummayer Biere paper in the future which was previously architecturally impossible.		2025-03-17 17:33:49 +00:00
..
BVDecide	refactor: the AIG framework to track negations in a more efficient way (#7381)	2025-03-17 17:33:49 +00:00
BVDecide.lean	feat: import LeanSAT's tactic frontends	2024-08-28 18:14:39 +02:00