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 [[option.mode.TPTP]]
  22   name       = "tptp"
  23   help       = "Output TPTP proof (work in progress)"
  24
  25 [[option]]
  26   name       = "proofPrintConclusion"
  27   category   = "regular"
  28   long       = "proof-print-conclusion"
  29   type       = "bool"
  30   default    = "false"
  31   help       = "Print conclusion of proof steps when printing AST"
  32
  33 [[option]]
  34   name       = "proofPedantic"
  35   category   = "regular"
  36   long       = "proof-pedantic=N"
  37   type       = "uint64_t"
  38   default    = "0"
  39   help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
  40
  41 [[option]]
  42   name       = "proofCheck"
  43   category   = "regular"
  44   long       = "proof-check=MODE"
  45   type       = "ProofCheckMode"
  46   default    = "LAZY"
  47   help       = "select proof checking mode"
  48   help_mode  = "Proof checking modes."
  49 [[option.mode.EAGER]]
  50   name       = "eager"
  51   help       = "check rule applications and proofs from generators eagerly for local debugging"
  52 [[option.mode.EAGER_SIMPLE]]
  53   name       = "eager-simple"
  54   help       = "check rule applications during construction"
  55 [[option.mode.LAZY]]
  56   name       = "lazy"
  57   help       = "check rule applications only during final proof construction"
  58 [[option.mode.NONE]]
  59   name       = "none"
  60   help       = "do not check rule applications"
  61
  62 [[option]]
  63   name       = "proofGranularityMode"
  64   category   = "regular"
  65   long       = "proof-granularity=MODE"
  66   type       = "ProofGranularityMode"
  67   default    = "THEORY_REWRITE"
  68   help       = "modes for proof granularity"
  69   help_mode  = "Modes for proof granularity."
  70 [[option.mode.OFF]]
  71   name = "off"
  72   help = "Do not improve the granularity of proofs."
  73 [[option.mode.REWRITE]]
  74   name = "rewrite"
  75   help = "Allow rewrite or substitution steps, expand macros."
  76 [[option.mode.THEORY_REWRITE]]
  77   name = "theory-rewrite"
  78   help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
  79 [[option.mode.DSL_REWRITE]]
  80   name = "dsl-rewrite"
  81   help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."