updates to resource exceptions, update master possibly handle pull request issue

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/normal_forms/nnf.cpp

@@ -373,7 +373,7 @@ struct nnf::imp {
         if (memory::get_allocation_size() > m_max_memory)
             throw nnf_exception(Z3_MAX_MEMORY_MSG);
         if (m().canceled()) 
-            throw nnf_exception(Z3_CANCELED_MSG);
+            throw nnf_exception(m().limit().get_cancel_msg());
     }
 
     void set_new_child_flag() {

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -28,7 +28,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
     if (memory::get_allocation_size() > m_max_memory)
         throw rewriter_exception(Z3_MAX_MEMORY_MSG);
     if (m().canceled())
-        throw rewriter_exception(Z3_CANCELED_MSG);
+        throw rewriter_exception(m().limit().get_cancel_msg());
     cooperate("bit-blaster");
 }
 

src/qe/qe.cpp

@@ -2051,7 +2051,7 @@ namespace qe {
                 
         void checkpoint() {
             if (m.canceled()) 
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             cooperate("qe");
         }
 

src/qe/qe_lite.cpp

@@ -738,7 +738,7 @@ namespace eq {
         void checkpoint() {
             cooperate("der");
             if (m.canceled()) 
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
         }
 
     public:
@@ -917,8 +917,8 @@ namespace ar {
         void checkpoint() {
             cooperate("der");
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
-        }
+                throw tactic_exception(m.limit().get_cancel_msg());
+    }
 
     public:
 
@@ -2207,7 +2207,7 @@ namespace fm {
         void checkpoint() {
             cooperate("fm");
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
         }
     public:
 
@@ -2477,7 +2477,7 @@ class qe_lite_tactic : public tactic {
 
         void checkpoint() {
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             cooperate("qe-lite");
         }
         

src/qe/qe_sat_tactic.cpp

@@ -662,7 +662,7 @@ namespace qe {
 
         void checkpoint() {
             if (m.canceled()) {
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             }
             cooperate("qe-sat");
         }

src/qe/qe_tactic.cpp

@@ -45,7 +45,7 @@ class qe_tactic : public tactic {
 
         void checkpoint() {
             if (m.canceled()) 
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             cooperate("qe");
         }
 

src/sat/tactic/goal2sat.cpp

@@ -333,7 +333,7 @@ struct goal2sat::imp {
         loop:
             cooperate("goal2sat");
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             if (memory::get_allocation_size() > m_max_memory)
                 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
             frame & fr = m_frame_stack.back();
@@ -626,7 +626,7 @@ struct sat2goal::imp {
 
     void checkpoint() {
         if (m.canceled())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
     }

src/smt/smt_model_finder.cpp

@@ -3318,7 +3318,7 @@ namespace smt {
     void model_finder::checkpoint(char const* msg) {
         cooperate(msg);
         if (m_context && m_context->get_cancel_flag())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m_context->get_manager().limit().get_cancel_msg());
     }
 
     mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const {

src/smt/tactic/unit_subsumption_tactic.cpp

@@ -58,7 +58,7 @@ struct unit_subsumption_tactic : public tactic {
     
     void checkpoint() {
         if (m.canceled()) {
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
         }
     }
 

src/smt/theory_seq.cpp

@@ -86,6 +86,13 @@ void theory_seq::solution_map::display(std::ostream& out) const {
     }
 }
 
+bool theory_seq::exclusion_table::contains(expr* e, expr* r) const {
+    if (e->get_id() > r->get_id()) {
+        std::swap(e, r);
+    }
+    return m_table.contains(std::make_pair(e, r));
+}
+
 void theory_seq::exclusion_table::update(expr* e, expr* r) {
     if (e->get_id() > r->get_id()) {
         std::swap(e, r);

src/smt/theory_seq.h

@@ -81,9 +81,7 @@ namespace smt {
             ~exclusion_table() { }
             bool empty() const { return m_table.empty(); }
             void update(expr* e, expr* r);
-            bool contains(expr* e, expr* r) {
-                return m_table.contains(std::make_pair(e, r));
-            }
+            bool contains(expr* e, expr* r) const;
             void push_scope() { m_limit.push_back(m_lhs.size()); }
             void pop_scope(unsigned num_scopes);
             void display(std::ostream& out) const;            

src/tactic/aig/aig.cpp

@@ -131,7 +131,7 @@ struct aig_manager::imp {
         if (memory::get_allocation_size() > m_max_memory)
             throw aig_exception(TACTIC_MAX_MEMORY_MSG);
         if (m().canceled())
-            throw aig_exception(TACTIC_CANCELED_MSG);
+            throw aig_exception(m().limit().get_cancel_msg());
         cooperate("aig");
     }
 

src/tactic/arith/arith_bounds_tactic.cpp

@@ -37,7 +37,7 @@ struct arith_bounds_tactic : public tactic {
     
     void checkpoint() {
         if (m.canceled()) {
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
         }
     }
     

src/tactic/arith/degree_shift_tactic.cpp

@@ -100,7 +100,7 @@ class degree_shift_tactic : public tactic {
 
         void checkpoint() {
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             cooperate("degree_shift");
         }
 

src/tactic/arith/diff_neq_tactic.cpp

@@ -289,7 +289,7 @@ class diff_neq_tactic : public tactic {
             unsigned nvars = num_vars();
             while (m_stack.size() < nvars) {
                 if (m.canceled())
-                    throw tactic_exception(TACTIC_CANCELED_MSG);
+                    throw tactic_exception(m.limit().get_cancel_msg());
                 TRACE("diff_neq_tactic", display_model(tout););
                 var x = m_stack.size();
                 if (extend_model(x))

src/tactic/arith/fm_tactic.cpp

@@ -197,7 +197,7 @@ class fm_tactic : public tactic {
                 clauses::iterator it  = m_clauses[i].begin();
                 clauses::iterator end = m_clauses[i].end();
                 for (; it != end; ++it) {
-                    if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG);
+                    if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg());
                     switch (process(x, *it, u, ev, val)) {
                     case NONE: 
                         TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
@@ -1543,7 +1543,7 @@ class fm_tactic : public tactic {
         void checkpoint() {
             cooperate("fm");
             if (m.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m.limit().get_cancel_msg());
             if (memory::get_allocation_size() > m_max_memory)
                 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         }

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -176,7 +176,7 @@ struct bv_size_reduction_tactic::imp {
     
     void checkpoint() {
         if (m.canceled())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
     }
     
     void operator()(goal & g, model_converter_ref & mc) {

src/tactic/bv/bvarray2uf_tactic.cpp

@@ -50,7 +50,7 @@ class bvarray2uf_tactic : public tactic {
 
         void checkpoint() {
             if (m_manager.canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+                throw tactic_exception(m_manager.limit().get_cancel_msg());
         }
 
         void operator()(goal_ref const & g,

src/tactic/core/cofactor_elim_term_ite.cpp

@@ -36,7 +36,7 @@ struct cofactor_elim_term_ite::imp {
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         if (m.canceled())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
     }
 
     // Collect atoms that contain term if-then-else

src/tactic/core/ctx_simplify_tactic.cpp

@@ -96,7 +96,7 @@ struct ctx_simplify_tactic::imp {
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         if (m.canceled())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m.limit().get_cancel_msg());
     }
 
     bool shared(expr * t) const { 

src/tactic/core/reduce_args_tactic.cpp

@@ -94,7 +94,7 @@ struct reduce_args_tactic::imp {
 
     void checkpoint() { 
         if (m_manager.canceled())
-            throw tactic_exception(TACTIC_CANCELED_MSG);
+            throw tactic_exception(m_manager.limit().get_cancel_msg());
         cooperate("reduce-args");
     }
     

src/tactic/core/solve_eqs_tactic.cpp

@@ -77,8 +77,8 @@ class solve_eqs_tactic : public tactic {
                 
         void checkpoint() {
             if (m().canceled())
-                throw tactic_exception(TACTIC_CANCELED_MSG);
-            cooperate("solve-eqs");
+                throw tactic_exception(m().limit().get_cancel_msg());
+        cooperate("solve-eqs");
         }
         
         // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs

src/tactic/sls/sls_engine.cpp

@@ -95,7 +95,7 @@ void sls_engine::collect_statistics(statistics& st) const {
 
 void sls_engine::checkpoint() {
     if (m_manager.canceled())
-        throw tactic_exception(TACTIC_CANCELED_MSG);
+        throw tactic_exception(m_manager.limit().get_cancel_msg());
     cooperate("sls");
 }
 

src/tactic/ufbv/quasi_macros_tactic.cpp

@@ -77,8 +77,8 @@ class quasi_macros_tactic : public tactic {
         
             while (more) { // CMW: use repeat(...) ?
                 if (m().canceled())
-                  throw tactic_exception(TACTIC_CANCELED_MSG);
-
+                    throw tactic_exception(m().limit().get_cancel_msg());
+            
                 new_forms.reset();
                 new_proofs.reset();
                 more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);