avoid patching vars in powers

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

src/ast/ast.cpp

@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
     if (n->get_id() != id) return;
     ++s_count;
     std::cout << s_count << "\n";
-    SASSERT(s_count != 1);
+    //SASSERT(s_count != 1);
 }
 #endif
 
@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-    // track_id(n, 2147483792);
+    // track_id(n, 70);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);

src/math/lp/lar_solver.cpp

@@ -2395,9 +2395,7 @@ bool lar_solver::inside_bounds(lpvar j, const impq& val) const {
 
 bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool (lpvar)>& blocker, const std::function<void (lpvar)>& report_change) {
     if (is_base(j)) {        
-        bool r = remove_from_basis(j);
+        VERIFY(remove_from_basis(j));
-        SASSERT(r);
-        (void)r;        
     }
     impq ival(val);
     if (!inside_bounds(j, ival))
@@ -2409,10 +2407,10 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
         const mpq & a = c.coeff();        
         unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
         impq rj_new_val = a * delta + get_column_value(rj);
-        if (column_is_int(rj) && ! rj_new_val.is_int())
+        if (column_is_int(rj) && !rj_new_val.is_int())
-            return  false;
+            return false;
         if (!inside_bounds(rj, rj_new_val) || blocker(rj))
-            return  false;
+            return false;
     }
 
     set_column_value(j, ival);
@@ -2423,6 +2421,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
         m_mpq_lar_core_solver.m_r_solver.add_delta_to_x(rj, a * delta);
         report_change(rj);
     }
+
     return true;
 }
 

src/math/lp/monic.h

@@ -16,6 +16,7 @@
 #include "util/vector.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/nla_defs.h"
