fixing parity bug in model generation for UTVPI

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

src/smt/diff_logic.h

@@ -306,14 +306,6 @@ private:
         return true;
     }
 
-    // Update the assignment of variable v, that is,
-    // m_assignment[v] += inc
-    // This method also stores the old value of v in the assignment stack.
-    void acc_assignment(dl_var v, const numeral & inc) {
-        TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
-        m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
-        m_assignment[v] += inc;
-    }
 
     // Restore the assignment using the information in m_assignment_stack.
     // This method is called when make_feasible fails.
@@ -827,6 +819,16 @@ public:
         }
     }
 
+    // Update the assignment of variable v, that is,
+    // m_assignment[v] += inc
+    // This method also stores the old value of v in the assignment stack.
+    void acc_assignment(dl_var v, const numeral & inc) {
+        TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
+        m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
+        m_assignment[v] += inc;
+    }
+
+
     struct every_var_proc {
         bool operator()(dl_var v) const {
             return true;
@@ -837,6 +839,36 @@ public:
         display_core(out, every_var_proc());
     }
 
+    void display_agl(std::ostream & out) const {
+        uint_set vars;
+        typename edges::const_iterator it  = m_edges.begin();
+        typename edges::const_iterator end = m_edges.end();
+        for (; it != end; ++it) {
+            edge const& e = *it;
+            if (e.is_enabled()) {
+                vars.insert(e.get_source());
+                vars.insert(e.get_target());
+            }
+        }
+        out << "digraph "" {\n";
+        
+        unsigned n = m_assignment.size();
+        for (unsigned v = 0; v < n; v++) {
+            if (vars.contains(v)) {
+                out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n";
+            }
+        }
+        it = m_edges.begin();
+        for (; it != end; ++it) {
+            edge const& e = *it;
+            if (e.is_enabled()) {
+                out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n";
+            }
+        }
+
+        out << "}\n";
+    }
+
     template<typename FilterAssignmentProc>
     void display_core(std::ostream & out, FilterAssignmentProc p) const {
         display_edges(out);
@@ -1000,6 +1032,38 @@ public:
         }
     }
 
+    void compute_zero_succ(dl_var v, int_vector& succ) {
+        unsigned n = m_assignment.size();
+        m_dfs_time.reset();
+        m_dfs_time.resize(n, -1);
+        m_dfs_time[v] = 0;
+        succ.push_back(v);
+        numeral gamma;
+        for (unsigned i = 0; i < succ.size(); ++i) {
+            v = succ[i];
+            edge_id_vector & edges = m_out_edges[v];
+            typename edge_id_vector::iterator it  = edges.begin();
+            typename edge_id_vector::iterator end = edges.end();
+            for (; it != end; ++it) {
+                edge_id e_id = *it;
+                edge & e     = m_edges[e_id];
+                if (!e.is_enabled()) {
+                    continue;
+                }
+                SASSERT(e.get_source() == v);
+                set_gamma(e, gamma);
+                if (gamma.is_zero()) {
+                    dl_var target = e.get_target();
+                    if (m_dfs_time[target] == -1) {
+                        succ.push_back(target);
+                        m_dfs_time[target] = 0;
+                    }
+                }
+            }
+
+        }
+    }
+
     numeral get_assignment(dl_var v) const {
         return m_assignment[v]; 
     }

src/smt/theory_utvpi.h

