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

src/api/python/z3/z3.py

@@ -3993,6 +3993,58 @@ def BVRedOr(a):
         _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
 
+def BVAddNoOverflow(a, b, signed):
+    """A predicate the determines that bit-vector addition does not overflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
+
+def BVAddNoUnderflow(a, b):
+    """A predicate the determines that signed bit-vector addition does not underflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+def BVSubNoOverflow(a, b):
+    """A predicate the determines that bit-vector subtraction does not overflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+    
+
+def BVSubNoUnderflow(a, b, signed):
+    """A predicate the determines that bit-vector subtraction does not underflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
+
+def BVSDivNoOverflow(a, b):
+    """A predicate the determines that bit-vector signed division does not overflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+def BVSNegNoOverflow(a):
+    """A predicate the determines that bit-vector unary negation does not overflow"""
+    if __debug__:
+        _z3_assert(is_bv(a), "Argument should be a bit-vector")
+    return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
+
+def BVMulNoOverflow(a, b, signed):
+    """A predicate the determines that bit-vector multiplication does not overflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
+
+
+def BVMulNoUnderflow(a, b):
+    """A predicate the determines that bit-vector signed multiplication does not underflow"""
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+
+
 #########################################
 #
 # Arrays

src/smt/smt_b_justification.h

@@ -93,6 +93,16 @@ namespace smt {
 
     const b_justification null_b_justification(static_cast<clause*>(0));
 
+    inline std::ostream& operator<<(std::ostream& out, b_justification::kind k) {
+        switch (k) {
+        case b_justification::CLAUSE: return out << "clause";
+        case b_justification::BIN_CLAUSE: return out << "bin_clause";
+        case b_justification::AXIOM: return out << "axiom";
+        case b_justification::JUSTIFICATION: return out << "theory";
+        }
+        return out;
+    }
+
     typedef std::pair<literal, b_justification> justified_literal;
 };
 

src/smt/smt_conflict_resolution.cpp

@@ -468,20 +468,6 @@ namespace smt {
     }
 
     bool conflict_resolution::resolve(b_justification conflict, literal not_l) {
-
-#if 0
-        // for debugging #1233
-        if (not_l == to_literal(22267)) {
-            std::cout << not_l << "\n";
-            enable_trace("conflict");
-            enable_trace("conflict_verbose");
-            TRACE("conflict", 
-                  unsigned idx = 0;
-                  for (literal lit : m_assigned_literals) {
-                      m_ctx.display_literal(tout << (idx++) << ":", lit); tout << "\n";
-                  });
-        }
-#endif
         b_justification js;
         literal consequent;
 

src/smt/smt_context.cpp

@@ -285,15 +285,7 @@ namespace smt {
         d.set_justification(j);
     }
 
-
     void context::assign_core(literal l, b_justification j, bool decision) {
-#if 0
-        // for debugging #1233
-        if (l.var() == 11133 && l.sign()) {
-            std::cout << l << "\n";
-            UNREACHABLE();
-        }
-#endif
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
               display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
               display(tout, j););

src/smt/smt_context_pp.cpp

@@ -601,7 +601,7 @@ namespace smt {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals(out, lits.size(), lits.c_ptr());
+            display_literals(out, lits);
             break;
         }
         default:

src/smt/theory_seq.cpp

@@ -1228,18 +1228,25 @@ bool theory_seq::is_solved() {
     return true;
 }
 
-void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
+/**
+   \brief while extracting dependency literals ensure that they have all been asserted on the context.
+*/
+bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
+    context & ctx = get_context();    
+    DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); );
+    bool asserted = true;
     svector<assumption> assumptions;
     const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
-    for (unsigned i = 0; i < assumptions.size(); ++i) {
+    for (assumption const& a : assumptions) {
-        assumption const& a = assumptions[i];
         if (a.lit != null_literal) {
             lits.push_back(a.lit);
+            asserted &= ctx.get_assignment(a.lit) == l_true;
         }
         if (a.n1 != 0) {
             eqs.push_back(enode_pair(a.n1, a.n2));
         }
     }
+    return asserted;
 }
 
 
@@ -1257,7 +1264,8 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
 
     ctx.mark_as_relevant(lit);
     enode_pair_vector eqs;
