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

src/api/api_opt.cpp

@@ -289,6 +289,10 @@ extern "C" {
         //LOG_Z3_optimize_from_file(c, d, s);
         std::ifstream is(s);
         if (!is) {
+            std::ostringstream strm;
+            strm << "Could not open file " << s;
+            throw default_exception(strm.str());
+
             SET_ERROR_CODE(Z3_PARSER_ERROR);
             return;
         }

src/opt/maxsmt.cpp

@@ -350,8 +350,10 @@ namespace opt {
         for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
             expr* e = m_soft_constraints[i];
             bool is_not = m.is_not(e, e);
-            out << mk_pp(e, m)
+            out << m_weights[i] << ": " << mk_pp(e, m)
-                << ((is_not != get_assignment(i))?" |-> true\n":" |-> false\n");
+                << ((is_not != get_assignment(i))?" |-> true ":" |-> false ")
+                << "\n";
+            
         }
     }
     

src/opt/opt_context.cpp

@@ -792,10 +792,14 @@ namespace opt {
                     arg = mk_not(m, arg);
                     offset -= weight;
                 }
-                if (m.is_true(arg) || weight.is_zero()) {
+                if (m.is_true(arg)) {
+                    IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> true\n";);
+                }
+                else if (weight.is_zero()) {
                     // skip
                 }
                 else if (m.is_false(arg)) {
+                    IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> false\n";);
                     offset += weight;
                 }
                 else {

src/sat/sat_config.cpp

@@ -26,6 +26,7 @@ namespace sat {
         m_always_true("always_true"),
         m_always_false("always_false"),
         m_caching("caching"),
+        m_restart_max(0),
         m_random("random"),
         m_geometric("geometric"),
         m_luby("luby"),
@@ -66,7 +67,8 @@ namespace sat {
 
         m_restart_initial = p.restart_initial();
         m_restart_factor  = p.restart_factor();
-        
+        m_restart_max     = p.restart_max();
+
         m_random_freq     = p.random_freq();
         m_random_seed     = p.random_seed();
         if (m_random_seed == 0) 

src/sat/sat_config.h

@@ -52,6 +52,7 @@ namespace sat {
         restart_strategy   m_restart;
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
+        unsigned           m_restart_max;
         double             m_random_freq;
         unsigned           m_random_seed;
         unsigned           m_burst_search;

src/sat/sat_params.pyg

@@ -7,6 +7,7 @@ def_module_params('sat',
                           ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
                           ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
+                          ('restart.max', UINT, 0, 'maximal number of restarts. Ignored if set to 0'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
                           ('random_seed', UINT, 0, 'random seed'),

src/sat/sat_solver.cpp

@@ -744,7 +744,6 @@ namespace sat {
             simplify_problem();
             if (check_inconsistent()) return l_false;
 
-
             if (m_config.m_max_conflicts == 0) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
                 return l_undef;
@@ -766,6 +765,12 @@ namespace sat {
                 simplify_problem();
                 if (check_inconsistent()) return l_false;
                 gc();
+
+                if (m_config.m_restart_max != 0 && m_config.m_restart_max <= m_restarts) {
+                    IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
+                    return l_undef;
+                }
+
             }
         }
         catch (abort_solver) {
@@ -1126,6 +1131,7 @@ namespace sat {
         m_restart_threshold       = m_config.m_restart_initial;
         m_luby_idx                = 1;
         m_gc_threshold            = m_config.m_gc_initial;
+        m_restarts                = 0;
         m_min_d_tk                = 1.0;
         m_stopwatch.reset();
         m_stopwatch.start();
@@ -1308,6 +1314,7 @@ namespace sat {
 
     void solver::restart() {
         m_stats.m_restart++;
+        m_restarts++;
         IF_VERBOSE(1,
                    verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
                    << " :restarts " << m_stats.m_restart << mk_stat(*this)

src/sat/sat_solver.h

@@ -293,6 +293,7 @@ namespace sat {
 
     protected:
         unsigned m_conflicts;
+        unsigned m_restarts;
         unsigned m_conflicts_since_restart;
         unsigned m_restart_threshold;
         unsigned m_luby_idx;

src/smt/arith_eq_adapter.cpp

@@ -264,7 +264,7 @@ namespace smt {
     }
 
     void arith_eq_adapter::collect_statistics(::statistics & st) const {
-        st.update("eq adapter", m_stats.m_num_eq_axioms);
+        st.update("arith eq adapter", m_stats.m_num_eq_axioms);
     }
 
     void arith_eq_adapter::display_already_processed(std::ostream & out) const {

src/smt/theory_arith_core.h

@@ -465,7 +465,7 @@ namespace smt {
               tout << s_ante << "\n" << s_conseq << "\n";);
 
         literal lits[2] = {l_ante, l_conseq};
-        ctx.mk_th_axiom(get_id(), 2, lits);
+        mk_clause(l_ante, l_conseq, 0, 0);
         if (ctx.relevancy()) {
             if (l_ante == false_literal) {
                 ctx.mark_as_relevant(l_conseq);
@@ -934,11 +934,13 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) {
+        TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; get_context().display_literals_verbose(tout, 2, lits); tout << "\n";);
         get_context().mk_th_axiom(get_id(), l1, l2, num_params, params);
     }
 
     template<typename Ext>
     void theory_arith<Ext>::mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
+        TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; get_context().display_literals_verbose(tout, 3, lits); tout << "\n";);
         get_context().mk_th_axiom(get_id(), l1, l2, l3, num_params, params);
     }
 

src/smt/theory_arith_eq.h

@@ -44,6 +44,7 @@ namespace smt {
         SASSERT(lower_bound(v).is_rational());
         numeral const & val = lower_bound(v).get_rational();
         value_sort_pair key(val, is_int_src(v));
+        TRACE("arith_eq", tout << mk_pp(get_enode(v)->get_owner(), get_manager()) << " = " << val << "\n";);
         theory_var v2;
         if (m_fixed_var_table.find(key, v2)) {
             if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
@@ -247,6 +248,7 @@ namespace smt {
                     //
                     // x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2
                     // 
+                    TRACE("arith_eq_propagation", tout << "fixed\n";);
                     lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     m_stats.m_fixed_eqs++;
@@ -324,28 +326,42 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
         // Ignore equality if variables are already known to be equal.
+        ast_manager& m = get_manager();
         if (is_equal(x, y))
             return;
         // I doesn't make sense to propagate an equality (to the core) of variables of different sort.
-        if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) {
+        if (m.get_sort(var2expr(x)) != m.get_sort(var2expr(y))) {
-            TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";);
+            TRACE("arith", tout << mk_pp(var2expr(x), m) << " = " << mk_pp(var2expr(y), m) << "\n";);
             return;
         }
         context & ctx      = get_context();
         region & r         = ctx.get_region();
         enode * _x         = get_enode(x);
         enode * _y         = get_enode(y);
+        eq_vector const& eqs = antecedents.eqs();
+        literal_vector const& lits = antecedents.lits();
         justification * js = 
             ctx.mk_justification(
                 ext_theory_eq_propagation_justification(
                     get_id(), r, 
-                    antecedents.lits().size(), antecedents.lits().c_ptr(),
+                    lits.size(), lits.c_ptr(),
-                    antecedents.eqs().size(), antecedents.eqs().c_ptr(),
+                    eqs.size(), eqs.c_ptr(),
                     _x, _y, 
                     antecedents.num_params(), antecedents.params("eq-propagate")));
         TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
               display_var(tout, x);
               display_var(tout, y););
+        TRACE("arith_eq_propagation",
+              for (unsigned i = 0; i <  lits.size(); ++i) {
+                  ctx.display_detailed_literal(tout, lits[i]);
+                  tout << "\n";
+              } 
+              for (unsigned i = 0; i < eqs.size(); ++i) {
+                  tout << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
+              } 
+              tout << " ==> ";
+              tout << mk_pp(_x->get_owner(), m) << " = " << mk_pp(_y->get_owner(), m) << "\n";
+              );
         ctx.assign_eq(_x, _y, eq_justification(js));
     }
 };

src/smt/theory_arith_pp.h

@@ -27,22 +27,22 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::collect_statistics(::statistics & st) const {
         st.update("arith conflicts", m_stats.m_conflicts);
-        st.update("add rows", m_stats.m_add_rows);
+        st.update("arith add rows", m_stats.m_add_rows);
-        st.update("pivots", m_stats.m_pivots);
+        st.update("arith pivots", m_stats.m_pivots);
-        st.update("assert lower", m_stats.m_assert_lower);
+        st.update("arith assert lower", m_stats.m_assert_lower);
-        st.update("assert upper", m_stats.m_assert_upper);
+        st.update("arith assert upper", m_stats.m_assert_upper);
-        st.update("assert diseq", m_stats.m_assert_diseq);
+        st.update("arith assert diseq", m_stats.m_assert_diseq);
-        st.update("bound prop", m_stats.m_bound_props);
+        st.update("arith bound prop", m_stats.m_bound_props);
-        st.update("fixed eqs", m_stats.m_fixed_eqs);
+        st.update("arith fixed eqs", m_stats.m_fixed_eqs);
-        st.update("offset eqs", m_stats.m_offset_eqs);
+        st.update("arith offset eqs", m_stats.m_offset_eqs);
-        st.update("gcd tests", m_stats.m_gcd_tests);
+        st.update("arith gcd tests", m_stats.m_gcd_tests);
-        st.update("ineq splits", m_stats.m_branches);
+        st.update("arith ineq splits", m_stats.m_branches);
-        st.update("gomory cuts", m_stats.m_gomory_cuts);
+        st.update("arith gomory cuts", m_stats.m_gomory_cuts);
-        st.update("max-min", m_stats.m_max_min);
+        st.update("arith max-min", m_stats.m_max_min);
-        st.update("grobner", m_stats.m_gb_compute_basis);
+        st.update("arith grobner", m_stats.m_gb_compute_basis);
-        st.update("pseudo nonlinear", m_stats.m_nl_linear);
+        st.update("arith pseudo nonlinear", m_stats.m_nl_linear);
-        st.update("nonlinear bounds", m_stats.m_nl_bounds);
+        st.update("arith nonlinear bounds", m_stats.m_nl_bounds);
-        st.update("nonlinear horner", m_stats.m_nl_cross_nested);
+        st.update("arith nonlinear horner", m_stats.m_nl_cross_nested);
         m_arith_eq_adapter.collect_statistics(st);
     }
 

src/smt/theory_pb.cpp

@@ -808,6 +808,7 @@ namespace smt {
     void theory_pb::assign_eh(bool_var v, bool is_true) {
         ptr_vector<ineq>* ineqs = 0;
         literal nlit(v, is_true);
+        init_watch(v);
         TRACE("pb", tout << "assign: " << ~nlit << "\n";);
         ineqs = m_var_infos[v].m_lit_watch[nlit.sign()];
         if (ineqs != 0) {