@@ -262,7 +262,11 @@ namespace smt {
 
     private:        
 
-        rational mk_value(theory_var v);
+        rational mk_value(theory_var v, bool is_int);
+
+        bool is_parity_ok(unsigned v) const;
+
+        void enforce_parity();
 
         void validate_model();
 

src/smt/theory_utvpi_def.h

@@ -397,7 +397,6 @@ namespace smt {
     template<typename Ext>
     final_check_status theory_utvpi<Ext>::final_check_eh() {
         SASSERT(is_consistent());
-        TRACE("utvpi", display(tout););
         if (can_propagate()) {
             propagate();
             return FC_CONTINUE;
@@ -424,7 +423,7 @@ namespace smt {
         unsigned sz = get_num_vars();
         for (unsigned i = 0; i < sz; ++i) {
             enode* e = get_enode(i);
-            if (a.is_int(e->get_owner())) {
+            if (!a.is_int(e->get_owner())) {
                 continue;
             }
             th_var v1 = to_var(i);
@@ -667,14 +666,80 @@ namespace smt {
         return m_graph.is_feasible();
     }
 
+
+    template<typename Ext>
+    bool theory_utvpi<Ext>::is_parity_ok(unsigned i) const {
+        th_var v1 = to_var(i);
+        th_var v2 = neg(v1);
+        rational r1 = m_graph.get_assignment(v1).get_rational();
+        rational r2 = m_graph.get_assignment(v2).get_rational();
+        return r1.is_even() == r2.is_even();
+    }
+
+ 
+    template<typename Ext>
+    void theory_utvpi<Ext>::enforce_parity() {
+       unsigned_vector todo;
+        
+        unsigned sz = get_num_vars();
+        for (unsigned i = 0; i < sz; ++i) {
+            enode* e = get_enode(i);
+            if (a.is_int(e->get_owner()) && !is_parity_ok(i)) {
+                todo.push_back(i);
+            }            
+        }
+        if (todo.empty()) {
+            return;
+        }
+        while (!todo.empty()) {
+            unsigned i = todo.back();
+            if (is_parity_ok(i)) {
+                continue;
+            }
+            todo.pop_back();
+            th_var v1 = to_var(i);
+            th_var v2 = neg(v1);
+            TRACE("utvpi", tout << "disparity: " << v1 << "\n";);
+            int_vector zero_v;
+            m_graph.compute_zero_succ(v1, zero_v);
+            bool found0 = false;
+            for (unsigned j = 0; !found0 && j < zero_v.size(); ++j) {
+                found0 = 
+                    (to_var(m_zero_int) == zero_v[j]) ||
+                    (neg(to_var(m_zero_int)) == zero_v[j]);                
+            }
+            if (found0) {
+                zero_v.reset();
+                m_graph.compute_zero_succ(v2, zero_v);
+            }
+            TRACE("utvpi", 
+                  for (unsigned j = 0; j < zero_v.size(); ++j) {
+                      tout << "increment: " << zero_v[j] << "\n";
+                  });
+
+            for (unsigned j = 0; j < zero_v.size(); ++j) {
+                int v = zero_v[j];
+                m_graph.acc_assignment(v, numeral(1));
+                th_var k = from_var(v);
+                if (!is_parity_ok(k)) {
+                    TRACE("utvpi", tout << "new disparity: " << k << "\n";);
+                    todo.push_back(k);
+                }
+            }            
+        }
+    }
+    
+
     // models:
     template<typename Ext>
     void theory_utvpi<Ext>::init_model(model_generator & m) {    
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
-        // TBD: enforce strong or tight coherence?
+        // TBD: enforce strong or tight coherence
+        enforce_parity();
         compute_delta();   
-        DEBUG_CODE(validate_model(););
+        // DEBUG_CODE(validate_model(););
+        validate_model();
     }
 
     template<typename Ext>    
@@ -688,7 +753,8 @@ namespace smt {
             }
             bool ok = true;
             expr* e = ctx.bool_var2expr(b);
-            switch(ctx.get_assignment(b)) {
+            lbool assign = ctx.get_assignment(b);
+            switch(assign) {
             case l_true:
                 ok = eval(e);
                 break;
@@ -698,7 +764,23 @@ namespace smt {
             default:
                 break;
             }
-            CTRACE("utvpi", !ok, tout << "validation failed:  " << mk_pp(e, get_manager()) << "\n";);
+            CTRACE("utvpi", !ok, 
+                   tout << "validation failed:\n";
+                   tout << "Assignment: " << assign << "\n";
+                   m_atoms[i].display(*this, tout);
+                   tout << "\n";
+                   display(tout);
+                   m_graph.display_agl(tout);
+                   );
+            if (!ok) {
+                std::cout << "validation failed:\n";
+                std::cout << "Assignment: " << assign << "\n";
+                m_atoms[i].display(*this, std::cout);
+                std::cout << "\n";
+                display(std::cout);
+                m_graph.display_agl(std::cout);
+
+            }
             // CTRACE("utvpi",  ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
             SASSERT(ok);
         }
@@ -751,7 +833,7 @@ namespace smt {
             return eval_num(e1);
         }
         if (is_uninterp_const(e)) {
-            return mk_value(mk_var(e));
+            return mk_value(mk_var(e), a.is_int(e));
         }
         TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";);
         UNREACHABLE();
@@ -760,23 +842,30 @@ namespace smt {
 
 
     template<typename Ext>    
-    rational theory_utvpi<Ext>::mk_value(th_var v) {
+        rational theory_utvpi<Ext>::mk_value(th_var v, bool is_int) {
         SASSERT(v != null_theory_var);
         numeral val1 = m_graph.get_assignment(to_var(v));
         numeral val2 = m_graph.get_assignment(neg(to_var(v)));
         numeral val = val1 - val2;
         rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational());
         num = num/rational(2);
+        if (is_int && !num.is_int()) {
             num = floor(num);
+        }
+        TRACE("utvpi", 
+              expr* n = get_enode(v)->get_owner();
+              tout << mk_pp(n, get_manager()) << " |-> (" << val1 << " - " << val2 << ")/2 = " << num << "\n";);
+
         return num;
     }
     
     template<typename Ext>    
     model_value_proc * theory_utvpi<Ext>::mk_value(enode * n, model_generator & mg) {
         theory_var v = n->get_th_var(get_id());
-        rational num = mk_value(v);
+        bool is_int = a.is_int(n->get_owner());
+        rational num = mk_value(v, is_int);
         TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
-        return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner())));
+        return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int));
     }
 
     /**