X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Foptions%2Fquantifiers_options.toml;h=b5147d1b7090bda2f9178f41f1fdcea846f3d771;hb=288ad5358ef79097f35a656def614c664006d6b9;hp=8ee7eebf63d15ac8efa6da0a7c5a794181731860;hpb=c898b0ec2144cae0515625f95cc6e05abe2fa186;p=cvc5.git

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 8ee7eebf6..b5147d1b7 100644
--- 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"