+#include <algorithm>
 namespace nla {
 
 class mon_eq {
@@ -38,7 +39,15 @@ public:
     unsigned size() const { return m_vs.size(); }
     const svector<lp::var_index>& vars() const { return m_vs; }
     bool empty() const { return m_vs.empty(); }
-
+    bool is_sorted() const {
+        for (unsigned i = 0; i + 1 < size(); i++)
+            if (m_vs[i] > m_vs[i + 1])
+                return false;
+        return true;
+    }
+    bool contains_var(lpvar j) const {
+        return std::binary_search(m_vs.begin(), m_vs.end(), j);
+    }
 protected:
     svector<lp::var_index>& vars1() { return m_vs; }
 };

src/math/lp/nla_core.cpp

@@ -1331,72 +1331,94 @@ bool core::elists_are_consistent(bool check_in_model) const {
 }
 
 bool core::var_is_used_in_a_correct_monic(lpvar j) const {
+    if (emons().is_monic_var(j)) {
+        if (!m_to_refine.contains(j))
+            return true;
+    }
     for (const monic & m : emons().get_use_list(j)) {
         if (!m_to_refine.contains(m.var())) {
             TRACE("nla_solver", tout << "j" << j << " is used in a correct monic \n";);
             return true;
         }
     }
+
     return false;
 }
 
 void core::update_to_refine_of_var(lpvar j) {
     for (const monic & m : emons().get_use_list(j)) {
-        if (val(var(m)) == mul_val(m))
+        if (var_val(m) == mul_val(m)) 
             m_to_refine.erase(var(m));
         else
             m_to_refine.insert(var(m));
     }
     if (is_monic_var(j)) {
         const monic& m = emons()[j];
-        if (val(var(m)) == mul_val(m))
+        if (var_val(m) == mul_val(m))
             m_to_refine.erase(j);
         else
-            m_to_refine.insert(j);
+            m_to_refine.insert(j);        
-        
     }
 }
 
 
-bool core::try_to_patch(lpvar k, const rational& v) {
+bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
     return m_lar_solver.try_to_patch(k, v,
-                                     [this](lpvar u) { return var_is_used_in_a_correct_monic(u);},
+                                     [this, m](lpvar u) { return
+                                             u == m.var()
+                                             ||
+                                             var_is_used_in_a_correct_monic(u)
+                                             ||
+                                             m.contains_var(u);
+                                     },
                                      [this](lpvar u) { update_to_refine_of_var(u); });
 }
 
+bool in_power(const svector<lpvar>& vs, unsigned l) {
+    unsigned k = vs[l];
+    return (l != 0 && vs[l - 1] == k) || (l + 1 < vs.size() && k == vs[l + 1]);
+}
 
 // looking for any real var to patch
 void core::patch_monomial_with_real_var(lpvar j) {    
     const monic& m = emons()[j];
+    TRACE("nla_solver", tout << "m = "; print_monic(m, tout) << "\n";);
     rational v = mul_val(m);
-    if (val(j) == v || val(j).is_zero() || v.is_zero()) // correct or a lemma will catch it
+    SASSERT(j == var(m));
-        return;
+    if (var_val(m) == v) {
-    if (!var_is_int(j)  &&
-        !var_is_used_in_a_correct_monic(j)
-        &&  try_to_patch(j, v)) {
-        SASSERT(v == val(j));
         m_to_refine.erase(j);
-    } else {
+        return;
-        rational r = val(j) / v;
+    }
-        for (lpvar k: m.vars()) {
+    if (val(j).is_zero() || v.is_zero()) // a lemma will catch it
-            if (var_is_int(k)) continue;            
+        return;
-            if (var_is_used_in_a_correct_monic(k))
+
-                continue;
+    if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) {
-            if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
+        // SASSERT(mul_val(m) == var_val(m));        
-                m_to_refine.erase(j);
+        m_to_refine.erase(j);
-                SASSERT(mul_val(m) == val(j));
+        return;
-                break;
+    } 
-            }
+
+    // We have v != abc. Let us suppose we patch b. Then b should
+    // be equal to v/ac = v/(abc/b) = b(v/abc)
+    rational r = val(j) / v;
+    SASSERT(m.is_sorted());
+    for (unsigned l = 0; l < m.size(); l++) {
+        lpvar k = m.vars()[l];
+        if (!in_power(m.vars(), l) &&
+            var_is_int(k) && 
+            !var_is_used_in_a_correct_monic(k) &&
+            try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
+            SASSERT(mul_val(m) == var_val(m));
+            m_to_refine.erase(j);
+            break;
         }
     }
-    
                               
 }
 
-
 void core::patch_monomials_with_real_vars() {
     auto to_refine = m_to_refine.index();
-    // the rest of the function might change m_to_refine, so have to copy
+    // the rest of the function might change m_to_refine, so have to copy    
     for (lpvar j : to_refine) {
         patch_monomial_with_real_var(j);
     }

src/math/lp/nla_core.h

@@ -419,7 +419,7 @@ public:
     void patch_monomial_with_real_var(lpvar);
     bool var_is_used_in_a_correct_monic(lpvar) const;
     void update_to_refine_of_var(lpvar j);
-    bool try_to_patch(lpvar, const rational&);
+    bool try_to_patch(lpvar, const rational&, const monic&);
 };  // end of core
 
 struct pp_mon {

src/math/lp/u_set.h

@@ -94,7 +94,7 @@ public:
         m_index.resize(0);
     }
 
-    std::ostream& operator<<(std::ostream& out) const {
+    std::ostream& display(std::ostream& out) const {
         for (unsigned j : m_index) {
             out << j << " ";
         }
@@ -105,4 +105,10 @@ public:
     const unsigned * end() const { return m_index.end(); }
     const unsigned_vector& index() { return m_index; }
 };
+
+
+}
+
+inline std::ostream& operator<<(std::ostream& out, lp::u_set const& s) {
+    return s.display(out);
 }

src/model/model_evaluator.cpp

@@ -160,7 +160,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         family_id fid = f->get_family_id();
         bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
-        if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
+        if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)) {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;
@@ -168,7 +168,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 TRACE("model_evaluator", tout << result << "\n";);
                 return st;
             }
