mirror of
https://github.com/Z3Prover/z3
synced 2025-09-03 00:28:06 +00:00
12 lines
No EOL
377 B
Text
12 lines
No EOL
377 B
Text
More focused (_FOCUS_ == 2) WalkSAT version.
|
|
Variables are chosen among candidates in only one unsatisfied bit-vector term.
|
|
Flip rate slightly slower; probably due to larger hash-table and recursive formula structure.
|
|
No restarts.
|
|
|
|
#define _CNF_ 0
|
|
#define _BFS_ 1
|
|
#define _FOCUS_ 3
|
|
#define _RESTARTS_ 0
|
|
#define _TIMELIMIT_ 300
|
|
#define _SCORE_AND_AVG_ 0
|
|
#define _SCORE_OR_MUL_ 0 |