#5336

Z3Prover · Jul 11, 2021 · cab1076 · cab1076
1 parent 18a76ab
commit cab1076
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 16 deletions.
diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
@@ -134,20 +134,29 @@ namespace opt {
     }
 
     void model_based_opt::def::normalize() {
-        if (m_div.is_one()) return;
+        SASSERT(m_div.is_int());
+        if (m_div.is_neg()) {
+            for (var& v : m_vars)
+                v.m_coeff.neg();
+            m_coeff.neg();
+            m_div.neg();
+        }
+        if (m_div.is_one())
+            return;
         rational g(m_div);
+        if (!m_coeff.is_int())
+            return;
         g = gcd(g, m_coeff);
         for (var const& v : m_vars) {
+            if (!v.m_coeff.is_int())
+                return;
             g = gcd(g, abs(v.m_coeff));
-            if (g.is_one()) break;
-        }
-        if (m_div.is_neg()) {
-            g.neg();
+            if (g.is_one()) 
+                break;
         }
         if (!g.is_one()) {
-            for (var& v : m_vars) {
-                v.m_coeff /= g;
-            }
+            for (var& v : m_vars) 
+                v.m_coeff /= g;            
             m_coeff /= g;
             m_div /= g;
         }
@@ -1130,9 +1139,12 @@ namespace opt {
         }
         TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
         def result = project(y, compute_def);
-        if (compute_def) 
-            result = (result * D) + u;     
-        SASSERT(!compute_def || eval(result) == eval(x));
+        if (compute_def) {
+            result = (result * D) + u;
+            m_var2value[x] = eval(result);
+        }
+        TRACE("opt1", display(tout << "tableau after project y" << y << "\n"););
+
         return result;
     }
 
@@ -1181,7 +1193,7 @@ namespace opt {
     // 3 | -t  & 21 | (-ct + 3s) & a-t <= 3u
 
     model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) {
-        TRACE("opt", tout << "v" << x << "\n" << m_rows[row_id1] << "\n";);
+        TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";);
         rational a = get_coefficient(row_id1, x), b;
         ineq_type ty = m_rows[row_id1].m_type;
         SASSERT(!a.is_zero());
@@ -1231,6 +1243,7 @@ namespace opt {
         if (compute_def) {
             result = def(m_rows[row_id1], x);
             m_var2value[x] = eval(result);
+            TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
         }
         retire_row(row_id1);
         return result;

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
@@ -294,7 +294,9 @@ namespace mbp {
                 }
             }
             fmls.shrink(j);
-            TRACE("qe", tout << "formulas\n" << fmls << "\n";);
+            TRACE("qe", tout << "formulas\n" << fmls << "\n";
+		                for (auto [e, id] : tids)
+		                    tout << mk_pp(e, m) << " -> " << id << "\n";);
 
             // fmls holds residue,
             // mbo holds linear inequalities that are in scope

diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp
@@ -102,7 +102,7 @@ namespace mbp {
         model_evaluator eval(model);
         eval.set_expand_array_equalities(true);
         TRACE("qe", tout << fmls << "\n";);
-        DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); });
+        DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
 
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -302,13 +302,17 @@ namespace euf {
         size_t* c = to_ptr(l);
         SASSERT(is_literal(c));
         SASSERT(l == get_literal(c));
-        if (!sign && n->is_equality()) {
+	    if (n->value_conflict()) {
+            euf::enode* nb = sign ? mk_false() : mk_true();
+            m_egraph.merge(n, nb, c);
+	    }
+        else if (!sign && n->is_equality()) {
             SASSERT(!m.is_iff(e));
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_tf() || n->value_conflict()) {
+        else if (n->merge_tf()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }