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

src/ast/rewriter/bv_rewriter.h

@@ -168,6 +168,8 @@ public:
     }
 
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool hi_div0() const { return m_hi_div0; }
 };
 
 #endif

src/opt/maxres.cpp

@@ -228,7 +228,6 @@ public:
             switch (is_sat) {
             case l_true: 
                 get_current_correction_set(cs);
-                IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs););
                 if (cs.empty()) {
                     m_found_feasible_optimum = m_model.get() != 0;
                     m_lower = m_upper;
@@ -350,9 +349,11 @@ public:
             is_sat = minimize_core(core);
             ++m_stats.m_num_cores;
             if (is_sat != l_true) {
+                IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
                 break;
             }
             if (core.empty()) {
+                IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";);
                 cores.reset();
                 m_lower = m_upper;
                 return l_true;
@@ -470,6 +471,7 @@ public:
         SASSERT(!core.empty());
         rational w = split_core(core);
         TRACE("opt", display_vec(tout << "minimized core: ", core););
+        IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
         max_resolve(core, w);
         fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);

src/sat/sat_solver.cpp

@@ -110,7 +110,7 @@ namespace sat {
                 buffer.reset();
                 for (unsigned i = 0; i < c.size(); i++)
                     buffer.push_back(c[i]);
-                mk_clause(buffer.size(), buffer.c_ptr());
+                mk_clause(buffer);
             }
         }
     }
@@ -892,6 +892,7 @@ namespace sat {
         if (num_lits == 0 && m_user_scope_literals.empty()) {
             return;
         }
+        m_replay_lit = null_literal;        
 
     retry_init_assumptions:
         m_assumptions.reset();
@@ -922,13 +923,8 @@ namespace sat {
             if (m_config.m_optimize_model) {
                 m_wsls.set_soft(num_lits, lits, weights);
             }
-            else {
+            else if (!init_weighted_assumptions(num_lits, lits, weights, max_weight)) {
-                svector<literal> blocker;
+                goto retry_init_assumptions;
-                if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) {
-                    pop_to_base_level();
-                    mk_clause(blocker.size(), blocker.c_ptr());
-                    goto retry_init_assumptions;
-                }
             }
             return;
         }
@@ -939,55 +935,124 @@ namespace sat {
             m_assumption_set.insert(lit);       
             m_assumptions.push_back(lit);       
             assign(lit, justification());       
-            //        propagate(false);         
         }
     }
 
-    bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, 
+    void solver::resolve_weighted() {
-                                           svector<literal>& blocker) {
+        flet<bool> _min1(m_config.m_minimize_core, false);
+        flet<bool> _min2(m_config.m_minimize_core_partial, false);
+        m_conflict_lvl = m_scope_lvl;
+        resolve_conflict_for_unsat_core();
+    }
+
+    bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
         double weight = 0;
-        blocker.reset();
+        literal_vector blocker;
+        literal_vector min_core;
+        bool min_core_valid = false;
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
             SASSERT(is_external(lit.var()));  
-            m_assumption_set.insert(lit);       
             TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
+            SASSERT(m_scope_lvl == 1);
 
