Turned Z3Exception into a RuntimeException such that throws declarati…

…ons are not needed anymore. Thanks to codeplex user steimann for this suggestion.
Z3Prover · Apr 8, 2015 · b7bb534 · b7bb534
1 parent 2f4c923
commit b7bb534
Show file tree

Hide file tree

Showing 62 changed files with 834 additions and 834 deletions.
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
@@ -54,7 +54,7 @@ public boolean equals(Object o)
      * positive if after else zero.
      * @throws Z3Exception on error
      **/
-    public int compareTo(Object other) throws Z3Exception
+    public int compareTo(Object other)
     {
         if (other == null)
             return 1;
@@ -95,7 +95,7 @@ public int hashCode()
      * A unique identifier for the AST (unique among all ASTs).
      * @throws Z3Exception on error
      **/
-    public int getId() throws Z3Exception
+    public int getId()
     {
         return Native.getAstId(getContext().nCtx(), getNativeObject());
     }
@@ -107,7 +107,7 @@ public int getId() throws Z3Exception
      * @return A copy of the AST which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
-    public AST translate(Context ctx) throws Z3Exception
+    public AST translate(Context ctx)
     {
 
         if (getContext() == ctx)
@@ -121,7 +121,7 @@ public AST translate(Context ctx) throws Z3Exception
      * The kind of the AST.
      * @throws Z3Exception on error
      **/
-    public Z3_ast_kind getASTKind() throws Z3Exception
+    public Z3_ast_kind getASTKind()
     {
         return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
                 getNativeObject()));
@@ -132,7 +132,7 @@ public Z3_ast_kind getASTKind() throws Z3Exception
      * @throws Z3Exception on error
      * @throws Z3Exception on error
      **/
-    public boolean isExpr() throws Z3Exception
+    public boolean isExpr()
     {
         switch (getASTKind())
         {
@@ -151,7 +151,7 @@ public boolean isExpr() throws Z3Exception
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isApp() throws Z3Exception
+    public boolean isApp()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
     }
@@ -161,7 +161,7 @@ public boolean isApp() throws Z3Exception
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isVar() throws Z3Exception
+    public boolean isVar()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
     }
@@ -171,23 +171,23 @@ public boolean isVar() throws Z3Exception
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isQuantifier() throws Z3Exception
+    public boolean isQuantifier()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
     }
 
     /**
      * Indicates whether the AST is a Sort
      **/
-    public boolean isSort() throws Z3Exception
+    public boolean isSort()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
     }
 
     /**
      * Indicates whether the AST is a FunctionDeclaration
      **/
-    public boolean isFuncDecl() throws Z3Exception
+    public boolean isFuncDecl()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
     }
@@ -209,7 +209,7 @@ public String toString()
     /**
      * A string representation of the AST in s-expression notation.
      **/
-    public String getSExpr() throws Z3Exception
+    public String getSExpr()
     {
         return Native.astToString(getContext().nCtx(), getNativeObject());
     }
@@ -219,12 +219,12 @@ public String getSExpr() throws Z3Exception
         super(ctx);
     }
 
-    AST(Context ctx, long obj) throws Z3Exception
+    AST(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         // Console.WriteLine("AST IncRef()");
         if (getContext() == null || o == 0)
@@ -233,7 +233,7 @@ void incRef(long o) throws Z3Exception
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         // Console.WriteLine("AST DecRef()");
         if (getContext() == null || o == 0)
@@ -242,7 +242,7 @@ void decRef(long o) throws Z3Exception
         super.decRef(o);
     }
 
