From bc4f587acc8a70cfbe4b934c024830f07e592536 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 8 Jan 2026 18:46:47 -0800
Subject: [PATCH] Add missing C# API functions for solver introspection and
 congruence closure (#8126)

* Initial plan

* Add missing C# API functions for NonUnits, Trail, and Congruence methods

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix formatting: remove extra blank lines in new properties

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/dotnet/NativeSolver.cs | 44 +++++++++++++++++++++++++
 src/api/dotnet/Solver.cs       | 60 ++++++++++++++++++++++++++++++++++
 2 files changed, 104 insertions(+)

diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs
index 7dc937234..acf8b177d 100644
--- a/src/api/dotnet/NativeSolver.cs
+++ b/src/api/dotnet/NativeSolver.cs
@@ -277,6 +277,50 @@ namespace Microsoft.Z3
         public Z3_ast[] Units
             => ntvContext.ToArray(Native.Z3_solver_get_units(nCtx, z3solver));
 
+        /// <summary>
+        /// Non-unit literals in the solver state.
+        /// </summary>
+        public Z3_ast[] NonUnits
+            => ntvContext.ToArray(Native.Z3_solver_get_non_units(nCtx, z3solver));
+
+        /// <summary>
+        /// Trail of the solver state after a check() call.
+        /// </summary>
+        public Z3_ast[] Trail
+            => ntvContext.ToArray(Native.Z3_solver_get_trail(nCtx, z3solver));
+
+        /// <summary>
+        /// Retrieve congruence closure root of the term t relative to the current search state.
+        /// The function primarily works for SimpleSolver.
+        /// Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
+        /// </summary>
+        public Z3_ast CongruenceRoot(Z3_ast t)
+        {
+            Debug.Assert(t != IntPtr.Zero);
+            return Native.Z3_solver_congruence_root(nCtx, z3solver, t);
+        }
+
+        /// <summary>
+        /// Retrieve congruence closure sibling of the term t relative to the current search state.
+        /// The function primarily works for SimpleSolver.
+        /// Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
+        /// </summary>
+        public Z3_ast CongruenceNext(Z3_ast t)
+        {
+            Debug.Assert(t != IntPtr.Zero);
+            return Native.Z3_solver_congruence_next(nCtx, z3solver, t);
+        }
+
+        /// <summary>
+        /// Explain congruence of a and b relative to the current search state.
+        /// </summary>
+        public Z3_ast CongruenceExplain(Z3_ast a, Z3_ast b)
+        {
+            Debug.Assert(a != IntPtr.Zero);
+            Debug.Assert(b != IntPtr.Zero);
+            return Native.Z3_solver_congruence_explain(nCtx, z3solver, a, b);
+        }
+
         /// <summary>
         /// Checks whether the assertions in the solver are consistent or not.
         /// </summary>
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 00b5117ea..c9651e16a 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -325,6 +325,66 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Non-unit literals in the solver state.
+        /// </summary>
+        public BoolExpr[] NonUnits
+        {
+            get
+            {
+                using ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_non_units(Context.nCtx, NativeObject));
+                return assertions.ToBoolExprArray();
+            }
+        }
+
+        /// <summary>
+        /// Trail of the solver state after a check() call.
+        /// </summary>
+        public BoolExpr[] Trail
+        {
+            get
+            {
+                using ASTVector trail = new ASTVector(Context, Native.Z3_solver_get_trail(Context.nCtx, NativeObject));
+                return trail.ToBoolExprArray();
+            }
+        }
+
+        /// <summary>
+        /// Retrieve congruence closure root of the term t relative to the current search state.
+        /// The function primarily works for SimpleSolver.
+        /// Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
+        /// </summary>
+        public Expr CongruenceRoot(Expr t)
+        {
+            Debug.Assert(t != null);
+            Context.CheckContextMatch(t);
+            return Expr.Create(Context, Native.Z3_solver_congruence_root(Context.nCtx, NativeObject, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Retrieve congruence closure sibling of the term t relative to the current search state.
+        /// The function primarily works for SimpleSolver.
+        /// Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
+        /// </summary>
+        public Expr CongruenceNext(Expr t)
+        {
+            Debug.Assert(t != null);
+            Context.CheckContextMatch(t);
+            return Expr.Create(Context, Native.Z3_solver_congruence_next(Context.nCtx, NativeObject, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Explain congruence of a and b relative to the current search state.
+        /// </summary>
+        public Expr CongruenceExplain(Expr a, Expr b)
+        {
+            Debug.Assert(a != null);
+            Debug.Assert(b != null);
+            Context.CheckContextMatch(a);
+            Context.CheckContextMatch(b);
+            return Expr.Create(Context, Native.Z3_solver_congruence_explain(Context.nCtx, NativeObject, a.NativeObject, b.NativeObject));
+        }
+
         /// <summary>
         /// Checks whether the assertions in the solver are consistent or not.
         /// </summary>