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

src/opt/maxres.cpp

@@ -375,7 +375,7 @@ public:
             get_mus_model(mdl);
             is_sat = minimize_core(_core);
             core.append(_core.size(), _core.c_ptr());
-            verify_core(core);
+            DEBUG_CODE(verify_core(core););
             ++m_stats.m_num_cores;
             if (is_sat != l_true) {
                 IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
@@ -738,7 +738,7 @@ public:
             m_correction_set_size = correction_set_size;
         }
 
-        TRACE("opt", tout << *mdl;);
+        TRACE("opt_verbose", tout << *mdl;);
 
         rational upper(0);
 
@@ -761,7 +761,7 @@ public:
         m_model = mdl;
         m_c.model_updated(mdl.get());
 
-        TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;);
+        TRACE("opt", tout << "updated upper: " << upper << "\n";);
 
         for (soft& s : m_soft) {
             s.set_value(m_model->is_true(s.s));
@@ -838,16 +838,17 @@ public:
 
     void commit_assignment() override {
         if (m_found_feasible_optimum) {
-            TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";);
             add(m_defs);
             add(m_asms);
+            TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";);
+
         }
         // else: there is only a single assignment to these soft constraints.
     }
 
     void verify_core(exprs const& core) {
         return;
-        IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";);                
+        IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";);                
         ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
         _solver->assert_expr(s().get_assertions());
         _solver->assert_expr(core);
@@ -855,8 +856,11 @@ public:
         IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n");
         CTRACE("opt", is_sat != l_false, 
                for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n";
-               _solver->display(tout););
+               _solver->display(tout);
-        VERIFY(is_sat == l_false);
+               tout << "other solver\n";
+               s().display(tout);
+               );
+        VERIFY(is_sat == l_false || m.canceled());
     }
 
     void verify_assumptions() {

src/sat/sat_solver.cpp

@@ -1664,6 +1664,7 @@ namespace sat {
         if (m_conflicts_since_init < m_next_simplify) {
             return;
         }
+        log_stats();
         m_simplifications++;
         IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
 
@@ -1890,75 +1891,81 @@ namespace sat {
             m_config.m_restart_margin * m_slow_glue_avg <= m_fast_glue_avg;
     }
 
+    void solver::log_stats() {
+        m_restart_logs++;
+        
+        std::stringstream strm;
+        strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " 
+             << std::setw(6) << m_stats.m_decision << " "
+             << std::setw(4) << m_stats.m_restart 
+             << mk_stat(*this)
+             << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
+        std::string str(strm.str());
+        svector<size_t> nums;
+        for (size_t i = 0; i < str.size(); ++i) {
+            while (i < str.size() && str[i] != ' ') ++i;
+            while (i < str.size() && str[i] == ' ') ++i;
+            // position of first character after space
+            if (i < str.size()) {
+                nums.push_back(i);
+            }
+        }   
+        bool same = m_last_positions.size() == nums.size();
+        size_t diff = 0;
+        for (unsigned i = 0; i < nums.size() && same; ++i) {
+            if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i];
+            if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i];
+        }
+        if (m_last_positions.empty() || 
+            m_restart_logs >= 20 + m_last_position_log || 
+            (m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) {
+            m_last_position_log = m_restart_logs;
+            //           conflicts          restarts          learned            gc               time
+            //                     decisions         clauses            units          memory
+            int adjust[9] = { -3,      -3,      -3,      -1,      -3,      -2,   -1,     -2,       -1 };
+            char const* tag[9]  = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" };
+            std::stringstream l1, l2;
+            l1 << "(sat.stats ";
+            l2 << "(sat.stats ";
+            size_t p1 = 11, p2 = 11;
+            SASSERT(nums.size() == 9);
+            for (unsigned i = 0; i < 9 && i < nums.size(); ++i) {
+                size_t p = nums[i];
+                if (i & 0x1) {
+                    // odd positions
+                    for (; p2 < p + adjust[i]; ++p2) l2 << " ";
+                    p2 += strlen(tag[i]);
+                    l2 << tag[i];
+                }
+                else {
+                    // even positions
+                    for (; p1 < p + adjust[i]; ++p1) l1 << " ";
+                    p1 += strlen(tag[i]);
+                    l1 << tag[i];
+                }                               
+            }
+            for (; p1 + 2 < str.size(); ++p1) l1 << " ";            
+            for (; p2 + 2 < str.size(); ++p2) l2 << " ";            
+            l1 << ")\n";
+            l2 << ")\n";
+            IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str());
+            m_last_positions.reset();
+            m_last_positions.append(nums);
+        }
+        IF_VERBOSE(1, verbose_stream() << str);            
+    }
+
     void solver::restart(bool to_base) {
         m_stats.m_restart++;
         m_restarts++;
         if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) {
-            m_restart_logs++;
             if (0 == m_restart_next_out) {
                 m_restart_next_out = 1;
             }
             else {
                 m_restart_next_out = (3*m_restart_next_out)/2 + 1; 
             }
-
+            log_stats();
-            std::stringstream strm;
-            strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " 
-                 << std::setw(6) << m_stats.m_decision << " "
-                 << std::setw(4) << m_stats.m_restart 
-                 << mk_stat(*this)
-                 << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
-            std::string str(strm.str());
-            svector<size_t> nums;
-            for (size_t i = 0; i < str.size(); ++i) {
-                while (i < str.size() && str[i] != ' ') ++i;
-                while (i < str.size() && str[i] == ' ') ++i;
-                // position of first character after space
-                if (i < str.size()) {
-                    nums.push_back(i);
-                }
-            }   
-            bool same = m_last_positions.size() == nums.size();
-            size_t diff = 0;
-            for (unsigned i = 0; i < nums.size() && same; ++i) {
-                if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i];
-                if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i];
-            }
-            if (m_last_positions.empty() || m_restart_logs >= 20 + m_last_position_log || (m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) {
-                m_last_position_log = m_restart_logs;
-                //           conflicts          restarts          learned            gc               time
-                //                     decisions         clauses            units          memory
-                int adjust[9] = { -3,      -3,      -3,      -1,      -3,      -2,   -1,     -2,       -1 };
-                char const* tag[9]  = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" };
-                std::stringstream l1, l2;
-                l1 << "(sat.stats ";
-                l2 << "(sat.stats ";
-                size_t p1 = 11, p2 = 11;
-                SASSERT(nums.size() == 9);
-                for (unsigned i = 0; i < 9 && i < nums.size(); ++i) {
-                    size_t p = nums[i];
-                    if (i & 0x1) {
-                        // odd positions
-                        for (; p2 < p + adjust[i]; ++p2) l2 << " ";
-                        p2 += strlen(tag[i]);
-                        l2 << tag[i];
-                    }
-                    else {
-                        // even positions
-                        for (; p1 < p + adjust[i]; ++p1) l1 << " ";
-                        p1 += strlen(tag[i]);
-                        l1 << tag[i];
-                    }                               
-                }
-                for (; p1 + 2 < str.size(); ++p1) l1 << " ";            
-                for (; p2 + 2 < str.size(); ++p2) l2 << " ";            
-                l1 << ")\n";
-                l2 << ")\n";
-                IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str());
-                m_last_positions.reset();
-                m_last_positions.append(nums);
-            }
-            IF_VERBOSE(1, verbose_stream() << str);            
         }
         IF_VERBOSE(30, display_status(verbose_stream()););
         pop_reinit(restart_level(to_base));

