integrating changes of Nikolaj with m_empty_clause etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/horner.cpp

@@ -72,7 +72,7 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
 template <typename T> 
 bool horner::lemmas_on_row(const T& row) {
     cross_nested cn(
-        [this](const nex* n) { return m_intervals->check_cross_nested_expr(n,  m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); },
+        [this](const nex* n) { return m_intervals->check_nex(n,  m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); },
         [this](unsigned j)   { return c().var_is_fixed(j); },
         [this]() { return c().random(); }, m_nex_creator);
 

src/math/lp/nla_grobner.cpp

@@ -453,7 +453,7 @@ void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equatio
 }
 
 void nla_grobner::check_eq(equation* target) {
-    if(m_intervals->check_cross_nested_expr(target->expr(), target->dep())) {
+    if(m_intervals->check_nex(target->expr(), target->dep())) {
         TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
               tout << "vars = \n";
               for (lpvar j : get_vars_of_expr(target->expr())) {

src/math/lp/nla_intervals.cpp

@@ -244,19 +244,19 @@ intervals::interv intervals::interval_of_mul(const nex_mul* e) {
     return a;
 }
 
-
+// return true iff the interval of n is does not contain 0
-bool intervals::check_cross_nested_expr(const nex* n, ci_dependency* initial_deps) {
+bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) {
-    TRACE("nla_intervals", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
+    TRACE("nla_grobner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
     m_core->lp_settings().stats().m_cross_nested_forms++;
 
     auto i = interval_of_expr(n, 1);
-    TRACE("nla_intervals", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";);
+    TRACE("nla_grobner", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";);
     if (!separated_from_zero(i)) {
         reset();
         return false;
     }
     auto interv_wd = interval_of_expr_with_deps(n, 1);
-    TRACE("nla_intervals", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";);
+    TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";);
     check_interval_for_conflict_on_zero(interv_wd, initial_deps);
     reset(); // clean the memory allocated by the interval bound dependencies
     return true;

src/math/lp/nla_intervals.h

@@ -452,7 +452,7 @@ public:
         return false;
     }
     void reset() { m_alloc.reset(); }
-    bool check_cross_nested_expr(const nex*, ci_dependency*);
+    bool check_nex(const nex*, ci_dependency*);
     interval interval_of_expr_with_deps(const nex* e, unsigned power);
     interval interval_of_expr(const nex* e, unsigned power);
     interval interval_of_sum(const nex_sum*);

src/smt/smt_context.cpp

@@ -75,6 +75,7 @@ namespace smt {
         m_phase_default(false),
         m_conflict(null_b_justification),
         m_not_l(null_literal),
+        m_empty_clause(false),
         m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
         m_unsat_proof(m),
         m_dyn_ack_manager(*this, p),
@@ -2396,9 +2397,10 @@ namespace smt {
                     m_unsat_proof = nullptr;
                 }
                 m_base_scopes.shrink(new_lvl);
+                m_empty_clause = false;
             }
             else {
-                m_conflict = null_b_justification;
+                m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
                 m_not_l = null_literal;
             }
             del_clauses(m_aux_clauses, s.m_aux_clauses_lim);

src/smt/smt_context.h

@@ -193,6 +193,7 @@ namespace smt {
         // levels survives to the base level.
         b_justification             m_conflict;
         literal                     m_not_l;
+        bool                        m_empty_clause;
         scoped_ptr<conflict_resolution> m_conflict_resolution;
         proof_ref                   m_unsat_proof;
 

src/smt/theory_lra.cpp

@@ -165,6 +165,7 @@ class theory_lra::imp {
     ast_manager&         m;
     theory_arith_params& m_arith_params;
     arith_util           a;
+    unsigned             m_final_check_idx;
     arith_eq_adapter     m_arith_eq_adapter;
     vector<rational>     m_columns;
       
@@ -943,6 +944,7 @@ public:
         th(th), m(m), 
         m_arith_params(ap), 
         a(m),
+        m_final_check_idx(0), 
         m_arith_eq_adapter(th, ap, a),            
         m_internalize_head(0),
         m_one_var(UINT_MAX),
@@ -1651,7 +1653,9 @@ public:
         if (lp().get_status() != lp::lp_status::OPTIMAL) {
             is_sat = make_feasible();
         }
+
         final_check_status st = FC_DONE;
+        unsigned old_idx = m_final_check_idx;
         switch (is_sat) {
         case l_true:
                 
@@ -1659,6 +1663,7 @@ public:
                 return FC_CONTINUE;
             }
                    
+
             TRACE("arith", display(tout););
             switch (check_lia()) {
             case l_true:
@@ -1680,19 +1685,18 @@ public:
                 TRACE("arith", tout << "check-nra giveup\n";);
                 st = FC_GIVEUP;
                 break;
+            }
+             if (assume_eqs()) {
+                return FC_CONTINUE;
             }    
             if (m_not_handled != nullptr) {
                 TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);        
                 st = FC_GIVEUP;
             }
                 
-            if (assume_eqs()) {
-                return FC_CONTINUE;
-            }            
-                
             return st;
         case l_false:
-            get_infeasibility_explanation_and_set_conflict();
+            set_conflict();
             return FC_CONTINUE;
         case l_undef:
             TRACE("arith", tout << "check feasiable is undef\n";);
@@ -1701,6 +1705,7 @@ public:
             UNREACHABLE();
             break;
         }
+
         TRACE("arith", tout << "default giveup\n";);
         return FC_GIVEUP;
     }
@@ -2172,7 +2177,7 @@ public:
             for(const nla::lemma & l : lv) {
                 m_lemma = l; //todo avoid the copy
                 m_explanation = l.expl();
-                m_stats.m_nla_explanations += l.expl().size();
+                m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
                 false_case_of_check_nla();
             }
             break;
@@ -2771,10 +2776,14 @@ public:
             bool sign = ub->get_bound_kind() != lp_api::upper_t;
             lit2 = literal(ub->get_bv(), sign);
         }
+        if (ctx().get_assignment(lit2) == l_true) {
+            return;
+        }
         TRACE("arith", 
               ctx().display_literal_verbose(tout, lit1);
-              ctx().display_literal_verbose(tout << " => ", lit2);
+              ctx().display_literal_verbose(tout << " => ", lit2) << "\n";
-              tout << "\n";);
+              tout << ctx().get_assignment(lit2) << " " << ctx().get_assignment(lit1) << "\n";
+              );
         updt_unassigned_bounds(v, -1);
         ++m_stats.m_bound_propagations2;
         m_params.reset();
@@ -2974,15 +2983,15 @@ public:
         auto vi = register_theory_var_in_lar_solver(b.get_var());
         rational bound = b.get_value();
         lp::constraint_index ci;
-        TRACE("arith", tout << "v" << b.get_var() << ", vi =  " << vi;);
+        TRACE("arith", tout << "v" << b.get_var() << ", vi =  " << vi << "\n";);
         if (is_int && !is_true) {
             rational bound = b.get_value(false).get_rational();
             ci = m_solver->add_var_bound(vi, k, bound);
-            TRACE("arith", tout << "\bbound = " << bound << ", ci = " << ci << "\n";);
+            TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";);
         }
         else {
             ci = m_solver->add_var_bound(vi, k, b.get_value());
-            TRACE("arith", tout << "\nbound = " << bound << ", ci = " << ci << "\n";);
+            TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";);
         }
         add_ineq_constraint(ci, literal(bv, !is_true));
         if (is_infeasible()) {