merge with master

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

src/math/lp/lar_solver.cpp

@@ -172,7 +172,7 @@ void lar_solver::analyze_new_bounds_on_row_tableau(
         return;
     lp_assert(use_tableau());
     bound_analyzer_on_row<row_strip<mpq>>::analyze_row(A_r().m_rows[row_index],
-                                       static_cast<unsigned>(-1),
+                                       null_ci,
                                        zero_of_type<numeric_pair<mpq>>(),
                                        row_index,
                                        bp
@@ -246,7 +246,7 @@ bool lar_solver::term_is_used_as_row(unsigned term) const {
     
 void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) {
     for (unsigned i = 0; i < m_terms.size(); i++) {
-        if (term_is_used_as_row(i + m_terms_start_index))
+        if (term_is_used_as_row(i))
             continue; // this term is used a left side of a constraint,
         // it was processed as a touched row if needed
         propagate_bounds_on_a_term(*m_terms[i], bp, i);
@@ -1118,7 +1118,7 @@ bool lar_solver::has_lower_bound(var_index var, constraint_index& ci, mpq& value
     }
     const ul_pair & ul = m_columns_to_ul_pairs[var];
     ci = ul.lower_bound_witness();
-    if (ci != static_cast<constraint_index>(-1)) {
+    if (ci != null_ci) {
         auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var];
         value = p.x;
         is_strict = p.y.is_pos();
@@ -1137,7 +1137,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value
     }
     const ul_pair & ul = m_columns_to_ul_pairs[var];
     ci = ul.upper_bound_witness();
-    if (ci != static_cast<constraint_index>(-1)) {
+    if (ci != null_ci) {
         auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var];
         value = p.x;
         is_strict = p.y.is_neg();
@@ -1363,7 +1363,7 @@ void lar_solver::pop() {
 }
 
 bool lar_solver::column_represents_row_in_tableau(unsigned j) {
-    return m_columns_to_ul_pairs()[j].m_i != static_cast<row_index>(-1);
+    return m_columns_to_ul_pairs()[j].m_i != UINT_MAX;
 }
 
 void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) {
@@ -1580,7 +1580,7 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
         return local_j;
     lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
     local_j = A_r().column_count();
-    m_columns_to_ul_pairs.push_back(ul_pair(static_cast<unsigned>(-1)));
+    m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX));
     add_non_basic_var_to_core_fields(ext_j, is_int);
     lp_assert(sizes_are_correct());
     return local_j;
@@ -2330,6 +2330,18 @@ bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair<mpq,
     TRACE("lar_solver_terms", tout << "have not found\n";);
     return false;
 }
+
+std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j, lpvar k) {
+    vector<std::pair<mpq, var_index>> coeffs;
+    coeffs.push_back(std::make_pair(mpq(1),j));
+    coeffs.push_back(std::make_pair(mpq(-1),k));    
+    unsigned ext_term_index = m_terms.size();
+    unsigned term_index = add_term(coeffs, ext_term_index);
+    return std::pair<constraint_index, constraint_index>(
+        add_var_bound(term_index, lconstraint_kind::LE, mpq(0)),
+        add_var_bound(term_index, lconstraint_kind::GE, mpq(0)));
+}
+
 } // namespace lp
 
 

src/math/lp/lar_solver.h

@@ -47,6 +47,7 @@ namespace lp {
 
 typedef unsigned lpvar;
 const lpvar null_lpvar = UINT_MAX;
+const constraint_index null_ci = UINT_MAX;
 
 class lar_solver : public column_namer {
     struct term_hasher {
@@ -536,6 +537,8 @@ public:
         return m_mpq_lar_core_solver.column_is_bounded(j);
     }
 
+    std::pair<constraint_index, constraint_index> add_equality(lpvar j, lpvar k);
+    
     void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const {
         const ul_pair & ul = m_columns_to_ul_pairs[j];
         lc = ul.lower_bound_witness();

src/smt/params/smt_params_helper.pyg

@@ -40,7 +40,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
-                          ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
+                          ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),
@@ -75,7 +75,7 @@ def_module_params(module_name='smt',
                           ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
                           ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
                           ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
-                          ('arith.nla', BOOL, True, 'call nonlinear solver'),
+                          ('arith.nla', BOOL, True, 'call nonlinear integer solver with incremental linearization'),
                           ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
                           ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),