-    static AST create(Context ctx, long obj) throws Z3Exception
+    static AST create(Context ctx, long obj)
     {
         switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
         {

diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
@@ -29,7 +29,7 @@ class ASTMap extends Z3Object
      * @return True if {@code k} is a key in the map, false
      *         otherwise.
      **/
-    public boolean contains(AST k) throws Z3Exception
+    public boolean contains(AST k)
     {
 
         return Native.astMapContains(getContext().nCtx(), getNativeObject(),
@@ -44,7 +44,7 @@ public boolean contains(AST k) throws Z3Exception
      * 
      * @throws Z3Exception
      **/
-    public AST find(AST k) throws Z3Exception
+    public AST find(AST k)
     {
         return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
                 getNativeObject(), k.getNativeObject()));
@@ -55,7 +55,7 @@ public AST find(AST k) throws Z3Exception
      * @param k The key AST
      * @param v The value AST
      **/
-    public void insert(AST k, AST v) throws Z3Exception
+    public void insert(AST k, AST v)
     {
 
         Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
@@ -66,23 +66,23 @@ public void insert(AST k, AST v) throws Z3Exception
      * Erases the key {@code k} from the map. 
      * @param k An AST
      **/
-    public void erase(AST k) throws Z3Exception
+    public void erase(AST k)
     {
         Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
     }
 
     /**
      * Removes all keys from the map.
      **/
-    public void reset() throws Z3Exception
+    public void reset()
     {
         Native.astMapReset(getContext().nCtx(), getNativeObject());
     }
 
     /**
      * The size of the map
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.astMapSize(getContext().nCtx(), getNativeObject());
     }
@@ -92,7 +92,7 @@ public int size() throws Z3Exception
      * 
      * @throws Z3Exception
      **/
-    public ASTVector getKeys() throws Z3Exception
+    public ASTVector getKeys()
     {
         return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
                 getNativeObject()));
@@ -112,23 +112,23 @@ public String toString()
         }
     }
 
-    ASTMap(Context ctx, long obj) throws Z3Exception
+    ASTMap(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ASTMap(Context ctx) throws Z3Exception
+    ASTMap(Context ctx)
     {
         super(ctx, Native.mkAstMap(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getASTMapDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getASTMapDRQ().add(o);
         super.decRef(o);

diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
@@ -25,7 +25,7 @@ public class ASTVector extends Z3Object
     /**
      * The size of the vector
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.astVectorSize(getContext().nCtx(), getNativeObject());
     }
@@ -39,13 +39,13 @@ public int size() throws Z3Exception
      * @return An AST
      * @throws Z3Exception
      **/
-    public AST get(int i) throws Z3Exception
+    public AST get(int i)
     {
         return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
                 getNativeObject(), i));
     }
 
-    public void set(int i, AST value) throws Z3Exception
+    public void set(int i, AST value)
     {
 
         Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
@@ -56,7 +56,7 @@ public void set(int i, AST value) throws Z3Exception
      * Resize the vector to {@code newSize}. 
      * @param newSize The new size of the vector.
      **/
-    public void resize(int newSize) throws Z3Exception
+    public void resize(int newSize)
     {
         Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
     }
@@ -66,7 +66,7 @@ public void resize(int newSize) throws Z3Exception
      * increased by 1. 
      * @param a An AST
      **/
-    public void push(AST a) throws Z3Exception
+    public void push(AST a)
     {
         Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
     }
@@ -78,7 +78,7 @@ public void push(AST a) throws Z3Exception
      * @return A new ASTVector
      * @throws Z3Exception
      **/
-    public ASTVector translate(Context ctx) throws Z3Exception
+    public ASTVector translate(Context ctx)
     {
         return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
                 .nCtx(), getNativeObject(), ctx.nCtx()));
@@ -98,23 +98,23 @@ public String toString()
         }
     }
 
-    ASTVector(Context ctx, long obj) throws Z3Exception
+    ASTVector(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ASTVector(Context ctx) throws Z3Exception
+    ASTVector(Context ctx)
     {
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getASTVectorDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);

diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java
@@ -32,7 +32,7 @@ public class AlgebraicNum extends ArithExpr
 	 * @return A numeral Expr of sort Real
 	 * @throws Z3Exception on error
 	 **/
-	public RatNum toUpper(int precision) throws Z3Exception
+	public RatNum toUpper(int precision)
 	{
 
 		return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
@@ -49,7 +49,7 @@ public RatNum toUpper(int precision) throws Z3Exception
 	 * @return A numeral Expr of sort Real
 	 * @throws Z3Exception on error
 	 **/
-	public RatNum toLower(int precision) throws Z3Exception
+	public RatNum toLower(int precision)
 	{
 
 		return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
@@ -63,14 +63,14 @@ public RatNum toLower(int precision) throws Z3Exception
 	 * @return String
 	 * @throws Z3Exception on error
 	 **/
-	public String toDecimal(int precision) throws Z3Exception
+	public String toDecimal(int precision)
 	{
 
 		return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
 				precision);
 	}
 
-	AlgebraicNum(Context ctx, long obj) throws Z3Exception
+	AlgebraicNum(Context ctx, long obj)
 	{
 		super(ctx, obj);
 

diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
@@ -26,7 +26,7 @@ public class ApplyResult extends Z3Object
     /**
      * The number of Subgoals.
      **/
-    public int getNumSubgoals() throws Z3Exception
+    public int getNumSubgoals()
     {
         return Native.applyResultGetNumSubgoals(getContext().nCtx(),
                 getNativeObject());
@@ -37,7 +37,7 @@ public int getNumSubgoals() throws Z3Exception
      * 
      * @throws Z3Exception
      **/
-    public Goal[] getSubgoals() throws Z3Exception
+    public Goal[] getSubgoals()
     {
         int n = getNumSubgoals();
         Goal[] res = new Goal[n];
@@ -54,7 +54,7 @@ public Goal[] getSubgoals() throws Z3Exception
      * @return A model for {@code g}
      * @throws Z3Exception
      **/
-    public Model convertModel(int i, Model m) throws Z3Exception
+    public Model convertModel(int i, Model m)
     {
         return new Model(getContext(), 
             Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
@@ -74,18 +74,18 @@ public String toString()
         }
     }
 
-    ApplyResult(Context ctx, long obj) throws Z3Exception
+    ApplyResult(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getApplyResultDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getApplyResultDRQ().add(o);
         super.decRef(o);

diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java
@@ -25,7 +25,7 @@ public class ArithExpr extends Expr
     /**
      * Constructor for ArithExpr
      **/
-    ArithExpr(Context ctx, long obj) throws Z3Exception
+    ArithExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }