Move non-stream options out of `printer_options.toml` (#8909)

[cvc5.git] / src / options / quantifiers_options.toml

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 8ee7eebf63d15ac8efa6da0a7c5a794181731860..b5147d1b7090bda2f9178f41f1fdcea846f3d771 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -448,6 +448,29 @@ name   = "Quantifiers"
   default    = "2"
   help       = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
 
+[[option]]
+  name       = "printInstMode"
+  category   = "common"
+  long       = "print-inst=MODE"
+  type       = "PrintInstMode"
+  default    = "LIST"
+  help       = "print format for printing instantiations"
+  help_mode  = "Print format for printing instantiations."
+[[option.mode.LIST]]
+  name = "list"
+  help = "Print the list of instantiations per quantified formula, when non-empty."
+[[option.mode.NUM]]
+  name = "num"
+  help = "Print the total number of instantiations per quantified formula, when non-zero."
+
+[[option]]
+  name       = "printInstFull"
+  category   = "regular"
+  long       = "print-inst-full"
+  type       = "bool"
+  default    = "true"
+  help       = "print instantiations for formulas that do not have given identifiers"
+
 [[option]]
   name       = "instMaxLevel"
   category   = "expert"
@@ -833,6 +856,24 @@ name   = "Quantifiers"
   default    = "false"
   help       = "support SyGuS commands"
 
+[[option]]
+  name       = "sygusOut"
+  category   = "regular"
+  long       = "sygus-out=MODE"
+  type       = "SygusSolutionOutMode"
+  default    = "STANDARD"
+  help       = "output mode for sygus"
+  help_mode  = "Modes for sygus solution output."
+[[option.mode.STATUS]]
+  name = "status"
+  help = "Print only status for check-synth calls."
+[[option.mode.STATUS_AND_DEF]]
+  name = "status-and-def"
+  help = "Print status followed by definition corresponding to solution."
+[[option.mode.STANDARD]]
+  name = "sygus-standard"
+  help = "Print based on SyGuS standard."
+
 [[option]]
   name       = "cegqiSingleInvMode"
   category   = "regular"