From dfc80d3b697125a2d4b3694786ef9507245c52a6 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 14:14:11 +0200 Subject: [PATCH] Do not needlessly catch exceptions in Java bindings A lot of existing code in Java bindings catches exceptions just to silence them later. This is: a) Unnecessary: it is OK for a function to throw a RuntimeException without declaring it. b) Highly unidiomatic and not recommended by Java experts (see Effective Java and others) c) Confusing as has the potential to hide the existing bugs and have them resurface at the most inconvenient/unexpected moment. --- src/api/java/AST.java | 11 ++--------- src/api/java/ASTMap.java | 8 +------- src/api/java/ASTVector.java | 11 ++--------- src/api/java/ApplyResult.java | 11 ++--------- src/api/java/BitVecNum.java | 8 +------- src/api/java/FPNum.java | 8 +------- src/api/java/FiniteDomainNum.java | 8 +------- src/api/java/Fixedpoint.java | 8 +------- src/api/java/FuncDecl.java | 8 +------- src/api/java/Goal.java | 11 ++--------- src/api/java/IntNum.java | 11 ++--------- src/api/java/Model.java | 11 ++--------- src/api/java/ParamDescrs.java | 11 ++--------- src/api/java/Params.java | 8 +------- src/api/java/Pattern.java | 8 +------- src/api/java/RatNum.java | 11 ++--------- src/api/java/Solver.java | 10 ++-------- src/api/java/Sort.java | 12 +++--------- src/api/java/Statistics.java | 21 +++++---------------- 19 files changed, 34 insertions(+), 161 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index e84dc8c81..f43aa85d2 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -175,15 +175,8 @@ public class AST extends Z3Object implements Comparable * A string representation of the AST. **/ @Override - public String toString() - { - try - { - return Native.astToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.astToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index 7bc485bf5..a6201d8a0 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -104,13 +104,7 @@ class ASTMap extends Z3Object @Override public String toString() { - try - { - return Native.astMapToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.astMapToString(getContext().nCtx(), getNativeObject()); } ASTMap(Context ctx, long obj) diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index ab99e2aee..da1ab0f12 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -88,15 +88,8 @@ public class ASTVector extends Z3Object * Retrieves a string representation of the vector. **/ @Override - public String toString() - { - try - { - return Native.astVectorToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.astVectorToString(getContext().nCtx(), getNativeObject()); } ASTVector(Context ctx, long obj) diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 84c63e966..f598c9504 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -64,15 +64,8 @@ public class ApplyResult extends Z3Object * A string representation of the ApplyResult. **/ @Override - public String toString() - { - try - { - return Native.applyResultToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.applyResultToString(getContext().nCtx(), getNativeObject()); } ApplyResult(Context ctx, long obj) diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 5a62f8087..d6c176855 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -66,13 +66,7 @@ public class BitVecNum extends BitVecExpr @Override public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } BitVecNum(Context ctx, long obj) diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 69a44c559..9aeb41759 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -87,13 +87,7 @@ public class FPNum extends FPExpr */ public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java index e53ed22b2..68467e408 100644 --- a/src/api/java/FiniteDomainNum.java +++ b/src/api/java/FiniteDomainNum.java @@ -68,12 +68,6 @@ public class FiniteDomainNum extends FiniteDomainExpr @Override public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 14fb3a44a..2ff10a1f3 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -255,14 +255,8 @@ public class Fixedpoint extends Z3Object @Override public String toString() { - try - { - return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), + return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), 0, null); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } } /** diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 301978c44..273e853c0 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -47,13 +47,7 @@ public class FuncDecl extends AST @Override public String toString() { - try - { - return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 46b04f6bf..e60971179 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -211,15 +211,8 @@ public class Goal extends Z3Object * * @return A string representation of the Goal. **/ - public String toString() - { - try - { - return Native.goalToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.goalToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index 71d878311..d3a5b456f 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -63,14 +63,7 @@ public class IntNum extends IntExpr /** * Returns a string representation of the numeral. **/ - public String toString() - { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 0695d7cf1..1bf77d246 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -283,15 +283,8 @@ public class Model extends Z3Object * @return A string representation of the model. **/ @Override - public String toString() - { - try - { - return Native.modelToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.modelToString(getContext().nCtx(), getNativeObject()); } Model(Context ctx, long obj) diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 8f8c6df0b..f265fb19e 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -82,15 +82,8 @@ public class ParamDescrs extends Z3Object * Retrieves a string representation of the ParamDescrs. **/ @Override - public String toString() - { - try - { - return Native.paramDescrsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.paramDescrsToString(getContext().nCtx(), getNativeObject()); } ParamDescrs(Context ctx, long obj) diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 25d009b12..4be36c23d 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -115,13 +115,7 @@ public class Params extends Z3Object @Override public String toString() { - try - { - return Native.paramsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.paramsToString(getContext().nCtx(), getNativeObject()); } Params(Context ctx) diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index eb12b6448..852ffcd0f 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -53,13 +53,7 @@ public class Pattern extends AST @Override public String toString() { - try - { - return Native.patternToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.patternToString(getContext().nCtx(), getNativeObject()); } Pattern(Context ctx, long obj) diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index f44823a2b..2bf1b28dd 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -75,15 +75,8 @@ public class RatNum extends RealExpr * Returns a string representation of the numeral. **/ @Override - public String toString() - { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } RatNum(Context ctx, long obj) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index ea76637c8..431811b8d 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -323,14 +323,8 @@ public class Solver extends Z3Object @Override public String toString() { - try - { - return Native - .solverToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native + .solverToString(getContext().nCtx(), getNativeObject()); } Solver(Context ctx, long obj) diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index e30e0b8b3..30a43e7dd 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -82,15 +82,9 @@ public class Sort extends AST /** * A string representation of the sort. **/ - public String toString() - { - try - { - return Native.sortToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + @Override + public String toString() { + return Native.sortToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 5af0cf863..1e842a892 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -84,15 +84,9 @@ public class Statistics extends Z3Object /** * The string representation of the Entry. **/ - public String toString() - { - try - { - return Key + ": " + getValueString(); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + @Override + public String toString() { + return Key + ": " + getValueString(); } private boolean m_is_int = false; @@ -118,15 +112,10 @@ public class Statistics extends Z3Object /** * A string representation of the statistical data. **/ + @Override public String toString() { - try - { - return Native.statsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.statsToString(getContext().nCtx(), getNativeObject()); } /**