+            if (m_replay_lit == lit && value(lit) == l_undef) {
+                mk_clause(m_replay_clause);
+                propagate(false);
+                SASSERT(inconsistent() || value(lit) == l_false);
+                if (inconsistent()) {
+                    IF_VERBOSE(1, verbose_stream() << lit << " cannot be false either\n";);
+                    return true;
+                }
+                IF_VERBOSE(1, verbose_stream() << lit << " set to false\n";);
+                SASSERT(value(lit) == l_false);
+                if (m_replay_clause.size() < min_core.size() || !min_core_valid) {
+                    min_core.reset();
+                    min_core.append(m_replay_clause);
+                    min_core_valid = true;
+                }
+                m_replay_clause.reset();
+                m_replay_lit = null_literal;
+                continue;
+            }
             switch(value(lit)) {
             case l_undef:
+                m_assumption_set.insert(lit);       
                 m_assumptions.push_back(lit);       
                 assign(lit, justification());
+                propagate(false);
+                if (inconsistent()) {
+                    resolve_weighted();
+                    m_replay_clause.reset();
+                    m_replay_lit = lit;
+                    // next time around, the negation of the literal will be implied.
+                    for (unsigned j = 0; j < m_core.size(); ++j) {
+                        m_replay_clause.push_back(~m_core[j]);
+                    }
+                    pop_to_base_level();
+                    IF_VERBOSE(11, 
+                               verbose_stream() << "undef: " << lit << " : " << m_replay_clause << "\n";
+                               verbose_stream() << m_assumptions << "\n";);
+                    return false;
+                }
+                blocker.push_back(~lit);
                 break;
-            case l_false: {
+                
+            case l_false: 
+                m_assumption_set.insert(lit);       
                 m_assumptions.push_back(lit);       
                 SASSERT(!inconsistent());
                 set_conflict(justification(), ~lit);
-                flet<bool> _min1(m_config.m_minimize_core, false);
+                resolve_weighted();
-                flet<bool> _min2(m_config.m_minimize_core_partial, false);
-                resolve_conflict_for_unsat_core();
-                m_assumptions.pop_back();
                 weight += weights[i];
-                blocker.push_back(lit);
                 TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
-                SASSERT(m_core.size() <= m_assumptions.size() + 1);
+                SASSERT(m_core.size() <= m_assumptions.size());
-                SASSERT(m_assumptions.size() <= i);
+                SASSERT(m_assumptions.size() <= i+1);
-                if (m_core.size() <= 3 || m_core.size() < blocker.size()) {
+                if (m_core.size() <= 3) {
-                    TRACE("opt", tout << "found small core: " << m_core.size() << "\n";); 
+                    m_inconsistent = true;
+                    TRACE("opt", tout << "found small core: " << m_core << "\n";); 
+                    IF_VERBOSE(11, verbose_stream() << "small core: " << m_core << "\n";);
                     return true;
                 }
-                m_inconsistent = false;                
                 if (weight >= max_weight) {
                     ++m_stats.m_blocked_corr_sets;
-                    TRACE("opt", tout << "blocking soft correction set: " << blocker.size() << "\n";); 
+                    TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); 
                     // block the current correction set candidate.
+                    IF_VERBOSE(11, verbose_stream() << "blocking " << blocker << "\n";);
+                    pop_to_base_level();
+                    mk_clause(blocker);
                     return false;
                 }
+                VERIFY(m_assumptions.back() == m_assumption_set.pop());
+                m_assumptions.pop_back();
+                m_inconsistent = false;                
+                if (!min_core_valid || m_core.size() < min_core.size()) {
+                    min_core.reset();
+                    min_core.append(m_core);
+                    min_core_valid = true;
+                }
+                blocker.push_back(lit);
                 break;
-            }
             case l_true:
                 break;
             }
-            propagate(false);         
+        }
+        TRACE("sat", tout << "initialized\n";);
+        IF_VERBOSE(11, verbose_stream() << "Blocker: " << blocker << " - " << min_core << "\n";);
+        if (min_core_valid && blocker.size() > min_core.size()) {
+            pop_to_base_level();
+            push();
+            m_assumption_set.reset();
+            m_assumptions.reset();
+            for (unsigned i = 0; i < min_core.size(); ++i) {
+                literal lit = min_core[i];
+                SASSERT(is_external(lit.var()));  
+                m_assumption_set.insert(lit);       
+                m_assumptions.push_back(lit);       
+                assign(lit, justification());       
+            }
+            propagate(false);
+            SASSERT(inconsistent());
         }
         return true;
     }
