Repository navigation
Conversation
"Starting solver" said nothing about what it started on. On a 256-word, 21-port register file the miter built in four minutes and the solver then ran for over half an hour with nothing more logged: no way to tell a hard problem from a hang, or to compare it with a smaller run. The two existing lines now carry it, without adding a line: Starting solver: <v> variables, <c> clauses, <n> outputs compared SAT solver finished: UNSAT in <s> s SATSolverWrapper counts the clauses it is handed and the largest variable they use. LecLogNamesTheSolverProblemAndItsTime runs an equivalent pair the miter cannot hash away (a & b against ~(~a | ~b)) and reads both lines from the log. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KeplerFormalCliTests.cpp is built by CMake only. MiterTests' LecLogNamesTheSolverProblemAndItsTime runs the binary on AND2 against NAND2 into INV (a tiny inline liberty), an equivalent pair the miter cannot hash away, and reads both solver lines from the log. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
"Starting solver" says nothing about what it started on. On a 256-word, 21-port register file, the miter built in four minutes, then the solver ran for over half an hour with nothing more logged. There was no way to tell a hard problem from a hang, or to compare it with a smaller run.
The two existing lines now carry the problem and the time, without adding a line:
SATSolverWrappercounts the clauses it is handed and the largest variable they use.MiterStrategylog it: the whole design and compact mode.KeplerCliSubprocessTests.LecLogNamesTheSolverProblemAndItsTimeinMiterTestsruns the binary on AND2 against NAND2 into INV, from a tiny inline liberty. That pair is equivalent but can't be hashed away, so the solver runs. The test reads both lines from the log and takes milliseconds.bazel-orfs carries this as a patch for now; it would drop the patch once this merges.
Tested:
bazel test //...passes, including the test above.Correction: an earlier version of this PR put its test in
KeplerFormalCliTests.cpp, which only CMake builds, so it did not run under Bazel. The test now lives inMiterTests. The CMake-side copy is still there; tell me if you'd rather drop it.🤖 Generated with Claude Code