move m_fixed_var_table to lar_solver

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

src/math/lp/lar_constraints.h

@@ -95,7 +95,6 @@ public:
     unsigned size() const override { return m_term->size();}
 };
 
-
 class constraint_set {
     region                         m_region;
     column_namer&                  m_namer;
@@ -151,20 +150,16 @@ public:
         m_constraint_count = m_constraints.size();
         m_constraint_count.push();
         m_region.push_scope();
-#if 1
         m_active_lim = m_active.size();
         m_active_lim.push();
-#endif
     }
 
     void pop(unsigned k) {
-#if 1
         m_active_lim.pop(k);
         for (unsigned i = m_active.size(); i-- > m_active_lim; ) {
             m_constraints[m_active[i]]->deactivate();
         }
         m_active.shrink(m_active_lim);
-#endif
         m_constraint_count.pop(k);        
         for (unsigned i = m_constraints.size(); i-- > m_constraint_count; )
             m_constraints[i]->~lar_base_constraint();        
@@ -181,17 +176,10 @@ public:
         return add(new (m_region) lar_term_constraint(j, t, k, rhs));
     }
 
-#if 0
-    bool is_active(constraint_index ci) const { return true; }
-
-    void activate(constraint_index ci) {}
-
-#else
     // future behavior uses activation bit.
     bool is_active(constraint_index ci) const { return m_constraints[ci]->is_active(); }
 
     void activate(constraint_index ci) { auto& c = *m_constraints[ci]; if (!c.is_active()) { c.activate(); m_active.push_back(ci); } }
-#endif
 
     lar_base_constraint const& operator[](constraint_index ci) const { return *m_constraints[ci]; }    
 
@@ -283,9 +271,6 @@ public:
         print_left_side_of_constraint(c, var_str, out); 
         return out << " " << lconstraint_kind_string(c.kind()) << " " << c.rhs() << std::endl;
     }
