mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
Fixed .equals for AST, FuncDecl, and Sort, and AST.compareTo in Java
Fixes #143
This commit is contained in:
parent
5f755a5bd8
commit
1bad614646
3 changed files with 21 additions and 26 deletions
|
@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind;
|
|||
**/
|
||||
public class FuncDecl extends AST
|
||||
{
|
||||
/**
|
||||
* Comparison operator.
|
||||
*
|
||||
* @return True if {@code a"/> and <paramref name="b} share the
|
||||
* same context and are equal, false otherwise.
|
||||
**/
|
||||
/* Overloaded operators are not translated. */
|
||||
|
||||
/**
|
||||
* Comparison operator.
|
||||
*
|
||||
* @return True if {@code a"/> and <paramref name="b} do not
|
||||
* share the same context or are not equal, false otherwise.
|
||||
**/
|
||||
/* Overloaded operators are not translated. */
|
||||
|
||||
/**
|
||||
* Object comparison.
|
||||
**/
|
||||
|
@ -55,7 +39,12 @@ public class FuncDecl extends AST
|
|||
return false;
|
||||
}
|
||||
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
return
|
||||
(this == casted) ||
|
||||
(this != null) &&
|
||||
(casted != null) &&
|
||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||
(Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue