mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Warning fix for Comparable<T> in Java API
This commit is contained in:
parent
00ce124db3
commit
9e756fb6db
|
@ -22,7 +22,7 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
|
||||||
/**
|
/**
|
||||||
* The abstract syntax tree (AST) class.
|
* The abstract syntax tree (AST) class.
|
||||||
**/
|
**/
|
||||||
public class AST extends Z3Object implements Comparable
|
public class AST extends Z3Object implements Comparable<AST>
|
||||||
{
|
{
|
||||||
/**
|
/**
|
||||||
* Object comparison.
|
* Object comparison.
|
||||||
|
@ -56,23 +56,14 @@ public class AST extends Z3Object implements Comparable
|
||||||
* positive if after else zero.
|
* positive if after else zero.
|
||||||
* @throws Z3Exception on error
|
* @throws Z3Exception on error
|
||||||
**/
|
**/
|
||||||
public int compareTo(Object other)
|
public int compareTo(AST other)
|
||||||
{
|
{
|
||||||
if (other == null)
|
if (other == null)
|
||||||
return 1;
|
return 1;
|
||||||
|
|
||||||
AST oAST = null;
|
if (getId() < other.getId())
|
||||||
try
|
|
||||||
{
|
|
||||||
oAST = AST.class.cast(other);
|
|
||||||
} catch (ClassCastException e)
|
|
||||||
{
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (getId() < oAST.getId())
|
|
||||||
return -1;
|
return -1;
|
||||||
else if (getId() > oAST.getId())
|
else if (getId() > other.getId())
|
||||||
return +1;
|
return +1;
|
||||||
else
|
else
|
||||||
return 0;
|
return 0;
|
||||||
|
|
Loading…
Reference in a new issue