-            else if (m_model_completion) {
+            else if (m_model_completion && !m_ar.is_as_array(f)) {
                 sort * s   = f->get_range();
                 expr * val = m_model.get_some_value(s);
                 m_model.register_decl(f, val);

src/sat/ba_solver.cpp

@@ -2048,40 +2048,38 @@ namespace sat {
         return lit;
     }
 
+
     ba_solver::constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) {
-        struct parity { 
-            bool sign; bool lit; 
-            parity(): sign(false), lit(false) {}
-            // {false, false},  p => {false, true}
-            // {false, false}, !p => {true, true}
-            // {false, true},   p => {true, false}
-            // {false, true},  !p => {true, false}            
-            void add(literal l) {
-                lit = !lit;
-                sign = sign != l.sign();
-            }                
-        };
         literal_vector lits;
-        u_map<parity> var2parity;
+        u_map<bool> var2sign;
+        bool sign = false, odd = false;
         for (literal lit : _lits) {
-            var2parity.insert_if_not_there2(lit.var(), parity())->get_data().m_value.add(lit);
+            if (var2sign.find(lit.var(), sign)) {
+                var2sign.erase(lit.var());
+                odd ^= (sign ^ lit.sign());
+            }
+            else {
+                var2sign.insert(lit.var(), lit.sign());
+            }
         }       
         
-        bool polarity = false;
+        for (auto const& kv : var2sign) {
-        for (auto const& kv : var2parity) {
+            lits.push_back(literal(kv.m_key, kv.m_value));
-            bool lit = kv.m_value.lit;
-            bool sign = kv.m_value.sign;
-            if (lit)
-                lits.push_back(literal(kv.m_key, sign));
-            else 
-                polarity = polarity ^ sign;
         }
-        if (lits.empty()) {
+        if (odd && !lits.empty()) {
-            throw default_exception("empty xor is TBD");
-        }
-        if (polarity) {
             lits[0].neg();
         }
+        switch (lits.size()) {
+        case 0:
+            if (!odd)
+                s().set_conflict(justification(0));
+            return nullptr;
+        case 1:            
+            s().assign_scoped(lits[0]);
+            return nullptr;
+        default:
+            break;
+        }
         void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
         xr* x = new (mem) xr(next_id(), lits);
         x->set_learned(learned);
@@ -3238,7 +3236,8 @@ namespace sat {
             recompile(c.to_pb());
             break;
         case xr_t:
-            //NOT_IMPLEMENTED_YET();
+            add_xr(c.to_xr().literals(), c.learned());
+            remove_constraint(c, "recompile xor");
             break;
         default:
             UNREACHABLE();

src/sat/sat_local_search.cpp

@@ -31,7 +31,9 @@ namespace sat {
         for (unsigned i = 0; i < m_assumptions.size(); ++i) {
             add_clause(1, m_assumptions.c_ptr() + i);
         }
-
+        if (m_is_unsat)
+            return;
+        
         // add sentinel variable.
         m_vars.push_back(var_info());
 
@@ -334,7 +336,12 @@ namespace sat {
 
     void local_search::add_unit(literal lit, literal exp) {
         bool_var v = lit.var();
-        if (is_unit(lit)) return;
+        if (is_unit(lit)) {
+            if (m_vars[v].m_value == lit.sign()) {
+                m_is_unsat = true;                
+            }
+            return;
+        }
         SASSERT(!m_units.contains(v));
         if (m_vars[v].m_value == lit.sign() && !m_initializing) {
             flip_walksat(v);
@@ -575,8 +582,11 @@ namespace sat {
         m_assumptions.append(sz, assumptions);
         unsigned num_units = m_units.size();
         init();
+        if (m_is_unsat)
+            return l_false;
         walksat();
-        
+
+        TRACE("sat", tout << m_units << "\n";);
         // remove unit clauses
         for (unsigned i = m_units.size(); i-- > num_units; ) {
             m_vars[m_units[i]].m_unit = false;

src/sat/sat_solver.cpp

@@ -1154,6 +1154,7 @@ namespace sat {
                 if (mdl[v] != l_true) l.neg();
                 push();
                 assign_core(l, justification(scope_lvl()));
+                propagate(false);
             }
             mk_model();
             break;
@@ -1281,7 +1282,10 @@ namespace sat {
         struct scoped_ls {
             solver& s;
             scoped_ls(solver& s): s(s) {}
-            ~scoped_ls() { dealloc(s.m_local_search); s.m_local_search = nullptr; }
+            ~scoped_ls() { 
+                dealloc(s.m_local_search); 
+                s.m_local_search = nullptr; 
+            }
         };
         scoped_ls _ls(*this);
         if (inconsistent()) return l_false;
@@ -1313,6 +1317,7 @@ namespace sat {
 
     lbool solver::do_prob_search(unsigned num_lits, literal const* lits) {
         if (m_ext) return l_undef;
+        if (num_lits > 0 || !m_user_scope_literals.empty()) return l_undef;
         SASSERT(!m_local_search);
         m_local_search = alloc(prob);
         return invoke_local_search(num_lits, lits);

src/smt/asserted_formulas.cpp

@@ -421,7 +421,7 @@ void asserted_formulas::nnf_cnf() {
     for (; i < sz; i++) {
         expr * n    = m_formulas[i].get_fml();
         TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
-        proof * pr  = m_formulas[i].get_proof();
+        proof_ref pr(m_formulas[i].get_proof(), m);
         expr_ref   r1(m);
         proof_ref  pr1(m);
         push_todo.reset();

src/smt/smt_context.cpp

@@ -2950,7 +2950,7 @@ namespace smt {
     void context::assert_expr_core(expr * e, proof * pr) {
         if (get_cancel_flag()) return;
         SASSERT(is_well_sorted(m, e));
-        TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m) << "\n";);
+        TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
         TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
         pop_to_base_lvl();
         if (pr == nullptr)
@@ -3141,20 +3141,24 @@ namespace smt {
             m_asserted_formulas.commit();
         }
         if (m_asserted_formulas.inconsistent() && !inconsistent()) {
-            proof * pr = m_asserted_formulas.get_inconsistency_proof();
+            asserted_inconsistent();
-            if (pr == nullptr) {
-                set_conflict(b_justification::mk_axiom());
-            }
-            else {
-                set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
-                m_unsat_proof = pr;
-            }
         }
         TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
               tout << "inconsistent: " << inconsistent() << "\n";);
         TRACE("after_internalize_assertions", display(tout););
     }
 
+    void context::asserted_inconsistent() {
+        proof * pr = m_asserted_formulas.get_inconsistency_proof();
+        m_unsat_proof = pr;
+        if (!pr) {
+            set_conflict(b_justification::mk_axiom());
+        }
+        else {
+            set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
+        }
+    }
+
     /**
        \brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
     */
@@ -3626,8 +3630,10 @@ namespace smt {
 
 
     lbool context::search() {
-        if (m_asserted_formulas.inconsistent()) 
+        if (m_asserted_formulas.inconsistent()) {
+            asserted_inconsistent();
             return l_false;
+        }
         if (inconsistent()) {
             VERIFY(!resolve_conflict());
             return l_false;

src/smt/smt_context.h

@@ -1138,6 +1138,8 @@ namespace smt {
 
         void internalize_assertions();
 
+        void asserted_inconsistent();
+
         bool validate_assumptions(expr_ref_vector const& asms);
 
         void init_assumptions(expr_ref_vector const& asms);

src/smt/tactic/smt_tactic.cpp

@@ -249,6 +249,7 @@ public:
                         lcore = m.mk_join(lcore, m.mk_leaf(d));
                     }
                 }
+                if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
                 in->assert_expr(m.mk_false(), pr, lcore);
                 result.push_back(in.get());
                 return;
@@ -268,6 +269,7 @@ public:
                 if (pr) {
                     in->reset();
                     in->assert_expr(m.get_fact(pr), pr, nullptr);
+                    in->updt_prec(goal::UNDER_OVER);
                 }
                 if (m_candidate_models) {
                     switch (m_ctx->last_failure()) {

src/smt/theory_lra.cpp

@@ -1038,12 +1038,12 @@ public:
 
     bool internalize_atom(app * atom, bool gate_ctx) {
         SASSERT(!ctx().b_internalized(atom));
-        bool_var bv = ctx().mk_bool_var(atom);
-        ctx().set_var_theory(bv, get_id());
         expr* n1, *n2;
         rational r;
         lp_api::bound_kind k;
         theory_var v = null_theory_var;
+        bool_var bv = ctx().mk_bool_var(atom);
+        ctx().set_var_theory(bv, get_id());
         if (a.is_le(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
             v = internalize_def(to_app(n1));
             k = lp_api::upper_t;
@@ -1061,6 +1061,7 @@ public:
             found_unsupported(atom);
             return true;
         }
+
         if (is_int(v) && !r.is_int()) {
             r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
         }
@@ -1069,7 +1070,7 @@ public:
         updt_unassigned_bounds(v, +1);
         m_bounds_trail.push_back(v);
         m_bool_var2bound.insert(bv, b);
-        TRACE("arith_verbose", tout << "Internalized " << mk_pp(atom, m) << "\n";);
+        TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
         mk_bound_axioms(*b);
         //add_use_lists(b);
         return true;
@@ -1560,8 +1561,8 @@ public:
 
     void init_variable_values() {
         reset_variable_values();
-        if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
+        if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {            
-            TRACE("arith", tout << "update variable values\n";);
+            TRACE("arith", display(tout << "update variable values\n"););
             lp().get_model(m_variable_values);
         }
     }
@@ -2241,12 +2242,14 @@ public:
             return;
         }
         while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) {
-            bool_var bv  = m_asserted_atoms[m_asserted_qhead].m_bv;
+            bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
-            bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;                
+            bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
             m_to_check.push_back(bv);
-            lp_api::bound& b = *m_bool_var2bound.find(bv);
+            lp_api::bound* b = nullptr;
-            assert_bound(bv, is_true, b);                
+            if (m_bool_var2bound.find(bv, b)) {
-            ++m_asserted_qhead;
+                assert_bound(bv, is_true, *b);
+                ++m_asserted_qhead;
+            }
         }
         if (ctx().inconsistent()) {
             m_to_check.reset();
@@ -2691,11 +2694,12 @@ public:
     }
 
     void propagate_basic_bounds() {
-        for (auto const& bv : m_to_check) {                
+        for (auto const& bv : m_to_check) {
-            lp_api::bound& b = *m_bool_var2bound.find(bv);
+            lp_api::bound* b = nullptr;
-            propagate_bound(bv, ctx().get_assignment(bv) == l_true, b);
+            if (m_bool_var2bound.find(bv, b)) {
-            if (ctx().inconsistent()) break;
+                propagate_bound(bv, ctx().get_assignment(bv) == l_true, *b);
-
+                if (ctx().inconsistent()) break;
+            }
         }
         m_to_check.reset();
     }