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.

8 files changed, 98 insertions, 12 deletions

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 */