sygus input language and benchmark

1 files changed, 10 insertions, 0 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9035ed8b8..c011671f8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -34,6 +34,7 @@
 #include "expr/command.h"
 #include "util/configuration.h"
 #include "options/options.h"
+#include "theory/quantifiers/options.h"
 #include "main/command_executor.h"
 
 #ifdef PORTFOLIO_BUILD
@@ -198,6 +199,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
         opts.set(options::inputLanguage, language::input::LANG_CVC4);
+      } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
+                || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
+        opts.set(options::inputLanguage, language::input::LANG_SYGUS);
       }
     }
   }
@@ -206,6 +210,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
   }
 
+  // if doing sygus, turn on CEGQI by default
+  if(opts[options::inputLanguage] == language::input::LANG_SYGUS &&
+     !opts.wasSetByUser(options::ceGuidedInst)) {
+    opts.set(options::ceGuidedInst, true);
+  }
+
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(CVC4::null_os);