mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
Adding @Override declarations
They are important, as they prevent miss-spelling the parent method and /or arguments name.
This commit is contained in:
parent
a3a8ba40e7
commit
1dcaddbec7
|
@ -29,6 +29,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
*
|
||||
* @param o another AST
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
AST casted = null;
|
||||
|
@ -56,6 +57,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
* positive if after else zero.
|
||||
* @throws Z3Exception on error
|
||||
**/
|
||||
@Override
|
||||
public int compareTo(AST other)
|
||||
{
|
||||
if (other == null)
|
||||
|
@ -74,6 +76,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
*
|
||||
* @return A hash code
|
||||
**/
|
||||
@Override
|
||||
public int hashCode()
|
||||
{
|
||||
int r = 0;
|
||||
|
@ -188,6 +191,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
/**
|
||||
* A string representation of the AST.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -217,6 +221,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
// Console.WriteLine("AST IncRef()");
|
||||
|
@ -226,6 +231,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
// Console.WriteLine("AST DecRef()");
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -101,6 +101,7 @@ class ASTMap extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the map.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -122,12 +123,14 @@ class ASTMap extends Z3Object
|
|||
super(ctx, Native.mkAstMap(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getASTMapDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getASTMapDRQ().add(o);
|
||||
|
|
|
@ -87,6 +87,7 @@ public class ASTVector extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the vector.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -108,12 +109,14 @@ public class ASTVector extends Z3Object
|
|||
super(ctx, Native.mkAstVector(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getASTVectorDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getASTVectorDRQ().add(o);
|
||||
|
|
|
@ -63,6 +63,7 @@ public class ApplyResult extends Z3Object
|
|||
/**
|
||||
* A string representation of the ApplyResult.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -79,12 +80,14 @@ public class ApplyResult extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getApplyResultDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getApplyResultDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -61,6 +61,7 @@ public class BitVecNum extends BitVecExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -206,6 +206,7 @@ public class Expr extends AST
|
|||
/**
|
||||
* Returns a string representation of the expression.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return super.toString();
|
||||
|
@ -2117,6 +2118,7 @@ public class Expr extends AST
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (!Native.isApp(getContext().nCtx(), obj) &&
|
||||
|
|
|
@ -63,6 +63,7 @@ public class FiniteDomainNum extends FiniteDomainExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -252,6 +252,7 @@ public class Fixedpoint extends Z3Object
|
|||
/**
|
||||
* Retrieve internal string representation of fixedpoint object.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -353,12 +354,14 @@ public class Fixedpoint extends Z3Object
|
|||
super(ctx, Native.mkFixedpoint(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getFixedpointDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getFixedpointDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ public class FuncDecl extends AST
|
|||
/**
|
||||
* Object comparison.
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
FuncDecl casted = null;
|
||||
|
@ -58,6 +59,7 @@ public class FuncDecl extends AST
|
|||
/**
|
||||
* A string representations of the function declaration.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -72,6 +74,7 @@ public class FuncDecl extends AST
|
|||
/**
|
||||
* Returns a unique identifier for the function declaration.
|
||||
**/
|
||||
@Override
|
||||
public int getId()
|
||||
{
|
||||
return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
|
||||
|
|
|
@ -70,6 +70,7 @@ public class FuncInterp extends Z3Object
|
|||
/**
|
||||
* A string representation of the function entry.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -91,12 +92,14 @@ public class FuncInterp extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getFuncEntryDRQ().add(o);
|
||||
|
@ -192,12 +195,14 @@ public class FuncInterp extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getFuncInterpDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class GoalDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class GoalDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -46,6 +46,7 @@ public class IntSymbol extends Symbol
|
|||
super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
|
||||
|
|
|
@ -282,6 +282,7 @@ public class Model extends Z3Object
|
|||
*
|
||||
* @return A string representation of the model.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -298,12 +299,14 @@ public class Model extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getModelDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getModelDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ModelDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ModelDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -112,8 +112,9 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Print a string representation of the handle.
|
||||
**/
|
||||
public String toString()
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return getValue().toString();
|
||||
}
|
||||
|
@ -237,7 +238,8 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Print the context to a String (SMT-LIB parseable benchmark).
|
||||
**/
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
|
||||
|
@ -262,13 +264,14 @@ public class Optimize extends Z3Object
|
|||
super(ctx, Native.mkOptimize(ctx.nCtx()));
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getOptimizeDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getOptimizeDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -72,6 +72,7 @@ public class ParamDescrs extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the ParamDescrs.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -88,12 +89,14 @@ public class ParamDescrs extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getParamDescrsDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -112,6 +112,7 @@ public class Params extends Z3Object
|
|||
/**
|
||||
* A string representation of the parameter set.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -128,12 +129,14 @@ public class Params extends Z3Object
|
|||
super(ctx, Native.mkParams(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getParamsDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getParamsDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ParamsDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ParamsDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -50,6 +50,7 @@ public class Pattern extends AST
|
|||
/**
|
||||
* A string representation of the pattern.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -51,12 +51,14 @@ public class Probe extends Z3Object
|
|||
super(ctx, Native.mkProbe(ctx.nCtx(), name));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getProbeDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getProbeDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ProbeDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ProbeDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -74,6 +74,7 @@ public class RatNum extends RealExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -315,6 +315,7 @@ public class Solver extends Z3Object
|
|||
/**
|
||||
* A string representation of the solver.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -332,12 +333,14 @@ public class Solver extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getSolverDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getSolverDRQ().add(o);
|
||||
|
|
|
@ -26,6 +26,7 @@ class SolverDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -37,6 +38,7 @@ class SolverDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -30,6 +30,7 @@ public class Sort extends AST
|
|||
* @param o
|
||||
* @return
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
Sort casted = null;
|
||||
|
|
|
@ -44,6 +44,7 @@ public class StringSymbol extends Symbol
|
|||
super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
|
||||
|
|
|
@ -62,6 +62,7 @@ public class Symbol extends Z3Object
|
|||
/**
|
||||
* A string representation of the symbol.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
Loading…
Reference in a new issue