added div/mod handling

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

src/math/lp/int_solver.cpp

@@ -49,8 +49,13 @@ namespace lp {
                 continue;
             patch_nbasic_column(v);
         }
+        unsigned num_fixed = 0;
+        for (unsigned v = 0; v < num; v++) 
+            if (lia.is_fixed(v))
+                ++num_fixed;
+            
         lp_assert(lia.is_feasible());
-        verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << "\n";
+        verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n";
         //lra.display(verbose_stream());
         //exit(0);
         if (!lia.has_inf_int()) {
@@ -72,16 +77,6 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
     bool val_is_int = lia.value_is_int(j);
 
 
-    const auto & A = lra.A_r();
-    if (!m_is_one) {
-        verbose_stream() << "divisor: " << m << "\n";
-        lia.display_column(verbose_stream(), j);
-        for (auto c : A.column(j)) {
-            unsigned row_index = c.var();
-            lia.display_row(verbose_stream(), A.m_rows[row_index]);
-            verbose_stream() << "\n";
-        }
-    }
 
     // check whether value of j is already a multiple of m.
     if (val_is_int && (m_is_one || (val.x / m).is_int())) {
@@ -92,6 +87,19 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
         return;
     }
 
+#if 0
+    const auto & A = lra.A_r();
+    if (!m_is_one) {
+        // lia.display_column(verbose_stream(), j);
+        for (auto c : A.column(j)) {
+            continue;
+            unsigned row_index = c.var();
+            lia.display_row(verbose_stream(), A.m_rows[row_index]);
+            verbose_stream() << "\n";
+        }
+    }
+#endif
+
     TRACE("patch_int",
           tout << "TARGET j" << j << " -> [";
           if (inf_l) tout << "-oo"; else tout << l;
@@ -126,6 +134,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
             lra.set_value_for_nbasic_column(j, l);
         }
         else {
+            verbose_stream() << "fail: " << j << " " << m << "\n";
             --m_patch_success;
             ++m_patch_fail;
             TRACE("patch_int", tout << "not patching " << l << "\n";);
@@ -354,7 +363,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
 
 // this function assumes that all basic columns dependend on j are feasible
 bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
-    if (lrac.m_r_heading[j] >= 0) // the basic var
+    if (lrac.m_r_heading[j] >= 0 || is_fixed(j)) // basic or fixed var
         return false;
 
     TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);

src/smt/theory_arith_aux.h

@@ -2059,7 +2059,9 @@ namespace smt {
         bool inf_l, inf_u;
         inf_numeral l, u;
         numeral m;
-        get_freedom_interval(v, inf_l, l, inf_u, u, m);
+        if (!get_freedom_interval(v, inf_l, l, inf_u, u, m))
+            return false;
+        
         if (inf_l && inf_u) {
             inf_numeral new_val = inf_numeral(m_random() % (RANGE + 1));
             set_value(v, new_val);

src/smt/theory_arith_core.h

@@ -1567,6 +1567,8 @@ namespace smt {
         m_liberal_final_check = true;
         m_changed_assignment  = false;
         final_check_status result = final_check_core();
+        //display(verbose_stream());
+        //exit(0);
         if (result != FC_DONE)
             return result;
         if (!m_changed_assignment)

src/smt/theory_arith_int.h

@@ -908,15 +908,21 @@ namespace smt {
         inf_numeral l, u;
         numeral m;
         unsigned num_patched = 0, num_not_patched = 0;
-        unsigned num_one = 0, num_divides = 0;
+        unsigned num_one = 0, num_divides = 0, num_fixed = 0;
+
+        for (theory_var v = 0; v < num; v++) 
+            if (is_fixed(v))
+                ++num_fixed;
+            
         for (theory_var v = 0; v < num; v++) {
-            if (!is_non_base(v)) 
+            if (!is_non_base(v) || is_fixed(v)) 
                 continue;
             get_freedom_interval(v, inf_l, l, inf_u, u, m);
             if (m.is_one() && get_value(v).is_int()) {
                 num_one++;
                 continue;
             }
+            
             // check whether value of v is already a multiple of m.
             if ((get_value(v).get_rational() / m).is_int()) {
                 num_divides++;
@@ -952,6 +958,7 @@ namespace smt {
             }
             if (!inf_l && !inf_u && l > u) {
                 ++num_not_patched;
+                verbose_stream() << "fail: " << v << " " << m << "\n";
                 continue; // cannot patch
             }
             ++num_patched;
@@ -963,7 +970,7 @@ namespace smt {
                 set_value(v, inf_numeral(0));
         }
         SASSERT(m_to_patch.empty());
-        verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << "\n";
+        verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n";
         //display(verbose_stream());
         //exit(0);
     }

src/smt/theory_lra.cpp

@@ -449,6 +449,29 @@ class theory_lra::imp {
         return v;
     }
 
+    theory_var internalize_mod(app* n) {
+        TRACE("arith", tout << "internalizing...\n" << mk_pp(n, m) << "\n";);
+        rational r(1);
+        theory_var s = mk_binary_op(n);
+        if (!a.is_numeral(n->get_arg(1), r) || r.is_zero())
+            found_underspecified(n);
+        if (!ctx().relevancy())
+            mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1));
+        return s;
+
+    }
+
+    theory_var mk_binary_op(app * n) {
+        SASSERT(n->get_num_args() == 2);
+        if (ctx().e_internalized(n))
+            return mk_var(n);
+        ctx().internalize(n->get_arg(0), false);
+        ctx().internalize(n->get_arg(1), false);
+        enode* e = mk_enode(n);
+        return mk_var(n);
+    }
+
+
     /**
      * \brief Internalize the given term and return an alias for it.
      *  Return null_theory_var if the term was not implemented by the theory yet.
@@ -472,16 +495,18 @@ class theory_lra::imp {
             return internalize_numeral(n, val);
         else if (a.is_mul(n))
             return internalize_mul1(n);
-        else if (a.is_arith_expr(n))
+        else if (a.is_mod(n))
+            return internalize_mod(n);
+        else if (a.is_idiv(n))
+            return internalize_mod(n);
+        else if (a.is_arith_expr(n)) {
+            verbose_stream() << "nyi " << mk_pp(n, m) << "\n";
             NOT_IMPLEMENTED_YET();
+        }
 #if 0
 
         else if (a.is_div(n))
             return internalize_div(n);
-        else if (a.is_idiv(n))
-            return internalize_idiv(n);
-        else if (a.is_mod(n))
-            return internalize_mod(n);
         else if (a.is_rem(n))
             return internalize_rem(n);
         else if (a.is_to_real(n))
@@ -1919,6 +1944,8 @@ public:
         m_changed_assignment = false;
         ctx().push_trail(value_trail<unsigned>(m_final_check_idx));
         final_check_status result = final_check_core();
+        //display(verbose_stream());
+        //exit(0);
         if (result != FC_DONE)
             return result;
         if (!m_changed_assignment)