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

src/api/api_context.cpp

@@ -70,22 +70,6 @@ namespace api {
     //
     // ------------------------
 
-    context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
-        m_ctx(ctx) {
-        #pragma omp critical (set_interruptable) 
-        {
-            SASSERT(m_ctx.m_interruptable == 0);
-            m_ctx.m_interruptable = &i;
-        }
-    }
-
-    context::set_interruptable::~set_interruptable() {
-        #pragma omp critical (set_interruptable) 
-        {
-            m_ctx.m_interruptable = 0;
-        }
-    }
-
     context::context(context_params * p, bool user_ref_count):
         m_params(p != 0 ? *p : context_params()),
         m_user_ref_count(user_ref_count),
@@ -105,11 +89,10 @@ namespace api {
         m_print_mode = Z3_PRINT_SMTLIB_FULL;
         m_searching  = false;
         
-        m_interruptable = 0;
-
         m_smtlib_parser           = 0;
         m_smtlib_parser_has_decls = false;
 
+        m_interruptable = 0;                
         m_error_handler = &default_error_handler;
 
         m_basic_fid = m().get_basic_family_id();
@@ -139,6 +122,22 @@ namespace api {
         }
     }
 
+    context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
+        m_ctx(ctx) {
+        #pragma omp critical (set_interruptable) 
+        {
+            SASSERT(m_ctx.m_interruptable == 0);
+            m_ctx.m_interruptable = &i;
+        }
+    }
+
+    context::set_interruptable::~set_interruptable() {
+        #pragma omp critical (set_interruptable) 
+        {
+            m_ctx.m_interruptable = 0;
+        }
+    }
+
     void context::interrupt() {
         #pragma omp critical (set_interruptable)
         {

src/api/python/z3.py

@@ -1549,6 +1549,9 @@ def And(*args):
     if isinstance(last_arg, Context):
         ctx = args[len(args)-1]
         args = args[:len(args)-1]
+    elif len(args) == 1 and isinstance(args[0], AstVector):
+        ctx = args[0].ctx
+        args = [a for a in args[0]]
     else:
         ctx = main_ctx()
     args = _get_args(args)
@@ -6775,7 +6778,7 @@ class Optimize(Z3PPObject):
         return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
 
     def statistics(self):
-        """Return statistics for the last `query()`.
+        """Return statistics for the last check`.
         """
         return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
 

src/api/z3_replayer.cpp

@@ -515,7 +515,7 @@ struct z3_replayer::imp {
                 if (idx >= m_cmds.size())
                     throw z3_replayer_exception("invalid command");
                 try {
-                    TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";);
+                    TRACE("z3_replayer_cmd", tout << idx << ":" << m_cmds_names[idx] << "\n";);
                     m_cmds[idx](m_owner);
                 }
                 catch (z3_error & ex) {

src/sat/sat_clause.cpp

@@ -123,21 +123,32 @@ namespace sat {
 
     clause_allocator::clause_allocator():
         m_allocator("clause-allocator") {
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         m_num_segments = 0;
+#if defined(Z3DEBUG)
+        m_overflow_valid = false;
+#endif
 #endif
     }
 
     clause * clause_allocator::get_clause(clause_offset cls_off) const {
-#ifdef _AMD64_
+#if defined(_AMD64_) 
+#if defined (Z3DEBUG)
+        clause const* result;
+        if (m_overflow_valid && m_cls_offset2ptr.find(cls_off, result)) {
+            return const_cast<clause*>(result);
+        }
+#endif
         return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask));
 #else
         return reinterpret_cast<clause *>(cls_off);
 #endif
     }
 
-#ifdef _AMD64_
+#if defined(_AMD64_) 
-    unsigned clause_allocator::get_segment(size_t ptr) {
+    unsigned clause_allocator::get_segment(clause const* cls) {
+        size_t ptr = reinterpret_cast<size_t>(cls);
+
         SASSERT((ptr & c_aligment_mask) == 0);
         ptr &= ~0xFFFFFFFFull; // Keep only high part
         unsigned i = 0;
@@ -145,18 +156,39 @@ namespace sat {
             if (m_segments[i] == ptr)
                 return i;
         i = m_num_segments;
-        m_num_segments++;
+#if defined(Z3DEBUG)
-        SASSERT(m_num_segments <= c_max_segments);
+        SASSERT(i < c_max_segments);
-        if (i >= c_max_segments)
+        if (i + 1 == c_max_segments) {
-            throw default_exception("segment out of range");
+            m_overflow_valid = true;
+            i += c_max_segments * m_cls_offset2ptr.size();
+            m_ptr2cls_offset.insert(ptr, i);
+            m_cls_offset2ptr.insert(i, cls);
+        }
+        else {
+            ++m_num_segments;
             m_segments[i] = ptr;
+        }
+#else
+        SASSERT(i <= c_max_segments);
+        if (i == c_max_segments) {
+            throw default_exception("segment out of range");
+        }
+        m_segments[i] = ptr;
+        ++m_num_segments;
+#endif
         return i;
     }
 #endif
 
     clause_offset clause_allocator::get_offset(clause const * ptr) const {
-#ifdef _AMD64_
+#if defined(_AMD64_) 
-        return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + const_cast<clause_allocator*>(this)->get_segment(reinterpret_cast<size_t>(ptr));
+        unsigned segment = const_cast<clause_allocator*>(this)->get_segment(ptr);
+#if defined(Z3DEBUG)
+        if (segment >= c_max_segments) {
+            return m_ptr2cls_offset.find(reinterpret_cast<size_t>(ptr));
+        }
+#endif
+        return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + segment;
 #else
         return reinterpret_cast<size_t>(ptr);
 #endif
@@ -164,7 +196,7 @@ namespace sat {
     
     clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) {
         size_t size = clause::get_obj_size(num_lits);
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         size_t slot = size >> c_cls_alignment;
         if ((size & c_aligment_mask) != 0)
             slot++;
@@ -181,7 +213,7 @@ namespace sat {
         TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
         size_t size = clause::get_obj_size(cls->m_capacity);
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         size_t slot = size >> c_cls_alignment;
         if ((size & c_aligment_mask) != 0)
             slot++;

src/sat/sat_clause.h

@@ -22,6 +22,7 @@ Revision History:
 #include"sat_types.h"
 #include"small_object_allocator.h"
 #include"id_gen.h"
+#include"map.h"
 
 #ifdef _MSC_VER
 #pragma warning(disable : 4200)
@@ -124,13 +125,18 @@ namespace sat {
     class clause_allocator {
         small_object_allocator m_allocator;
         id_gen                 m_id_gen;
-#ifdef _AMD64_
+#if defined(_AMD64_) 
-        unsigned get_segment(size_t ptr);
+        unsigned get_segment(clause const* cls);
         static const unsigned  c_cls_alignment = 3; 
         static const unsigned  c_max_segments  = 1 << c_cls_alignment;
         static const size_t    c_aligment_mask = (1ull << c_cls_alignment) - 1ull;
         unsigned               m_num_segments;
         size_t                 m_segments[c_max_segments];
+#if defined(Z3DEBUG)
+        bool                   m_overflow_valid;
+        size_t_map<unsigned>   m_ptr2cls_offset;
+        u_map<clause const*>   m_cls_offset2ptr;
+#endif
 #endif
     public:
         clause_allocator();

src/smt/asserted_formulas.cpp

@@ -543,8 +543,12 @@ void asserted_formulas::infer_patterns() {
 }
 
 void asserted_formulas::commit() {
-    m_macro_manager.mark_forbidden(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
+    commit(m_asserted_formulas.size());
-    m_asserted_qhead = m_asserted_formulas.size();
+}
+
+void asserted_formulas::commit(unsigned new_qhead) {
+    m_macro_manager.mark_forbidden(new_qhead - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
+    m_asserted_qhead = new_qhead;
 }
 
 void asserted_formulas::eliminate_term_ite() {

src/smt/asserted_formulas.h

@@ -113,6 +113,7 @@ public:
     unsigned get_formulas_last_level() const;
     unsigned get_qhead() const { return m_asserted_qhead; }
     void commit(); 
+    void commit(unsigned new_qhead); 
     expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
     proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
     expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }

src/smt/smt_consequences.cpp

@@ -23,9 +23,9 @@ Revision History:
 
 namespace smt {
 
-    expr_ref context::antecedent2fml(uint_set const& vars) {
+    expr_ref context::antecedent2fml(index_set const& vars) {
         expr_ref_vector premises(m_manager);
-        uint_set::iterator it = vars.begin(), end = vars.end();
+        index_set::iterator it = vars.begin(), end = vars.end();
         for (; it != end; ++it) {
             expr* e =  bool_var2expr(*it);
             premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e));
@@ -42,14 +42,14 @@ namespace smt {
     // - e is an equality between a variable and value that is to be fixed.
     // - e is a data-type recognizer of a variable that is to be fixed.
     // 
-    void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
+    void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
         ast_manager& m = m_manager;
         datatype_util dt(m);
         expr* e1, *e2;       
         expr_ref fml(m);        
         if (lit == true_literal) return;
         expr* e = bool_var2expr(lit.var());
-        uint_set s;
+        index_set s;
         if (assumptions.contains(lit.var())) {
             s.insert(lit.var());
         }
@@ -86,7 +86,11 @@ namespace smt {
             }
         }
         m_antecedents.insert(lit.var(), s);
-        TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";);
+        TRACE("context", display_literal_verbose(tout, lit); 
+              for (index_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
+                  tout << " " << *it;
+              }
+              tout << "\n";);
         bool found = false;
         if (vars.contains(e)) {
             found = true;
@@ -116,7 +120,7 @@ namespace smt {
         }
     }
 
-    void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
+    void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
         pop_to_search_lvl();
         SASSERT(!inconsistent());
         literal_vector const& lits = assigned_literals();
@@ -174,6 +178,9 @@ namespace smt {
             else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) {
                 to_delete.push_back(k);
             }
+            else if (get_assignment(mk_diseq(k, v)) == l_true) {
+                to_delete.push_back(k);
+            }
         }
         for (unsigned i = 0; i < to_delete.size(); ++i) {
             var2val.remove(to_delete[i]);
@@ -201,7 +208,7 @@ namespace smt {
             if (!m.is_bool(k) && are_equal(k, v)) {
                 literal_vector literals;
                 m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals);
-                uint_set s;
+                index_set s;
                 for (unsigned i = 0; i < literals.size(); ++i) {
                     SASSERT(get_assign_level(literals[i]) <= get_search_level());
                     s |= m_antecedents.find(literals[i].var());
@@ -215,9 +222,7 @@ namespace smt {
                 for (unsigned i = 0; i < literals.size(); ++i) {
                     literals[i].neg();
                 }
-                eq = mk_eq_atom(k, v);
+                literal lit = mk_diseq(k, v);
-                internalize_formula(eq, false);
-                literal lit(get_bool_var(eq), false);
                 literals.push_back(lit);
                 mk_clause(literals.size(), literals.c_ptr(), 0);
                 TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr()););
@@ -229,6 +234,18 @@ namespace smt {
         return to_delete.size();
     }
 
+    literal context::mk_diseq(expr* e, expr* val) {
+        ast_manager& m = m_manager;
+        if (m.is_bool(e)) {
+            return literal(get_bool_var(e), m.is_true(val));
+        }
+        else {
+            expr_ref eq(mk_eq_atom(e, val), m);
+            internalize_formula(eq, false);
+            return literal(get_bool_var(eq), true);
+        }
+    }
+
     lbool context::get_consequences(expr_ref_vector const& assumptions, 
                                     expr_ref_vector const& vars, 
                                     expr_ref_vector& conseq, 
@@ -241,7 +258,7 @@ namespace smt {
             return is_sat;
         }
         obj_map<expr, expr*> var2val;
-        uint_set _assumptions;
+        index_set _assumptions;
         for (unsigned i = 0; i < assumptions.size(); ++i) {
             _assumptions.insert(get_literal(assumptions[i]).var());
         }
@@ -288,18 +305,7 @@ namespace smt {
             // the opposite value of the current reference model.
             // If the variable is a non-Boolean, it means adding a disequality.
             //
-            literal lit;
+            literal lit = mk_diseq(e, val);
-            if (m.is_bool(e)) {
-                lit = literal(get_bool_var(e), m.is_true(val));
-            }
-            else {
-                eq = mk_eq_atom(e, val);
-                internalize_formula(eq, false);
-                lit = literal(get_bool_var(eq), true);
-                TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";
-                      display_literal_verbose(tout, lit); tout << "\n"; 
-                      tout << "Equal: " << are_equal(e, val) << "\n";);
-            }
             mark_as_relevant(lit);
             push_scope();
             assign(lit, b_justification::mk_axiom(), true);
@@ -434,10 +440,11 @@ namespace smt {
         pop_to_base_lvl();
         lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
         if (is_sat != l_true) {
+            TRACE("context", tout << is_sat << "\n";);
             return is_sat;
         }
         obj_map<expr, expr*> var2val;
-        uint_set _assumptions;
+        index_set _assumptions;
         for (unsigned i = 0; i < assumptions.size(); ++i) {
             _assumptions.insert(get_literal(assumptions[i]).var());
         }
@@ -475,20 +482,12 @@ namespace smt {
             obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
             unsigned num_vars = 0;
             for (; it != end && num_vars < chunk_size; ++it) {
+                if (get_cancel_flag()) {
+                    return l_undef;
+                }
                 expr* e = it->m_key;
                 expr* val = it->m_value;
-                literal lit;
+                literal lit = mk_diseq(e, val);
-                if (m.is_bool(e)) {
-                    lit = literal(get_bool_var(e), m.is_true(val));
-                }
-                else {
-                    eq = mk_eq_atom(e, val);
-                    internalize_formula(eq, false);
-                    lit = literal(get_bool_var(eq), true);
-                    TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";
-                          display_literal_verbose(tout, lit); tout << "\n"; 
-                          tout << "Equal: " << are_equal(e, val) << "\n";);
-                }
                 mark_as_relevant(lit);
                 if (get_assignment(lit) != l_undef) {
                     continue;
@@ -504,9 +503,6 @@ namespace smt {
                         m_not_l = null_literal;
                         SASSERT(m_search_lvl == get_search_level());
                     }
-                    if (get_cancel_flag()) {
-                        return l_undef;
-                    }
                 }
             }
             SASSERT(!inconsistent());

src/smt/smt_context.cpp

@@ -1833,7 +1833,7 @@ namespace smt {
         m_stats.m_num_decisions++;
         
         push_scope();
-        TRACE("context", tout << "splitting, lvl: " << m_scope_lvl << "\n";);
+        TRACE("decide", tout << "splitting, lvl: " << m_scope_lvl << "\n";);
 
         TRACE("decide_detail", tout << mk_pp(bool_var2expr(var), m_manager) << "\n";);
 
@@ -2949,7 +2949,11 @@ namespace smt {
         if (!m_asserted_formulas.inconsistent()) {
             unsigned sz    = m_asserted_formulas.get_num_formulas();
             unsigned qhead = m_asserted_formulas.get_qhead();
-            while (qhead < sz && !m_manager.canceled()) {
+            while (qhead < sz) {
+                if (get_cancel_flag()) {
+                    m_asserted_formulas.commit(qhead);
+                    return;
+                }
                 expr * f   = m_asserted_formulas.get_formula(qhead);
                 proof * pr = m_asserted_formulas.get_formula_proof(qhead);
                 internalize_assertion(f, pr, 0);

src/smt/smt_context.h

@@ -1344,9 +1344,11 @@ namespace smt {
             literal lit, context& src_ctx, context& dst_ctx,
             vector<bool_var> b2v, ast_translation& tr);
         
-        u_map<uint_set> m_antecedents;
+        typedef hashtable<unsigned, u_hash, u_eq> index_set;
-        void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
+        //typedef uint_set index_set;
-        void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
+        u_map<index_set> m_antecedents;
+        void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
+        void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
        
         void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq);
 
@@ -1354,7 +1356,9 @@ namespace smt {
 
         unsigned extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq);
 
-        expr_ref antecedent2fml(uint_set const& ante);
+        expr_ref antecedent2fml(index_set const& ante);
+
+        literal mk_diseq(expr* v, expr* val);
 
         void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                    expr_ref_vector const& conseq, expr_ref_vector const& unfixed);

src/util/hashtable.h

@@ -558,14 +558,13 @@ public:
 
     core_hashtable& operator|=(core_hashtable const& other) {
         if (this == &other) return *this;
-        iterator i = begin(), e = end();
+        iterator i = other.begin(), e = other.end();
         for (; i != e; ++i) {
             insert(*i);
         }
         return *this;
     }
 
-
     core_hashtable& operator&=(core_hashtable const& other) {
         if (this == &other) return *this;
         core_hashtable copy(*this);

src/util/rlimit.cpp

@@ -36,7 +36,7 @@ bool reslimit::inc() {
 
 bool reslimit::inc(unsigned offset) {
     m_count += offset;
-    return !m_cancel && (m_limit == 0 || m_count <= m_limit);
+    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
 }
 
 void reslimit::push(unsigned delta_limit) {