From 8e84aac36cdd4ffdf0bde93c1081897cc77c864c Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 21 Dec 2023 14:34:12 +0100
Subject: [PATCH] solver::eval

---
 src/math/polysat/solver.cpp | 6 ++++++
 src/math/polysat/solver.h   | 1 +
 2 files changed, 7 insertions(+)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b9d41cec9..ed05dd498 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1473,6 +1473,12 @@ namespace polysat {
         return r.is_val();
     }
 
+    rational solver::eval(pdd const& p) const {
+        rational r;
+        VERIFY(try_eval(p, r));
+        return r;
+    }
+
     /**
      * Variable activity accounting.
      * As a placeholder we increment activity
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 00669a44c..046ce20d3 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -415,6 +415,7 @@ namespace polysat {
          * Evaluate term under the current assignment.
          */
         bool try_eval(pdd const& p, rational& out_value) const;
+        rational eval(pdd const& p) const;
 
         /**
          * Add variable with bit-size.