Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit.

2 files changed, 51 insertions, 0 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 242e018f6..1c7c1d171 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1187,6 +1187,44 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
   return "get-instantiations";
 }
 
+/* class GetSynthSolutionCommand */
+
+GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
+}
+
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_smtEngine = smtEngine;
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    d_smtEngine->printSynthSolution(out);
+  }
+}
+
+Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+Command* GetSynthSolutionCommand::clone() const {
+  GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+std::string GetSynthSolutionCommand::getCommandName() const throw() {
+  return "get-instantiations";
+}
+
 /* class GetUnsatCoreCommand */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index cfa00bff4..9165961fb 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -610,6 +610,19 @@ public:
   std::string getCommandName() const throw();
 };/* class GetInstantiationsCommand */
 
+class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
+protected:
+  SmtEngine* d_smtEngine;
+public:
+  GetSynthSolutionCommand() throw();
+  ~GetSynthSolutionCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class GetSynthSolutionCommand */
+
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
   UnsatCore d_result;