-    linearize(dep, eqs, lits);
+    if (!linearize(dep, eqs, lits)) 
+        return;
     TRACE("seq",
           tout << "assert:";
           ctx.display_detailed_literal(tout, lit);
@@ -1276,7 +1284,8 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
     context& ctx = get_context();
     enode_pair_vector eqs;
     literal_vector lits(_lits);
-    linearize(dep, eqs, lits);
+    if (!linearize(dep, eqs, lits)) 
+        return;
     TRACE("seq", display_deps(tout << "assert conflict:", lits, eqs););
     m_new_propagation = true;
     ctx.set_conflict(
@@ -1292,27 +1301,13 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
     context& ctx = get_context();
     literal_vector lits;
     enode_pair_vector eqs;
-    linearize(dep, eqs, lits);
+    if (!linearize(dep, eqs, lits))
+        return;
     TRACE("seq",
           tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
           display_deps(tout, dep); 
           );
 
-#if 0
-    //std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
-    //display_deps(std::cout, dep);
-
-    for (literal lit : lits) {
-        SASSERT(ctx.get_assignment(lit) == l_true);
-    }
-    for (enode_pair p : eqs) {
-        if (p.first->get_root() != p.second->get_root()) {
-            std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n";
-        }
-        SASSERT(p.first->get_root() == p.second->get_root());
-    }
-#endif
-
     justification* js = ctx.mk_justification(
         ext_theory_eq_propagation_justification(
             get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
@@ -1858,12 +1853,12 @@ bool theory_seq::solve_ne(unsigned idx) {
     ne const& n = m_nqs[idx];
 
     unsigned num_undef_lits = 0;
-    for (unsigned i = 0; i < n.lits().size(); ++i) {
+    for (literal lit : n.lits()) {
-        switch (ctx.get_assignment(n.lits(i))) {
+        switch (ctx.get_assignment(lit)) {
         case l_false:
             TRACE("seq", display_disequation(tout << "has false literal\n", n);
-                  ctx.display_literal_verbose(tout, n.lits(i));                  
+                  ctx.display_literal_verbose(tout, lit);
-                  tout << "\n" << n.lits(i) << " " << ctx.is_relevant(n.lits(i)) << "\n";
+                  tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
                   );
             return true;
         case l_true:
@@ -1967,8 +1962,7 @@ bool theory_seq::solve_ne(unsigned idx) {
     if (num_undef_lits == 1 && new_ls.empty()) {
         literal_vector lits;
         literal undef_lit = null_literal;
-        for (unsigned i = 0; i < new_lits.size(); ++i) {
+        for (literal lit : new_lits) {
-            literal lit = new_lits[i];
             switch (ctx.get_assignment(lit)) {
             case l_true:
                 lits.push_back(lit);
@@ -2574,8 +2568,8 @@ void theory_seq::display_disequations(std::ostream& out) const {
 }
 
 void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
-    for (unsigned j = 0; j < e.lits().size(); ++j) {
+    for (literal lit : e.lits()) {
-        out << e.lits(j) << " ";
+        out << lit << " ";
     }
     if (e.lits().size() > 0) {
         out << "\n";
@@ -3820,11 +3814,11 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
     }
     expr_ref_vector concats(m);
     m_util.str.get_concat(e, concats);
-    for (unsigned i = 0; i < concats.size(); ++i) {
+    for (expr* c : concats) {
-        if (m_util.str.is_unit(concats[i].get())) {
+        if (m_util.str.is_unit(c)) {
             return false_literal;
         }
-        if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) {
+        if (m_util.str.is_string(c, s) && s.length() > 0) {
             return false_literal;
         }
     }
@@ -3895,8 +3889,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
     
     literal_vector lits(_lits);
     enode_pair_vector eqs;
-    linearize(deps, eqs, lits);
+    if (!linearize(deps, eqs, lits))
-
+        return;
+    
     if (add_to_eqs) {
         deps = mk_join(deps, _lits);
         new_eq_eh(deps, n1, n2);

src/smt/theory_seq.h

@@ -431,7 +431,7 @@ namespace smt {
         bool explain_empty(expr_ref_vector& es, dependency*& dep);
 
         // asserting consequences
-        void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
+        bool linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
         void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
         void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
         void propagate_eq(dependency* dep, enode* n1, enode* n2);