|
|
|
|
|
|
by hackerblues
721 days ago
|
|
|
I'd be interested to know if you might be able to if you could find problems by looking at invariants over partitions of the space. Like Is the number of solutions with v1=false plus the number with v1=true the number with v1 free? If we have n constraints then there 2*n variants where you negate subsets of constraints. Is the sum of solution counts over the 2*n subproblems equal the size of the variable space? |
|
|
The search method is propagate constraints for a while then pick a variable and bisect it, solve each side and combine.
Generalising slightly from your suggestion, varying the order in which the search runs, and whether various propagations or optimisations are active, should only change runtime and not the set of results.
The other thing I've discovered since that project is clang's AST based branch coverage recording. Getting to the point where smallish unit tests that can be perturbed as above or enumerated exercise each path through the solver would probably shake out the bugs.