From 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 5 Nov 2018 16:50:48 -0600
Subject: Change default sygus enumeration mode to auto (#2689)

---
 src/options/options_handler.cpp      | 7 +++++++
 src/options/quantifiers_modes.h      | 2 ++
 src/options/quantifiers_options.toml | 4 ++--
 3 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'src/options')

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e4c0276ea..565f28334 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -538,6 +538,9 @@ enum  \n\
 var-agnostic \n\
 + Use sygus solver to enumerate terms that are agnostic to variables. \n\
 \n\
+auto (default) \n\
++ Internally decide the best policy for each enumerator. \n\
+\n\
 ";
 
 const std::string OptionsHandler::s_macrosQuantHelp = "\
@@ -987,6 +990,10 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option,
   {
     return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
   }
+  else if (optarg == "auto")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO;
+  }
   else if (optarg == "help")
   {
     puts(s_sygusActiveGenHelp.c_str());
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 392393a91..05388cdf6 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -272,6 +272,8 @@ enum SygusActiveGenMode
   SYGUS_ACTIVE_GEN_ENUM,
   /** use variable-agnostic enumerators */
   SYGUS_ACTIVE_GEN_VAR_AGNOSTIC,
+  /** internally decide the best policy for each enumerator */
+  SYGUS_ACTIVE_GEN_AUTO,
 };
 
 enum MacrosQuantMode {
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 0b28c6a27..c555c37bf 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1044,7 +1044,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-active-gen=MODE"
   type       = "CVC4::theory::quantifiers::SygusActiveGenMode"
-  default    = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE"
+  default    = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO"
   handler    = "stringToSygusActiveGenMode"
   includes   = ["options/quantifiers_modes.h"]
   read_only  = true
@@ -1135,7 +1135,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-pbe-multi-fair"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
 
 [[option]]
-- 
cgit v1.2.3