src/options/proof_options.toml

   1 id     = "PROOF"
   2 name   = "Proof"
   3
   4 [[option]]
   5   name       = "proofFormatMode"
   6   category   = "regular"
   7   long       = "proof-format-mode=MODE"
   8   type       = "ProofFormatMode"
   9   default    = "NONE"
  10   help       = "select language of proof output"
  11   help_mode  = "Proof format modes."
  12 [[option.mode.NONE]]
  13   name       = "none"
  14   help       = "Do not translate proof output"
  15 [[option.mode.DOT]]
  16   name       = "dot"
  17   help       = "Output DOT proof"
  18 [[option.mode.VERIT]]
  19   name       = "verit"
  20   help       = "Output veriT proof"
  21
  22 [[option]]
  23   name       = "proofPrintConclusion"
  24   category   = "regular"
  25   long       = "proof-print-conclusion"
  26   type       = "bool"
  27   default    = "false"
  28   help       = "Print conclusion of proof steps when printing AST"
  29
  30 [[option]]
  31   name       = "proofPedantic"
  32   category   = "regular"
  33   long       = "proof-pedantic=N"
  34   type       = "uint32_t"
  35   default    = "0"
  36   help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
  37
  38 [[option]]
  39   name       = "proofEagerChecking"
  40   category   = "regular"
  41   long       = "proof-eager-checking"
  42   type       = "bool"
  43   default    = "false"
  44   help       = "check proofs eagerly with proof for local debugging"
  45
  46 [[option]]
  47   name       = "proofGranularityMode"
  48   category   = "regular"
  49   long       = "proof-granularity=MODE"
  50   type       = "ProofGranularityMode"
  51   default    = "THEORY_REWRITE"
  52   help       = "modes for proof granularity"
  53   help_mode  = "Modes for proof granularity."
  54 [[option.mode.OFF]]
  55   name = "off"
  56   help = "Do not improve the granularity of proofs."
  57 [[option.mode.REWRITE]]
  58   name = "rewrite"
  59   help = "Allow rewrite or substitution steps, expand macros."
  60 [[option.mode.THEORY_REWRITE]]
  61   name = "theory-rewrite"
  62   help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
  63 [[option.mode.DSL_REWRITE]]
  64   name = "dsl-rewrite"
  65   help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."