From 9d1852343c47ca6abd05752a60650f521bf399e4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 23 Jun 2017 16:34:38 -0700
Subject: [PATCH] add separate get-objectives command #1107

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  3 +--
 src/opt/opt_cmds.cpp            | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index af16f5796..d252c3629 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1360,7 +1360,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             throw ex;
         }
         catch (z3_exception & ex) {
-            get_opt()->display_assignment(regular_stream());
             throw cmd_exception(ex.msg());
         }
         if (m_processing_pareto && r != l_true) {
@@ -1398,7 +1397,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     validate_check_sat_result(r);
     if (was_opt && r != l_false && !m_processing_pareto) {
-        get_opt()->display_assignment(regular_stream());
+        // get_opt()->display_assignment(regular_stream());
     }
 
     if (r == l_true && m_params.m_dump_models) {
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index a5c163562..0264a6a24 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -143,12 +143,35 @@ public:
     }
 };
 
+class get_objectives_cmd : public cmd {
+    opt::context* m_opt;
+public:
+    get_objectives_cmd(opt::context* opt):
+        cmd("get-objectives"),
+        m_opt(opt)
+    {}
+    
+    virtual void reset(cmd_context & ctx) { }
+    virtual char const * get_usage() const { return "(get-objectives)"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; }
+    virtual unsigned get_arity() const { return 0; }
+    virtual void prepare(cmd_context & ctx) {}
 
 
+    virtual void failure_cleanup(cmd_context & ctx) {
+        reset(ctx);
+    }
+
+    virtual void execute(cmd_context & ctx) {
+        get_opt(ctx, m_opt).display_assignment(ctx.regular_stream());        
+    }
+};
+
 void install_opt_cmds(cmd_context & ctx, opt::context* opt) {
     ctx.insert(alloc(assert_soft_cmd, opt));
     ctx.insert(alloc(min_maximize_cmd, true, opt));
     ctx.insert(alloc(min_maximize_cmd, false, opt));
+    ctx.insert(alloc(get_objectives_cmd, opt));
 }