Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

src/cmd_context/context_params.cpp

@@ -33,7 +33,7 @@ context_params::context_params() {
     m_trace          = false;
     m_debug_ref_count = false;
     m_smtlib2_compliant = false;
-    m_well_sorted_check = false;
+    m_well_sorted_check = true;
     m_timeout = UINT_MAX;
     updt_params();
 }

src/muz/base/dl_rule_set.cpp

@@ -457,7 +457,7 @@ namespace datalog {
             rule * r = *it;
             app * head = r->get_head();
             func_decl * head_decl = head->get_decl();
-            unsigned head_strat = get_predicate_strat(head_decl);
+            // unsigned head_strat = get_predicate_strat(head_decl);
             unsigned n = r->get_tail_size();
             for (unsigned i = 0; i < n; i++) {
                 func_decl * tail_decl = r->get_tail(i)->get_decl();

src/smt/smt_context.cpp

@@ -4016,6 +4016,7 @@ namespace smt {
     void context::set_cancel_flag(bool f) {
         m_cancel_flag = f;
         m_asserted_formulas.set_cancel_flag(f);
+        m_qmanager->set_cancel(f);
     }
 
 };

src/smt/smt_model_checker.cpp

@@ -40,6 +40,7 @@ namespace smt {
         m_max_cexs(1),
         m_iteration_idx(0),
         m_curr_model(0),
+        m_cancel(false),
         m_new_instances_bindings(m) {
     }
 

src/smt/smt_model_checker.h

@@ -51,6 +51,7 @@ namespace smt {
         unsigned                                    m_iteration_idx;
         proto_model *                               m_curr_model;
         obj_map<expr, expr *>                       m_value2expr;
+        bool                                        m_cancel;
         friend class instantiation_set;
 
         void init_aux_context();
@@ -92,6 +93,8 @@ namespace smt {
         void restart_eh();
 
         void reset();
+
+        void set_cancel(bool f) { m_cancel = f; }
     };
 };
 

src/smt/smt_model_finder.cpp

@@ -34,6 +34,8 @@ Revision History:
 #include"well_sorted.h"
 #include"model_pp.h"
 #include"ast_smt2_pp.h"
+#include"cooperate.h"
+#include"tactic_exception.h"
 
 namespace smt {
 
@@ -1714,14 +1716,22 @@ namespace smt {
             // when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver.
             // in this case, the quantifier_info stores the instantiation sets.
             ptr_vector<instantiation_set>  * m_uvar_inst_sets;
+            bool                     m_cancel;
 
             friend class quantifier_analyzer;
 
+            void checkpoint() {
+                cooperate("quantifier_info");
+                if (m_cancel)
+                    throw tactic_exception(TACTIC_CANCELED_MSG);
+            }
+
             void insert_qinfo(qinfo * qi) {
                 // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal.
                 ptr_vector<qinfo>::iterator it  = m_qinfo_vect.begin();            
                 ptr_vector<qinfo>::iterator end = m_qinfo_vect.end();            
                 for (; it != end; ++it) {
+                    checkpoint();
                     if (qi->is_equal(*it)) {
                         dealloc(qi);
                         return;
@@ -1743,7 +1753,8 @@ namespace smt {
                 m_is_auf(true),
                 m_has_x_eq_y(false),
                 m_the_one(0),
-                m_uvar_inst_sets(0) {
+                m_uvar_inst_sets(0),
+                m_cancel(false) {
                 if (has_quantifiers(q->get_expr())) {
                     static bool displayed_flat_msg = false;
                     if (!displayed_flat_msg) {
@@ -1896,6 +1907,7 @@ namespace smt {
                 }
             }
 
+            void set_cancel(bool f) { m_cancel = f; }
         };
         
         /**
@@ -1908,6 +1920,7 @@ namespace smt {
             array_util           m_array_util;
             arith_util           m_arith_util;
             bv_util              m_bv_util;
+            bool                 m_cancel;
 
             quantifier_info *    m_info;
 
@@ -2318,9 +2331,16 @@ namespace smt {
                 visit_formula(n->get_arg(1), POS);
                 visit_formula(n->get_arg(1), NEG);
             }
+
+            void checkpoint() {
+                cooperate("quantifier_analyzer");
+                if (m_cancel)
+                    throw tactic_exception(TACTIC_CANCELED_MSG);
+            }
             
             void process_formulas_on_stack() {
                 while (!m_ftodo.empty()) {
+                    checkpoint();
                     entry & e = m_ftodo.back();
                     expr * curr  = e.first;
                     polarity pol = e.second;
@@ -2411,6 +2431,7 @@ namespace smt {
                 m_array_util(m), 
                 m_arith_util(m),
                 m_bv_util(m),
+                m_cancel(false),
                 m_info(0) {
             }
             
@@ -2441,6 +2462,11 @@ namespace smt {
                 m_info = 0;
             }
 
+            void set_cancel(bool f) { 
+                m_cancel = f; 
+                if (m_info) m_info->set_cancel(f);
+            }
+
         };
 
         /**
@@ -3259,6 +3285,7 @@ namespace smt {
         m_sm_solver(alloc(simple_macro_solver, m, m_q2info)),
         m_hint_solver(alloc(hint_solver, m, m_q2info)),
         m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)),
+        m_cancel(false),
         m_new_constraints(m) {
     }
     
@@ -3535,4 +3562,9 @@ namespace smt {
         }
     }
 
+    void model_finder::set_cancel(bool f) {
+        m_cancel = f;
+        m_analyzer->set_cancel(f);
+    }
+
 };

src/smt/smt_model_finder.h

@@ -50,6 +50,8 @@ Revision History:
 #include"func_decl_dependencies.h"
 #include"simplifier.h"
 #include"proto_model.h"
+#include"cooperate.h"
+#include"tactic_exception.h"
 
 namespace smt {
     class context;
@@ -83,6 +85,7 @@ namespace smt {
         scoped_ptr<simple_macro_solver>        m_sm_solver;
         scoped_ptr<hint_solver>                m_hint_solver;
         scoped_ptr<non_auf_macro_solver>       m_nm_solver;
+        bool                                   m_cancel;
         
         struct scope {
             unsigned                           m_quantifiers_lim;
@@ -102,6 +105,12 @@ namespace smt {
         void process_auf(ptr_vector<quantifier> const & qs, proto_model * m);
         instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const;
 
+        void checkpoint() {
+            cooperate("model_finder");
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+        }
+
     public:
         model_finder(ast_manager & m, simplifier & s);
         ~model_finder();
@@ -119,6 +128,8 @@ namespace smt {
         bool restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks);
 
         void restart_eh();
+
+        void set_cancel(bool f);
     };
 };
 

src/smt/smt_quantifier.cpp

@@ -593,6 +593,8 @@ namespace smt {
 
         virtual void set_cancel(bool f) {
             // TODO: interrupt MAM and MBQI
+            m_model_finder->set_cancel(f);
+            m_model_checker->set_cancel(f);
         }
 
         virtual final_check_status final_check_eh(bool full) {

src/smt/theory_array_full.cpp

@@ -778,7 +778,7 @@ namespace smt {
         TRACE("array", 
               tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" 
               << mk_bounded_pp(v2, get_manager()) << "\n";);
-        context& ctx = get_context();
+        
         if (m_eqs.contains(v1, v2)) {
             return false;
         }