src/sat/sat_solver.h

@@ -425,6 +425,7 @@ namespace sat {
         unsigned m_last_position_log;
         unsigned m_restart_logs;
         unsigned restart_level(bool to_base);
+        void log_stats();
         bool should_restart() const;
         void set_next_restart();
         bool reached_max_conflicts();

src/smt/smt_conflict_resolution.cpp

@@ -1372,7 +1372,7 @@ namespace smt {
         }
 
         while (true) {
-            TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
+            TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";);
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
@@ -1417,7 +1417,7 @@ namespace smt {
             }
             while (idx >= 0) {
                 literal l = m_assigned_literals[idx];
-                TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
+                CTRACE("unsat_core_bug", m_ctx.is_marked(l.var()), tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << "\n";);
                 if (m_ctx.get_assign_level(l) < search_lvl)
                     goto end_unsat_core;
                 if (m_ctx.is_marked(l.var()))

src/smt/smt_context.cpp

@@ -3244,8 +3244,13 @@ namespace smt {
                 proof * pr = m_manager.mk_asserted(curr_assumption);
                 internalize_assertion(curr_assumption, pr, 0);
                 literal l = get_literal(curr_assumption);
+                if (l == true_literal)
+                    continue;
+                if (l == false_literal) {
+                    set_conflict(b_justification::mk_axiom());
+                    break;
+                }
                 m_literal2assumption.insert(l.index(), orig_assumption);
-                // mark_as_relevant(l); <<< not needed
                 // internalize_assertion marked l as relevant.
                 SASSERT(is_relevant(l));
                 TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);

src/smt/smt_context.h

@@ -1358,7 +1358,7 @@ namespace smt {
 
         void display_profile(std::ostream & out) const;
 
-        void display(std::ostream& out, b_justification j) const;
+        std::ostream& display(std::ostream& out, b_justification j) const;
 
         // -----------------------------------
         //

src/smt/smt_context_pp.cpp

@@ -356,9 +356,9 @@ namespace smt {
     }
 
     void context::display_unsat_core(std::ostream & out) const {
-        unsigned sz = m_unsat_core.size();
+        for (expr* c : m_unsat_core) {
-        for (unsigned i = 0; i < sz; i++)
+            out << mk_pp(c, m_manager) << "\n";
-            out << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
+        }
     }
 
     void context::collect_statistics(::statistics & st) const {
@@ -563,13 +563,14 @@ namespace smt {
             }
             out << "\n";
             if (is_app(n)) {
-                for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
+                for (expr* arg : *to_app(n)) {
-                    todo.push_back(to_app(n)->get_arg(i));
+                    todo.push_back(arg);
+                }
             }
         }
     }
 
-    void context::display(std::ostream& out, b_justification j) const {
+    std::ostream& context::display(std::ostream& out, b_justification j) const {
         switch (j.get_kind()) {
         case b_justification::AXIOM:
             out << "axiom";
@@ -593,7 +594,7 @@ namespace smt {
             UNREACHABLE();
             break;
         }
-        out << "\n";
+        return out << "\n";
     }
 
     void context::trace_assign(literal l, b_justification j, bool decision) const {

src/smt/theory_pb.cpp

@@ -1924,6 +1924,7 @@ namespace smt {
                 process_antecedent(~js.get_literal(), offset);
                 break;
             case b_justification::AXIOM:
+                bound = 0;
                 break;
             case b_justification::JUSTIFICATION: {
                 justification* j = js.get_justification(); 
@@ -1934,6 +1935,7 @@ namespace smt {
                 }
                 if (pbj == nullptr) {
                     TRACE("pb", tout << "skip justification for " << conseq << "\n";);
+                    bound = 0;
                     // this is possible when conseq is an assumption.
                     // The justification of conseq is itself, 
                     // don't increment the cofficient here because it assumes

src/smt/theory_seq.cpp

@@ -2905,17 +2905,26 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_skolem(m_tail, e)) {
-        // e = tail(s, l), len(s) > l => 
+        // e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1
-        // len(tail(s, l)) = len(s) - l - 1
+        // e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0
+
         s = to_app(e)->get_arg(0);
         l = to_app(e)->get_arg(1);
         expr_ref len_s = mk_len(s);
         literal len_s_gt_l = mk_simplified_literal(m_autil.mk_ge(mk_sub(len_s, l), m_autil.mk_int(1)));
-        if (ctx.get_assignment(len_s_gt_l) == l_true) {
+        switch (ctx.get_assignment(len_s_gt_l)) {
+        case l_true:
             len = mk_sub(len_s, mk_sub(l, m_autil.mk_int(1)));
             TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";);
             lits.push_back(len_s_gt_l);
             return true;
+        case l_false:
+            len = m_autil.mk_int(0);
+            TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";);
+            lits.push_back(~len_s_gt_l);
+            return true;
+        default:
+            break;
         }
     }
     else if (m_util.str.is_unit(e)) {

src/solver/solver.cpp

@@ -338,8 +338,11 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
 }
 
 void solver::dump_state(unsigned sz, expr* const* assumptions) {
-    std::string file = m_cancel_backup_file.str();
+    if ((symbol::null != m_cancel_backup_file) &&
-    if (file != "") {
+        !m_cancel_backup_file.is_numerical() && 
+        m_cancel_backup_file.c_ptr() &&
+        m_cancel_backup_file.bare_str()[0]) {
+        std::string file = m_cancel_backup_file.str();
         std::ofstream ous(file);
         display(ous, sz, assumptions);
     }