diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index d96553c19..5d56a474b 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -159,7 +159,7 @@ class JavaExample Sort t = f.Range(); Sort[] dom = f.Domain(); - if (dom.length != 2 || !t.Equals(dom[0]) || !t.Equals(dom[1])) + if (dom.length != 2 || !t.equals(dom[0]) || !t.equals(dom[1])) { System.out.println(Integer.toString(dom.length) + " " + dom[0].toString() + " " + dom[1].toString() + " " @@ -700,7 +700,7 @@ class JavaExample System.out.println(q2); } - System.out.println(q1.Equals(q2)); + System.out.println(q1.equals(q2)); } // / Prove that f(x, y) = f(w, v) implies y = v when diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5edace6cb..d96c4a0ec 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -990,10 +990,13 @@ class JavaDLLComponent(Component): else: out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(SO_EXT)\n') out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name) - # for java_file in get_java_files(self.src_dir): - # out.write('%s ' % java_file) - # for java_file in get_java_files((self.src_dir + "/%s/enumerations") % subdir): - # out.write('%s ' % java_file) + deps = '' + for jfile in get_java_files(self.src_dir): + deps += ('%s/%s ' % (self.to_src_dir, jfile)) + for jfile in get_java_files((self.src_dir + "/enumerations")): + deps += ('%s/enumerations/%s ' % (self.to_src_dir, jfile)) + if IS_WINDOWS: deps = deps.replace('/', '\\') + out.write(deps) out.write('\n') t = ('\t%s %s/enumerations/*.java -d api/java/classes\n' % (JAVAC, self.to_src_dir)) if IS_WINDOWS: t = t.replace('/','\\') @@ -1103,10 +1106,12 @@ class JavaExampleComponent(ExampleComponent): if JAVA_ENABLED: pkg = get_component(JAVA_COMPONENT).package_name + '.jar' out.write('_ex_%s: %s' % (self.name, pkg)) - # for javafile in get_java_files(self.ex_dir): - # out.write(' ') - # out.write('%s/%s' % (self.to_ex_dir, javafile)) - out.write('\n') + deps = '' + for jfile in get_java_files(self.ex_dir): + out.write(' %s/%s' % (self.to_ex_dir, jfile)) + if IS_WINDOWS: + deps = deps.replace('/', '\\') + out.write('%s\n' % deps) out.write('\t%s -cp %s ' % (JAVAC, pkg)) win_ex_dir = self.to_ex_dir for javafile in get_java_files(self.ex_dir): diff --git a/scripts/update_api.py b/scripts/update_api.py index e55a3a356..354f5728f 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -489,18 +489,19 @@ def mk_java(): java_native = open(java_nativef, 'w') java_native.write('// Automatically generated file\n') java_native.write('package %s;\n' % get_component('java').package_name) + java_native.write('import %s.enumerations.*;\n' % get_component('java').package_name) java_native.write('public final class Native {\n') java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') java_native.write(' public static class errorHandler { public long ptr; }\n') - if IS_WINDOWS: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) else: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name + java_native.write('\n\n') for name, result, params in _dotnet_decls: - java_native.write(' public static native %s %s(' % (type2java(result), java_method_name(name))) + java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) first = True i = 0; for param in params: @@ -511,12 +512,46 @@ def mk_java(): java_native.write('%s a%d' % (param2java(param), i)) i = i + 1 java_native.write(');\n') - java_native.write(' public static void main(String[] args) {\n') - java_native.write(' IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();\n') - java_native.write(' getVersion(major, minor, build, revision);\n') - java_native.write(' System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);\n') - java_native.write(' }\n') - java_native.write('}\n'); + java_native.write('\n\n') + # Exception wrappers + for name, result, params in _dotnet_decls: + java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) + first = True + i = 0; + for param in params: + if first: + first = False + else: + java_native.write(', ') + java_native.write('%s a%d' % (param2java(param), i)) + i = i + 1 + java_native.write(')') + if len(params) > 0 and param_type(params[0]) == CONTEXT: + java_native.write(' throws Z3Exception') + java_native.write('\n') + java_native.write(' {\n') + java_native.write(' ') + if result != VOID: + java_native.write('%s res = ' % type2java(result)) + java_native.write('INTERNAL%s(' % (java_method_name(name))) + first = True + i = 0; + for param in params: + if first: + first = False + else: + java_native.write(', ') + java_native.write('a%d' % i) + i = i + 1 + java_native.write(');\n') + if len(params) > 0 and param_type(params[0]) == CONTEXT: + java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + if result != VOID: + java_native.write(' return res;\n') + java_native.write(' }\n\n') + java_native.write('}\n') java_wrapper = open(java_wrapperf, 'w') java_wrapper.write('// Automatically generated file\n') java_wrapper.write('#include\n') @@ -544,7 +579,7 @@ def mk_java(): java_wrapper.write(' delete [] NEW; \n\n') pkg_str = get_component('java').package_name.replace('.', '_') for name, result, params in _dotnet_decls: - java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) + java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0; for param in params: java_wrapper.write(', ') @@ -629,7 +664,7 @@ def mk_java(): if result == STRING: java_wrapper.write(' return jenv->NewStringUTF(result);\n') elif result != VOID: - java_wrapper.write(' return (%s) result;\n' % type2javaw(result)) + java_wrapper.write(' return (%s) result;\n' % type2javaw(result)) java_wrapper.write('}\n') java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('}\n') diff --git a/src/api/java/AST.java b/src/api/java/AST.java index f30e67673..fbefbf5e2 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -13,216 +13,222 @@ import com.microsoft.z3.enumerations.*; **/ public class AST extends Z3Object { - /** - * Comparison operator. An AST An - * AST - * - * @return True if and are from - * the same context and represent the same sort; false otherwise. - **/ - /* Overloaded operators are not translated. */ + /** + * Comparison operator. An AST An + * AST + * + * @return True if and are from + * the same context and represent the same sort; false otherwise. + **/ + /* Overloaded operators are not translated. */ - /** - * Comparison operator. An AST An - * AST - * - * @return True if and are not - * from the same context or represent different sorts; false - * otherwise. - **/ - /* Overloaded operators are not translated. */ + /** + * Comparison operator. An AST An + * AST + * + * @return True if and are not + * from the same context or represent different sorts; false + * otherwise. + **/ + /* Overloaded operators are not translated. */ - /** - * Object comparison. - **/ - public boolean Equals(Object o) - { - AST casted = (AST) o; - if (casted == null) - return false; - return this == casted; - } + /** + * Object comparison. + **/ + public boolean equals(Object o) + { + AST casted = (AST) o; + if (casted == null) + return false; + return this == casted; + } - /** - * Object Comparison. Another AST - * - * @return Negative if the object should be sorted before , positive if after else zero. - **/ - public int CompareTo(Object other) throws Z3Exception - { - if (other == null) - return 1; - AST oAST = (AST) other; - if (oAST == null) - return 1; - else - { - if (Id() < oAST.Id()) - return -1; - else if (Id() > oAST.Id()) - return +1; - else - return 0; - } - } + /** + * Object Comparison. Another AST + * + * @return Negative if the object should be sorted before , positive if after else zero. + **/ + public int compareTo(Object other) throws Z3Exception + { + if (other == null) + return 1; + AST oAST = (AST) other; + if (oAST == null) + return 1; + else + { + if (Id() < oAST.Id()) + return -1; + else if (Id() > oAST.Id()) + return +1; + else + return 0; + } + } - /** - * The AST's hash code. - * - * @return A hash code - **/ - public int GetHashCode() throws Z3Exception - { - return (int) Native.getAstHash(Context().nCtx(), NativeObject()); - } + /** + * The AST's hash code. + * + * @return A hash code + **/ + public int GetHashCode() throws Z3Exception + { + return (int) Native.getAstHash(Context().nCtx(), NativeObject()); + } - /** - * A unique identifier for the AST (unique among all ASTs). - **/ - public int Id() throws Z3Exception - { - return Native.getAstId(Context().nCtx(), NativeObject()); - } + /** + * A unique identifier for the AST (unique among all ASTs). + **/ + public int Id() throws Z3Exception + { + return Native.getAstId(Context().nCtx(), NativeObject()); + } - /** - * Translates (copies) the AST to the Context . A context - * - * @return A copy of the AST which is associated with - **/ - public AST Translate(Context ctx) throws Z3Exception - { + /** + * Translates (copies) the AST to the Context . A context + * + * @return A copy of the AST which is associated with + **/ + public AST Translate(Context ctx) throws Z3Exception + { - if (Context() == ctx) - return this; - else - return new AST(ctx, Native.translate(Context().nCtx(), - NativeObject(), ctx.nCtx())); - } + if (Context() == ctx) + return this; + else + return new AST(ctx, Native.translate(Context().nCtx(), + NativeObject(), ctx.nCtx())); + } - /** - * The kind of the AST. - **/ - public Z3_ast_kind ASTKind() - { - return Z3_ast_kind.fromInt(Native.getAstKind(Context().nCtx(), - NativeObject())); - } + /** + * The kind of the AST. + **/ + public Z3_ast_kind ASTKind() throws Z3Exception + { + return Z3_ast_kind.fromInt(Native.getAstKind(Context().nCtx(), + NativeObject())); + } - /** - * Indicates whether the AST is an Expr - **/ - public boolean IsExpr() throws Z3Exception - { - switch (ASTKind()) - { - case Z3_APP_AST: - case Z3_NUMERAL_AST: - case Z3_QUANTIFIER_AST: - case Z3_VAR_AST: - return true; - default: - return false; - } - } + /** + * Indicates whether the AST is an Expr + **/ + public boolean IsExpr() throws Z3Exception + { + switch (ASTKind()) + { + case Z3_APP_AST: + case Z3_NUMERAL_AST: + case Z3_QUANTIFIER_AST: + case Z3_VAR_AST: + return true; + default: + return false; + } + } - /** - * Indicates whether the AST is a BoundVariable - **/ - public boolean IsVar() throws Z3Exception - { - return this.ASTKind() == Z3_ast_kind.Z3_VAR_AST; - } + /** + * Indicates whether the AST is a BoundVariable + **/ + public boolean IsVar() throws Z3Exception + { + return this.ASTKind() == Z3_ast_kind.Z3_VAR_AST; + } - /** - * Indicates whether the AST is a Quantifier - **/ - public boolean IsQuantifier() throws Z3Exception - { - return this.ASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST; - } + /** + * Indicates whether the AST is a Quantifier + **/ + public boolean IsQuantifier() throws Z3Exception + { + return this.ASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST; + } - /** - * Indicates whether the AST is a Sort - **/ - public boolean IsSort() throws Z3Exception - { - return this.ASTKind() == Z3_ast_kind.Z3_SORT_AST; - } + /** + * Indicates whether the AST is a Sort + **/ + public boolean IsSort() throws Z3Exception + { + return this.ASTKind() == Z3_ast_kind.Z3_SORT_AST; + } - /** - * Indicates whether the AST is a FunctionDeclaration - **/ - public boolean IsFuncDecl() throws Z3Exception - { - return this.ASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST; - } + /** + * Indicates whether the AST is a FunctionDeclaration + **/ + public boolean IsFuncDecl() throws Z3Exception + { + return this.ASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST; + } - /** - * A string representation of the AST. - **/ - public String toString() - { - return Native.astToString(Context().nCtx(), NativeObject()); - } + /** + * A string representation of the AST. + **/ + public String toString() + { + try + { + return Native.astToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - /** - * A string representation of the AST in s-expression notation. - **/ - public String SExpr() throws Z3Exception - { - return Native.astToString(Context().nCtx(), NativeObject()); - } + /** + * A string representation of the AST in s-expression notation. + **/ + public String SExpr() throws Z3Exception + { + return Native.astToString(Context().nCtx(), NativeObject()); + } - AST(Context ctx) - { - super(ctx); - } + AST(Context ctx) + { + super(ctx); + } - AST(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + AST(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - void IncRef(long o) throws Z3Exception - { - // Console.WriteLine("AST IncRef()"); - if (Context() == null) - throw new Z3Exception("inc() called on null context"); - if (o == 0) - throw new Z3Exception("inc() called on null AST"); - Context().AST_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } + void IncRef(long o) throws Z3Exception + { + // Console.WriteLine("AST IncRef()"); + if (Context() == null) + throw new Z3Exception("inc() called on null context"); + if (o == 0) + throw new Z3Exception("inc() called on null AST"); + Context().AST_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - void DecRef(long o) throws Z3Exception - { - // Console.WriteLine("AST DecRef()"); - if (Context() == null) - throw new Z3Exception("dec() called on null context"); - if (o == 0) - throw new Z3Exception("dec() called on null AST"); - Context().AST_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + // Console.WriteLine("AST DecRef()"); + if (Context() == null) + throw new Z3Exception("dec() called on null context"); + if (o == 0) + throw new Z3Exception("dec() called on null AST"); + Context().AST_DRQ().Add(o); + super.DecRef(o); + } - static AST Create(Context ctx, long obj) throws Z3Exception - { - switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj))) - { - case Z3_FUNC_DECL_AST: - return new FuncDecl(ctx, obj); - case Z3_QUANTIFIER_AST: - return new Quantifier(ctx, obj); - case Z3_SORT_AST: - return Sort.Create(ctx, obj); - case Z3_APP_AST: - case Z3_NUMERAL_AST: - case Z3_VAR_AST: - return Expr.Create(ctx, obj); - default: - throw new Z3Exception("Unknown AST kind"); - } - } + static AST Create(Context ctx, long obj) throws Z3Exception + { + switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj))) + { + case Z3_FUNC_DECL_AST: + return new FuncDecl(ctx, obj); + case Z3_QUANTIFIER_AST: + return new Quantifier(ctx, obj); + case Z3_SORT_AST: + return Sort.Create(ctx, obj); + case Z3_APP_AST: + case Z3_NUMERAL_AST: + case Z3_VAR_AST: + return Expr.Create(ctx, obj); + default: + throw new Z3Exception("Unknown AST kind"); + } + } } diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index 720e90a4c..f66c54006 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; public class ASTDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.incRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.incRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.decRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.decRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index a2d334b0e..c40c4c6b8 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -11,106 +11,114 @@ package com.microsoft.z3; **/ class ASTMap extends Z3Object { - /** - * Checks whether the map contains the key . An AST - * - * @return True if is a key in the map, false - * otherwise. - **/ - public boolean Contains(AST k) - { + /** + * Checks whether the map contains the key . An AST + * + * @return True if is a key in the map, false + * otherwise. + **/ + public boolean Contains(AST k) throws Z3Exception + { - return Native.astMapContains(Context().nCtx(), NativeObject(), - k.NativeObject()); - } + return Native.astMapContains(Context().nCtx(), NativeObject(), + k.NativeObject()); + } - /** - * Finds the value associated with the key . - * This function signs an error when is not a key in - * the map. An AST - * @throws Z3Exception - **/ - public AST Find(AST k) throws Z3Exception - { - return new AST(Context(), Native.astMapFind(Context().nCtx(), - NativeObject(), k.NativeObject())); - } + /** + * Finds the value associated with the key . + * This function signs an error when is not a key in + * the map. An AST + * + * @throws Z3Exception + **/ + public AST Find(AST k) throws Z3Exception + { + return new AST(Context(), Native.astMapFind(Context().nCtx(), + NativeObject(), k.NativeObject())); + } - /** - * Stores or replaces a new key/value pair in the map. The - * key AST The value AST - **/ - public void Insert(AST k, AST v) - { + /** + * Stores or replaces a new key/value pair in the map. The + * key AST The value AST + **/ + public void Insert(AST k, AST v) throws Z3Exception + { - Native.astMapInsert(Context().nCtx(), NativeObject(), k.NativeObject(), - v.NativeObject()); - } + Native.astMapInsert(Context().nCtx(), NativeObject(), k.NativeObject(), + v.NativeObject()); + } - /** - * Erases the key from the map. An - * AST - **/ - public void Erase(AST k) - { + /** + * Erases the key from the map. An + * AST + **/ + public void Erase(AST k) throws Z3Exception + { - Native.astMapErase(Context().nCtx(), NativeObject(), k.NativeObject()); - } + Native.astMapErase(Context().nCtx(), NativeObject(), k.NativeObject()); + } - /** - * Removes all keys from the map. - **/ - public void Reset() - { - Native.astMapReset(Context().nCtx(), NativeObject()); - } + /** + * Removes all keys from the map. + **/ + public void Reset() throws Z3Exception + { + Native.astMapReset(Context().nCtx(), NativeObject()); + } - /** - * The size of the map - **/ - public int Size() - { - return Native.astMapSize(Context().nCtx(), NativeObject()); - } + /** + * The size of the map + **/ + public int Size() throws Z3Exception + { + return Native.astMapSize(Context().nCtx(), NativeObject()); + } - /** - * The keys stored in the map. - * @throws Z3Exception - **/ - public ASTVector Keys() throws Z3Exception - { - return new ASTVector(Context(), Native.astMapKeys(Context().nCtx(), - NativeObject())); - } + /** + * The keys stored in the map. + * + * @throws Z3Exception + **/ + public ASTVector Keys() throws Z3Exception + { + return new ASTVector(Context(), Native.astMapKeys(Context().nCtx(), + NativeObject())); + } - /** - * Retrieves a string representation of the map. - **/ - public String toString() - { - return Native.astMapToString(Context().nCtx(), NativeObject()); - } + /** + * Retrieves a string representation of the map. + **/ + public String toString() + { + try + { + return Native.astMapToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - ASTMap(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + ASTMap(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - ASTMap(Context ctx) throws Z3Exception - { - super(ctx, Native.mkAstMap(ctx.nCtx())); - } + ASTMap(Context ctx) throws Z3Exception + { + super(ctx, Native.mkAstMap(ctx.nCtx())); + } - void IncRef(long o) throws Z3Exception - { - Context().ASTMap_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } + void IncRef(long o) throws Z3Exception + { + Context().ASTMap_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - void DecRef(long o) throws Z3Exception - { - Context().ASTMap_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + Context().ASTMap_DRQ().Add(o); + super.DecRef(o); + } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index b93c9f4bd..0e9cf1ae7 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -11,94 +11,99 @@ package com.microsoft.z3; **/ class ASTVector extends Z3Object { - /** - * The size of the vector - **/ - public int Size() - { - return Native.astVectorSize(Context().nCtx(), NativeObject()); - } + /** + * The size of the vector + **/ + public int Size() throws Z3Exception + { + return Native.astVectorSize(Context().nCtx(), NativeObject()); + } - /** - * Retrieves the i-th object in the vector. May throw an - * IndexOutOfBoundsException when is out of - * range. Index - * - * @return An AST - * @throws Z3Exception - **/ - public AST get(int i) throws Z3Exception - { - return new AST(Context(), Native.astVectorGet(Context().nCtx(), - NativeObject(), i)); - } + /** + * Retrieves the i-th object in the vector. May throw an + * IndexOutOfBoundsException when is out of + * range. Index + * + * @return An AST + * @throws Z3Exception + **/ + public AST get(int i) throws Z3Exception + { + return new AST(Context(), Native.astVectorGet(Context().nCtx(), + NativeObject(), i)); + } - public void set(int i, AST value) - { + public void set(int i, AST value) throws Z3Exception + { - Native.astVectorSet(Context().nCtx(), NativeObject(), i, - value.NativeObject()); - } + Native.astVectorSet(Context().nCtx(), NativeObject(), i, + value.NativeObject()); + } - /** - * Resize the vector to . The new size of the vector. - **/ - public void Resize(int newSize) - { - Native.astVectorResize(Context().nCtx(), NativeObject(), newSize); - } + /** + * Resize the vector to . The new size of the vector. + **/ + public void Resize(int newSize) throws Z3Exception + { + Native.astVectorResize(Context().nCtx(), NativeObject(), newSize); + } - /** - * Add the AST to the back of the vector. The size is - * increased by 1. An AST - **/ - public void Push(AST a) - { + /** + * Add the AST to the back of the vector. The size is + * increased by 1. An AST + **/ + public void Push(AST a) throws Z3Exception + { + Native.astVectorPush(Context().nCtx(), NativeObject(), a.NativeObject()); + } - Native.astVectorPush(Context().nCtx(), NativeObject(), a.NativeObject()); - } + /** + * Translates all ASTs in the vector to . A context + * + * @return A new ASTVector + * @throws Z3Exception + **/ + public ASTVector Translate(Context ctx) throws Z3Exception + { + return new ASTVector(Context(), Native.astVectorTranslate(Context() + .nCtx(), NativeObject(), ctx.nCtx())); + } - /** - * Translates all ASTs in the vector to . A context - * - * @return A new ASTVector - * @throws Z3Exception - **/ - public ASTVector Translate(Context ctx) throws Z3Exception - { - return new ASTVector(Context(), Native.astVectorTranslate(Context() - .nCtx(), NativeObject(), ctx.nCtx())); - } + /** + * Retrieves a string representation of the vector. + **/ + public String toString() + { + try + { + return Native.astVectorToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - /** - * Retrieves a string representation of the vector. - **/ - public String toString() - { - return Native.astVectorToString(Context().nCtx(), NativeObject()); - } + ASTVector(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - ASTVector(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + ASTVector(Context ctx) throws Z3Exception + { + super(ctx, Native.mkAstVector(ctx.nCtx())); + } - ASTVector(Context ctx) throws Z3Exception - { - super(ctx, Native.mkAstVector(ctx.nCtx())); - } + void IncRef(long o) throws Z3Exception + { + Context().ASTVector_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - void IncRef(long o) throws Z3Exception - { - Context().ASTVector_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } - - void DecRef(long o) throws Z3Exception - { - Context().ASTVector_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + Context().ASTVector_DRQ().Add(o); + super.DecRef(o); + } } diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index feb8dc5ea..31267b536 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -12,64 +12,71 @@ package com.microsoft.z3; **/ public class ApplyResult extends Z3Object { - /** - * The number of Subgoals. - **/ - public int NumSubgoals() - { - return Native.applyResultGetNumSubgoals(Context().nCtx(), - NativeObject()); - } + /** + * The number of Subgoals. + **/ + public int NumSubgoals() throws Z3Exception + { + return Native.applyResultGetNumSubgoals(Context().nCtx(), + NativeObject()); + } - /** - * Retrieves the subgoals from the ApplyResult. - * @throws Z3Exception - **/ - public Goal[] Subgoals() throws Z3Exception - { - int n = NumSubgoals(); - Goal[] res = new Goal[n]; - for (int i = 0; i < n; i++) - res[i] = new Goal(Context(), Native.applyResultGetSubgoal(Context() - .nCtx(), NativeObject(), i)); - return res; - } + /** + * Retrieves the subgoals from the ApplyResult. + * + * @throws Z3Exception + **/ + public Goal[] Subgoals() throws Z3Exception + { + int n = NumSubgoals(); + Goal[] res = new Goal[n]; + for (int i = 0; i < n; i++) + res[i] = new Goal(Context(), Native.applyResultGetSubgoal(Context() + .nCtx(), NativeObject(), i)); + return res; + } - /** - * Convert a model for the subgoal into a model for the - * original goal g, that the ApplyResult was obtained from. - * - * @return A model for g - * @throws Z3Exception - **/ - public Model ConvertModel(int i, Model m) throws Z3Exception - { - return new Model(Context(), Native.applyResultConvertModel(Context() - .nCtx(), NativeObject(), i, m.NativeObject())); - } + /** + * Convert a model for the subgoal into a model for the + * original goal g, that the ApplyResult was obtained from. + * + * @return A model for g + * @throws Z3Exception + **/ + public Model ConvertModel(int i, Model m) throws Z3Exception + { + return new Model(Context(), Native.applyResultConvertModel(Context() + .nCtx(), NativeObject(), i, m.NativeObject())); + } - /** - * A string representation of the ApplyResult. - **/ - public String toString() - { - return Native.applyResultToString(Context().nCtx(), NativeObject()); - } + /** + * A string representation of the ApplyResult. + **/ + public String toString() + { + try + { + return Native.applyResultToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - ApplyResult(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + ApplyResult(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - void IncRef(long o) throws Z3Exception - { - Context().ApplyResult_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } + void IncRef(long o) throws Z3Exception + { + Context().ApplyResult_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - void DecRef(long o) throws Z3Exception - { - Context().ApplyResult_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + Context().ApplyResult_DRQ().Add(o); + super.DecRef(o); + } } diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 96d18bef1..c459e85aa 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class ApplyResultDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.applyResultIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.applyResultIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.applyResultDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.applyResultDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index 23cb3c6fd..d59074cdb 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class ASTMapDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.astMapIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.astMapIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.astMapDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.astMapDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index 4496c092e..d4b508a54 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class ASTVectorDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.astVectorIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.astVectorIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.astVectorDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.astVectorDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 10dad6423..3560d5efa 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -13,50 +13,56 @@ import java.math.BigInteger; **/ public class BitVecNum extends BitVecExpr { - /** - * Retrieve the int value. - * - * @throws Z3Exception - **/ - public int Int() throws Z3Exception - { - Native.IntPtr res = new Native.IntPtr(); - if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int"); - return res.value; - } + /** + * Retrieve the int value. + * + * @throws Z3Exception + **/ + public int Int() throws Z3Exception + { + Native.IntPtr res = new Native.IntPtr(); + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int"); + return res.value; + } - /** - * Retrieve the 64-bit int value. - * - * @throws Z3Exception - **/ - public long Long() throws Z3Exception - { - Native.LongPtr res = new Native.LongPtr(); - if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int64"); - return res.value; - } + /** + * Retrieve the 64-bit int value. + * + * @throws Z3Exception + **/ + public long Long() throws Z3Exception + { + Native.LongPtr res = new Native.LongPtr(); + if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int64"); + return res.value; + } - /** - * Retrieve the BigInteger value. - **/ - public BigInteger BigInteger() - { - return new BigInteger(this.toString()); - } + /** + * Retrieve the BigInteger value. + **/ + public BigInteger BigInteger() + { + return new BigInteger(this.toString()); + } - /** - * Returns a string representation of the numeral. - **/ - public String toString() - { - return Native.getNumeralString(Context().nCtx(), NativeObject()); - } + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + try + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - BitVecNum(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + BitVecNum(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } } diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java index e8cd0af27..58781302e 100644 --- a/src/api/java/BitVecSort.java +++ b/src/api/java/BitVecSort.java @@ -13,7 +13,7 @@ public class BitVecSort extends Sort /** * The size of the bit-vector sort. **/ - public int Size() + public int Size() throws Z3Exception { return Native.getBvSortSize(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 3ddb8664b..e267998a0 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -54,7 +54,7 @@ public class Constructor extends Z3Object /** * Destructor. **/ - protected void finalize() + protected void finalize() throws Z3Exception { Native.delConstructor(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 857ec3cf0..87b6bd4fd 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -14,7 +14,7 @@ public class ConstructorList extends Z3Object /** * Destructor. **/ - protected void finalize() + protected void finalize() throws Z3Exception { Native.delConstructorList(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index c3fbeab15..1d2f800ba 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -14,3110 +14,3116 @@ import com.microsoft.z3.enumerations.*; **/ public class Context extends IDisposable { - /** - * Constructor. - **/ - public Context() throws Z3Exception - { - super(); - m_ctx = Native.mkContextRc(0); - InitContext(); - } - - /** - * Constructor. - **/ - public Context(Map settings) throws Z3Exception - { - super(); - long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) - Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - m_ctx = Native.mkContextRc(cfg); - Native.delConfig(cfg); - InitContext(); - } - - private Context(long ctx, long refCount, Native.errorHandler errh) - { - super(); - this.m_ctx = ctx; - this.m_refCount = refCount; - this.m_n_err_handler = errh; - } - - /** - * Creates a new symbol using an integer. 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 - { - return new IntSymbol(this, i); - } - - /** - * Create a symbol using a string. - **/ - public StringSymbol MkSymbol(String name) throws Z3Exception - { - return new StringSymbol(this, name); - } - - /** - * Create an array of symbols. - **/ - Symbol[] MkSymbols(String[] names) throws Z3Exception - { - if (names == null) - return null; - Symbol[] result = new Symbol[names.length]; - for (int i = 0; i < names.length; ++i) - result[i] = MkSymbol(names[i]); - return result; - } - - private BoolSort m_boolSort = null; - private IntSort m_intSort = null; - private RealSort m_realSort = null; - - /** - * Retrieves the Boolean sort of the context. - **/ - public BoolSort BoolSort() throws Z3Exception - { - if (m_boolSort == null) - m_boolSort = new BoolSort(this); - return m_boolSort; - } - - /** - * Retrieves the Integer sort of the context. - **/ - public IntSort IntSort() throws Z3Exception - { - if (m_intSort == null) - m_intSort = new IntSort(this); - return m_intSort; - } - - /** - * Retrieves the Real sort of the context. - **/ - public RealSort RealSort() throws Z3Exception - { - if (m_realSort== null) - m_realSort = new RealSort(this); - return m_realSort; - } - - /** - * Create a new Boolean sort. - **/ - public BoolSort MkBoolSort() throws Z3Exception - { - - return new BoolSort(this); - } - - /** - * Create a new uninterpreted sort. - **/ - public UninterpretedSort MkUninterpretedSort(Symbol s) throws Z3Exception - { - - CheckContextMatch(s); - return new UninterpretedSort(this, s); - } - - /** - * Create a new uninterpreted sort. - **/ - public UninterpretedSort MkUninterpretedSort(String str) throws Z3Exception - { - - return MkUninterpretedSort(MkSymbol(str)); - } - - /** - * Create a new integer sort. - **/ - public IntSort MkIntSort() throws Z3Exception - { - - return new IntSort(this); - } - - /** - * Create a real sort. - **/ - public RealSort MkRealSort() throws Z3Exception - { - - return new RealSort(this); - } - - /** - * Create a new bit-vector sort. - **/ - public BitVecSort MkBitVecSort(int size) throws Z3Exception - { - - return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); - } - - /** - * Create a new array sort. - **/ - public ArraySort MkArraySort(Sort domain, Sort range) throws Z3Exception - { - - CheckContextMatch(domain); - CheckContextMatch(range); - return new ArraySort(this, domain, range); - } - - /** - * Create a new tuple sort. - **/ - public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, - Sort[] fieldSorts) throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(fieldNames); - CheckContextMatch(fieldSorts); - return new TupleSort(this, name, (int) fieldNames.length, fieldNames, - fieldSorts); - } - - /** - * Create a new enumeration sort. - **/ - public EnumSort MkEnumSort(Symbol name, Symbol[] enumNames) - throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(enumNames); - return new EnumSort(this, name, enumNames); - } - - /** - * Create a new enumeration sort. - **/ - public EnumSort MkEnumSort(String name, String[] enumNames) - throws Z3Exception - { - - return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames)); - } - - /** - * Create a new list sort. - **/ - public ListSort MkListSort(Symbol name, Sort elemSort) throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(elemSort); - return new ListSort(this, name, elemSort); - } - - /** - * Create a new list sort. - **/ - public ListSort MkListSort(String name, Sort elemSort) throws Z3Exception - { - - CheckContextMatch(elemSort); - return new ListSort(this, MkSymbol(name), elemSort); - } - - /** - * Create a new finite domain sort. - **/ - public FiniteDomainSort MkFiniteDomainSort(Symbol name, long size) - throws Z3Exception - { - - CheckContextMatch(name); - return new FiniteDomainSort(this, name, size); - } - - /** - * Create a new finite domain sort. - **/ - public FiniteDomainSort MkFiniteDomainSort(String name, long size) - throws Z3Exception - { - - return new FiniteDomainSort(this, MkSymbol(name), size); - } - - /** - * Create a datatype constructor. constructor - * name name of recognizer - * function. names of the constructor - * fields. field sorts, 0 if the field sort - * refers to a recursive sort. reference to - * datatype sort that is an argument to the constructor; if the - * corresponding sort reference is 0, then the value in sort_refs should be - * an index referring to one of the recursive datatypes that is - * declared. - **/ - public Constructor MkConstructor(Symbol name, Symbol recognizer, - Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) - throws Z3Exception - { - - return new Constructor(this, name, recognizer, fieldNames, sorts, - sortRefs); - } - - /** - * Create a datatype constructor. - * - * @return - **/ - public Constructor MkConstructor(String name, String recognizer, - String[] fieldNames, Sort[] sorts, int[] sortRefs) - throws Z3Exception - { - - return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), - MkSymbols(fieldNames), sorts, sortRefs); - } - - /** - * Create a new datatype sort. - **/ - public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors) - throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(constructors); - return new DatatypeSort(this, name, constructors); - } - - /** - * Create a new datatype sort. - **/ - public DatatypeSort MkDatatypeSort(String name, Constructor[] constructors) - throws Z3Exception - { - - CheckContextMatch(constructors); - return new DatatypeSort(this, MkSymbol(name), constructors); - } - - /** - * Create mutually recursive datatypes. names of - * datatype sorts list of constructors, one list per - * sort. - **/ - public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c) - throws Z3Exception - { - - CheckContextMatch(names); - int n = (int) names.length; - ConstructorList[] cla = new ConstructorList[n]; - long[] n_constr = new long[n]; - for (int i = 0; i < n; i++) - { - Constructor[] constructor = c[i]; - - CheckContextMatch(constructor); - cla[i] = new ConstructorList(this, constructor); - n_constr[i] = cla[i].NativeObject(); - } - long[] n_res = new long[n]; - Native.mkDatatypes(nCtx(), n, Symbol.ArrayToNative(names), n_res, - n_constr); - DatatypeSort[] res = new DatatypeSort[n]; - for (int i = 0; i < n; i++) - res[i] = new DatatypeSort(this, n_res[i]); - return res; - } - - /** - * Create mutually recursive data-types. - * - * @return - **/ - public DatatypeSort[] MkDatatypeSorts(String[] names, Constructor[][] c) - throws Z3Exception - { - - return MkDatatypeSorts(MkSymbols(names), c); - } - - /** - * Creates a new function declaration. - **/ - public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range) - throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(domain); - CheckContextMatch(range); - return new FuncDecl(this, name, domain, range); - } - - /** - * Creates a new function declaration. - **/ - public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range) - throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(domain); - CheckContextMatch(range); - Sort[] q = new Sort[] { domain }; - return new FuncDecl(this, name, q, range); - } - - /** - * Creates a new function declaration. - **/ - public FuncDecl MkFuncDecl(String name, Sort[] domain, Sort range) - throws Z3Exception - { - - CheckContextMatch(domain); - CheckContextMatch(range); - return new FuncDecl(this, MkSymbol(name), domain, range); - } - - /** - * Creates a new function declaration. - **/ - public FuncDecl MkFuncDecl(String name, Sort domain, Sort range) - throws Z3Exception - { - - CheckContextMatch(domain); - CheckContextMatch(range); - Sort[] q = new Sort[] { domain }; - return new FuncDecl(this, MkSymbol(name), q, range); - } - - /** - * Creates a fresh function declaration with a name prefixed with . - **/ - public FuncDecl MkFreshFuncDecl(String prefix, Sort[] domain, Sort range) - throws Z3Exception - { - - CheckContextMatch(domain); - CheckContextMatch(range); - return new FuncDecl(this, prefix, domain, range); - } - - /** - * Creates a new constant function declaration. - **/ - public FuncDecl MkConstDecl(Symbol name, Sort range) throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(range); - return new FuncDecl(this, name, null, range); - } - - /** - * Creates a new constant function declaration. - **/ - public FuncDecl MkConstDecl(String name, Sort range) throws Z3Exception - { - - CheckContextMatch(range); - return new FuncDecl(this, MkSymbol(name), null, range); - } - - /** - * Creates a fresh constant function declaration with a name prefixed with - * . - * - **/ - public FuncDecl MkFreshConstDecl(String prefix, Sort range) - throws Z3Exception - { - - CheckContextMatch(range); - return new FuncDecl(this, prefix, null, range); - } - - /** - * Creates a new bound variable. The de-Bruijn index of - * the variable The sort of the variable - **/ - public Expr MkBound(int index, Sort ty) throws Z3Exception - { - return Expr.Create(this, - Native.mkBound(nCtx(), index, ty.NativeObject())); - } - - /** - * Create a quantifier pattern. - **/ - public Pattern MkPattern(Expr[] terms) throws Z3Exception - { - if (terms.length == 0) - throw new Z3Exception("Cannot create a pattern from zero terms"); - - long[] termsNative = AST.ArrayToNative(terms); - return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length, - termsNative)); - } - - /** - * Creates a new Constant of sort and named - * . - **/ - public Expr MkConst(Symbol name, Sort range) throws Z3Exception - { - - CheckContextMatch(name); - CheckContextMatch(range); - - return Expr.Create( - this, - Native.mkConst(nCtx(), name.NativeObject(), - range.NativeObject())); - } - - /** - * Creates a new Constant of sort and named - * . - **/ - public Expr MkConst(String name, Sort range) throws Z3Exception - { - - return MkConst(MkSymbol(name), range); - } - - /** - * Creates a fresh Constant of sort and a name - * prefixed with . - **/ - public Expr MkFreshConst(String prefix, Sort range) throws Z3Exception - { - - CheckContextMatch(range); - return Expr.Create(this, - Native.mkFreshConst(nCtx(), prefix, range.NativeObject())); - } - - /** - * Creates a fresh constant from the FuncDecl . A decl of a 0-arity function - **/ - public Expr MkConst(FuncDecl f) throws Z3Exception - { - - return MkApp(f, (Expr)null); - } - - /** - * Create a Boolean constant. - **/ - public BoolExpr MkBoolConst(Symbol name) throws Z3Exception - { - - return (BoolExpr) MkConst(name, BoolSort()); - } - - /** - * Create a Boolean constant. - **/ - public BoolExpr MkBoolConst(String name) throws Z3Exception - { - - return (BoolExpr) MkConst(MkSymbol(name), BoolSort()); - } - - /** - * Creates an integer constant. - **/ - public IntExpr MkIntConst(Symbol name) throws Z3Exception - { - - return (IntExpr) MkConst(name, IntSort()); - } - - /** - * Creates an integer constant. - **/ - public IntExpr MkIntConst(String name) throws Z3Exception - { - - return (IntExpr) MkConst(name, IntSort()); - } - - /** - * Creates a real constant. - **/ - public RealExpr MkRealConst(Symbol name) throws Z3Exception - { - - return (RealExpr) MkConst(name, RealSort()); - } - - /** - * Creates a real constant. - **/ - public RealExpr MkRealConst(String name) throws Z3Exception - { - - return (RealExpr) MkConst(name, RealSort()); - } - - /** - * Creates a bit-vector constant. - **/ - public BitVecExpr MkBVConst(Symbol name, int size) throws Z3Exception - { - - return (BitVecExpr) MkConst(name, MkBitVecSort(size)); - } - - /** - * Creates a bit-vector constant. - **/ - public BitVecExpr MkBVConst(String name, int size) throws Z3Exception - { - - return (BitVecExpr) MkConst(name, MkBitVecSort(size)); - } - - /** - * Create a new function application. - **/ - public Expr MkApp(FuncDecl f, Expr arg) throws Z3Exception - { - CheckContextMatch(f); - CheckContextMatch(arg); - Expr[] args = { arg }; - return Expr.Create(this, f, args); - } - - /** - * Create a new function application. - **/ - public Expr MkApp(FuncDecl f, Expr[] args) throws Z3Exception - { - - CheckContextMatch(f); - CheckContextMatch(args); - return Expr.Create(this, f, args); - } - - /** - * The true Term. - **/ - public BoolExpr MkTrue() throws Z3Exception - { - return new BoolExpr(this, Native.mkTrue(nCtx())); - } - - /** - * The false Term. - **/ - public BoolExpr MkFalse() throws Z3Exception - { - return new BoolExpr(this, Native.mkFalse(nCtx())); - } - - /** - * Creates a Boolean value. - **/ - public BoolExpr MkBool(boolean value) throws Z3Exception - { - return value ? MkTrue() : MkFalse(); - } - - /** - * Creates the equality = . - **/ - public BoolExpr MkEq(Expr x, Expr y) throws Z3Exception - { - CheckContextMatch(x); - CheckContextMatch(y); - return new BoolExpr(this, Native.mkEq(nCtx(), x.NativeObject(), - y.NativeObject())); - } - - /** - * Creates a distinct term. - **/ - public BoolExpr MkDistinct(Expr[] args) throws Z3Exception - { - CheckContextMatch(args); - return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length, - AST.ArrayToNative(args))); - } - - /** - * Mk an expression representing not(a). - **/ - public BoolExpr MkNot(BoolExpr a) throws Z3Exception - { - - CheckContextMatch(a); - return new BoolExpr(this, Native.mkNot(nCtx(), a.NativeObject())); - } - - /** - * Create an expression representing an if-then-else: - * ite(t1, t2, t3). An expression with Boolean - * sort An expression An - * expression with the same sort as - **/ - public Expr MkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - CheckContextMatch(t3); - return Expr.Create( - this, - Native.mkIte(nCtx(), t1.NativeObject(), t2.NativeObject(), - t3.NativeObject())); - } - - /** - * Create an expression representing t1 iff t2. - **/ - public BoolExpr MkIff(BoolExpr t1, BoolExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkIff(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 -> t2. - **/ - public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkImplies(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 xor t2. - **/ - public BoolExpr MkXor(BoolExpr t1, BoolExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkXor(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t[0] and t[1] and .... - **/ - public BoolExpr MkAnd(BoolExpr[] t) throws Z3Exception - { - - CheckContextMatch(t); - return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, - AST.ArrayToNative(t))); - } - - /** - * Create an expression representing t[0] or t[1] or .... - **/ - public BoolExpr MkOr(BoolExpr[] t) throws Z3Exception - { - - CheckContextMatch(t); - return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, - AST.ArrayToNative(t))); - } - - /** - * Create an expression representing t[0] + t[1] + .... - **/ - public ArithExpr MkAdd(ArithExpr[] t) throws Z3Exception - { - - CheckContextMatch(t); - return (ArithExpr) Expr.Create(this, - Native.mkAdd(nCtx(), (int) t.length, AST.ArrayToNative(t))); - } - - /** - * Create an expression representing t[0] * t[1] * .... - **/ - public ArithExpr MkMul(ArithExpr[] t) throws Z3Exception - { - - CheckContextMatch(t); - return (ArithExpr) Expr.Create(this, - Native.mkMul(nCtx(), (int) t.length, AST.ArrayToNative(t))); - } - - /** - * Create an expression representing t[0] - t[1] - .... - **/ - public ArithExpr MkSub(ArithExpr[] t) throws Z3Exception - { - - CheckContextMatch(t); - return (ArithExpr) Expr.Create(this, - Native.mkSub(nCtx(), (int) t.length, AST.ArrayToNative(t))); - } - - /** - * Create an expression representing -t. - **/ - public ArithExpr MkUnaryMinus(ArithExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return (ArithExpr) Expr.Create(this, - Native.mkUnaryMinus(nCtx(), t.NativeObject())); - } - - /** - * Create an expression representing t1 / t2. - **/ - public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return (ArithExpr) Expr.Create(this, - Native.mkDiv(nCtx(), t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create an expression representing t1 mod t2. The - * arguments must have int type. - **/ - public IntExpr MkMod(IntExpr t1, IntExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new IntExpr(this, Native.mkMod(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 rem t2. The - * arguments must have int type. - **/ - public IntExpr MkRem(IntExpr t1, IntExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new IntExpr(this, Native.mkRem(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 ^ t2. - **/ - public ArithExpr MkPower(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return (ArithExpr) Expr.Create(this, - Native.mkPower(nCtx(), t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create an expression representing t1 < t2 - **/ - public BoolExpr MkLt(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkLt(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 <= t2 - **/ - public BoolExpr MkLe(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkLe(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 > t2 - **/ - public BoolExpr MkGt(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkGt(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create an expression representing t1 >= t2 - **/ - public BoolExpr MkGe(ArithExpr t1, ArithExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkGe(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Coerce an integer to a real. There is also a converse operation - * exposed. It follows the semantics prescribed by the SMT-LIB standard. - * - * You can take the floor of a real by creating an auxiliary integer Term - * k and and asserting - * MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument - * must be of integer sort. - **/ - public RealExpr MkInt2Real(IntExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new RealExpr(this, Native.mkInt2real(nCtx(), t.NativeObject())); - } - - /** - * Coerce a real to an integer. The semantics of this function - * follows the SMT-LIB standard for the function to_int. The argument must - * be of real sort. - **/ - public IntExpr MkReal2Int(RealExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new IntExpr(this, Native.mkReal2int(nCtx(), t.NativeObject())); - } - - /** - * Creates an expression that checks whether a real number is an integer. - **/ - public BoolExpr MkIsInteger(RealExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BoolExpr(this, Native.mkIsInt(nCtx(), t.NativeObject())); - } - - /** - * Bitwise negation. The argument must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVNot(BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.NativeObject())); - } - - /** - * Take conjunction of bits in a vector, return vector of length 1. - * The argument must have a bit-vector sort. - **/ - public BitVecExpr MkBVRedAND(BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvredand(nCtx(), t.NativeObject())); - } - - /** - * Take disjunction of bits in a vector, return vector of length 1. - * The argument must have a bit-vector sort. - **/ - public BitVecExpr MkBVRedOR(BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvredor(nCtx(), t.NativeObject())); - } - - /** - * Bitwise conjunction. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvand(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bitwise disjunction. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bitwise XOR. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvxor(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bitwise NAND. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvnand(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bitwise NOR. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvnor(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bitwise XNOR. The arguments must have a bit-vector - * sort. - **/ - public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvxnor(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Standard two's complement unary minus. The arguments must have a - * bit-vector sort. - **/ - public BitVecExpr MkBVNeg(BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.NativeObject())); - } - - /** - * Two's complement addition. The arguments must have the same - * bit-vector sort. - **/ - public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvadd(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement subtraction. The arguments must have the same - * bit-vector sort. - **/ - public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsub(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement multiplication. The arguments must have the - * same bit-vector sort. - **/ - public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvmul(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned division. It is defined as the floor of - * t1/t2 if \c t2 is different from zero. If t2 is - * zero, then the result is undefined. The arguments must have the same - * bit-vector sort. - **/ - public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvudiv(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Signed division. It is defined in the following way: - * - * - The \c floor of t1/t2 if \c t2 is different from zero, and - * t1*t2 >= 0. - * - * - The \c ceiling of t1/t2 if \c t2 is different from zero, - * and t1*t2 < 0. - * - * If t2 is zero, then the result is undefined. The arguments - * must have the same bit-vector sort. - **/ - public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsdiv(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned remainder. It is defined as - * t1 - (t1 /u t2) * t2, where /u represents - * unsigned division. If t2 is zero, then the result is - * undefined. The arguments must have the same bit-vector sort. - **/ - public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvurem(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Signed remainder. It is defined as - * t1 - (t1 /s t2) * t2, where /s represents - * signed division. The most significant bit (sign) of the result is equal - * to the most significant bit of \c t1. - * - * If t2 is zero, then the result is undefined. The arguments - * must have the same bit-vector sort. - **/ - public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsrem(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement signed remainder (sign follows divisor). If - * t2 is zero, then the result is undefined. The arguments must - * have the same bit-vector sort. - **/ - public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsmod(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned less-than The arguments must have the same bit-vector - * sort. - **/ - public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvult(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement signed less-than The arguments must have the - * same bit-vector sort. - **/ - public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned less-than or equal to. The arguments must have the - * same bit-vector sort. - **/ - public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvule(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement signed less-than or equal to. The arguments - * must have the same bit-vector sort. - **/ - public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned greater than or equal to. The arguments must have the - * same bit-vector sort. - **/ - public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement signed greater than or equal to. The arguments - * must have the same bit-vector sort. - **/ - public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Unsigned greater-than. The arguments must have the same - * bit-vector sort. - **/ - public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Two's complement signed greater-than. The arguments must have - * the same bit-vector sort. - **/ - public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bit-vector concatenation. The arguments must have a bit-vector - * sort. - * - * @return The result is a bit-vector of size n1+n2, where - * n1 (n2) is the size of t1 - * (t2). - * - **/ - public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkConcat(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Bit-vector extraction. Extract the bits - * down to from a bitvector of size m to - * yield a new bitvector of size n, where - * n = high - low + 1. The argument must - * have a bit-vector sort. - **/ - public BitVecExpr MkExtract(int high, int low, BitVecExpr t) - throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low, - t.NativeObject())); - } - - /** - * Bit-vector sign extension. Sign-extends the given bit-vector to - * the (signed) equivalent bitvector of size m+i, where \c m is - * the size of the given bit-vector. The argument must - * have a bit-vector sort. - **/ - public BitVecExpr MkSignExt(int i, BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, - t.NativeObject())); - } - - /** - * Bit-vector zero extension. Extend the given bit-vector with - * zeros to the (unsigned) equivalent bitvector of size m+i, - * where \c m is the size of the given bit-vector. The argument must have a bit-vector sort. - **/ - public BitVecExpr MkZeroExt(int i, BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, - t.NativeObject())); - } - - /** - * Bit-vector repetition. The argument must - * have a bit-vector sort. - **/ - public BitVecExpr MkRepeat(int i, BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, - Native.mkRepeat(nCtx(), i, t.NativeObject())); - } - - /** - * Shift left. It is equivalent to multiplication by - * 2^x where \c x is the value of . - * - * NB. The semantics of shift operations varies between environments. This - * definition does not necessarily capture directly the semantics of the - * programming language or assembly architecture you are modeling. - * - * The arguments must have a bit-vector sort. - **/ - public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvshl(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Logical shift right It is equivalent to unsigned division by - * 2^x where \c x is the value of . - * - * NB. The semantics of shift operations varies between environments. This - * definition does not necessarily capture directly the semantics of the - * programming language or assembly architecture you are modeling. - * - * The arguments must have a bit-vector sort. - **/ - public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvlshr(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Arithmetic shift right It is like logical shift right except - * that the most significant bits of the result always copy the most - * significant bit of the second argument. - * - * NB. The semantics of shift operations varies between environments. This - * definition does not necessarily capture directly the semantics of the - * programming language or assembly architecture you are modeling. - * - * The arguments must have a bit-vector sort. - **/ - public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvashr(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Rotate Left. Rotate bits of \c t to the left \c i times. The - * argument must have a bit-vector sort. - **/ - public BitVecExpr MkBVRotateLeft(int i, BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, - t.NativeObject())); - } - - /** - * Rotate Right. Rotate bits of \c t to the right \c i times. The - * argument must have a bit-vector sort. - **/ - public BitVecExpr MkBVRotateRight(int i, BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, - t.NativeObject())); - } - - /** - * Rotate Left. Rotate bits of to the left - * times. The arguments must have the same bit-vector - * sort. - **/ - public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Rotate Right. Rotate bits of to the - * right times. The arguments must have the same - * bit-vector sort. - **/ - public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create an bit bit-vector from the integer argument - * . NB. This function is essentially treated - * as uninterpreted. So you cannot expect Z3 to precisely reflect the - * semantics of this function when solving constraints with this function. - * - * The argument must be of integer sort. - **/ - public BitVecExpr MkInt2BV(int n, IntExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BitVecExpr(this, - Native.mkInt2bv(nCtx(), n, t.NativeObject())); - } - - /** - * Create an integer from the bit-vector argument . - * If \c is_signed is false, then the bit-vector \c t1 is treated - * as unsigned. So the result is non-negative and in the range - * [0..2^N-1], where N are the number of bits in . If \c is_signed is true, \c t1 is treated as a signed - * bit-vector. - * - * NB. This function is essentially treated as uninterpreted. So you cannot - * expect Z3 to precisely reflect the semantics of this function when - * solving constraints with this function. - * - * The argument must be of bit-vector sort. - **/ - public IntExpr MkBV2Int(BitVecExpr t, boolean signed) throws Z3Exception - { - - CheckContextMatch(t); - return new IntExpr(this, Native.mkBv2int(nCtx(), t.NativeObject(), - (signed) ? true : false)); - } - - /** - * Create a predicate that checks that the bit-wise addition does not - * overflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, - boolean isSigned) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, - Native.mkBvaddNoOverflow(nCtx(), t1.NativeObject(), - t2.NativeObject(), (isSigned) ? true : false)); - } - - /** - * Create a predicate that checks that the bit-wise addition does not - * underflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create a predicate that checks that the bit-wise subtraction does not - * overflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create a predicate that checks that the bit-wise subtraction does not - * underflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, - boolean isSigned) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, - Native.mkBvsubNoUnderflow(nCtx(), t1.NativeObject(), - t2.NativeObject(), (isSigned) ? true : false)); - } - - /** - * Create a predicate that checks that the bit-wise signed division does not - * overflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create a predicate that checks that the bit-wise negation does not - * overflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVNegNoOverflow(BitVecExpr t) throws Z3Exception - { - - CheckContextMatch(t); - return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), - t.NativeObject())); - } - - /** - * Create a predicate that checks that the bit-wise multiplication does not - * overflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, - boolean isSigned) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, - Native.mkBvmulNoOverflow(nCtx(), t1.NativeObject(), - t2.NativeObject(), (isSigned) ? true : false)); - } - - /** - * Create a predicate that checks that the bit-wise multiplication does not - * underflow. The arguments must be of bit-vector sort. - **/ - public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) - throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create an array constant. - **/ - public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range) - throws Z3Exception - { - - return (ArrayExpr) MkConst(name, MkArraySort(domain, range)); - } - - /** - * Create an array constant. - **/ - public ArrayExpr MkArrayConst(String name, Sort domain, Sort range) - throws Z3Exception - { - - return (ArrayExpr) MkConst(MkSymbol(name), MkArraySort(domain, range)); - } - - /** - * Array read. The argument a is the array and - * i is the index of the array that gets read. - * - * The node a must have an array sort - * [domain -> range], and i must have the sort - * domain. The sort of the result is range. - * - **/ - public Expr MkSelect(ArrayExpr a, Expr i) throws Z3Exception - { - - CheckContextMatch(a); - CheckContextMatch(i); - return Expr.Create(this, - Native.mkSelect(nCtx(), a.NativeObject(), i.NativeObject())); - } - - /** - * Array update. The node a must have an array sort - * [domain -> range], i must have sort - * domain, v must have sort range. The sort of the - * result is [domain -> range]. The semantics of this function - * is given by the theory of arrays described in the SMT-LIB standard. See - * http://smtlib.org for more details. The result of this function is an - * array that is equal to a (with respect to - * select) on all indices except for i, where it - * maps to v (and the select of a - * with respect to i may be a different value). - **/ - public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v) throws Z3Exception - { - - CheckContextMatch(a); - CheckContextMatch(i); - CheckContextMatch(v); - return new ArrayExpr(this, Native.mkStore(nCtx(), a.NativeObject(), - i.NativeObject(), v.NativeObject())); - } - - /** - * Create a constant array. The resulting term is an array, such - * that a selecton an arbitrary index produces the value - * v. - * - **/ - public ArrayExpr MkConstArray(Sort domain, Expr v) throws Z3Exception - { - - CheckContextMatch(domain); - CheckContextMatch(v); - return new ArrayExpr(this, Native.mkConstArray(nCtx(), - domain.NativeObject(), v.NativeObject())); - } - - /** - * Maps f on the argument arrays. Eeach element of - * args must be of an array sort - * [domain_i -> range_i]. The function declaration - * f must have type range_1 .. range_n -> range. - * v must have sort range. The sort of the result is - * [domain_i -> range]. - **/ - public ArrayExpr MkMap(FuncDecl f, ArrayExpr[] args) throws Z3Exception - { - - CheckContextMatch(f); - CheckContextMatch(args); - return (ArrayExpr) Expr.Create(this, Native.mkMap(nCtx(), - f.NativeObject(), AST.ArrayLength(args), - AST.ArrayToNative(args))); - } - - /** - * Access the array default value. Produces the default range - * value, for arrays that can be represented as finite maps with a default - * range value. - **/ - public Expr MkTermArray(ArrayExpr array) throws Z3Exception - { - - CheckContextMatch(array); - return Expr.Create(this, - Native.mkArrayDefault(nCtx(), array.NativeObject())); - } - - /** - * Create a set type. - **/ - public SetSort MkSetSort(Sort ty) throws Z3Exception - { - - CheckContextMatch(ty); - return new SetSort(this, ty); - } - - /** - * Create an empty set. - **/ - public Expr MkEmptySet(Sort domain) throws Z3Exception - { - - CheckContextMatch(domain); - return Expr.Create(this, - Native.mkEmptySet(nCtx(), domain.NativeObject())); - } - - /** - * Create the full set. - **/ - public Expr MkFullSet(Sort domain) throws Z3Exception - { - - CheckContextMatch(domain); - return Expr.Create(this, - Native.mkFullSet(nCtx(), domain.NativeObject())); - } - - /** - * Add an element to the set. - **/ - public Expr MkSetAdd(Expr set, Expr element) throws Z3Exception - { - - CheckContextMatch(set); - CheckContextMatch(element); - return Expr.Create( - this, - Native.mkSetAdd(nCtx(), set.NativeObject(), - element.NativeObject())); - } - - /** - * Remove an element from a set. - **/ - public Expr MkSetDel(Expr set, Expr element) throws Z3Exception - { - - CheckContextMatch(set); - CheckContextMatch(element); - return Expr.Create( - this, - Native.mkSetDel(nCtx(), set.NativeObject(), - element.NativeObject())); - } - - /** - * Take the union of a list of sets. - **/ - public Expr MkSetUnion(Expr[] args) throws Z3Exception - { - - CheckContextMatch(args); - return Expr.Create( - this, - Native.mkSetUnion(nCtx(), (int) args.length, - AST.ArrayToNative(args))); - } - - /** - * Take the intersection of a list of sets. - **/ - public Expr MkSetIntersection(Expr[] args) throws Z3Exception - { - - CheckContextMatch(args); - return Expr.Create( - this, - Native.mkSetIntersect(nCtx(), (int) args.length, - AST.ArrayToNative(args))); - } - - /** - * Take the difference between two sets. - **/ - public Expr MkSetDifference(Expr arg1, Expr arg2) throws Z3Exception - { - - CheckContextMatch(arg1); - CheckContextMatch(arg2); - return Expr.Create( - this, - Native.mkSetDifference(nCtx(), arg1.NativeObject(), - arg2.NativeObject())); - } - - /** - * Take the complement of a set. - **/ - public Expr MkSetComplement(Expr arg) throws Z3Exception - { - - CheckContextMatch(arg); - return Expr.Create(this, - Native.mkSetComplement(nCtx(), arg.NativeObject())); - } - - /** - * Check for set membership. - **/ - public Expr MkSetMembership(Expr elem, Expr set) throws Z3Exception - { - - CheckContextMatch(elem); - CheckContextMatch(set); - return Expr.Create( - this, - Native.mkSetMember(nCtx(), elem.NativeObject(), - set.NativeObject())); - } - - /** - * Check for subsetness of sets. - **/ - public Expr MkSetSubset(Expr arg1, Expr arg2) throws Z3Exception - { - - CheckContextMatch(arg1); - CheckContextMatch(arg2); - return Expr.Create( - this, - Native.mkSetSubset(nCtx(), arg1.NativeObject(), - arg2.NativeObject())); - } - - /** - * Create a Term of a given sort. A string representing the - * Term value in decimal notation. If the given sort is a real, then the - * Term can be a rational, that is, a string of the form - * [num]* / [num]*. The sort of the - * numeral. In the current implementation, the given sort can be an int, - * real, or bit-vectors of arbitrary size. - * - * @return A Term with value and sort - **/ - public Expr MkNumeral(String v, Sort ty) throws Z3Exception - { - - CheckContextMatch(ty); - return Expr - .Create(this, Native.mkNumeral(nCtx(), v, ty.NativeObject())); - } - - /** - * Create a Term of a given sort. This function can be use to create - * numerals that fit in a machine integer. It is slightly faster than - * MakeNumeral since it is not necessary to parse a string. - * Value of the numeral Sort of the - * numeral - * - * @return A Term with value and type - **/ - public Expr MkNumeral(int v, Sort ty) throws Z3Exception - { - - CheckContextMatch(ty); - return Expr.Create(this, Native.mkInt(nCtx(), v, ty.NativeObject())); - } - - /** - * Create a Term of a given sort. This function can be use to create - * numerals that fit in a machine integer. It is slightly faster than - * MakeNumeral since it is not necessary to parse a string. - * Value of the numeral Sort of the - * numeral - * - * @return A Term with value and type - **/ - public Expr MkNumeral(long v, Sort ty) throws Z3Exception - { - - CheckContextMatch(ty); - return Expr.Create(this, Native.mkInt64(nCtx(), v, ty.NativeObject())); - } - - /** - * Create a real from a fraction. numerator of - * rational. denominator of rational. - * - * @return A Term with value / - * and sort Real - **/ - public RatNum MkReal(int num, int den) throws Z3Exception - { - if (den == 0) - throw new Z3Exception("Denominator is zero"); - - return new RatNum(this, Native.mkReal(nCtx(), num, den)); - } - - /** - * Create a real numeral. A string representing the Term - * value in decimal notation. - * - * @return A Term with value and sort Real - **/ - public RatNum MkReal(String v) throws Z3Exception - { - - return new RatNum(this, Native.mkNumeral(nCtx(), v, RealSort() - .NativeObject())); - } - - /** - * Create a real numeral. value of the numeral. - * - * @return A Term with value and sort Real - **/ - public RatNum MkReal(int v) throws Z3Exception - { - - return new RatNum(this, Native.mkInt(nCtx(), v, RealSort() - .NativeObject())); - } - - /** - * Create a real numeral. value of the numeral. - * - * @return A Term with value and sort Real - **/ - public RatNum MkReal(long v) throws Z3Exception - { - - return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort() - .NativeObject())); - } - - /** - * Create an integer numeral. A string representing the Term - * value in decimal notation. - **/ - public IntNum MkInt(String v) throws Z3Exception - { - - return new IntNum(this, Native.mkNumeral(nCtx(), v, IntSort() - .NativeObject())); - } - - /** - * Create an integer numeral. value of the numeral. - * - * @return A Term with value and sort Integer - **/ - public IntNum MkInt(int v) throws Z3Exception - { - - return new IntNum(this, Native.mkInt(nCtx(), v, IntSort() - .NativeObject())); - } - - /** - * Create an integer numeral. value of the numeral. - * - * @return A Term with value and sort Integer - **/ - public IntNum MkInt(long v) throws Z3Exception - { - - return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort() - .NativeObject())); - } - - /** - * Create a bit-vector numeral. A string representing the - * value in decimal notation. the size of the - * bit-vector - **/ - public BitVecNum MkBV(String v, int size) throws Z3Exception - { - - return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); - } - - /** - * Create a bit-vector numeral. value of the - * numeral. the size of the bit-vector - **/ - public BitVecNum MkBV(int v, int size) throws Z3Exception - { - - return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); - } - - /** - * Create a bit-vector numeral. value of the - * numeral. * the size of the bit-vector - **/ - public BitVecNum MkBV(long v, int size) throws Z3Exception - { - - return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); - } - - /** - * Create a universal Quantifier. Creates a forall formula, where - * is the weight, is - * an array of patterns, is an array with the sorts - * of the bound variables, is an array with the - * 'names' of the bound variables, and is the body - * of the quantifier. Quantifiers are associated with weights indicating the - * importance of using the quantifier during instantiation. - * the sorts of the bound variables. names of the bound variables the - * body of the quantifier. quantifiers are - * associated with weights indicating the importance of using the quantifier - * during instantiation. By default, pass the weight 0. array containing the patterns created using - * MkPattern. array containing - * the anti-patterns created using MkPattern. optional symbol to track quantifier. optional symbol to track skolem constants. - **/ - public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, - int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) throws Z3Exception - { - - return new Quantifier(this, true, sorts, names, body, weight, patterns, - noPatterns, quantifierID, skolemID); - } - - /** - * Create a universal Quantifier. - **/ - public Quantifier MkForall(Expr[] boundConstants, Expr body, int weight, - Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, - Symbol skolemID) throws Z3Exception - { - - return new Quantifier(this, true, boundConstants, body, weight, - patterns, noPatterns, quantifierID, skolemID); - } - - /** - * Create an existential Quantifier. - **/ - public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, - int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) throws Z3Exception - { - - return new Quantifier(this, false, sorts, names, body, weight, - patterns, noPatterns, quantifierID, skolemID); - } - - /** - * Create an existential Quantifier. - **/ - public Quantifier MkExists(Expr[] boundConstants, Expr body, int weight, - Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, - Symbol skolemID) throws Z3Exception - { - - return new Quantifier(this, false, boundConstants, body, weight, - patterns, noPatterns, quantifierID, skolemID); - } - - /** - * Create a Quantifier. - **/ - public Quantifier MkQuantifier(boolean universal, Sort[] sorts, - Symbol[] names, Expr body, int weight, Pattern[] patterns, - Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) - throws Z3Exception - { - - if (universal) - return MkForall(sorts, names, body, weight, patterns, noPatterns, - quantifierID, skolemID); - else - return MkExists(sorts, names, body, weight, patterns, noPatterns, - quantifierID, skolemID); - } - - /** - * Create a Quantifier. - **/ - public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, - Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) throws Z3Exception - { - - if (universal) - return MkForall(boundConstants, body, weight, patterns, noPatterns, - quantifierID, skolemID); - else - return MkExists(boundConstants, body, weight, patterns, noPatterns, - quantifierID, skolemID); - } - - /** - * Selects the format used for pretty-printing expressions. The - * default mode for pretty printing expressions is to produce SMT-LIB style - * output where common subexpressions are printed at each occurrence. The - * mode is called Z3_PRINT_SMTLIB_FULL. To print shared common - * subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in - * way that conforms to SMT-LIB standards and uses let expressions to share - * common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. - **/ - public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception - { - Native.setAstPrintMode(nCtx(), value.toInt()); - } - - /** - * Convert a benchmark into an SMT-LIB formatted string. Name of the benchmark. The argument is optional. - * The benchmark logic. The status string (sat, unsat, or unknown) Other attributes, such as source, difficulty or - * category. Auxiliary - * assumptions. Formula to be checked for - * consistency in conjunction with assumptions. - * - * @return A string representation of the benchmark. - **/ - public String BenchmarkToSMTString(String name, String logic, - String status, String attributes, BoolExpr[] assumptions, - BoolExpr formula) throws Z3Exception - { - - return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, - attributes, (int) assumptions.length, - AST.ArrayToNative(assumptions), formula.NativeObject()); - } - - /** - * Parse the given string using the SMT-LIB parser. The symbol - * table of the parser can be initialized using the given sorts and - * declarations. The symbols in the arrays and - * don't need to match the names of the sorts - * and declarations in the arrays and . This is a useful feature since we can use arbitrary names - * to reference sorts and declarations. - **/ - public void ParseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, - Symbol[] declNames, FuncDecl[] decls) throws Z3Exception - { - int csn = Symbol.ArrayLength(sortNames); - int cs = Sort.ArrayLength(sorts); - int cdn = Symbol.ArrayLength(declNames); - int cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibString(nCtx(), str, AST.ArrayLength(sorts), - Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), - AST.ArrayToNative(decls)); - } - - /** - * Parse the given file using the SMT-LIB parser. - **/ - public void ParseSMTLIBFile(String fileName, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - throws Z3Exception - { - int csn = Symbol.ArrayLength(sortNames); - int cs = Sort.ArrayLength(sorts); - int cdn = Symbol.ArrayLength(declNames); - int cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibFile(nCtx(), fileName, AST.ArrayLength(sorts), - Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), - AST.ArrayToNative(decls)); - } - - /** - * The number of SMTLIB formulas parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public int NumSMTLIBFormulas() throws Z3Exception - { - return Native.getSmtlibNumFormulas(nCtx()); - } - - /** - * The formulas parsed by the last call to ParseSMTLIBString or - * ParseSMTLIBFile. - **/ - public BoolExpr[] SMTLIBFormulas() throws Z3Exception - { - - int n = NumSMTLIBFormulas(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = (BoolExpr) Expr.Create(this, - Native.getSmtlibFormula(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB assumptions parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public int NumSMTLIBAssumptions() throws Z3Exception - { - return Native.getSmtlibNumAssumptions(nCtx()); - } - - /** - * The assumptions parsed by the last call to ParseSMTLIBString - * or ParseSMTLIBFile. - **/ - public BoolExpr[] SMTLIBAssumptions() throws Z3Exception - { - - int n = NumSMTLIBAssumptions(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = (BoolExpr) Expr.Create(this, - Native.getSmtlibAssumption(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public int NumSMTLIBDecls() throws Z3Exception - { - return Native.getSmtlibNumDecls(nCtx()); - } - - /** - * The declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public FuncDecl[] SMTLIBDecls() throws Z3Exception - { - - int n = NumSMTLIBDecls(); - FuncDecl[] res = new FuncDecl[n]; - for (int i = 0; i < n; i++) - res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB sorts parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public int NumSMTLIBSorts() throws Z3Exception - { - return Native.getSmtlibNumSorts(nCtx()); - } - - /** - * The declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. - **/ - public Sort[] SMTLIBSorts() throws Z3Exception - { - - int n = NumSMTLIBSorts(); - Sort[] res = new Sort[n]; - for (int i = 0; i < n; i++) - res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx(), i)); - return res; - } - - /** - * Parse the given string using the SMT-LIB2 parser. - * - * @return A conjunction of assertions in the scope (up to push/pop) at the - * end of the string. - **/ - public BoolExpr ParseSMTLIB2String(String str, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - throws Z3Exception - { - - int csn = Symbol.ArrayLength(sortNames); - int cs = Sort.ArrayLength(sorts); - int cdn = Symbol.ArrayLength(declNames); - int cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - return (BoolExpr) Expr.Create(this, Native.parseSmtlib2String(nCtx(), - str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), - AST.ArrayToNative(sorts), AST.ArrayLength(decls), - Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); - } - - /** - * Parse the given file using the SMT-LIB2 parser. - **/ - public BoolExpr ParseSMTLIB2File(String fileName, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - throws Z3Exception - { - - int csn = Symbol.ArrayLength(sortNames); - int cs = Sort.ArrayLength(sorts); - int cdn = Symbol.ArrayLength(declNames); - int cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - return (BoolExpr) Expr.Create(this, Native.parseSmtlib2File(nCtx(), - fileName, AST.ArrayLength(sorts), - Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), - AST.ArrayToNative(decls))); - } - - /** - * Creates a new Goal. Note that the Context must have been - * created with proof generation support if is set - * to true here. Indicates whether model - * generation should be enabled. Indicates - * whether unsat core generation should be enabled. Indicates whether proof generation should be - * enabled. - **/ - public Goal MkGoal(boolean models, boolean unsatCores, boolean proofs) - throws Z3Exception - { - - return new Goal(this, models, unsatCores, proofs); - } - - /** - * Creates a new ParameterSet. - **/ - public Params MkParams() throws Z3Exception - { - - return new Params(this); - } - - /** - * The number of supported tactics. - **/ - public int NumTactics() throws Z3Exception - { - return Native.getNumTactics(nCtx()); - } - - /** - * The names of all supported tactics. - **/ - public String[] TacticNames() throws Z3Exception - { - - int n = NumTactics(); - String[] res = new String[n]; - for (int i = 0; i < n; i++) - res[i] = Native.getTacticName(nCtx(), i); - return res; - } - - /** - * Returns a string containing a description of the tactic with the given - * name. - **/ - public String TacticDescription(String name) throws Z3Exception - { - - return Native.tacticGetDescr(nCtx(), name); - } - - /** - * Creates a new Tactic. - **/ - public Tactic MkTactic(String name) throws Z3Exception - { - - return new Tactic(this, name); - } - - /** - * Create a tactic that applies to a Goal and then - * to every subgoal produced by . - **/ - public Tactic AndThen(Tactic t1, Tactic t2, Tactic[] ts) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - CheckContextMatch(ts); - - long last = 0; - if (ts != null && ts.length > 0) - { - last = ts[ts.length - 1].NativeObject(); - for (int i = ts.length - 2; i >= 0; i--) - last = Native.tacticAndThen(nCtx(), ts[i].NativeObject(), last); - } - if (last != 0) - { - last = Native.tacticAndThen(nCtx(), t2.NativeObject(), last); - return new Tactic(this, Native.tacticAndThen(nCtx(), - t1.NativeObject(), last)); - } else - return new Tactic(this, Native.tacticAndThen(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create a tactic that applies to a Goal and then - * to every subgoal produced by . - * Shorthand for AndThen. - **/ - public Tactic Then(Tactic t1, Tactic t2, Tactic[] ts) throws Z3Exception - { - - return AndThen(t1, t2, ts); - } - - /** - * Create a tactic that first applies to a Goal and if - * it fails then returns the result of applied to the - * Goal. - **/ - public Tactic OrElse(Tactic t1, Tactic t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Native.tacticOrElse(nCtx(), t1.NativeObject(), - t2.NativeObject())); - } - - /** - * Create a tactic that applies to a goal for milliseconds. If does not - * terminate within milliseconds, then it fails. - * - **/ - public Tactic TryFor(Tactic t, int ms) throws Z3Exception - { - - CheckContextMatch(t); - return new Tactic(this, Native.tacticTryFor(nCtx(), t.NativeObject(), - ms)); - } - - /** - * Create a tactic that applies to a given goal if the - * probe evaluates to true. If evaluates to false, then the new tactic behaves like the - * skip tactic. - **/ - public Tactic When(Probe p, Tactic t) throws Z3Exception - { - - CheckContextMatch(t); - CheckContextMatch(p); - return new Tactic(this, Native.tacticWhen(nCtx(), p.NativeObject(), - t.NativeObject())); - } - - /** - * Create a tactic that applies to a given goal if the - * probe evaluates to true and - * otherwise. - **/ - public Tactic Cond(Probe p, Tactic t1, Tactic t2) throws Z3Exception - { - - CheckContextMatch(p); - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Native.tacticCond(nCtx(), p.NativeObject(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Create a tactic that keeps applying until the goal - * is not modified anymore or the maximum number of iterations is reached. - **/ - public Tactic Repeat(Tactic t, int max) throws Z3Exception - { - - CheckContextMatch(t); - return new Tactic(this, Native.tacticRepeat(nCtx(), t.NativeObject(), - max)); - } - - /** - * Create a tactic that just returns the given goal. - **/ - public Tactic Skip() throws Z3Exception - { - - return new Tactic(this, Native.tacticSkip(nCtx())); - } - - /** - * Create a tactic always fails. - **/ - public Tactic Fail() throws Z3Exception - { - - return new Tactic(this, Native.tacticFail(nCtx())); - } - - /** - * Create a tactic that fails if the probe evaluates to - * false. - **/ - public Tactic FailIf(Probe p) throws Z3Exception - { - - CheckContextMatch(p); - return new Tactic(this, Native.tacticFailIf(nCtx(), p.NativeObject())); - } - - /** - * Create a tactic that fails if the goal is not triviall satisfiable (i.e., - * empty) or trivially unsatisfiable (i.e., contains `false'). - **/ - public Tactic FailIfNotDecided() throws Z3Exception - { - - return new Tactic(this, Native.tacticFailIfNotDecided(nCtx())); - } - - /** - * Create a tactic that applies using the given set of - * parameters . - **/ - public Tactic UsingParams(Tactic t, Params p) throws Z3Exception - { - - CheckContextMatch(t); - CheckContextMatch(p); - return new Tactic(this, Native.tacticUsingParams(nCtx(), - t.NativeObject(), p.NativeObject())); - } - - /** - * Create a tactic that applies using the given set of - * parameters . Alias for - * UsingParams - **/ - public Tactic With(Tactic t, Params p) throws Z3Exception - { - - return UsingParams(t, p); - } - - /** - * Create a tactic that applies the given tactics in parallel. - **/ - public Tactic ParOr(Tactic[] t) throws Z3Exception - { - - CheckContextMatch(t); - return new Tactic(this, Native.tacticParOr(nCtx(), - Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); - } - - /** - * Create a tactic that applies to a given goal and - * then to every subgoal produced by . The subgoals are processed in parallel. - **/ - public Tactic ParAndThen(Tactic t1, Tactic t2) throws Z3Exception - { - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Native.tacticParAndThen(nCtx(), - t1.NativeObject(), t2.NativeObject())); - } - - /** - * Interrupt the execution of a Z3 procedure. This procedure can be - * used to interrupt: solvers, simplifiers and tactics. - **/ - public void Interrupt() throws Z3Exception - { - Native.interrupt(nCtx()); - } - - /** - * The number of supported Probes. - **/ - public int NumProbes() throws Z3Exception - { - return Native.getNumProbes(nCtx()); - } - - /** - * The names of all supported Probes. - **/ - public String[] ProbeNames() throws Z3Exception - { - - int n = NumProbes(); - String[] res = new String[n]; - for (int i = 0; i < n; i++) - res[i] = Native.getProbeName(nCtx(), i); - return res; - } - - /** - * Returns a string containing a description of the probe with the given - * name. - **/ - public String ProbeDescription(String name) throws Z3Exception - { - - return Native.probeGetDescr(nCtx(), name); - } - - /** - * Creates a new Probe. - **/ - public Probe MkProbe(String name) throws Z3Exception - { - - return new Probe(this, name); - } - - /** - * Create a probe that always evaluates to . - **/ - public Probe Const(double val) throws Z3Exception - { - - return new Probe(this, Native.probeConst(nCtx(), val)); - } - - /** - * Create a probe that evaluates to "true" when the value returned by - * is less than the value returned by - **/ - public Probe Lt(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeLt(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value returned by - * is greater than the value returned by - **/ - public Probe Gt(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeGt(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value returned by - * is less than or equal the value returned by - * - **/ - public Probe Le(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeLe(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value returned by - * is greater than or equal the value returned by - * - **/ - public Probe Ge(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeGe(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value returned by - * is equal to the value returned by - **/ - public Probe Eq(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeEq(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value and evaluate to "true". - **/ - public Probe And(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeAnd(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value or evaluate to "true". - **/ - public Probe Or(Probe p1, Probe p2) throws Z3Exception - { - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Native.probeOr(nCtx(), p1.NativeObject(), - p2.NativeObject())); - } - - /** - * Create a probe that evaluates to "true" when the value does not evaluate to "true". - **/ - public Probe Not(Probe p) throws Z3Exception - { - - CheckContextMatch(p); - return new Probe(this, Native.probeNot(nCtx(), p.NativeObject())); - } - - /** - * Creates a new (incremental) solver. This solver also uses a set - * of builtin tactics for handling the first check-sat command, and - * check-sat commands that take more than a given number of milliseconds to - * be solved. - **/ - public Solver MkSolver() throws Z3Exception - { - return MkSolver((Symbol)null); - } - - /** - * Creates a new (incremental) solver. This solver also uses a set - * of builtin tactics for handling the first check-sat command, and - * check-sat commands that take more than a given number of milliseconds to - * be solved. - **/ - public Solver MkSolver(Symbol logic) throws Z3Exception - { - - if (logic == null) - return new Solver(this, Native.mkSolver(nCtx())); - else - return new Solver(this, Native.mkSolverForLogic(nCtx(), - logic.NativeObject())); - } - - /** - * Creates a new (incremental) solver. - **/ - public Solver MkSolver(String logic) throws Z3Exception - { - - return MkSolver(MkSymbol(logic)); - } - - /** - * Creates a new (incremental) solver. - **/ - public Solver MkSimpleSolver() throws Z3Exception - { - - return new Solver(this, Native.mkSimpleSolver(nCtx())); - } - - /** - * Creates a solver that is implemented using the given tactic. - * The solver supports the commands Push and Pop, - * but it will always solve each check from scratch. - **/ - public Solver MkSolver(Tactic t) throws Z3Exception - { - - return new Solver(this, Native.mkSolverFromTactic(nCtx(), - t.NativeObject())); - } - - /** - * Create a Fixedpoint context. - **/ - public Fixedpoint MkFixedpoint() throws Z3Exception - { - - return new Fixedpoint(this); - } - - /** - * Wraps an AST. This function is used for transitions between - * native and managed objects. Note that - * must be a native object obtained from Z3 (e.g., through ) and that it must have a correct reference count (see - * e.g., . The native pointer to - * wrap. - **/ - public AST WrapAST(long nativeObject) throws Z3Exception - { - - return AST.Create(this, nativeObject); - } - - /** - * Unwraps an AST. This function is used for transitions between - * native and managed objects. It returns the native pointer to the AST. - * Note that AST objects are reference counted and unwrapping an AST - * disables automatic reference counting, i.e., all references to the IntPtr - * that is returned must be handled externally and through native calls (see - * e.g., ). The AST to unwrap. - **/ - public long UnwrapAST(AST a) - { - return a.NativeObject(); - } - - /** - * Return a string describing all available parameters to - * Expr.Simplify. - **/ - public String SimplifyHelp() throws Z3Exception - { - - return Native.simplifyGetHelp(nCtx()); - } - - /** - * Retrieves parameter descriptions for simplifier. - **/ - public ParamDescrs SimplifyParameterDescriptions() throws Z3Exception - { - return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx())); - } - - /** - * Enable/disable printing of warning messages to the console. Note - * that this function is static and effects the behaviour of all contexts - * globally. - **/ - public static void ToggleWarningMessages(boolean enabled) - throws Z3Exception - { - Native.toggleWarningMessages((enabled) ? true : false); - } - - // /// - // /// A delegate which is executed when an error is raised. - // /// - // /// - // /// Note that it is possible for memory leaks to occur if error handlers - // /// throw exceptions. - // /// - // public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, - // String errorString); - - // /// - // /// The OnError event. - // /// - // public event ErrorHandler OnError = null; - - /** - * Update a mutable configuration parameter. The list of all - * configuration parameters can be obtained using the Z3 executable: - * z3.exe -ini? Only a few configuration parameters are mutable - * once the context is created. An exception is thrown when trying to modify - * an immutable parameter. - **/ - public void UpdateParamValue(String id, String value) throws Z3Exception - { - Native.updateParamValue(nCtx(), id, value); - } - - /** - * Get a configuration parameter. Returns null if the parameter - * value does not exist. - **/ - public String GetParamValue(String id) throws Z3Exception - { - Native.StringPtr res = new Native.StringPtr(); - boolean r = Native.getParamValue(nCtx(), id, res); - if (!r) - return null; - else - return res.value; - } - - long m_ctx = 0; - Native.errorHandler m_n_err_handler = null; - - long nCtx() - { - return m_ctx; - } - - // void NativeErrorHandler(long ctx, Z3_error_code errorCode) - // { - // // Do-nothing error handler. The wrappers in Z3.Native will throw - // exceptions upon errors. - // } - - void InitContext() throws Z3Exception - { - setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - // m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // - // keep reference so it doesn't get collected. - // if (m_n_err_handler != null) Native.setErrorHandler(m_ctx, - // m_n_err_handler); - } - - void CheckContextMatch(Z3Object other) throws Z3Exception - { - if (this != other.Context()) - throw new Z3Exception("Context mismatch"); - } - - void CheckContextMatch(Z3Object[] arr) throws Z3Exception - { - if (arr != null) - for (Z3Object a : arr) - CheckContextMatch(a); - } - - private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue(); - private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(); - private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(); - private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(); - private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(); - private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(); - private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(); - private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(); - private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(); - private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(); - private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(); - private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(); - private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(); - private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(); - private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(); - - ASTDecRefQueue AST_DRQ() - { - return m_AST_DRQ; - } - - ASTMapDecRefQueue ASTMap_DRQ() - { - return m_ASTMap_DRQ; - } - - ASTVectorDecRefQueue ASTVector_DRQ() - { - return m_ASTVector_DRQ; - } - - ApplyResultDecRefQueue ApplyResult_DRQ() - { - return m_ApplyResult_DRQ; - } - - FuncInterpEntryDecRefQueue FuncEntry_DRQ() - { - return m_FuncEntry_DRQ; - } - - FuncInterpDecRefQueue FuncInterp_DRQ() - { - return m_FuncInterp_DRQ; - } - - GoalDecRefQueue Goal_DRQ() - { - return m_Goal_DRQ; - } - - ModelDecRefQueue Model_DRQ() - { - return m_Model_DRQ; - } - - ParamsDecRefQueue Params_DRQ() - { - return m_Params_DRQ; - } - - ParamDescrsDecRefQueue ParamDescrs_DRQ() - { - return m_ParamDescrs_DRQ; - } - - ProbeDecRefQueue Probe_DRQ() - { - return m_Probe_DRQ; - } - - SolverDecRefQueue Solver_DRQ() - { - return m_Solver_DRQ; - } - - StatisticsDecRefQueue Statistics_DRQ() - { - return m_Statistics_DRQ; - } - - TacticDecRefQueue Tactic_DRQ() - { - return m_Tactic_DRQ; - } - - FixedpointDecRefQueue Fixedpoint_DRQ() - { - return m_Fixedpoint_DRQ; - } - - protected long m_refCount = 0; - - /** - * Finalizer. - **/ - protected void finalize() - { - Dispose(); - - if (m_refCount == 0) - { - m_n_err_handler = null; - Native.delContext(m_ctx); - m_ctx = 0; - } else - /* re-queue the finalizer */ - /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount, m_n_err_handler); - } - - /** - * Disposes of the context. - **/ - public void Dispose() - { - m_AST_DRQ.Clear(this); - m_ASTMap_DRQ.Clear(this); - m_ASTVector_DRQ.Clear(this); - m_ApplyResult_DRQ.Clear(this); - m_FuncEntry_DRQ.Clear(this); - m_FuncInterp_DRQ.Clear(this); - m_Goal_DRQ.Clear(this); - m_Model_DRQ.Clear(this); - m_Params_DRQ.Clear(this); - m_Probe_DRQ.Clear(this); - m_Solver_DRQ.Clear(this); - m_Statistics_DRQ.Clear(this); - m_Tactic_DRQ.Clear(this); - m_Fixedpoint_DRQ.Clear(this); - - m_boolSort = null; - m_intSort = null; - m_realSort = null; - } + /** + * Constructor. + **/ + public Context() throws Z3Exception + { + super(); + m_ctx = Native.mkContextRc(0); + InitContext(); + } + + /** + * Constructor. + **/ + public Context(Map settings) throws Z3Exception + { + super(); + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkContextRc(cfg); + Native.delConfig(cfg); + InitContext(); + } + + private Context(long ctx, long refCount, Native.errorHandler errh) + { + super(); + this.m_ctx = ctx; + this.m_refCount = refCount; + this.m_n_err_handler = errh; + } + + /** + * Creates a new symbol using an integer. 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 + { + return new IntSymbol(this, i); + } + + /** + * Create a symbol using a string. + **/ + public StringSymbol MkSymbol(String name) throws Z3Exception + { + return new StringSymbol(this, name); + } + + /** + * Create an array of symbols. + **/ + Symbol[] MkSymbols(String[] names) throws Z3Exception + { + if (names == null) + return null; + Symbol[] result = new Symbol[names.length]; + for (int i = 0; i < names.length; ++i) + result[i] = MkSymbol(names[i]); + return result; + } + + private BoolSort m_boolSort = null; + private IntSort m_intSort = null; + private RealSort m_realSort = null; + + /** + * Retrieves the Boolean sort of the context. + **/ + public BoolSort BoolSort() throws Z3Exception + { + if (m_boolSort == null) + m_boolSort = new BoolSort(this); + return m_boolSort; + } + + /** + * Retrieves the Integer sort of the context. + **/ + public IntSort IntSort() throws Z3Exception + { + if (m_intSort == null) + m_intSort = new IntSort(this); + return m_intSort; + } + + /** + * Retrieves the Real sort of the context. + **/ + public RealSort RealSort() throws Z3Exception + { + if (m_realSort == null) + m_realSort = new RealSort(this); + return m_realSort; + } + + /** + * Create a new Boolean sort. + **/ + public BoolSort MkBoolSort() throws Z3Exception + { + + return new BoolSort(this); + } + + /** + * Create a new uninterpreted sort. + **/ + public UninterpretedSort MkUninterpretedSort(Symbol s) throws Z3Exception + { + + CheckContextMatch(s); + return new UninterpretedSort(this, s); + } + + /** + * Create a new uninterpreted sort. + **/ + public UninterpretedSort MkUninterpretedSort(String str) throws Z3Exception + { + + return MkUninterpretedSort(MkSymbol(str)); + } + + /** + * Create a new integer sort. + **/ + public IntSort MkIntSort() throws Z3Exception + { + + return new IntSort(this); + } + + /** + * Create a real sort. + **/ + public RealSort MkRealSort() throws Z3Exception + { + + return new RealSort(this); + } + + /** + * Create a new bit-vector sort. + **/ + public BitVecSort MkBitVecSort(int size) throws Z3Exception + { + + return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); + } + + /** + * Create a new array sort. + **/ + public ArraySort MkArraySort(Sort domain, Sort range) throws Z3Exception + { + + CheckContextMatch(domain); + CheckContextMatch(range); + return new ArraySort(this, domain, range); + } + + /** + * Create a new tuple sort. + **/ + public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, + Sort[] fieldSorts) throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(fieldNames); + CheckContextMatch(fieldSorts); + return new TupleSort(this, name, (int) fieldNames.length, fieldNames, + fieldSorts); + } + + /** + * Create a new enumeration sort. + **/ + public EnumSort MkEnumSort(Symbol name, Symbol[] enumNames) + throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(enumNames); + return new EnumSort(this, name, enumNames); + } + + /** + * Create a new enumeration sort. + **/ + public EnumSort MkEnumSort(String name, String[] enumNames) + throws Z3Exception + { + + return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames)); + } + + /** + * Create a new list sort. + **/ + public ListSort MkListSort(Symbol name, Sort elemSort) throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(elemSort); + return new ListSort(this, name, elemSort); + } + + /** + * Create a new list sort. + **/ + public ListSort MkListSort(String name, Sort elemSort) throws Z3Exception + { + + CheckContextMatch(elemSort); + return new ListSort(this, MkSymbol(name), elemSort); + } + + /** + * Create a new finite domain sort. + **/ + public FiniteDomainSort MkFiniteDomainSort(Symbol name, long size) + throws Z3Exception + { + + CheckContextMatch(name); + return new FiniteDomainSort(this, name, size); + } + + /** + * Create a new finite domain sort. + **/ + public FiniteDomainSort MkFiniteDomainSort(String name, long size) + throws Z3Exception + { + + return new FiniteDomainSort(this, MkSymbol(name), size); + } + + /** + * Create a datatype constructor. constructor + * name name of recognizer + * function. names of the constructor + * fields. field sorts, 0 if the field sort + * refers to a recursive sort. reference to + * datatype sort that is an argument to the constructor; if the + * corresponding sort reference is 0, then the value in sort_refs should be + * an index referring to one of the recursive datatypes that is + * declared. + **/ + public Constructor MkConstructor(Symbol name, Symbol recognizer, + Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) + throws Z3Exception + { + + return new Constructor(this, name, recognizer, fieldNames, sorts, + sortRefs); + } + + /** + * Create a datatype constructor. + * + * @return + **/ + public Constructor MkConstructor(String name, String recognizer, + String[] fieldNames, Sort[] sorts, int[] sortRefs) + throws Z3Exception + { + + return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), + MkSymbols(fieldNames), sorts, sortRefs); + } + + /** + * Create a new datatype sort. + **/ + public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors) + throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(constructors); + return new DatatypeSort(this, name, constructors); + } + + /** + * Create a new datatype sort. + **/ + public DatatypeSort MkDatatypeSort(String name, Constructor[] constructors) + throws Z3Exception + { + + CheckContextMatch(constructors); + return new DatatypeSort(this, MkSymbol(name), constructors); + } + + /** + * Create mutually recursive datatypes. names of + * datatype sorts list of constructors, one list per + * sort. + **/ + public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c) + throws Z3Exception + { + + CheckContextMatch(names); + int n = (int) names.length; + ConstructorList[] cla = new ConstructorList[n]; + long[] n_constr = new long[n]; + for (int i = 0; i < n; i++) + { + Constructor[] constructor = c[i]; + + CheckContextMatch(constructor); + cla[i] = new ConstructorList(this, constructor); + n_constr[i] = cla[i].NativeObject(); + } + long[] n_res = new long[n]; + Native.mkDatatypes(nCtx(), n, Symbol.ArrayToNative(names), n_res, + n_constr); + DatatypeSort[] res = new DatatypeSort[n]; + for (int i = 0; i < n; i++) + res[i] = new DatatypeSort(this, n_res[i]); + return res; + } + + /** + * Create mutually recursive data-types. + * + * @return + **/ + public DatatypeSort[] MkDatatypeSorts(String[] names, Constructor[][] c) + throws Z3Exception + { + + return MkDatatypeSorts(MkSymbols(names), c); + } + + /** + * Creates a new function declaration. + **/ + public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range) + throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(domain); + CheckContextMatch(range); + return new FuncDecl(this, name, domain, range); + } + + /** + * Creates a new function declaration. + **/ + public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range) + throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(domain); + CheckContextMatch(range); + Sort[] q = new Sort[] { domain }; + return new FuncDecl(this, name, q, range); + } + + /** + * Creates a new function declaration. + **/ + public FuncDecl MkFuncDecl(String name, Sort[] domain, Sort range) + throws Z3Exception + { + + CheckContextMatch(domain); + CheckContextMatch(range); + return new FuncDecl(this, MkSymbol(name), domain, range); + } + + /** + * Creates a new function declaration. + **/ + public FuncDecl MkFuncDecl(String name, Sort domain, Sort range) + throws Z3Exception + { + + CheckContextMatch(domain); + CheckContextMatch(range); + Sort[] q = new Sort[] { domain }; + return new FuncDecl(this, MkSymbol(name), q, range); + } + + /** + * Creates a fresh function declaration with a name prefixed with . + **/ + public FuncDecl MkFreshFuncDecl(String prefix, Sort[] domain, Sort range) + throws Z3Exception + { + + CheckContextMatch(domain); + CheckContextMatch(range); + return new FuncDecl(this, prefix, domain, range); + } + + /** + * Creates a new constant function declaration. + **/ + public FuncDecl MkConstDecl(Symbol name, Sort range) throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(range); + return new FuncDecl(this, name, null, range); + } + + /** + * Creates a new constant function declaration. + **/ + public FuncDecl MkConstDecl(String name, Sort range) throws Z3Exception + { + + CheckContextMatch(range); + return new FuncDecl(this, MkSymbol(name), null, range); + } + + /** + * Creates a fresh constant function declaration with a name prefixed with + * . + * + **/ + public FuncDecl MkFreshConstDecl(String prefix, Sort range) + throws Z3Exception + { + + CheckContextMatch(range); + return new FuncDecl(this, prefix, null, range); + } + + /** + * Creates a new bound variable. The de-Bruijn index of + * the variable The sort of the variable + **/ + public Expr MkBound(int index, Sort ty) throws Z3Exception + { + return Expr.Create(this, + Native.mkBound(nCtx(), index, ty.NativeObject())); + } + + /** + * Create a quantifier pattern. + **/ + public Pattern MkPattern(Expr[] terms) throws Z3Exception + { + if (terms.length == 0) + throw new Z3Exception("Cannot create a pattern from zero terms"); + + long[] termsNative = AST.ArrayToNative(terms); + return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length, + termsNative)); + } + + /** + * Creates a new Constant of sort and named + * . + **/ + public Expr MkConst(Symbol name, Sort range) throws Z3Exception + { + + CheckContextMatch(name); + CheckContextMatch(range); + + return Expr.Create( + this, + Native.mkConst(nCtx(), name.NativeObject(), + range.NativeObject())); + } + + /** + * Creates a new Constant of sort and named + * . + **/ + public Expr MkConst(String name, Sort range) throws Z3Exception + { + + return MkConst(MkSymbol(name), range); + } + + /** + * Creates a fresh Constant of sort and a name + * prefixed with . + **/ + public Expr MkFreshConst(String prefix, Sort range) throws Z3Exception + { + + CheckContextMatch(range); + return Expr.Create(this, + Native.mkFreshConst(nCtx(), prefix, range.NativeObject())); + } + + /** + * Creates a fresh constant from the FuncDecl . A decl of a 0-arity function + **/ + public Expr MkConst(FuncDecl f) throws Z3Exception + { + + return MkApp(f, (Expr) null); + } + + /** + * Create a Boolean constant. + **/ + public BoolExpr MkBoolConst(Symbol name) throws Z3Exception + { + + return (BoolExpr) MkConst(name, BoolSort()); + } + + /** + * Create a Boolean constant. + **/ + public BoolExpr MkBoolConst(String name) throws Z3Exception + { + + return (BoolExpr) MkConst(MkSymbol(name), BoolSort()); + } + + /** + * Creates an integer constant. + **/ + public IntExpr MkIntConst(Symbol name) throws Z3Exception + { + + return (IntExpr) MkConst(name, IntSort()); + } + + /** + * Creates an integer constant. + **/ + public IntExpr MkIntConst(String name) throws Z3Exception + { + + return (IntExpr) MkConst(name, IntSort()); + } + + /** + * Creates a real constant. + **/ + public RealExpr MkRealConst(Symbol name) throws Z3Exception + { + + return (RealExpr) MkConst(name, RealSort()); + } + + /** + * Creates a real constant. + **/ + public RealExpr MkRealConst(String name) throws Z3Exception + { + + return (RealExpr) MkConst(name, RealSort()); + } + + /** + * Creates a bit-vector constant. + **/ + public BitVecExpr MkBVConst(Symbol name, int size) throws Z3Exception + { + + return (BitVecExpr) MkConst(name, MkBitVecSort(size)); + } + + /** + * Creates a bit-vector constant. + **/ + public BitVecExpr MkBVConst(String name, int size) throws Z3Exception + { + + return (BitVecExpr) MkConst(name, MkBitVecSort(size)); + } + + /** + * Create a new function application. + **/ + public Expr MkApp(FuncDecl f, Expr arg) throws Z3Exception + { + CheckContextMatch(f); + CheckContextMatch(arg); + Expr[] args = { arg }; + return Expr.Create(this, f, args); + } + + /** + * Create a new function application. + **/ + public Expr MkApp(FuncDecl f, Expr[] args) throws Z3Exception + { + + CheckContextMatch(f); + CheckContextMatch(args); + return Expr.Create(this, f, args); + } + + /** + * The true Term. + **/ + public BoolExpr MkTrue() throws Z3Exception + { + return new BoolExpr(this, Native.mkTrue(nCtx())); + } + + /** + * The false Term. + **/ + public BoolExpr MkFalse() throws Z3Exception + { + return new BoolExpr(this, Native.mkFalse(nCtx())); + } + + /** + * Creates a Boolean value. + **/ + public BoolExpr MkBool(boolean value) throws Z3Exception + { + return value ? MkTrue() : MkFalse(); + } + + /** + * Creates the equality = . + **/ + public BoolExpr MkEq(Expr x, Expr y) throws Z3Exception + { + CheckContextMatch(x); + CheckContextMatch(y); + return new BoolExpr(this, Native.mkEq(nCtx(), x.NativeObject(), + y.NativeObject())); + } + + /** + * Creates a distinct term. + **/ + public BoolExpr MkDistinct(Expr[] args) throws Z3Exception + { + CheckContextMatch(args); + return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length, + AST.ArrayToNative(args))); + } + + /** + * Mk an expression representing not(a). + **/ + public BoolExpr MkNot(BoolExpr a) throws Z3Exception + { + + CheckContextMatch(a); + return new BoolExpr(this, Native.mkNot(nCtx(), a.NativeObject())); + } + + /** + * Create an expression representing an if-then-else: + * ite(t1, t2, t3). An expression with Boolean + * sort An expression An + * expression with the same sort as + **/ + public Expr MkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + CheckContextMatch(t3); + return Expr.Create( + this, + Native.mkIte(nCtx(), t1.NativeObject(), t2.NativeObject(), + t3.NativeObject())); + } + + /** + * Create an expression representing t1 iff t2. + **/ + public BoolExpr MkIff(BoolExpr t1, BoolExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkIff(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 -> t2. + **/ + public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkImplies(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 xor t2. + **/ + public BoolExpr MkXor(BoolExpr t1, BoolExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkXor(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t[0] and t[1] and .... + **/ + public BoolExpr MkAnd(BoolExpr[] t) throws Z3Exception + { + + CheckContextMatch(t); + return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, + AST.ArrayToNative(t))); + } + + /** + * Create an expression representing t[0] or t[1] or .... + **/ + public BoolExpr MkOr(BoolExpr[] t) throws Z3Exception + { + + CheckContextMatch(t); + return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, + AST.ArrayToNative(t))); + } + + /** + * Create an expression representing t[0] + t[1] + .... + **/ + public ArithExpr MkAdd(ArithExpr[] t) throws Z3Exception + { + + CheckContextMatch(t); + return (ArithExpr) Expr.Create(this, + Native.mkAdd(nCtx(), (int) t.length, AST.ArrayToNative(t))); + } + + /** + * Create an expression representing t[0] * t[1] * .... + **/ + public ArithExpr MkMul(ArithExpr[] t) throws Z3Exception + { + + CheckContextMatch(t); + return (ArithExpr) Expr.Create(this, + Native.mkMul(nCtx(), (int) t.length, AST.ArrayToNative(t))); + } + + /** + * Create an expression representing t[0] - t[1] - .... + **/ + public ArithExpr MkSub(ArithExpr[] t) throws Z3Exception + { + + CheckContextMatch(t); + return (ArithExpr) Expr.Create(this, + Native.mkSub(nCtx(), (int) t.length, AST.ArrayToNative(t))); + } + + /** + * Create an expression representing -t. + **/ + public ArithExpr MkUnaryMinus(ArithExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return (ArithExpr) Expr.Create(this, + Native.mkUnaryMinus(nCtx(), t.NativeObject())); + } + + /** + * Create an expression representing t1 / t2. + **/ + public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return (ArithExpr) Expr.Create(this, + Native.mkDiv(nCtx(), t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create an expression representing t1 mod t2. The + * arguments must have int type. + **/ + public IntExpr MkMod(IntExpr t1, IntExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new IntExpr(this, Native.mkMod(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 rem t2. The + * arguments must have int type. + **/ + public IntExpr MkRem(IntExpr t1, IntExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new IntExpr(this, Native.mkRem(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 ^ t2. + **/ + public ArithExpr MkPower(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return (ArithExpr) Expr.Create(this, + Native.mkPower(nCtx(), t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create an expression representing t1 < t2 + **/ + public BoolExpr MkLt(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkLt(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 <= t2 + **/ + public BoolExpr MkLe(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkLe(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 > t2 + **/ + public BoolExpr MkGt(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkGt(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create an expression representing t1 >= t2 + **/ + public BoolExpr MkGe(ArithExpr t1, ArithExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkGe(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Coerce an integer to a real. There is also a converse operation + * exposed. It follows the semantics prescribed by the SMT-LIB standard. + * + * You can take the floor of a real by creating an auxiliary integer Term + * k and and asserting + * MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument + * must be of integer sort. + **/ + public RealExpr MkInt2Real(IntExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new RealExpr(this, Native.mkInt2real(nCtx(), t.NativeObject())); + } + + /** + * Coerce a real to an integer. The semantics of this function + * follows the SMT-LIB standard for the function to_int. The argument must + * be of real sort. + **/ + public IntExpr MkReal2Int(RealExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new IntExpr(this, Native.mkReal2int(nCtx(), t.NativeObject())); + } + + /** + * Creates an expression that checks whether a real number is an integer. + **/ + public BoolExpr MkIsInteger(RealExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BoolExpr(this, Native.mkIsInt(nCtx(), t.NativeObject())); + } + + /** + * Bitwise negation. The argument must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVNot(BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.NativeObject())); + } + + /** + * Take conjunction of bits in a vector, return vector of length 1. + * The argument must have a bit-vector sort. + **/ + public BitVecExpr MkBVRedAND(BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkBvredand(nCtx(), t.NativeObject())); + } + + /** + * Take disjunction of bits in a vector, return vector of length 1. + * The argument must have a bit-vector sort. + **/ + public BitVecExpr MkBVRedOR(BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkBvredor(nCtx(), t.NativeObject())); + } + + /** + * Bitwise conjunction. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvand(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bitwise disjunction. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bitwise XOR. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvxor(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bitwise NAND. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvnand(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bitwise NOR. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvnor(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bitwise XNOR. The arguments must have a bit-vector + * sort. + **/ + public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvxnor(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Standard two's complement unary minus. The arguments must have a + * bit-vector sort. + **/ + public BitVecExpr MkBVNeg(BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.NativeObject())); + } + + /** + * Two's complement addition. The arguments must have the same + * bit-vector sort. + **/ + public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvadd(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement subtraction. The arguments must have the same + * bit-vector sort. + **/ + public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvsub(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement multiplication. The arguments must have the + * same bit-vector sort. + **/ + public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvmul(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned division. It is defined as the floor of + * t1/t2 if \c t2 is different from zero. If t2 is + * zero, then the result is undefined. The arguments must have the same + * bit-vector sort. + **/ + public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvudiv(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Signed division. It is defined in the following way: + * + * - The \c floor of t1/t2 if \c t2 is different from zero, and + * t1*t2 >= 0. + * + * - The \c ceiling of t1/t2 if \c t2 is different from zero, + * and t1*t2 < 0. + * + * If t2 is zero, then the result is undefined. The arguments + * must have the same bit-vector sort. + **/ + public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvsdiv(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned remainder. It is defined as + * t1 - (t1 /u t2) * t2, where /u represents + * unsigned division. If t2 is zero, then the result is + * undefined. The arguments must have the same bit-vector sort. + **/ + public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvurem(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Signed remainder. It is defined as + * t1 - (t1 /s t2) * t2, where /s represents + * signed division. The most significant bit (sign) of the result is equal + * to the most significant bit of \c t1. + * + * If t2 is zero, then the result is undefined. The arguments + * must have the same bit-vector sort. + **/ + public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvsrem(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement signed remainder (sign follows divisor). If + * t2 is zero, then the result is undefined. The arguments must + * have the same bit-vector sort. + **/ + public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvsmod(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned less-than The arguments must have the same bit-vector + * sort. + **/ + public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvult(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement signed less-than The arguments must have the + * same bit-vector sort. + **/ + public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned less-than or equal to. The arguments must have the + * same bit-vector sort. + **/ + public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvule(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement signed less-than or equal to. The arguments + * must have the same bit-vector sort. + **/ + public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned greater than or equal to. The arguments must have the + * same bit-vector sort. + **/ + public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement signed greater than or equal to. The arguments + * must have the same bit-vector sort. + **/ + public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Unsigned greater-than. The arguments must have the same + * bit-vector sort. + **/ + public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Two's complement signed greater-than. The arguments must have + * the same bit-vector sort. + **/ + public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bit-vector concatenation. The arguments must have a bit-vector + * sort. + * + * @return The result is a bit-vector of size n1+n2, where + * n1 (n2) is the size of t1 + * (t2). + * + **/ + public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkConcat(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Bit-vector extraction. Extract the bits + * down to from a bitvector of size m to + * yield a new bitvector of size n, where + * n = high - low + 1. The argument must + * have a bit-vector sort. + **/ + public BitVecExpr MkExtract(int high, int low, BitVecExpr t) + throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low, + t.NativeObject())); + } + + /** + * Bit-vector sign extension. Sign-extends the given bit-vector to + * the (signed) equivalent bitvector of size m+i, where \c m is + * the size of the given bit-vector. The argument must + * have a bit-vector sort. + **/ + public BitVecExpr MkSignExt(int i, BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, + t.NativeObject())); + } + + /** + * Bit-vector zero extension. Extend the given bit-vector with + * zeros to the (unsigned) equivalent bitvector of size m+i, + * where \c m is the size of the given bit-vector. The argument must have a bit-vector sort. + **/ + public BitVecExpr MkZeroExt(int i, BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, + t.NativeObject())); + } + + /** + * Bit-vector repetition. The argument must + * have a bit-vector sort. + **/ + public BitVecExpr MkRepeat(int i, BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, + Native.mkRepeat(nCtx(), i, t.NativeObject())); + } + + /** + * Shift left. It is equivalent to multiplication by + * 2^x where \c x is the value of . + * + * NB. The semantics of shift operations varies between environments. This + * definition does not necessarily capture directly the semantics of the + * programming language or assembly architecture you are modeling. + * + * The arguments must have a bit-vector sort. + **/ + public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvshl(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Logical shift right It is equivalent to unsigned division by + * 2^x where \c x is the value of . + * + * NB. The semantics of shift operations varies between environments. This + * definition does not necessarily capture directly the semantics of the + * programming language or assembly architecture you are modeling. + * + * The arguments must have a bit-vector sort. + **/ + public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvlshr(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Arithmetic shift right It is like logical shift right except + * that the most significant bits of the result always copy the most + * significant bit of the second argument. + * + * NB. The semantics of shift operations varies between environments. This + * definition does not necessarily capture directly the semantics of the + * programming language or assembly architecture you are modeling. + * + * The arguments must have a bit-vector sort. + **/ + public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkBvashr(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Rotate Left. Rotate bits of \c t to the left \c i times. The + * argument must have a bit-vector sort. + **/ + public BitVecExpr MkBVRotateLeft(int i, BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, + t.NativeObject())); + } + + /** + * Rotate Right. Rotate bits of \c t to the right \c i times. The + * argument must have a bit-vector sort. + **/ + public BitVecExpr MkBVRotateRight(int i, BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, + t.NativeObject())); + } + + /** + * Rotate Left. Rotate bits of to the left + * times. The arguments must have the same bit-vector + * sort. + **/ + public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Rotate Right. Rotate bits of to the + * right times. The arguments must have the same + * bit-vector sort. + **/ + public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create an bit bit-vector from the integer argument + * . NB. This function is essentially treated + * as uninterpreted. So you cannot expect Z3 to precisely reflect the + * semantics of this function when solving constraints with this function. + * + * The argument must be of integer sort. + **/ + public BitVecExpr MkInt2BV(int n, IntExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BitVecExpr(this, + Native.mkInt2bv(nCtx(), n, t.NativeObject())); + } + + /** + * Create an integer from the bit-vector argument . + * If \c is_signed is false, then the bit-vector \c t1 is treated + * as unsigned. So the result is non-negative and in the range + * [0..2^N-1], where N are the number of bits in . If \c is_signed is true, \c t1 is treated as a signed + * bit-vector. + * + * NB. This function is essentially treated as uninterpreted. So you cannot + * expect Z3 to precisely reflect the semantics of this function when + * solving constraints with this function. + * + * The argument must be of bit-vector sort. + **/ + public IntExpr MkBV2Int(BitVecExpr t, boolean signed) throws Z3Exception + { + + CheckContextMatch(t); + return new IntExpr(this, Native.mkBv2int(nCtx(), t.NativeObject(), + (signed) ? true : false)); + } + + /** + * Create a predicate that checks that the bit-wise addition does not + * overflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, + boolean isSigned) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, + Native.mkBvaddNoOverflow(nCtx(), t1.NativeObject(), + t2.NativeObject(), (isSigned) ? true : false)); + } + + /** + * Create a predicate that checks that the bit-wise addition does not + * underflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create a predicate that checks that the bit-wise subtraction does not + * overflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create a predicate that checks that the bit-wise subtraction does not + * underflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, + boolean isSigned) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, + Native.mkBvsubNoUnderflow(nCtx(), t1.NativeObject(), + t2.NativeObject(), (isSigned) ? true : false)); + } + + /** + * Create a predicate that checks that the bit-wise signed division does not + * overflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create a predicate that checks that the bit-wise negation does not + * overflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVNegNoOverflow(BitVecExpr t) throws Z3Exception + { + + CheckContextMatch(t); + return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), + t.NativeObject())); + } + + /** + * Create a predicate that checks that the bit-wise multiplication does not + * overflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, + boolean isSigned) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, + Native.mkBvmulNoOverflow(nCtx(), t1.NativeObject(), + t2.NativeObject(), (isSigned) ? true : false)); + } + + /** + * Create a predicate that checks that the bit-wise multiplication does not + * underflow. The arguments must be of bit-vector sort. + **/ + public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) + throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create an array constant. + **/ + public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range) + throws Z3Exception + { + + return (ArrayExpr) MkConst(name, MkArraySort(domain, range)); + } + + /** + * Create an array constant. + **/ + public ArrayExpr MkArrayConst(String name, Sort domain, Sort range) + throws Z3Exception + { + + return (ArrayExpr) MkConst(MkSymbol(name), MkArraySort(domain, range)); + } + + /** + * Array read. The argument a is the array and + * i is the index of the array that gets read. + * + * The node a must have an array sort + * [domain -> range], and i must have the sort + * domain. The sort of the result is range. + * + **/ + public Expr MkSelect(ArrayExpr a, Expr i) throws Z3Exception + { + + CheckContextMatch(a); + CheckContextMatch(i); + return Expr.Create(this, + Native.mkSelect(nCtx(), a.NativeObject(), i.NativeObject())); + } + + /** + * Array update. The node a must have an array sort + * [domain -> range], i must have sort + * domain, v must have sort range. The sort of the + * result is [domain -> range]. The semantics of this function + * is given by the theory of arrays described in the SMT-LIB standard. See + * http://smtlib.org for more details. The result of this function is an + * array that is equal to a (with respect to + * select) on all indices except for i, where it + * maps to v (and the select of a + * with respect to i may be a different value). + **/ + public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v) throws Z3Exception + { + + CheckContextMatch(a); + CheckContextMatch(i); + CheckContextMatch(v); + return new ArrayExpr(this, Native.mkStore(nCtx(), a.NativeObject(), + i.NativeObject(), v.NativeObject())); + } + + /** + * Create a constant array. The resulting term is an array, such + * that a selecton an arbitrary index produces the value + * v. + * + **/ + public ArrayExpr MkConstArray(Sort domain, Expr v) throws Z3Exception + { + + CheckContextMatch(domain); + CheckContextMatch(v); + return new ArrayExpr(this, Native.mkConstArray(nCtx(), + domain.NativeObject(), v.NativeObject())); + } + + /** + * Maps f on the argument arrays. Eeach element of + * args must be of an array sort + * [domain_i -> range_i]. The function declaration + * f must have type range_1 .. range_n -> range. + * v must have sort range. The sort of the result is + * [domain_i -> range]. + **/ + public ArrayExpr MkMap(FuncDecl f, ArrayExpr[] args) throws Z3Exception + { + + CheckContextMatch(f); + CheckContextMatch(args); + return (ArrayExpr) Expr.Create(this, Native.mkMap(nCtx(), + f.NativeObject(), AST.ArrayLength(args), + AST.ArrayToNative(args))); + } + + /** + * Access the array default value. Produces the default range + * value, for arrays that can be represented as finite maps with a default + * range value. + **/ + public Expr MkTermArray(ArrayExpr array) throws Z3Exception + { + + CheckContextMatch(array); + return Expr.Create(this, + Native.mkArrayDefault(nCtx(), array.NativeObject())); + } + + /** + * Create a set type. + **/ + public SetSort MkSetSort(Sort ty) throws Z3Exception + { + + CheckContextMatch(ty); + return new SetSort(this, ty); + } + + /** + * Create an empty set. + **/ + public Expr MkEmptySet(Sort domain) throws Z3Exception + { + + CheckContextMatch(domain); + return Expr.Create(this, + Native.mkEmptySet(nCtx(), domain.NativeObject())); + } + + /** + * Create the full set. + **/ + public Expr MkFullSet(Sort domain) throws Z3Exception + { + + CheckContextMatch(domain); + return Expr.Create(this, + Native.mkFullSet(nCtx(), domain.NativeObject())); + } + + /** + * Add an element to the set. + **/ + public Expr MkSetAdd(Expr set, Expr element) throws Z3Exception + { + + CheckContextMatch(set); + CheckContextMatch(element); + return Expr.Create( + this, + Native.mkSetAdd(nCtx(), set.NativeObject(), + element.NativeObject())); + } + + /** + * Remove an element from a set. + **/ + public Expr MkSetDel(Expr set, Expr element) throws Z3Exception + { + + CheckContextMatch(set); + CheckContextMatch(element); + return Expr.Create( + this, + Native.mkSetDel(nCtx(), set.NativeObject(), + element.NativeObject())); + } + + /** + * Take the union of a list of sets. + **/ + public Expr MkSetUnion(Expr[] args) throws Z3Exception + { + + CheckContextMatch(args); + return Expr.Create( + this, + Native.mkSetUnion(nCtx(), (int) args.length, + AST.ArrayToNative(args))); + } + + /** + * Take the intersection of a list of sets. + **/ + public Expr MkSetIntersection(Expr[] args) throws Z3Exception + { + + CheckContextMatch(args); + return Expr.Create( + this, + Native.mkSetIntersect(nCtx(), (int) args.length, + AST.ArrayToNative(args))); + } + + /** + * Take the difference between two sets. + **/ + public Expr MkSetDifference(Expr arg1, Expr arg2) throws Z3Exception + { + + CheckContextMatch(arg1); + CheckContextMatch(arg2); + return Expr.Create( + this, + Native.mkSetDifference(nCtx(), arg1.NativeObject(), + arg2.NativeObject())); + } + + /** + * Take the complement of a set. + **/ + public Expr MkSetComplement(Expr arg) throws Z3Exception + { + + CheckContextMatch(arg); + return Expr.Create(this, + Native.mkSetComplement(nCtx(), arg.NativeObject())); + } + + /** + * Check for set membership. + **/ + public Expr MkSetMembership(Expr elem, Expr set) throws Z3Exception + { + + CheckContextMatch(elem); + CheckContextMatch(set); + return Expr.Create( + this, + Native.mkSetMember(nCtx(), elem.NativeObject(), + set.NativeObject())); + } + + /** + * Check for subsetness of sets. + **/ + public Expr MkSetSubset(Expr arg1, Expr arg2) throws Z3Exception + { + + CheckContextMatch(arg1); + CheckContextMatch(arg2); + return Expr.Create( + this, + Native.mkSetSubset(nCtx(), arg1.NativeObject(), + arg2.NativeObject())); + } + + /** + * Create a Term of a given sort. A string representing the + * Term value in decimal notation. If the given sort is a real, then the + * Term can be a rational, that is, a string of the form + * [num]* / [num]*. The sort of the + * numeral. In the current implementation, the given sort can be an int, + * real, or bit-vectors of arbitrary size. + * + * @return A Term with value and sort + **/ + public Expr MkNumeral(String v, Sort ty) throws Z3Exception + { + + CheckContextMatch(ty); + return Expr + .Create(this, Native.mkNumeral(nCtx(), v, ty.NativeObject())); + } + + /** + * Create a Term of a given sort. This function can be use to create + * numerals that fit in a machine integer. It is slightly faster than + * MakeNumeral since it is not necessary to parse a string. + * Value of the numeral Sort of the + * numeral + * + * @return A Term with value and type + **/ + public Expr MkNumeral(int v, Sort ty) throws Z3Exception + { + + CheckContextMatch(ty); + return Expr.Create(this, Native.mkInt(nCtx(), v, ty.NativeObject())); + } + + /** + * Create a Term of a given sort. This function can be use to create + * numerals that fit in a machine integer. It is slightly faster than + * MakeNumeral since it is not necessary to parse a string. + * Value of the numeral Sort of the + * numeral + * + * @return A Term with value and type + **/ + public Expr MkNumeral(long v, Sort ty) throws Z3Exception + { + + CheckContextMatch(ty); + return Expr.Create(this, Native.mkInt64(nCtx(), v, ty.NativeObject())); + } + + /** + * Create a real from a fraction. numerator of + * rational. denominator of rational. + * + * @return A Term with value / + * and sort Real + **/ + public RatNum MkReal(int num, int den) throws Z3Exception + { + if (den == 0) + throw new Z3Exception("Denominator is zero"); + + return new RatNum(this, Native.mkReal(nCtx(), num, den)); + } + + /** + * Create a real numeral. A string representing the Term + * value in decimal notation. + * + * @return A Term with value and sort Real + **/ + public RatNum MkReal(String v) throws Z3Exception + { + + return new RatNum(this, Native.mkNumeral(nCtx(), v, RealSort() + .NativeObject())); + } + + /** + * Create a real numeral. value of the numeral. + * + * @return A Term with value and sort Real + **/ + public RatNum MkReal(int v) throws Z3Exception + { + + return new RatNum(this, Native.mkInt(nCtx(), v, RealSort() + .NativeObject())); + } + + /** + * Create a real numeral. value of the numeral. + * + * @return A Term with value and sort Real + **/ + public RatNum MkReal(long v) throws Z3Exception + { + + return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort() + .NativeObject())); + } + + /** + * Create an integer numeral. A string representing the Term + * value in decimal notation. + **/ + public IntNum MkInt(String v) throws Z3Exception + { + + return new IntNum(this, Native.mkNumeral(nCtx(), v, IntSort() + .NativeObject())); + } + + /** + * Create an integer numeral. value of the numeral. + * + * @return A Term with value and sort Integer + **/ + public IntNum MkInt(int v) throws Z3Exception + { + + return new IntNum(this, Native.mkInt(nCtx(), v, IntSort() + .NativeObject())); + } + + /** + * Create an integer numeral. value of the numeral. + * + * @return A Term with value and sort Integer + **/ + public IntNum MkInt(long v) throws Z3Exception + { + + return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort() + .NativeObject())); + } + + /** + * Create a bit-vector numeral. A string representing the + * value in decimal notation. the size of the + * bit-vector + **/ + public BitVecNum MkBV(String v, int size) throws Z3Exception + { + + return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); + } + + /** + * Create a bit-vector numeral. value of the + * numeral. the size of the bit-vector + **/ + public BitVecNum MkBV(int v, int size) throws Z3Exception + { + + return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); + } + + /** + * Create a bit-vector numeral. value of the + * numeral. * the size of the bit-vector + **/ + public BitVecNum MkBV(long v, int size) throws Z3Exception + { + + return (BitVecNum) MkNumeral(v, MkBitVecSort(size)); + } + + /** + * Create a universal Quantifier. Creates a forall formula, where + * is the weight, is + * an array of patterns, is an array with the sorts + * of the bound variables, is an array with the + * 'names' of the bound variables, and is the body + * of the quantifier. Quantifiers are associated with weights indicating the + * importance of using the quantifier during instantiation. + * the sorts of the bound variables. names of the bound variables the + * body of the quantifier. quantifiers are + * associated with weights indicating the importance of using the quantifier + * during instantiation. By default, pass the weight 0. array containing the patterns created using + * MkPattern. array containing + * the anti-patterns created using MkPattern. optional symbol to track quantifier. optional symbol to track skolem constants. + **/ + public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, + int weight, Pattern[] patterns, Expr[] noPatterns, + Symbol quantifierID, Symbol skolemID) throws Z3Exception + { + + return new Quantifier(this, true, sorts, names, body, weight, patterns, + noPatterns, quantifierID, skolemID); + } + + /** + * Create a universal Quantifier. + **/ + public Quantifier MkForall(Expr[] boundConstants, Expr body, int weight, + Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, + Symbol skolemID) throws Z3Exception + { + + return new Quantifier(this, true, boundConstants, body, weight, + patterns, noPatterns, quantifierID, skolemID); + } + + /** + * Create an existential Quantifier. + **/ + public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, + int weight, Pattern[] patterns, Expr[] noPatterns, + Symbol quantifierID, Symbol skolemID) throws Z3Exception + { + + return new Quantifier(this, false, sorts, names, body, weight, + patterns, noPatterns, quantifierID, skolemID); + } + + /** + * Create an existential Quantifier. + **/ + public Quantifier MkExists(Expr[] boundConstants, Expr body, int weight, + Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, + Symbol skolemID) throws Z3Exception + { + + return new Quantifier(this, false, boundConstants, body, weight, + patterns, noPatterns, quantifierID, skolemID); + } + + /** + * Create a Quantifier. + **/ + public Quantifier MkQuantifier(boolean universal, Sort[] sorts, + Symbol[] names, Expr body, int weight, Pattern[] patterns, + Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + throws Z3Exception + { + + if (universal) + return MkForall(sorts, names, body, weight, patterns, noPatterns, + quantifierID, skolemID); + else + return MkExists(sorts, names, body, weight, patterns, noPatterns, + quantifierID, skolemID); + } + + /** + * Create a Quantifier. + **/ + public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, + Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, + Symbol quantifierID, Symbol skolemID) throws Z3Exception + { + + if (universal) + return MkForall(boundConstants, body, weight, patterns, noPatterns, + quantifierID, skolemID); + else + return MkExists(boundConstants, body, weight, patterns, noPatterns, + quantifierID, skolemID); + } + + /** + * Selects the format used for pretty-printing expressions. The + * default mode for pretty printing expressions is to produce SMT-LIB style + * output where common subexpressions are printed at each occurrence. The + * mode is called Z3_PRINT_SMTLIB_FULL. To print shared common + * subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in + * way that conforms to SMT-LIB standards and uses let expressions to share + * common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. + **/ + public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception + { + Native.setAstPrintMode(nCtx(), value.toInt()); + } + + /** + * Convert a benchmark into an SMT-LIB formatted string. Name of the benchmark. The argument is optional. + * The benchmark logic. The status string (sat, unsat, or unknown) Other attributes, such as source, difficulty or + * category. Auxiliary + * assumptions. Formula to be checked for + * consistency in conjunction with assumptions. + * + * @return A string representation of the benchmark. + **/ + public String BenchmarkToSMTString(String name, String logic, + String status, String attributes, BoolExpr[] assumptions, + BoolExpr formula) throws Z3Exception + { + + return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, + attributes, (int) assumptions.length, + AST.ArrayToNative(assumptions), formula.NativeObject()); + } + + /** + * Parse the given string using the SMT-LIB parser. The symbol + * table of the parser can be initialized using the given sorts and + * declarations. The symbols in the arrays and + * don't need to match the names of the sorts + * and declarations in the arrays and . This is a useful feature since we can use arbitrary names + * to reference sorts and declarations. + **/ + public void ParseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, + Symbol[] declNames, FuncDecl[] decls) throws Z3Exception + { + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + Native.parseSmtlibString(nCtx(), str, AST.ArrayLength(sorts), + Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), + AST.ArrayToNative(decls)); + } + + /** + * Parse the given file using the SMT-LIB parser. + **/ + public void ParseSMTLIBFile(String fileName, Symbol[] sortNames, + Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) + throws Z3Exception + { + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + Native.parseSmtlibFile(nCtx(), fileName, AST.ArrayLength(sorts), + Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), + AST.ArrayToNative(decls)); + } + + /** + * The number of SMTLIB formulas parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public int NumSMTLIBFormulas() throws Z3Exception + { + return Native.getSmtlibNumFormulas(nCtx()); + } + + /** + * The formulas parsed by the last call to ParseSMTLIBString or + * ParseSMTLIBFile. + **/ + public BoolExpr[] SMTLIBFormulas() throws Z3Exception + { + + int n = NumSMTLIBFormulas(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (BoolExpr) Expr.Create(this, + Native.getSmtlibFormula(nCtx(), i)); + return res; + } + + /** + * The number of SMTLIB assumptions parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public int NumSMTLIBAssumptions() throws Z3Exception + { + return Native.getSmtlibNumAssumptions(nCtx()); + } + + /** + * The assumptions parsed by the last call to ParseSMTLIBString + * or ParseSMTLIBFile. + **/ + public BoolExpr[] SMTLIBAssumptions() throws Z3Exception + { + + int n = NumSMTLIBAssumptions(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (BoolExpr) Expr.Create(this, + Native.getSmtlibAssumption(nCtx(), i)); + return res; + } + + /** + * The number of SMTLIB declarations parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public int NumSMTLIBDecls() throws Z3Exception + { + return Native.getSmtlibNumDecls(nCtx()); + } + + /** + * The declarations parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public FuncDecl[] SMTLIBDecls() throws Z3Exception + { + + int n = NumSMTLIBDecls(); + FuncDecl[] res = new FuncDecl[n]; + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i)); + return res; + } + + /** + * The number of SMTLIB sorts parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public int NumSMTLIBSorts() throws Z3Exception + { + return Native.getSmtlibNumSorts(nCtx()); + } + + /** + * The declarations parsed by the last call to + * ParseSMTLIBString or ParseSMTLIBFile. + **/ + public Sort[] SMTLIBSorts() throws Z3Exception + { + + int n = NumSMTLIBSorts(); + Sort[] res = new Sort[n]; + for (int i = 0; i < n; i++) + res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx(), i)); + return res; + } + + /** + * Parse the given string using the SMT-LIB2 parser. + * + * @return A conjunction of assertions in the scope (up to push/pop) at the + * end of the string. + **/ + public BoolExpr ParseSMTLIB2String(String str, Symbol[] sortNames, + Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) + throws Z3Exception + { + + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + return (BoolExpr) Expr.Create(this, Native.parseSmtlib2String(nCtx(), + str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), + AST.ArrayToNative(sorts), AST.ArrayLength(decls), + Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); + } + + /** + * Parse the given file using the SMT-LIB2 parser. + **/ + public BoolExpr ParseSMTLIB2File(String fileName, Symbol[] sortNames, + Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) + throws Z3Exception + { + + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + return (BoolExpr) Expr.Create(this, Native.parseSmtlib2File(nCtx(), + fileName, AST.ArrayLength(sorts), + Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), + AST.ArrayToNative(decls))); + } + + /** + * Creates a new Goal. Note that the Context must have been + * created with proof generation support if is set + * to true here. Indicates whether model + * generation should be enabled. Indicates + * whether unsat core generation should be enabled. Indicates whether proof generation should be + * enabled. + **/ + public Goal MkGoal(boolean models, boolean unsatCores, boolean proofs) + throws Z3Exception + { + + return new Goal(this, models, unsatCores, proofs); + } + + /** + * Creates a new ParameterSet. + **/ + public Params MkParams() throws Z3Exception + { + + return new Params(this); + } + + /** + * The number of supported tactics. + **/ + public int NumTactics() throws Z3Exception + { + return Native.getNumTactics(nCtx()); + } + + /** + * The names of all supported tactics. + **/ + public String[] TacticNames() throws Z3Exception + { + + int n = NumTactics(); + String[] res = new String[n]; + for (int i = 0; i < n; i++) + res[i] = Native.getTacticName(nCtx(), i); + return res; + } + + /** + * Returns a string containing a description of the tactic with the given + * name. + **/ + public String TacticDescription(String name) throws Z3Exception + { + + return Native.tacticGetDescr(nCtx(), name); + } + + /** + * Creates a new Tactic. + **/ + public Tactic MkTactic(String name) throws Z3Exception + { + + return new Tactic(this, name); + } + + /** + * Create a tactic that applies to a Goal and then + * to every subgoal produced by . + **/ + public Tactic AndThen(Tactic t1, Tactic t2, Tactic[] ts) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + CheckContextMatch(ts); + + long last = 0; + if (ts != null && ts.length > 0) + { + last = ts[ts.length - 1].NativeObject(); + for (int i = ts.length - 2; i >= 0; i--) + last = Native.tacticAndThen(nCtx(), ts[i].NativeObject(), last); + } + if (last != 0) + { + last = Native.tacticAndThen(nCtx(), t2.NativeObject(), last); + return new Tactic(this, Native.tacticAndThen(nCtx(), + t1.NativeObject(), last)); + } else + return new Tactic(this, Native.tacticAndThen(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create a tactic that applies to a Goal and then + * to every subgoal produced by . + * Shorthand for AndThen. + **/ + public Tactic Then(Tactic t1, Tactic t2, Tactic[] ts) throws Z3Exception + { + + return AndThen(t1, t2, ts); + } + + /** + * Create a tactic that first applies to a Goal and if + * it fails then returns the result of applied to the + * Goal. + **/ + public Tactic OrElse(Tactic t1, Tactic t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new Tactic(this, Native.tacticOrElse(nCtx(), t1.NativeObject(), + t2.NativeObject())); + } + + /** + * Create a tactic that applies to a goal for milliseconds. If does not + * terminate within milliseconds, then it fails. + * + **/ + public Tactic TryFor(Tactic t, int ms) throws Z3Exception + { + + CheckContextMatch(t); + return new Tactic(this, Native.tacticTryFor(nCtx(), t.NativeObject(), + ms)); + } + + /** + * Create a tactic that applies to a given goal if the + * probe evaluates to true. If evaluates to false, then the new tactic behaves like the + * skip tactic. + **/ + public Tactic When(Probe p, Tactic t) throws Z3Exception + { + + CheckContextMatch(t); + CheckContextMatch(p); + return new Tactic(this, Native.tacticWhen(nCtx(), p.NativeObject(), + t.NativeObject())); + } + + /** + * Create a tactic that applies to a given goal if the + * probe evaluates to true and + * otherwise. + **/ + public Tactic Cond(Probe p, Tactic t1, Tactic t2) throws Z3Exception + { + + CheckContextMatch(p); + CheckContextMatch(t1); + CheckContextMatch(t2); + return new Tactic(this, Native.tacticCond(nCtx(), p.NativeObject(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Create a tactic that keeps applying until the goal + * is not modified anymore or the maximum number of iterations is reached. + **/ + public Tactic Repeat(Tactic t, int max) throws Z3Exception + { + + CheckContextMatch(t); + return new Tactic(this, Native.tacticRepeat(nCtx(), t.NativeObject(), + max)); + } + + /** + * Create a tactic that just returns the given goal. + **/ + public Tactic Skip() throws Z3Exception + { + + return new Tactic(this, Native.tacticSkip(nCtx())); + } + + /** + * Create a tactic always fails. + **/ + public Tactic Fail() throws Z3Exception + { + + return new Tactic(this, Native.tacticFail(nCtx())); + } + + /** + * Create a tactic that fails if the probe evaluates to + * false. + **/ + public Tactic FailIf(Probe p) throws Z3Exception + { + + CheckContextMatch(p); + return new Tactic(this, Native.tacticFailIf(nCtx(), p.NativeObject())); + } + + /** + * Create a tactic that fails if the goal is not triviall satisfiable (i.e., + * empty) or trivially unsatisfiable (i.e., contains `false'). + **/ + public Tactic FailIfNotDecided() throws Z3Exception + { + + return new Tactic(this, Native.tacticFailIfNotDecided(nCtx())); + } + + /** + * Create a tactic that applies using the given set of + * parameters . + **/ + public Tactic UsingParams(Tactic t, Params p) throws Z3Exception + { + + CheckContextMatch(t); + CheckContextMatch(p); + return new Tactic(this, Native.tacticUsingParams(nCtx(), + t.NativeObject(), p.NativeObject())); + } + + /** + * Create a tactic that applies using the given set of + * parameters . Alias for + * UsingParams + **/ + public Tactic With(Tactic t, Params p) throws Z3Exception + { + + return UsingParams(t, p); + } + + /** + * Create a tactic that applies the given tactics in parallel. + **/ + public Tactic ParOr(Tactic[] t) throws Z3Exception + { + + CheckContextMatch(t); + return new Tactic(this, Native.tacticParOr(nCtx(), + Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); + } + + /** + * Create a tactic that applies to a given goal and + * then to every subgoal produced by . The subgoals are processed in parallel. + **/ + public Tactic ParAndThen(Tactic t1, Tactic t2) throws Z3Exception + { + + CheckContextMatch(t1); + CheckContextMatch(t2); + return new Tactic(this, Native.tacticParAndThen(nCtx(), + t1.NativeObject(), t2.NativeObject())); + } + + /** + * Interrupt the execution of a Z3 procedure. This procedure can be + * used to interrupt: solvers, simplifiers and tactics. + **/ + public void Interrupt() throws Z3Exception + { + Native.interrupt(nCtx()); + } + + /** + * The number of supported Probes. + **/ + public int NumProbes() throws Z3Exception + { + return Native.getNumProbes(nCtx()); + } + + /** + * The names of all supported Probes. + **/ + public String[] ProbeNames() throws Z3Exception + { + + int n = NumProbes(); + String[] res = new String[n]; + for (int i = 0; i < n; i++) + res[i] = Native.getProbeName(nCtx(), i); + return res; + } + + /** + * Returns a string containing a description of the probe with the given + * name. + **/ + public String ProbeDescription(String name) throws Z3Exception + { + + return Native.probeGetDescr(nCtx(), name); + } + + /** + * Creates a new Probe. + **/ + public Probe MkProbe(String name) throws Z3Exception + { + + return new Probe(this, name); + } + + /** + * Create a probe that always evaluates to . + **/ + public Probe Const(double val) throws Z3Exception + { + + return new Probe(this, Native.probeConst(nCtx(), val)); + } + + /** + * Create a probe that evaluates to "true" when the value returned by + * is less than the value returned by + **/ + public Probe Lt(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeLt(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value returned by + * is greater than the value returned by + **/ + public Probe Gt(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeGt(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value returned by + * is less than or equal the value returned by + * + **/ + public Probe Le(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeLe(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value returned by + * is greater than or equal the value returned by + * + **/ + public Probe Ge(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeGe(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value returned by + * is equal to the value returned by + **/ + public Probe Eq(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeEq(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value and evaluate to "true". + **/ + public Probe And(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeAnd(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value or evaluate to "true". + **/ + public Probe Or(Probe p1, Probe p2) throws Z3Exception + { + + CheckContextMatch(p1); + CheckContextMatch(p2); + return new Probe(this, Native.probeOr(nCtx(), p1.NativeObject(), + p2.NativeObject())); + } + + /** + * Create a probe that evaluates to "true" when the value does not evaluate to "true". + **/ + public Probe Not(Probe p) throws Z3Exception + { + + CheckContextMatch(p); + return new Probe(this, Native.probeNot(nCtx(), p.NativeObject())); + } + + /** + * Creates a new (incremental) solver. This solver also uses a set + * of builtin tactics for handling the first check-sat command, and + * check-sat commands that take more than a given number of milliseconds to + * be solved. + **/ + public Solver MkSolver() throws Z3Exception + { + return MkSolver((Symbol) null); + } + + /** + * Creates a new (incremental) solver. This solver also uses a set + * of builtin tactics for handling the first check-sat command, and + * check-sat commands that take more than a given number of milliseconds to + * be solved. + **/ + public Solver MkSolver(Symbol logic) throws Z3Exception + { + + if (logic == null) + return new Solver(this, Native.mkSolver(nCtx())); + else + return new Solver(this, Native.mkSolverForLogic(nCtx(), + logic.NativeObject())); + } + + /** + * Creates a new (incremental) solver. + **/ + public Solver MkSolver(String logic) throws Z3Exception + { + + return MkSolver(MkSymbol(logic)); + } + + /** + * Creates a new (incremental) solver. + **/ + public Solver MkSimpleSolver() throws Z3Exception + { + + return new Solver(this, Native.mkSimpleSolver(nCtx())); + } + + /** + * Creates a solver that is implemented using the given tactic. + * The solver supports the commands Push and Pop, + * but it will always solve each check from scratch. + **/ + public Solver MkSolver(Tactic t) throws Z3Exception + { + + return new Solver(this, Native.mkSolverFromTactic(nCtx(), + t.NativeObject())); + } + + /** + * Create a Fixedpoint context. + **/ + public Fixedpoint MkFixedpoint() throws Z3Exception + { + + return new Fixedpoint(this); + } + + /** + * Wraps an AST. This function is used for transitions between + * native and managed objects. Note that + * must be a native object obtained from Z3 (e.g., through ) and that it must have a correct reference count (see + * e.g., . The native pointer to + * wrap. + **/ + public AST WrapAST(long nativeObject) throws Z3Exception + { + + return AST.Create(this, nativeObject); + } + + /** + * Unwraps an AST. This function is used for transitions between + * native and managed objects. It returns the native pointer to the AST. + * Note that AST objects are reference counted and unwrapping an AST + * disables automatic reference counting, i.e., all references to the IntPtr + * that is returned must be handled externally and through native calls (see + * e.g., ). The AST to unwrap. + **/ + public long UnwrapAST(AST a) + { + return a.NativeObject(); + } + + /** + * Return a string describing all available parameters to + * Expr.Simplify. + **/ + public String SimplifyHelp() throws Z3Exception + { + + return Native.simplifyGetHelp(nCtx()); + } + + /** + * Retrieves parameter descriptions for simplifier. + **/ + public ParamDescrs SimplifyParameterDescriptions() throws Z3Exception + { + return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx())); + } + + /** + * Enable/disable printing of warning messages to the console. Note + * that this function is static and effects the behaviour of all contexts + * globally. + **/ + public static void ToggleWarningMessages(boolean enabled) + throws Z3Exception + { + Native.toggleWarningMessages((enabled) ? true : false); + } + + // /// + // /// A delegate which is executed when an error is raised. + // /// + // /// + // /// Note that it is possible for memory leaks to occur if error handlers + // /// throw exceptions. + // /// + // public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, + // String errorString); + + // /// + // /// The OnError event. + // /// + // public event ErrorHandler OnError = null; + + /** + * Update a mutable configuration parameter. The list of all + * configuration parameters can be obtained using the Z3 executable: + * z3.exe -ini? Only a few configuration parameters are mutable + * once the context is created. An exception is thrown when trying to modify + * an immutable parameter. + **/ + public void UpdateParamValue(String id, String value) throws Z3Exception + { + Native.updateParamValue(nCtx(), id, value); + } + + /** + * Get a configuration parameter. Returns null if the parameter + * value does not exist. + **/ + public String GetParamValue(String id) throws Z3Exception + { + Native.StringPtr res = new Native.StringPtr(); + boolean r = Native.getParamValue(nCtx(), id, res); + if (!r) + return null; + else + return res.value; + } + + long m_ctx = 0; + Native.errorHandler m_n_err_handler = null; + + long nCtx() + { + return m_ctx; + } + + // void NativeErrorHandler(long ctx, Z3_error_code errorCode) + // { + // // Do-nothing error handler. The wrappers in Z3.Native will throw + // exceptions upon errors. + // } + + void InitContext() throws Z3Exception + { + setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); + // m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // + // keep reference so it doesn't get collected. + // if (m_n_err_handler != null) Native.setErrorHandler(m_ctx, + // m_n_err_handler); + } + + void CheckContextMatch(Z3Object other) throws Z3Exception + { + if (this != other.Context()) + throw new Z3Exception("Context mismatch"); + } + + void CheckContextMatch(Z3Object[] arr) throws Z3Exception + { + if (arr != null) + for (Z3Object a : arr) + CheckContextMatch(a); + } + + private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue(); + private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(); + private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(); + private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(); + private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(); + private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(); + private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(); + private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(); + private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(); + private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(); + private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(); + private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(); + private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(); + private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(); + private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(); + + ASTDecRefQueue AST_DRQ() + { + return m_AST_DRQ; + } + + ASTMapDecRefQueue ASTMap_DRQ() + { + return m_ASTMap_DRQ; + } + + ASTVectorDecRefQueue ASTVector_DRQ() + { + return m_ASTVector_DRQ; + } + + ApplyResultDecRefQueue ApplyResult_DRQ() + { + return m_ApplyResult_DRQ; + } + + FuncInterpEntryDecRefQueue FuncEntry_DRQ() + { + return m_FuncEntry_DRQ; + } + + FuncInterpDecRefQueue FuncInterp_DRQ() + { + return m_FuncInterp_DRQ; + } + + GoalDecRefQueue Goal_DRQ() + { + return m_Goal_DRQ; + } + + ModelDecRefQueue Model_DRQ() + { + return m_Model_DRQ; + } + + ParamsDecRefQueue Params_DRQ() + { + return m_Params_DRQ; + } + + ParamDescrsDecRefQueue ParamDescrs_DRQ() + { + return m_ParamDescrs_DRQ; + } + + ProbeDecRefQueue Probe_DRQ() + { + return m_Probe_DRQ; + } + + SolverDecRefQueue Solver_DRQ() + { + return m_Solver_DRQ; + } + + StatisticsDecRefQueue Statistics_DRQ() + { + return m_Statistics_DRQ; + } + + TacticDecRefQueue Tactic_DRQ() + { + return m_Tactic_DRQ; + } + + FixedpointDecRefQueue Fixedpoint_DRQ() + { + return m_Fixedpoint_DRQ; + } + + protected long m_refCount = 0; + + /** + * Finalizer. + **/ + protected void finalize() + { + Dispose(); + + if (m_refCount == 0) + { + m_n_err_handler = null; + try + { + Native.delContext(m_ctx); + } catch (Z3Exception e) + { + // OK. + } + m_ctx = 0; + } else + /* re-queue the finalizer */ + /* BUG: DRQ's need to be taken over too! */ + new Context(m_ctx, m_refCount, m_n_err_handler); + } + + /** + * Disposes of the context. + **/ + public void Dispose() + { + m_AST_DRQ.Clear(this); + m_ASTMap_DRQ.Clear(this); + m_ASTVector_DRQ.Clear(this); + m_ApplyResult_DRQ.Clear(this); + m_FuncEntry_DRQ.Clear(this); + m_FuncInterp_DRQ.Clear(this); + m_Goal_DRQ.Clear(this); + m_Model_DRQ.Clear(this); + m_Params_DRQ.Clear(this); + m_Probe_DRQ.Clear(this); + m_Solver_DRQ.Clear(this); + m_Statistics_DRQ.Clear(this); + m_Tactic_DRQ.Clear(this); + m_Fixedpoint_DRQ.Clear(this); + + m_boolSort = null; + m_intSort = null; + m_realSort = null; + } } diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index 1ff123706..7e6d002aa 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -14,7 +14,7 @@ public class DatatypeSort extends Sort /** * The number of constructors of the datatype sort. **/ - public int NumConstructors() + public int NumConstructors() throws Z3Exception { return Native.getDatatypeSortNumConstructors(Context().nCtx(), NativeObject()); diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java index 0183bec60..8c39320ad 100644 --- a/src/api/java/FiniteDomainSort.java +++ b/src/api/java/FiniteDomainSort.java @@ -14,7 +14,7 @@ public class FiniteDomainSort extends Sort /** * The size of the finite domain sort. **/ - public long Size() + public long Size() throws Z3Exception { Native.LongPtr res = new Native.LongPtr(); Native.getFiniteDomainSortSize(Context().nCtx(), NativeObject(), res); diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 860629eec..375cb7b97 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -14,314 +14,320 @@ import com.microsoft.z3.enumerations.*; public class Fixedpoint extends Z3Object { - /** - * A string that describes all available fixedpoint solver parameters. - **/ - public String Help() - { + /** + * A string that describes all available fixedpoint solver parameters. + **/ + public String Help() throws Z3Exception + { + return Native.fixedpointGetHelp(Context().nCtx(), NativeObject()); + } - return Native.fixedpointGetHelp(Context().nCtx(), NativeObject()); - } + /** + * Sets the fixedpoint solver parameters. + * + * @throws Z3Exception + **/ + public void setParameters(Params value) throws Z3Exception + { - /** - * Sets the fixedpoint solver parameters. - * - * @throws Z3Exception - **/ - public void setParameters(Params value) throws Z3Exception - { + Context().CheckContextMatch(value); + Native.fixedpointSetParams(Context().nCtx(), NativeObject(), + value.NativeObject()); + } - Context().CheckContextMatch(value); - Native.fixedpointSetParams(Context().nCtx(), NativeObject(), - value.NativeObject()); - } + /** + * Retrieves parameter descriptions for Fixedpoint solver. + * + * @throws Z3Exception + **/ + public ParamDescrs ParameterDescriptions() throws Z3Exception + { + return new ParamDescrs(Context(), Native.fixedpointGetParamDescrs( + Context().nCtx(), NativeObject())); + } - /** - * Retrieves parameter descriptions for Fixedpoint solver. - * @throws Z3Exception - **/ - public ParamDescrs ParameterDescriptions() throws Z3Exception - { - return new ParamDescrs(Context(), Native.fixedpointGetParamDescrs( - Context().nCtx(), NativeObject())); - } + /** + * Assert a constraint (or multiple) into the fixedpoint solver. + * + * @throws Z3Exception + **/ + public void Assert(BoolExpr[] constraints) throws Z3Exception + { + Context().CheckContextMatch(constraints); + for (BoolExpr a : constraints) + { + Native.fixedpointAssert(Context().nCtx(), NativeObject(), + a.NativeObject()); + } + } - /** - * Assert a constraint (or multiple) into the fixedpoint solver. - * - * @throws Z3Exception - **/ - public void Assert(BoolExpr[] constraints) throws Z3Exception - { + /** + * Register predicate as recursive relation. + * + * @throws Z3Exception + **/ + public void RegisterRelation(FuncDecl f) throws Z3Exception + { - Context().CheckContextMatch(constraints); - for (BoolExpr a : constraints) - { - Native.fixedpointAssert(Context().nCtx(), NativeObject(), - a.NativeObject()); - } - } + Context().CheckContextMatch(f); + Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), + f.NativeObject()); + } - /** - * Register predicate as recursive relation. - * - * @throws Z3Exception - **/ - public void RegisterRelation(FuncDecl f) throws Z3Exception - { + /** + * Add rule into the fixedpoint solver. + * + * @throws Z3Exception + **/ + public void AddRule(BoolExpr rule, Symbol name) throws Z3Exception + { - Context().CheckContextMatch(f); - Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), - f.NativeObject()); - } + Context().CheckContextMatch(rule); + Native.fixedpointAddRule(Context().nCtx(), NativeObject(), + rule.NativeObject(), AST.GetNativeObject(name)); + } - /** - * Add rule into the fixedpoint solver. - * - * @throws Z3Exception - **/ - public void AddRule(BoolExpr rule, Symbol name) throws Z3Exception - { + /** + * Add table fact to the fixedpoint solver. + * + * @throws Z3Exception + **/ + public void AddFact(FuncDecl pred, int[] args) throws Z3Exception + { - Context().CheckContextMatch(rule); - Native.fixedpointAddRule(Context().nCtx(), NativeObject(), - rule.NativeObject(), AST.GetNativeObject(name)); - } + Context().CheckContextMatch(pred); + Native.fixedpointAddFact(Context().nCtx(), NativeObject(), + pred.NativeObject(), (int) args.length, args); + } - /** - * Add table fact to the fixedpoint solver. - * - * @throws Z3Exception - **/ - public void AddFact(FuncDecl pred, int[] args) throws Z3Exception - { + /** + * Query the fixedpoint solver. A query is a conjunction of constraints. The + * constraints may include the recursively defined relations. The query is + * satisfiable if there is an instance of the query variables and a + * derivation for it. The query is unsatisfiable if there are no derivations + * satisfying the query variables. + * + * @throws Z3Exception + **/ + public Status Query(BoolExpr query) throws Z3Exception + { - Context().CheckContextMatch(pred); - Native.fixedpointAddFact(Context().nCtx(), NativeObject(), - pred.NativeObject(), (int) args.length, args); - } + Context().CheckContextMatch(query); + Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(Context().nCtx(), + NativeObject(), query.NativeObject())); + switch (r) + { + case Z3_L_TRUE: + return Status.SATISFIABLE; + case Z3_L_FALSE: + return Status.UNSATISFIABLE; + default: + return Status.UNKNOWN; + } + } - /** - * Query the fixedpoint solver. A query is a conjunction of constraints. The - * constraints may include the recursively defined relations. The query is - * satisfiable if there is an instance of the query variables and a - * derivation for it. The query is unsatisfiable if there are no derivations - * satisfying the query variables. - * - * @throws Z3Exception - **/ - public Status Query(BoolExpr query) throws Z3Exception - { + /** + * Query the fixedpoint solver. A query is an array of relations. The query + * is satisfiable if there is an instance of some relation that is + * non-empty. The query is unsatisfiable if there are no derivations + * satisfying any of the relations. + * + * @throws Z3Exception + **/ + public Status Query(FuncDecl[] relations) throws Z3Exception + { - Context().CheckContextMatch(query); - Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(Context().nCtx(), - NativeObject(), query.NativeObject())); - switch (r) - { - case Z3_L_TRUE: - return Status.SATISFIABLE; - case Z3_L_FALSE: - return Status.UNSATISFIABLE; - default: - return Status.UNKNOWN; - } - } + Context().CheckContextMatch(relations); + Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(Context() + .nCtx(), NativeObject(), AST.ArrayLength(relations), AST + .ArrayToNative(relations))); + switch (r) + { + case Z3_L_TRUE: + return Status.SATISFIABLE; + case Z3_L_FALSE: + return Status.UNSATISFIABLE; + default: + return Status.UNKNOWN; + } + } - /** - * Query the fixedpoint solver. A query is an array of relations. The query - * is satisfiable if there is an instance of some relation that is - * non-empty. The query is unsatisfiable if there are no derivations - * satisfying any of the relations. - * - * @throws Z3Exception - **/ - public Status Query(FuncDecl[] relations) throws Z3Exception - { + /** + * Creates a backtracking point. + **/ + public void Push() throws Z3Exception + { + Native.fixedpointPush(Context().nCtx(), NativeObject()); + } - Context().CheckContextMatch(relations); - Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(Context() - .nCtx(), NativeObject(), AST.ArrayLength(relations), AST - .ArrayToNative(relations))); - switch (r) - { - case Z3_L_TRUE: - return Status.SATISFIABLE; - case Z3_L_FALSE: - return Status.UNSATISFIABLE; - default: - return Status.UNKNOWN; - } - } + /** + * Backtrack one backtracking point. Note that an exception is + * thrown if Pop is called without a corresponding Push + * + **/ + public void Pop() throws Z3Exception + { + Native.fixedpointPop(Context().nCtx(), NativeObject()); + } - /** - * Creates a backtracking point. - **/ - public void Push() - { - Native.fixedpointPush(Context().nCtx(), NativeObject()); - } + /** + * Update named rule into in the fixedpoint solver. + * + * @throws Z3Exception + **/ + public void UpdateRule(BoolExpr rule, Symbol name) throws Z3Exception + { - /** - * Backtrack one backtracking point. Note that an exception is - * thrown if Pop is called without a corresponding Push - * - **/ - public void Pop() - { - Native.fixedpointPop(Context().nCtx(), NativeObject()); - } + Context().CheckContextMatch(rule); + Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), + rule.NativeObject(), AST.GetNativeObject(name)); + } - /** - * Update named rule into in the fixedpoint solver. - * - * @throws Z3Exception - **/ - public void UpdateRule(BoolExpr rule, Symbol name) throws Z3Exception - { + /** + * Retrieve satisfying instance or instances of solver, or definitions for + * the recursive predicates that show unsatisfiability. + * + * @throws Z3Exception + **/ + public Expr GetAnswer() throws Z3Exception + { + long ans = Native.fixedpointGetAnswer(Context().nCtx(), NativeObject()); + return (ans == 0) ? null : Expr.Create(Context(), ans); + } - Context().CheckContextMatch(rule); - Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), - rule.NativeObject(), AST.GetNativeObject(name)); - } + /** + * Retrieve explanation why fixedpoint engine returned status Unknown. + **/ + public String GetReasonUnknown() throws Z3Exception + { - /** - * Retrieve satisfying instance or instances of solver, or definitions for - * the recursive predicates that show unsatisfiability. - * - * @throws Z3Exception - **/ - public Expr GetAnswer() throws Z3Exception - { - long ans = Native.fixedpointGetAnswer(Context().nCtx(), NativeObject()); - return (ans == 0) ? null : Expr.Create(Context(), ans); - } + return Native.fixedpointGetReasonUnknown(Context().nCtx(), + NativeObject()); + } - /** - * Retrieve explanation why fixedpoint engine returned status Unknown. - **/ - public String GetReasonUnknown() - { + /** + * Retrieve the number of levels explored for a given predicate. + **/ + public int GetNumLevels(FuncDecl predicate) throws Z3Exception + { + return Native.fixedpointGetNumLevels(Context().nCtx(), NativeObject(), + predicate.NativeObject()); + } - return Native.fixedpointGetReasonUnknown(Context().nCtx(), - NativeObject()); - } + /** + * Retrieve the cover of a predicate. + * + * @throws Z3Exception + **/ + public Expr GetCoverDelta(int level, FuncDecl predicate) throws Z3Exception + { + long res = Native.fixedpointGetCoverDelta(Context().nCtx(), + NativeObject(), level, predicate.NativeObject()); + return (res == 0) ? null : Expr.Create(Context(), res); + } - /** - * Retrieve the number of levels explored for a given predicate. - **/ - public int GetNumLevels(FuncDecl predicate) - { - return Native.fixedpointGetNumLevels(Context().nCtx(), NativeObject(), - predicate.NativeObject()); - } + /** + * Add property about the predicate. The property is added + * at level. + **/ + public void AddCover(int level, FuncDecl predicate, Expr property) + throws Z3Exception + { + Native.fixedpointAddCover(Context().nCtx(), NativeObject(), level, + predicate.NativeObject(), property.NativeObject()); + } - /** - * Retrieve the cover of a predicate. - * - * @throws Z3Exception - **/ - public Expr GetCoverDelta(int level, FuncDecl predicate) throws Z3Exception - { - long res = Native.fixedpointGetCoverDelta(Context().nCtx(), - NativeObject(), level, predicate.NativeObject()); - return (res == 0) ? null : Expr.Create(Context(), res); - } + /** + * Retrieve internal string representation of fixedpoint object. + **/ + public String toString() + { + try + { + return Native.fixedpointToString(Context().nCtx(), NativeObject(), + 0, null); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - /** - * Add property about the predicate. The property is added - * at level. - **/ - public void AddCover(int level, FuncDecl predicate, Expr property) - { - Native.fixedpointAddCover(Context().nCtx(), NativeObject(), level, - predicate.NativeObject(), property.NativeObject()); - } + /** + * Instrument the Datalog engine on which table representation to use for + * recursive predicate. + **/ + public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception + { - /** - * Retrieve internal string representation of fixedpoint object. - **/ - public String toString() - { - return Native.fixedpointToString(Context().nCtx(), NativeObject(), 0, - null); - } + Native.fixedpointSetPredicateRepresentation(Context().nCtx(), + NativeObject(), f.NativeObject(), AST.ArrayLength(kinds), + Symbol.ArrayToNative(kinds)); - /** - * Instrument the Datalog engine on which table representation to use for - * recursive predicate. - **/ - public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds) - { + } - Native.fixedpointSetPredicateRepresentation(Context().nCtx(), - NativeObject(), f.NativeObject(), AST.ArrayLength(kinds), - Symbol.ArrayToNative(kinds)); + /** + * Convert benchmark given as set of axioms, rules and queries to a string. + **/ + public String toString(BoolExpr[] queries) throws Z3Exception + { - } + return Native.fixedpointToString(Context().nCtx(), NativeObject(), + AST.ArrayLength(queries), AST.ArrayToNative(queries)); + } - /** - * Convert benchmark given as set of axioms, rules and queries to a string. - **/ - public String toString(BoolExpr[] queries) - { + /** + * Retrieve set of rules added to fixedpoint context. + * + * @throws Z3Exception + **/ + public BoolExpr[] Rules() throws Z3Exception + { - return Native.fixedpointToString(Context().nCtx(), NativeObject(), - AST.ArrayLength(queries), AST.ArrayToNative(queries)); - } + ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules( + Context().nCtx(), NativeObject())); + int n = v.Size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), v.get(i).NativeObject()); + return res; + } - /** - * Retrieve set of rules added to fixedpoint context. - * - * @throws Z3Exception - **/ - public BoolExpr[] Rules() throws Z3Exception - { + /** + * Retrieve set of assertions added to fixedpoint context. + * + * @throws Z3Exception + **/ + public BoolExpr[] Assertions() throws Z3Exception + { - ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules( - Context().nCtx(), NativeObject())); - int n = v.Size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(Context(), v.get(i).NativeObject()); - return res; - } + ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions( + Context().nCtx(), NativeObject())); + int n = v.Size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), v.get(i).NativeObject()); + return res; + } - /** - * Retrieve set of assertions added to fixedpoint context. - * - * @throws Z3Exception - **/ - public BoolExpr[] Assertions() throws Z3Exception - { + Fixedpoint(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions( - Context().nCtx(), NativeObject())); - int n = v.Size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(Context(), v.get(i).NativeObject()); - return res; - } + Fixedpoint(Context ctx) throws Z3Exception + { + super(ctx, Native.mkFixedpoint(ctx.nCtx())); + } - Fixedpoint(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + void IncRef(long o) throws Z3Exception + { + Context().Fixedpoint_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - Fixedpoint(Context ctx) throws Z3Exception - { - super(ctx, Native.mkFixedpoint(ctx.nCtx())); - } - - void IncRef(long o) throws Z3Exception - { - Context().Fixedpoint_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } - - void DecRef(long o) throws Z3Exception - { - Context().Fixedpoint_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + Context().Fixedpoint_DRQ().Add(o); + super.DecRef(o); + } } diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index 3d436eafb..677691db8 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class FixedpointDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.fixedpointIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.fixedpointIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.fixedpointDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index c001dc982..a2bf28c5d 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -13,379 +13,385 @@ import com.microsoft.z3.enumerations.*; **/ public class FuncDecl extends AST { - /** - * Comparison operator. - * - * @return True if and share the - * same context and are equal, false otherwise. - **/ - /* Overloaded operators are not translated. */ + /** + * Comparison operator. + * + * @return True if and share the + * same context and are equal, false otherwise. + **/ + /* Overloaded operators are not translated. */ - /** - * Comparison operator. - * - * @return True if and do not - * share the same context or are not equal, false otherwise. - **/ - /* Overloaded operators are not translated. */ + /** + * Comparison operator. + * + * @return True if and do not + * share the same context or are not equal, false otherwise. + **/ + /* Overloaded operators are not translated. */ - /** - * Object comparison. - **/ - public boolean Equals(Object o) - { - FuncDecl casted = (FuncDecl) o; - if (casted == null) - return false; - return this == casted; - } + /** + * Object comparison. + **/ + public boolean Equals(Object o) + { + FuncDecl casted = (FuncDecl) o; + if (casted == null) + return false; + return this == casted; + } - /** - * A hash code. - **/ - public int GetHashCode() throws Z3Exception - { - return super.GetHashCode(); - } + /** + * A hash code. + **/ + public int GetHashCode() throws Z3Exception + { + return super.GetHashCode(); + } - /** - * A string representations of the function declaration. - **/ - public String toString() - { - return Native.funcDeclToString(Context().nCtx(), NativeObject()); - } + /** + * A string representations of the function declaration. + **/ + public String toString() + { + try + { + return Native.funcDeclToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - /** - * Returns a unique identifier for the function declaration. - **/ - public int Id() throws Z3Exception - { - return Native.getFuncDeclId(Context().nCtx(), NativeObject()); - } + /** + * Returns a unique identifier for the function declaration. + **/ + public int Id() throws Z3Exception + { + return Native.getFuncDeclId(Context().nCtx(), NativeObject()); + } - /** - * The arity of the function declaration - **/ - public int Arity() throws Z3Exception - { - return Native.getArity(Context().nCtx(), NativeObject()); - } + /** + * The arity of the function declaration + **/ + public int Arity() throws Z3Exception + { + return Native.getArity(Context().nCtx(), NativeObject()); + } - /** - * The size of the domain of the function declaration - **/ - public int DomainSize() - { - return Native.getDomainSize(Context().nCtx(), NativeObject()); - } + /** + * The size of the domain of the function declaration + **/ + public int DomainSize() throws Z3Exception + { + return Native.getDomainSize(Context().nCtx(), NativeObject()); + } - /** - * The domain of the function declaration - **/ - public Sort[] Domain() throws Z3Exception - { + /** + * The domain of the function declaration + **/ + public Sort[] Domain() throws Z3Exception + { - int n = DomainSize(); + int n = DomainSize(); - Sort[] res = new Sort[n]; - for (int i = 0; i < n; i++) - res[i] = Sort.Create(Context(), - Native.getDomain(Context().nCtx(), NativeObject(), i)); - return res; - } + Sort[] res = new Sort[n]; + for (int i = 0; i < n; i++) + res[i] = Sort.Create(Context(), + Native.getDomain(Context().nCtx(), NativeObject(), i)); + return res; + } - /** - * The range of the function declaration - **/ - public Sort Range() throws Z3Exception - { + /** + * The range of the function declaration + **/ + public Sort Range() throws Z3Exception + { - return Sort.Create(Context(), - Native.getRange(Context().nCtx(), NativeObject())); - } + return Sort.Create(Context(), + Native.getRange(Context().nCtx(), NativeObject())); + } - /** - * The kind of the function declaration. - **/ - public Z3_decl_kind DeclKind() throws Z3Exception - { - return Z3_decl_kind.fromInt(Native.getDeclKind(Context().nCtx(), - NativeObject())); - } + /** + * The kind of the function declaration. + **/ + public Z3_decl_kind DeclKind() throws Z3Exception + { + return Z3_decl_kind.fromInt(Native.getDeclKind(Context().nCtx(), + NativeObject())); + } - /** - * The name of the function declaration - **/ - public Symbol Name() throws Z3Exception - { + /** + * The name of the function declaration + **/ + public Symbol Name() throws Z3Exception + { - return Symbol.Create(Context(), - Native.getDeclName(Context().nCtx(), NativeObject())); - } + return Symbol.Create(Context(), + Native.getDeclName(Context().nCtx(), NativeObject())); + } - /** - * The number of parameters of the function declaration - **/ - public int NumParameters() throws Z3Exception - { - return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); - } + /** + * The number of parameters of the function declaration + **/ + public int NumParameters() throws Z3Exception + { + return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); + } - /** - * The parameters of the function declaration - **/ - public Parameter[] Parameters() throws Z3Exception - { + /** + * The parameters of the function declaration + **/ + public Parameter[] Parameters() throws Z3Exception + { - int num = NumParameters(); - Parameter[] res = new Parameter[num]; - for (int i = 0; i < num; i++) - { - Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native - .getDeclParameterKind(Context().nCtx(), NativeObject(), i)); - switch (k) - { - case Z3_PARAMETER_INT: - res[i] = new Parameter(k, Native.getDeclIntParameter(Context() - .nCtx(), NativeObject(), i)); - break; - case Z3_PARAMETER_DOUBLE: - res[i] = new Parameter(k, Native.getDeclDoubleParameter( - Context().nCtx(), NativeObject(), i)); - break; - case Z3_PARAMETER_SYMBOL: - res[i] = new Parameter(k, Symbol.Create(Context(), Native - .getDeclSymbolParameter(Context().nCtx(), - NativeObject(), i))); - break; - case Z3_PARAMETER_SORT: - res[i] = new Parameter(k, Sort.Create(Context(), Native - .getDeclSortParameter(Context().nCtx(), NativeObject(), - i))); - break; - case Z3_PARAMETER_AST: - res[i] = new Parameter(k, new AST(Context(), - Native.getDeclAstParameter(Context().nCtx(), - NativeObject(), i))); - break; - case Z3_PARAMETER_FUNC_DECL: - res[i] = new Parameter(k, new FuncDecl(Context(), - Native.getDeclFuncDeclParameter(Context().nCtx(), - NativeObject(), i))); - break; - case Z3_PARAMETER_RATIONAL: - res[i] = new Parameter(k, Native.getDeclRationalParameter( - Context().nCtx(), NativeObject(), i)); - break; - default: - throw new Z3Exception( - "Unknown function declaration parameter kind encountered"); - } - } - return res; - } + int num = NumParameters(); + Parameter[] res = new Parameter[num]; + for (int i = 0; i < num; i++) + { + Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native + .getDeclParameterKind(Context().nCtx(), NativeObject(), i)); + switch (k) + { + case Z3_PARAMETER_INT: + res[i] = new Parameter(k, Native.getDeclIntParameter(Context() + .nCtx(), NativeObject(), i)); + break; + case Z3_PARAMETER_DOUBLE: + res[i] = new Parameter(k, Native.getDeclDoubleParameter( + Context().nCtx(), NativeObject(), i)); + break; + case Z3_PARAMETER_SYMBOL: + res[i] = new Parameter(k, Symbol.Create(Context(), Native + .getDeclSymbolParameter(Context().nCtx(), + NativeObject(), i))); + break; + case Z3_PARAMETER_SORT: + res[i] = new Parameter(k, Sort.Create(Context(), Native + .getDeclSortParameter(Context().nCtx(), NativeObject(), + i))); + break; + case Z3_PARAMETER_AST: + res[i] = new Parameter(k, new AST(Context(), + Native.getDeclAstParameter(Context().nCtx(), + NativeObject(), i))); + break; + case Z3_PARAMETER_FUNC_DECL: + res[i] = new Parameter(k, new FuncDecl(Context(), + Native.getDeclFuncDeclParameter(Context().nCtx(), + NativeObject(), i))); + break; + case Z3_PARAMETER_RATIONAL: + res[i] = new Parameter(k, Native.getDeclRationalParameter( + Context().nCtx(), NativeObject(), i)); + break; + default: + throw new Z3Exception( + "Unknown function declaration parameter kind encountered"); + } + } + return res; + } - /** - * Function declarations can have Parameters associated with them. - **/ - public class Parameter - { - private Z3_parameter_kind kind; - private int i; - private double d; - private Symbol sym; - private Sort srt; - private AST ast; - private FuncDecl fd; - private String r; + /** + * Function declarations can have Parameters associated with them. + **/ + public class Parameter + { + private Z3_parameter_kind kind; + private int i; + private double d; + private Symbol sym; + private Sort srt; + private AST ast; + private FuncDecl fd; + private String r; - /** - * The int value of the parameter. - **/ - public int Int() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) - throw new Z3Exception("parameter is not an int"); - return i; - } + /** + * The int value of the parameter. + **/ + public int Int() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) + throw new Z3Exception("parameter is not an int"); + return i; + } - /** - * The double value of the parameter. - **/ - public double Double() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) - throw new Z3Exception("parameter is not a double "); - return d; - } + /** + * The double value of the parameter. + **/ + public double Double() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) + throw new Z3Exception("parameter is not a double "); + return d; + } - /** - * The Symbol value of the parameter. - **/ - public Symbol Symbol() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) - throw new Z3Exception("parameter is not a Symbol"); - return sym; - } + /** + * The Symbol value of the parameter. + **/ + public Symbol Symbol() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) + throw new Z3Exception("parameter is not a Symbol"); + return sym; + } - /** - * The Sort value of the parameter. - **/ - public Sort Sort() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) - throw new Z3Exception("parameter is not a Sort"); - return srt; - } + /** + * The Sort value of the parameter. + **/ + public Sort Sort() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) + throw new Z3Exception("parameter is not a Sort"); + return srt; + } - /** - * The AST value of the parameter. - **/ - public AST AST() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) - throw new Z3Exception("parameter is not an AST"); - return ast; - } + /** + * The AST value of the parameter. + **/ + public AST AST() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) + throw new Z3Exception("parameter is not an AST"); + return ast; + } - /** - * The FunctionDeclaration value of the parameter. - **/ - public FuncDecl FuncDecl() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) - throw new Z3Exception("parameter is not a function declaration"); - return fd; - } + /** + * The FunctionDeclaration value of the parameter. + **/ + public FuncDecl FuncDecl() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) + throw new Z3Exception("parameter is not a function declaration"); + return fd; + } - /** - * The rational string value of the parameter. - **/ - public String Rational() throws Z3Exception - { - if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) - throw new Z3Exception("parameter is not a rational String"); - return r; - } + /** + * The rational string value of the parameter. + **/ + public String Rational() throws Z3Exception + { + if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) + throw new Z3Exception("parameter is not a rational String"); + return r; + } - /** - * The kind of the parameter. - **/ - public Z3_parameter_kind ParameterKind() throws Z3Exception - { - return kind; - } + /** + * The kind of the parameter. + **/ + public Z3_parameter_kind ParameterKind() throws Z3Exception + { + return kind; + } - Parameter(Z3_parameter_kind k, int i) - { - this.kind = k; - this.i = i; - } + Parameter(Z3_parameter_kind k, int i) + { + this.kind = k; + this.i = i; + } - Parameter(Z3_parameter_kind k, double d) - { - this.kind = k; - this.d = d; - } + Parameter(Z3_parameter_kind k, double d) + { + this.kind = k; + this.d = d; + } - Parameter(Z3_parameter_kind k, Symbol s) - { - this.kind = k; - this.sym = s; - } + Parameter(Z3_parameter_kind k, Symbol s) + { + this.kind = k; + this.sym = s; + } - Parameter(Z3_parameter_kind k, Sort s) - { - this.kind = k; - this.srt = s; - } + Parameter(Z3_parameter_kind k, Sort s) + { + this.kind = k; + this.srt = s; + } - Parameter(Z3_parameter_kind k, AST a) - { - this.kind = k; - this.ast = a; - } + Parameter(Z3_parameter_kind k, AST a) + { + this.kind = k; + this.ast = a; + } - Parameter(Z3_parameter_kind k, FuncDecl fd) - { - this.kind = k; - this.fd = fd; - } + Parameter(Z3_parameter_kind k, FuncDecl fd) + { + this.kind = k; + this.fd = fd; + } - Parameter(Z3_parameter_kind k, String r) - { - this.kind = k; - this.r = r; - } - } + Parameter(Z3_parameter_kind k, String r) + { + this.kind = k; + this.r = r; + } + } - FuncDecl(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); + FuncDecl(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); - } + } - FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - throws Z3Exception - { - super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.NativeObject(), - AST.ArrayLength(domain), AST.ArrayToNative(domain), - range.NativeObject())); + FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) + throws Z3Exception + { + super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.NativeObject(), + AST.ArrayLength(domain), AST.ArrayToNative(domain), + range.NativeObject())); - } + } - FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - throws Z3Exception - { - super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, - AST.ArrayLength(domain), AST.ArrayToNative(domain), - range.NativeObject())); + FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) + throws Z3Exception + { + super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, + AST.ArrayLength(domain), AST.ArrayToNative(domain), + range.NativeObject())); - } + } - void CheckNativeObject(long obj) throws Z3Exception - { - if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST - .toInt()) - throw new Z3Exception( - "Underlying object is not a function declaration"); - super.CheckNativeObject(obj); - } + void CheckNativeObject(long obj) throws Z3Exception + { + if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST + .toInt()) + throw new Z3Exception( + "Underlying object is not a function declaration"); + super.CheckNativeObject(obj); + } - /** - * Create expression that applies function to arguments. - * - * - * @return - **/ - /* operator this[] not translated */ + /** + * Create expression that applies function to arguments. + * + * @return + **/ + /* operator this[] not translated */ - /** - * Create expression that applies function to arguments. - * - * - * @return - **/ - public Expr Apply(Expr[] args) throws Z3Exception - { - Context().CheckContextMatch(args); - return Expr.Create(Context(), this, args); - } + /** + * Create expression that applies function to arguments. + * + * @return + **/ + public Expr Apply(Expr[] args) throws Z3Exception + { + Context().CheckContextMatch(args); + return Expr.Create(Context(), this, args); + } - /** - * Create expression that applies function to one argument. - * - * - * @return - **/ - public Expr Apply(Expr arg) throws Z3Exception - { - Context().CheckContextMatch(arg); - Expr[] a = { arg }; - return Expr.Create(Context(), this, a); - } + /** + * Create expression that applies function to one argument. + * + * @return + **/ + public Expr Apply(Expr arg) throws Z3Exception + { + Context().CheckContextMatch(arg); + Expr[] a = { arg }; + return Expr.Create(Context(), this, a); + } } diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 25d3fe1c8..261f433e7 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -33,7 +33,7 @@ public class FuncInterp extends Z3Object /** * The number of arguments of the entry. **/ - public int NumArgs() + public int NumArgs() throws Z3Exception { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); } @@ -93,7 +93,7 @@ public class FuncInterp extends Z3Object /** * The number of entries in the function interpretation. **/ - public int NumEntries() + public int NumEntries() throws Z3Exception { return Native.funcInterpGetNumEntries(Context().nCtx(), NativeObject()); } @@ -127,7 +127,7 @@ public class FuncInterp extends Z3Object /** * The arity of the function interpretation **/ - public int Arity() + public int Arity() throws Z3Exception { return Native.funcInterpGetArity(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index e41551b66..d1b662cb2 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class FuncInterpDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.funcInterpIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.funcInterpIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.funcInterpDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.funcInterpDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 8d642217f..df2702020 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class FuncInterpEntryDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.funcEntryIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.funcEntryIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.funcEntryDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.funcEntryDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 0add69fd5..61ac96d30 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -14,207 +14,218 @@ import com.microsoft.z3.enumerations.*; **/ public class Goal extends Z3Object { - /** - * The precision of the goal. Goals can be transformed using over - * and under approximations. An under approximation is applied when the - * objective is to find a model for a given goal. An over approximation is - * applied when the objective is to find a proof for a given goal. - * - **/ - public Z3_goal_prec Precision() - { - return Z3_goal_prec.fromInt(Native.goalPrecision(Context().nCtx(), - NativeObject())); - } + /** + * The precision of the goal. Goals can be transformed using over + * and under approximations. An under approximation is applied when the + * objective is to find a model for a given goal. An over approximation is + * applied when the objective is to find a proof for a given goal. + * + **/ + public Z3_goal_prec Precision() throws Z3Exception + { + return Z3_goal_prec.fromInt(Native.goalPrecision(Context().nCtx(), + NativeObject())); + } - /** - * Indicates whether the goal is precise. - **/ - public boolean IsPrecise() - { - return Precision() == Z3_goal_prec.Z3_GOAL_PRECISE; - } + /** + * Indicates whether the goal is precise. + **/ + public boolean IsPrecise() throws Z3Exception + { + return Precision() == Z3_goal_prec.Z3_GOAL_PRECISE; + } - /** - * Indicates whether the goal is an under-approximation. - **/ - public boolean IsUnderApproximation() - { - return Precision() == Z3_goal_prec.Z3_GOAL_UNDER; - } + /** + * Indicates whether the goal is an under-approximation. + **/ + public boolean IsUnderApproximation() throws Z3Exception + { + return Precision() == Z3_goal_prec.Z3_GOAL_UNDER; + } - /** - * Indicates whether the goal is an over-approximation. - **/ - public boolean IsOverApproximation() - { - return Precision() == Z3_goal_prec.Z3_GOAL_OVER; - } + /** + * Indicates whether the goal is an over-approximation. + **/ + public boolean IsOverApproximation() throws Z3Exception + { + return Precision() == Z3_goal_prec.Z3_GOAL_OVER; + } - /** - * Indicates whether the goal is garbage (i.e., the product of over- and - * under-approximations). - **/ - public boolean IsGarbage() - { - return Precision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; - } + /** + * Indicates whether the goal is garbage (i.e., the product of over- and + * under-approximations). + **/ + public boolean IsGarbage() throws Z3Exception + { + return Precision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; + } - /** - * Adds the to the given goal. - * @throws Z3Exception - **/ - public void Assert(BoolExpr[] constraints) throws Z3Exception - { - Context().CheckContextMatch(constraints); - for (BoolExpr c : constraints) - { - Native.goalAssert(Context().nCtx(), NativeObject(), - c.NativeObject()); - } - } + /** + * Adds the to the given goal. + * + * @throws Z3Exception + **/ + public void Assert(BoolExpr[] constraints) throws Z3Exception + { + Context().CheckContextMatch(constraints); + for (BoolExpr c : constraints) + { + Native.goalAssert(Context().nCtx(), NativeObject(), + c.NativeObject()); + } + } - /** - * Adds a to the given goal. - * @throws Z3Exception - **/ - public void Assert(BoolExpr constraint) throws Z3Exception - { - Context().CheckContextMatch(constraint); - Native.goalAssert(Context().nCtx(), NativeObject(), - constraint.NativeObject()); - } + /** + * Adds a to the given goal. + * + * @throws Z3Exception + **/ + public void Assert(BoolExpr constraint) throws Z3Exception + { + Context().CheckContextMatch(constraint); + Native.goalAssert(Context().nCtx(), NativeObject(), + constraint.NativeObject()); + } - /** - * Indicates whether the goal contains `false'. - **/ - public boolean Inconsistent() - { - return Native.goalInconsistent(Context().nCtx(), NativeObject()); - } + /** + * Indicates whether the goal contains `false'. + **/ + public boolean Inconsistent() throws Z3Exception + { + return Native.goalInconsistent(Context().nCtx(), NativeObject()); + } - /** - * The depth of the goal. This tracks how many transformations - * were applied to it. - **/ - public int Depth() - { - return Native.goalDepth(Context().nCtx(), NativeObject()); - } + /** + * The depth of the goal. This tracks how many transformations + * were applied to it. + **/ + public int Depth() throws Z3Exception + { + return Native.goalDepth(Context().nCtx(), NativeObject()); + } - /** - * Erases all formulas from the given goal. - **/ - public void Reset() - { - Native.goalReset(Context().nCtx(), NativeObject()); - } + /** + * Erases all formulas from the given goal. + **/ + public void Reset() throws Z3Exception + { + Native.goalReset(Context().nCtx(), NativeObject()); + } - /** - * The number of formulas in the goal. - **/ - public int Size() - { - return Native.goalSize(Context().nCtx(), NativeObject()); - } + /** + * The number of formulas in the goal. + **/ + public int Size() throws Z3Exception + { + return Native.goalSize(Context().nCtx(), NativeObject()); + } - /** - * The formulas in the goal. - * @throws Z3Exception - **/ - public BoolExpr[] Formulas() throws Z3Exception - { - int n = Size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(Context(), Native.goalFormula(Context() - .nCtx(), NativeObject(), i)); - return res; - } + /** + * The formulas in the goal. + * + * @throws Z3Exception + **/ + public BoolExpr[] Formulas() throws Z3Exception + { + int n = Size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), Native.goalFormula(Context() + .nCtx(), NativeObject(), i)); + return res; + } - /** - * The number of formulas, subformulas and terms in the goal. - **/ - public int NumExprs() - { - return Native.goalNumExprs(Context().nCtx(), NativeObject()); - } + /** + * The number of formulas, subformulas and terms in the goal. + **/ + public int NumExprs() throws Z3Exception + { + return Native.goalNumExprs(Context().nCtx(), NativeObject()); + } - /** - * Indicates whether the goal is empty, and it is precise or the product of - * an under approximation. - **/ - public boolean IsDecidedSat() - { - return Native.goalIsDecidedSat(Context().nCtx(), NativeObject()); - } + /** + * Indicates whether the goal is empty, and it is precise or the product of + * an under approximation. + **/ + public boolean IsDecidedSat() throws Z3Exception + { + return Native.goalIsDecidedSat(Context().nCtx(), NativeObject()); + } - /** - * Indicates whether the goal contains `false', and it is precise or the - * product of an over approximation. - **/ - public boolean IsDecidedUnsat() - { - return Native.goalIsDecidedUnsat(Context().nCtx(), NativeObject()); - } + /** + * Indicates whether the goal contains `false', and it is precise or the + * product of an over approximation. + **/ + public boolean IsDecidedUnsat() throws Z3Exception + { + return Native.goalIsDecidedUnsat(Context().nCtx(), NativeObject()); + } - /** - * Translates (copies) the Goal to the target Context . - * @throws Z3Exception - **/ - public Goal Translate(Context ctx) throws Z3Exception - { - return new Goal(ctx, Native.goalTranslate(Context().nCtx(), - NativeObject(), ctx.nCtx())); - } + /** + * Translates (copies) the Goal to the target Context . + * + * @throws Z3Exception + **/ + public Goal Translate(Context ctx) throws Z3Exception + { + return new Goal(ctx, Native.goalTranslate(Context().nCtx(), + NativeObject(), ctx.nCtx())); + } - /** - * Simplifies the goal. Essentially invokes the `simplify' tactic - * on the goal. - **/ - public Goal Simplify(Params p) throws Z3Exception - { - Tactic t = Context().MkTactic("simplify"); - ApplyResult res = t.Apply(this, p); + /** + * Simplifies the goal. Essentially invokes the `simplify' tactic + * on the goal. + **/ + public Goal Simplify(Params p) throws Z3Exception + { + Tactic t = Context().MkTactic("simplify"); + ApplyResult res = t.Apply(this, p); - if (res.NumSubgoals() == 0) - throw new Z3Exception("No subgoals"); - else - return res.Subgoals()[0]; - } + if (res.NumSubgoals() == 0) + throw new Z3Exception("No subgoals"); + else + return res.Subgoals()[0]; + } - /** - * Goal to string conversion. - * - * @return A string representation of the Goal. - **/ - public String toString() - { - return Native.goalToString(Context().nCtx(), NativeObject()); - } + /** + * Goal to string conversion. + * + * @return A string representation of the Goal. + **/ + public String toString() + { + try + { + return Native.goalToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } - Goal(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + Goal(Context ctx, long obj) throws Z3Exception + { + 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)); - } + 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 - { - Context().Goal_DRQ().IncAndClear(Context(), o); - super.IncRef(o); - } + void IncRef(long o) throws Z3Exception + { + Context().Goal_DRQ().IncAndClear(Context(), o); + super.IncRef(o); + } - void DecRef(long o) throws Z3Exception - { - Context().Goal_DRQ().Add(o); - super.DecRef(o); - } + void DecRef(long o) throws Z3Exception + { + Context().Goal_DRQ().Add(o); + super.DecRef(o); + } } diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index 9bd2b79db..7dd52285f 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -7,13 +7,25 @@ package com.microsoft.z3; class GoalDecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, long obj) - { - Native.goalIncRef(ctx.nCtx(), obj); - } + public void IncRef(Context ctx, long obj) + { + try + { + Native.goalIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } - public void DecRef(Context ctx, long obj) - { - Native.goalDecRef(ctx.nCtx(), obj); - } + public void DecRef(Context ctx, long obj) + { + try + { + Native.goalDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } + } }; diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index aecf68ee7..1397616c6 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -14,46 +14,52 @@ import java.math.BigInteger; public class IntNum extends IntExpr { - IntNum(Context ctx, long obj) throws Z3Exception - { - super(ctx, obj); - } + IntNum(Context ctx, long obj) throws Z3Exception + { + super(ctx, obj); + } - /** - * Retrieve the int value. - **/ - public int Int() throws Z3Exception - { - Native.IntPtr res = new Native.IntPtr(); - if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int"); - return res.value; - } + /** + * Retrieve the int value. + **/ + public int Int() throws Z3Exception + { + Native.IntPtr res = new Native.IntPtr(); + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int"); + return res.value; + } - /** - * Retrieve the 64-bit int value. - **/ - public long Int64() throws Z3Exception - { - Native.LongPtr res = new Native.LongPtr(); - if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int64"); - return res.value; - } + /** + * Retrieve the 64-bit int value. + **/ + public long Int64() throws Z3Exception + { + Native.LongPtr res = new Native.LongPtr(); + if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int64"); + return res.value; + } - /** - * Retrieve the BigInteger value. - **/ - public BigInteger BigInteger() throws Z3Exception - { - return new BigInteger(this.toString()); - } + /** + * Retrieve the BigInteger value. + **/ + public BigInteger BigInteger() throws Z3Exception + { + return new BigInteger(this.toString()); + } - /** - * Returns a string representation of the numeral. - **/ - public String toString() - { - return Native.getNumeralString(Context().nCtx(), NativeObject()); - } + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + try + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 2616f26be..e38c260c4 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -19,7 +19,7 @@ public class Model extends Z3Object * * @return An expression if the constant has an interpretation in the model, * null otherwise. - * @throws Z3Exception + * @throws Z3Exception **/ public Expr ConstInterp(Expr a) throws Z3Exception { @@ -33,7 +33,7 @@ public class Model extends Z3Object * * @return An expression if the function has an interpretation in the model, * null otherwise. - * @throws Z3Exception + * @throws Z3Exception **/ public Expr ConstInterp(FuncDecl f) throws Z3Exception { @@ -60,7 +60,7 @@ public class Model extends Z3Object * * @return A FunctionInterpretation if the function has an interpretation in * the model, null otherwise. - * @throws Z3Exception + * @throws Z3Exception **/ public FuncInterp FuncInterp(FuncDecl f) throws Z3Exception { @@ -105,14 +105,15 @@ public class Model extends Z3Object /** * The number of constants that have an interpretation in the model. **/ - public int NumConsts() + public int NumConsts() throws Z3Exception { return Native.modelGetNumConsts(Context().nCtx(), NativeObject()); } /** * The function declarations of the constants in the model. - * @throws Z3Exception + * + * @throws Z3Exception **/ public FuncDecl[] ConstDecls() throws Z3Exception { @@ -127,14 +128,15 @@ public class Model extends Z3Object /** * The number of function interpretations in the model. **/ - public int NumFuncs() + public int NumFuncs() throws Z3Exception { return Native.modelGetNumFuncs(Context().nCtx(), NativeObject()); } /** * The function declarations of the function interpretations in the model. - * @throws Z3Exception + * + * @throws Z3Exception **/ public FuncDecl[] FuncDecls() throws Z3Exception { @@ -148,7 +150,8 @@ public class Model extends Z3Object /** * All symbols that have an interpretation in the model. - * @throws Z3Exception + * + * @throws Z3Exception **/ public FuncDecl[] Decls() throws Z3Exception { @@ -192,7 +195,7 @@ public class Model extends Z3Object * that does not have an interpretation in the model. * * @return The evaluation of in the model. - * @throws Z3Exception + * @throws Z3Exception **/ public Expr Eval(Expr t, boolean completion) throws Z3Exception { @@ -206,7 +209,8 @@ public class Model extends Z3Object /** * Alias for Eval. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Expr Evaluate(Expr t, boolean completion) throws Z3Exception { @@ -217,7 +221,7 @@ public class Model extends Z3Object * The number of uninterpreted sorts that the model has an interpretation * for. **/ - public int NumSorts() + public int NumSorts() throws Z3Exception { return Native.modelGetNumSorts(Context().nCtx(), NativeObject()); } @@ -228,7 +232,8 @@ public class Model extends Z3Object * in a formula. The interpretation for a sort is a finite set of distinct * values. We say this finite set is the "universe" of the sort. * - * @throws Z3Exception + * + * @throws Z3Exception **/ public Sort[] Sorts() throws Z3Exception { @@ -248,7 +253,7 @@ public class Model extends Z3Object * * @return An array of expressions, where each is an element of the universe * of - * @throws Z3Exception + * @throws Z3Exception **/ public Expr[] SortUniverse(Sort s) throws Z3Exception { @@ -269,7 +274,13 @@ public class Model extends Z3Object **/ public String toString() { - return Native.modelToString(Context().nCtx(), NativeObject()); + try + { + return Native.modelToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } Model(Context ctx, long obj) throws Z3Exception diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index 89a0bbd78..71fb939cf 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -9,11 +9,23 @@ class ModelDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.modelIncRef(ctx.nCtx(), obj); + try + { + Native.modelIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.modelDecRef(ctx.nCtx(), obj); + try + { + Native.modelDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 11a8ee8b2..09b70f5c7 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -16,7 +16,7 @@ public class ParamDescrs extends Z3Object /** * validate a set of parameters. **/ - public void Validate(Params p) + public void Validate(Params p) throws Z3Exception { Native.paramsValidate(Context().nCtx(), p.NativeObject(), @@ -26,7 +26,7 @@ public class ParamDescrs extends Z3Object /** * Retrieve kind of parameter. **/ - public Z3_param_kind GetKind(Symbol name) + public Z3_param_kind GetKind(Symbol name) throws Z3Exception { return Z3_param_kind.fromInt(Native.paramDescrsGetKind( @@ -53,7 +53,7 @@ public class ParamDescrs extends Z3Object /** * The size of the ParamDescrs. **/ - public int Size() + public int Size() throws Z3Exception { return Native.paramDescrsSize(Context().nCtx(), NativeObject()); } @@ -63,7 +63,13 @@ public class ParamDescrs extends Z3Object **/ public String toString() { - return Native.paramDescrsToString(Context().nCtx(), NativeObject()); + try + { + return Native.paramDescrsToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } ParamDescrs(Context ctx, long obj) throws Z3Exception diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index f36d302ba..75e2a2c7e 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -9,11 +9,23 @@ class ParamDescrsDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.paramDescrsIncRef(ctx.nCtx(), obj); + try + { + Native.paramDescrsIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.paramDescrsDecRef(ctx.nCtx(), obj); + try + { + Native.paramDescrsDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 33ca34a23..3bc8b4574 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -80,7 +80,13 @@ public class Params extends Z3Object **/ public String toString() { - return Native.paramsToString(Context().nCtx(), NativeObject()); + try + { + return Native.paramsToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } Params(Context ctx) throws Z3Exception diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index 27fa3cadd..7c3ccbee8 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -9,11 +9,23 @@ class ParamsDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.paramsIncRef(ctx.nCtx(), obj); + try + { + Native.paramsIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.paramsDecRef(ctx.nCtx(), obj); + try + { + Native.paramsDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index 47f4a7c6a..ed36ad0e7 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -15,7 +15,7 @@ public class Pattern extends AST /** * The number of terms in the pattern. **/ - public int NumTerms() + public int NumTerms() throws Z3Exception { return Native.getPatternNumTerms(Context().nCtx(), NativeObject()); } @@ -41,7 +41,13 @@ public class Pattern extends AST **/ public String toString() { - return Native.patternToString(Context().nCtx(), NativeObject()); + try + { + return Native.patternToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } Pattern(Context ctx, long obj) throws Z3Exception diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 01d2e3852..b368702df 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -9,11 +9,23 @@ class ProbeDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.probeIncRef(ctx.nCtx(), obj); + try + { + Native.probeIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.probeDecRef(ctx.nCtx(), obj); + try + { + Native.probeDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index a0b5c9e6a..82e5a958b 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -16,7 +16,7 @@ public class Quantifier extends BoolExpr /** * Indicates whether the quantifier is universal. **/ - public boolean IsUniversal() + public boolean IsUniversal() throws Z3Exception { return Native.isQuantifierForall(Context().nCtx(), NativeObject()); } @@ -24,7 +24,7 @@ public class Quantifier extends BoolExpr /** * Indicates whether the quantifier is existential. **/ - public boolean IsExistential() + public boolean IsExistential() throws Z3Exception { return !IsUniversal(); } @@ -32,7 +32,7 @@ public class Quantifier extends BoolExpr /** * The weight of the quantifier. **/ - public int Weight() + public int Weight() throws Z3Exception { return Native.getQuantifierWeight(Context().nCtx(), NativeObject()); } @@ -40,7 +40,7 @@ public class Quantifier extends BoolExpr /** * The number of patterns. **/ - public int NumPatterns() + public int NumPatterns() throws Z3Exception { return Native .getQuantifierNumPatterns(Context().nCtx(), NativeObject()); @@ -64,7 +64,7 @@ public class Quantifier extends BoolExpr /** * The number of no-patterns. **/ - public int NumNoPatterns() + public int NumNoPatterns() throws Z3Exception { return Native.getQuantifierNumNoPatterns(Context().nCtx(), NativeObject()); @@ -88,7 +88,7 @@ public class Quantifier extends BoolExpr /** * The number of bound variables. **/ - public int NumBound() + public int NumBound() throws Z3Exception { return Native.getQuantifierNumBound(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index 045416973..bdc57fbdb 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -7,6 +7,7 @@ package com.microsoft.z3; import java.math.BigInteger; + /** * Rational Numerals **/ @@ -63,7 +64,13 @@ public class RatNum extends RealExpr **/ public String toString() { - return Native.getNumeralString(Context().nCtx(), NativeObject()); + try + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } RatNum(Context ctx, long obj) throws Z3Exception diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java index 2880eadc9..820228e82 100644 --- a/src/api/java/RelationSort.java +++ b/src/api/java/RelationSort.java @@ -14,7 +14,7 @@ public class RelationSort extends Sort /** * The arity of the relation sort. **/ - public int Arity() + public int Arity() throws Z3Exception { return Native.getRelationArity(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index f3ec9c916..278427d49 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -16,14 +16,15 @@ public class Solver extends Z3Object /** * A string that describes all available solver parameters. **/ - public String Help() + public String Help() throws Z3Exception { return Native.solverGetHelp(Context().nCtx(), NativeObject()); } /** * Sets the solver parameters. - * @throws Z3Exception + * + * @throws Z3Exception **/ public void setParameters(Params value) throws Z3Exception { @@ -34,7 +35,8 @@ public class Solver extends Z3Object /** * Retrieves parameter descriptions for solver. - * @throws Z3Exception + * + * @throws Z3Exception **/ public ParamDescrs ParameterDescriptions() throws Z3Exception { @@ -46,7 +48,7 @@ public class Solver extends Z3Object * The current number of backtracking points (scopes). * **/ - public int NumScopes() + public int NumScopes() throws Z3Exception { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); } @@ -54,7 +56,7 @@ public class Solver extends Z3Object /** * Creates a backtracking point. **/ - public void Push() + public void Push() throws Z3Exception { Native.solverPush(Context().nCtx(), NativeObject()); } @@ -62,9 +64,9 @@ public class Solver extends Z3Object /** * Backtracks one backtracking point. . **/ - public void Pop() + public void Pop() throws Z3Exception { - Pop(1); + Pop(1); } /** @@ -72,7 +74,7 @@ public class Solver extends Z3Object * an exception is thrown if is not smaller than * NumScopes **/ - public void Pop(int n) + public void Pop(int n) throws Z3Exception { Native.solverPop(Context().nCtx(), NativeObject(), n); } @@ -81,14 +83,15 @@ public class Solver extends Z3Object * Resets the Solver. This removes all assertions from the * solver. **/ - public void Reset() + public void Reset() throws Z3Exception { Native.solverReset(Context().nCtx(), NativeObject()); } /** * Assert a multiple constraints into the solver. - * @throws Z3Exception + * + * @throws Z3Exception **/ public void Assert(BoolExpr[] constraints) throws Z3Exception { @@ -102,17 +105,20 @@ public class Solver extends Z3Object /** * Assert one constraint into the solver. - * @throws Z3Exception + * + * @throws Z3Exception **/ public void Assert(BoolExpr constraint) throws Z3Exception { Context().CheckContextMatch(constraint); - Native.solverAssert(Context().nCtx(), NativeObject(), constraint.NativeObject()); + Native.solverAssert(Context().nCtx(), NativeObject(), + constraint.NativeObject()); } /** * The number of assertions in the solver. - * @throws Z3Exception + * + * @throws Z3Exception **/ public int NumAssertions() throws Z3Exception { @@ -123,7 +129,8 @@ public class Solver extends Z3Object /** * The set of asserted formulas. - * @throws Z3Exception + * + * @throws Z3Exception **/ public BoolExpr[] Assertions() throws Z3Exception { @@ -141,7 +148,7 @@ public class Solver extends Z3Object * **/ - public Status Check(Expr[] assumptions) + public Status Check(Expr[] assumptions) throws Z3Exception { Z3_lbool r; if (assumptions == null) @@ -167,9 +174,9 @@ public class Solver extends Z3Object * **/ - public Status Check() + public Status Check() throws Z3Exception { - return Check(null); + return Check(null); } /** @@ -177,7 +184,8 @@ public class Solver extends Z3Object * null if Check was not invoked before, if its * results was not SATISFIABLE, or if model production is not * enabled. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Model Model() throws Z3Exception { @@ -193,7 +201,8 @@ public class Solver extends Z3Object * null if Check was not invoked before, if its * results was not UNSATISFIABLE, or if proof production is * disabled. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Expr Proof() throws Z3Exception { @@ -209,7 +218,8 @@ public class Solver extends Z3Object * is a subset of Assertions The result is empty if * Check was not invoked before, if its results was not * UNSATISFIABLE, or if core production is disabled. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Expr[] UnsatCore() throws Z3Exception { @@ -227,15 +237,15 @@ public class Solver extends Z3Object * A brief justification of why the last call to Check returned * UNKNOWN. **/ - public String ReasonUnknown() + public String ReasonUnknown() throws Z3Exception { - return Native.solverGetReasonUnknown(Context().nCtx(), NativeObject()); } /** * Solver statistics. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Statistics Statistics() throws Z3Exception { @@ -248,7 +258,13 @@ public class Solver extends Z3Object **/ public String toString() { - return Native.solverToString(Context().nCtx(), NativeObject()); + try + { + return Native.solverToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } Solver(Context ctx, long obj) throws Z3Exception diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index 11a670732..2696f6ecc 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -9,11 +9,23 @@ class SolverDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.solverIncRef(ctx.nCtx(), obj); + try + { + Native.solverIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.solverDecRef(ctx.nCtx(), obj); + try + { + Native.solverDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 9a6f8aa9a..526329146 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -37,7 +37,7 @@ public class Sort extends AST * * @return **/ - public boolean Equals(Object o) + public boolean equals(Object o) { Sort casted = (Sort) o; if (casted == null) @@ -86,7 +86,13 @@ public class Sort extends AST **/ public String toString() { - return Native.sortToString(Context().nCtx(), NativeObject()); + try + { + return Native.sortToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } /** diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 07a573940..3f6e31f96 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -56,7 +56,8 @@ public class Statistics extends Z3Object /** * The string representation of the the entry's value. - * @throws Z3Exception + * + * @throws Z3Exception **/ public String Value() throws Z3Exception { @@ -107,20 +108,27 @@ public class Statistics extends Z3Object **/ public String toString() { - return Native.statsToString(Context().nCtx(), NativeObject()); + try + { + return Native.statsToString(Context().nCtx(), NativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } } /** * The number of statistical data. **/ - public int Size() + public int Size() throws Z3Exception { return Native.statsSize(Context().nCtx(), NativeObject()); } /** * The data entries. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Entry[] Entries() throws Z3Exception { @@ -147,7 +155,7 @@ public class Statistics extends Z3Object /** * The statistical counters. **/ - public String[] Keys() + public String[] Keys() throws Z3Exception { int n = Size(); String[] res = new String[n]; @@ -159,7 +167,8 @@ public class Statistics extends Z3Object /** * The value of a particular statistical counter. Returns null if * the key is unknown. - * @throws Z3Exception + * + * @throws Z3Exception **/ public Entry get(String key) throws Z3Exception { diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index 0bbd7914a..907cf8760 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -9,11 +9,23 @@ class StatisticsDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.statsIncRef(ctx.nCtx(), obj); + try + { + Native.statsIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } - + public void DecRef(Context ctx, long obj) { - Native.statsDecRef(ctx.nCtx(), obj); + try + { + Native.statsDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 526960e88..cd987adf2 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -16,7 +16,7 @@ public class Symbol extends Z3Object /** * The kind of the symbol (int or string) **/ - protected Z3_symbol_kind Kind() + protected Z3_symbol_kind Kind() throws Z3Exception { return Z3_symbol_kind.fromInt(Native.getSymbolKind(Context().nCtx(), NativeObject())); @@ -25,7 +25,7 @@ public class Symbol extends Z3Object /** * Indicates whether the symbol is of Int kind **/ - public boolean IsIntSymbol() + public boolean IsIntSymbol() throws Z3Exception { return Kind() == Z3_symbol_kind.Z3_INT_SYMBOL; } @@ -33,7 +33,7 @@ public class Symbol extends Z3Object /** * Indicates whether the symbol is of string kind. **/ - public boolean IsStringSymbol() + public boolean IsStringSymbol() throws Z3Exception { return Kind() == Z3_symbol_kind.Z3_STRING_SYMBOL; } diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index b9a0ba0c7..124db0ef2 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -18,7 +18,7 @@ public class Tactic extends Z3Object /** * A string containing a description of parameters accepted by the tactic. **/ - public String Help() + public String Help() throws Z3Exception { return Native.tacticGetHelp(Context().nCtx(), NativeObject()); } diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index ff0e27b5c..c2ea2c079 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -9,11 +9,23 @@ class TacticDecRefQueue extends IDecRefQueue { public void IncRef(Context ctx, long obj) { - Native.tacticIncRef(ctx.nCtx(), obj); + try + { + Native.tacticIncRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } public void DecRef(Context ctx, long obj) { - Native.tacticDecRef(ctx.nCtx(), obj); + try + { + Native.tacticDecRef(ctx.nCtx(), obj); + } catch (Z3Exception e) + { + // OK. + } } }; diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index f05885f35..3eb28b88e 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -25,7 +25,7 @@ public class TupleSort extends Sort /** * The number of fields in the tuple. **/ - public int NumFields() + public int NumFields() throws Z3Exception { return Native.getTupleSortNumFields(Context().nCtx(), NativeObject()); }