From 7fe9ad5cb4a7829374e04f318d8b1b7bfd8b5b21 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 8 Jan 2015 17:22:02 +0000 Subject: [PATCH] Java FPA API overhaul Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 20 ++++++++++---------- src/api/java/AST.java | 12 ++++-------- src/api/java/ArithExpr.java | 5 ----- src/api/java/ArrayExpr.java | 5 ----- src/api/java/BitVecExpr.java | 5 ----- src/api/java/BoolExpr.java | 8 -------- src/api/java/Context.java | 6 +----- src/api/java/DatatypeExpr.java | 5 ----- src/api/java/EnumSort.java | 2 +- src/api/java/Expr.java | 15 +-------------- src/api/java/IntExpr.java | 5 ----- src/api/java/ListSort.java | 2 +- src/api/java/Quantifier.java | 4 ++-- src/api/java/RealExpr.java | 5 ----- src/api/java/Sort.java | 13 ++++--------- src/api/java/TupleSort.java | 2 +- 16 files changed, 25 insertions(+), 89 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 878ec4693..af8662700 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2212,29 +2212,29 @@ class JavaExample { System.out.println("FloatingPointExample2"); Log.append("FloatingPointExample2"); - FPSort double_sort = ctx.mkFPSort(11, 53); FPRMSort rm_sort = ctx.mkFPRoundingModeSort(); FPRMExpr rm = (FPRMExpr)ctx.mkConst(ctx.mkSymbol("rm"), rm_sort); BitVecExpr x = (BitVecExpr)ctx.mkConst(ctx.mkSymbol("x"), ctx.mkBitVecSort(64)); - RealExpr real_val = ctx.mkReal(42); + FPExpr y = (FPExpr)ctx.mkConst(ctx.mkSymbol("y"), double_sort); FPExpr fp_val = ctx.mkFP(42, double_sort); - - BoolExpr c1 = ctx.mkEq(x, ctx.mkFPToIEEEBV(fp_val)); - BoolExpr c2 = ctx.mkEq(x, ctx.mkBV(42, 64)); - BoolExpr c3 = ctx.mkEq(fp_val, ctx.mkFPToFP(rm, real_val, double_sort)); - BoolExpr c4 = ctx.mkAnd(c1, c2); - System.out.println("c3 = " + c3); + + BoolExpr c1 = ctx.mkEq(y, fp_val); + BoolExpr c2 = ctx.mkEq(x, ctx.mkFPToBV(rm, y, 64, false)); + BoolExpr c3 = ctx.mkEq(x, ctx.mkBV(42, 64)); + BoolExpr c4 = ctx.mkEq(ctx.mkNumeral(42, ctx.getRealSort()), ctx.mkFPToReal(fp_val)); + BoolExpr c5 = ctx.mkAnd(c1, c2, c3, c4); + System.out.println("c5 = " + c5); /* Generic solver */ Solver s = ctx.mkSolver(); - s.add(c3); + s.add(c5); if (s.check() != Status.SATISFIABLE) throw new TestFailedException(); - System.out.println("OK, model: " + s.getModel().toString()); + System.out.println("OK, model: " + s.getModel().toString()); } public static void main(String[] args) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 579d4b24d..5bea58054 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -213,10 +213,8 @@ public class AST extends Z3Object void incRef(long o) throws Z3Exception { // Console.WriteLine("AST IncRef()"); - if (getContext() == null) - throw new Z3Exception("inc() called on null context"); - if (o == 0) - throw new Z3Exception("inc() called on null AST"); + if (getContext() == null || o == 0) + return; getContext().ast_DRQ().incAndClear(getContext(), o); super.incRef(o); } @@ -224,10 +222,8 @@ public class AST extends Z3Object void decRef(long o) throws Z3Exception { // Console.WriteLine("AST DecRef()"); - if (getContext() == null) - throw new Z3Exception("dec() called on null context"); - if (o == 0) - throw new Z3Exception("dec() called on null AST"); + if (getContext() == null || o == 0) + return; getContext().ast_DRQ().add(o); super.decRef(o); } diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java index 83ec35d01..97873f0b0 100644 --- a/src/api/java/ArithExpr.java +++ b/src/api/java/ArithExpr.java @@ -25,11 +25,6 @@ public class ArithExpr extends Expr /** * Constructor for ArithExpr **/ - protected ArithExpr(Context ctx) - { - super(ctx); - } - ArithExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index 2d5a5a273..2985d19a2 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -26,11 +26,6 @@ public class ArrayExpr extends Expr /** * Constructor for ArrayExpr **/ - protected ArrayExpr(Context ctx) - { - super(ctx); - } - ArrayExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index 24b1cfdf3..a7c704497 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -35,11 +35,6 @@ public class BitVecExpr extends Expr /** * Constructor for BitVecExpr **/ - BitVecExpr(Context ctx) - { - super(ctx); - } - BitVecExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 99453496a..8f9d10d18 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -22,14 +22,6 @@ package com.microsoft.z3; **/ public class BoolExpr extends Expr { - /** - * Constructor for BoolExpr - **/ - protected BoolExpr(Context ctx) - { - super(ctx); - } - /** * Constructor for BoolExpr * @throws Z3Exception diff --git a/src/api/java/Context.java b/src/api/java/Context.java index cd3b9bebd..cfbd7c2c8 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -504,14 +504,10 @@ public class Context extends IDisposable **/ public Expr mkConst(Symbol name, Sort range) throws Z3Exception { - checkContextMatch(name); checkContextMatch(range); - return Expr.create( - this, - Native.mkConst(nCtx(), name.getNativeObject(), - range.getNativeObject())); + return Expr.create(this, Native.mkConst(nCtx(), name.getNativeObject(), range.getNativeObject())); } /** diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java index 806ceacab..d4612e6ff 100644 --- a/src/api/java/DatatypeExpr.java +++ b/src/api/java/DatatypeExpr.java @@ -25,11 +25,6 @@ public class DatatypeExpr extends Expr /** * Constructor for DatatypeExpr **/ - protected DatatypeExpr(Context ctx) - { - super(ctx); - } - DatatypeExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index 9715b9a97..51bdfe0e8 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -60,7 +60,7 @@ public class EnumSort extends Sort EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception { - super(ctx); + super(ctx, 0); int n = enumNames.length; long[] n_constdecls = new long[n]; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 4bd522b51..886c69f08 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2092,24 +2092,12 @@ public class Expr extends AST return Native.getIndexValue(getContext().nCtx(), getNativeObject()); } - /** - * Constructor for Expr - **/ - protected Expr(Context ctx) - { - super(ctx); - { - } - } - /** * Constructor for Expr **/ protected Expr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); - { - } } void checkNativeObject(long obj) throws Z3Exception @@ -2135,8 +2123,7 @@ public class Expr extends AST if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) return new Quantifier(ctx, obj); long s = Native.getSort(ctx.nCtx(), obj); - Z3_sort_kind sk = Z3_sort_kind - .fromInt(Native.getSortKind(ctx.nCtx(), s)); + Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), s)); if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index 2e90c3cbf..de3ae222a 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -25,11 +25,6 @@ public class IntExpr extends ArithExpr /** * Constructor for IntExpr **/ - protected IntExpr(Context ctx) throws Z3Exception - { - super(ctx); - } - IntExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index 52cb1a179..a7ad0403b 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -88,7 +88,7 @@ public class ListSort extends Sort ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception { - super(ctx); + super(ctx, 0); Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr(); Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr(); diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index e9aeefcca..58245d723 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -149,7 +149,7 @@ public class Quantifier extends BoolExpr Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception { - super(ctx); + super(ctx, 0); getContext().checkContextMatch(patterns); getContext().checkContextMatch(noPatterns); @@ -185,7 +185,7 @@ public class Quantifier extends BoolExpr int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception { - super(ctx); + super(ctx, 0); getContext().checkContextMatch(noPatterns); getContext().checkContextMatch(patterns); diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index 6188e2999..c699e13e2 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -25,11 +25,6 @@ public class RealExpr extends ArithExpr /** * Constructor for RealExpr **/ - protected RealExpr(Context ctx) - { - super(ctx); - } - RealExpr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 7d89428c6..fa556e67f 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -98,18 +98,9 @@ public class Sort extends AST /** * Sort constructor **/ - protected Sort(Context ctx) throws Z3Exception - { - super(ctx); - { - } - } - Sort(Context ctx, long obj) throws Z3Exception { super(ctx, obj); - { - } } void checkNativeObject(long obj) throws Z3Exception @@ -143,6 +134,10 @@ public class Sort extends AST return new FiniteDomainSort(ctx, obj); case Z3_RELATION_SORT: return new RelationSort(ctx, obj); + case Z3_FLOATING_POINT_SORT: + return new FPSort(ctx, obj); + case Z3_ROUNDING_MODE_SORT: + return new FPRMSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 523f8d676..87572b9ee 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -59,7 +59,7 @@ public class TupleSort extends Sort TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception { - super(ctx); + super(ctx, 0); Native.LongPtr t = new Native.LongPtr(); setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),