mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 14:13:23 +00:00
Since classes are non-final "instanceof" check is better in #equals
This commit is contained in:
parent
529b9d6833
commit
f93c41b1be
4 changed files with 4 additions and 8 deletions
|
@ -32,9 +32,8 @@ public class AST extends Z3Object implements Comparable<AST>
|
||||||
@Override
|
@Override
|
||||||
public boolean equals(Object o)
|
public boolean equals(Object o)
|
||||||
{
|
{
|
||||||
if (o == null) return false;
|
|
||||||
if (o == this) return true;
|
if (o == this) return true;
|
||||||
if (o.getClass() != this.getClass()) return false;
|
if (!(o instanceof AST)) return false;
|
||||||
AST casted = (AST) o;
|
AST casted = (AST) o;
|
||||||
|
|
||||||
return
|
return
|
||||||
|
|
|
@ -32,9 +32,8 @@ public class FuncDecl extends AST
|
||||||
@Override
|
@Override
|
||||||
public boolean equals(Object o)
|
public boolean equals(Object o)
|
||||||
{
|
{
|
||||||
if (o == null) return false;
|
|
||||||
if (o == this) return true;
|
if (o == this) return true;
|
||||||
if (o.getClass() != this.getClass()) return false;
|
if (!(o instanceof FuncDecl)) return false;
|
||||||
FuncDecl other = (FuncDecl) o;
|
FuncDecl other = (FuncDecl) o;
|
||||||
|
|
||||||
return
|
return
|
||||||
|
|
|
@ -31,9 +31,8 @@ public class Sort extends AST
|
||||||
@Override
|
@Override
|
||||||
public boolean equals(Object o)
|
public boolean equals(Object o)
|
||||||
{
|
{
|
||||||
if (o == null) return false;
|
|
||||||
if (o == this) return true;
|
if (o == this) return true;
|
||||||
if (o.getClass() != this.getClass()) return false;
|
if (!(o instanceof Sort)) return false;
|
||||||
Sort other = (Sort) o;
|
Sort other = (Sort) o;
|
||||||
|
|
||||||
return (getContext().nCtx() == other.getContext().nCtx()) &&
|
return (getContext().nCtx() == other.getContext().nCtx()) &&
|
||||||
|
|
|
@ -52,9 +52,8 @@ public class Symbol extends Z3Object
|
||||||
@Override
|
@Override
|
||||||
public boolean equals(Object o)
|
public boolean equals(Object o)
|
||||||
{
|
{
|
||||||
if (o == null) return false;
|
|
||||||
if (o == this) return true;
|
if (o == this) return true;
|
||||||
if (o.getClass() != this.getClass()) return false;
|
if (!(o instanceof Symbol)) return false;
|
||||||
Symbol other = (Symbol) o;
|
Symbol other = (Symbol) o;
|
||||||
return this.getNativeObject() == other.getNativeObject();
|
return this.getNativeObject() == other.getNativeObject();
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue