mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Add missing C# API functions for solver introspection and congruence closure (#8126)

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-08 18:46:47 -08:00 • committed by GitHub
parent 7a35caa60a
commit bc4f587acc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 104 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/api/dotnet/NativeSolver.cs
View file

@ -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>

60
src/api/dotnet/Solver.cs
View file

@ -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>