feat: Convert Circuit to AIG, which will then be passed to cadical for bitblasting #952
+449
−79
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This uses 'shareCommon' to allow us to print the pointer-location of arbitrary lean variables as a cheap way to identify variables. Actually plumbing a [ToString a] instance throughout the entire machinery will be a bit too nightmarish for me to contemplate. This also lets me test out the technique, in case I want to reuse it to automatically fold our circuits into a DAG and prove this version to be equivalent to the slow tree version. These games that people play have sharp edges, so we should only go down this route if it turns out that 'eval' is the bottleneck.
bollu
changed the title
|
Alive Statistics: 90 / 93 (3 failed) |
…rough It's really now clear how painful plumbing a [Hashable a] through the entirity of the thousand line FiniteStateMachine.lean will be. God protect my soul.
Now I must perform the unenviable task of finding out which modules bv_decide needs to correctly invoke cadical.
> uncaught exception: auxiliary declaration cannot be created when declaration name is not available
bollu@ultrapower ~/n/b/ssa (circuit-to-aig-to-cnf-to-cadical) lake build bv-circuit-profile && ./.lake/build/bin/bv-circuit-profile
Predicate.eq
(Term.add
(Term.sub (Term.neg (Term.not (Term.xor (Term.var 0) (Term.var 1)))) (Term.shiftL (Term.var 1) 1))
(Term.not (Term.var 0)))
(Term.sub
(Term.neg (Term.not (Term.or (Term.var 0) (Term.not (Term.var 1)))))
(Term.add (Term.and (Term.var 0) (Term.var 1)) (Term.shiftL (Term.and (Term.var 0) (Term.var 1)) 1)))
Iteration #1
(pure) is all zeroes: 'true' | time: '1315' ms
(cadical) is all zeroes: 'true' | time: '307' ms
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This tests the ability of our infrastructure to switch over to AIG, and should also provide a fairly hefty speedup by querying a SAT solver for the expensive check. Based off of #950 which adds files that this PR builds on.
Currently a draft as the AIG builder is half-done.