@@ -2510,6 +2575,7 @@ namespace sat {
     //
     // -----------------------
     bool solver::check_invariant() const {
+        if (m_cancel) return true;
         integrity_checker checker(*this);
         SASSERT(checker());
         return true;
@@ -2630,7 +2696,7 @@ namespace sat {
         out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
 
         for (unsigned i = 0; i < m_trail.size(); i++) {
-            out << dimacs_lit(m_trail[i]) << " 0\n";
+            out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
         }
         vector<watch_list>::const_iterator it  = m_watches.begin();
         vector<watch_list>::const_iterator end = m_watches.end();

src/sat/sat_solver.h

@@ -175,6 +175,7 @@ namespace sat {
         //
         // -----------------------
         bool_var mk_var(bool ext = false, bool dvar = true);
+        void mk_clause(literal_vector const& lits) { mk_clause(lits.size(), lits.c_ptr()); }
         void mk_clause(unsigned num_lits, literal * lits);
         void mk_clause(literal l1, literal l2);
         void mk_clause(literal l1, literal l2, literal l3);
@@ -296,8 +297,12 @@ namespace sat {
         bool_var next_var();
         lbool bounded_search();
         void init_search();
+        
+        literal m_replay_lit;
+        literal_vector m_replay_clause;
         void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
-        bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, svector<literal>& blocker);
+        bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
+        void resolve_weighted();
         void reinit_assumptions();
         bool tracking_assumptions() const;
         bool is_assumption(literal l) const;

src/sat/sat_types.h

@@ -228,6 +228,7 @@ namespace sat {
             return result;
         }
         void insert(literal l) { m_set.insert(l.index()); }
+        literal pop() { return to_literal(m_set.erase()); }
         bool contains(literal l) const { return m_set.contains(l.index()); }
         bool empty() const { return m_set.empty(); }
         unsigned size() const { return m_set.size(); }

src/smt/asserted_formulas.cpp

@@ -252,6 +252,7 @@ void asserted_formulas::reduce() {
     TRACE("before_reduce", display(tout););
     CASSERT("well_sorted", check_well_sorted());
 
+
 #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); }  TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return;  }
     
     set_eliminate_and(false); // do not eliminate and before nnf.

src/smt/smt_conflict_resolution.cpp

@@ -115,8 +115,7 @@ namespace smt {
             break;
         case eq_justification::CONGRUENCE: {
             TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " congruence\n";);
-            if (!lhs->is_eq())
+            CTRACE("dyn_ack_target", !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";);
-                TRACE("dyn_ack_target", tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";);
             m_dyn_ack_manager.used_cg_eh(lhs->get_owner(), rhs->get_owner());
             unsigned num_args = lhs->get_num_args();
             SASSERT(num_args == rhs->get_num_args());

src/smt/smt_setup.cpp

@@ -52,6 +52,7 @@ namespace smt {
         // }
         TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";);
         m_already_configured = true;
+        
         switch (cm) {
         case CFG_BASIC: setup_unknown(); break;
         case CFG_LOGIC: setup_default(); break;
@@ -550,6 +551,7 @@ namespace smt {
         m_params.m_bv_cc               = false;
         m_params.m_bb_ext_gates        = true;
         m_params.m_nnf_cnf             = false;
+        m_params.m_propagate_booleans  = true;
         m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
         m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
     }

src/smt/tactic/smt_tactic.cpp

@@ -161,9 +161,11 @@ public:
     
     struct scoped_init_ctx {
         smt_tactic & m_owner;
+        smt_params   m_params; // smt-setup overwrites parameters depending on the current assertions.
 
         scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
-            smt::kernel * new_ctx = alloc(smt::kernel, m, o.fparams());
+            m_params = o.fparams();
+            smt::kernel * new_ctx = alloc(smt::kernel, m, m_params);
             TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
             new_ctx->set_logic(o.m_logic);
             if (o.m_callback) {
@@ -199,7 +201,8 @@ public:
                   << " PREPROCESS: " << fparams().m_preprocess << "\n";
                   tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
                   tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
-                  tout << "params_ref: " << m_params_ref << "\n";);
+                  tout << "params_ref: " << m_params_ref << "\n";
+                  tout << "nnf: " << fparams().m_nnf_cnf << "\n";);
             TRACE("smt_tactic_detail", in->display(tout););
             TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);        
             scoped_init_ctx  init(*this, m);
@@ -239,7 +242,6 @@ public:
             else
                 r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
             m_ctx->collect_statistics(m_stats);
-            
             switch (r) {
             case l_true: {
                 if (m_fail_if_inconclusive && !in->sat_preserved())

src/smt/theory_dl.cpp

@@ -235,13 +235,14 @@ namespace smt {
         }
 
         app* mk_bv_constant(uint64 val, sort* s) {
-            return b().mk_numeral(rational(val,rational::ui64()),64);
+            return b().mk_numeral(rational(val, rational::ui64()), 64);
         }
 
         app* max_value(sort* s) {
             uint64 sz;
             VERIFY(u().try_get_size(s, sz));
-            return mk_bv_constant(sz, s);
+            SASSERT(sz > 0);
+            return mk_bv_constant(sz-1, s);
         }
 
         void mk_lt(app* x, app* y) {

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -28,6 +28,7 @@ Notes:
 #include"rewriter_def.h"
 #include"for_each_expr.h"
 #include"cooperate.h"
+#include"bv_rewriter.h"
 
 class bv1_blaster_tactic : public tactic {
 
@@ -491,6 +492,8 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
 class is_qfbv_eq_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
+        bv_rewriter rw(g.m());
+        if (!rw.hi_div0()) return false;
         bv1_blaster_tactic t(g.m());
         return t.is_target(g);
 

src/tactic/probe.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"goal_util.h"
+#include"bv_rewriter.h"
 
 class memory_probe : public probe {
 public:
@@ -303,6 +304,8 @@ public:
 class is_qfbv_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
+        bv_rewriter rw(g.m());
+        if (!rw.hi_div0()) return false;
         return !test<is_non_qfbv_predicate>(g);
     }
 };