Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.

12 files changed, 146 insertions, 32 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8ffb47e40..ebfc7266b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -187,16 +187,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
   }
 
-  // if doing sygus, turn on CEGQI by default
-  if(opts.getInputLanguage() == language::input::LANG_SYGUS ){
-    if( !opts.wasSetByUserCeGuidedInst()) {
-      opts.setCeGuidedInst(true);
-    }
-    if( !opts.wasSetByUserDumpSynth()) {
-      opts.setDumpSynth(true);
-    }
-  }
-
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&CVC4::null_os);
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index ff889bcb2..54027c128 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -252,6 +252,7 @@ liboptions_la_SOURCES = \
 	set_language.h \
 	simplification_mode.cpp \
 	simplification_mode.h \
+	sygus_out_mode.h \
 	theoryof_mode.cpp \
 	theoryof_mode.h \
 	ufss_mode.h
diff --git a/src/options/options.h b/src/options/options.h
index f93663095..474ef0f96 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -242,8 +242,6 @@ public:
 
 
   // TODO: Document these.
-  void setCeGuidedInst(bool);
-  void setDumpSynth(bool);
   void setInputLanguage(InputLanguage);
   void setInteractive(bool);
   void setOut(std::ostream*);
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 351c8b608..3d74091fd 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -554,7 +554,6 @@ all \n\
 \n\
 ";
 
-
 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -1311,6 +1310,56 @@ SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option
   }
 }
 
