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.

1 files changed, 9 insertions, 5 deletions

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