From 9734407cde074c5bc65029548919f4a94f2d905f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Tue, 2 Jun 2015 11:14:59 -0700
Subject: [PATCH] disable throttle on unbounded objectives in shared theories.
 It may violate an interface equality, to fix issue #120

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
---
 src/smt/theory_arith.h     |  1 +
 src/smt/theory_arith_aux.h | 31 ++++++++++++++++++++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index db4b01395..6531c33f2 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -885,6 +885,7 @@ namespace smt {
         void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);
         enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT};
         max_min_t max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared);
+        bool has_interface_equality(theory_var v);
         bool max_min(svector<theory_var> const & vars);
 
         max_min_t max_min(row& r, bool max, bool maintain_integrality, bool& has_shared);
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 91ee6def5..8bf366682 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1545,6 +1545,25 @@ namespace smt {
         return is_tighter;
     }
 
+    /**
+       \brief Check if bound change affects interface equality.
+    */
+    template<typename Ext>
+    bool theory_arith<Ext>::has_interface_equality(theory_var x) {
+        theory_var num = get_num_vars();
+        context& ctx = get_context();
+        enode* r = get_enode(x)->get_root();
+        for (theory_var v = 0; v < num; v++) {
+            if (v == x) continue;
+            enode* n = get_enode(v);
+            if (ctx.is_shared(n) && n->get_root() == r) {
+                return true;
+            }
+        }
+        return false;
+    }
+    
+
     /**
        \brief Maximize (Minimize) the given temporary row.
        Return true if succeeded.
@@ -1660,13 +1679,23 @@ namespace smt {
                     SASSERT(!maintain_integrality || valid_assignment());
                     continue;
                 }
-                if (ctx.is_shared(get_enode(x_j))) {
+#if 0
+                if (ctx.is_shared(get_enode(x_j)) && has_interface_equality(x_j)) {
                     ++best_efforts;
                 }
                 else {
                     SASSERT(unbounded_gain(max_gain));
+                    has_shared = false;
                     best_efforts = 0;
                 }
+#endif
+                //
+                // NB. As it stands this is a possibly unsound conclusion for shared theories.
+                // the tradeoff is non-termination for unbounded objectives in the
+                // presence of sharing.
+                // 
+                has_shared = false;
+                best_efforts = 0;
                 result = UNBOUNDED;
                 break;
             }