+const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
+    "\
+Modes for finite model finding bound minimization, supported by --sygus-out:\n\
+\n\
+status \n\
++ Print only status for check-synth calls.\n\
+\n\
+status-and-def (default) \n\
++ Print status followed by definition corresponding to solution.\n\
+\n\
+status-or-def \n\
++ Print status if infeasible, or definition corresponding to\n\
+  solution if feasible.\n\
+\n\
+sygus-standard \n\
++ Print based on SyGuS standard.\n\
+\n\
+";
+
+SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
+    std::string option, std::string optarg) throw(OptionException)
+{
+  if (optarg == "status")
+  {
+    return SYGUS_SOL_OUT_STATUS;
+  }
+  else if (optarg == "status-and-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_AND_DEF;
+  }
+  else if (optarg == "status-or-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_OR_DEF;
+  }
+  else if (optarg == "sygus-standard")
+  {
+    return SYGUS_SOL_OUT_STANDARD;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusSolutionOutModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --sygus-out: `")
+                          + optarg
+                          + "'.  Try --sygus-out help.");
+  }
+}
 
 void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
   options::produceAssertions.set(value);
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index c525c9e0e..9d5f8cc6e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -28,14 +28,15 @@
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_handlers.h"
 #include "options/bv_bitblast_mode.h"
-#include "options/decision_mode.h"
 #include "options/datatypes_modes.h"
+#include "options/decision_mode.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_modes.h"
 #include "options/simplification_mode.h"
+#include "options/sygus_out_mode.h"
 #include "options/theoryof_mode.h"
 #include "options/ufss_mode.h"
 
@@ -143,6 +144,8 @@ public:
   void notifyBeforeSearch(const std::string& option) throw(ModalException);
   void notifyDumpMode(std::string option) throw(OptionException);
   SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
+  SygusSolutionOutMode stringToSygusSolutionOutMode(
+      std::string option, std::string optarg) throw(OptionException);
   void setProduceAssertions(std::string option, bool value) throw();
   void proofEnabledBuild(std::string option, bool value) throw(OptionException);
   void LFSCEnabledBuild(std::string option, bool value);
@@ -218,6 +221,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 7d71c267a..b8db9d9da 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -241,13 +241,6 @@ std::ostream* Options::currentGetOut() {
 
 
 // TODO: Document these.
-void Options::setCeGuidedInst(bool value) {
-  set(options::ceGuidedInst, value);
-}
-
-void Options::setDumpSynth(bool value) {
-  set(options::dumpSynth, value);
-}
 
 void Options::setInputLanguage(InputLanguage value) {
   set(options::inputLanguage, value);
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index ba7c8338a..c92813bf4 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -246,7 +246,7 @@ option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3
 ### synthesis options 
 
 option ceGuidedInst --cegqi bool :default false :read-write
-  counterexample-guided quantifier instantiation
+  counterexample-guided quantifier instantiation for sygus
 option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
   mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false
diff --git a/src/options/smt_options b/src/options/smt_options
index 00424e103..c701d5c20 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -39,6 +39,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
+option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
+  output mode for sygus
 option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h
new file mode 100644
index 000000000..9f94be27f
--- /dev/null
+++ b/src/options/sygus_out_mode.h
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file sygus_out_mode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Options for sygus solution output.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H
+#define __CVC4__SMT__SYGUS_OUT_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/** Mode for printing sygus solutions. */
+enum SygusSolutionOutMode
+{
+  /** print status */
+  SYGUS_SOL_OUT_STATUS,
+  /** (default) print status and solution */
+  SYGUS_SOL_OUT_STATUS_AND_DEF,
+  /** print status if infeasible, or solution if feasible */
+  SYGUS_SOL_OUT_STATUS_OR_DEF,
+  /** print output specified by sygus standard */
+  SYGUS_SOL_OUT_STANDARD,
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 8012c868c..fee109923 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -383,8 +383,8 @@ CheckSynthCommand::CheckSynthCommand() throw() :
   d_expr() {
 }
 
-CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
-  d_expr(expr), d_inUnsatCore(inUnsatCore) {
+CheckSynthCommand::CheckSynthCommand(const Expr& expr) throw() :
+  d_expr(expr) {
 }
 
 Expr CheckSynthCommand::getExpr() const throw() {
@@ -395,6 +395,33 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSynth(d_expr);
     d_commandStatus = CommandSuccess::instance();
+    smt::SmtScope scope(smtEngine);
+    d_solution.clear();
+    // check whether we should print the status
+    if (d_result.asSatisfiabilityResult() != Result::UNSAT
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS_AND_DEF
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS)
+    {
+      if (options::sygusOut() == SYGUS_SOL_OUT_STANDARD)
+      {
+        d_solution << "(fail)" << endl;
+      }
+      else
+      {
+        d_solution << d_result << endl;
+      }
+    }
+    // check whether we should print the solution
+    if (d_result.asSatisfiabilityResult() == Result::UNSAT
+        && options::sygusOut() != SYGUS_SOL_OUT_STATUS)
+    {
+      // printing a synthesis solution is a non-constant
+      // method, since it invokes a sophisticated algorithm
+      // (Figure 5 of Reynolds et al. CAV 2015).
+      // Hence, we must call here print solution here,
+      // instead of during printResult.
+      smtEngine->printSynthSolution(d_solution);
+    }
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -408,18 +435,18 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    out << d_result << endl;
+    out << d_solution.str();
   }
 }
 
 Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSynthCommand::clone() const {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr);
   c->d_result = d_result;
   return c;
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index f5be9ddfe..a60c85a3c 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -529,13 +529,9 @@ public:
 };/* class QueryCommand */
 
 class CVC4_PUBLIC CheckSynthCommand : public Command {
-protected:
-  Expr d_expr;
-  Result d_result;
-  bool d_inUnsatCore;
 public:
   CheckSynthCommand() throw();
-  CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
+  CheckSynthCommand(const Expr& expr) throw();
   ~CheckSynthCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine);
@@ -544,6 +540,14 @@ public:
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
+
+ protected:
+  /** the assertion of check-synth */
+  Expr d_expr;
+  /** result of the check-synth call */
+  Result d_result;
+  /** string stream that stores the output of the solution */
+  std::stringstream d_solution;
 };/* class CheckSynthCommand */
 
 // this is TRANSFORM in the CVC presentation language
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f93d8bd7f..2ff115606 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1294,6 +1294,13 @@ void SmtEngine::setDefaults() {
     options::bitvectorDivByZeroConst.set(options::inputLanguage()
                                          == language::input::LANG_SMTLIB_V2_6);
   }
+  if (options::inputLanguage() == language::input::LANG_SYGUS)
+  {
+    if (!options::ceGuidedInst.wasSetByUser())
+    {
+      options::ceGuidedInst.set(true);
+    }
+  }
 
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());