From 11fee1c8d0120d4c02140aef3973be9c8f2e43e2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 10 Oct 2014 14:57:39 -0700
Subject: [PATCH] fix opb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/shell/main.cpp         | 10 +++++-----
 src/shell/opt_frontend.cpp | 26 +++++++++++++++++++-------
 2 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 10fc916ca..2a8ed5022 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -36,7 +36,7 @@ Revision History:
 #include"gparams.h"
 #include"env_params.h"
 
-typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_PBO, IN_Z3_LOG } input_kind;
+typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG } input_kind;
 
 std::string         g_aux_input_file;
 char const *        g_input_file          = 0;
@@ -173,7 +173,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
                 g_input_kind = IN_WCNF;
             }
             else if (strcmp(opt_name, "bpo") == 0) {
-                g_input_kind = IN_PBO;
+                g_input_kind = IN_OPB;
             }
             else if (strcmp(opt_name, "log") == 0) {
                 g_input_kind = IN_Z3_LOG;
@@ -316,8 +316,8 @@ int main(int argc, char ** argv) {
                 else if (strcmp(ext, "wcnf") == 0) {
                     g_input_kind = IN_WCNF;
                 }
-                else if (strcmp(ext, "pbo") == 0) {
-                    g_input_kind = IN_PBO;
+                else if (strcmp(ext, "opb") == 0) {
+                    g_input_kind = IN_OPB;
                 }
                 else if (strcmp(ext, "log") == 0) {
                     g_input_kind = IN_Z3_LOG;
@@ -344,7 +344,7 @@ int main(int argc, char ** argv) {
         case IN_WCNF:
             return_value = parse_opt(g_input_file, true);
             break;
-        case IN_PBO:
+        case IN_OPB:
             return_value = parse_opt(g_input_file, false);
             break;
         case IN_DATALOG:
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 5269f51bc..566a2c911 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -8,10 +8,8 @@
 #include"timeout.h"
 #include"reg_decl_plugins.h"
 
-static bool g_display_statistics = false;
+extern bool g_display_statistics;
 static bool g_first_interrupt = true;
-static int g_timeout = 0;
-static bool g_display_model = false;
 static opt::context* g_opt = 0;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
@@ -143,7 +141,10 @@ public:
                     opt.add_hard_constraint(cls);
                 }
                 else {
-                    opt.add_soft_constraint(cls, rational(weight), symbol::null);
+                    unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
+                    if (g_handles.empty()) {
+                        g_handles.push_back(id);
+                    }
                 }
             }
         }
@@ -255,9 +256,16 @@ static void display_statistics() {
         g_opt->collect_statistics(stats);
         stats.display(std::cout);
         double end_time = static_cast<double>(clock());
-        std::cout << "time:   " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n";
+        std::cout << "time:                " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n";
         for (unsigned i = 0; i < g_handles.size(); ++i) {
-            std::cout << "  [" << g_opt->get_lower(g_handles[i]) << ":" << g_opt->get_upper(g_handles[i]) << "]\n";
+            expr_ref lo = g_opt->get_lower(g_handles[i]);
+            expr_ref hi = g_opt->get_upper(g_handles[i]);
+            if (lo == hi) {
+                std::cout << "   " << lo << "\n";
+            }
+            else {
+                std::cout << "  [" << lo << ":" << hi << "]\n";
+            }
         }
     }    
 }
@@ -302,7 +310,11 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
         opb.parse();
     }
     lbool r = opt.optimize();
-    std::cout << r << "\n";
+    switch (r) {
+    case l_true: std::cout << "sat\n"; break;
+    case l_false: std::cout << "unsat\n"; break;
+    case l_undef: std::cout << "unknown\n"; break;
+    }
     #pragma omp critical (g_display_stats) 
     {
         display_statistics();