touhou-formal/SmtMain.lean at main · N0zoM1z0/touhou-formal · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
import TouhouFormal.Search.SMT

def smtUsage : String :=
  "usage: lake exe smt <th06-sub-oob|th06-find-oob|th07-negative-oob|th08-negative-noop-unsat|th08-positive-oob|th06-jump-minus-one-oob|th07-jump-minus-one-oob|th08-jump-minus-one-oob|th06-timeline-size-before-buffer|th07-timeline-size-before-buffer|th08-timeline-size-before-buffer-unsat|th08-timeline-size-nonprogress|th06-nextoffset-before-buffer|th07-nextoffset-before-buffer|th08-nextoffset-before-buffer|th08-raw-difficulty-override-delta>"

def main (args : List String) : IO UInt32 := do
  match args with
  | ["th06-sub-oob"] =>
      IO.print TouhouFormal.Search.SMT.th06SubTableOobQuery
      return 0
  | ["th06-find-oob"] =>
      IO.print TouhouFormal.Search.SMT.th06FindAnySubTableOobQuery
      return 0
  | ["th07-negative-oob"] =>
      IO.print TouhouFormal.Search.SMT.th07NegativeSubTableOobQuery
      return 0
  | ["th08-negative-noop-unsat"] =>
      IO.print TouhouFormal.Search.SMT.th08NegativeSubTableNoopUnsatQuery
      return 0
  | ["th08-positive-oob"] =>
      IO.print TouhouFormal.Search.SMT.th08PositiveSubTableOobQuery
      return 0
  | ["th06-jump-minus-one-oob"] =>
      IO.print TouhouFormal.Search.SMT.th06JumpMinusOneOobQuery
      return 0
  | ["th07-jump-minus-one-oob"] =>
      IO.print TouhouFormal.Search.SMT.th07JumpMinusOneOobQuery
      return 0
  | ["th08-jump-minus-one-oob"] =>
      IO.print TouhouFormal.Search.SMT.th08JumpMinusOneOobQuery
      return 0
  | ["th06-timeline-size-before-buffer"] =>
      IO.print TouhouFormal.Search.SMT.th06TimelineSizeBeforeBufferQuery
      return 0
  | ["th07-timeline-size-before-buffer"] =>
      IO.print TouhouFormal.Search.SMT.th07TimelineSizeBeforeBufferQuery
      return 0
  | ["th08-timeline-size-before-buffer-unsat"] =>
      IO.print TouhouFormal.Search.SMT.th08TimelineSizeBeforeBufferUnsatQuery
      return 0
  | ["th08-timeline-size-nonprogress"] =>
      IO.print TouhouFormal.Search.SMT.th08TimelineSizeNonProgressQuery
      return 0
  | ["th06-nextoffset-before-buffer"] =>
      IO.print TouhouFormal.Search.SMT.th06RawNextOffsetBeforeBufferQuery
      return 0
  | ["th07-nextoffset-before-buffer"] =>
      IO.print TouhouFormal.Search.SMT.th07RawNextOffsetBeforeBufferQuery
      return 0
  | ["th08-nextoffset-before-buffer"] =>
      IO.print TouhouFormal.Search.SMT.th08RawNextOffsetBeforeBufferQuery
      return 0
  | ["th08-raw-difficulty-override-delta"] =>
      IO.print TouhouFormal.Search.SMT.th08RawDifficultyOverrideDeltaQuery
      return 0
  | _ =>
      IO.eprintln smtUsage
      return 2