mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 00:07:36 +00:00
Code Activity

Merge pull request #8710 from Z3Prover/copilot/fix-discussed-issues-8709

Browse source 
Align congruence closure API naming in Python and Java bindings
This commit is contained in:
Nikolaj Bjorner 2026-02-20 19:13:11 -08:00 • committed by GitHub
commit ee1a6a2f91
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -472,7 +472,7 @@ public class Solver extends Z3Object {
* @return The root expression of the congruence class
* @throws Z3Exception
**/
public Expr<?> getCongruenceRoot(Expr<?> t)
public Expr<?> congruenceRoot(Expr<?> t)
{
getContext().checkContextMatch(t);
return Expr.create(getContext(),
@ -487,7 +487,7 @@ public class Solver extends Z3Object {
* @return The next expression in the congruence class
* @throws Z3Exception
**/
public Expr<?> getCongruenceNext(Expr<?> t)
public Expr<?> congruenceNext(Expr<?> t)
{
getContext().checkContextMatch(t);
return Expr.create(getContext(),
@ -502,7 +502,7 @@ public class Solver extends Z3Object {
* @return An expression explaining the congruence between a and b
* @throws Z3Exception
**/
public Expr<?> getCongruenceExplain(Expr<?> a, Expr<?> b)
public Expr<?> congruenceExplain(Expr<?> a, Expr<?> b)
{
getContext().checkContextMatch(a);
getContext().checkContextMatch(b);

6
src/api/python/z3/z3.py
View file

@ -7777,7 +7777,7 @@ class Solver(Z3PPObject):
cube are likely more useful to cube on."""
return self.cube_vs
def root(self, t):
def congruence_root(self, t):
"""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.
@ -7785,7 +7785,7 @@ class Solver(Z3PPObject):
t = _py2expr(t, self.ctx)
return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
def next(self, t):
def congruence_next(self, t):
"""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.
@ -7793,7 +7793,7 @@ class Solver(Z3PPObject):
t = _py2expr(t, self.ctx)
return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
def explain_congruent(self, a, b):
def congruence_explain(self, a, b):
"""Explain congruence of a and b relative to the current search state"""
a = _py2expr(a, self.ctx)
b = _py2expr(b, self.ctx)