mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 01:45:15 +00:00
Code Activity

Add solver introspection APIs to Java bindings (getUnits, getNonUnits, getTrail) (#8130)

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-09 09:04:56 -08:00 • committed by Nikolaj Bjorner
parent 5bf49cbd5a
commit 6b3adcf259
1 changed files with 42 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/api/java/Solver.java
View file

@ -338,6 +338,48 @@ public class Solver extends Z3Object {
return core.ToBoolExprArray(); 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 * A brief justification of why the last call to {@code Check} returned
* {@code UNKNOWN}. * {@code UNKNOWN}.