From b7bb53406f7807daddf025d7849b2cf7b49c1fb4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Apr 2015 13:16:32 +0100 Subject: [PATCH] Turned Z3Exception into a RuntimeException such that throws declarations are not needed anymore. Thanks to codeplex user steimann for this suggestion. --- src/api/java/AST.java | 30 +- src/api/java/ASTMap.java | 22 +- src/api/java/ASTVector.java | 20 +- src/api/java/AlgebraicNum.java | 8 +- src/api/java/ApplyResult.java | 12 +- src/api/java/ArithExpr.java | 2 +- src/api/java/ArithSort.java | 2 +- src/api/java/ArrayExpr.java | 2 +- src/api/java/ArraySort.java | 8 +- src/api/java/BitVecExpr.java | 4 +- src/api/java/BitVecNum.java | 6 +- src/api/java/BitVecSort.java | 4 +- src/api/java/BoolExpr.java | 2 +- src/api/java/BoolSort.java | 4 +- src/api/java/Constructor.java | 12 +- src/api/java/ConstructorList.java | 6 +- src/api/java/Context.java | 584 ++++++++++++------------- src/api/java/DatatypeExpr.java | 2 +- src/api/java/DatatypeSort.java | 12 +- src/api/java/EnumSort.java | 14 +- src/api/java/Expr.java | 348 +++++++-------- src/api/java/FPExpr.java | 6 +- src/api/java/FPNum.java | 10 +- src/api/java/FPRMExpr.java | 2 +- src/api/java/FPRMNum.java | 22 +- src/api/java/FPRMSort.java | 4 +- src/api/java/FPSort.java | 8 +- src/api/java/FiniteDomainSort.java | 6 +- src/api/java/Fixedpoint.java | 50 +-- src/api/java/FuncDecl.java | 44 +- src/api/java/FuncInterp.java | 26 +- src/api/java/Global.java | 2 +- src/api/java/Goal.java | 42 +- src/api/java/IDisposable.java | 2 +- src/api/java/IntExpr.java | 2 +- src/api/java/IntNum.java | 8 +- src/api/java/IntSort.java | 4 +- src/api/java/IntSymbol.java | 8 +- src/api/java/InterpolationContext.java | 18 +- src/api/java/ListSort.java | 16 +- src/api/java/Log.java | 2 +- src/api/java/Model.java | 32 +- src/api/java/ParamDescrs.java | 14 +- src/api/java/Params.java | 24 +- src/api/java/Pattern.java | 6 +- src/api/java/Probe.java | 10 +- src/api/java/Quantifier.java | 30 +- src/api/java/RatNum.java | 12 +- src/api/java/RealExpr.java | 2 +- src/api/java/RealSort.java | 4 +- src/api/java/RelationSort.java | 6 +- src/api/java/SetSort.java | 4 +- src/api/java/Solver.java | 46 +- src/api/java/Sort.java | 12 +- src/api/java/Statistics.java | 16 +- src/api/java/StringSymbol.java | 8 +- src/api/java/Symbol.java | 10 +- src/api/java/Tactic.java | 18 +- src/api/java/TupleSort.java | 8 +- src/api/java/UninterpretedSort.java | 4 +- src/api/java/Z3Exception.java | 2 +- src/api/java/Z3Object.java | 14 +- 62 files changed, 834 insertions(+), 834 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 870f1d5d30f..436a9fdcb94 100644 --- 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,7 +171,7 @@ 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; } @@ -179,7 +179,7 @@ public boolean isQuantifier() throws Z3Exception /** * Indicates whether the AST is a Sort **/ - public boolean isSort() throws Z3Exception + public boolean isSort() { return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST; } @@ -187,7 +187,7 @@ public boolean isSort() throws Z3Exception /** * 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 index a37e9d0ff5a..398aac77f41 100644 --- 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,7 +66,7 @@ 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()); } @@ -74,7 +74,7 @@ public void erase(AST k) throws Z3Exception /** * Removes all keys from the map. **/ - public void reset() throws Z3Exception + public void reset() { Native.astMapReset(getContext().nCtx(), getNativeObject()); } @@ -82,7 +82,7 @@ public void reset() throws Z3Exception /** * 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 index 03e1b0a98b9..9c650449367 100644 --- 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 index 322b24d3913..6725d393772 100644 --- 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 index 8e998111fe6..2812efd705f 100644 --- 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 index 24051813453..d92d8523bb3 100644 --- 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); } diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java index 848d23554b7..5f4d4c1eba4 100644 --- a/src/api/java/ArithSort.java +++ b/src/api/java/ArithSort.java @@ -22,7 +22,7 @@ **/ public class ArithSort extends Sort { - ArithSort(Context ctx, long obj) throws Z3Exception + ArithSort(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index 4e6d9ed4d86..b8318b648a7 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -26,7 +26,7 @@ public class ArrayExpr extends Expr /** * Constructor for ArrayExpr **/ - ArrayExpr(Context ctx, long obj) throws Z3Exception + ArrayExpr(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index a5b52a8f582..1574823d1a4 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -28,7 +28,7 @@ public class ArraySort extends Sort * @throws Z3Exception on error * @return a sort **/ - public Sort getDomain() throws Z3Exception + public Sort getDomain() { return Sort.create(getContext(), Native.getArraySortDomain(getContext().nCtx(), getNativeObject())); @@ -40,18 +40,18 @@ public Sort getDomain() throws Z3Exception * @throws Z3Exception on error * @return a sort **/ - public Sort getRange() throws Z3Exception + public Sort getRange() { return Sort.create(getContext(), Native.getArraySortRange(getContext().nCtx(), getNativeObject())); } - ArraySort(Context ctx, long obj) throws Z3Exception + ArraySort(Context ctx, long obj) { super(ctx, obj); } - ArraySort(Context ctx, Sort domain, Sort range) throws Z3Exception + ArraySort(Context ctx, Sort domain, Sort range) { super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(), range.getNativeObject())); diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index 926a26b252e..175da9d6692 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -29,7 +29,7 @@ public class BitVecExpr extends Expr * @throws Z3Exception on error * @return an int **/ - public int getSortSize() throws Z3Exception + public int getSortSize() { return ((BitVecSort) getSort()).getSize(); } @@ -37,7 +37,7 @@ public int getSortSize() throws Z3Exception /** * Constructor for BitVecExpr **/ - BitVecExpr(Context ctx, long obj) throws Z3Exception + BitVecExpr(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 69ac5dadc51..08da40256d7 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -29,7 +29,7 @@ public class BitVecNum extends BitVecExpr * * @throws Z3Exception **/ - public int getInt() throws Z3Exception + public int getInt() { Native.IntPtr res = new Native.IntPtr(); if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) @@ -42,7 +42,7 @@ public int getInt() throws Z3Exception * * @throws Z3Exception **/ - public long getLong() throws Z3Exception + public long getLong() { Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) @@ -72,7 +72,7 @@ public String toString() } } - BitVecNum(Context ctx, long obj) throws Z3Exception + BitVecNum(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java index 7fd644acb7f..5c8e9a1e5f0 100644 --- a/src/api/java/BitVecSort.java +++ b/src/api/java/BitVecSort.java @@ -27,12 +27,12 @@ public class BitVecSort extends Sort * @throws Z3Exception on error * @return an int **/ - public int getSize() throws Z3Exception + public int getSize() { return Native.getBvSortSize(getContext().nCtx(), getNativeObject()); } - BitVecSort(Context ctx, long obj) throws Z3Exception + BitVecSort(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 6709e2ae907..02eabd2b5de 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -35,7 +35,7 @@ protected BoolExpr(Context ctx) * @throws Z3Exception * @throws Z3Exception on error **/ - BoolExpr(Context ctx, long obj) throws Z3Exception + BoolExpr(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/BoolSort.java b/src/api/java/BoolSort.java index 85ca0a7f7a5..66a4ddaa94b 100644 --- a/src/api/java/BoolSort.java +++ b/src/api/java/BoolSort.java @@ -22,6 +22,6 @@ **/ public class BoolSort extends Sort { - BoolSort(Context ctx, long obj) throws Z3Exception { super(ctx, obj); { }} - BoolSort(Context ctx) throws Z3Exception { super(ctx, Native.mkBoolSort(ctx.nCtx())); { }} + BoolSort(Context ctx, long obj) { super(ctx, obj); { }} + BoolSort(Context ctx) { super(ctx, Native.mkBoolSort(ctx.nCtx())); { }} }; diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 95e7799e170..2ceaddcffb9 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -28,7 +28,7 @@ public class Constructor extends Z3Object * @throws Z3Exception on error * @return an int **/ - public int getNumFields() throws Z3Exception + public int getNumFields() { return n; } @@ -38,7 +38,7 @@ public int getNumFields() throws Z3Exception * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl ConstructorDecl() throws Z3Exception + public FuncDecl ConstructorDecl() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); @@ -52,7 +52,7 @@ public FuncDecl ConstructorDecl() throws Z3Exception * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl getTesterDecl() throws Z3Exception + public FuncDecl getTesterDecl() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); @@ -66,7 +66,7 @@ public FuncDecl getTesterDecl() throws Z3Exception * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl[] getAccessorDecls() throws Z3Exception + public FuncDecl[] getAccessorDecls() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); @@ -82,7 +82,7 @@ public FuncDecl[] getAccessorDecls() throws Z3Exception * Destructor. * @throws Z3Exception on error **/ - protected void finalize() throws Z3Exception + protected void finalize() { Native.delConstructor(getContext().nCtx(), getNativeObject()); } @@ -91,7 +91,7 @@ protected void finalize() throws Z3Exception Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) - throws Z3Exception + { super(ctx); diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 0cff4cfa49c..2b3aa94e2c9 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -26,17 +26,17 @@ public class ConstructorList extends Z3Object * Destructor. * @throws Z3Exception on error **/ - protected void finalize() throws Z3Exception + protected void finalize() { Native.delConstructorList(getContext().nCtx(), getNativeObject()); } - ConstructorList(Context ctx, long obj) throws Z3Exception + ConstructorList(Context ctx, long obj) { super(ctx, obj); } - ConstructorList(Context ctx, Constructor[] constructors) throws Z3Exception + ConstructorList(Context ctx, Constructor[] constructors) { super(ctx); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index ce7cef5c255..744cfc03fb2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -29,7 +29,7 @@ public class Context extends IDisposable /** * Constructor. **/ - public Context() throws Z3Exception + public Context() { super(); m_ctx = Native.mkContextRc(0); @@ -53,7 +53,7 @@ public Context() throws Z3Exception * Note that in previous versions of Z3, this constructor was also used to set global and * module parameters. For this purpose we should now use {@code Global.setParameter} **/ - public Context(Map settings) throws Z3Exception + public Context(Map settings) { super(); long cfg = Native.mkConfig(); @@ -69,7 +69,7 @@ public Context(Map settings) throws Z3Exception * Remarks: Not all integers can be passed to this function. * The legal range of unsigned integers is 0 to 2^30-1. **/ - public IntSymbol mkSymbol(int i) throws Z3Exception + public IntSymbol mkSymbol(int i) { return new IntSymbol(this, i); } @@ -77,7 +77,7 @@ public IntSymbol mkSymbol(int i) throws Z3Exception /** * Create a symbol using a string. **/ - public StringSymbol mkSymbol(String name) throws Z3Exception + public StringSymbol mkSymbol(String name) { return new StringSymbol(this, name); } @@ -85,7 +85,7 @@ public StringSymbol mkSymbol(String name) throws Z3Exception /** * Create an array of symbols. **/ - Symbol[] mkSymbols(String[] names) throws Z3Exception + Symbol[] mkSymbols(String[] names) { if (names == null) return null; @@ -102,7 +102,7 @@ Symbol[] mkSymbols(String[] names) throws Z3Exception /** * Retrieves the Boolean sort of the context. **/ - public BoolSort getBoolSort() throws Z3Exception + public BoolSort getBoolSort() { if (m_boolSort == null) m_boolSort = new BoolSort(this); @@ -112,7 +112,7 @@ public BoolSort getBoolSort() throws Z3Exception /** * Retrieves the Integer sort of the context. **/ - public IntSort getIntSort() throws Z3Exception + public IntSort getIntSort() { if (m_intSort == null) m_intSort = new IntSort(this); @@ -122,7 +122,7 @@ public IntSort getIntSort() throws Z3Exception /** * Retrieves the Real sort of the context. **/ - public RealSort getRealSort() throws Z3Exception + public RealSort getRealSort() { if (m_realSort == null) m_realSort = new RealSort(this); @@ -132,7 +132,7 @@ public RealSort getRealSort() throws Z3Exception /** * Create a new Boolean sort. **/ - public BoolSort mkBoolSort() throws Z3Exception + public BoolSort mkBoolSort() { return new BoolSort(this); } @@ -140,7 +140,7 @@ public BoolSort mkBoolSort() throws Z3Exception /** * Create a new uninterpreted sort. **/ - public UninterpretedSort mkUninterpretedSort(Symbol s) throws Z3Exception + public UninterpretedSort mkUninterpretedSort(Symbol s) { checkContextMatch(s); return new UninterpretedSort(this, s); @@ -149,7 +149,7 @@ public UninterpretedSort mkUninterpretedSort(Symbol s) throws Z3Exception /** * Create a new uninterpreted sort. **/ - public UninterpretedSort mkUninterpretedSort(String str) throws Z3Exception + public UninterpretedSort mkUninterpretedSort(String str) { return mkUninterpretedSort(mkSymbol(str)); } @@ -157,7 +157,7 @@ public UninterpretedSort mkUninterpretedSort(String str) throws Z3Exception /** * Create a new integer sort. **/ - public IntSort mkIntSort() throws Z3Exception + public IntSort mkIntSort() { return new IntSort(this); } @@ -165,7 +165,7 @@ public IntSort mkIntSort() throws Z3Exception /** * Create a real sort. **/ - public RealSort mkRealSort() throws Z3Exception + public RealSort mkRealSort() { return new RealSort(this); } @@ -173,7 +173,7 @@ public RealSort mkRealSort() throws Z3Exception /** * Create a new bit-vector sort. **/ - public BitVecSort mkBitVecSort(int size) throws Z3Exception + public BitVecSort mkBitVecSort(int size) { return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); } @@ -181,7 +181,7 @@ public BitVecSort mkBitVecSort(int size) throws Z3Exception /** * Create a new array sort. **/ - public ArraySort mkArraySort(Sort domain, Sort range) throws Z3Exception + public ArraySort mkArraySort(Sort domain, Sort range) { checkContextMatch(domain); checkContextMatch(range); @@ -192,7 +192,7 @@ public ArraySort mkArraySort(Sort domain, Sort range) throws Z3Exception * Create a new tuple sort. **/ public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, - Sort[] fieldSorts) throws Z3Exception + Sort[] fieldSorts) { checkContextMatch(name); checkContextMatch(fieldNames); @@ -205,7 +205,7 @@ public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, * Create a new enumeration sort. **/ public EnumSort mkEnumSort(Symbol name, Symbol... enumNames) - throws Z3Exception + { checkContextMatch(name); checkContextMatch(enumNames); @@ -216,7 +216,7 @@ public EnumSort mkEnumSort(Symbol name, Symbol... enumNames) * Create a new enumeration sort. **/ public EnumSort mkEnumSort(String name, String... enumNames) - throws Z3Exception + { return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames)); } @@ -224,7 +224,7 @@ public EnumSort mkEnumSort(String name, String... enumNames) /** * Create a new list sort. **/ - public ListSort mkListSort(Symbol name, Sort elemSort) throws Z3Exception + public ListSort mkListSort(Symbol name, Sort elemSort) { checkContextMatch(name); checkContextMatch(elemSort); @@ -234,7 +234,7 @@ public ListSort mkListSort(Symbol name, Sort elemSort) throws Z3Exception /** * Create a new list sort. **/ - public ListSort mkListSort(String name, Sort elemSort) throws Z3Exception + public ListSort mkListSort(String name, Sort elemSort) { checkContextMatch(elemSort); return new ListSort(this, mkSymbol(name), elemSort); @@ -244,7 +244,7 @@ public ListSort mkListSort(String name, Sort elemSort) throws Z3Exception * Create a new finite domain sort. **/ public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size) - throws Z3Exception + { checkContextMatch(name); return new FiniteDomainSort(this, name, size); @@ -254,7 +254,7 @@ public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size) * Create a new finite domain sort. **/ public FiniteDomainSort mkFiniteDomainSort(String name, long size) - throws Z3Exception + { return new FiniteDomainSort(this, mkSymbol(name), size); } @@ -272,7 +272,7 @@ public FiniteDomainSort mkFiniteDomainSort(String name, long size) **/ public Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) - throws Z3Exception + { return new Constructor(this, name, recognizer, fieldNames, sorts, @@ -291,7 +291,7 @@ public Constructor mkConstructor(Symbol name, Symbol recognizer, **/ public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) - throws Z3Exception + { return new Constructor(this, mkSymbol(name), mkSymbol(recognizer), @@ -302,7 +302,7 @@ public Constructor mkConstructor(String name, String recognizer, * Create a new datatype sort. **/ public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors) - throws Z3Exception + { checkContextMatch(name); checkContextMatch(constructors); @@ -313,7 +313,7 @@ public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors) * Create a new datatype sort. **/ public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) - throws Z3Exception + { checkContextMatch(constructors); return new DatatypeSort(this, mkSymbol(name), constructors); @@ -325,7 +325,7 @@ public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) * @param c list of constructors, one list per sort. **/ public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c) - throws Z3Exception + { checkContextMatch(names); int n = (int) names.length; @@ -356,7 +356,7 @@ public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c) * @return **/ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) - throws Z3Exception + { return mkDatatypeSorts(mkSymbols(names), c); } @@ -365,7 +365,7 @@ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) * Creates a new function declaration. **/ public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range) - throws Z3Exception + { checkContextMatch(name); checkContextMatch(domain); @@ -377,7 +377,7 @@ public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range) * Creates a new function declaration. **/ public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range) - throws Z3Exception + { checkContextMatch(name); checkContextMatch(domain); @@ -390,7 +390,7 @@ public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range) * Creates a new function declaration. **/ public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range) - throws Z3Exception + { checkContextMatch(domain); checkContextMatch(range); @@ -401,7 +401,7 @@ public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range) * Creates a new function declaration. **/ public FuncDecl mkFuncDecl(String name, Sort domain, Sort range) - throws Z3Exception + { checkContextMatch(domain); checkContextMatch(range); @@ -416,7 +416,7 @@ public FuncDecl mkFuncDecl(String name, Sort domain, Sort range) * @see mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) - throws Z3Exception + { checkContextMatch(domain); checkContextMatch(range); @@ -426,7 +426,7 @@ public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) /** * Creates a new constant function declaration. **/ - public FuncDecl mkConstDecl(Symbol name, Sort range) throws Z3Exception + public FuncDecl mkConstDecl(Symbol name, Sort range) { checkContextMatch(name); checkContextMatch(range); @@ -436,7 +436,7 @@ public FuncDecl mkConstDecl(Symbol name, Sort range) throws Z3Exception /** * Creates a new constant function declaration. **/ - public FuncDecl mkConstDecl(String name, Sort range) throws Z3Exception + public FuncDecl mkConstDecl(String name, Sort range) { checkContextMatch(range); return new FuncDecl(this, mkSymbol(name), null, range); @@ -449,7 +449,7 @@ public FuncDecl mkConstDecl(String name, Sort range) throws Z3Exception * @see mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshConstDecl(String prefix, Sort range) - throws Z3Exception + { checkContextMatch(range); return new FuncDecl(this, prefix, null, range); @@ -460,7 +460,7 @@ public FuncDecl mkFreshConstDecl(String prefix, Sort range) * @param index The de-Bruijn index of the variable * @param ty The sort of the variable **/ - public Expr mkBound(int index, Sort ty) throws Z3Exception + public Expr mkBound(int index, Sort ty) { return Expr.create(this, Native.mkBound(nCtx(), index, ty.getNativeObject())); @@ -469,7 +469,7 @@ public Expr mkBound(int index, Sort ty) throws Z3Exception /** * Create a quantifier pattern. **/ - public Pattern mkPattern(Expr... terms) throws Z3Exception + public Pattern mkPattern(Expr... terms) { if (terms.length == 0) throw new Z3Exception("Cannot create a pattern from zero terms"); @@ -483,7 +483,7 @@ public Pattern mkPattern(Expr... terms) throws Z3Exception * Creates a new Constant of sort {@code range} and named * {@code name}. **/ - public Expr mkConst(Symbol name, Sort range) throws Z3Exception + public Expr mkConst(Symbol name, Sort range) { checkContextMatch(name); checkContextMatch(range); @@ -498,7 +498,7 @@ public Expr mkConst(Symbol name, Sort range) throws Z3Exception * Creates a new Constant of sort {@code range} and named * {@code name}. **/ - public Expr mkConst(String name, Sort range) throws Z3Exception + public Expr mkConst(String name, Sort range) { return mkConst(mkSymbol(name), range); } @@ -507,7 +507,7 @@ public Expr mkConst(String name, Sort range) throws Z3Exception * Creates a fresh Constant of sort {@code range} and a name * prefixed with {@code prefix}. **/ - public Expr mkFreshConst(String prefix, Sort range) throws Z3Exception + public Expr mkFreshConst(String prefix, Sort range) { checkContextMatch(range); return Expr.create(this, @@ -518,7 +518,7 @@ public Expr mkFreshConst(String prefix, Sort range) throws Z3Exception * Creates a fresh constant from the FuncDecl {@code f}. * @param f A decl of a 0-arity function **/ - public Expr mkConst(FuncDecl f) throws Z3Exception + public Expr mkConst(FuncDecl f) { return mkApp(f, (Expr[]) null); } @@ -526,7 +526,7 @@ public Expr mkConst(FuncDecl f) throws Z3Exception /** * Create a Boolean constant. **/ - public BoolExpr mkBoolConst(Symbol name) throws Z3Exception + public BoolExpr mkBoolConst(Symbol name) { return (BoolExpr) mkConst(name, getBoolSort()); } @@ -534,7 +534,7 @@ public BoolExpr mkBoolConst(Symbol name) throws Z3Exception /** * Create a Boolean constant. **/ - public BoolExpr mkBoolConst(String name) throws Z3Exception + public BoolExpr mkBoolConst(String name) { return (BoolExpr) mkConst(mkSymbol(name), getBoolSort()); } @@ -542,7 +542,7 @@ public BoolExpr mkBoolConst(String name) throws Z3Exception /** * Creates an integer constant. **/ - public IntExpr mkIntConst(Symbol name) throws Z3Exception + public IntExpr mkIntConst(Symbol name) { return (IntExpr) mkConst(name, getIntSort()); } @@ -550,7 +550,7 @@ public IntExpr mkIntConst(Symbol name) throws Z3Exception /** * Creates an integer constant. **/ - public IntExpr mkIntConst(String name) throws Z3Exception + public IntExpr mkIntConst(String name) { return (IntExpr) mkConst(name, getIntSort()); } @@ -558,7 +558,7 @@ public IntExpr mkIntConst(String name) throws Z3Exception /** * Creates a real constant. **/ - public RealExpr mkRealConst(Symbol name) throws Z3Exception + public RealExpr mkRealConst(Symbol name) { return (RealExpr) mkConst(name, getRealSort()); } @@ -566,7 +566,7 @@ public RealExpr mkRealConst(Symbol name) throws Z3Exception /** * Creates a real constant. **/ - public RealExpr mkRealConst(String name) throws Z3Exception + public RealExpr mkRealConst(String name) { return (RealExpr) mkConst(name, getRealSort()); } @@ -574,7 +574,7 @@ public RealExpr mkRealConst(String name) throws Z3Exception /** * Creates a bit-vector constant. **/ - public BitVecExpr mkBVConst(Symbol name, int size) throws Z3Exception + public BitVecExpr mkBVConst(Symbol name, int size) { return (BitVecExpr) mkConst(name, mkBitVecSort(size)); } @@ -582,7 +582,7 @@ public BitVecExpr mkBVConst(Symbol name, int size) throws Z3Exception /** * Creates a bit-vector constant. **/ - public BitVecExpr mkBVConst(String name, int size) throws Z3Exception + public BitVecExpr mkBVConst(String name, int size) { return (BitVecExpr) mkConst(name, mkBitVecSort(size)); } @@ -590,7 +590,7 @@ public BitVecExpr mkBVConst(String name, int size) throws Z3Exception /** * Create a new function application. **/ - public Expr mkApp(FuncDecl f, Expr... args) throws Z3Exception + public Expr mkApp(FuncDecl f, Expr... args) { checkContextMatch(f); checkContextMatch(args); @@ -600,7 +600,7 @@ public Expr mkApp(FuncDecl f, Expr... args) throws Z3Exception /** * The true Term. **/ - public BoolExpr mkTrue() throws Z3Exception + public BoolExpr mkTrue() { return new BoolExpr(this, Native.mkTrue(nCtx())); } @@ -608,7 +608,7 @@ public BoolExpr mkTrue() throws Z3Exception /** * The false Term. **/ - public BoolExpr mkFalse() throws Z3Exception + public BoolExpr mkFalse() { return new BoolExpr(this, Native.mkFalse(nCtx())); } @@ -616,7 +616,7 @@ public BoolExpr mkFalse() throws Z3Exception /** * Creates a Boolean value. **/ - public BoolExpr mkBool(boolean value) throws Z3Exception + public BoolExpr mkBool(boolean value) { return value ? mkTrue() : mkFalse(); } @@ -624,7 +624,7 @@ public BoolExpr mkBool(boolean value) throws Z3Exception /** * Creates the equality {@code x"/> = to every subgoal produced by evaluates to true and level. **/ public void addCover(int level, FuncDecl predicate, Expr property) - throws Z3Exception + { Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level, predicate.getNativeObject(), property.getNativeObject()); @@ -269,7 +269,7 @@ public String toString() * Instrument the Datalog engine on which table representation to use for * recursive predicate. **/ - public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception + public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) { Native.fixedpointSetPredicateRepresentation(getContext().nCtx(), @@ -281,7 +281,7 @@ public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exce /** * Convert benchmark given as set of axioms, rules and queries to a string. **/ - public String toString(BoolExpr[] queries) throws Z3Exception + public String toString(BoolExpr[] queries) { return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), @@ -293,7 +293,7 @@ public String toString(BoolExpr[] queries) throws Z3Exception * * @throws Z3Exception **/ - public BoolExpr[] getRules() throws Z3Exception + public BoolExpr[] getRules() { ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( @@ -310,7 +310,7 @@ public BoolExpr[] getRules() throws Z3Exception * * @throws Z3Exception **/ - public BoolExpr[] getAssertions() throws Z3Exception + public BoolExpr[] getAssertions() { ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( @@ -322,23 +322,23 @@ public BoolExpr[] getAssertions() throws Z3Exception return res; } - Fixedpoint(Context ctx, long obj) throws Z3Exception + Fixedpoint(Context ctx, long obj) { super(ctx, obj); } - Fixedpoint(Context ctx) throws Z3Exception + Fixedpoint(Context ctx) { super(ctx, Native.mkFixedpoint(ctx.nCtx())); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getFixedpointDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getFixedpointDRQ().add(o); super.decRef(o); diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index e9b05f08c15..f7e9de2b298 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -78,7 +78,7 @@ public String toString() /** * Returns a unique identifier for the function declaration. **/ - public int getId() throws Z3Exception + public int getId() { return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); } @@ -86,7 +86,7 @@ public int getId() throws Z3Exception /** * The arity of the function declaration **/ - public int getArity() throws Z3Exception + public int getArity() { return Native.getArity(getContext().nCtx(), getNativeObject()); } @@ -95,7 +95,7 @@ public int getArity() throws Z3Exception * The size of the domain of the function declaration * @see getArity **/ - public int getDomainSize() throws Z3Exception + public int getDomainSize() { return Native.getDomainSize(getContext().nCtx(), getNativeObject()); } @@ -103,7 +103,7 @@ public int getDomainSize() throws Z3Exception /** * The domain of the function declaration **/ - public Sort[] getDomain() throws Z3Exception + public Sort[] getDomain() { int n = getDomainSize(); @@ -118,7 +118,7 @@ public Sort[] getDomain() throws Z3Exception /** * The range of the function declaration **/ - public Sort getRange() throws Z3Exception + public Sort getRange() { return Sort.create(getContext(), @@ -128,7 +128,7 @@ public Sort getRange() throws Z3Exception /** * The kind of the function declaration. **/ - public Z3_decl_kind getDeclKind() throws Z3Exception + public Z3_decl_kind getDeclKind() { return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(), getNativeObject())); @@ -137,7 +137,7 @@ public Z3_decl_kind getDeclKind() throws Z3Exception /** * The name of the function declaration **/ - public Symbol getName() throws Z3Exception + public Symbol getName() { return Symbol.create(getContext(), @@ -147,7 +147,7 @@ public Symbol getName() throws Z3Exception /** * The number of parameters of the function declaration **/ - public int getNumParameters() throws Z3Exception + public int getNumParameters() { return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject()); } @@ -155,7 +155,7 @@ public int getNumParameters() throws Z3Exception /** * The parameters of the function declaration **/ - public Parameter[] getParameters() throws Z3Exception + public Parameter[] getParameters() { int num = getNumParameters(); @@ -223,7 +223,7 @@ public class Parameter /** * The int value of the parameter. **/ - public int getInt() throws Z3Exception + public int getInt() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); @@ -233,7 +233,7 @@ public int getInt() throws Z3Exception /** * The double value of the parameter. **/ - public double getDouble() throws Z3Exception + public double getDouble() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); @@ -243,7 +243,7 @@ public double getDouble() throws Z3Exception /** * The Symbol value of the parameter. **/ - public Symbol getSymbol() throws Z3Exception + public Symbol getSymbol() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); @@ -253,7 +253,7 @@ public Symbol getSymbol() throws Z3Exception /** * The Sort value of the parameter. **/ - public Sort getSort() throws Z3Exception + public Sort getSort() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); @@ -263,7 +263,7 @@ public Sort getSort() throws Z3Exception /** * The AST value of the parameter. **/ - public AST getAST() throws Z3Exception + public AST getAST() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); @@ -273,7 +273,7 @@ public AST getAST() throws Z3Exception /** * The FunctionDeclaration value of the parameter. **/ - public FuncDecl getFuncDecl() throws Z3Exception + public FuncDecl getFuncDecl() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); @@ -283,7 +283,7 @@ public FuncDecl getFuncDecl() throws Z3Exception /** * The rational string value of the parameter. **/ - public String getRational() throws Z3Exception + public String getRational() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); @@ -293,7 +293,7 @@ public String getRational() throws Z3Exception /** * The kind of the parameter. **/ - public Z3_parameter_kind getParameterKind() throws Z3Exception + public Z3_parameter_kind getParameterKind() { return kind; } @@ -341,14 +341,14 @@ public Z3_parameter_kind getParameterKind() throws Z3Exception } } - FuncDecl(Context ctx, long obj) throws Z3Exception + FuncDecl(Context ctx, long obj) { super(ctx, obj); } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - throws Z3Exception + { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), @@ -357,7 +357,7 @@ public Z3_parameter_kind getParameterKind() throws Z3Exception } FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - throws Z3Exception + { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.arrayLength(domain), AST.arrayToNative(domain), @@ -365,7 +365,7 @@ public Z3_parameter_kind getParameterKind() throws Z3Exception } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST .toInt()) @@ -380,7 +380,7 @@ void checkNativeObject(long obj) throws Z3Exception * * @return **/ - public Expr apply(Expr ... args) throws Z3Exception + public Expr apply(Expr ... args) { getContext().checkContextMatch(args); return Expr.create(getContext(), this, args); diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 31f37a4ba5e..59a8a0398a7 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -36,7 +36,7 @@ public class Entry extends Z3Object * @throws Z3Exception * @throws Z3Exception on error **/ - public Expr getValue() throws Z3Exception + public Expr getValue() { return Expr.create(getContext(), Native.funcEntryGetValue(getContext().nCtx(), getNativeObject())); @@ -46,7 +46,7 @@ public Expr getValue() throws Z3Exception * The number of arguments of the entry. * @throws Z3Exception on error **/ - public int getNumArgs() throws Z3Exception + public int getNumArgs() { return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject()); } @@ -57,7 +57,7 @@ public int getNumArgs() throws Z3Exception * @throws Z3Exception * @throws Z3Exception on error **/ - public Expr[] getArgs() throws Z3Exception + public Expr[] getArgs() { int n = getNumArgs(); Expr[] res = new Expr[n]; @@ -86,18 +86,18 @@ public String toString() } } - Entry(Context ctx, long obj) throws Z3Exception + Entry(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getFuncEntryDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getFuncEntryDRQ().add(o); super.decRef(o); @@ -109,7 +109,7 @@ void decRef(long o) throws Z3Exception * @throws Z3Exception on error * @return an int **/ - public int getNumEntries() throws Z3Exception + public int getNumEntries() { return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject()); } @@ -120,7 +120,7 @@ public int getNumEntries() throws Z3Exception * @throws Z3Exception * @throws Z3Exception on error **/ - public Entry[] getEntries() throws Z3Exception + public Entry[] getEntries() { int n = getNumEntries(); Entry[] res = new Entry[n]; @@ -137,7 +137,7 @@ public Entry[] getEntries() throws Z3Exception * @throws Z3Exception on error * @return an Expr **/ - public Expr getElse() throws Z3Exception + public Expr getElse() { return Expr.create(getContext(), Native.funcInterpGetElse(getContext().nCtx(), getNativeObject())); @@ -148,7 +148,7 @@ public Expr getElse() throws Z3Exception * @throws Z3Exception on error * @return an int **/ - public int getArity() throws Z3Exception + public int getArity() { return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject()); } @@ -187,18 +187,18 @@ public String toString() } } - FuncInterp(Context ctx, long obj) throws Z3Exception + FuncInterp(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getFuncInterpDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getFuncInterpDRQ().add(o); super.decRef(o); diff --git a/src/api/java/Global.java b/src/api/java/Global.java index 65bae9a01bc..67a051792ba 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -81,7 +81,7 @@ public static void resetParameters() * globally. **/ public static void ToggleWarningMessages(boolean enabled) - throws Z3Exception + { Native.toggleWarningMessages((enabled) ? true : false); } diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 64f2e0acbe2..18aecb55785 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -33,7 +33,7 @@ public class Goal extends Z3Object * applied when the objective is to find a proof for a given goal. * **/ - public Z3_goal_prec getPrecision() throws Z3Exception + public Z3_goal_prec getPrecision() { return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(), getNativeObject())); @@ -42,7 +42,7 @@ public Z3_goal_prec getPrecision() throws Z3Exception /** * Indicates whether the goal is precise. **/ - public boolean isPrecise() throws Z3Exception + public boolean isPrecise() { return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE; } @@ -50,7 +50,7 @@ public boolean isPrecise() throws Z3Exception /** * Indicates whether the goal is an under-approximation. **/ - public boolean isUnderApproximation() throws Z3Exception + public boolean isUnderApproximation() { return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER; } @@ -58,7 +58,7 @@ public boolean isUnderApproximation() throws Z3Exception /** * Indicates whether the goal is an over-approximation. **/ - public boolean isOverApproximation() throws Z3Exception + public boolean isOverApproximation() { return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER; } @@ -67,7 +67,7 @@ public boolean isOverApproximation() throws Z3Exception * Indicates whether the goal is garbage (i.e., the product of over- and * under-approximations). **/ - public boolean isGarbage() throws Z3Exception + public boolean isGarbage() { return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; } @@ -77,7 +77,7 @@ public boolean isGarbage() throws Z3Exception * * @throws Z3Exception **/ - public void add(BoolExpr ... constraints) throws Z3Exception + public void add(BoolExpr ... constraints) { getContext().checkContextMatch(constraints); for (BoolExpr c : constraints) @@ -90,7 +90,7 @@ public void add(BoolExpr ... constraints) throws Z3Exception /** * Indicates whether the goal contains `false'. **/ - public boolean inconsistent() throws Z3Exception + public boolean inconsistent() { return Native.goalInconsistent(getContext().nCtx(), getNativeObject()); } @@ -100,7 +100,7 @@ public boolean inconsistent() throws Z3Exception * Remarks: This tracks how many transformations * were applied to it. **/ - public int getDepth() throws Z3Exception + public int getDepth() { return Native.goalDepth(getContext().nCtx(), getNativeObject()); } @@ -108,7 +108,7 @@ public int getDepth() throws Z3Exception /** * Erases all formulas from the given goal. **/ - public void reset() throws Z3Exception + public void reset() { Native.goalReset(getContext().nCtx(), getNativeObject()); } @@ -116,7 +116,7 @@ public void reset() throws Z3Exception /** * The number of formulas in the goal. **/ - public int size() throws Z3Exception + public int size() { return Native.goalSize(getContext().nCtx(), getNativeObject()); } @@ -126,7 +126,7 @@ public int size() throws Z3Exception * * @throws Z3Exception **/ - public BoolExpr[] getFormulas() throws Z3Exception + public BoolExpr[] getFormulas() { int n = size(); BoolExpr[] res = new BoolExpr[n]; @@ -139,7 +139,7 @@ public BoolExpr[] getFormulas() throws Z3Exception /** * The number of formulas, subformulas and terms in the goal. **/ - public int getNumExprs() throws Z3Exception + public int getNumExprs() { return Native.goalNumExprs(getContext().nCtx(), getNativeObject()); } @@ -148,7 +148,7 @@ public int getNumExprs() throws Z3Exception * Indicates whether the goal is empty, and it is precise or the product of * an under approximation. **/ - public boolean isDecidedSat() throws Z3Exception + public boolean isDecidedSat() { return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject()); } @@ -157,7 +157,7 @@ public boolean isDecidedSat() throws Z3Exception * Indicates whether the goal contains `false', and it is precise or the * product of an over approximation. **/ - public boolean isDecidedUnsat() throws Z3Exception + public boolean isDecidedUnsat() { return Native .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject()); @@ -168,7 +168,7 @@ public boolean isDecidedUnsat() throws Z3Exception * * @throws Z3Exception **/ - public Goal translate(Context ctx) throws Z3Exception + public Goal translate(Context ctx) { return new Goal(ctx, Native.goalTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx())); @@ -179,7 +179,7 @@ public Goal translate(Context ctx) throws Z3Exception * Remarks: Essentially invokes the `simplify' tactic * on the goal. **/ - public Goal simplify() throws Z3Exception + public Goal simplify() { Tactic t = getContext().mkTactic("simplify"); ApplyResult res = t.apply(this); @@ -195,7 +195,7 @@ public Goal simplify() throws Z3Exception * Remarks: Essentially invokes the `simplify' tactic * on the goal. **/ - public Goal simplify(Params p) throws Z3Exception + public Goal simplify(Params p) { Tactic t = getContext().mkTactic("simplify"); ApplyResult res = t.apply(this, p); @@ -222,25 +222,25 @@ public String toString() } } - Goal(Context ctx, long obj) throws Z3Exception + Goal(Context ctx, long obj) { super(ctx, obj); } Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) - throws Z3Exception + { super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false)); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getGoalDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getGoalDRQ().add(o); super.decRef(o); diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java index dddfa5824f6..c3855c42873 100644 --- a/src/api/java/IDisposable.java +++ b/src/api/java/IDisposable.java @@ -21,7 +21,7 @@ Christoph Wintersteiger (cwinter) 2012-03-16 public class IDisposable { - public void dispose() throws Z3Exception + public void dispose() { } } diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index a424cd51e1f..56ba9ccdf52 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -26,7 +26,7 @@ public class IntExpr extends ArithExpr * Constructor for IntExpr * @throws Z3Exception on error **/ - IntExpr(Context ctx, long obj) throws Z3Exception + IntExpr(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index 0fdcf1aa6f5..4078b3db372 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -25,7 +25,7 @@ public class IntNum extends IntExpr { - IntNum(Context ctx, long obj) throws Z3Exception + IntNum(Context ctx, long obj) { super(ctx, obj); } @@ -33,7 +33,7 @@ public class IntNum extends IntExpr /** * Retrieve the int value. **/ - public int getInt() throws Z3Exception + public int getInt() { Native.IntPtr res = new Native.IntPtr(); if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) @@ -44,7 +44,7 @@ public int getInt() throws Z3Exception /** * Retrieve the 64-bit int value. **/ - public long getInt64() throws Z3Exception + public long getInt64() { Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) @@ -55,7 +55,7 @@ public long getInt64() throws Z3Exception /** * Retrieve the BigInteger value. **/ - public BigInteger getBigInteger() throws Z3Exception + public BigInteger getBigInteger() { return new BigInteger(this.toString()); } diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java index 0b104771814..59526ed0b40 100644 --- a/src/api/java/IntSort.java +++ b/src/api/java/IntSort.java @@ -22,12 +22,12 @@ **/ public class IntSort extends ArithSort { - IntSort(Context ctx, long obj) throws Z3Exception + IntSort(Context ctx, long obj) { super(ctx, obj); } - IntSort(Context ctx) throws Z3Exception + IntSort(Context ctx) { super(ctx, Native.mkIntSort(ctx.nCtx())); } diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java index 01f75e0a47e..db99e684004 100644 --- a/src/api/java/IntSymbol.java +++ b/src/api/java/IntSymbol.java @@ -29,24 +29,24 @@ public class IntSymbol extends Symbol * Remarks: Throws an exception if the symbol * is not of int kind. **/ - public int getInt() throws Z3Exception + public int getInt() { if (!isIntSymbol()) throw new Z3Exception("Int requested from non-Int symbol"); return Native.getSymbolInt(getContext().nCtx(), getNativeObject()); } - IntSymbol(Context ctx, long obj) throws Z3Exception + IntSymbol(Context ctx, long obj) { super(ctx, obj); } - IntSymbol(Context ctx, int i) throws Z3Exception + IntSymbol(Context ctx, int i) { super(ctx, Native.mkIntSymbol(ctx.nCtx(), i)); } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL .toInt()) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 91aac7f93c2..897c0e9e9b4 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -33,7 +33,7 @@ public class InterpolationContext extends Context /** * Constructor. **/ - public InterpolationContext() throws Z3Exception + public InterpolationContext() { m_ctx = Native.mkInterpolationContext(0); initContext(); @@ -46,7 +46,7 @@ public InterpolationContext() throws Z3Exception * Remarks: * @see Context#Context **/ - public InterpolationContext(Map settings) throws Z3Exception + public InterpolationContext(Map settings) { long cfg = Native.mkConfig(); for (Map.Entry kv : settings.entrySet()) @@ -60,7 +60,7 @@ public InterpolationContext(Map settings) throws Z3Exception * Create an expression that marks a formula position for interpolation. * @throws Z3Exception **/ - public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception + public BoolExpr MkInterpolant(BoolExpr a) { checkContextMatch(a); return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); @@ -73,7 +73,7 @@ public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception * well documented. * @throws Z3Exception **/ - public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception + public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) { checkContextMatch(pf); checkContextMatch(pat); @@ -94,7 +94,7 @@ public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception * well documented. * @throws Z3Exception **/ - public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception + public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) { checkContextMatch(pat); checkContextMatch(p); @@ -113,7 +113,7 @@ public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model m /// Remarks: For more information on interpolation please refer /// too the function Z3_interpolation_profile in the C/C++ API, which is /// well documented. - public String InterpolationProfile() throws Z3Exception + public String InterpolationProfile() { return Native.interpolationProfile(nCtx()); } @@ -124,7 +124,7 @@ public String InterpolationProfile() throws Z3Exception /// Remarks: For more information on interpolation please refer /// too the function Z3_check_interpolant in the C/C++ API, which is /// well documented. - public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception + public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) { Native.StringPtr n_err_str = new Native.StringPtr(); int r = Native.checkInterpolant(nCtx(), @@ -145,7 +145,7 @@ public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String /// Remarks: For more information on interpolation please refer /// too the function Z3_read_interpolation_problem in the C/C++ API, which is /// well documented. - public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) { Native.IntPtr n_num = new Native.IntPtr(); Native.IntPtr n_num_theory = new Native.IntPtr(); @@ -176,7 +176,7 @@ public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents /// Remarks: For more information on interpolation please refer /// too the function Z3_write_interpolation_problem in the C/C++ API, which is /// well documented. - public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) { Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); } diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index a7ad0403b08..705e9357988 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -26,7 +26,7 @@ public class ListSort extends Sort * The declaration of the nil function of this list sort. * @throws Z3Exception **/ - public FuncDecl getNilDecl() throws Z3Exception + public FuncDecl getNilDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0)); } @@ -35,7 +35,7 @@ public FuncDecl getNilDecl() throws Z3Exception * The empty list. * @throws Z3Exception **/ - public Expr getNil() throws Z3Exception + public Expr getNil() { return getContext().mkApp(getNilDecl()); } @@ -44,7 +44,7 @@ public Expr getNil() throws Z3Exception * The declaration of the isNil function of this list sort. * @throws Z3Exception **/ - public FuncDecl getIsNilDecl() throws Z3Exception + public FuncDecl getIsNilDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0)); } @@ -53,7 +53,7 @@ public FuncDecl getIsNilDecl() throws Z3Exception * The declaration of the cons function of this list sort. * @throws Z3Exception **/ - public FuncDecl getConsDecl() throws Z3Exception + public FuncDecl getConsDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1)); } @@ -63,7 +63,7 @@ public FuncDecl getConsDecl() throws Z3Exception * @throws Z3Exception * **/ - public FuncDecl getIsConsDecl() throws Z3Exception + public FuncDecl getIsConsDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1)); } @@ -72,7 +72,7 @@ public FuncDecl getIsConsDecl() throws Z3Exception * The declaration of the head function of this list sort. * @throws Z3Exception **/ - public FuncDecl getHeadDecl() throws Z3Exception + public FuncDecl getHeadDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0)); } @@ -81,12 +81,12 @@ public FuncDecl getHeadDecl() throws Z3Exception * The declaration of the tail function of this list sort. * @throws Z3Exception **/ - public FuncDecl getTailDecl() throws Z3Exception + public FuncDecl getTailDecl() { return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1)); } - ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception + ListSort(Context ctx, Symbol name, Sort elemSort) { super(ctx, 0); diff --git a/src/api/java/Log.java b/src/api/java/Log.java index ac0ebfb7f49..7dc9a1ef12a 100644 --- a/src/api/java/Log.java +++ b/src/api/java/Log.java @@ -53,7 +53,7 @@ public static void close() * log. * @throws Z3Exception **/ - public static void append(String s) throws Z3Exception + public static void append(String s) { if (!m_is_open) throw new Z3Exception("Log cannot be closed."); diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 3d68d5485f5..22d2320065d 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -33,7 +33,7 @@ public class Model extends Z3Object * null otherwise. * @throws Z3Exception **/ - public Expr getConstInterp(Expr a) throws Z3Exception + public Expr getConstInterp(Expr a) { getContext().checkContextMatch(a); return getConstInterp(a.getFuncDecl()); @@ -48,7 +48,7 @@ public Expr getConstInterp(Expr a) throws Z3Exception * null otherwise. * @throws Z3Exception **/ - public Expr getConstInterp(FuncDecl f) throws Z3Exception + public Expr getConstInterp(FuncDecl f) { getContext().checkContextMatch(f); if (f.getArity() != 0 @@ -74,7 +74,7 @@ public Expr getConstInterp(FuncDecl f) throws Z3Exception * the model, null otherwise. * @throws Z3Exception **/ - public FuncInterp getFuncInterp(FuncDecl f) throws Z3Exception + public FuncInterp getFuncInterp(FuncDecl f) { getContext().checkContextMatch(f); @@ -117,7 +117,7 @@ public FuncInterp getFuncInterp(FuncDecl f) throws Z3Exception /** * The number of constants that have an interpretation in the model. **/ - public int getNumConsts() throws Z3Exception + public int getNumConsts() { return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject()); } @@ -127,7 +127,7 @@ public int getNumConsts() throws Z3Exception * * @throws Z3Exception **/ - public FuncDecl[] getConstDecls() throws Z3Exception + public FuncDecl[] getConstDecls() { int n = getNumConsts(); FuncDecl[] res = new FuncDecl[n]; @@ -140,7 +140,7 @@ public FuncDecl[] getConstDecls() throws Z3Exception /** * The number of function interpretations in the model. **/ - public int getNumFuncs() throws Z3Exception + public int getNumFuncs() { return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject()); } @@ -150,7 +150,7 @@ public int getNumFuncs() throws Z3Exception * * @throws Z3Exception **/ - public FuncDecl[] getFuncDecls() throws Z3Exception + public FuncDecl[] getFuncDecls() { int n = getNumFuncs(); FuncDecl[] res = new FuncDecl[n]; @@ -165,7 +165,7 @@ public FuncDecl[] getFuncDecls() throws Z3Exception * * @throws Z3Exception **/ - public FuncDecl[] getDecls() throws Z3Exception + public FuncDecl[] getDecls() { int nFuncs = getNumFuncs(); int nConsts = getNumConsts(); @@ -208,7 +208,7 @@ public ModelEvaluationFailedException() * @return The evaluation of {@code t} in the model. * @throws Z3Exception **/ - public Expr eval(Expr t, boolean completion) throws Z3Exception + public Expr eval(Expr t, boolean completion) { Native.LongPtr v = new Native.LongPtr(); if (Native.modelEval(getContext().nCtx(), getNativeObject(), @@ -223,7 +223,7 @@ public Expr eval(Expr t, boolean completion) throws Z3Exception * * @throws Z3Exception **/ - public Expr evaluate(Expr t, boolean completion) throws Z3Exception + public Expr evaluate(Expr t, boolean completion) { return eval(t, completion); } @@ -232,7 +232,7 @@ public Expr evaluate(Expr t, boolean completion) throws Z3Exception * The number of uninterpreted sorts that the model has an interpretation * for. **/ - public int getNumSorts() throws Z3Exception + public int getNumSorts() { return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject()); } @@ -248,7 +248,7 @@ public int getNumSorts() throws Z3Exception * * @throws Z3Exception **/ - public Sort[] getSorts() throws Z3Exception + public Sort[] getSorts() { int n = getNumSorts(); @@ -268,7 +268,7 @@ public Sort[] getSorts() throws Z3Exception * of {@code s} * @throws Z3Exception **/ - public Expr[] getSortUniverse(Sort s) throws Z3Exception + public Expr[] getSortUniverse(Sort s) { ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse( @@ -296,18 +296,18 @@ public String toString() } } - Model(Context ctx, long obj) throws Z3Exception + Model(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getModelDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getModelDRQ().add(o); super.decRef(o); diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index e1f0d16e507..514c65b4672 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -27,7 +27,7 @@ public class ParamDescrs extends Z3Object /** * validate a set of parameters. **/ - public void validate(Params p) throws Z3Exception + public void validate(Params p) { Native.paramsValidate(getContext().nCtx(), p.getNativeObject(), @@ -37,7 +37,7 @@ public void validate(Params p) throws Z3Exception /** * Retrieve kind of parameter. **/ - public Z3_param_kind getKind(Symbol name) throws Z3Exception + public Z3_param_kind getKind(Symbol name) { return Z3_param_kind.fromInt(Native.paramDescrsGetKind( @@ -49,7 +49,7 @@ public Z3_param_kind getKind(Symbol name) throws Z3Exception * * @throws Z3Exception **/ - public Symbol[] getNames() throws Z3Exception + public Symbol[] getNames() { int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject()); Symbol[] names = new Symbol[sz]; @@ -64,7 +64,7 @@ public Symbol[] getNames() throws Z3Exception /** * The size of the ParamDescrs. **/ - public int size() throws Z3Exception + public int size() { return Native.paramDescrsSize(getContext().nCtx(), getNativeObject()); } @@ -83,18 +83,18 @@ public String toString() } } - ParamDescrs(Context ctx, long obj) throws Z3Exception + ParamDescrs(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getParamDescrsDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getParamDescrsDRQ().add(o); super.decRef(o); diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 693491f4162..c241ac8aad8 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -26,7 +26,7 @@ public class Params extends Z3Object /** * Adds a parameter setting. **/ - public void add(Symbol name, boolean value) throws Z3Exception + public void add(Symbol name, boolean value) { Native.paramsSetBool(getContext().nCtx(), getNativeObject(), name.getNativeObject(), (value) ? true : false); @@ -35,7 +35,7 @@ public void add(Symbol name, boolean value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(Symbol name, double value) throws Z3Exception + public void add(Symbol name, double value) { Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), name.getNativeObject(), value); @@ -44,7 +44,7 @@ public void add(Symbol name, double value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(Symbol name, String value) throws Z3Exception + public void add(Symbol name, String value) { Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), @@ -55,7 +55,7 @@ public void add(Symbol name, String value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(Symbol name, Symbol value) throws Z3Exception + public void add(Symbol name, Symbol value) { Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), @@ -65,7 +65,7 @@ public void add(Symbol name, Symbol value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(String name, boolean value) throws Z3Exception + public void add(String name, boolean value) { Native.paramsSetBool(getContext().nCtx(), getNativeObject(), getContext().mkSymbol(name).getNativeObject(), value); @@ -74,7 +74,7 @@ public void add(String name, boolean value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(String name, int value) throws Z3Exception + public void add(String name, int value) { Native.paramsSetUint(getContext().nCtx(), getNativeObject(), getContext() .mkSymbol(name).getNativeObject(), value); @@ -83,7 +83,7 @@ public void add(String name, int value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(String name, double value) throws Z3Exception + public void add(String name, double value) { Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), getContext() .mkSymbol(name).getNativeObject(), value); @@ -92,7 +92,7 @@ public void add(String name, double value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(String name, Symbol value) throws Z3Exception + public void add(String name, Symbol value) { Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), getContext() .mkSymbol(name).getNativeObject(), value.getNativeObject()); @@ -101,7 +101,7 @@ public void add(String name, Symbol value) throws Z3Exception /** * Adds a parameter setting. **/ - public void add(String name, String value) throws Z3Exception + public void add(String name, String value) { Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), @@ -123,18 +123,18 @@ public String toString() } } - Params(Context ctx) throws Z3Exception + Params(Context ctx) { super(ctx, Native.mkParams(ctx.nCtx())); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getParamsDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getParamsDRQ().add(o); super.decRef(o); diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index 797b387d096..d51315abf0a 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -26,7 +26,7 @@ public class Pattern extends AST /** * The number of terms in the pattern. **/ - public int getNumTerms() throws Z3Exception + public int getNumTerms() { return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject()); } @@ -36,7 +36,7 @@ public int getNumTerms() throws Z3Exception * * @throws Z3Exception **/ - public Expr[] getTerms() throws Z3Exception + public Expr[] getTerms() { int n = getNumTerms(); @@ -61,7 +61,7 @@ public String toString() } } - Pattern(Context ctx, long obj) throws Z3Exception + Pattern(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index 62b0612b9c6..e190229dfd1 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -34,30 +34,30 @@ public class Probe extends Z3Object * 0.0 for false, and a value different from 0.0 for true. * @throws Z3Exception **/ - public double apply(Goal g) throws Z3Exception + public double apply(Goal g) { getContext().checkContextMatch(g); return Native.probeApply(getContext().nCtx(), getNativeObject(), g.getNativeObject()); } - Probe(Context ctx, long obj) throws Z3Exception + Probe(Context ctx, long obj) { super(ctx, obj); } - Probe(Context ctx, String name) throws Z3Exception + Probe(Context ctx, String name) { super(ctx, Native.mkProbe(ctx.nCtx(), name)); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getProbeDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getProbeDRQ().add(o); super.decRef(o); diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 3ea2b2eaf8e..08df1c1f554 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -27,7 +27,7 @@ public class Quantifier extends BoolExpr /** * Indicates whether the quantifier is universal. **/ - public boolean isUniversal() throws Z3Exception + public boolean isUniversal() { return Native.isQuantifierForall(getContext().nCtx(), getNativeObject()); } @@ -35,7 +35,7 @@ public boolean isUniversal() throws Z3Exception /** * Indicates whether the quantifier is existential. **/ - public boolean isExistential() throws Z3Exception + public boolean isExistential() { return !isUniversal(); } @@ -43,7 +43,7 @@ public boolean isExistential() throws Z3Exception /** * The weight of the quantifier. **/ - public int getWeight() throws Z3Exception + public int getWeight() { return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject()); } @@ -51,7 +51,7 @@ public int getWeight() throws Z3Exception /** * The number of patterns. **/ - public int getNumPatterns() throws Z3Exception + public int getNumPatterns() { return Native .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject()); @@ -62,7 +62,7 @@ public int getNumPatterns() throws Z3Exception * * @throws Z3Exception **/ - public Pattern[] getPatterns() throws Z3Exception + public Pattern[] getPatterns() { int n = getNumPatterns(); Pattern[] res = new Pattern[n]; @@ -75,7 +75,7 @@ public Pattern[] getPatterns() throws Z3Exception /** * The number of no-patterns. **/ - public int getNumNoPatterns() throws Z3Exception + public int getNumNoPatterns() { return Native.getQuantifierNumNoPatterns(getContext().nCtx(), getNativeObject()); @@ -86,7 +86,7 @@ public int getNumNoPatterns() throws Z3Exception * * @throws Z3Exception **/ - public Pattern[] getNoPatterns() throws Z3Exception + public Pattern[] getNoPatterns() { int n = getNumNoPatterns(); Pattern[] res = new Pattern[n]; @@ -99,7 +99,7 @@ public Pattern[] getNoPatterns() throws Z3Exception /** * The number of bound variables. **/ - public int getNumBound() throws Z3Exception + public int getNumBound() { return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject()); } @@ -109,7 +109,7 @@ public int getNumBound() throws Z3Exception * * @throws Z3Exception **/ - public Symbol[] getBoundVariableNames() throws Z3Exception + public Symbol[] getBoundVariableNames() { int n = getNumBound(); Symbol[] res = new Symbol[n]; @@ -124,7 +124,7 @@ public Symbol[] getBoundVariableNames() throws Z3Exception * * @throws Z3Exception **/ - public Sort[] getBoundVariableSorts() throws Z3Exception + public Sort[] getBoundVariableSorts() { int n = getNumBound(); Sort[] res = new Sort[n]; @@ -139,7 +139,7 @@ public Sort[] getBoundVariableSorts() throws Z3Exception * * @throws Z3Exception **/ - public BoolExpr getBody() throws Z3Exception + public BoolExpr getBody() { return new BoolExpr(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); @@ -147,7 +147,7 @@ public BoolExpr getBody() throws Z3Exception Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) throws Z3Exception + Symbol quantifierID, Symbol skolemID) { super(ctx, 0); @@ -183,7 +183,7 @@ public BoolExpr getBody() throws Z3Exception Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) throws Z3Exception + Symbol quantifierID, Symbol skolemID) { super(ctx, 0); @@ -210,12 +210,12 @@ public BoolExpr getBody() throws Z3Exception } } - Quantifier(Context ctx, long obj) throws Z3Exception + Quantifier(Context ctx, long obj) { super(ctx, obj); } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST .toInt()) diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index 278aba65e00..8fd81574260 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -27,7 +27,7 @@ public class RatNum extends RealExpr /** * The numerator of a rational numeral. **/ - public IntNum getNumerator() throws Z3Exception + public IntNum getNumerator() { return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(), getNativeObject())); @@ -36,7 +36,7 @@ public IntNum getNumerator() throws Z3Exception /** * The denominator of a rational numeral. **/ - public IntNum getDenominator() throws Z3Exception + public IntNum getDenominator() { return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(), getNativeObject())); @@ -45,7 +45,7 @@ public IntNum getDenominator() throws Z3Exception /** * Converts the numerator of the rational to a BigInteger **/ - public BigInteger getBigIntNumerator() throws Z3Exception + public BigInteger getBigIntNumerator() { IntNum n = getNumerator(); return new BigInteger(n.toString()); @@ -54,7 +54,7 @@ public BigInteger getBigIntNumerator() throws Z3Exception /** * Converts the denominator of the rational to a BigInteger **/ - public BigInteger getBigIntDenominator() throws Z3Exception + public BigInteger getBigIntDenominator() { IntNum n = getDenominator(); return new BigInteger(n.toString()); @@ -65,7 +65,7 @@ public BigInteger getBigIntDenominator() throws Z3Exception * Remarks: The result * has at most {@code precision} decimal places. **/ - public String toDecimalString(int precision) throws Z3Exception + public String toDecimalString(int precision) { return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(), precision); @@ -85,7 +85,7 @@ public String toString() } } - RatNum(Context ctx, long obj) throws Z3Exception + RatNum(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index 579d344e191..c977e2ac0e0 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -25,7 +25,7 @@ public class RealExpr extends ArithExpr /** * Constructor for RealExpr **/ - RealExpr(Context ctx, long obj) throws Z3Exception + RealExpr(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/RealSort.java b/src/api/java/RealSort.java index d76823a0dd6..0f6333314a4 100644 --- a/src/api/java/RealSort.java +++ b/src/api/java/RealSort.java @@ -22,12 +22,12 @@ **/ public class RealSort extends ArithSort { - RealSort(Context ctx, long obj) throws Z3Exception + RealSort(Context ctx, long obj) { super(ctx, obj); } - RealSort(Context ctx) throws Z3Exception + RealSort(Context ctx) { super(ctx, Native.mkRealSort(ctx.nCtx())); } diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java index 77f6c595bca..e996479aba4 100644 --- a/src/api/java/RelationSort.java +++ b/src/api/java/RelationSort.java @@ -25,7 +25,7 @@ public class RelationSort extends Sort /** * The arity of the relation sort. **/ - public int getArity() throws Z3Exception + public int getArity() { return Native.getRelationArity(getContext().nCtx(), getNativeObject()); } @@ -34,7 +34,7 @@ public int getArity() throws Z3Exception * The sorts of the columns of the relation sort. * @throws Z3Exception **/ - public Sort[] getColumnSorts() throws Z3Exception + public Sort[] getColumnSorts() { if (m_columnSorts != null) @@ -50,7 +50,7 @@ public Sort[] getColumnSorts() throws Z3Exception private Sort[] m_columnSorts = null; - RelationSort(Context ctx, long obj) throws Z3Exception + RelationSort(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java index 69126933a07..2aa821250e0 100644 --- a/src/api/java/SetSort.java +++ b/src/api/java/SetSort.java @@ -22,12 +22,12 @@ **/ public class SetSort extends Sort { - SetSort(Context ctx, long obj) throws Z3Exception + SetSort(Context ctx, long obj) { super(ctx, obj); } - SetSort(Context ctx, Sort ty) throws Z3Exception + SetSort(Context ctx, Sort ty) { super(ctx, Native.mkSetSort(ctx.nCtx(), ty.getNativeObject())); } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index db3f46bfd57..e4ba9de4263 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -27,7 +27,7 @@ public class Solver extends Z3Object /** * A string that describes all available solver parameters. **/ - public String getHelp() throws Z3Exception + public String getHelp() { return Native.solverGetHelp(getContext().nCtx(), getNativeObject()); } @@ -37,7 +37,7 @@ public String getHelp() throws Z3Exception * * @throws Z3Exception **/ - public void setParameters(Params value) throws Z3Exception + public void setParameters(Params value) { getContext().checkContextMatch(value); Native.solverSetParams(getContext().nCtx(), getNativeObject(), @@ -49,7 +49,7 @@ public void setParameters(Params value) throws Z3Exception * * @throws Z3Exception **/ - public ParamDescrs getParameterDescriptions() throws Z3Exception + public ParamDescrs getParameterDescriptions() { return new ParamDescrs(getContext(), Native.solverGetParamDescrs( getContext().nCtx(), getNativeObject())); @@ -60,7 +60,7 @@ public ParamDescrs getParameterDescriptions() throws Z3Exception * @see pop * @see push **/ - public int getNumScopes() throws Z3Exception + public int getNumScopes() { return Native .solverGetNumScopes(getContext().nCtx(), getNativeObject()); @@ -70,7 +70,7 @@ public int getNumScopes() throws Z3Exception * Creates a backtracking point. * @see pop **/ - public void push() throws Z3Exception + public void push() { Native.solverPush(getContext().nCtx(), getNativeObject()); } @@ -79,7 +79,7 @@ public void push() throws Z3Exception * Backtracks one backtracking point. * Remarks: . **/ - public void pop() throws Z3Exception + public void pop() { pop(1); } @@ -91,7 +91,7 @@ public void pop() throws Z3Exception * {@code NumScopes} * @see push **/ - public void pop(int n) throws Z3Exception + public void pop(int n) { Native.solverPop(getContext().nCtx(), getNativeObject(), n); } @@ -101,7 +101,7 @@ public void pop(int n) throws Z3Exception * Remarks: This removes all assertions from the * solver. **/ - public void reset() throws Z3Exception + public void reset() { Native.solverReset(getContext().nCtx(), getNativeObject()); } @@ -111,7 +111,7 @@ public void reset() throws Z3Exception * * @throws Z3Exception **/ - public void add(BoolExpr... constraints) throws Z3Exception + public void add(BoolExpr... constraints) { getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) @@ -135,7 +135,7 @@ public void add(BoolExpr... constraints) throws Z3Exception * and the Boolean literals * provided using with assumptions. **/ - public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception + public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { getContext().checkContextMatch(constraints); getContext().checkContextMatch(ps); @@ -160,7 +160,7 @@ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Excep * and the Boolean literals * provided using with assumptions. */ - public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception + public void assertAndTrack(BoolExpr constraint, BoolExpr p) { getContext().checkContextMatch(constraint); getContext().checkContextMatch(p); @@ -174,7 +174,7 @@ public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception * * @throws Z3Exception **/ - public int getNumAssertions() throws Z3Exception + public int getNumAssertions() { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); @@ -186,7 +186,7 @@ public int getNumAssertions() throws Z3Exception * * @throws Z3Exception **/ - public BoolExpr[] getAssertions() throws Z3Exception + public BoolExpr[] getAssertions() { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); @@ -204,7 +204,7 @@ public BoolExpr[] getAssertions() throws Z3Exception * @see getUnsatCore * @see getProof **/ - public Status check(Expr... assumptions) throws Z3Exception + public Status check(Expr... assumptions) { Z3_lbool r; if (assumptions == null) @@ -232,7 +232,7 @@ public Status check(Expr... assumptions) throws Z3Exception * @see getUnsatCore * @see getProof **/ - public Status check() throws Z3Exception + public Status check() { return check((Expr[]) null); } @@ -246,7 +246,7 @@ public Status check() throws Z3Exception * * @throws Z3Exception **/ - public Model getModel() throws Z3Exception + public Model getModel() { long x = Native.solverGetModel(getContext().nCtx(), getNativeObject()); if (x == 0) @@ -264,7 +264,7 @@ public Model getModel() throws Z3Exception * * @throws Z3Exception **/ - public Expr getProof() throws Z3Exception + public Expr getProof() { long x = Native.solverGetProof(getContext().nCtx(), getNativeObject()); if (x == 0) @@ -282,7 +282,7 @@ public Expr getProof() throws Z3Exception * * @throws Z3Exception **/ - public Expr[] getUnsatCore() throws Z3Exception + public Expr[] getUnsatCore() { ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore( @@ -298,7 +298,7 @@ public Expr[] getUnsatCore() throws Z3Exception * A brief justification of why the last call to {@code Check} returned * {@code UNKNOWN}. **/ - public String getReasonUnknown() throws Z3Exception + public String getReasonUnknown() { return Native.solverGetReasonUnknown(getContext().nCtx(), getNativeObject()); @@ -309,7 +309,7 @@ public String getReasonUnknown() throws Z3Exception * * @throws Z3Exception **/ - public Statistics getStatistics() throws Z3Exception + public Statistics getStatistics() { return new Statistics(getContext(), Native.solverGetStatistics( getContext().nCtx(), getNativeObject())); @@ -330,18 +330,18 @@ public String toString() } } - Solver(Context ctx, long obj) throws Z3Exception + Solver(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getSolverDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getSolverDRQ().add(o); super.decRef(o); diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index e1cbbea7c17..46e349cc7ab 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -58,7 +58,7 @@ public int hashCode() /** * Returns a unique identifier for the sort. **/ - public int getId() throws Z3Exception + public int getId() { return Native.getSortId(getContext().nCtx(), getNativeObject()); } @@ -66,7 +66,7 @@ public int getId() throws Z3Exception /** * The kind of the sort. **/ - public Z3_sort_kind getSortKind() throws Z3Exception + public Z3_sort_kind getSortKind() { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), getNativeObject())); @@ -75,7 +75,7 @@ public Z3_sort_kind getSortKind() throws Z3Exception /** * The name of the sort **/ - public Symbol getName() throws Z3Exception + public Symbol getName() { return Symbol.create(getContext(), Native.getSortName(getContext().nCtx(), getNativeObject())); @@ -98,12 +98,12 @@ public String toString() /** * Sort constructor **/ - Sort(Context ctx, long obj) throws Z3Exception + Sort(Context ctx, long obj) { super(ctx, obj); } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST .toInt()) @@ -111,7 +111,7 @@ void checkNativeObject(long obj) throws Z3Exception super.checkNativeObject(obj); } - static Sort create(Context ctx, long obj) throws Z3Exception + static Sort create(Context ctx, long obj) { Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj)); switch (sk) diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index aa909b9bd62..de5a52ebb5b 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -70,7 +70,7 @@ public boolean isDouble() * * @throws Z3Exception **/ - public String getValueString() throws Z3Exception + public String getValueString() { if (isUInt()) return Integer.toString(m_int); @@ -131,7 +131,7 @@ public String toString() /** * The number of statistical data. **/ - public int size() throws Z3Exception + public int size() { return Native.statsSize(getContext().nCtx(), getNativeObject()); } @@ -141,7 +141,7 @@ public int size() throws Z3Exception * * @throws Z3Exception **/ - public Entry[] getEntries() throws Z3Exception + public Entry[] getEntries() { int n = size(); @@ -166,7 +166,7 @@ else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) /** * The statistical counters. **/ - public String[] getKeys() throws Z3Exception + public String[] getKeys() { int n = size(); String[] res = new String[n]; @@ -182,7 +182,7 @@ public String[] getKeys() throws Z3Exception * * @throws Z3Exception **/ - public Entry get(String key) throws Z3Exception + public Entry get(String key) { int n = size(); Entry[] es = getEntries(); @@ -192,18 +192,18 @@ public Entry get(String key) throws Z3Exception return null; } - Statistics(Context ctx, long obj) throws Z3Exception + Statistics(Context ctx, long obj) { super(ctx, obj); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getStatisticsDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getStatisticsDRQ().add(o); super.decRef(o); diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 122c7765f9b..efbd3a9d275 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -29,22 +29,22 @@ public class StringSymbol extends Symbol * Remarks: Throws an exception if the * symbol is not of string kind. **/ - public String getString() throws Z3Exception + public String getString() { return Native.getSymbolString(getContext().nCtx(), getNativeObject()); } - StringSymbol(Context ctx, long obj) throws Z3Exception + StringSymbol(Context ctx, long obj) { super(ctx, obj); } - StringSymbol(Context ctx, String s) throws Z3Exception + StringSymbol(Context ctx, String s) { super(ctx, Native.mkStringSymbol(ctx.nCtx(), s)); } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL .toInt()) diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 856c9b57e82..6f12dda383b 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -27,7 +27,7 @@ public class Symbol extends Z3Object /** * The kind of the symbol (int or string) **/ - protected Z3_symbol_kind getKind() throws Z3Exception + protected Z3_symbol_kind getKind() { return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(), getNativeObject())); @@ -36,7 +36,7 @@ protected Z3_symbol_kind getKind() throws Z3Exception /** * Indicates whether the symbol is of Int kind **/ - public boolean isIntSymbol() throws Z3Exception + public boolean isIntSymbol() { return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL; } @@ -44,7 +44,7 @@ public boolean isIntSymbol() throws Z3Exception /** * Indicates whether the symbol is of string kind. **/ - public boolean isStringSymbol() throws Z3Exception + public boolean isStringSymbol() { return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL; } @@ -72,12 +72,12 @@ else if (isStringSymbol()) /** * Symbol constructor **/ - protected Symbol(Context ctx, long obj) throws Z3Exception + protected Symbol(Context ctx, long obj) { super(ctx, obj); } - static Symbol create(Context ctx, long obj) throws Z3Exception + static Symbol create(Context ctx, long obj) { switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj))) { diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 65404a927bf..81d88653710 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -29,7 +29,7 @@ public class Tactic extends Z3Object /** * A string containing a description of parameters accepted by the tactic. **/ - public String getHelp() throws Z3Exception + public String getHelp() { return Native.tacticGetHelp(getContext().nCtx(), getNativeObject()); } @@ -38,7 +38,7 @@ public String getHelp() throws Z3Exception * Retrieves parameter descriptions for Tactics. * @throws Z3Exception **/ - public ParamDescrs getParameterDescriptions() throws Z3Exception + public ParamDescrs getParameterDescriptions() { return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext() .nCtx(), getNativeObject())); @@ -48,7 +48,7 @@ public ParamDescrs getParameterDescriptions() throws Z3Exception * Execute the tactic over the goal. * @throws Z3Exception **/ - public ApplyResult apply(Goal g) throws Z3Exception + public ApplyResult apply(Goal g) { return apply(g, null); } @@ -57,7 +57,7 @@ public ApplyResult apply(Goal g) throws Z3Exception * Execute the tactic over the goal. * @throws Z3Exception **/ - public ApplyResult apply(Goal g, Params p) throws Z3Exception + public ApplyResult apply(Goal g, Params p) { getContext().checkContextMatch(g); if (p == null) @@ -77,28 +77,28 @@ public ApplyResult apply(Goal g, Params p) throws Z3Exception * @see Context#mkSolver(Tactic) * @throws Z3Exception **/ - public Solver getSolver() throws Z3Exception + public Solver getSolver() { return getContext().mkSolver(this); } - Tactic(Context ctx, long obj) throws Z3Exception + Tactic(Context ctx, long obj) { super(ctx, obj); } - Tactic(Context ctx, String name) throws Z3Exception + Tactic(Context ctx, String name) { super(ctx, Native.mkTactic(ctx.nCtx(), name)); } - void incRef(long o) throws Z3Exception + void incRef(long o) { getContext().getTacticDRQ().incAndClear(getContext(), o); super.incRef(o); } - void decRef(long o) throws Z3Exception + void decRef(long o) { getContext().getTacticDRQ().add(o); super.decRef(o); diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 87572b9ee99..1594b874ddc 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -26,7 +26,7 @@ public class TupleSort extends Sort * The constructor function of the tuple. * @throws Z3Exception **/ - public FuncDecl mkDecl() throws Z3Exception + public FuncDecl mkDecl() { return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext() @@ -36,7 +36,7 @@ public FuncDecl mkDecl() throws Z3Exception /** * The number of fields in the tuple. **/ - public int getNumFields() throws Z3Exception + public int getNumFields() { return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject()); } @@ -45,7 +45,7 @@ public int getNumFields() throws Z3Exception * The field declarations. * @throws Z3Exception **/ - public FuncDecl[] getFieldDecls() throws Z3Exception + public FuncDecl[] getFieldDecls() { int n = getNumFields(); @@ -57,7 +57,7 @@ public FuncDecl[] getFieldDecls() throws Z3Exception } TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames, - Sort[] fieldSorts) throws Z3Exception + Sort[] fieldSorts) { super(ctx, 0); diff --git a/src/api/java/UninterpretedSort.java b/src/api/java/UninterpretedSort.java index 07e4707f50b..7f742749321 100644 --- a/src/api/java/UninterpretedSort.java +++ b/src/api/java/UninterpretedSort.java @@ -22,12 +22,12 @@ **/ public class UninterpretedSort extends Sort { - UninterpretedSort(Context ctx, long obj) throws Z3Exception + UninterpretedSort(Context ctx, long obj) { super(ctx, obj); } - UninterpretedSort(Context ctx, Symbol s) throws Z3Exception + UninterpretedSort(Context ctx, Symbol s) { super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.getNativeObject())); } diff --git a/src/api/java/Z3Exception.java b/src/api/java/Z3Exception.java index 2522db6274f..a27e400489a 100644 --- a/src/api/java/Z3Exception.java +++ b/src/api/java/Z3Exception.java @@ -22,7 +22,7 @@ * The exception base class for error reporting from Z3 **/ @SuppressWarnings("serial") -public class Z3Exception extends Exception +public class Z3Exception extends RuntimeException { /** * Constructor. diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 9b39a3e2f04..877e22cac1c 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -26,7 +26,7 @@ public class Z3Object extends IDisposable /** * Finalizer. **/ - protected void finalize() throws Z3Exception + protected void finalize() { dispose(); } @@ -34,7 +34,7 @@ protected void finalize() throws Z3Exception /** * Disposes of the underlying native Z3 object. **/ - public void dispose() throws Z3Exception + public void dispose() { if (m_n_obj != 0) { @@ -58,7 +58,7 @@ public void dispose() throws Z3Exception m_ctx = ctx; } - Z3Object(Context ctx, long obj) throws Z3Exception + Z3Object(Context ctx, long obj) { ctx.m_refCount++; m_ctx = ctx; @@ -66,15 +66,15 @@ public void dispose() throws Z3Exception m_n_obj = obj; } - void incRef(long o) throws Z3Exception + void incRef(long o) { } - void decRef(long o) throws Z3Exception + void decRef(long o) { } - void checkNativeObject(long obj) throws Z3Exception + void checkNativeObject(long obj) { } @@ -83,7 +83,7 @@ long getNativeObject() return m_n_obj; } - void setNativeObject(long value) throws Z3Exception + void setNativeObject(long value) { if (value != 0) {