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

src/opt/maxres.cpp

@@ -171,7 +171,7 @@ public:
     }
 
     void new_assumption(expr* e, rational const& w) {
-        IF_VERBOSE(3, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";);
+        IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";);
         TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";);
         m_asm2weight.insert(e, w);
         m_asms.push_back(e);
@@ -186,7 +186,6 @@ public:
         init();
         init_local();
         trace();
-        display();
         while (m_lower < m_upper) {
             TRACE("opt", 
                   display_vec(tout, m_asms);
@@ -220,7 +219,6 @@ public:
         init();
         init_local();
         trace();
-        display();
         exprs cs;
         while (m_lower < m_upper) {
             lbool is_sat = check_sat_hill_climb(m_asms);
@@ -253,14 +251,6 @@ public:
         return l_true;
     }
 
-    void display() {
-        if (m_dump_benchmarks && m_c.sat_enabled()) {
-            unsigned sz = m_soft.size();
-            inc_sat_display(verbose_stream(), s(), sz, 
-                            m_soft.c_ptr(), m_weights.c_ptr());
-        }
-    }
-
 
     lbool check_sat_hill_climb(expr_ref_vector& asms1) {
         expr_ref_vector asms(asms1);

src/opt/maxsls.cpp

@@ -20,6 +20,8 @@ Notes:
 #include "maxsls.h"
 #include "ast_pp.h"
 #include "model_smt2_pp.h"
+#include "opt_context.h"
+#include "inc_sat_solver.h"
 
 
 namespace opt {
@@ -34,7 +36,7 @@ namespace opt {
             IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
             init();
             enable_sls(true);
-            lbool is_sat = s().check_sat(0, 0);
+            lbool is_sat = check();
             if (is_sat == l_true) {
                 s().get_model(m_model);
                 m_upper.reset();
@@ -49,6 +51,16 @@ namespace opt {
             }
             return is_sat;
         }
+        
+        lbool check() {
+            if (m_c.sat_enabled()) {
+                return inc_sat_check_sat(
+                    s(), m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr(), m_upper);
+            }
+            else {
+                return s().check_sat(0, 0);
+            }
+        }
 
     };
 

src/opt/opt_context.cpp

@@ -41,6 +41,7 @@ Notes:
 #include "ast_smt_pp.h"
 #include "filter_model_converter.h"
 #include "ast_pp_util.h"
+#include "inc_sat_solver.h"
 
 namespace opt {
 
@@ -220,7 +221,7 @@ namespace opt {
             TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;);
             s.assert_expr(m_hard_constraints[i].get());
         }
-
+        display_benchmark();
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
         lbool is_sat = s.check_sat(0,0);
         TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
@@ -1069,6 +1070,18 @@ namespace opt {
         }
     }
 
+    void context::display_benchmark() {
+        if (opt_params(m_params).dump_benchmarks() && 
+            sat_enabled() && 
+            m_objectives.size() == 1 &&
+            m_objectives[0].m_type == O_MAXSMT
+            ) {
+            objective& o = m_objectives[0];
+            unsigned sz = o.m_terms.size();
+            inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.c_ptr(), o.m_weights.c_ptr());
+        }
+    }
+
     void context::display(std::ostream& out) {
         display_assignment(out);
     }

src/opt/opt_context.h

@@ -280,6 +280,8 @@ namespace opt {
 
         void validate_lex();
 
+        void display_benchmark();
+
 
         // pareto
         void yield();

src/sat/sat_sls.cpp

@@ -386,6 +386,7 @@ namespace sat {
                     m_best_value = val;
                     m_best_model.reset();
                     m_best_model.append(m_model);
+                    s.set_model(m_best_model);
                     IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
                     if (i*2 > m_max_tries) {
                         m_max_tries *= 2;

src/sat/sat_sls.h

@@ -97,7 +97,6 @@ namespace sat {
         void set_soft(unsigned sz, literal const* lits, double const* weights);        
         bool has_soft() const { return !m_soft.empty(); }
         void opt(unsigned sz, literal const* tabu, bool reuse_model);
-        model const& get_model() { return m_best_model; }
         virtual void display(std::ostream& out) const;
         double evaluate_model(model& mdl);
     private:        

src/sat/sat_solver.cpp

@@ -1105,6 +1105,12 @@ namespace sat {
         }
     }
 
+    void solver::set_model(model const& mdl) {
+        m_model.reset();
+        m_model.append(mdl);
+        m_model_is_current = !m_model.empty();
+    }
+
     void solver::mk_model() {
         m_model.reset();
         m_model_is_current = true;
@@ -1117,8 +1123,6 @@ namespace sat {
         TRACE("sat_mc_bug", m_mc.display(tout););
         if (m_config.m_optimize_model) {
             m_wsls.opt(0, 0, false);
-            m_model.reset();
-            m_model.append(m_wsls.get_model());
         }
         m_mc(m_model);
         TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
@@ -1808,9 +1812,7 @@ namespace sat {
             // apply optional clause minimization by detecting subsumed literals.
             // initial experiment suggests it has no effect.
             m_mus(); // ignore return value on cancelation.
-            m_model.reset();
+            set_model(m_mus.get_model());
-            m_model.append(m_mus.get_model());            
-            m_model_is_current = !m_model.empty();
         }
     }
 

src/sat/sat_solver.h

@@ -280,6 +280,7 @@ namespace sat {
         bool model_is_current() const { return m_model_is_current; }
         literal_vector const& get_core() const { return m_core; }
         model_converter const & get_model_converter() const { return m_mc; }
+        void set_model(model const& mdl);
 
     protected:
         unsigned m_conflicts;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -56,7 +56,7 @@ class inc_sat_solver : public solver {
     proof_converter_ref m_pc;   
     model_converter_ref m_mc2;   
     expr_dependency_ref m_dep_core;
-
+    svector<double>       m_weights;
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -82,8 +82,6 @@ public:
         simp2_p.set_bool("hoist_mul", false); // required by som
         m_preprocess = 
             and_then(mk_card2bv_tactic(m, m_params),
-                     //mk_simplify_tactic(m),
-                     //mk_propagate_values_tactic(m),
                      using_params(mk_simplify_tactic(m), simp2_p),
                      mk_max_bv_sharing_tactic(m),
                      mk_bit_blaster_tactic(m), 
@@ -100,25 +98,32 @@ public:
     }
 
     void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
+        m_weights.reset();
+        if (weights != 0) {
+            for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
+        }
         m_solver.pop_to_base_level();
         dep2asm_t dep2asm;
         VERIFY(l_true == internalize_formulas());
-        VERIFY(l_true == internalize_assumptions(sz, assumptions, 0 != weights, dep2asm));
+        VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm));
         m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights);
     }
  
     lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {       
-
+        m_weights.reset();
+        if (weights != 0) {
+            m_weights.append(sz, weights);
+        }
+        SASSERT(m_weights.empty() == (m_weights.c_ptr() == 0));
         m_solver.pop_to_base_level();
         dep2asm_t dep2asm;
         m_model = 0;
         lbool r = internalize_formulas();
         if (r != l_true) return r;
-        r = internalize_assumptions(sz, assumptions, 0 != weights, dep2asm);
+        r = internalize_assumptions(sz, assumptions, dep2asm);
         if (r != l_true) return r;
 
-        //m_solver.display_dimacs(std::cout);
+        r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
-        r = m_solver.check(m_asms.size(), m_asms.c_ptr(), weights, max_weight);
         switch (r) {
         case l_true:
             if (sz > 0 && !weights) {
@@ -179,7 +184,7 @@ public:
         }
     }
     virtual void assert_expr(expr * t) {
-        TRACE("opt", tout << mk_pp(t, m) << "\n";);
+        TRACE("sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
     virtual void set_produce_models(bool f) {}
@@ -238,9 +243,10 @@ private:
         m_pc.reset();
         m_dep_core.reset();
         m_subgoals.reset();
+        m_preprocess->reset();
         SASSERT(g->models_enabled());
         SASSERT(!g->proofs_enabled());
-        TRACE("opt", g->display(tout););
+        TRACE("sat", g->display(tout););        
         try {                   
             (*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core);
         }
@@ -254,61 +260,26 @@ private:
             return l_undef;
         }
         g = m_subgoals[0];
-        TRACE("opt", g->display_with_dependencies(tout););
+        TRACE("sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         return l_true;
     }
 
-    lbool internalize_assumptions(unsigned sz, expr* const* asms, bool is_weighted, dep2asm_t& dep2asm) {
+    lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
         if (sz == 0) {
             return l_true;
         }
-        if (is_weighted) {
-            return internalize_weighted(sz, asms, dep2asm);
-        }
-        return internalize_unweighted(sz, asms, dep2asm);
-    }
-
-    lbool internalize_unweighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
         goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
-        lbool res = l_undef;
         for (unsigned i = 0; i < sz; ++i) {
             g->assert_expr(asms[i], m.mk_leaf(asms[i]));
         }
-        res = internalize_goal(g, dep2asm);
+        lbool res = internalize_goal(g, dep2asm);
         if (res == l_true) {
-            extract_assumptions(dep2asm);
+            extract_assumptions(sz, asms, dep2asm);
         }        
         return res;
     }
 
-    /*
-      \brief extract weighted assumption literals in the same order as the weights.
-      For this purpose we enforce tha assumptions are literals.
-     */
-    lbool internalize_weighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
-        goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
-        lbool res = l_undef;
-        m_asms.reset();
-        expr_ref_vector lits(m);
-        filter_model_converter_ref fmc = alloc(filter_model_converter, m);
-        for (unsigned i = 0; i < sz; ++i) {
-            expr_ref lit = ensure_literal(g, asms[i], fmc.get());
-            lits.push_back(lit);
-            g->assert_expr(lit, m.mk_leaf(lit));
-        }
-        m_mc = concat(m_mc.get(), fmc.get());
-        res = internalize_goal(g, dep2asm);
-        if (res == l_true) {
-            for (unsigned i = 0; i < lits.size(); ++i) {
-                sat::literal l;
-                VERIFY (dep2asm.find(lits[i].get(), l));
-                m_asms.push_back(l);
-            }
-        }
-        return res;
-    }
-
     lbool internalize_formulas() {
         if (m_fmls_head == m_fmls.size()) {
             return l_true;
@@ -321,39 +292,31 @@ private:
         return internalize_goal(g, dep2asm);
     }
 
-    expr_ref ensure_literal(goal_ref& g, expr* e, filter_model_converter* fmc) {
+    void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
-        expr_ref result(m), fml(m);
-        expr* e1;
-        if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) {
-            result = e;
-        }
-        else {
-            // TBD: need a filter_model_converter to remove
-            result = m.mk_fresh_const("soft", m.mk_bool_sort());
-            fmc->insert(to_app(result)->get_decl());
-            fml = m.mk_implies(result, e);
-            g->assert_expr(fml);
-        }
-        return result;
-    }
-
-    void extract_assumptions(dep2asm_t& dep2asm) {
         m_asms.reset();
-        dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
+        unsigned j = 0;
-        for (; it != end; ++it) {
+        sat::literal lit;
-            m_asms.push_back(it->m_value);
+        for (unsigned i = 0; i < sz; ++i) {
+            if (dep2asm.find(asms[i], lit)) {
+                m_asms.push_back(lit);
+                if (i != j && !m_weights.empty()) {
+                    m_weights[j] = m_weights[i];
+                }
+                ++j;
+            }
         }
-        //IF_VERBOSE(0, verbose_stream() << asms << "\n";);
+        SASSERT(dep2asm.size() == m_asms.size());
     }
 
     void extract_core(dep2asm_t& dep2asm) {
         u_map<expr*> asm2dep;
         dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
         for (; it != end; ++it) {
-            asm2dep.insert(it->m_value.index(), it->m_key);
+            expr* e = it->m_key;
+            asm2dep.insert(it->m_value.index(), e);
         }
         sat::literal_vector const& core = m_solver.get_core();
-        TRACE("opt",
+        TRACE("sat",
               dep2asm_t::iterator it2 = dep2asm.begin();
               dep2asm_t::iterator end2 = dep2asm.end();
               for (; it2 != end2; ++it2) {
@@ -426,7 +389,7 @@ private:
             for (unsigned i = 0; i < m_fmls.size(); ++i) {
                 expr_ref tmp(m);
                 VERIFY(m_model->eval(m_fmls[i].get(), tmp));                
-                CTRACE("opt", !m.is_true(tmp),
+                CTRACE("sat", !m.is_true(tmp),
                        tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) 
                        << " to " << tmp << "\n";
                        model_smt2_pp(tout, m, *(m_model.get()), 0););
@@ -461,3 +424,4 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof
     }
     return s.display_weighted(out, sz, soft, weights.c_ptr());
 }
+

src/tactic/arith/card2bv_tactic.cpp

@@ -24,6 +24,7 @@ Notes:
 #include"card2bv_tactic.h"
 #include"pb_rewriter.h"
 #include"ast_util.h"
+#include"ast_pp.h"
 
 namespace pb {
     unsigned card2bv_rewriter::get_num_bits(func_decl* f) {

src/tactic/core/simplify_tactic.cpp

@@ -18,7 +18,7 @@ Notes:
 --*/
 #include"simplify_tactic.h"
 #include"th_rewriter.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 
 struct simplify_tactic::imp {
     ast_manager &   m_manager;
@@ -65,6 +65,9 @@ struct simplify_tactic::imp {
                 proof * pr = g.pr(idx);
                 new_pr     = m().mk_modus_ponens(pr, new_pr);
             }
+            if (m_manager.is_false(new_curr)) {
+                std::cout << mk_pp(curr, m_manager) << " => " << new_curr << "\n";
+            }
             g.update(idx, new_curr, new_pr, g.dep(idx));
         }
         TRACE("after_simplifier_bug", g.display(tout););