Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

1 files changed, 8 insertions, 4 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 653eaca8f..b9e951f7b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,9 +213,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 
   // 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);
+  if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){
+    if( !opts.wasSetByUser(options::ceGuidedInst)) {
+      opts.set(options::ceGuidedInst, true);
+    }
+    if( !opts.wasSetByUser(options::dumpSynth)) {
+      opts.set(options::dumpSynth, true);
+    }
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -572,7 +576,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     // make sure out and err streams are flushed too
     *opts[options::out] << flush;
     *opts[options::err] << flush;
- 
+
 #ifdef CVC4_DEBUG
     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
       _exit(returnValue);