Make make test d-DNNF fuzzing fast

`make test` ran the compile fuzzer at 100 cases with up to 16 vars; the oracle
(brute force + model-set + function-model enumeration) is 2^nv, so it took ~21s.

- Add --minvars/--maxvars knobs to ddnnf_fuzz.py (default 7..16 unchanged for
  manual deep runs).
- ctest now runs fewer, smaller cases: compile fuzz 40 @ vars 6..10, synth
  weak0/weak3 30 each.

Total d-DNNF test time ~21s -> ~2.6s for the compile fuzz; whole `make test`
~6.5s. Deep fuzzing is still a manual `ddnnf_fuzz.py 200 [--maxvars N]` away.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: msoos

CLAUDE.md

@@ -81,6 +81,9 @@ python3 tests/ddnnf_fuzz.py 200            # circuit count == true count, model
                                            #   == true models (validates arc literals),
                                            #   strictly decomposable, faithful as a fn
 python3 tests/ddnnf_fuzz.py 200 --seed N   # reproduce a specific run
+python3 tests/ddnnf_fuzz.py 200 --maxvars 14  # cap var count (oracle is 2^nv, so
+                                           #   this is the main runtime/coverage knob;
+                                           #   also --minvars N)
 ```
 
 `ganak --compile out.nnf in.cnf` writes a faithful d-DNNF. `--weak 0` is that

CMakeLists.txt

@@ -565,12 +565,15 @@ if(ENABLE_TESTING)
   # count/model set as an oracle, and check the emitted circuit against it.
   # Seeded so a regression reproduces identically; they self-check against the
   # oracle, so there is no golden file to break when the circuit shape changes.
+  # Small/few by design: the oracle is 2^nv and each case spawns ganak, so we
+  # keep these quick for `make test`. For deep fuzzing run them by hand with a
+  # larger count / --maxvars (see CLAUDE.md).
   add_test(NAME ddnnf_compile_fuzz
-    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_fuzz.py 100 --seed 1)
+    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_fuzz.py 40 --seed 1 --minvars 6 --maxvars 10)
   add_test(NAME ddnnf_synth_weak0
-    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_synth.py 60 --seed 1)
+    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_synth.py 30 --seed 1)
   add_test(NAME ddnnf_synth_weak3
-    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_synth.py 60 --seed 1 --weak 3)
+    COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/tests/ddnnf_synth.py 30 --seed 1 --weak 3)
 endif()
 
 # -----------------------------------------------------------------------------

tests/ddnnf_fuzz.py

@@ -102,17 +102,25 @@ def compile_nnf(path, nnf, weak_level):
 def main():
     n = 200
     seed = random.randrange(1 << 30)
+    minv, maxv = 7, 16    # var-count range; the oracle is 2^nv, so this drives runtime
     args = sys.argv[1:]
     i = 0
     while i < len(args):
         if args[i] == "--seed":
             seed = int(args[i + 1])
             i += 1
+        elif args[i] == "--minvars":
+            minv = int(args[i + 1])
+            i += 1
+        elif args[i] == "--maxvars":
+            maxv = int(args[i + 1])
+            i += 1
         else:
             n = int(args[i])
         i += 1
+    minv = min(minv, maxv)
     random.seed(seed)
-    print(f"seed={seed} tests={n} mode=STRONG")
+    print(f"seed={seed} tests={n} vars={minv}..{maxv} mode=STRONG")
 
     fails = 0
 
@@ -129,7 +137,7 @@ def save_fail(t):
             shutil.copy(clean, unique_file("fail", ".clean.nnf"))
 
     for t in range(n):
-        nv = random.randint(7, 16)
+        nv = random.randint(minv, maxv)
         nc = random.randint(nv, nv * 4)
         k = random.choice([2, 3, 3, 4])
         clauses = gen_cnf(nv, nc, k)