From f9b1b4e65dd4375fecdb1e2f2ca7239eaca2635f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Sep 2021 14:13:31 +0200
Subject: [PATCH] add mode to display to get constraints without wild-card
 notation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/constraint.h       | 3 ++-
 src/math/polysat/ule_constraint.cpp | 9 +++++++++
 src/math/polysat/ule_constraint.h   | 1 +
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 2725ec466..5f0da9368 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -160,7 +160,8 @@ namespace polysat {
         virtual bool is_eq() const { return false; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
         ckind_t kind() const { return m_kind; }
-        virtual std::ostream& display(std::ostream& out, lbool status = l_undef) const = 0;
+        virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
+        virtual std::ostream& display(std::ostream& out) const = 0;
 
         bool propagate(solver& s, bool is_positive, pvar v);
         virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index ccc23876a..eab319365 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -42,6 +42,15 @@ namespace polysat {
         return display_extra(out, status);
     }
 
+    std::ostream& ule_constraint::display(std::ostream& out) const {
+        out << m_lhs;
+        if (is_eq())
+            out << " == ";
+        else
+            out << " <= ";
+        return out << m_rhs;        
+    }
+
     void ule_constraint::narrow(solver& s, bool is_positive) {
         LOG_H3("Narrowing " << *this);
         LOG("Assignment: " << assignments_pp(s));
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index d4b63d7d4..f7e978db0 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -36,6 +36,7 @@ namespace polysat {
         pdd const& lhs() const { return m_lhs; }
         pdd const& rhs() const { return m_rhs; }
         std::ostream& display(std::ostream& out, lbool status) const override;
+        std::ostream& display(std::ostream& out) const;
         bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const;
         bool is_always_false(bool is_positive) const override;
         bool is_currently_false(solver& s, bool is_positive) const override;