pretty printing

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

src/math/polysat/eq_constraint.cpp

@@ -34,7 +34,7 @@ namespace polysat {
 
     void eq_constraint::narrow(solver& s) {
         SASSERT(!is_undef());
-        LOG("Assignment: " << s.assignment());
+        LOG("Assignment: " << assignments_pp(s));
         auto q = p().subst_val(s.assignment());
         LOG("Substituted: " << p() << " := " << q);
         if (q.is_zero()) {

src/math/polysat/solver.cpp

@@ -124,7 +124,7 @@ namespace polysat {
             m_stats.m_num_iterations++;
             LOG_H1("Next solving loop iteration");
             LOG("Free variables: " << m_free_vars);
-            LOG("Assignments:    " << assignment());
+            LOG("Assignment:     " << assignments_pp(*this));
             LOG("Conflict:       " << m_conflict);
             IF_LOGGING(log_viable());
 
@@ -286,7 +286,7 @@ namespace polysat {
     }
 
     void solver::propagate(pvar v, rational const& val, constraint& c) {
-        LOG("Propagation: pvar " << v << " := " << val << ", due to " << c);
+        LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
         if (is_viable(v, val)) {
             m_free_vars.del_var_eh(v);
             assign_core(v, val, justification::propagation(m_level));        
@@ -1224,6 +1224,22 @@ namespace polysat {
         return out;
     }
 
+    std::ostream& assignments_pp::display(std::ostream& out) const {
+        for (auto [var, val] : s.assignment())
+            out << assignment_pp(s, var, val) << " ";
+        return out;
+    }
+
+    std::ostream& assignment_pp::display(std::ostream& out) const {
+        out << "v" << var << " := ";
+        rational const& p = rational::power_of_two(s.size(var));
+        if (val > mod(-val, p))
+            return out << -mod(-val, p);
+        else 
+            return out << val;
+    }
+    
+
     void solver::collect_statistics(statistics& st) const {
         st.update("polysat iterations",   m_stats.m_num_iterations);
         st.update("polysat decisions",    m_stats.m_num_decisions);

src/math/polysat/solver.h

@@ -52,6 +52,8 @@ namespace polysat {
         friend class conflict_explainer;
         friend class forbidden_intervals;
         friend class linear_solver;
+        friend class assignment_pp;
+        friend class assignments_pp;
 
         typedef ptr_vector<constraint> constraints;
 
@@ -380,8 +382,28 @@ namespace polysat {
 
     };
 
+    class assignments_pp {
+        solver& s;
+    public:
+        assignments_pp(solver& s): s(s) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    class assignment_pp {
+        solver& s;
+        pvar var;
+        rational const& val;
+    public:
+        assignment_pp(solver& s, pvar var, rational const& val): s(s), var(var), val(val) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
     inline std::ostream& operator<<(std::ostream& out, solver const& s) { return s.display(out); }
 
+    inline std::ostream& operator<<(std::ostream& out, assignment_pp const& p) { return p.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }
+
 }
 
 

src/math/polysat/ule_constraint.cpp

@@ -29,7 +29,7 @@ namespace polysat {
 
     void ule_constraint::narrow(solver& s) {
         LOG_H3("Narrowing " << *this);
-        LOG("Assignment: " << s.assignment());
+        LOG("Assignment: " << assignments_pp(s));
         auto p = lhs().subst_val(s.assignment());
         LOG("Substituted LHS: " << lhs() << " := " << p);
         auto q = rhs().subst_val(s.assignment());