From 92bb984305a34839c6d42f29ace3281b678a1d15 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 10:19:44 +0100 Subject: [PATCH 01/17] catch/throw is redundant. --- src/api/java/Z3Object.java | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 574a2820c..dc1feecbf 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -31,11 +31,7 @@ public class Z3Object extends IDisposable { try { dispose(); - } - catch (Throwable t) { - throw t; - } - finally { + } finally { super.finalize(); } } From 56db1867ef352cba591225958aae7665a3297e00 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 10:24:00 +0100 Subject: [PATCH 02/17] Proper idiomatic isEquals implementation. --- src/api/java/Symbol.java | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 44c08e572..b54474beb 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -49,17 +49,14 @@ public class Symbol extends Z3Object return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL; } + @Override public boolean equals(Object o) { - Symbol casted = null; - try { - casted = Symbol.class.cast(o); - } - catch (ClassCastException e) { - return false; - } - - return this.getNativeObject() == casted.getNativeObject(); + if (o == null) return false; + if (o == this) return true; + if (o.getClass() != this.getClass()) return false; + Symbol other = (Symbol) o; + return this.getNativeObject() == other.getNativeObject(); } /** From a3a8ba40e7e7314f776c32f177b4b0f0f41be907 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 10:25:52 +0100 Subject: [PATCH 03/17] "static final" does not do anything --- src/api/java/Status.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Status.java b/src/api/java/Status.java index a08f47909..c1f534d6a 100644 --- a/src/api/java/Status.java +++ b/src/api/java/Status.java @@ -38,7 +38,7 @@ public enum Status this.intValue = v; } - public static final Status fromInt(int v) + public static Status fromInt(int v) { for (Status k : values()) if (k.intValue == v) From 1dcaddbec735cfa3ee55ad9187c661dfcfc780b8 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:07:48 +0100 Subject: [PATCH 04/17] Adding @Override declarations They are important, as they prevent miss-spelling the parent method and /or arguments name. --- src/api/java/AST.java | 6 ++++++ src/api/java/ASTDecRefQueue.java | 2 ++ src/api/java/ASTMap.java | 3 +++ src/api/java/ASTVector.java | 3 +++ src/api/java/ApplyResult.java | 3 +++ src/api/java/ApplyResultDecRefQueue.java | 2 ++ src/api/java/AstMapDecRefQueue.java | 2 ++ src/api/java/AstVectorDecRefQueue.java | 2 ++ src/api/java/BitVecNum.java | 1 + src/api/java/Expr.java | 2 ++ src/api/java/FiniteDomainNum.java | 1 + src/api/java/Fixedpoint.java | 3 +++ src/api/java/FixedpointDecRefQueue.java | 2 ++ src/api/java/FuncDecl.java | 3 +++ src/api/java/FuncInterp.java | 5 +++++ src/api/java/FuncInterpDecRefQueue.java | 2 ++ src/api/java/FuncInterpEntryDecRefQueue.java | 2 ++ src/api/java/GoalDecRefQueue.java | 2 ++ src/api/java/IntSymbol.java | 1 + src/api/java/Model.java | 3 +++ src/api/java/ModelDecRefQueue.java | 2 ++ src/api/java/Optimize.java | 11 +++++++---- src/api/java/OptimizeDecRefQueue.java | 2 ++ src/api/java/ParamDescrs.java | 3 +++ src/api/java/ParamDescrsDecRefQueue.java | 2 ++ src/api/java/Params.java | 3 +++ src/api/java/ParamsDecRefQueue.java | 2 ++ src/api/java/Pattern.java | 1 + src/api/java/Probe.java | 2 ++ src/api/java/ProbeDecRefQueue.java | 2 ++ src/api/java/RatNum.java | 1 + src/api/java/Solver.java | 3 +++ src/api/java/SolverDecRefQueue.java | 2 ++ src/api/java/Sort.java | 1 + src/api/java/StringSymbol.java | 1 + src/api/java/Symbol.java | 1 + 36 files changed, 85 insertions(+), 4 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 4be02ce30..7bc2a79fc 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -29,6 +29,7 @@ public class AST extends Z3Object implements Comparable * * @param o another AST **/ + @Override public boolean equals(Object o) { AST casted = null; @@ -56,6 +57,7 @@ public class AST extends Z3Object implements Comparable * 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 * * @return A hash code **/ + @Override public int hashCode() { int r = 0; @@ -188,6 +191,7 @@ public class AST extends Z3Object implements Comparable /** * A string representation of the AST. **/ + @Override public String toString() { try @@ -217,6 +221,7 @@ public class AST extends Z3Object implements Comparable super(ctx, obj); } + @Override void incRef(long o) { // Console.WriteLine("AST IncRef()"); @@ -226,6 +231,7 @@ public class AST extends Z3Object implements Comparable super.incRef(o); } + @Override void decRef(long o) { // Console.WriteLine("AST DecRef()"); diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index a8ee83e57..32f6a5d0e 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -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 diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index afeb868ca..7bc485bf5 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -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); diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 5b57db9d9..ab99e2aee 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -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); diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 2812efd70..84c63e966 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -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); diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 4cdf312fe..63f315ecd 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -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 diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index 2106ff0c2..1598f75e7 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -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 diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index 698e9e06b..a63d808d3 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -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 diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 08da40256..cd5e789b9 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -61,6 +61,7 @@ public class BitVecNum extends BitVecExpr /** * Returns a string representation of the numeral. **/ + @Override public String toString() { try diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index e03d5b1c9..b59a41e1d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -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) && diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java index 79845c700..73613e4e0 100644 --- a/src/api/java/FiniteDomainNum.java +++ b/src/api/java/FiniteDomainNum.java @@ -63,6 +63,7 @@ public class FiniteDomainNum extends FiniteDomainExpr /** * Returns a string representation of the numeral. **/ + @Override public String toString() { try diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 0bdbfb571..a6ef9714c 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -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); diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index da2af3a41..e65538a30 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -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 diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index bc2baab91..ac72c4012 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -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()); diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 59a8a0398..fb549b3f2 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -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); diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index 56660d2f9..c888e9e3d 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -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 diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 406c0b33a..7dfdaa27d 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -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 diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index dd9d69414..be921241b 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -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 diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java index db99e6840..fab242d28 100644 --- a/src/api/java/IntSymbol.java +++ b/src/api/java/IntSymbol.java @@ -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 diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 17e5de2a2..16613af68 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -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); diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index c954a1fa8..b97add310 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -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 diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index f12bb7e06..9d62873e2 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -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); diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java index c9bc251e1..795a8a399 100644 --- a/src/api/java/OptimizeDecRefQueue.java +++ b/src/api/java/OptimizeDecRefQueue.java @@ -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 diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 514c65b46..9c6fbd0dc 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -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); diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index 95a92475e..e3515bff6 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -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 diff --git a/src/api/java/Params.java b/src/api/java/Params.java index c241ac8aa..8eef253b0 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -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); diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index 7b9f34c00..f989f8015 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -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 diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index d51315abf..eb12b6448 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -50,6 +50,7 @@ public class Pattern extends AST /** * A string representation of the pattern. **/ + @Override public String toString() { try diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index 625b41e09..bcaa76ce6 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -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); diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index e271bd949..368bd5bba 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -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 diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index 8fd815742..f44823a2b 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -74,6 +74,7 @@ public class RatNum extends RealExpr /** * Returns a string representation of the numeral. **/ + @Override public String toString() { try diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index f312da051..e58b140a6 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -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); diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index cbe5bbc3b..f4d5fb139 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -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 diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 1481a44e2..f59569132 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -30,6 +30,7 @@ public class Sort extends AST * @param o * @return **/ + @Override public boolean equals(Object o) { Sort casted = null; diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index efbd3a9d2..8470e1cd4 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -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 diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index b54474beb..b90f8d915 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -62,6 +62,7 @@ public class Symbol extends Z3Object /** * A string representation of the symbol. **/ + @Override public String toString() { try From 4d3675cb4e7a87184ce88d85889fe4c4203973da Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:10:03 +0100 Subject: [PATCH 05/17] Consistent #equals() implementation Also dropped #hashCode(), as it just calls the parent class implementation. --- src/api/java/AST.java | 21 +++++++-------------- src/api/java/FuncDecl.java | 31 ++++++++++--------------------- 2 files changed, 17 insertions(+), 35 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 7bc2a79fc..ebb9fc18e 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -28,24 +28,17 @@ public class AST extends Z3Object implements Comparable * Object comparison. * * @param o another AST - **/ + **/ @Override public boolean equals(Object o) { - AST casted = null; + if (o == null) return false; + if (o == this) return true; + if (o.getClass() != this.getClass()) return false; + AST casted = (AST) o; - try - { - casted = AST.class.cast(o); - } catch (ClassCastException e) - { - return false; - } - - return (this == casted) || - (this != null) && - (casted != null) && - (getContext().nCtx() == casted.getContext().nCtx()) && + return + (getContext().nCtx() == casted.getContext().nCtx()) && (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); } diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index ac72c4012..762cc42a2 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -32,28 +32,17 @@ public class FuncDecl extends AST @Override public boolean equals(Object o) { - FuncDecl casted = null; + if (o == null) return false; + if (o == this) return true; + if (o.getClass() != this.getClass()) return false; + FuncDecl other = (FuncDecl) o; - try { - casted = FuncDecl.class.cast(o); - } catch (ClassCastException e) { - return false; - } - - return - (this == casted) || - (this != null) && - (casted != null) && - (getContext().nCtx() == casted.getContext().nCtx()) && - (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); - } - - /** - * A hash code. - **/ - public int hashCode() - { - return super.hashCode(); + return + (getContext().nCtx() == other.getContext().nCtx()) && + (Native.isEqFuncDecl( + getContext().nCtx(), + getNativeObject(), + other.getNativeObject())); } /** From 27c684f743d34b33c0e0fffdcc7df0263cef62e3 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:11:01 +0100 Subject: [PATCH 06/17] AST#hashCode bugfix Previous implementation always returned zero. I can only assume that it wanted to cache it as well, but I haven't implemented that to keep the changes light. --- src/api/java/AST.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index ebb9fc18e..43002c714 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -72,12 +72,7 @@ public class AST extends Z3Object implements Comparable @Override public int hashCode() { - int r = 0; - try { - Native.getAstHash(getContext().nCtx(), getNativeObject()); - } - catch (Z3Exception ex) {} - return r; + return Native.getAstHash(getContext().nCtx(), getNativeObject()); } /** From ccd88a63a5decf3cd35e90401435a7547ea44382 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:12:33 +0100 Subject: [PATCH 07/17] No need to call "new String()" --- src/api/java/FuncInterp.java | 6 +++--- src/api/java/Statistics.java | 2 +- src/api/java/Symbol.java | 5 ++--- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index fb549b3f2..72f6bb25d 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -83,7 +83,7 @@ public class FuncInterp extends Z3Object return res + getValue() + "]"; } catch (Z3Exception e) { - return new String("Z3Exception: " + e.getMessage()); + return "Z3Exception: " + e.getMessage(); } } @@ -105,7 +105,7 @@ public class FuncInterp extends Z3Object getContext().getFuncEntryDRQ().add(o); super.decRef(o); } - }; + } /** * The number of entries in the function interpretation. @@ -186,7 +186,7 @@ public class FuncInterp extends Z3Object return res; } catch (Z3Exception e) { - return new String("Z3Exception: " + e.getMessage()); + return "Z3Exception: " + e.getMessage(); } } diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index de5a52ebb..051912468 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -90,7 +90,7 @@ public class Statistics extends Z3Object return Key + ": " + getValueString(); } catch (Z3Exception e) { - return new String("Z3Exception: " + e.getMessage()); + return "Z3Exception: " + e.getMessage(); } } diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index b90f8d915..60b60dbdf 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -72,11 +72,10 @@ public class Symbol extends Z3Object else if (isStringSymbol()) return ((StringSymbol) this).getString(); else - return new String( - "Z3Exception: Unknown symbol kind encountered."); + return "Z3Exception: Unknown symbol kind encountered."; } catch (Z3Exception ex) { - return new String("Z3Exception: " + ex.getMessage()); + return "Z3Exception: " + ex.getMessage(); } } From c435bc379b9f93045e8f20af5ee082104a461011 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:14:53 +0100 Subject: [PATCH 08/17] Added braces Lack of braces on multi-line statements is considered very scary in Java. --- src/api/java/AST.java | 18 ++++------ src/api/java/Context.java | 12 ++++--- src/api/java/Expr.java | 55 +++++++++++++++++-------------- src/api/java/FiniteDomainNum.java | 6 ++-- src/api/java/Global.java | 5 +-- src/api/java/Optimize.java | 11 ++++--- src/api/java/Solver.java | 21 +++++++----- src/api/java/Statistics.java | 24 ++++++++------ 8 files changed, 84 insertions(+), 68 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 43002c714..b57246356 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -53,15 +53,10 @@ public class AST extends Z3Object implements Comparable @Override public int compareTo(AST other) { - if (other == null) + if (other == null) { return 1; - - if (getId() < other.getId()) - return -1; - else if (getId() > other.getId()) - return +1; - else - return 0; + } + return Integer.compare(getId(), other.getId()); } /** @@ -94,11 +89,12 @@ public class AST extends Z3Object implements Comparable public AST translate(Context ctx) { - if (getContext() == ctx) + if (getContext() == ctx) { return this; - else + } else { return new AST(ctx, Native.translate(getContext().nCtx(), - getNativeObject(), ctx.nCtx())); + getNativeObject(), ctx.nCtx())); + } } /** diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 40b597be4..29f353f07 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -110,8 +110,9 @@ public class Context extends IDisposable **/ public BoolSort getBoolSort() { - if (m_boolSort == null) + if (m_boolSort == null) { m_boolSort = new BoolSort(this); + } return m_boolSort; } @@ -120,8 +121,9 @@ public class Context extends IDisposable **/ public IntSort getIntSort() { - if (m_intSort == null) + if (m_intSort == null) { m_intSort = new IntSort(this); + } return m_intSort; } @@ -130,8 +132,9 @@ public class Context extends IDisposable **/ public RealSort getRealSort() { - if (m_realSort == null) + if (m_realSort == null) { m_realSort = new RealSort(this); + } return m_realSort; } @@ -148,8 +151,9 @@ public class Context extends IDisposable **/ public SeqSort getStringSort() { - if (m_stringSort == null) + if (m_stringSort == null) { m_stringSort = mkStringSort(); + } return m_stringSort; } diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index b59a41e1d..065ee5f32 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -53,14 +53,16 @@ public class Expr extends AST public Expr simplify(Params p) { - if (p == null) + if (p == null) { return Expr.create(getContext(), - Native.simplify(getContext().nCtx(), getNativeObject())); - else + Native.simplify(getContext().nCtx(), getNativeObject())); + } + else { return Expr.create( - getContext(), - Native.simplifyEx(getContext().nCtx(), getNativeObject(), - p.getNativeObject())); + getContext(), + Native.simplifyEx(getContext().nCtx(), getNativeObject(), + p.getNativeObject())); + } } /** @@ -106,9 +108,10 @@ public class Expr extends AST { int n = getNumArgs(); Expr[] res = new Expr[n]; - for (int i = 0; i < n; i++) + for (int i = 0; i < n; i++) { res[i] = Expr.create(getContext(), - Native.getAppArg(getContext().nCtx(), getNativeObject(), i)); + Native.getAppArg(getContext().nCtx(), getNativeObject(), i)); + } return res; } @@ -122,10 +125,11 @@ public class Expr extends AST public void update(Expr[] args) { getContext().checkContextMatch(args); - if (isApp() && args.length != getNumArgs()) + if (isApp() && args.length != getNumArgs()) { throw new Z3Exception("Number of arguments does not match"); + } setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(), - (int) args.length, Expr.arrayToNative(args))); + args.length, Expr.arrayToNative(args))); } /** @@ -144,10 +148,11 @@ public class Expr extends AST { getContext().checkContextMatch(from); getContext().checkContextMatch(to); - if (from.length != to.length) + if (from.length != to.length) { throw new Z3Exception("Argument sizes do not match"); + } return Expr.create(getContext(), Native.substitute(getContext().nCtx(), - getNativeObject(), (int) from.length, Expr.arrayToNative(from), + getNativeObject(), from.length, Expr.arrayToNative(from), Expr.arrayToNative(to))); } @@ -160,7 +165,6 @@ public class Expr extends AST **/ public Expr substitute(Expr from, Expr to) { - return substitute(new Expr[] { from }, new Expr[] { to }); } @@ -179,7 +183,7 @@ public class Expr extends AST getContext().checkContextMatch(to); return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(), - getNativeObject(), (int) to.length, Expr.arrayToNative(to))); + getNativeObject(), to.length, Expr.arrayToNative(to))); } /** @@ -193,14 +197,14 @@ public class Expr extends AST **/ public Expr translate(Context ctx) { - - if (getContext() == ctx) + if (getContext() == ctx) { return this; - else + } else { return Expr.create( - ctx, - Native.translate(getContext().nCtx(), getNativeObject(), - ctx.nCtx())); + ctx, + Native.translate(getContext().nCtx(), getNativeObject(), + ctx.nCtx())); + } } /** @@ -2123,8 +2127,9 @@ public class Expr extends AST { if (!Native.isApp(getContext().nCtx(), obj) && Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() && - Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) + Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) { throw new Z3Exception("Underlying object is not a term"); + } super.checkNativeObject(obj); } @@ -2188,10 +2193,10 @@ public class Expr extends AST return new FPRMExpr(ctx, obj); case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj); - case Z3_SEQ_SORT: - return new SeqExpr(ctx, obj); - case Z3_RE_SORT: - return new ReExpr(ctx, obj); + case Z3_SEQ_SORT: + return new SeqExpr(ctx, obj); + case Z3_RE_SORT: + return new ReExpr(ctx, obj); default: ; } diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java index 73613e4e0..e53ed22b2 100644 --- a/src/api/java/FiniteDomainNum.java +++ b/src/api/java/FiniteDomainNum.java @@ -36,8 +36,9 @@ public class FiniteDomainNum extends FiniteDomainExpr public int getInt() { Native.IntPtr res = new Native.IntPtr(); - if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) { throw new Z3Exception("Numeral is not an int"); + } return res.value; } @@ -47,8 +48,9 @@ public class FiniteDomainNum extends FiniteDomainExpr public long getInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) { throw new Z3Exception("Numeral is not an int64"); + } return res.value; } diff --git a/src/api/java/Global.java b/src/api/java/Global.java index 67a051792..74106d8e9 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -57,10 +57,11 @@ public final class Global public static String getParameter(String id) { Native.StringPtr res = new Native.StringPtr(); - if (!Native.globalParamGet(id, res)) + if (!Native.globalParamGet(id, res)) { return null; - else + } else { return res.value; + } } /** diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 9d62873e2..76c0d1204 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -183,11 +183,12 @@ public class Optimize extends Z3Object **/ public Model getModel() { - long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject()); - if (x == 0) - return null; - else - return new Model(getContext(), x); + long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject()); + if (x == 0) { + return null; + } else { + return new Model(getContext(), x); + } } /** diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index e58b140a6..425ccbbc6 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -201,13 +201,14 @@ public class Solver extends Z3Object public Status check(Expr... assumptions) { Z3_lbool r; - if (assumptions == null) + if (assumptions == null) { r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(), - getNativeObject())); - else + getNativeObject())); + } else { r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext() - .nCtx(), getNativeObject(), (int) assumptions.length, AST - .arrayToNative(assumptions))); + .nCtx(), getNativeObject(), assumptions.length, AST + .arrayToNative(assumptions))); + } switch (r) { case Z3_L_TRUE: @@ -243,10 +244,11 @@ public class Solver extends Z3Object public Model getModel() { long x = Native.solverGetModel(getContext().nCtx(), getNativeObject()); - if (x == 0) + if (x == 0) { return null; - else + } else { return new Model(getContext(), x); + } } /** @@ -261,10 +263,11 @@ public class Solver extends Z3Object public Expr getProof() { long x = Native.solverGetProof(getContext().nCtx(), getNativeObject()); - if (x == 0) + if (x == 0) { return null; - else + } else { return Expr.create(getContext(), x); + } } /** diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 051912468..5af0cf863 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -72,12 +72,13 @@ public class Statistics extends Z3Object **/ public String getValueString() { - if (isUInt()) + if (isUInt()) { return Integer.toString(m_int); - else if (isDouble()) + } else if (isDouble()) { return Double.toString(m_double); - else + } else { throw new Z3Exception("Unknown statistical entry type"); + } } /** @@ -150,14 +151,15 @@ public class Statistics extends Z3Object { Entry e; String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i); - if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) + if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) { e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(), - getNativeObject(), i)); - else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) + getNativeObject(), i)); + } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) { e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(), - getNativeObject(), i)); - else + getNativeObject(), i)); + } else { throw new Z3Exception("Unknown data entry value"); + } res[i] = e; } return res; @@ -186,9 +188,11 @@ public class Statistics extends Z3Object { int n = size(); Entry[] es = getEntries(); - for (int i = 0; i < n; i++) - if (es[i].Key == key) + for (int i = 0; i < n; i++) { + if (es[i].Key.equals(key)) { return es[i]; + } + } return null; } From 52fdf73178ed6042758ed781009b932eb8eb2ee7 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:15:11 +0100 Subject: [PATCH 09/17] IDisposable is effectively an abstract class. --- src/api/java/IDisposable.java | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java index c3855c428..dae8a7262 100644 --- a/src/api/java/IDisposable.java +++ b/src/api/java/IDisposable.java @@ -19,9 +19,7 @@ Notes: package com.microsoft.z3; -public class IDisposable +public abstract class IDisposable { - public void dispose() - { - } + public abstract void dispose(); } From a816b4895ce3eca95784ee85fafaa6aabcda5d27 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:16:30 +0100 Subject: [PATCH 10/17] Logic simplifications There is no point in writing "boolean ? true : false" instead of "boolean" --- src/api/java/BitVecNum.java | 6 ++++-- src/api/java/Context.java | 9 +++------ src/api/java/Goal.java | 4 ++-- src/api/java/IntNum.java | 4 ++-- src/api/java/Model.java | 6 +++--- src/api/java/Params.java | 2 +- src/api/java/Quantifier.java | 12 ++++++------ 7 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index cd5e789b9..5a62f8087 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -32,8 +32,9 @@ public class BitVecNum extends BitVecExpr public int getInt() { Native.IntPtr res = new Native.IntPtr(); - if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) { throw new Z3Exception("Numeral is not an int"); + } return res.value; } @@ -45,8 +46,9 @@ public class BitVecNum extends BitVecExpr public long getLong() { Native.LongPtr res = new Native.LongPtr(); - if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) { throw new Z3Exception("Numeral is not a long"); + } return res.value; } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 29f353f07..f1baa92f2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1537,8 +1537,7 @@ public class Context extends IDisposable checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1 - .getNativeObject(), t2.getNativeObject(), (isSigned) ? true - : false)); + .getNativeObject(), t2.getNativeObject(), (isSigned))); } /** @@ -1580,8 +1579,7 @@ public class Context extends IDisposable checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1 - .getNativeObject(), t2.getNativeObject(), (isSigned) ? true - : false)); + .getNativeObject(), t2.getNativeObject(), (isSigned))); } /** @@ -1621,8 +1619,7 @@ public class Context extends IDisposable checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1 - .getNativeObject(), t2.getNativeObject(), (isSigned) ? true - : false)); + .getNativeObject(), t2.getNativeObject(), (isSigned))); } /** diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 41d4e27ac..46b04f6bf 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -246,8 +246,8 @@ public class Goal extends Z3Object Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) { - super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, - (unsatCores) ? true : false, (proofs) ? true : false)); + super(ctx, Native.mkGoal(ctx.nCtx(), (models), + (unsatCores), (proofs))); } void incRef(long o) diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index 4078b3db3..71d878311 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -36,7 +36,7 @@ public class IntNum extends IntExpr public int getInt() { Native.IntPtr res = new Native.IntPtr(); - if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Numeral is not an int"); return res.value; } @@ -47,7 +47,7 @@ public class IntNum extends IntExpr public long getInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Numeral is not an int64"); return res.value; } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 16613af68..795a08fe8 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -92,7 +92,7 @@ public class Model extends Z3Object return null; else { - if (Native.isAsArray(getContext().nCtx(), n) ^ true) + if (!Native.isAsArray(getContext().nCtx(), n)) throw new Z3Exception( "Argument was not an array constant"); long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); @@ -212,8 +212,8 @@ public class Model extends Z3Object public Expr eval(Expr t, boolean completion) { Native.LongPtr v = new Native.LongPtr(); - if (Native.modelEval(getContext().nCtx(), getNativeObject(), - t.getNativeObject(), (completion) ? true : false, v) ^ true) + if (!Native.modelEval(getContext().nCtx(), getNativeObject(), + t.getNativeObject(), (completion), v)) throw new ModelEvaluationFailedException(); else return Expr.create(getContext(), v.value); diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 8eef253b0..25d009b12 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -29,7 +29,7 @@ public class Params extends Z3Object public void add(Symbol name, boolean value) { Native.paramsSetBool(getContext().nCtx(), getNativeObject(), - name.getNativeObject(), (value) ? true : false); + name.getNativeObject(), (value)); } /** diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 08df1c1f5..1b425d3e4 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -163,15 +163,14 @@ public class Quantifier extends BoolExpr if (noPatterns == null && quantifierID == null && skolemID == null) { - setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true - : false, weight, AST.arrayLength(patterns), AST + setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST .arrayToNative(patterns), AST.arrayLength(sorts), AST .arrayToNative(sorts), Symbol.arrayToNative(names), body .getNativeObject())); } else { - setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), - (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), + setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), + (isForall), weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), @@ -195,13 +194,13 @@ public class Quantifier extends BoolExpr if (noPatterns == null && quantifierID == null && skolemID == null) { setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), - (isForall) ? true : false, weight, AST.arrayLength(bound), + isForall, weight, AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(patterns), body.getNativeObject())); } else { setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), - (isForall) ? true : false, weight, + isForall, weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), @@ -215,6 +214,7 @@ public class Quantifier extends BoolExpr super(ctx, obj); } + @Override void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST From d0d7a5b712e32abec1315849a0d9e4d9f0ec540e Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:16:45 +0100 Subject: [PATCH 11/17] Consistent Sort#equals --- src/api/java/Sort.java | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index f59569132..dd556d71e 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -33,20 +33,17 @@ public class Sort extends AST @Override 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 { - casted = Sort.class.cast(o); - } catch (ClassCastException e) { - return false; - } - - return - (this == casted) || - (this != null) && - (casted != null) && - (getContext().nCtx() == casted.getContext().nCtx()) && - (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); + return (getContext().nCtx() == other.getContext().nCtx()) && + (Native.isEqSort( + getContext().nCtx(), + getNativeObject(), + other.getNativeObject() + )); } /** From 93ad8d32b9ee392a07939a030adb9ef27f3acbd4 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:17:32 +0100 Subject: [PATCH 12/17] Remove redundant "throw" statement which has no effect. --- src/api/java/Constructor.java | 6 +----- src/api/java/ConstructorList.java | 6 +----- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 26b33ed35..a6c2856d4 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -87,11 +87,7 @@ public class Constructor extends Z3Object { try { Native.delConstructor(getContext().nCtx(), getNativeObject()); - } - catch (Throwable t) { - throw t; - } - finally { + } finally { super.finalize(); } } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 82b119513..a50ff11ea 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -31,11 +31,7 @@ public class ConstructorList extends Z3Object { try { Native.delConstructorList(getContext().nCtx(), getNativeObject()); - } - catch (Throwable t) { - throw t; - } - finally { + } finally { super.finalize(); } } From 54e5bf242230f6bfedd0cf5217e6322f3e6c2821 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:18:22 +0100 Subject: [PATCH 13/17] Remove redundant cast --- src/api/java/ConstructorList.java | 2 +- src/api/java/Context.java | 4 ++-- src/api/java/DatatypeSort.java | 2 +- src/api/java/EnumSort.java | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index a50ff11ea..fe3fae1ac 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -46,7 +46,7 @@ public class ConstructorList extends Z3Object super(ctx); setNativeObject(Native.mkConstructorList(getContext().nCtx(), - (int) constructors.length, + constructors.length, Constructor.arrayToNative(constructors))); } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index f1baa92f2..eb51af101 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -373,7 +373,7 @@ public class Context extends IDisposable { checkContextMatch(names); - int n = (int) names.length; + int n = names.length; ConstructorList[] cla = new ConstructorList[n]; long[] n_constr = new long[n]; for (int i = 0; i < n; i++) @@ -2384,7 +2384,7 @@ public class Context extends IDisposable { return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, - attributes, (int) assumptions.length, + attributes, assumptions.length, AST.arrayToNative(assumptions), formula.getNativeObject()); } diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index d7896b15f..644d434d3 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -101,7 +101,7 @@ public class DatatypeSort extends Sort { super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(), - (int) constructors.length, arrayToNative(constructors))); + constructors.length, arrayToNative(constructors))); } }; diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index da471f5ea..bb60eef56 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -98,7 +98,7 @@ public class EnumSort extends Sort long[] n_constdecls = new long[n]; long[] n_testers = new long[n]; setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), - name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames), + name.getNativeObject(), n, Symbol.arrayToNative(enumNames), n_constdecls, n_testers)); } }; From 8bb0010dc320c69f346b03c114d48a33ce9ab4ef Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:19:26 +0100 Subject: [PATCH 14/17] Javadoc and indentation fixes - A proper way to refer to the function in the same class is "#funcName" - There is no point in "@param p" declaration if no description follows it. --- src/api/java/Context.java | 73 ++++++++++++++++-------------------- src/api/java/Expr.java | 8 +--- src/api/java/Fixedpoint.java | 4 +- src/api/java/FuncDecl.java | 8 +--- src/api/java/Global.java | 4 +- src/api/java/Model.java | 4 +- src/api/java/Optimize.java | 50 ++++++++++++------------ src/api/java/Solver.java | 40 ++++++++++---------- src/api/java/Sort.java | 10 ++--- 9 files changed, 91 insertions(+), 110 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index eb51af101..9fa17fcd4 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -326,13 +326,6 @@ public class Context extends IDisposable /** * Create a datatype constructor. - * @param name - * @param recognizer - * @param fieldNames - * @param sorts - * @param sortRefs - * - * @return **/ public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) @@ -395,10 +388,6 @@ public class Context extends IDisposable /** * Create mutually recursive data-types. - * @param names - * @param c - * - * @return **/ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) @@ -410,7 +399,7 @@ public class Context extends IDisposable * Update a datatype field at expression t with value v. * The function performs a record update at t. The field * that is passed in as argument is updated with value v, - * the remainig fields of t are unchanged. + * the remaining fields of t are unchanged. **/ public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) throws Z3Exception @@ -506,8 +495,8 @@ public class Context extends IDisposable /** * Creates a fresh constant function declaration with a name prefixed with * {@code prefix"}. - * @see mkFuncDecl(String,Sort,Sort) - * @see mkFuncDecl(String,Sort[],Sort) + * @see #mkFuncDecl(String,Sort,Sort) + * @see #mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshConstDecl(String prefix, Sort range) @@ -1523,7 +1512,7 @@ public class Context extends IDisposable { checkContextMatch(t); return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(), - (signed) ? true : false)); + (signed))); } /** @@ -1663,8 +1652,8 @@ public class Context extends IDisposable * {@code [domain -> range]}, and {@code i} must have the sort * {@code domain}. The sort of the result is {@code range}. * - * @see mkArraySort - * @see mkStore + * @see #mkArraySort + * @see #mkStore **/ public Expr mkSelect(ArrayExpr a, Expr i) @@ -1689,8 +1678,8 @@ public class Context extends IDisposable * {@code select}) on all indices except for {@code i}, where it * maps to {@code v} (and the {@code select} of {@code a} * with respect to {@code i} may be a different value). - * @see mkArraySort - * @see mkSelect + * @see #mkArraySort + * @see #mkSelect **/ public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) @@ -1707,8 +1696,8 @@ public class Context extends IDisposable * Remarks: The resulting term is an array, such * that a {@code select} on an arbitrary index produces the value * {@code v}. - * @see mkArraySort - * @see mkSelect + * @see #mkArraySort + * @see #mkSelect * **/ public ArrayExpr mkConstArray(Sort domain, Expr v) @@ -1721,15 +1710,15 @@ public class Context extends IDisposable /** * Maps f on the argument arrays. - * Remarks: Eeach element of + * Remarks: Each element of * {@code args} must be of an array sort * {@code [domain_i -> range_i]}. The function declaration * {@code f} must have type {@code range_1 .. range_n -> range}. * {@code v} must have sort range. The sort of the result is * {@code [domain_i -> range]}. - * @see mkArraySort - * @see mkSelect - * @see mkStore + * @see #mkArraySort + * @see #mkSelect + * @see #mkStore **/ public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) @@ -2122,12 +2111,13 @@ public class Context extends IDisposable * * @return A Term with value {@code num}/{@code den} * and sort Real - * @see mkNumeral(String,Sort) + * @see #mkNumeral(String,Sort) **/ public RatNum mkReal(int num, int den) { - if (den == 0) + if (den == 0) { throw new Z3Exception("Denominator is zero"); + } return new RatNum(this, Native.mkReal(nCtx(), num, den)); } @@ -2257,7 +2247,7 @@ public class Context extends IDisposable * 'names' of the bound variables, and {@code body} is the body * of the quantifier. Quantifiers are associated with weights indicating the * importance of using the quantifier during instantiation. - * Note that the bound variables are de-Bruijn indices created using {@link mkBound}. + * Note that the bound variables are de-Bruijn indices created using {@link #mkBound}. * Z3 applies the convention that the last element in {@code names} and * {@code sorts} refers to the variable with index 0, the second to last element * of {@code names} and {@code sorts} refers to the variable @@ -2287,7 +2277,7 @@ public class Context extends IDisposable /** * Creates an existential quantifier using de-Brujin indexed variables. - * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) + * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, @@ -2414,7 +2404,7 @@ public class Context extends IDisposable /** * Parse the given file using the SMT-LIB parser. - * @see parseSMTLIBString + * @see #parseSMTLIBString **/ public void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) @@ -2528,7 +2518,7 @@ public class Context extends IDisposable /** * Parse the given string using the SMT-LIB2 parser. - * @see parseSMTLIBString + * @see #parseSMTLIBString * * @return A conjunction of assertions in the scope (up to push/pop) at the * end of the string. @@ -2542,8 +2532,9 @@ public class Context extends IDisposable int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); - if (csn != cs || cdn != cd) + if (csn != cs || cdn != cd) { throw new Z3Exception("Argument size mismatch"); + } return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(), str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), @@ -2552,13 +2543,12 @@ public class Context extends IDisposable /** * Parse the given file using the SMT-LIB2 parser. - * @see parseSMTLIB2String + * @see #parseSMTLIB2String **/ public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); @@ -2649,9 +2639,10 @@ public class Context extends IDisposable if (ts != null && ts.length > 0) { last = ts[ts.length - 1].getNativeObject(); - for (int i = ts.length - 2; i >= 0; i--) + for (int i = ts.length - 2; i >= 0; i--) { last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(), - last); + last); + } } if (last != 0) { @@ -2665,7 +2656,7 @@ public class Context extends IDisposable /** * Create a tactic that applies {@code t1} to a Goal and then - * {@code t2"/> to every subgoal produced by with assumptions for + * This API is an alternative to {@link #check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@code assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link #check} with assumptions. **/ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { getContext().checkContextMatch(constraints); getContext().checkContextMatch(ps); - if (constraints.length != ps.length) + if (constraints.length != ps.length) { throw new Z3Exception("Argument size mismatch"); + } - for (int i = 0; i < constraints.length; i++) + for (int i = 0; i < constraints.length; i++) { Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(), - constraints[i].getNativeObject(), ps[i].getNativeObject()); + constraints[i].getNativeObject(), ps[i].getNativeObject()); + } } /** @@ -152,13 +154,13 @@ public class Solver extends Z3Object * using the Boolean constant p. * * Remarks: - * This API is an alternative to with assumptions for + * This API is an alternative to {@link #check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@link #assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link #check} with assumptions. */ public void assertAndTrack(BoolExpr constraint, BoolExpr p) { @@ -194,9 +196,9 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. * Remarks: - * @see getModel - * @see getUnsatCore - * @see getProof + * @see #getModel + * @see #getUnsatCore + * @see #getProof **/ public Status check(Expr... assumptions) { @@ -223,9 +225,9 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. * Remarks: - * @see getModel - * @see getUnsatCore - * @see getProof + * @see #getModel + * @see #getUnsatCore + * @see #getProof **/ public Status check() { diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index dd556d71e..c92432ad3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -27,8 +27,6 @@ public class Sort extends AST { /** * Equality operator for objects of type Sort. - * @param o - * @return **/ @Override public boolean equals(Object o) @@ -139,10 +137,10 @@ public class Sort extends AST return new FPSort(ctx, obj); case Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj); - case Z3_SEQ_SORT: - return new SeqSort(ctx, obj); - case Z3_RE_SORT: - return new ReSort(ctx, obj); + case Z3_SEQ_SORT: + return new SeqSort(ctx, obj); + case Z3_RE_SORT: + return new ReSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } From 529b9d6833dc753a07002e8b24fb6205dbcabf7f Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:19:38 +0100 Subject: [PATCH 15/17] The locking field should be final. --- src/api/java/IDecRefQueue.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index 823288a20..1a99a3d92 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -21,7 +21,7 @@ import java.util.LinkedList; public abstract class IDecRefQueue { - protected Object m_lock = new Object(); + protected final Object m_lock = new Object(); protected LinkedList m_queue = new LinkedList(); protected int m_move_limit; From f93c41b1be6232d1c524a9e8a9ef234664aa32c8 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:27:58 +0100 Subject: [PATCH 16/17] Since classes are non-final "instanceof" check is better in #equals --- src/api/java/AST.java | 3 +-- src/api/java/FuncDecl.java | 3 +-- src/api/java/Sort.java | 3 +-- src/api/java/Symbol.java | 3 +-- 4 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index b57246356..e84dc8c81 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -32,9 +32,8 @@ public class AST extends Z3Object implements Comparable @Override public boolean equals(Object o) { - if (o == null) return false; if (o == this) return true; - if (o.getClass() != this.getClass()) return false; + if (!(o instanceof AST)) return false; AST casted = (AST) o; return diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 878ce84cc..301978c44 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -32,9 +32,8 @@ public class FuncDecl extends AST @Override public boolean equals(Object o) { - if (o == null) return false; if (o == this) return true; - if (o.getClass() != this.getClass()) return false; + if (!(o instanceof FuncDecl)) return false; FuncDecl other = (FuncDecl) o; return diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index c92432ad3..e30e0b8b3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -31,9 +31,8 @@ public class Sort extends AST @Override public boolean equals(Object o) { - if (o == null) return false; if (o == this) return true; - if (o.getClass() != this.getClass()) return false; + if (!(o instanceof Sort)) return false; Sort other = (Sort) o; return (getContext().nCtx() == other.getContext().nCtx()) && diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 60b60dbdf..beeaebb69 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -52,9 +52,8 @@ public class Symbol extends Z3Object @Override public boolean equals(Object o) { - if (o == null) return false; if (o == this) return true; - if (o.getClass() != this.getClass()) return false; + if (!(o instanceof Symbol)) return false; Symbol other = (Symbol) o; return this.getNativeObject() == other.getNativeObject(); } From fa598edf4351c549628a9c0650fca3042ce8dc2c Mon Sep 17 00:00:00 2001 From: Michael Sullivan Date: Wed, 10 Feb 2016 20:27:28 +0000 Subject: [PATCH 17/17] Fix gcc build failure on ARM caused by including src/util/hwf.cpp tries to use to directly use SSE intrinsics. Make sure to only use those when actually on x86 or x86_64. --- src/util/hwf.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 3963836f2..74a03b620 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -29,7 +29,8 @@ Revision History: #include #endif -#ifndef _M_IA64 +#if defined(__x86_64__) || defined(_M_X64) || \ + defined(__i386) || defined(_M_IX86) #define USE_INTRINSICS #endif @@ -47,7 +48,9 @@ Revision History: // Luckily, these are kind of standardized, at least for Windows/Linux/OSX. #ifdef __clang__ #undef USE_INTRINSICS -#else +#endif + +#ifdef USE_INTRINSICS #include #endif