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

src/smt/theory_seq.cpp

@@ -2677,6 +2677,7 @@ literal theory_seq::mk_seq_eq(expr* a, expr* b) {
 }
 
 literal theory_seq::mk_eq_empty(expr* _e) {
+    context& ctx = get_context();
     expr_ref e(_e, m);
     SASSERT(m_util.is_seq(e));
     expr_ref emp(m);
@@ -2696,9 +2697,9 @@ literal theory_seq::mk_eq_empty(expr* _e) {
     }
     emp = m_util.str.mk_empty(m.get_sort(e));
 
-
     literal lit = mk_eq(e, emp, false);
-    get_context().force_phase(lit);
+    ctx.force_phase(lit);
+    ctx.mark_as_relevant(lit);
     return lit;
 }
 
@@ -3384,16 +3385,15 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     }
     expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
 
-    TRACE("seq", tout << mk_pp(e, m) << "\n";);
-
     literal e2_is_emp = mk_eq_empty(e2);
     switch (ctx.get_assignment(e2_is_emp)) {
     case l_true:
-        TRACE("seq", tout << mk_pp(e2, m) << " = empty\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e2, m) << " = empty\n";
+              ctx.display_literals_verbose(tout, 1, &e2_is_emp); tout << "\n"; );        
         return false; // done
     case l_undef:
         // ctx.force_phase(e2_is_emp);
-        TRACE("seq", tout << mk_pp(e2, m) << " ~ empty\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e2, m) << " ~ empty\n";);
         return true;  // retry
     default:
         break;
@@ -3406,10 +3406,11 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     literal e1_is_emp = mk_eq_empty(e1);
     switch (ctx.get_assignment(e1_is_emp)) {
     case l_true:        
-        TRACE("seq", tout << mk_pp(e1, m) << " = empty\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " !=  empty\n";);
+        add_axiom(ctx.get_literal(e), ~e1_is_emp);
         return false; // done
     case l_undef:        
-        TRACE("seq", tout << mk_pp(e1, m) << " ~ empty\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " ~ empty\n";);
         return true;  // retry
     default:
         break;
@@ -3425,11 +3426,11 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     case l_true: 
         break;
     case l_false:
-        TRACE("seq", tout << head1 << " = " << head2 << "\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << head1 << " != " << head2 << "\n";);
         return false;
     case l_undef:
         ctx.force_phase(~lit);
-        TRACE("seq", tout << head1 << " ~ " << head2 << "\n";);
+        TRACE("seq", tout << mk_pp(e, m) << ": " << head1 << " ~ " << head2 << "\n";);
         return true;
     }
     change = true;
@@ -3438,7 +3439,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     lits.push_back(~e2_is_emp);
     lits.push_back(lit);
     propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2)));
-    TRACE("seq", tout << "saturate: " << tail1 << " = " << tail2 << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " saturate: " << tail1 << " = " << tail2 << "\n";);
     return false;
 }
 

src/tactic/bv/bv_bounds_tactic.cpp

@@ -36,6 +36,11 @@ struct interval {
 
     explicit interval() : l(0), h(0), sz(0), tight(false) {}
     interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
+        // canonicalize full set
+        if (is_wrapped() && l == h + rational::one()) {
+            this->l = rational::zero();
+            this->h = uMaxInt(sz);
+        }
         SASSERT(invariant());
     }
 
@@ -147,10 +152,12 @@ std::ostream& operator<<(std::ostream& o, const interval& I) {
 
 
 class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
-    ast_manager&                     m;
+    typedef obj_map<expr, interval> map;
-    bv_util                          m_bv;
+
-    vector<obj_map<expr, interval> > m_scopes;
+    ast_manager& m;
-    obj_map<expr, interval>         *m_bound;
+    bv_util      m_bv;
+    vector<map>  m_scopes;
+    map         *m_bound;
 
     bool is_bound(expr *e, expr*& v, interval& b) {
         rational n;
@@ -203,7 +210,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
 public:
 
     bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) {
-        m_scopes.push_back(obj_map<expr, interval>());
+        m_scopes.push_back(map());
         m_bound = &m_scopes.back();
     }
 
@@ -270,8 +277,11 @@ public:
 
     virtual void push() {
         TRACE("bv", tout << "push\n";);
-        m_scopes.push_back(*m_bound);
+        unsigned sz = m_scopes.size();
+        m_scopes.resize(sz + 1);
         m_bound = &m_scopes.back();
+        m_bound->~map();
+        new (m_bound) map(m_scopes[sz - 1]);
     }
 
     virtual void pop(unsigned num_scopes) {

src/tactic/core/ctx_simplify_tactic.cpp

@@ -180,6 +180,7 @@ struct ctx_simplify_tactic::imp {
         pop(scope_level());
         SASSERT(scope_level() == 0);
         restore_cache(0);
+        dealloc(m_simp);
         DEBUG_CODE({
             for (unsigned i = 0; i < m_cache.size(); i++) {
                 CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, 
@@ -458,7 +459,11 @@ struct ctx_simplify_tactic::imp {
             }
             simplify(t, new_t);
             pop(scope_level() - old_lvl);
-            VERIFY(assert_expr(new_c, true));
+            if (!assert_expr(new_c, true)) {
+                r = new_t;
+                cache(ite, r);
+                return;
+            }
             simplify(e, new_e);
             pop(scope_level() - old_lvl);
             if (c == new_c && t == new_t && e == new_e) {
@@ -568,13 +573,15 @@ struct ctx_simplify_tactic::imp {
 
 ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p):
     m_imp(alloc(imp, m, simp, p)),
-    m_params(p),
+    m_params(p) {
-    m_simp(simp) {
+}
+
+tactic * ctx_simplify_tactic::translate(ast_manager & m) {
+    return alloc(ctx_simplify_tactic, m, m_imp->m_simp->translate(m), m_params);
 }
 
 ctx_simplify_tactic::~ctx_simplify_tactic() {
     dealloc(m_imp);
-    dealloc(m_simp);
 }
 
 void ctx_simplify_tactic::updt_params(params_ref const & p) {
@@ -602,7 +609,7 @@ void ctx_simplify_tactic::operator()(goal_ref const & in,
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = alloc(imp, m, m_simp->translate(m), m_params);
+    imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params);
     std::swap(d, m_imp);    
     dealloc(d);
 }

src/tactic/core/ctx_simplify_tactic.h

@@ -42,13 +42,10 @@ protected:
     struct      imp;
     imp *       m_imp;
     params_ref  m_params;
-    simplifier* m_simp;
 public:
     ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p = params_ref());
 
-    virtual tactic * translate(ast_manager & m) {
+    virtual tactic * translate(ast_manager & m);
-        return alloc(ctx_simplify_tactic, m, m_simp->translate(m), m_params);
-    }
 
     virtual ~ctx_simplify_tactic();