Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

src/ast/ast.cpp

@@ -2254,9 +2254,10 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const
     }
     else {
         string_buffer<64> buffer;
-        buffer << prefix;
         if (prefix == symbol::null)
             buffer << "sk";
+        else
+            buffer << prefix;
         buffer << "!";
         if (suffix != symbol::null)
             buffer << suffix << "!";

src/ast/bv_decl_plugin.cpp

@@ -717,7 +717,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
     op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT));
     op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
 
-    if (logic == symbol::null) {
+    if (logic == symbol::null || logic == "QF_FD") {
         op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
         op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
         op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));

src/sat/ba_solver.cpp

@@ -2396,7 +2396,7 @@ namespace sat {
             init_use_lists();
             remove_unused_defs();
             set_non_external();
-            elim_pure();
+            if (get_config().m_elim_vars) elim_pure();
             for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
             cleanup_clauses();

src/sat/sat_config.cpp

@@ -19,6 +19,8 @@ Revision History:
 #include "sat/sat_config.h"
 #include "sat/sat_types.h"
 #include "sat/sat_params.hpp"
+#include "sat/sat_simplifier_params.hpp"
+
 
 namespace sat {
 
@@ -39,6 +41,7 @@ namespace sat {
         m_local_search = 0;
         m_lookahead_search = false;
         m_lookahead_simplify = false;
+        m_elim_vars = false;
         updt_params(p); 
     }
 
@@ -188,6 +191,9 @@ namespace sat {
         }
         m_dimacs_display  = p.dimacs_display();
         m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
+
+        sat_simplifier_params sp(_p);
+        m_elim_vars = sp.elim_vars();
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_config.h

@@ -133,6 +133,10 @@ namespace sat {
         double             m_step_size_min;
         double             m_reward_multiplier;
         double             m_reward_offset;
+
+        // simplifier configurations used outside of sat_simplifier
+        bool               m_elim_vars;
+
         config(params_ref const & p);
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);

src/sat/sat_elim_vars.cpp

@@ -303,17 +303,16 @@ namespace sat{
 
     bdd elim_vars::make_clauses(clause_use_list & occs) {
         bdd result = m.mk_true();       
-        clause_use_list::iterator it = occs.mk_iterator();
+        for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) {
-        while (!it.at_end()) {
             clause const& c = it.curr();
-            if (c.is_blocked()) continue;
+            if (!c.is_blocked()) {
                 bdd cl = m.mk_false();
                 for (literal l : c) {
                     cl |= mk_literal(l);
                 }           
-            it.next();
                 result &= cl;
             }
+        }
         return result;
     }
 

src/sat/sat_simplifier.cpp

@@ -418,8 +418,7 @@ namespace sat {
                                             literal target) {
         if (c1.is_blocked()) return;
         clause_use_list const & cs = m_use_list.get(target);
-        clause_use_list::iterator it = cs.mk_iterator();
+        for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
-        while (!it.at_end()) {
             clause & c2 = it.curr();
             CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";);
             SASSERT(!c2.was_removed());
@@ -433,7 +432,6 @@ namespace sat {
                     out_lits.push_back(l);
                 }
             }
-            it.next();
         }
     }
 
@@ -532,7 +530,7 @@ namespace sat {
         if (c1.is_blocked()) return;
         clause_use_list const & cs = m_use_list.get(target);
         clause_use_list::iterator it = cs.mk_iterator();
-        while (!it.at_end()) {
+        for (; !it.at_end(); it.next()) {
             clause & c2 = it.curr();
             SASSERT(!c2.was_removed());
             if (&c2 != &c1 &&
@@ -543,7 +541,6 @@ namespace sat {
                     out.push_back(&c2);
                 }
             }
-            it.next();
         }
     }
 
@@ -652,31 +649,18 @@ namespace sat {
         unsigned new_trail_sz = s.m_trail.size();
         for (unsigned i = old_trail_sz; i < new_trail_sz; i++) {
             literal l = s.m_trail[i];
-            {
             // put clauses with literals assigned to false back into todo-list
-                clause_use_list & cs = m_use_list.get(~l);
+            for (auto it = m_use_list.get(~l).mk_iterator(); !it.at_end(); it.next()) {
-                clause_use_list::iterator it = cs.mk_iterator();
+                m_sub_todo.insert(it.curr());
-                while (!it.at_end()) {
-                    clause & c = it.curr();
-                    it.next();
-                    m_sub_todo.insert(c);
             }
-            }
-            {
-                // erase satisfied clauses
             clause_use_list& cs = m_use_list.get(l);
-                {
+            for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
-                    clause_use_list::iterator it = cs.mk_iterator();
-                    while (!it.at_end()) {
                 clause & c = it.curr();
-                        it.next();
                 remove_clause(c, l);
             }
-                }
             cs.reset();            
         }
     }
-    }
 
     void simplifier::elim_lit(clause & c, literal l) {
         TRACE("elim_lit", tout << "processing: " << c << "\n";);
@@ -1086,7 +1070,7 @@ namespace sat {
             for (; !it.at_end(); it.next()) {
                 bool tautology = false;
                 clause & c = it.curr();
-                if (c.is_blocked()) continue;
+                if (c.is_blocked() && !adding) continue;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
                         tautology = true;
@@ -1338,10 +1322,12 @@ namespace sat {
                 }                
                 if (!found) {
                     IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
-                    watched w(l2, true);
+                    watched w1(l2, false);
-                    s.get_wlist(~l).push_back(w);
+                    w1.set_blocked();
-                    w = watched(l, true);
+                    watched w2(l, false);
-                    s.get_wlist(~l2).push_back(w);
+                    w2.set_blocked();
+                    s.get_wlist(~l).push_back(w1);
+                    s.get_wlist(~l2).push_back(w2);
                     ++s.m_num_bca;
                 }
             }
@@ -1471,32 +1457,21 @@ namespace sat {
     void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) {
         clause_use_list const & cs = m_use_list.get(l);
         clause_use_list::iterator it = cs.mk_iterator();
-        while (!it.at_end()) {
+        for (; !it.at_end(); it.next()) {
             if (!it.curr().is_blocked() || include_blocked) {
                 r.push_back(clause_wrapper(it.curr()));
                 SASSERT(r.back().size() == it.curr().size());
             }
-            it.next();
         }
 
         watch_list & wlist = get_wlist(~l);
-        if (include_blocked) {
         for (auto & w : wlist) {
-                if (w.is_binary_non_learned_clause2()) {
+            if (include_blocked ? w.is_binary_non_learned_clause() : w.is_binary_unblocked_clause()) {
                 r.push_back(clause_wrapper(l, w.get_literal()));
                 SASSERT(r.back().size() == 2);
             }
         }
     }
-        else {
-            for (auto & w : wlist) {
-                if (w.is_binary_unblocked_clause()) {
-                    r.push_back(clause_wrapper(l, w.get_literal()));
-                    SASSERT(r.back().size() == 2);
-                }
-            }
-        }
-    }
 
     /**
        \brief Resolve clauses c1 and c2.
@@ -1605,8 +1580,7 @@ namespace sat {
        \brief Eliminate the clauses where the variable being eliminated occur.
     */
     void simplifier::remove_clauses(clause_use_list const & cs, literal l) {
-        clause_use_list::iterator it  = cs.mk_iterator();
+        for (auto it = cs.mk_iterator(); !it.at_end(); ) {
-        while (!it.at_end()) {
             clause & c = it.curr();
             it.next();
             SASSERT(c.contains(l));
@@ -1639,22 +1613,14 @@ namespace sat {
 
         unsigned before_lits = num_bin_pos*2 + num_bin_neg*2;
 
-        {
+        for (auto it = pos_occs.mk_iterator(); !it.at_end(); it.next()) {
-            clause_use_list::iterator it = pos_occs.mk_iterator();
-            while (!it.at_end()) {
             if (!it.curr().is_blocked())
                 before_lits += it.curr().size();
-                it.next();
-            }
         }
 
-        {
+        for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
-            clause_use_list::iterator it2 = neg_occs.mk_iterator();
+            if (!it.curr().is_blocked())
-            while (!it2.at_end()) {
+                before_lits += it.curr().size();
-                if (!it2.curr().is_blocked())
-                    before_lits += it2.curr().size();
-                it2.next();
-            }
         }
 
         TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";);

src/sat/sat_solver.cpp

@@ -1553,8 +1553,10 @@ namespace sat {
 
 // #ifndef _EXTERNAL_RELEASE
         IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
-        if (!check_model(m_model))
+        if (!check_model(m_model)) {
+            UNREACHABLE();
             throw solver_exception("check model failed");
+        }
 
         if (m_clone) {
             IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
@@ -1576,6 +1578,9 @@ namespace sat {
                       tout << "model: " << m << "\n";
                       m_mc.display(tout);
                       );
+                for (literal l : c) {
+                    if (was_eliminated(l.var())) IF_VERBOSE(0, verbose_stream() << "eliminated: " << l << "\n";);
+                }
                 ok = false;
             }
         }
@@ -1588,7 +1593,7 @@ namespace sat {
                         continue;
                     literal l2 = w.get_literal();
                     if (value_at(l2, m) != l_true) {
-                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << " "  << "\n";);
+                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << "\n";);
                         TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
                         ok = false;
                     }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -511,7 +511,6 @@ public:
         }
         m_internalized_fmls.reset();
         g.get_formulas(m_internalized_fmls);
-        // g.display(std::cout);
         m_internalized_converted = true;
         // if (mc) mc->display(std::cout << "mc");
         // if (m_mc) m_mc->display(std::cout << "m_mc\n");

src/sat/sat_watched.h

@@ -88,7 +88,7 @@ namespace sat {
 
         bool is_binary_unblocked_clause() const { return m_val2 == 0; }
         bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
-        bool is_binary_non_learned_clause2() const { return is_binary_clause() && !is_learned(); }
+        bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); }
 
         void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
         void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); }

src/sat/tactic/goal2sat.cpp

@@ -1063,7 +1063,7 @@ struct sat2goal::imp {
         for (sat::literal l : c) {
             lits.push_back(lit2expr(l));
         }
-        expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
+        expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
         
         if (c.lit() != sat::null_literal) {
             fml = m.mk_eq(lit2expr(c.lit()), fml);            
@@ -1135,7 +1135,6 @@ struct sat2goal::imp {
         }
         // collect clauses
         assert_clauses(s, s.clauses(), r, true);
-        assert_clauses(s, s.learned(), r, false);
 
         sat::ba_solver* ext = get_ba_solver(s);
         if (ext) {

src/solver/tactic2solver.cpp

@@ -173,6 +173,10 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
             m_result->set_status(l_undef);
             if (reason_unknown != "")
                 m_result->m_unknown = reason_unknown;
+            if (num_assumptions == 0) {
+                m_assertions.reset();
+                g->get_formulas(m_assertions);
+            }
             break;
         }
     }