-
-    
-    
 };
 
 inline std::ostream& operator<<(std::ostream& out, constraint_set const& cs) { 

src/math/lp/lar_solver.cpp

@@ -18,14 +18,16 @@ void clear() {lp_assert(false); // not implemented
 }
 
 
-lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
+lar_solver::lar_solver(const std::function<void(unsigned, unsigned)>& report_equality_of_fixed_vars) :
-                           m_crossed_bounds_column(-1),
+    m_status(lp_status::UNKNOWN),
-                           m_mpq_lar_core_solver(m_settings, *this),
+    m_crossed_bounds_column(-1),
-                           m_int_solver(nullptr),
+    m_mpq_lar_core_solver(m_settings, *this),
-                           m_need_register_terms(false),
+    m_int_solver(nullptr),
-                           m_var_register(false),
+    m_need_register_terms(false),
-                           m_term_register(true),
+    m_var_register(false),
-                           m_constraints(*this)
+    m_term_register(true),
+    m_constraints(*this),
+    m_report_equality_of_fixed_vars(report_equality_of_fixed_vars)
 {}
     
 void lar_solver::set_track_pivoted_rows(bool v) {
@@ -271,6 +273,7 @@ void lar_solver::pop(unsigned k) {
     m_columns_to_ul_pairs.pop(k);
 
     m_mpq_lar_core_solver.pop(k);
+    remove_non_fixed_from_fixed_var_table();
     clean_popped_elements(n, m_columns_with_changed_bound);
     clean_popped_elements(n, m_incorrect_columns);
     
@@ -1721,6 +1724,36 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c
     return ci;
 }
 
+void lar_solver::remove_non_fixed_from_fixed_var_table() {
+    vector<value_sort_pair> to_remove;
+    for (const auto& p : m_fixed_var_table) {
+        unsigned j = p.m_value;
+        if (j >= column_count() || column_is_fixed(j) == false)
+            to_remove.push_back(p.m_key);
+    }
+    for (const auto & p : to_remove)
+        m_fixed_var_table.erase(p);
+}
+
+void lar_solver::register_in_fixed_var_table(unsigned j) {
+    SASSERT(column_is_fixed(j));
+    const impq& bound = get_lower_bound(j);
+    if (bound.y.is_zero() == false)
+        return;
+
+    value_sort_pair key(bound.x, column_is_int(j));
+    unsigned k;
+    if (m_fixed_var_table.find(key, k) == false ) {
+        m_fixed_var_table.insert(key, j);
+        return;
+    }
+    SASSERT(column_is_fixed(k));
+    if (j != k && column_is_int(j) == column_is_int(k))
+        m_report_equality_of_fixed_vars(
+            column_to_reported_index(j),
+            column_to_reported_index(k));
+}
+
 void lar_solver::activate(constraint_index ci) {
     auto const& c = m_constraints[ci];
     update_column_type_and_bound(c.column(), c.kind(), c.rhs(), ci);
@@ -1784,13 +1817,19 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq &
     }
 }
 
-void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side,
+void lar_solver::update_column_type_and_bound(var_index j,
+                                              lconstraint_kind kind,
+                                              const mpq & right_side,
                                               constraint_index constr_index) {
     m_constraints.activate(constr_index);
     if (column_has_upper_bound(j))
         update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
     else 
         update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
+    if (column_is_fixed(j)) {
+        register_in_fixed_var_table(j);
+    }
+
 }
 
 constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) {

src/math/lp/lar_solver.h

@@ -49,6 +49,8 @@ namespace lp {
 class int_branch;
 class int_solver;
 class lar_solver : public column_namer {
+    typedef std::pair<mpq, bool> value_sort_pair;
+    typedef pair_hash<obj_hash<mpq>, bool_hash> value_sort_pair_hash;
     struct term_hasher {
         std::size_t operator()(const lar_term &t) const
         {            
@@ -102,6 +104,12 @@ class lar_solver : public column_namer {
     m_normalized_terms_to_columns;
     vector<impq>                                        m_backup_x;
     stacked_vector<unsigned>                            m_usage_in_terms;
+    // ((x[j], is_int(j))->j)  for fixed j, used in equalities propagation
+    map<value_sort_pair,
+        unsigned,
+        value_sort_pair_hash,
+        default_eq<value_sort_pair>>                    m_fixed_var_table;
+    std::function <void(unsigned, unsigned)>            m_report_equality_of_fixed_vars;
     // end of fields
 
     ////////////////// methods ////////////////////////////////
@@ -142,7 +150,8 @@ class lar_solver : public column_namer {
     void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
     void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
     void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
-    
+    void register_in_fixed_var_table(var_index);
+    void remove_non_fixed_from_fixed_var_table();
     constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side);
     inline void set_infeasible_column(unsigned j) {
         set_status(lp_status::INFEASIBLE);
@@ -281,6 +290,18 @@ class lar_solver : public column_namer {
     void register_normalized_term(const lar_term&, lpvar);
     void deregister_normalized_term(const lar_term&);
 public:
+    const map<value_sort_pair,
+        unsigned,
+        value_sort_pair_hash,
+                  default_eq<value_sort_pair>>& fixed_var_table() const {
+        return m_fixed_var_table;
+    }
+    map<value_sort_pair,
+        unsigned,
+        value_sort_pair_hash,
+                  default_eq<value_sort_pair>>& fixed_var_table() {
+        return m_fixed_var_table;
+    }
     unsigned external_to_column_index(unsigned) const;
     bool inside_bounds(lpvar, const impq&) const;
     inline void set_column_value(unsigned j, const impq& v) {
@@ -572,7 +593,7 @@ public:
     void fill_explanation_from_crossed_bounds_column(explanation & evidence) const;
     bool term_is_used_as_row(unsigned term) const;
     bool tighten_term_bounds_by_delta(tv const& t, const impq&);
-    lar_solver();
+    lar_solver(const std::function <void(unsigned, unsigned)>& report_equality_of_fixed_vars);
     void set_track_pivoted_rows(bool v);
     bool get_track_pivoted_rows() const;    
     virtual ~lar_solver();

src/math/lp/lp_bound_propagator.h

@@ -325,19 +325,9 @@ public:
             if (y == null_lpvar) {
                 // x is an implied fixed var at k.
                 value_sort_pair key(k, is_int(x));
-                int x2;
+                unsigned x2;
-                if (m_imp.m_fixed_var_table.find(key, x2) && 
+                if (lp().fixed_var_table().find(key, x2) && !is_equal(x, x2)) {
-                    x2 < static_cast<int>(m_imp.get_num_vars())                    
+                    SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k && is_int(x) == is_int(x2)); 
-                    && 
-                    lp().column_is_fixed(x2 = imp_to_col(x2)) && // change x2
-                        get_lower_bound_rational(x2) == k &&
-                    // We must check whether x2 is an integer. 
-                    // The table m_fixed_var_table is not restored during backtrack. So, it may
-                    // contain invalid (key -> value) pairs. 
-                    // So, we must check whether x2 is really equal to k (previous test) 
-                    // AND has the same sort of x.
-                        is_int(x) == is_int(x2) &&
-                    !is_equal(x, x2)) {
                     explanation ex;
                     constraint_index lc, uc;
                     lp().get_bound_constraint_witnesses_for_column(x2, lc, uc);

src/math/lp/mps_reader.h

@@ -883,7 +883,7 @@ public:
     }
 
     lar_solver * create_lar_solver() {
-        lar_solver * solver =  new lar_solver();
+        lar_solver * solver =  new lar_solver([](unsigned, unsigned) { });
         fill_lar_solver(solver);
         return solver;
     }

src/smt/theory_lra.cpp

@@ -327,42 +327,7 @@ class theory_lra::imp {
     bool is_real(enode* n) const { return a.is_real(n->get_owner()); }
     enode* get_enode(theory_var v) const { return th.get_enode(v); }
     enode* get_enode(expr* e) const { return ctx().get_enode(e); }
-    expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }        
+    expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }    
-
-    void init_solver() {
-        if (m_solver) return;
-
-        reset_variable_values();
-        m_solver = alloc(lp::lar_solver); 
-
-        // initialize 0, 1 variables:
-        get_one(true);
-        get_one(false);
-        get_zero(true);
-        get_zero(false);
-
-        smt_params_helper lpar(ctx().get_params());
-        lp().settings().set_resource_limit(m_resource_limit);
-        lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.arith_simplex_strategy());
-        lp().settings().bound_propagation() = BP_NONE != propagation_mode();
-        lp().settings().enable_hnf() = lpar.arith_enable_hnf();
-        lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names();
-        lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows());
-        lp().settings().report_frequency = lpar.arith_rep_freq();
-        lp().settings().print_statistics = lpar.arith_print_stats();
-
-        // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
-        unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
-        lp().set_cut_strategy(branch_cut_ratio);
-        
-        lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
-        lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
-        m_lia = alloc(lp::int_solver, *m_solver.get());
-        get_one(true);
-        get_zero(true);
-        get_one(false);
-        get_zero(false);
-    }
 
     lpvar add_const(int c, lpvar& var, bool is_int) {
         if (var != UINT_MAX) {
@@ -371,7 +336,7 @@ class theory_lra::imp {
         app_ref cnst(a.mk_numeral(rational(c), is_int), m);
         mk_enode(cnst);
         theory_var v = mk_var(cnst);
-        var = lp().add_var(v, true);
+        var = lp().add_var(v, is_int);
         lp().push();
         add_def_constraint(lp().add_var_bound(var, lp::GE, rational(c)));
         add_def_constraint(lp().add_var_bound(var, lp::LE, rational(c)));
@@ -933,10 +898,6 @@ class theory_lra::imp {
                 }
             }
 
-            rational val;
-            if (a.is_numeral(term, val)) {
-                m_fixed_var_table.insert(value_sort_pair(val, is_int(v)), v);
-            }
             return v;
         }
     }
@@ -976,8 +937,7 @@ public:
         if (m_solver) return;
 
         reset_variable_values();
-        m_solver = alloc(lp::lar_solver); 
+        m_solver = alloc(lp::lar_solver, [&](unsigned j, unsigned k) { report_equality_of_fixed_vars(j, k); }); 
-
         // initialize 0, 1 variables:
         get_one(true);
         get_one(false);
@@ -3055,10 +3015,6 @@ public:
     typedef std::pair<lp::constraint_index, rational> constraint_bound;
     vector<constraint_bound>        m_lower_terms;
     vector<constraint_bound>        m_upper_terms;
-    typedef std::pair<rational, bool> value_sort_pair;
-    typedef pair_hash<obj_hash<rational>, bool_hash> value_sort_pair_hash;
-    typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-    value2var                       m_fixed_var_table;
 
     void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) {
         if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) {
@@ -3191,62 +3147,61 @@ public:
     }
 
     unsigned get_num_vars() const { return th.get_num_vars(); }
+
+    void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) {
+        lp::constraint_index ci1, ci2, ci3, ci4;
+        theory_var v1 = lp().local_to_external(vi1);
+        theory_var v2 = lp().local_to_external(vi2);
+        if (is_equal(v1, v2))
+            return;
+        SASSERT(is_int(v1) == is_int(v2));
+
+        lp::mpq bound;
+        TRACE("arith",
+              bool hlb = has_lower_bound(vi2, ci3, bound); // has_lower_bound in turn trace "arith"
+              tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;);
+        if (!(has_lower_bound(vi2, ci3, bound)
+              &&
+              has_upper_bound(vi2, ci4, bound)
+              &&
+              has_lower_bound(vi1, ci1, bound)
+              &&
+              has_upper_bound(vi1, ci2, bound))) {
+            TRACE("arith", tout << "strange\n";);
+            return;
+        }
+        ++m_stats.m_fixed_eqs;
+        reset_evidence();
+        set_evidence(ci1, m_core, m_eqs);
+        set_evidence(ci2, m_core, m_eqs);
+        set_evidence(ci3, m_core, m_eqs);
+        set_evidence(ci4, m_core, m_eqs);
+        enode* x = get_enode(v1);
+        enode* y = get_enode(v2);
+        justification* js = 
+            ctx().mk_justification(
+                ext_theory_eq_propagation_justification(
+                    get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
+        
+        TRACE("arith",
+              for (unsigned i = 0; i < m_core.size(); ++i) {
+                  ctx().display_detailed_literal(tout, m_core[i]);
+                  tout << "\n";
+              } 
+              for (unsigned i = 0; i < m_eqs.size(); ++i) {
+                  tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
+              } 
+              tout << " ==> ";
+              tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
+              );
+        
+        // parameters are TBD.
+        //                    SASSERT(validate_eq(x, y));
+        ctx().assign_eq(x, y, eq_justification(js));
+    }
     
     void fixed_var_eh(theory_var v1, rational const& bound) {
-        // IF_VERBOSE(0, verbose_stream() << "fix " << mk_bounded_pp(get_owner(v1), m) << " " << bound << "\n");
+        // no op
-
-        theory_var v2;
-        value_sort_pair key(bound, is_int(v1));
-        if (m_fixed_var_table.find(key, v2)) {
-            if (static_cast<unsigned>(v2) < th.get_num_vars() && !is_equal(v1, v2) && is_int(v1) == is_int(v2)) {
-                auto vi1 = register_theory_var_in_lar_solver(v1);
-                auto vi2 = register_theory_var_in_lar_solver(v2);
-                lp::constraint_index ci1, ci2, ci3, ci4;
-                
-                TRACE("arith",
-                      bool hlb = has_lower_bound(vi2, ci3, bound); // has_lower_bound in turn trace "arith"
-                      tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;);
-                if (has_lower_bound(vi2, ci3, bound) && has_upper_bound(vi2, ci4, bound)) {
-                    VERIFY (has_lower_bound(vi1, ci1, bound));
-                    VERIFY (has_upper_bound(vi1, ci2, bound));
-                    ++m_stats.m_fixed_eqs;
-                    reset_evidence();
-                    set_evidence(ci1, m_core, m_eqs);
-                    set_evidence(ci2, m_core, m_eqs);
-                    set_evidence(ci3, m_core, m_eqs);
-                    set_evidence(ci4, m_core, m_eqs);
-                    enode* x = get_enode(v1);
-                    enode* y = get_enode(v2);
-                    justification* js = 
-                        ctx().mk_justification(
-                            ext_theory_eq_propagation_justification(
-                                get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
-
-                    TRACE("arith",
-                          for (unsigned i = 0; i < m_core.size(); ++i) {
-                              ctx().display_detailed_literal(tout, m_core[i]);
-                              tout << "\n";
-                          } 
-                          for (unsigned i = 0; i < m_eqs.size(); ++i) {
-                              tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
-                          } 
-                          tout << " ==> ";
-                          tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
-                          );
-
-                    // parameters are TBD.
-                    //                    SASSERT(validate_eq(x, y));
-                    ctx().assign_eq(x, y, eq_justification(js));
-                }
-            }
-            else {
-                // bounds on v2 were changed.
-                m_fixed_var_table.insert(key, v1);
-            }
-        }
-        else {
-            m_fixed_var_table.insert(key, v1);
-        }
     }
 
     lbool make_feasible() {