Small polysat fixes (#5183)

* Add some display functions

* Add new variables to free vars

src/math/polysat/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(polysat
   SOURCES
     solver.cpp
     constraint.cpp
+    justification.cpp
   COMPONENT_DEPENDENCIES
     util
     dd

src/math/polysat/justification.cpp

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat justification
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+
+--*/
+
+#include "math/polysat/justification.h"
+
+namespace polysat {
+
+    std::ostream& justification::display(std::ostream& out) const {
+        switch (kind()) {
+        case justification_k::unassigned:
+            return out << "unassigned";
+        case justification_k::decision:
+            return out << "decision (level " << level() << ")";
+        case justification_k::propagation:
+            return out << "propagation (level " << level() << ")";
+        }
+    }
+
+}

src/math/polysat/solver.cpp

@@ -100,6 +100,7 @@ namespace polysat {
         m_vars.push_back(sz2pdd(sz).mk_var(v));
         m_size.push_back(sz);
         m_trail.push(t_del_var(*this));
+        m_free_vars.mk_var_eh(v);
         return v;
     }
 
@@ -115,6 +116,7 @@ namespace polysat {
         m_activity.pop_back();
         m_vars.pop_back();
         m_size.pop_back();
+        m_free_vars.del_var_eh(v);
     }
 
     void solver::add_eq(pdd const& p, unsigned dep) {

src/util/var_queue.h

@@ -76,5 +76,21 @@ public:
     var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
     
     bool more_active(var v1, var v2) const { return m_queue.less_than(v1, v2); }
+
+    std::ostream& display(std::ostream& out) const {
+        bool first = true;
+        for (auto v : m_queue) {
+            if (first) {
+                first = false;
+            } else {
+                out << " ";
+            }
+            out << v;
+        }
+        return out;
+    }
 };
 
+inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) {
+    return queue.display(out);
+}