From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 Jul 2018 02:42:55 +0000 (-0500)
Subject: sygusComp2018: update sygus-related options setting in smt engine (#2108)
X-Git-Tag: cvc5-1.0.0~4923
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76d03115cfcade000a9fd18ff9ba7008636eb662;p=cvc5.git

sygusComp2018: update sygus-related options setting in smt engine (#2108)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 53ea9fd58..22916e354 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1292,8 +1292,10 @@ void SmtEngine::setDefaults() {
     options::bitvectorDivByZeroConst.set(
         language::isInputLang_smt2_6(options::inputLanguage()));
   }
+  bool is_sygus = false;
   if (options::inputLanguage() == language::input::LANG_SYGUS)
   {
+    is_sygus = true;
     if (!options::ceGuidedInst.wasSetByUser())
     {
       options::ceGuidedInst.set(true);
@@ -1303,17 +1305,14 @@ void SmtEngine::setDefaults() {
     {
       options::cbqiMidpoint.set(true);
     }
-    // do not assign function values (optimization)
-    if (!options::assignFunctionValues.wasSetByUser())
+    if (options::sygusRepairConst())
     {
-      options::assignFunctionValues.set(false);
+      if (!options::cbqi.wasSetByUser())
+      {
+        options::cbqi.set(true);
+      }
     }
   }
-  else
-  {
-    // cannot use sygus repair constants
-    options::sygusRepairConst.set(false);
-  }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
   {
@@ -1603,7 +1602,7 @@ void SmtEngine::setDefaults() {
   // cases where we need produce models
   if (!options::produceModels()
       && (options::produceAssignments() || options::sygusRewSynthCheck()
-          || options::sygusRepairConst()))
+          || is_sygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));