From 9b10733ebd712098e74c77a009c2d2f259141365 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 30 Nov 2022 14:50:14 +0100
Subject: [PATCH] assignment helpers

---
 src/math/polysat/assignment.cpp | 13 +++++++++++++
 src/math/polysat/assignment.h   |  4 ++++
 2 files changed, 17 insertions(+)

diff --git a/src/math/polysat/assignment.cpp b/src/math/polysat/assignment.cpp
index 70bbb55ed..2b85e603a 100644
--- a/src/math/polysat/assignment.cpp
+++ b/src/math/polysat/assignment.cpp
@@ -31,6 +31,11 @@ namespace polysat {
         return p.subst_val(m_subst);
     }
 
+    bool substitution::contains(pvar var) const {
+        rational out_value;
+        return value(var, out_value);
+    }
+
     bool substitution::value(pvar var, rational& out_value) const {
         return m_subst.subst_get(var, out_value);
     }
@@ -49,6 +54,14 @@ namespace polysat {
         return a;
     }
 
+    bool assignment::contains(pvar var) const {
+        return subst(s().size(var)).contains(var);
+    }
+
+    bool assignment::value(pvar var, rational& out_value) const {
+        return subst(s().size(var)).value(var, out_value);
+    }
+
     substitution& assignment::subst(unsigned sz) {
         return const_cast<substitution&>(std::as_const(*this).subst(sz));
     }
diff --git a/src/math/polysat/assignment.h b/src/math/polysat/assignment.h
index db2e52b68..2f8f65474 100644
--- a/src/math/polysat/assignment.h
+++ b/src/math/polysat/assignment.h
@@ -56,6 +56,7 @@ namespace polysat {
         substitution add(pvar var, rational const& value) const;
         pdd apply_to(pdd const& p) const;
 
+        bool contains(pvar var) const;
         bool value(pvar var, rational& out_value) const;
 
         bool empty() const { return m_subst.is_one(); }
@@ -96,6 +97,9 @@ namespace polysat {
 
         pdd apply_to(pdd const& p) const;
 
+        bool contains(pvar var) const;
+        bool value(pvar var, rational& out_value) const;
+        rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
         bool empty() const { return pairs().empty(); }
         substitution const& subst(unsigned sz) const;
         vector<assignment_item_t> const& pairs() const { return m_pairs; }