improve parser error message over API, streamline names of statistics for arithmetic solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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/opt/opt_solver.cpp

@@ -47,6 +47,7 @@ namespace opt {
         m_first(true),
         m_was_unknown(false) {
         m_params.updt_params(p);
+        std::cout << "Case split strategy " << m_params.m_case_split_strategy << "\n";
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
             m_params.m_relevancy_lvl = 0;
         }

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);
     }