mirror of
https://github.com/Z3Prover/z3
synced 2025-06-13 17:36:15 +00:00
Consistent Sort#equals
This commit is contained in:
parent
a816b4895c
commit
d0d7a5b712
1 changed files with 10 additions and 13 deletions
|
@ -33,20 +33,17 @@ public class Sort extends AST
|
||||||
@Override
|
@Override
|
||||||
public boolean equals(Object o)
|
public boolean equals(Object o)
|
||||||
{
|
{
|
||||||
Sort casted = null;
|
if (o == null) return false;
|
||||||
|
if (o == this) return true;
|
||||||
|
if (o.getClass() != this.getClass()) return false;
|
||||||
|
Sort other = (Sort) o;
|
||||||
|
|
||||||
try {
|
return (getContext().nCtx() == other.getContext().nCtx()) &&
|
||||||
casted = Sort.class.cast(o);
|
(Native.isEqSort(
|
||||||
} catch (ClassCastException e) {
|
getContext().nCtx(),
|
||||||
return false;
|
getNativeObject(),
|
||||||
}
|
other.getNativeObject()
|
||||||
|
));
|
||||||
return
|
|
||||||
(this == casted) ||
|
|
||||||
(this != null) &&
|
|
||||||
(casted != null) &&
|
|
||||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
|
||||||
(Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue