From 6b3adcf2598458ae25fbbd1af4f24327caa31df1 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 9 Jan 2026 09:04:56 -0800
Subject: [PATCH] Add solver introspection APIs to Java bindings (getUnits,
 getNonUnits, getTrail) (#8130)

* Initial plan

* Add getUnits(), getNonUnits(), and getTrail() methods to Java Solver API

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

* Add SolverIntrospectionExample and update Java examples README

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

* Revert changes in examples/java directory, keep only Solver.java API changes

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/java/Solver.java | 42 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index b814a4db6..b34b72e3b 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -338,6 +338,48 @@ public class Solver extends Z3Object {
         return core.ToBoolExprArray();
     }
 
+    /**
+     * Retrieve currently inferred units.
+     * Remarks: This retrieves the set of literals that the solver has inferred
+     * at the current decision level after a {@code check} call.
+     * 
+     * @return An array of Boolean expressions representing the inferred units
+     * @throws Z3Exception
+     **/
+    public BoolExpr[] getUnits()
+    {
+        ASTVector units = new ASTVector(getContext(), Native.solverGetUnits(getContext().nCtx(), getNativeObject()));
+        return units.ToBoolExprArray();
+    }
+
+    /**
+     * Retrieve non-unit atomic formulas in the solver state.
+     * Remarks: This retrieves atomic formulas that are not units after a {@code check} call.
+     * 
+     * @return An array of Boolean expressions representing the non-unit formulas
+     * @throws Z3Exception
+     **/
+    public BoolExpr[] getNonUnits()
+    {
+        ASTVector nonUnits = new ASTVector(getContext(), Native.solverGetNonUnits(getContext().nCtx(), getNativeObject()));
+        return nonUnits.ToBoolExprArray();
+    }
+
+    /**
+     * Retrieve the solver decision trail.
+     * Remarks: This retrieves the trail of decisions made by the solver after a {@code check} call.
+     * The trail represents the sequence of Boolean literals (decisions and propagations) in the order
+     * they were assigned.
+     * 
+     * @return An array of Boolean expressions representing the decision trail
+     * @throws Z3Exception
+     **/
+    public BoolExpr[] getTrail()
+    {
+        ASTVector trail = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
+        return trail.ToBoolExprArray();
+    }
+
     /**
      * A brief justification of why the last call to {@code Check} returned
      * {@code UNKNOWN}.