From 520bcaf720589d27f41233315f7066ddc1d95c23 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 23 Nov 2012 00:46:44 +0000 Subject: [PATCH] More Java API. This is still under heavy construction and cannot be used. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_project.py | 2 +- scripts/mk_util.py | 106 +- scripts/update_api.py | 7 +- src/api/java/com/Microsoft/Z3/AST.java | 40 +- src/api/java/com/Microsoft/Z3/ASTMap.java | 8 +- src/api/java/com/Microsoft/Z3/ASTVector.java | 14 +- .../java/com/Microsoft/Z3/ApplyResult.java | 14 +- .../java/com/Microsoft/Z3/Constructor.java | 63 +- src/api/java/com/Microsoft/Z3/Context.java | 329 ++--- .../java/com/Microsoft/Z3/DecRefQUeue.java | 40 +- .../Z3/Enumerations/Z3_ast_kind.java | 19 + .../Z3/Enumerations/Z3_ast_print_mode.java | 16 + .../Z3/Enumerations/Z3_decl_kind.java | 164 +++ .../Z3/Enumerations/Z3_error_code.java | 25 + .../Z3/Enumerations/Z3_goal_prec.java | 16 + .../Microsoft/Z3/Enumerations/Z3_lbool.java | 15 + .../Z3/Enumerations/Z3_param_kind.java | 19 + .../Z3/Enumerations/Z3_parameter_kind.java | 19 + .../Z3/Enumerations/Z3_sort_kind.java | 22 + .../Z3/Enumerations/Z3_symbol_kind.java | 14 + src/api/java/com/Microsoft/Z3/Expr.java | 1222 ++++++++++++++++- src/api/java/com/Microsoft/Z3/Fixedpoint.java | 44 +- src/api/java/com/Microsoft/Z3/FuncDecl.java | 113 +- src/api/java/com/Microsoft/Z3/FuncInterp.java | 36 +- src/api/java/com/Microsoft/Z3/Goal.java | 26 +- src/api/java/com/Microsoft/Z3/Log.java | 10 +- src/api/java/com/Microsoft/Z3/Model.java | 46 +- src/api/java/com/Microsoft/Z3/Native.java | 9 +- src/api/java/com/Microsoft/Z3/Numeral.java | 54 +- .../java/com/Microsoft/Z3/ParamDescrs.java | 16 +- src/api/java/com/Microsoft/Z3/Params.java | 12 +- src/api/java/com/Microsoft/Z3/Pattern.java | 8 +- src/api/java/com/Microsoft/Z3/Probe.java | 4 +- src/api/java/com/Microsoft/Z3/Quantifier.java | 42 +- src/api/java/com/Microsoft/Z3/Solver.java | 46 +- src/api/java/com/Microsoft/Z3/Sort.java | 140 +- src/api/java/com/Microsoft/Z3/Statistics.java | 56 +- src/api/java/com/Microsoft/Z3/Symbol.java | 22 +- src/api/java/com/Microsoft/Z3/Tactic.java | 12 +- src/api/java/com/Microsoft/Z3/Version.java | 26 +- src/api/java/com/Microsoft/Z3/Z3Object.java | 40 +- src/api/java/mk_java.py | 84 +- 42 files changed, 2353 insertions(+), 667 deletions(-) create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java create mode 100644 src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6d2b7c70e..862a0915b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -71,7 +71,7 @@ def init_project_def(): static=build_static_lib(), export_files=API_files) add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties') - add_java_dll('java', 'api/java', dll_name='libz3java') + add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.Microsoft.Z3") add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') # Examples diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 35ef7166d..b69171a24 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -52,6 +52,7 @@ PATTERN_COMPONENT='pattern' UTIL_COMPONENT='util' API_COMPONENT='api' DOTNET_COMPONENT='dotnet' +JAVA_COMPONENT='java' CPP_COMPONENT='cpp' ##################### IS_WINDOWS=False @@ -921,11 +922,12 @@ class DotNetDLLComponent(Component): class JavaDLLComponent(Component): - def __init__(self, name, dll_name, path): - Component.__init__(self, name, path, []) + def __init__(self, name, dll_name, package_name, path, deps): + Component.__init__(self, name, path, deps) if dll_name == None: dll_name = name - self.dll_name = dll_name + self.dll_name = dll_name + self.package_name = package_name def mk_makefile(self, out): if is_java_enabled(): @@ -942,6 +944,7 @@ class JavaDLLComponent(Component): out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir)) out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile) out.write('%s: %s\n\n' % (self.name, dllfile)) + # TODO: Compile and package all the .class files. def main_component(self): return is_java_enabled() @@ -1080,8 +1083,8 @@ def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=N c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir) reg_component(name, c) -def add_java_dll(name, path=None, dll_name=None): - c = JavaDLLComponent(name, dll_name, path) +def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None): + c = JavaDLLComponent(name, dll_name, package_name, path, deps) reg_component(name, c) def add_cpp_example(name, path=None): @@ -1604,7 +1607,7 @@ def cp_z3pyc_to_build(): def mk_bindings(api_files): if not ONLY_MAKEFILES: mk_z3consts_py(api_files) - mk_z3consts_donet(api_files) + mk_z3consts_dotnet(api_files) new_api_files = [] api = get_component(API_COMPONENT) for api_file in api_files: @@ -1614,6 +1617,7 @@ def mk_bindings(api_files): g["API_FILES"] = new_api_files if is_java_enabled(): check_java() + mk_z3consts_java(api_files) execfile('scripts/update_api.py', g) # HACK cp_z3pyc_to_build() @@ -1696,7 +1700,7 @@ def mk_z3consts_py(api_files): # Extract enumeration types from z3_api.h, and add .Net definitions -def mk_z3consts_donet(api_files): +def mk_z3consts_dotnet(api_files): blank_pat = re.compile("^ *$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") @@ -1779,6 +1783,94 @@ def mk_z3consts_donet(api_files): if VERBOSE: print "Generated '%s'" % ('%s/Enumerations.cs' % dotnet.src_dir) + +# Extract enumeration types from z3_api.h, and add Java definitions +def mk_z3consts_java(api_files): + blank_pat = re.compile("^ *$") + comment_pat = re.compile("^ *//.*$") + typedef_pat = re.compile("typedef enum *") + typedef2_pat = re.compile("typedef enum { *") + openbrace_pat = re.compile("{ *") + closebrace_pat = re.compile("}.*;") + + java = get_component(JAVA_COMPONENT) + + DeprecatedEnums = [ 'Z3_search_failure' ] + gendir = java.src_dir + "/" + java.package_name.replace(".", "/") + "/Enumerations" + if not os.path.exists(gendir): + os.mkdir(gendir) + + for api_file in api_files: + api_file_c = java.find_file(api_file, java.name) + api_file = '%s/%s' % (api_file_c.src_dir, api_file) + + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + if name not in DeprecatedEnums: + efile = open('%s/%s.java' % (gendir, name), 'w') + efile.write('/**\n * Automatically generated file\n **/\n\n') + efile.write('package %s;\n\n' % java.package_name); + + efile.write('/**\n') + efile.write(' * %s\n' % name) + efile.write(' **/\n') + efile.write('public enum %s {\n' % name) + efile.write + for k, i in decls.iteritems(): + efile.write('%s (%s),\n' % (k, i)) + efile.write('}\n\n') + efile.close() + mode = SEARCHING + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + if VERBOSE: + print "Generated '%s'" % ('%s' % gendir) + def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index 3caca21ab..7e1439375 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -506,6 +506,9 @@ def mk_java(): java_native.write('// Automatically generated file\n') java_native.write('package com.Microsoft.Z3;\n') 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') if is_windows(): java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java')) @@ -524,9 +527,9 @@ def mk_java(): i = i + 1 java_native.write(');\n') java_native.write(' public static void main(String[] args) {\n') - java_native.write(' Integer major = 0, minor = 0, build = 0, revision = 0;\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, minor, build);\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_wrapper = open(java_wrapperf, 'w') diff --git a/src/api/java/com/Microsoft/Z3/AST.java b/src/api/java/com/Microsoft/Z3/AST.java index 9cd3286a2..ad4c9d94a 100644 --- a/src/api/java/com/Microsoft/Z3/AST.java +++ b/src/api/java/com/Microsoft/Z3/AST.java @@ -75,7 +75,7 @@ package com.Microsoft.Z3; /** * A unique identifier for the AST (unique among all ASTs). **/ - public Integer Id() { return Native.getAstId(Context.nCtx, NativeObject); } + public long Id() { return Native.getAstId(Context.nCtx, NativeObject); } /** * Translates (copies) the AST to the Context . @@ -96,7 +96,7 @@ package com.Microsoft.Z3; /** * The kind of the AST. **/ - public Z3_ast_kind ASTKind() { return (Z3AstKind)Native.getAstKind(Context.nCtx, NativeObject); } + public Z3_ast_kind ASTKind() { return (Z3_ast_kind)Native.getAstKind(Context.nCtx, NativeObject); } /** * Indicates whether the AST is an Expr @@ -105,33 +105,33 @@ package com.Microsoft.Z3; { switch (ASTKind) { - case Z3AstKind.Z3APPAST: - case Z3AstKind.Z3NUMERALAST: - case Z3AstKind.Z3QUANTIFIERAST: - case Z3AstKind.Z3VARAST: return true; + case Z3_ast_kind.Z3_APP_AST: + case Z3_ast_kind.Z3_NUMERAL_AST: + case Z3_ast_kind.Z3_QUANTIFIER_AST: + case Z3_ast_kind.Z3_VAR_AST: return true; default: return false; - } + } } /** * Indicates whether the AST is a BoundVariable **/ - public boolean IsVar() { return this.ASTKind == Z3AstKind.Z3VARAST; } + public boolean IsVar() { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; } /** * Indicates whether the AST is a Quantifier **/ - public boolean IsQuantifier() { return this.ASTKind == Z3AstKind.Z3QUANTIFIERAST; } + public boolean IsQuantifier() { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; } /** * Indicates whether the AST is a Sort **/ - public boolean IsSort() { return this.ASTKind == Z3AstKind.Z3SORTAST; } + public boolean IsSort() { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; } /** * Indicates whether the AST is a FunctionDeclaration **/ - public boolean IsFuncDecl() { return this.ASTKind == Z3AstKind.Z3FUNCDECLAST; } + public boolean IsFuncDecl() { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; } /** * A string representation of the AST. @@ -174,7 +174,7 @@ package com.Microsoft.Z3; throw new Z3Exception("inc() called on null context"); if (o == IntPtr.Zero) throw new Z3Exception("inc() called on null AST"); - Context.ASTDRQ.IncAndClear(Context, o); + Context.AST_DRQ.IncAndClear(Context, o); super.IncRef(o); } @@ -185,7 +185,7 @@ package com.Microsoft.Z3; throw new Z3Exception("dec() called on null context"); if (o == IntPtr.Zero) throw new Z3Exception("dec() called on null AST"); - Context.ASTDRQ.Add(o); + Context.AST_DRQ.Add(o); super.DecRef(o); } @@ -194,14 +194,14 @@ package com.Microsoft.Z3; - switch ((Z3AstKind)Native.getAstKind(ctx.nCtx, obj)) + switch ((Z3_ast_kind)Native.getAstKind(ctx.nCtx, obj)) { - case Z3AstKind.Z3FUNCDECLAST: return new FuncDecl(ctx, obj); - case Z3AstKind.Z3QUANTIFIERAST: return new Quantifier(ctx, obj); - case Z3AstKind.Z3SORTAST: return Sort.Create(ctx, obj); - case Z3AstKind.Z3APPAST: - case Z3AstKind.Z3NUMERALAST: - case Z3AstKind.Z3VARAST: return Expr.Create(ctx, obj); + case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj); + case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); + case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj); + case Z3_ast_kind.Z3_APP_AST: + case Z3_ast_kind.Z3_NUMERAL_AST: + case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj); default: throw new Z3Exception("Unknown AST kind"); } diff --git a/src/api/java/com/Microsoft/Z3/ASTMap.java b/src/api/java/com/Microsoft/Z3/ASTMap.java index 55a100a7b..7b95861b4 100644 --- a/src/api/java/com/Microsoft/Z3/ASTMap.java +++ b/src/api/java/com/Microsoft/Z3/ASTMap.java @@ -73,7 +73,7 @@ package com.Microsoft.Z3; /** * The size of the map **/ - public Integer Size() { return Native.astMapSize(Context.nCtx, NativeObject); } + public long Size() { return Native.astMapSize(Context.nCtx, NativeObject); } /** * The keys stored in the map. @@ -81,7 +81,7 @@ package com.Microsoft.Z3; public ASTVector Keys() { return new ASTVector(Context, Native.astMapKeys(Context.nCtx, NativeObject)); - } + } /** * Retrieves a string representation of the map. @@ -115,13 +115,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ASTMapDRQ.IncAndClear(Context, o); + Context.ASTMap_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ASTMapDRQ.Add(o); + Context.ASTMap_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/ASTVector.java b/src/api/java/com/Microsoft/Z3/ASTVector.java index c57635289..0ae2ff20a 100644 --- a/src/api/java/com/Microsoft/Z3/ASTVector.java +++ b/src/api/java/com/Microsoft/Z3/ASTVector.java @@ -14,7 +14,7 @@ package com.Microsoft.Z3; /** * The size of the vector **/ - public Integer Size() { return Native.astVectorSize(Context.nCtx, NativeObject); } + public long Size() { return Native.astVectorSize(Context.nCtx, NativeObject); } /** * Retrieves the i-th object in the vector. @@ -22,24 +22,24 @@ package com.Microsoft.Z3; * Index * @return An AST **/ - public AST this[Integer i]() + public AST get(long i) { return new AST(Context, Native.astVectorGet(Context.nCtx, NativeObject, i)); - set + } + public void set(long i, AST value) { Native.astVectorSet(Context.nCtx, NativeObject, i, value.NativeObject); } - } /** * Resize the vector to . * The new size of the vector. **/ - public void Resize(Integer newSize) + public void Resize(long newSize) { Native.astVectorResize(Context.nCtx, NativeObject, newSize); } @@ -95,13 +95,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ASTVectorDRQ.IncAndClear(Context, o); + Context.ASTVector_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ASTVectorDRQ.Add(o); + Context.ASTVector_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/ApplyResult.java b/src/api/java/com/Microsoft/Z3/ApplyResult.java index 7e5390237..9bd613930 100644 --- a/src/api/java/com/Microsoft/Z3/ApplyResult.java +++ b/src/api/java/com/Microsoft/Z3/ApplyResult.java @@ -15,7 +15,7 @@ package com.Microsoft.Z3; /** * The number of Subgoals. **/ - public Integer NumSubgoals() { return Native.applyResultGetNumSubgoals(Context.nCtx, NativeObject); } + public long NumSubgoals() { return Native.applyResultGetNumSubgoals(Context.nCtx, NativeObject); } /** * Retrieves the subgoals from the ApplyResult. @@ -25,19 +25,19 @@ package com.Microsoft.Z3; - Integer n = NumSubgoals; + long n = NumSubgoals; Goal[] res = new Goal[n]; - for (Integer i = 0; i < n; i++) + for (long 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 **/ - public Model ConvertModel(Integer i, Model m) + public Model ConvertModel(long i, Model m) { @@ -72,13 +72,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ApplyResultDRQ.IncAndClear(Context, o); + Context.ApplyResult_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ApplyResultDRQ.Add(o); + Context.ApplyResult_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java index 2f9a2009e..7c9b2a85c 100644 --- a/src/api/java/com/Microsoft/Z3/Constructor.java +++ b/src/api/java/com/Microsoft/Z3/Constructor.java @@ -14,28 +14,41 @@ package com.Microsoft.Z3; /** * The number of fields of the constructor. **/ - public Integer NumFields() { init(); return n; } + public long NumFields() + { + init(); + return n; + } /** * The function declaration of the constructor. **/ - public FuncDecl ConstructorDecl() { + public FuncDecl ConstructorDecl() + { - init(); return mConstructorDecl; } + init(); + return m_constructorDecl; + } /** * The function declaration of the tester. **/ - public FuncDecl TesterDecl() { + public FuncDecl TesterDecl() + { - init(); return mTesterDecl; } + init(); + return m_testerDecl; + } /** * The function declarations of the accessors **/ - public FuncDecl[] AccessorDecls() { + public FuncDecl[] AccessorDecls() + { - init(); return mAccessorDecls; } + init(); + return m_accessorDecls; + } /** * Destructor. @@ -51,15 +64,15 @@ package com.Microsoft.Z3; } - - private Integer n = 0; - private FuncDecl mTesterDecl = null; - private FuncDecl mConstructorDecl = null; - private FuncDecl[] mAccessorDecls = null; + + private long n = 0; + private FuncDecl m_testerDecl = null; + private FuncDecl m_constructorDecl = null; + private FuncDecl[] m_accessorDecls = null; Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, - Sort[] sorts, Integer[] sortRefs) + Sort[] sorts, long[] sortRefs) { super(ctx); @@ -71,8 +84,8 @@ package com.Microsoft.Z3; throw new Z3Exception("Number of field names does not match number of sorts"); if (sortRefs != null && sortRefs.Length != n) throw new Z3Exception("Number of field names does not match number of sort refs"); - - if (sortRefs == null) sortRefs = new Integer[n]; + + if (sortRefs == null) sortRefs = new long[n]; NativeObject = Native.mkConstructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject, n, @@ -82,22 +95,22 @@ package com.Microsoft.Z3; } - private void init() + private void init() { - if (mTesterDecl != null) return; + if (m_testerDecl != null) return; IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; Native.queryConstructor(Context.nCtx, NativeObject, n, constructor, tester, accessors); - mConstructorDecl = new FuncDecl(Context, constructor); - mTesterDecl = new FuncDecl(Context, tester); - mAccessorDecls = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) - mAccessorDecls[i] = new FuncDecl(Context, accessors[i]); + m_constructorDecl = new FuncDecl(Context, constructor); + m_testerDecl = new FuncDecl(Context, tester); + m_accessorDecls = new FuncDecl[n]; + for (long i = 0; i < n; i++) + m_accessorDecls[i] = new FuncDecl(Context, accessors[i]); } } @@ -111,7 +124,7 @@ package com.Microsoft.Z3; * Destructor. **/ protected void finalize() - { + { Native.delConstructorList(Context.nCtx, NativeObject); } @@ -125,6 +138,6 @@ package com.Microsoft.Z3; - NativeObject = Native.mkConstructorList(Context.nCtx, (Integer)constructors.Length, Constructor.ArrayToNative(constructors)); - } + NativeObject = Native.mkConstructorList(Context.nCtx, (long)constructors.Length, Constructor.ArrayToNative(constructors)); + } } diff --git a/src/api/java/com/Microsoft/Z3/Context.java b/src/api/java/com/Microsoft/Z3/Context.java index 471c82120..c18fb7414 100644 --- a/src/api/java/com/Microsoft/Z3/Context.java +++ b/src/api/java/com/Microsoft/Z3/Context.java @@ -18,7 +18,7 @@ package com.Microsoft.Z3; **/ public Context() { super(); - mCtx = Native.mkContextRc(IntPtr.Zero); + m_ctx = Native.mkContextRc(IntPtr.Zero); InitContext(); } @@ -32,7 +32,7 @@ package com.Microsoft.Z3; IntPtr cfg = Native.mkConfig(); for (KeyValuePair.Iterator kv = settings.iterator(); kv.hasNext(); ) Native.setParamValue(cfg, kv.Key, kv.Value); - mCtx = Native.mkContextRc(cfg); + m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); InitContext(); } @@ -77,9 +77,9 @@ package com.Microsoft.Z3; return result; } - private BoolSort mBooleanSort = null; - private IntSort mIntSort = null; - private RealSort mRealSort = null; + private BoolSort m_booleanSort = null; + private IntSort m_intSort = null; + private RealSort m_realSort = null; /** * Retrieves the Boolean sort of the context. @@ -88,8 +88,8 @@ package com.Microsoft.Z3; { - if (mBooleanSort == null) mBooleanSort = new BoolSort(this); return mBooleanSort; - } + if (m_booleanSort == null) m_booleanSort = new BoolSort(this); return m_booleanSort; + } /** * Retrieves the Integer sort of the context. @@ -97,14 +97,23 @@ package com.Microsoft.Z3; public IntSort IntSort() { - if (mIntSort == null) mIntSort = new IntSort(this); return mIntSort; - } + if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort; + } /** * Retrieves the Real sort of the context. **/ - /* Overloaded operators are not translated. */ + public RealSort RealSort () { return m_realSort; } + + /** + * Create a new Boolean sort. + **/ + public BoolSort MkBoolSort() + { + + return new BoolSort(this); + } /** * Create a new uninterpreted sort. @@ -150,7 +159,7 @@ package com.Microsoft.Z3; /** * Create a new bit-vector sort. **/ - public BitVecSort MkBitVecSort(Integer size) + public BitVecSort MkBitVecSort(long size) { @@ -185,7 +194,7 @@ package com.Microsoft.Z3; CheckContextMatch(name); CheckContextMatch(fieldNames); CheckContextMatch(fieldSorts); - return new TupleSort(this, name, (Integer)fieldNames.Length, fieldNames, fieldSorts); + return new TupleSort(this, name, (long)fieldNames.Length, fieldNames, fieldSorts); } /** @@ -274,7 +283,7 @@ package com.Microsoft.Z3; * 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, Integer[] sortRefs) + public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, long[] sortRefs) { @@ -292,7 +301,7 @@ package com.Microsoft.Z3; * * @return **/ - public Constructor MkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, Integer[] sortRefs) + public Constructor MkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, long[] sortRefs) { @@ -343,22 +352,22 @@ package com.Microsoft.Z3; CheckContextMatch(names); - Integer n = (Integer)names.Length; + long n = (long)names.Length; ConstructorList[] cla = new ConstructorList[n]; - IntPtr[] nConstr = new IntPtr[n]; - for (Integer i = 0; i < n; i++) + IntPtr[] n_constr = new IntPtr[n]; + for (long i = 0; i < n; i++) { var constructor = c[i]; CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); - nConstr[i] = cla[i].NativeObject; + n_constr[i] = cla[i].NativeObject; } - IntPtr[] nRes = new IntPtr[n]; - Native.mkDatatypes(nCtx, n, Symbol.ArrayToNative(names), nRes, nConstr); + IntPtr[] n_res = new IntPtr[n]; + Native.mkDatatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; - for (Integer i = 0; i < n; i++) - res[i] = new DatatypeSort(this, nRes[i]); + for (long i = 0; i < n; i++) + res[i] = new DatatypeSort(this, n_res[i]); return res; } @@ -504,7 +513,7 @@ package com.Microsoft.Z3; * The de-Bruijn index of the variable * The sort of the variable **/ - public Expr MkBound(Integer index, Sort ty) + public Expr MkBound(long index, Sort ty) { @@ -526,7 +535,7 @@ package com.Microsoft.Z3; IntPtr[] termsNative = AST.ArrayToNative(terms); - return new Pattern(this, Native.mkPattern(nCtx, (Integer)terms.Length, termsNative)); + return new Pattern(this, Native.mkPattern(nCtx, (long)terms.Length, termsNative)); } /** @@ -647,7 +656,7 @@ package com.Microsoft.Z3; /** * Creates a bit-vector constant. **/ - public BitVecExpr MkBVConst(Symbol name, Integer size) + public BitVecExpr MkBVConst(Symbol name, long size) { @@ -658,7 +667,7 @@ package com.Microsoft.Z3; /** * Creates a bit-vector constant. **/ - public BitVecExpr MkBVConst(String name, Integer size) + public BitVecExpr MkBVConst(String name, long size) { @@ -734,7 +743,7 @@ package com.Microsoft.Z3; CheckContextMatch(args); - return new BoolExpr(this, Native.mkDistinct(nCtx, (Integer)args.Length, AST.ArrayToNative(args))); + return new BoolExpr(this, Native.mkDistinct(nCtx, (long)args.Length, AST.ArrayToNative(args))); } /** @@ -820,7 +829,7 @@ package com.Microsoft.Z3; CheckContextMatch(t); - return new BoolExpr(this, Native.mkAnd(nCtx, (Integer)t.Length, AST.ArrayToNative(t))); + return new BoolExpr(this, Native.mkAnd(nCtx, (long)t.Length, AST.ArrayToNative(t))); } /** @@ -833,7 +842,7 @@ package com.Microsoft.Z3; CheckContextMatch(t); - return new BoolExpr(this, Native.mkOr(nCtx, (Integer)t.Length, AST.ArrayToNative(t))); + return new BoolExpr(this, Native.mkOr(nCtx, (long)t.Length, AST.ArrayToNative(t))); } /** @@ -846,7 +855,7 @@ package com.Microsoft.Z3; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkAdd(nCtx, (Integer)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkAdd(nCtx, (long)t.Length, AST.ArrayToNative(t))); } /** @@ -859,7 +868,7 @@ package com.Microsoft.Z3; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkMul(nCtx, (Integer)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkMul(nCtx, (long)t.Length, AST.ArrayToNative(t))); } /** @@ -872,7 +881,7 @@ package com.Microsoft.Z3; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkSub(nCtx, (Integer)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkSub(nCtx, (long)t.Length, AST.ArrayToNative(t))); } /** @@ -1503,7 +1512,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkExtract(Integer high, Integer low, BitVecExpr t) + public BitVecExpr MkExtract(long high, long low, BitVecExpr t) { @@ -1520,7 +1529,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkSignExt(Integer i, BitVecExpr t) + public BitVecExpr MkSignExt(long i, BitVecExpr t) { @@ -1538,7 +1547,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkZeroExt(Integer i, BitVecExpr t) + public BitVecExpr MkZeroExt(long i, BitVecExpr t) { @@ -1553,7 +1562,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkRepeat(Integer i, BitVecExpr t) + public BitVecExpr MkRepeat(long i, BitVecExpr t) { @@ -1640,7 +1649,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkBVRotateLeft(Integer i, BitVecExpr t) + public BitVecExpr MkBVRotateLeft(long i, BitVecExpr t) { @@ -1656,7 +1665,7 @@ package com.Microsoft.Z3; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkBVRotateRight(Integer i, BitVecExpr t) + public BitVecExpr MkBVRotateRight(long i, BitVecExpr t) { @@ -1711,7 +1720,7 @@ package com.Microsoft.Z3; * The argument must be of integer sort. * **/ - public BitVecExpr MkInt2BV(Integer n, IntExpr t) + public BitVecExpr MkInt2BV(long n, IntExpr t) { @@ -2089,7 +2098,7 @@ package com.Microsoft.Z3; CheckContextMatch(args); - return Expr.Create(this, Native.mkSetUnion(nCtx, (Integer)args.Length, AST.ArrayToNative(args))); + return Expr.Create(this, Native.mkSetUnion(nCtx, (long)args.Length, AST.ArrayToNative(args))); } /** @@ -2102,7 +2111,7 @@ package com.Microsoft.Z3; CheckContextMatch(args); - return Expr.Create(this, Native.mkSetIntersect(nCtx, (Integer)args.Length, AST.ArrayToNative(args))); + return Expr.Create(this, Native.mkSetIntersect(nCtx, (long)args.Length, AST.ArrayToNative(args))); } /** @@ -2198,7 +2207,7 @@ package com.Microsoft.Z3; * Sort of the numeral * @return A Term with value and type **/ - public Expr MkNumeral(Integer v, Sort ty) + public Expr MkNumeral(long v, Sort ty) { @@ -2286,7 +2295,7 @@ package com.Microsoft.Z3; * value of the numeral. * @return A Term with value and sort Real **/ - public RatNum MkReal(Integer v) + public RatNum MkReal(long v) { @@ -2345,7 +2354,7 @@ package com.Microsoft.Z3; * value of the numeral. * @return A Term with value and sort Integer **/ - public IntNum MkInt(Integer v) + public IntNum MkInt(long v) { @@ -2381,7 +2390,7 @@ package com.Microsoft.Z3; * A string representing the value in decimal notation. * the size of the bit-vector **/ - public BitVecNum MkBV(String v, Integer size) + public BitVecNum MkBV(String v, long size) { @@ -2393,7 +2402,7 @@ package com.Microsoft.Z3; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(int v, Integer size) + public BitVecNum MkBV(int v, long size) { @@ -2405,7 +2414,7 @@ package com.Microsoft.Z3; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(Integer v, Integer size) + public BitVecNum MkBV(long v, long size) { @@ -2417,7 +2426,7 @@ package com.Microsoft.Z3; * value of the numeral. * * the size of the bit-vector **/ - public BitVecNum MkBV(long v, Integer size) + public BitVecNum MkBV(long v, long size) { @@ -2429,7 +2438,7 @@ package com.Microsoft.Z3; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(ulong v, Integer size) + public BitVecNum MkBV(ulong v, long size) { @@ -2456,7 +2465,7 @@ package com.Microsoft.Z3; * optional symbol to track quantifier. * optional symbol to track skolem constants. **/ - public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2476,7 +2485,7 @@ package com.Microsoft.Z3; /** * Create a universal Quantifier. **/ - public Quantifier MkForall(Expr[] boundConstants, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkForall(Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2492,7 +2501,7 @@ package com.Microsoft.Z3; * Create an existential Quantifier. * **/ - public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2510,7 +2519,7 @@ package com.Microsoft.Z3; /** * Create an existential Quantifier. **/ - public Quantifier MkExists(Expr[] boundConstants, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkExists(Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2525,7 +2534,7 @@ package com.Microsoft.Z3; /** * Create a Quantifier. **/ - public Quantifier MkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2548,7 +2557,7 @@ package com.Microsoft.Z3; /** * Create a Quantifier. **/ - public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2581,7 +2590,7 @@ package com.Microsoft.Z3; * * **/ - public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx, Integer(value)); } + public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx, (long)value); } /** * Convert a benchmark into an SMT-LIB formatted string. @@ -2601,7 +2610,7 @@ package com.Microsoft.Z3; return Native.benchmarkToSmtlibString(nCtx, name, logic, status, attributes, - (Integer)assumptions.Length, AST.ArrayToNative(assumptions), + (long)assumptions.Length, AST.ArrayToNative(assumptions), formula.NativeObject); } @@ -2617,10 +2626,10 @@ package com.Microsoft.Z3; **/ public void ParseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - Integer csn = Symbol.ArrayLength(sortNames); - Integer cs = Sort.ArrayLength(sorts); - Integer cdn = Symbol.ArrayLength(declNames); - Integer cd = AST.ArrayLength(decls); + long csn = Symbol.ArrayLength(sortNames); + long cs = Sort.ArrayLength(sorts); + long cdn = Symbol.ArrayLength(declNames); + long cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); Native.parseSmtlibString(nCtx, str, @@ -2634,10 +2643,10 @@ package com.Microsoft.Z3; **/ public void ParseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - Integer csn = Symbol.ArrayLength(sortNames); - Integer cs = Sort.ArrayLength(sorts); - Integer cdn = Symbol.ArrayLength(declNames); - Integer cd = AST.ArrayLength(decls); + long csn = Symbol.ArrayLength(sortNames); + long cs = Sort.ArrayLength(sorts); + long cdn = Symbol.ArrayLength(declNames); + long cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); Native.parseSmtlibFile(nCtx, fileName, @@ -2648,7 +2657,7 @@ package com.Microsoft.Z3; /** * The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. **/ - public Integer NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); } + public long NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); } /** * The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2657,17 +2666,17 @@ package com.Microsoft.Z3; { - Integer n = NumSMTLIBFormulas; + long n = NumSMTLIBFormulas; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long 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 Integer NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); } + public long NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); } /** * The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2676,17 +2685,17 @@ package com.Microsoft.Z3; { - Integer n = NumSMTLIBAssumptions; + long n = NumSMTLIBAssumptions; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long 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 Integer NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); } + public long NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); } /** * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2695,17 +2704,17 @@ package com.Microsoft.Z3; { - Integer n = NumSMTLIBDecls; + long n = NumSMTLIBDecls; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long 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 Integer NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); } + public long NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); } /** * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2714,12 +2723,12 @@ package com.Microsoft.Z3; { - Integer n = NumSMTLIBSorts; + long n = NumSMTLIBSorts; Sort[] res = new Sort[n]; - for (Integer i = 0; i < n; i++) + for (long 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. @@ -2730,10 +2739,10 @@ package com.Microsoft.Z3; { - Integer csn = Symbol.ArrayLength(sortNames); - Integer cs = Sort.ArrayLength(sorts); - Integer cdn = Symbol.ArrayLength(declNames); - Integer cd = AST.ArrayLength(decls); + long csn = Symbol.ArrayLength(sortNames); + long cs = Sort.ArrayLength(sorts); + long cdn = Symbol.ArrayLength(declNames); + long cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); return (BoolExpr)Expr.Create(this, Native.parseSmtlib2String(nCtx, str, @@ -2749,10 +2758,10 @@ package com.Microsoft.Z3; { - Integer csn = Symbol.ArrayLength(sortNames); - Integer cs = Sort.ArrayLength(sorts); - Integer cdn = Symbol.ArrayLength(declNames); - Integer cd = AST.ArrayLength(decls); + long csn = Symbol.ArrayLength(sortNames); + long cs = Sort.ArrayLength(sorts); + long cdn = Symbol.ArrayLength(declNames); + long cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); return (BoolExpr)Expr.Create(this, Native.parseSmtlib2File(nCtx, fileName, @@ -2790,7 +2799,7 @@ package com.Microsoft.Z3; /** * The number of supported tactics. **/ - public Integer NumTactics() { return Native.getNumTactics(nCtx); } + public long NumTactics() { return Native.getNumTactics(nCtx); } /** * The names of all supported tactics. @@ -2799,12 +2808,12 @@ package com.Microsoft.Z3; { - Integer n = NumTactics; + long n = NumTactics; String[] res = new String[n]; - for (Integer i = 0; i < n; i++) + for (long 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. @@ -2896,7 +2905,7 @@ package com.Microsoft.Z3; * If does not terminate within milliseconds, then it fails. * **/ - public Tactic TryFor(Tactic t, Integer ms) + public Tactic TryFor(Tactic t, long ms) { @@ -2944,7 +2953,7 @@ package com.Microsoft.Z3; * 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, Integer max) + public Tactic Repeat(Tactic t, long max) { @@ -3062,7 +3071,7 @@ package com.Microsoft.Z3; /** * The number of supported Probes. **/ - public Integer NumProbes() { return Native.getNumProbes(nCtx); } + public long NumProbes() { return Native.getNumProbes(nCtx); } /** * The names of all supported Probes. @@ -3071,12 +3080,12 @@ package com.Microsoft.Z3; { - Integer n = NumProbes; + long n = NumProbes; String[] res = new String[n]; - for (Integer i = 0; i < n; i++) + for (long 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. @@ -3355,7 +3364,7 @@ package com.Microsoft.Z3; ///// Note that it is possible for memory leaks to occur if error handlers ///// throw exceptions. ///// - //public delegate void ErrorHandler(Context ctx, Z3ErrorCode errorCode, String errorString); + //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, String errorString); ///// ///// The OnError event. @@ -3386,29 +3395,29 @@ package com.Microsoft.Z3; **/ public String GetParamValue(String id) { - IntPtr res = IntPtr.Zero; - int r = Native.getParamValue(nCtx, id, out res); - if (r == (int)Z3Lboolean.Z3LFALSE) + Native.IntPtr res = new Native.IntPtr(); + int r = Native.getParamValue(nCtx, id, res); + if (r == (int)Z3_lboolean.Z3_L_FALSE) return null; else return Marshal.PtrtoStringAnsi(res); } - IntPtr mCtx = IntPtr.Zero; + IntPtr m_ctx = IntPtr.Zero; Native.errorHandler mNErrHandler = null; - IntPtr nCtx () { return mCtx; } + IntPtr nCtx () { return m_ctx; } - void NativeErrorHandler(IntPtr ctx, Z3ErrorCode errorCode) + void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) { // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. } void InitContext() { - PrintMode = Z3AstPrintMode.Z3PRINTSMTLIB2COMPLIANT; - mNErrHandler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected. - Native.setErrorHandler(mCtx, mNErrHandler); + PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT; + m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected. + Native.setErrorHandler(m_ctx, m_n_err_handler); GC.SuppressFinalize(this); } @@ -3453,40 +3462,40 @@ package com.Microsoft.Z3; } - private AST.DecRefQueue mASTDRQ = new AST.DecRefQueue(); - private ASTMap.DecRefQueue mASTMapDRQ = new ASTMap.DecRefQueue(); - private ASTVector.DecRefQueue mASTVectorDRQ = new ASTVector.DecRefQueue(); - private ApplyResult.DecRefQueue mApplyResultDRQ = new ApplyResult.DecRefQueue(); - private FuncInterp.Entry.DecRefQueue mFuncEntryDRQ = new FuncInterp.Entry.DecRefQueue(); - private FuncInterp.DecRefQueue mFuncInterpDRQ = new FuncInterp.DecRefQueue(); - private Goal.DecRefQueue mGoalDRQ = new Goal.DecRefQueue(); - private Model.DecRefQueue mModelDRQ = new Model.DecRefQueue(); - private Params.DecRefQueue mParamsDRQ = new Params.DecRefQueue(); - private ParamDescrs.DecRefQueue mParamDescrsDRQ = new ParamDescrs.DecRefQueue(); - private Probe.DecRefQueue mProbeDRQ = new Probe.DecRefQueue(); - private Solver.DecRefQueue mSolverDRQ = new Solver.DecRefQueue(); - private Statistics.DecRefQueue mStatisticsDRQ = new Statistics.DecRefQueue(); - private Tactic.DecRefQueue mTacticDRQ = new Tactic.DecRefQueue(); - private Fixedpoint.DecRefQueue mFixedpointDRQ = new Fixedpoint.DecRefQueue(); + private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue(); + private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(); + private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(); + private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(); + private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(); + private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(); + private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(); + private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(); + private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(); + private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(); + private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(); + private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(); + private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(); + private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(); + private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(); - AST.DecRefQueue AST_DRQ () { Contract.Ensures(Contract.Result() != null); return mASTDRQ; } - ASTMap.DecRefQueue ASTMap_DRQ () { Contract.Ensures(Contract.Result() != null); return mASTMapDRQ; } - ASTVector.DecRefQueue ASTVector_DRQ () { Contract.Ensures(Contract.Result() != null); return mASTVectorDRQ; } - ApplyResult.DecRefQueue ApplyResult_DRQ () { Contract.Ensures(Contract.Result() != null); return mApplyResultDRQ; } - FuncInterp.Entry.DecRefQueue FuncEntry_DRQ () { Contract.Ensures(Contract.Result() != null); return mFuncEntryDRQ; } - FuncInterp.DecRefQueue FuncInterp_DRQ () { Contract.Ensures(Contract.Result() != null); return mFuncInterpDRQ; } - Goal.DecRefQueue Goal_DRQ () { Contract.Ensures(Contract.Result() != null); return mGoalDRQ; } - Model.DecRefQueue Model_DRQ () { Contract.Ensures(Contract.Result() != null); return mModelDRQ; } - Params.DecRefQueue Params_DRQ () { Contract.Ensures(Contract.Result() != null); return mParamsDRQ; } - ParamDescrs.DecRefQueue ParamDescrs_DRQ () { Contract.Ensures(Contract.Result() != null); return mParamDescrsDRQ; } - Probe.DecRefQueue Probe_DRQ () { Contract.Ensures(Contract.Result() != null); return mProbeDRQ; } - Solver.DecRefQueue Solver_DRQ () { Contract.Ensures(Contract.Result() != null); return mSolverDRQ; } - Statistics.DecRefQueue Statistics_DRQ () { Contract.Ensures(Contract.Result() != null); return mStatisticsDRQ; } - Tactic.DecRefQueue Tactic_DRQ () { Contract.Ensures(Contract.Result() != null); return mTacticDRQ; } - Fixedpoint.DecRefQueue Fixedpoint_DRQ () { Contract.Ensures(Contract.Result() != null); return mFixedpointDRQ; } + AST.DecRefQueue AST_DRQ () { return m_AST_DRQ; } + ASTMap.DecRefQueue ASTMap_DRQ () { return m_ASTMap_DRQ; } + ASTVector.DecRefQueue ASTVector_DRQ () { return m_ASTVector_DRQ; } + ApplyResult.DecRefQueue ApplyResult_DRQ () { return m_ApplyResult_DRQ; } + FuncInterp.Entry.DecRefQueue FuncEntry_DRQ () { return m_FuncEntry_DRQ; } + FuncInterp.DecRefQueue FuncInterp_DRQ () { return m_FuncInterp_DRQ; } + Goal.DecRefQueue Goal_DRQ () { return m_Goal_DRQ; } + Model.DecRefQueue Model_DRQ () { return m_Model_DRQ; } + Params.DecRefQueue Params_DRQ () { return m_Params_DRQ; } + ParamDescrs.DecRefQueue ParamDescrs_DRQ () { return m_ParamDescrs_DRQ; } + Probe.DecRefQueue Probe_DRQ () { return m_Probe_DRQ; } + Solver.DecRefQueue Solver_DRQ () { return m_Solver_DRQ; } + Statistics.DecRefQueue Statistics_DRQ () { return m_Statistics_DRQ; } + Tactic.DecRefQueue Tactic_DRQ () { return m_Tactic_DRQ; } + Fixedpoint.DecRefQueue Fixedpoint_DRQ () { return m_Fixedpoint_DRQ; } - Integer refCount = 0; + long refCount = 0; /** * Finalizer. @@ -3498,9 +3507,9 @@ package com.Microsoft.Z3; if (refCount == 0) { - mNErrHandler = null; - Native.delContext(mCtx); - mCtx = IntPtr.Zero; + m_n_err_handler = null; + Native.delContext(m_ctx); + m_ctx = IntPtr.Zero; } else GC.ReRegisterForFinalize(this); @@ -3512,23 +3521,23 @@ package com.Microsoft.Z3; public void Dispose() { // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId); - ASTDRQ.Clear(this); - ASTMapDRQ.Clear(this); - ASTVectorDRQ.Clear(this); - ApplyResultDRQ.Clear(this); - FuncEntryDRQ.Clear(this); - FuncInterpDRQ.Clear(this); - GoalDRQ.Clear(this); - ModelDRQ.Clear(this); - ParamsDRQ.Clear(this); - ProbeDRQ.Clear(this); - SolverDRQ.Clear(this); - StatisticsDRQ.Clear(this); - TacticDRQ.Clear(this); - FixedpointDRQ.Clear(this); + AST_DRQ.Clear(this); + ASTMap_DRQ.Clear(this); + ASTVector_DRQ.Clear(this); + ApplyResult_DRQ.Clear(this); + FuncEntry_DRQ.Clear(this); + FuncInterp_DRQ.Clear(this); + Goal_DRQ.Clear(this); + Model_DRQ.Clear(this); + Params_DRQ.Clear(this); + Probe_DRQ.Clear(this); + Solver_DRQ.Clear(this); + Statistics_DRQ.Clear(this); + Tactic_DRQ.Clear(this); + Fixedpoint_DRQ.Clear(this); - mBooleanSort = null; - mIntSort = null; - mRealSort = null; + m_booleanSort = null; + m_intSort = null; + m_realSort = null; } } diff --git a/src/api/java/com/Microsoft/Z3/DecRefQUeue.java b/src/api/java/com/Microsoft/Z3/DecRefQUeue.java index 1e1f13881..279887a7c 100644 --- a/src/api/java/com/Microsoft/Z3/DecRefQUeue.java +++ b/src/api/java/com/Microsoft/Z3/DecRefQUeue.java @@ -10,41 +10,61 @@ package com.Microsoft.Z3; /* using System.Threading; */ abstract class DecRefQueue + { private void ObjectInvariant() + { + } - readonly protected Object mLock = new Object(); - readonly protected List mQueue = new List(); - const Integer mMoveLimit = 1024; + protected Object m_lock = new Object(); + protected List m_queue = new List(); + final long m_move_limit = 1024; public abstract void IncRef(Context ctx, IntPtr obj); public abstract void DecRef(Context ctx, IntPtr obj); public void IncAndClear(Context ctx, IntPtr o) + { IncRef(ctx, o); - if (mQueue.Count >= mMoveLimit) Clear(ctx); + if (m_queue.Count >= m_move_limit) Clear(ctx); + } public void Add(IntPtr o) + { if (o == IntPtr.Zero) return; - lock (mLock) - mQueue.Add(o); + synchronized (m_lock) + { + m_queue.Add(o); + } + } public void Clear(Context ctx) + { - lock (mLock) - for (IntPtr.Iterator o = mQueue.iterator(); o.hasNext(); ) + synchronized (m_lock) + { + for (IntPtr.Iterator o = m_queue.iterator(); o.hasNext(); ) DecRef(ctx, o); - mQueue.Clear(); + m_queue.Clear(); + } + } + } - abstract class DecRefQueueContracts : DecRefQueue + abstract class DecRefQueueContracts extends DecRefQueue + { public void IncRef(Context ctx, IntPtr obj) + { + } public void DecRef(Context ctx, IntPtr obj) + { + } + } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java new file mode 100644 index 000000000..2ba3f58ab --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java @@ -0,0 +1,19 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_ast_kind + **/ +public enum Z3_ast_kind { +Z3_VAR_AST (2), +Z3_SORT_AST (4), +Z3_QUANTIFIER_AST (3), +Z3_UNKNOWN_AST (1000), +Z3_FUNC_DECL_AST (5), +Z3_NUMERAL_AST (0), +Z3_APP_AST (1), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java new file mode 100644 index 000000000..4aa4a2716 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java @@ -0,0 +1,16 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_ast_print_mode + **/ +public enum Z3_ast_print_mode { +Z3_PRINT_SMTLIB2_COMPLIANT (3), +Z3_PRINT_SMTLIB_COMPLIANT (2), +Z3_PRINT_SMTLIB_FULL (0), +Z3_PRINT_LOW_LEVEL (1), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java new file mode 100644 index 000000000..3b0b01715 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java @@ -0,0 +1,164 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_decl_kind + **/ +public enum Z3_decl_kind { +Z3_OP_LABEL (1792), +Z3_OP_PR_REWRITE (1294), +Z3_OP_UNINTERPRETED (2051), +Z3_OP_SUB (519), +Z3_OP_ZERO_EXT (1058), +Z3_OP_ADD (518), +Z3_OP_IS_INT (528), +Z3_OP_BREDOR (1061), +Z3_OP_BNOT (1051), +Z3_OP_BNOR (1054), +Z3_OP_PR_CNF_STAR (1315), +Z3_OP_RA_JOIN (1539), +Z3_OP_LE (514), +Z3_OP_SET_UNION (773), +Z3_OP_PR_UNDEF (1280), +Z3_OP_BREDAND (1062), +Z3_OP_LT (516), +Z3_OP_RA_UNION (1540), +Z3_OP_BADD (1028), +Z3_OP_BUREM0 (1039), +Z3_OP_OEQ (267), +Z3_OP_PR_MODUS_PONENS (1284), +Z3_OP_RA_CLONE (1548), +Z3_OP_REPEAT (1060), +Z3_OP_RA_NEGATION_FILTER (1544), +Z3_OP_BSMOD0 (1040), +Z3_OP_BLSHR (1065), +Z3_OP_BASHR (1066), +Z3_OP_PR_UNIT_RESOLUTION (1304), +Z3_OP_ROTATE_RIGHT (1068), +Z3_OP_ARRAY_DEFAULT (772), +Z3_OP_PR_PULL_QUANT (1296), +Z3_OP_PR_APPLY_DEF (1310), +Z3_OP_PR_REWRITE_STAR (1295), +Z3_OP_IDIV (523), +Z3_OP_PR_GOAL (1283), +Z3_OP_PR_IFF_TRUE (1305), +Z3_OP_LABEL_LIT (1793), +Z3_OP_BOR (1050), +Z3_OP_PR_SYMMETRY (1286), +Z3_OP_TRUE (256), +Z3_OP_SET_COMPLEMENT (776), +Z3_OP_CONCAT (1056), +Z3_OP_PR_NOT_OR_ELIM (1293), +Z3_OP_IFF (263), +Z3_OP_BSHL (1064), +Z3_OP_PR_TRANSITIVITY (1287), +Z3_OP_SGT (1048), +Z3_OP_RA_WIDEN (1541), +Z3_OP_PR_DEF_INTRO (1309), +Z3_OP_NOT (265), +Z3_OP_PR_QUANT_INTRO (1290), +Z3_OP_UGT (1047), +Z3_OP_DT_RECOGNISER (2049), +Z3_OP_SET_INTERSECT (774), +Z3_OP_BSREM (1033), +Z3_OP_RA_STORE (1536), +Z3_OP_SLT (1046), +Z3_OP_ROTATE_LEFT (1067), +Z3_OP_PR_NNF_NEG (1313), +Z3_OP_PR_REFLEXIVITY (1285), +Z3_OP_ULEQ (1041), +Z3_OP_BIT1 (1025), +Z3_OP_BIT0 (1026), +Z3_OP_EQ (258), +Z3_OP_BMUL (1030), +Z3_OP_ARRAY_MAP (771), +Z3_OP_STORE (768), +Z3_OP_PR_HYPOTHESIS (1302), +Z3_OP_RA_RENAME (1545), +Z3_OP_AND (261), +Z3_OP_TO_REAL (526), +Z3_OP_PR_NNF_POS (1312), +Z3_OP_PR_AND_ELIM (1292), +Z3_OP_MOD (525), +Z3_OP_BUDIV0 (1037), +Z3_OP_PR_TRUE (1281), +Z3_OP_BNAND (1053), +Z3_OP_PR_ELIM_UNUSED_VARS (1299), +Z3_OP_RA_FILTER (1543), +Z3_OP_FD_LT (1549), +Z3_OP_RA_EMPTY (1537), +Z3_OP_DIV (522), +Z3_OP_ANUM (512), +Z3_OP_MUL (521), +Z3_OP_UGEQ (1043), +Z3_OP_BSREM0 (1038), +Z3_OP_PR_TH_LEMMA (1318), +Z3_OP_BXOR (1052), +Z3_OP_DISTINCT (259), +Z3_OP_PR_IFF_FALSE (1306), +Z3_OP_BV2INT (1072), +Z3_OP_EXT_ROTATE_LEFT (1069), +Z3_OP_PR_PULL_QUANT_STAR (1297), +Z3_OP_BSUB (1029), +Z3_OP_PR_ASSERTED (1282), +Z3_OP_BXNOR (1055), +Z3_OP_EXTRACT (1059), +Z3_OP_PR_DER (1300), +Z3_OP_DT_CONSTRUCTOR (2048), +Z3_OP_GT (517), +Z3_OP_BUREM (1034), +Z3_OP_IMPLIES (266), +Z3_OP_SLEQ (1042), +Z3_OP_GE (515), +Z3_OP_BAND (1049), +Z3_OP_ITE (260), +Z3_OP_AS_ARRAY (778), +Z3_OP_RA_SELECT (1547), +Z3_OP_CONST_ARRAY (770), +Z3_OP_BSDIV (1031), +Z3_OP_OR (262), +Z3_OP_PR_HYPER_RESOLVE (1319), +Z3_OP_AGNUM (513), +Z3_OP_PR_PUSH_QUANT (1298), +Z3_OP_BSMOD (1035), +Z3_OP_PR_IFF_OEQ (1311), +Z3_OP_PR_LEMMA (1303), +Z3_OP_SET_SUBSET (777), +Z3_OP_SELECT (769), +Z3_OP_RA_PROJECT (1542), +Z3_OP_BNEG (1027), +Z3_OP_UMINUS (520), +Z3_OP_REM (524), +Z3_OP_TO_INT (527), +Z3_OP_PR_QUANT_INST (1301), +Z3_OP_SGEQ (1044), +Z3_OP_POWER (529), +Z3_OP_XOR3 (1074), +Z3_OP_RA_IS_EMPTY (1538), +Z3_OP_CARRY (1073), +Z3_OP_DT_ACCESSOR (2050), +Z3_OP_PR_TRANSITIVITY_STAR (1288), +Z3_OP_PR_NNF_STAR (1314), +Z3_OP_PR_COMMUTATIVITY (1307), +Z3_OP_ULT (1045), +Z3_OP_BSDIV0 (1036), +Z3_OP_SET_DIFFERENCE (775), +Z3_OP_INT2BV (1071), +Z3_OP_XOR (264), +Z3_OP_PR_MODUS_PONENS_OEQ (1317), +Z3_OP_BNUM (1024), +Z3_OP_BUDIV (1032), +Z3_OP_PR_MONOTONICITY (1289), +Z3_OP_PR_DEF_AXIOM (1308), +Z3_OP_FALSE (257), +Z3_OP_EXT_ROTATE_RIGHT (1070), +Z3_OP_PR_DISTRIBUTIVITY (1291), +Z3_OP_SIGN_EXT (1057), +Z3_OP_PR_SKOLEMIZE (1316), +Z3_OP_BCOMP (1063), +Z3_OP_RA_COMPLEMENT (1546), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java new file mode 100644 index 000000000..ef5fa6f2c --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java @@ -0,0 +1,25 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_error_code + **/ +public enum Z3_error_code { +Z3_INVALID_PATTERN (6), +Z3_MEMOUT_FAIL (7), +Z3_NO_PARSER (5), +Z3_OK (0), +Z3_INVALID_ARG (3), +Z3_EXCEPTION (12), +Z3_IOB (2), +Z3_INTERNAL_FATAL (9), +Z3_INVALID_USAGE (10), +Z3_FILE_ACCESS_ERROR (8), +Z3_SORT_ERROR (1), +Z3_PARSER_ERROR (4), +Z3_DEC_REF_ERROR (11), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java new file mode 100644 index 000000000..38e2fdf96 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java @@ -0,0 +1,16 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_goal_prec + **/ +public enum Z3_goal_prec { +Z3_GOAL_UNDER (1), +Z3_GOAL_PRECISE (0), +Z3_GOAL_UNDER_OVER (3), +Z3_GOAL_OVER (2), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java new file mode 100644 index 000000000..63ee2e227 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java @@ -0,0 +1,15 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_lbool + **/ +public enum Z3_lbool { +Z3_L_TRUE (1), +Z3_L_UNDEF (0), +Z3_L_FALSE (-1), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java new file mode 100644 index 000000000..e3d8c0e77 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java @@ -0,0 +1,19 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_param_kind + **/ +public enum Z3_param_kind { +Z3_PK_BOOL (1), +Z3_PK_SYMBOL (3), +Z3_PK_OTHER (5), +Z3_PK_INVALID (6), +Z3_PK_UINT (0), +Z3_PK_STRING (4), +Z3_PK_DOUBLE (2), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java new file mode 100644 index 000000000..0de56c3cd --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java @@ -0,0 +1,19 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_parameter_kind + **/ +public enum Z3_parameter_kind { +Z3_PARAMETER_FUNC_DECL (6), +Z3_PARAMETER_DOUBLE (1), +Z3_PARAMETER_SYMBOL (3), +Z3_PARAMETER_INT (0), +Z3_PARAMETER_AST (5), +Z3_PARAMETER_SORT (4), +Z3_PARAMETER_RATIONAL (2), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java new file mode 100644 index 000000000..59a69b4c0 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java @@ -0,0 +1,22 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_sort_kind + **/ +public enum Z3_sort_kind { +Z3_BV_SORT (4), +Z3_FINITE_DOMAIN_SORT (8), +Z3_ARRAY_SORT (5), +Z3_UNKNOWN_SORT (1000), +Z3_RELATION_SORT (7), +Z3_REAL_SORT (3), +Z3_INT_SORT (2), +Z3_UNINTERPRETED_SORT (0), +Z3_BOOL_SORT (1), +Z3_DATATYPE_SORT (6), +} + diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java new file mode 100644 index 000000000..efe5804eb --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java @@ -0,0 +1,14 @@ +/** + * Automatically generated file + **/ + +package com.Microsoft.Z3; + +/** + * Z3_symbol_kind + **/ +public enum Z3_symbol_kind { +Z3_INT_SYMBOL (0), +Z3_STRING_SYMBOL (1), +} + diff --git a/src/api/java/com/Microsoft/Z3/Expr.java b/src/api/java/com/Microsoft/Z3/Expr.java index 480f5f6b6..760fe813d 100644 --- a/src/api/java/com/Microsoft/Z3/Expr.java +++ b/src/api/java/com/Microsoft/Z3/Expr.java @@ -29,20 +29,22 @@ package com.Microsoft.Z3; /** * The function declaration of the function that is applied in this expression. **/ - public FuncDecl FuncDecl() { + public FuncDecl FuncDecl() + { - return new FuncDecl(Context, Native.getAppDecl(Context.nCtx, NativeObject)); } + return new FuncDecl(Context, Native.getAppDecl(Context.nCtx, NativeObject)); + } /** * Indicates whether the expression is the true or false expression * or something else (Z3_L_UNDEF). **/ - public Z3_lboolean BoolValue() { return (Z3Lboolean)Native.getBooleanValue(Context.nCtx, NativeObject); } + public Z3_lboolean BoolValue() { return (Z3_lboolean)Native.getBooleanValue(Context.nCtx, NativeObject); } /** * The number of arguments of the expression. **/ - public Integer NumArgs() { return Native.getAppNumArgs(Context.nCtx, NativeObject); } + public long NumArgs() { return Native.getAppNumArgs(Context.nCtx, NativeObject); } /** * The arguments of the expression. @@ -51,12 +53,12 @@ package com.Microsoft.Z3; { - Integer n = NumArgs; + long n = NumArgs; Expr[] res = new Expr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Expr.Create(Context, Native.getAppArg(Context.nCtx, NativeObject, i)); return res; - } + } /** * Update the arguments of the expression using the arguments @@ -70,7 +72,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(args); if (args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); - NativeObject = Native.updateTerm(Context.nCtx, NativeObject, (Integer)args.Length, Expr.ArrayToNative(args)); + NativeObject = Native.updateTerm(Context.nCtx, NativeObject, (long)args.Length, Expr.ArrayToNative(args)); } /** @@ -93,7 +95,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(to); if (from.Length != to.Length) throw new Z3Exception("Argument sizes do not match"); - return Expr.Create(Context, Native.substitute(Context.nCtx, NativeObject, (Integer)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); + return Expr.Create(Context, Native.substitute(Context.nCtx, NativeObject, (long)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); } /** @@ -122,7 +124,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(to); - return Expr.Create(Context, Native.substituteVars(Context.nCtx, NativeObject, (Integer)to.Length, Expr.ArrayToNative(to))); + return Expr.Create(Context, Native.substituteVars(Context.nCtx, NativeObject, (long)to.Length, Expr.ArrayToNative(to))); } /** @@ -147,7 +149,7 @@ package com.Microsoft.Z3; public String toString() { return super.toString(); - } + } /** * Indicates whether the term is a numeral @@ -163,9 +165,11 @@ package com.Microsoft.Z3; /** * The Sort of the term. **/ - public Sort Sort() { + public Sort Sort() + { - return Sort.Create(Context, Native.getSort(Context.nCtx, NativeObject)); } + return Sort.Create(Context, Native.getSort(Context.nCtx, NativeObject)); + } /** * Indicates whether the term represents a constant. @@ -197,37 +201,1024 @@ package com.Microsoft.Z3; Native.isEqSort(Context.nCtx, Native.mkBooleanSort(Context.nCtx), Native.getSort(Context.nCtx, NativeObject)) != 0); - } + } /** * Indicates whether the term is the constant true. **/ - /* Overloaded operators are not translated. */ - } + public boolean IsTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } + + /** + * Indicates whether the term is the constant false. + **/ + public boolean IsFalse() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } + + /** + * Indicates whether the term is an equality predicate. + **/ + public boolean IsEq() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } + + /** + * Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). + **/ + public boolean IsDistinct() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } + + /** + * Indicates whether the term is a ternary if-then-else term + **/ + public boolean IsITE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } + + /** + * Indicates whether the term is an n-ary conjunction + **/ + public boolean IsAnd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } + + /** + * Indicates whether the term is an n-ary disjunction + **/ + public boolean IsOr() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } + + /** + * Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) + **/ + public boolean IsIff() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } + + /** + * Indicates whether the term is an exclusive or + **/ + public boolean IsXor() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } + + /** + * Indicates whether the term is a negation + **/ + public boolean IsNot() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } + + /** + * Indicates whether the term is an implication + **/ + public boolean IsImplies() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } + + /** + * Indicates whether the term is of integer sort. + **/ + public boolean IsInt() + { + return (Native.isNumeralAst(Context.nCtx, NativeObject) != 0 && + Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == (long)Z3_sort_kind.Z3_INT_SORT); + } /** * Indicates whether the term is of sort real. **/ - public boolean IsReal() { return Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == (Integer)Z3SortKind.Z3REALSORT; } + public boolean IsReal() { return Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == (long)Z3_sort_kind.Z3_REAL_SORT; } /** * Indicates whether the term is an arithmetic numeral. **/ - /* Overloaded operators are not translated. */ - } + public boolean IsArithmeticNumeral() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } + + /** + * Indicates whether the term is a less-than-or-equal + **/ + public boolean IsLE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } + + /** + * Indicates whether the term is a greater-than-or-equal + **/ + public boolean IsGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } + + /** + * Indicates whether the term is a less-than + **/ + public boolean IsLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } + + /** + * Indicates whether the term is a greater-than + **/ + public boolean IsGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } + + /** + * Indicates whether the term is addition (binary) + **/ + public boolean IsAdd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } + + /** + * Indicates whether the term is subtraction (binary) + **/ + public boolean IsSub() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } + + /** + * Indicates whether the term is a unary minus + **/ + public boolean IsUMinus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } + + /** + * Indicates whether the term is multiplication (binary) + **/ + public boolean IsMul() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } + + /** + * Indicates whether the term is division (binary) + **/ + public boolean IsDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } + + /** + * Indicates whether the term is integer division (binary) + **/ + public boolean IsIDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } + + /** + * Indicates whether the term is remainder (binary) + **/ + public boolean IsRemainder() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } + + /** + * Indicates whether the term is modulus (binary) + **/ + public boolean IsModulus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } + + /** + * Indicates whether the term is a coercion of integer to real (unary) + **/ + public boolean IsIntToReal() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } + + /** + * Indicates whether the term is a coercion of real to integer (unary) + **/ + public boolean IsRealToInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } + + /** + * Indicates whether the term is a check that tests whether a real is integral (unary) + **/ + public boolean IsRealIsInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } + + /** + * Indicates whether the term is of an array sort. + **/ + public boolean IsArray() + { + return (Native.isApp(Context.nCtx, NativeObject) != 0 && + (Z3_sort_kind)Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); + } /** * Indicates whether the term is an array store. * It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). * Array store takes at least 3 arguments. **/ - /* Overloaded operators are not translated. */ + public boolean IsStore() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } + + /** + * Indicates whether the term is an array select. + **/ + public boolean IsSelect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } + + /** + * Indicates whether the term is a constant array. + * For example, select(const(v),i) = v holds for every v and i. The function is unary. + **/ + public boolean IsConstantArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } + + /** + * Indicates whether the term is a default array. + * For example default(const(v)) = v. The function is unary. + **/ + public boolean IsDefaultArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } + + /** + * Indicates whether the term is an array map. + * It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. + **/ + public boolean IsArrayMap() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } + + /** + * Indicates whether the term is an as-array term. + * An as-array term is n array value that behaves as the function graph of the + * function passed as parameter. + **/ + public boolean IsAsArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } + + /** + * Indicates whether the term is set union + **/ + public boolean IsSetUnion() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } + + /** + * Indicates whether the term is set intersection + **/ + public boolean IsSetIntersect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } + + /** + * Indicates whether the term is set difference + **/ + public boolean IsSetDifference() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } + + /** + * Indicates whether the term is set complement + **/ + public boolean IsSetComplement() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } + + /** + * Indicates whether the term is set subset + **/ + public boolean IsSetSubset() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } + + /** + * Indicates whether the terms is of bit-vector sort. + **/ + public boolean IsBV() { return Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == (long)Z3_sort_kind.Z3_BV_SORT; } /** * Indicates whether the term is a bit-vector numeral **/ - /* Overloaded operators are not translated. */ - } + public boolean IsBVNumeral() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } + + /** + * Indicates whether the term is a one-bit bit-vector with value one + **/ + public boolean IsBVBitOne() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } + + /** + * Indicates whether the term is a one-bit bit-vector with value zero + **/ + public boolean IsBVBitZero() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } + + /** + * Indicates whether the term is a bit-vector unary minus + **/ + public boolean IsBVUMinus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } + + /** + * Indicates whether the term is a bit-vector addition (binary) + **/ + public boolean IsBVAdd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } + + /** + * Indicates whether the term is a bit-vector subtraction (binary) + **/ + public boolean IsBVSub() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } + + /** + * Indicates whether the term is a bit-vector multiplication (binary) + **/ + public boolean IsBVMul() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } + + /** + * Indicates whether the term is a bit-vector signed division (binary) + **/ + public boolean IsBVSDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } + + /** + * Indicates whether the term is a bit-vector unsigned division (binary) + **/ + public boolean IsBVUDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } + + /** + * Indicates whether the term is a bit-vector signed remainder (binary) + **/ + public boolean IsBVSRem() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } + + /** + * Indicates whether the term is a bit-vector unsigned remainder (binary) + **/ + public boolean IsBVURem() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } + + /** + * Indicates whether the term is a bit-vector signed modulus + **/ + public boolean IsBVSMod() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } + + /** + * Indicates whether the term is a bit-vector signed division by zero + **/ + boolean IsBVSDiv0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } + + /** + * Indicates whether the term is a bit-vector unsigned division by zero + **/ + boolean IsBVUDiv0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } + + /** + * Indicates whether the term is a bit-vector signed remainder by zero + **/ + boolean IsBVSRem0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } + + /** + * Indicates whether the term is a bit-vector unsigned remainder by zero + **/ + boolean IsBVURem0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } + + /** + * Indicates whether the term is a bit-vector signed modulus by zero + **/ + boolean IsBVSMod0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } + + /** + * Indicates whether the term is an unsigned bit-vector less-than-or-equal + **/ + public boolean IsBVULE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } + + /** + * Indicates whether the term is a signed bit-vector less-than-or-equal + **/ + public boolean IsBVSLE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } + + /** + * Indicates whether the term is an unsigned bit-vector greater-than-or-equal + **/ + public boolean IsBVUGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } + + /** + * Indicates whether the term is a signed bit-vector greater-than-or-equal + **/ + public boolean IsBVSGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } + + /** + * Indicates whether the term is an unsigned bit-vector less-than + **/ + public boolean IsBVULT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } + + /** + * Indicates whether the term is a signed bit-vector less-than + **/ + public boolean IsBVSLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } + + /** + * Indicates whether the term is an unsigned bit-vector greater-than + **/ + public boolean IsBVUGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } + + /** + * Indicates whether the term is a signed bit-vector greater-than + **/ + public boolean IsBVSGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } + + /** + * Indicates whether the term is a bit-wise AND + **/ + public boolean IsBVAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } + + /** + * Indicates whether the term is a bit-wise OR + **/ + public boolean IsBVOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } + + /** + * Indicates whether the term is a bit-wise NOT + **/ + public boolean IsBVNOT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } + + /** + * Indicates whether the term is a bit-wise XOR + **/ + public boolean IsBVXOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } + + /** + * Indicates whether the term is a bit-wise NAND + **/ + public boolean IsBVNAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } + + /** + * Indicates whether the term is a bit-wise NOR + **/ + public boolean IsBVNOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } + + /** + * Indicates whether the term is a bit-wise XNOR + **/ + public boolean IsBVXNOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } + + /** + * Indicates whether the term is a bit-vector concatenation (binary) + **/ + public boolean IsBVConcat() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } + + /** + * Indicates whether the term is a bit-vector sign extension + **/ + public boolean IsBVSignExtension() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } + + /** + * Indicates whether the term is a bit-vector zero extension + **/ + public boolean IsBVZeroExtension() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } + + /** + * Indicates whether the term is a bit-vector extraction + **/ + public boolean IsBVExtract() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } + + /** + * Indicates whether the term is a bit-vector repetition + **/ + public boolean IsBVRepeat() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } + + /** + * Indicates whether the term is a bit-vector reduce OR + **/ + public boolean IsBVReduceOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } + + /** + * Indicates whether the term is a bit-vector reduce AND + **/ + public boolean IsBVReduceAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } + + /** + * Indicates whether the term is a bit-vector comparison + **/ + public boolean IsBVComp() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } + + /** + * Indicates whether the term is a bit-vector shift left + **/ + public boolean IsBVShiftLeft() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } + + /** + * Indicates whether the term is a bit-vector logical shift right + **/ + public boolean IsBVShiftRightLogical() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } + + /** + * Indicates whether the term is a bit-vector arithmetic shift left + **/ + public boolean IsBVShiftRightArithmetic() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } + + /** + * Indicates whether the term is a bit-vector rotate left + **/ + public boolean IsBVRotateLeft() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } + + /** + * Indicates whether the term is a bit-vector rotate right + **/ + public boolean IsBVRotateRight() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } + + /** + * Indicates whether the term is a bit-vector rotate left (extended) + * Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. + **/ + public boolean IsBVRotateLeftExtended() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } + + /** + * Indicates whether the term is a bit-vector rotate right (extended) + * Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. + **/ + public boolean IsBVRotateRightExtended() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } + + /** + * Indicates whether the term is a coercion from integer to bit-vector + * This function is not supported by the decision procedures. Only the most + * rudimentary simplification rules are applied to this function. + **/ + public boolean IsIntToBV() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } + + /** + * Indicates whether the term is a coercion from bit-vector to integer + * This function is not supported by the decision procedures. Only the most + * rudimentary simplification rules are applied to this function. + **/ + public boolean IsBVToInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } + + /** + * Indicates whether the term is a bit-vector carry + * Compute the carry bit in a full-adder. The meaning is given by the + * equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) + **/ + public boolean IsBVCarry() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } + + /** + * Indicates whether the term is a bit-vector ternary XOR + * The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) + **/ + public boolean IsBVXOR3() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } + + + /** + * Indicates whether the term is a label (used by the Boogie Verification condition generator). + * The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. + **/ + public boolean IsLabel() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } + + /** + * Indicates whether the term is a label literal (used by the Boogie Verification condition generator). + * A label literal has a set of string parameters. It takes no arguments. + **/ + public boolean IsLabelLit() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } + + /** + * Indicates whether the term is a binary equivalence modulo namings. + * This binary predicate is used in proof terms. + * It captures equisatisfiability and equivalence modulo renamings. + **/ + public boolean IsOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } + + /** + * Indicates whether the term is a Proof for the expression 'true'. + **/ + public boolean IsProofTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } + + /** + * Indicates whether the term is a proof for a fact asserted by the user. + **/ + public boolean IsProofAsserted() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } + + /** + * Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. + **/ + public boolean IsProofGoal() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } + + /** + * Indicates whether the term is proof via modus ponens + * + * Given a proof for p and a proof for (implies p q), produces a proof for q. + * T1: p + * T2: (implies p q) + * [mp T1 T2]: q + * The second antecedents may also be a proof for (iff p q). + **/ + public boolean IsProofModusPonens() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } + + /** + * Indicates whether the term is a proof for (R t t), where R is a reflexive relation. + * This proof object has no antecedents. + * The only reflexive relations that are used are + * equivalence modulo namings, equality and equivalence. + * That is, R is either '~', '=' or 'iff'. + **/ + public boolean IsProofReflexivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } + + /** + * Indicates whether the term is proof by symmetricity of a relation + * + * Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). + * T1: (R t s) + * [symmetry T1]: (R s t) + * T1 is the antecedent of this proof object. + * + **/ + public boolean IsProofSymmetry() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } + + /** + * Indicates whether the term is a proof by transitivity of a relation + * + * Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof + * for (R t u). + * T1: (R t s) + * T2: (R s u) + * [trans T1 T2]: (R t u) + * + **/ + public boolean IsProofTransitivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } + + /** + * Indicates whether the term is a proof by condensed transitivity of a relation + * + * Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. + * It combines several symmetry and transitivity proofs. + * Example: + * T1: (R a b) + * T2: (R c b) + * T3: (R c d) + * [trans* T1 T2 T3]: (R a d) + * R must be a symmetric and transitive relation. + * + * Assuming that this proof object is a proof for (R s t), then + * a proof checker must check if it is possible to prove (R s t) + * using the antecedents, symmetry and transitivity. That is, + * if there is a path from s to t, if we view every + * antecedent (R a b) as an edge between a and b. + * + **/ + public boolean IsProofTransitivityStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } + + + /** + * Indicates whether the term is a monotonicity proof object. + * + * T1: (R t_1 s_1) + * ... + * Tn: (R t_n s_n) + * [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) + * Remark: if t_i == s_i, then the antecedent Ti is suppressed. + * That is, reflexivity proofs are supressed to save space. + * + **/ + public boolean IsProofMonotonicity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } + + /** + * Indicates whether the term is a quant-intro proof + * + * Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). + * T1: (~ p q) + * [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) + * + **/ + public boolean IsProofQuantIntro() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } + + /** + * Indicates whether the term is a distributivity proof object. + * + * Given that f (= or) distributes over g (= and), produces a proof for + * (= (f a (g c d)) + * (g (f a c) (f a d))) + * If f and g are associative, this proof also justifies the following equality: + * (= (f (g a b) (g c d)) + * (g (f a c) (f a d) (f b c) (f b d))) + * where each f and g can have arbitrary number of arguments. + * + * This proof object has no antecedents. + * Remark. This rule is used by the CNF conversion pass and + * instantiated by f = or, and g = and. + * + **/ + public boolean IsProofDistributivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } + + /** + * Indicates whether the term is a proof by elimination of AND + * + * Given a proof for (and l_1 ... l_n), produces a proof for l_i + * T1: (and l_1 ... l_n) + * [and-elim T1]: l_i + * + **/ + public boolean IsProofAndElimination() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } + + /** + * Indicates whether the term is a proof by eliminiation of not-or + * + * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). + * T1: (not (or l_1 ... l_n)) + * [not-or-elim T1]: (not l_i) + * + **/ + public boolean IsProofOrElimination() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } + + /** + * Indicates whether the term is a proof by rewriting + * + * A proof for a local rewriting step (= t s). + * The head function symbol of t is interpreted. + * + * This proof object has no antecedents. + * The conclusion of a rewrite rule is either an equality (= t s), + * an equivalence (iff t s), or equi-satisfiability (~ t s). + * Remark: if f is bool, then = is iff. + * + * Examples: + * (= (+ x 0) x) + * (= (+ x 1 2) (+ 3 x)) + * (iff (or x false) x) + * + **/ + public boolean IsProofRewrite() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } + + /** + * Indicates whether the term is a proof by rewriting + * + * A proof for rewriting an expression t into an expression s. + * This proof object is used if the parameter PROOF_MODE is 1. + * This proof object can have n antecedents. + * The antecedents are proofs for equalities used as substitution rules. + * The object is also used in a few cases if the parameter PROOF_MODE is 2. + * The cases are: + * - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) + * - When converting bit-vectors to Booleans (BIT2BOOL=true) + * - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) + * + **/ + public boolean IsProofRewriteStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } + + /** + * Indicates whether the term is a proof for pulling quantifiers out. + * + * A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. + * + **/ + public boolean IsProofPullQuant() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } + + /** + * Indicates whether the term is a proof for pulling quantifiers out. + * + * A proof for (iff P Q) where Q is in prenex normal form. + * This proof object is only used if the parameter PROOF_MODE is 1. + * This proof object has no antecedents + * + **/ + public boolean IsProofPullQuantStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } + + /** + * Indicates whether the term is a proof for pushing quantifiers in. + * + * A proof for: + * (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) + * (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) + * ... + * (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) + * This proof object has no antecedents + * + **/ + public boolean IsProofPushQuant() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } + + /** + * Indicates whether the term is a proof for elimination of unused variables. + * + * A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) + * (forall (x_1 ... x_n) p[x_1 ... x_n])) + * + * It is used to justify the elimination of unused variables. + * This proof object has no antecedents. + * + **/ + public boolean IsProofElimUnusedVars() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } + + /** + * Indicates whether the term is a proof for destructive equality resolution + * + * A proof for destructive equality resolution: + * (iff (forall (x) (or (not (= x t)) P[x])) P[t]) + * if x does not occur in t. + * + * This proof object has no antecedents. + * + * Several variables can be eliminated simultaneously. + * + **/ + public boolean IsProofDER() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } + + /** + * Indicates whether the term is a proof for quantifier instantiation + * + * A proof of (or (not (forall (x) (P x))) (P a)) + * + **/ + public boolean IsProofQuantInst() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } + + /** + * Indicates whether the term is a hypthesis marker. + * Mark a hypothesis in a natural deduction style proof. + **/ + public boolean IsProofHypothesis() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } + + /** + * Indicates whether the term is a proof by lemma + * + * T1: false + * [lemma T1]: (or (not l_1) ... (not l_n)) + * + * This proof object has one antecedent: a hypothetical proof for false. + * It converts the proof in a proof for (or (not l_1) ... (not l_n)), + * when T1 contains the hypotheses: l_1, ..., l_n. + * + **/ + public boolean IsProofLemma() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } + + /** + * Indicates whether the term is a proof by unit resolution + * + * T1: (or l_1 ... l_n l_1' ... l_m') + * T2: (not l_1) + * ... + * T(n+1): (not l_n) + * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + * + **/ + public boolean IsProofUnitResolution() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } + + /** + * Indicates whether the term is a proof by iff-true + * + * T1: p + * [iff-true T1]: (iff p true) + * + **/ + public boolean IsProofIFFTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } + + /** + * Indicates whether the term is a proof by iff-false + * + * T1: (not p) + * [iff-false T1]: (iff p false) + * + **/ + public boolean IsProofIFFFalse() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } + + /** + * Indicates whether the term is a proof by commutativity + * + * [comm]: (= (f a b) (f b a)) + * + * f is a commutative operator. + * + * This proof object has no antecedents. + * Remark: if f is bool, then = is iff. + * + **/ + public boolean IsProofCommutativity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } + + /** + * Indicates whether the term is a proof for Tseitin-like axioms + * + * Proof object used to justify Tseitin's like axioms: + * + * (or (not (and p q)) p) + * (or (not (and p q)) q) + * (or (not (and p q r)) p) + * (or (not (and p q r)) q) + * (or (not (and p q r)) r) + * ... + * (or (and p q) (not p) (not q)) + * (or (not (or p q)) p q) + * (or (or p q) (not p)) + * (or (or p q) (not q)) + * (or (not (iff p q)) (not p) q) + * (or (not (iff p q)) p (not q)) + * (or (iff p q) (not p) (not q)) + * (or (iff p q) p q) + * (or (not (ite a b c)) (not a) b) + * (or (not (ite a b c)) a c) + * (or (ite a b c) (not a) (not b)) + * (or (ite a b c) a (not c)) + * (or (not (not a)) (not a)) + * (or (not a) a) + * + * This proof object has no antecedents. + * Note: all axioms are propositional tautologies. + * Note also that 'and' and 'or' can take multiple arguments. + * You can recover the propositional tautologies by + * unfolding the Boolean connectives in the axioms a small + * bounded number of steps (=3). + * + **/ + public boolean IsProofDefAxiom() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } + + /** + * Indicates whether the term is a proof for introduction of a name + * + * Introduces a name for a formula/term. + * Suppose e is an expression with free variables x, and def-intro + * introduces the name n(x). The possible cases are: + * + * When e is of Boolean type: + * [def-intro]: (and (or n (not e)) (or (not n) e)) + * + * or: + * [def-intro]: (or (not n) e) + * when e only occurs positively. + * + * When e is of the form (ite cond th el): + * [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) + * + * Otherwise: + * [def-intro]: (= n e) + * + **/ + public boolean IsProofDefIntro() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } + + /** + * Indicates whether the term is a proof for application of a definition + * + * [apply-def T1]: F ~ n + * F is 'equivalent' to n, given that T1 is a proof that + * n is a name for F. + * + **/ + public boolean IsProofApplyDef() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } + + /** + * Indicates whether the term is a proof iff-oeq + * + * T1: (iff p q) + * [iff~ T1]: (~ p q) + * + **/ + public boolean IsProofIFFOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } + + /** + * Indicates whether the term is a proof for a positive NNF step + * + * Proof for a (positive) NNF step. Example: + * + * T1: (not s_1) ~ r_1 + * T2: (not s_2) ~ r_2 + * T3: s_1 ~ r_1' + * T4: s_2 ~ r_2' + * [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) + * (and (or r_1 r_2') (or r_1' r_2))) + * + * The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: + * (a) When creating the NNF of a positive force quantifier. + * The quantifier is retained (unless the bound variables are eliminated). + * Example + * T1: q ~ q_new + * [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) + * + * (b) When recursively creating NNF over Boolean formulas, where the top-level + * connective is changed during NNF conversion. The relevant Boolean connectives + * for NNF_POS are 'implies', 'iff', 'xor', 'ite'. + * NNF_NEG furthermore handles the case where negation is pushed + * over Boolean connectives 'and' and 'or'. + * + **/ + public boolean IsProofNNFPos() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } + + /** + * Indicates whether the term is a proof for a negative NNF step + * + * Proof for a (negative) NNF step. Examples: + * + * T1: (not s_1) ~ r_1 + * ... + * Tn: (not s_n) ~ r_n + * [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) + * and + * T1: (not s_1) ~ r_1 + * ... + * Tn: (not s_n) ~ r_n + * [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) + * and + * T1: (not s_1) ~ r_1 + * T2: (not s_2) ~ r_2 + * T3: s_1 ~ r_1' + * T4: s_2 ~ r_2' + * [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) + * (and (or r_1 r_2) (or r_1' r_2'))) + * + **/ + public boolean IsProofNNFNeg() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } + + /** + * Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. + * + * A proof for (~ P Q) where Q is in negation normal form. + * + * This proof object is only used if the parameter PROOF_MODE is 1. + * + * This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. + * + **/ + public boolean IsProofNNFStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } + + /** + * Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. + * + * A proof for (~ P Q) where Q is in conjunctive normal form. + * This proof object is only used if the parameter PROOF_MODE is 1. + * This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. + * + **/ + public boolean IsProofCNFStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } + + /** + * Indicates whether the term is a proof for a Skolemization step + * + * Proof for: + * + * [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) + * [sk]: (~ (exists x (p x y)) (p (sk y) y)) + * + * This proof object has no antecedents. + * + **/ + public boolean IsProofSkolemize() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } + + /** + * Indicates whether the term is a proof by modus ponens for equi-satisfiability. + * + * Modus ponens style rule for equi-satisfiability. + * T1: p + * T2: (~ p q) + * [mp~ T1 T2]: q + * + **/ + public boolean IsProofModusPonensOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } + + /** + * Indicates whether the term is a proof for theory lemma + * + * Generic proof for theory lemmas. + * + * The theory lemma function comes with one or more parameters. + * The first parameter indicates the name of the theory. + * For the theory of arithmetic, additional parameters provide hints for + * checking the theory lemma. + * The hints for arithmetic are: + * - farkas - followed by rational coefficients. Multiply the coefficients to the + * inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. + * - triangle-eq - Indicates a lemma related to the equivalence: + * (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) + * - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. + * + **/ + public boolean IsProofTheoryLemma() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } + + /** + * Indicates whether the term is of an array sort. + **/ + public boolean IsRelation() + { + return (Native.isApp(Context.nCtx, NativeObject) != 0 && + (Z3_sort_kind)Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_RELATION_SORT); + } /** * Indicates whether the term is an relation store @@ -237,53 +1228,188 @@ package com.Microsoft.Z3; * correspond to the n columns of the relation. * **/ - /* Overloaded operators are not translated. */ - } + public boolean IsRelationStore() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } + + /** + * Indicates whether the term is an empty relation + **/ + public boolean IsEmptyRelation() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } + + /** + * Indicates whether the term is a test for the emptiness of a relation + **/ + public boolean IsIsEmptyRelation() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } + + /** + * Indicates whether the term is a relational join + **/ + public boolean IsRelationalJoin() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } + + /** + * Indicates whether the term is the union or convex hull of two relations. + * The function takes two arguments. + **/ + public boolean IsRelationUnion() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } + + /** + * Indicates whether the term is the widening of two relations + * The function takes two arguments. + **/ + public boolean IsRelationWiden() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } + + /** + * Indicates whether the term is a projection of columns (provided as numbers in the parameters). + * The function takes one argument. + **/ + public boolean IsRelationProject() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } + + /** + * Indicates whether the term is a relation filter + * + * Filter (restrict) a relation with respect to a predicate. + * The first argument is a relation. + * The second argument is a predicate with free de-Brujin indices + * corresponding to the columns of the relation. + * So the first column in the relation has index 0. + * + **/ + public boolean IsRelationFilter() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } + + /** + * Indicates whether the term is an intersection of a relation with the negation of another. + * + * Intersect the first relation with respect to negation + * of the second relation (the function takes two arguments). + * Logically, the specification can be described by a function + * + * target = filter_by_negation(pos, neg, columns) + * + * where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that + * target are elements in x in pos, such that there is no y in neg that agrees with + * x on the columns c1, d1, .., cN, dN. + * + **/ + public boolean IsRelationNegationFilter() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } + + /** + * Indicates whether the term is the renaming of a column in a relation + * + * The function takes one argument. + * The parameters contain the renaming as a cycle. + * + **/ + public boolean IsRelationRename() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } + + /** + * Indicates whether the term is the complement of a relation + **/ + public boolean IsRelationComplement() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } + + /** + * Indicates whether the term is a relational select + * + * Check if a record is an element of the relation. + * The function takes n+1 arguments, where the first argument is a relation, + * and the remaining n arguments correspond to a record. + * + **/ + public boolean IsRelationSelect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } + + /** + * Indicates whether the term is a relational clone (copy) + * + * Create a fresh copy (clone) of a relation. + * The function is logically the identity, but + * in the context of a register machine allows + * for terms of kind + * to perform destructive updates to the first argument. + * + **/ + public boolean IsRelationClone() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } + + /** + * Indicates whether the term is of an array sort. + **/ + public boolean IsFiniteDomain() + { + return (Native.isApp(Context.nCtx, NativeObject) != 0 && + (Z3_sort_kind)Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); + } /** * Indicates whether the term is a less than predicate over a finite domain. **/ - /* Overloaded operators are not translated. */ - } + public boolean IsFiniteDomainLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } - /** Constructor for Expr + /** + * The de-Burijn index of a bound variable. + * + * Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain + * the meaning of de-Bruijn indices by indicating the compilation process from + * non-de-Bruijn formulas to de-Bruijn format. + * + * abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) + * abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) + * abs1(x, x, n) = b_n + * abs1(y, x, n) = y + * abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) + * abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) + * + * The last line is significant: the index of a bound variable is different depending + * on the scope in which it appears. The deeper x appears, the higher is its + * index. + * + **/ + public long Index() + { + if (!IsVar) + throw new Z3Exception("Term is not a bound variable."); + + + + return Native.getIndexValue(Context.nCtx, NativeObject); + } + + /** + * Constructor for Expr **/ protected Expr(Context ctx) { super(ctx); } - /** Constructor for Expr + /** + * Constructor for Expr **/ protected Expr(Context ctx, IntPtr obj) { super(ctx, obj); } void CheckNativeObject(IntPtr obj) { if (Native.isApp(Context.nCtx, obj) == 0 && - (Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3VARAST && - (Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3QUANTIFIERAST) + (Z3_ast_kind)Native.getAstKind(Context.nCtx, obj) != Z3_ast_kind.Z3_VAR_AST && + (Z3_ast_kind)Native.getAstKind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a term"); super.CheckNativeObject(obj); } - static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments) + static Expr Create(Context ctx, FuncDecl f, Expr[] arguments) { - IntPtr obj = Native.mkApp(ctx.nCtx, f.NativeObject, - AST.ArrayLength(arguments), + IntPtr obj = Native.mkApp(ctx.nCtx, f.NativeObject, + AST.ArrayLength(arguments), AST.ArrayToNative(arguments)); return Create(ctx, obj); - } + } - new static Expr Create(Context ctx, IntPtr obj) + static Expr Create(Context ctx, IntPtr obj) { - Z3AstKind k = (Z3AstKind)Native.getAstKind(ctx.nCtx, obj); - if (k == Z3AstKind.Z3QUANTIFIERAST) + Z3_ast_kind k = (Z3_ast_kind)Native.getAstKind(ctx.nCtx, obj); + if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) return new Quantifier(ctx, obj); IntPtr s = Native.getSort(ctx.nCtx, obj); - Z3SortKind sk = (Z3SortKind)Native.getSortKind(ctx.nCtx, s); + Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(ctx.nCtx, s); if (Native.isAlgebraicNumber(ctx.nCtx, obj) != 0) // is this a numeral ast? return new AlgebraicNum(ctx, obj); @@ -292,20 +1418,20 @@ package com.Microsoft.Z3; { switch (sk) { - case Z3SortKind.Z3INTSORT: return new IntNum(ctx, obj); - case Z3SortKind.Z3REALSORT: return new RatNum(ctx, obj); - case Z3SortKind.Z3BVSORT: return new BitVecNum(ctx, obj); + case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); + case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj); + case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); } } switch (sk) { - case Z3SortKind.Z3BOOLSORT: return new BoolExpr(ctx, obj); - case Z3SortKind.Z3INTSORT: return new IntExpr(ctx, obj); - case Z3SortKind.Z3REALSORT: return new RealExpr(ctx, obj); - case Z3SortKind.Z3BVSORT: return new BitVecExpr(ctx, obj); - case Z3SortKind.Z3ARRAYSORT: return new ArrayExpr(ctx, obj); - case Z3SortKind.Z3DATATYPESORT: return new DatatypeExpr(ctx, obj); + case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj); + case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj); + case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj); + case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj); + case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj); + case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); } return new Expr(ctx, obj); @@ -385,7 +1511,7 @@ package com.Microsoft.Z3; /** * The size of the sort of a bit-vector term. **/ - public Integer SortSize() { return ((BitVecSort)Sort).Size; } + public long SortSize() { return ((BitVecSort)Sort).Size; } /** Constructor for BitVecExpr **/ diff --git a/src/api/java/com/Microsoft/Z3/Fixedpoint.java b/src/api/java/com/Microsoft/Z3/Fixedpoint.java index 9d4f61c94..77ce576ac 100644 --- a/src/api/java/com/Microsoft/Z3/Fixedpoint.java +++ b/src/api/java/com/Microsoft/Z3/Fixedpoint.java @@ -19,7 +19,7 @@ package com.Microsoft.Z3; { return Native.fixedpointGetHelp(Context.nCtx, NativeObject); - } + } /** * Sets the fixedpoint solver parameters. @@ -29,7 +29,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(value); Native.fixedpointSetParams(Context.nCtx, NativeObject, value.NativeObject); - } + } /** * Retrieves parameter descriptions for Fixedpoint solver. @@ -77,13 +77,13 @@ package com.Microsoft.Z3; /** * Add table fact to the fixedpoint solver. **/ - public void AddFact(FuncDecl pred, Integer[] args) + public void AddFact(FuncDecl pred, long[] args) { Context.CheckContextMatch(pred); - Native.fixedpointAddFact(Context.nCtx, NativeObject, pred.NativeObject, (Integer)args.Length, args); + Native.fixedpointAddFact(Context.nCtx, NativeObject, pred.NativeObject, (long)args.Length, args); } /** @@ -97,11 +97,11 @@ package com.Microsoft.Z3; Context.CheckContextMatch(query); - Z3Lboolean r = (Z3Lboolean)Native.fixedpointQuery(Context.nCtx, NativeObject, query.NativeObject); + Z3_lboolean r = (Z3_lboolean)Native.fixedpointQuery(Context.nCtx, NativeObject, query.NativeObject); switch (r) { - case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE; - case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE; + case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -118,12 +118,12 @@ package com.Microsoft.Z3; Context.CheckContextMatch(relations); - Z3Lboolean r = (Z3Lboolean)Native.fixedpointQueryRelations(Context.nCtx, NativeObject, + Z3_lboolean r = (Z3_lboolean)Native.fixedpointQueryRelations(Context.nCtx, NativeObject, AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) { - case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE; - case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE; + case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -182,7 +182,7 @@ package com.Microsoft.Z3; /** * Retrieve the number of levels explored for a given predicate. **/ - public Integer GetNumLevels(FuncDecl predicate) + public long GetNumLevels(FuncDecl predicate) { return Native.fixedpointGetNumLevels(Context.nCtx, NativeObject, predicate.NativeObject); } @@ -238,30 +238,32 @@ package com.Microsoft.Z3; /** * Retrieve set of rules added to fixedpoint context. **/ - public BoolExpr[] Rules {() + public BoolExpr[] Rules() + { ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context.nCtx, NativeObject)); - Integer n = v.Size; + long n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new BoolExpr(Context, v[i].NativeObject); return res; - } + } /** * Retrieve set of assertions added to fixedpoint context. **/ - public BoolExpr[] Assertions {() + public BoolExpr[] Assertions() + { ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context.nCtx, NativeObject)); - Integer n = v.Size; + long n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new BoolExpr(Context, v[i].NativeObject); return res; - } + } Fixedpoint(Context ctx, IntPtr obj) @@ -288,13 +290,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.FixedpointDRQ.IncAndClear(Context, o); + Context.Fixedpoint_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.FixedpointDRQ.Add(o); + Context.Fixedpoint_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/FuncDecl.java b/src/api/java/com/Microsoft/Z3/FuncDecl.java index afd171813..ddedcf4ee 100644 --- a/src/api/java/com/Microsoft/Z3/FuncDecl.java +++ b/src/api/java/com/Microsoft/Z3/FuncDecl.java @@ -28,7 +28,7 @@ package com.Microsoft.Z3; **/ public boolean Equals(object o) { - FuncDecl casted = o as FuncDecl; + FuncDecl casted = (FuncDecl) o; if (casted == null) return false; return this == casted; } @@ -52,18 +52,18 @@ package com.Microsoft.Z3; /** * Returns a unique identifier for the function declaration. **/ - new public Integer Id() { return Native.getFuncDeclId(Context.nCtx, NativeObject); } + public long Id() { return Native.getFuncDeclId(Context.nCtx, NativeObject); } /** * The arity of the function declaration **/ - public Integer Arity() { return Native.getArity(Context.nCtx, NativeObject); } + public long Arity() { return Native.getArity(Context.nCtx, NativeObject); } /** * The size of the domain of the function declaration * **/ - public Integer DomainSize() { return Native.getDomainSize(Context.nCtx, NativeObject); } + public long DomainSize() { return Native.getDomainSize(Context.nCtx, NativeObject); } /** * The domain of the function declaration @@ -75,34 +75,38 @@ package com.Microsoft.Z3; var n = DomainSize; Sort[] res = new Sort[n]; - for (Integer i = 0; i < n; i++) + for (long 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() { + public Sort Range() + { - 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() { return (Z3DeclKind)Native.getDeclKind(Context.nCtx, NativeObject); } + public Z3_decl_kind DeclKind() { return (Z3_decl_kind)Native.getDeclKind(Context.nCtx, NativeObject); } /** * The name of the function declaration **/ - public Symbol Name() { + public Symbol Name() + { - 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 Integer NumParameters() { return Native.getDeclNumParameters(Context.nCtx, NativeObject); } + public long NumParameters() { return Native.getDeclNumParameters(Context.nCtx, NativeObject); } /** * The parameters of the function declaration @@ -111,37 +115,37 @@ package com.Microsoft.Z3; { - Integer num = NumParameters; + long num = NumParameters; Parameter[] res = new Parameter[num]; - for (Integer i = 0; i < num; i++) + for (long i = 0; i < num; i++) { - Z3ParameterKind k = (Z3ParameterKind)Native.getDeclParameterKind(Context.nCtx, NativeObject, i); + Z3_parameter_kind k = (Z3_parameter_kind)Native.getDeclParameterKind(Context.nCtx, NativeObject, i); switch (k) { - case Z3ParameterKind.Z3PARAMETERINT: + case Z3_parameter_kind.Z3_PARAMETER_INT: res[i] = new Parameter(k, Native.getDeclIntParameter(Context.nCtx, NativeObject, i)); break; - case Z3ParameterKind.Z3PARAMETERDOUBLE: + case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context.nCtx, NativeObject, i)); break; - case Z3ParameterKind.Z3PARAMETERSYMBOL: + case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context.nCtx, NativeObject, i))); break; - case Z3ParameterKind.Z3PARAMETERSORT: + case Z3_parameter_kind.Z3_PARAMETER_SORT: res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context.nCtx, NativeObject, i))); break; - case Z3ParameterKind.Z3PARAMETERAST: + case Z3_parameter_kind.Z3_PARAMETER_AST: res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context.nCtx, NativeObject, i))); break; - case Z3ParameterKind.Z3PARAMETERFUNCDECL: + case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context.nCtx, NativeObject, i))); break; - case Z3ParameterKind.Z3PARAMETERRATIONAL: + case Z3_parameter_kind.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; } } @@ -151,7 +155,7 @@ package com.Microsoft.Z3; **/ public class Parameter { - private Z3ParameterKind kind; + private Z3_parameter_kind kind; private int i; private double d; private Symbol sym; @@ -162,47 +166,76 @@ package com.Microsoft.Z3; /**The int value of the parameter. **/ - /* Overloaded operators are not translated. */ + public int Int () { 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 () { 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 () { 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 () { 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 () { 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 () { 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 () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; } - Parameter(Z3ParameterKind k, double d) + /** + * The kind of the parameter. + **/ + public Z3_parameter_kind ParameterKind() { return kind; } + + 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(Z3ParameterKind k, Symbol s) + Parameter(Z3_parameter_kind k, Symbol s) { this.kind = k; this.sym = s; } - Parameter(Z3ParameterKind k, Sort s) + Parameter(Z3_parameter_kind k, Sort s) { this.kind = k; this.srt = s; } - Parameter(Z3ParameterKind k, AST a) + Parameter(Z3_parameter_kind k, AST a) { this.kind = k; this.ast = a; } - Parameter(Z3ParameterKind k, FuncDecl fd) + Parameter(Z3_parameter_kind k, FuncDecl fd) { this.kind = k; this.fd = fd; } - Parameter(Z3ParameterKind k, String r) + Parameter(Z3_parameter_kind k, String r) { this.kind = k; this.r = r; } } - FuncDecl(Context ctx, IntPtr obj) { super(ctx, obj); - + FuncDecl(Context ctx, IntPtr obj) + { super(ctx, obj); + } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) @@ -212,7 +245,7 @@ package com.Microsoft.Z3; - } + } FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) : base(ctx, Native.mkFreshFuncDecl(ctx.nCtx, prefix, @@ -224,7 +257,7 @@ package com.Microsoft.Z3; void CheckNativeObject(IntPtr obj) { - if (Native.getAstKind(Context.nCtx, obj) != (Integer)Z3AstKind.Z3FUNCDECLAST) + if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_FUNC_DECL_AST) throw new Z3Exception("Underlying object is not a function declaration"); super.CheckNativeObject(obj); } @@ -234,12 +267,14 @@ package com.Microsoft.Z3; * * @return **/ - public Expr this[params() lic Expr this[params Expr[] args] - public Expr this[params() { + public Expr this[params() lic Expr this[params Expr[] args + { + public Expr this[params() + { - return Apply(args); - } + return Apply(args); + } /** * Create expression that applies function to arguments. diff --git a/src/api/java/com/Microsoft/Z3/FuncInterp.java b/src/api/java/com/Microsoft/Z3/FuncInterp.java index e6b5dd7f1..6aeb33759 100644 --- a/src/api/java/com/Microsoft/Z3/FuncInterp.java +++ b/src/api/java/com/Microsoft/Z3/FuncInterp.java @@ -24,11 +24,12 @@ package com.Microsoft.Z3; public Expr Value() { return Expr.Create(Context, Native.funcEntryGetValue(Context.nCtx, NativeObject)); } + } /** * The number of arguments of the entry. **/ - public Integer NumArgs() { return Native.funcEntryGetNumArgs(Context.nCtx, NativeObject); } + public long NumArgs() { return Native.funcEntryGetNumArgs(Context.nCtx, NativeObject); } /** * The arguments of the function entry. @@ -38,22 +39,22 @@ package com.Microsoft.Z3; - Integer n = NumArgs; + long n = NumArgs; Expr[] res = new Expr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context.nCtx, NativeObject, i)); return res; - } + } /** * A string representation of the function entry. **/ public String toString() { - Integer n = NumArgs; + long n = NumArgs; String res = "["; Expr[] args = Args; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res += args[i] + ", "; return res + Value + "]"; } @@ -75,13 +76,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.FuncEntryDRQ.IncAndClear(Context, o); + Context.FuncEntry_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.FuncEntryDRQ.Add(o); + Context.FuncEntry_DRQ.Add(o); super.DecRef(o); } }; @@ -89,7 +90,7 @@ package com.Microsoft.Z3; /** * The number of entries in the function interpretation. **/ - public Integer NumEntries() { return Native.funcInterpGetNumEntries(Context.nCtx, NativeObject); } + public long NumEntries() { return Native.funcInterpGetNumEntries(Context.nCtx, NativeObject); } /** * The entries in the function interpretation @@ -100,12 +101,12 @@ package com.Microsoft.Z3; Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, j => Contract.Result()[j] != null)); - Integer n = NumEntries; + long n = NumEntries; Entry[] res = new Entry[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new Entry(Context, Native.funcInterpGetEntry(Context.nCtx, NativeObject, i)); return res; - } + } /** * The (symbolic) `else' value of the function interpretation. @@ -114,11 +115,12 @@ package com.Microsoft.Z3; return Expr.Create(Context, Native.funcInterpGetElse(Context.nCtx, NativeObject)); } + } /** * The arity of the function interpretation **/ - public Integer Arity() { return Native.funcInterpGetArity(Context.nCtx, NativeObject); } + public long Arity() { return Native.funcInterpGetArity(Context.nCtx, NativeObject); } /** * A string representation of the function interpretation. @@ -129,10 +131,10 @@ package com.Microsoft.Z3; res += "["; for (Entry.Iterator e = Entries.iterator(); e.hasNext(); ) { - Integer n = e.NumArgs; + long n = e.NumArgs; if (n > 1) res += "["; Expr[] args = e.Args; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) { if (i != 0) res += ", "; res += args[i]; @@ -165,13 +167,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.FuncInterpDRQ.IncAndClear(Context, o); + Context.FuncInterp_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.FuncInterpDRQ.Add(o); + Context.FuncInterp_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Goal.java b/src/api/java/com/Microsoft/Z3/Goal.java index 0042d2bac..171b81d47 100644 --- a/src/api/java/com/Microsoft/Z3/Goal.java +++ b/src/api/java/com/Microsoft/Z3/Goal.java @@ -21,26 +21,26 @@ package com.Microsoft.Z3; * An over approximation is applied when the objective is to find a proof for a given goal. * **/ - public Z3_goal_prec Precision() { return (Z3GoalPrec)Native.goalPrecision(Context.nCtx, NativeObject); } + public Z3_goal_prec Precision() { return (Z3_goal_prec)Native.goalPrecision(Context.nCtx, NativeObject); } /** * Indicates whether the goal is precise. **/ - public boolean IsPrecise() { return Precision == Z3GoalPrec.Z3GOALPRECISE; } + public boolean IsPrecise() { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; } /** * Indicates whether the goal is an under-approximation. **/ - public boolean IsUnderApproximation() { return Precision == Z3GoalPrec.Z3GOALUNDER; } + public boolean IsUnderApproximation() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; } /** * Indicates whether the goal is an over-approximation. **/ - public boolean IsOverApproximation() { return Precision == Z3GoalPrec.Z3GOALOVER; } + public boolean IsOverApproximation() { 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 == Z3GoalPrec.Z3GOALUNDEROVER; } + public boolean IsGarbage() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; } /** * Adds the to the given goal. @@ -69,7 +69,7 @@ package com.Microsoft.Z3; * This tracks how many transformations were applied to it. * **/ - public Integer Depth() { return Native.goalDepth(Context.nCtx, NativeObject); } + public long Depth() { return Native.goalDepth(Context.nCtx, NativeObject); } /** * Erases all formulas from the given goal. @@ -82,7 +82,7 @@ package com.Microsoft.Z3; /** * The number of formulas in the goal. **/ - public Integer Size() { return Native.goalSize(Context.nCtx, NativeObject); } + public long Size() { return Native.goalSize(Context.nCtx, NativeObject); } /** * The formulas in the goal. @@ -91,17 +91,17 @@ package com.Microsoft.Z3; { - Integer n = Size; + long n = Size; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long 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 Integer NumExprs() { return Native.goalNumExprs(Context.nCtx, NativeObject); } + public long NumExprs() { return Native.goalNumExprs(Context.nCtx, NativeObject); } /** * Indicates whether the goal is empty, and it is precise or the product of an under approximation. @@ -169,13 +169,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.GoalDRQ.IncAndClear(Context, o); + Context.Goal_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.GoalDRQ.Add(o); + Context.Goal_DRQ.Add(o); super.DecRef(o); } diff --git a/src/api/java/com/Microsoft/Z3/Log.java b/src/api/java/com/Microsoft/Z3/Log.java index 28a9e015e..35ac0e022 100644 --- a/src/api/java/com/Microsoft/Z3/Log.java +++ b/src/api/java/com/Microsoft/Z3/Log.java @@ -15,7 +15,7 @@ package com.Microsoft.Z3; **/ public final class Log { - private boolean mIsOpen = false; + private boolean m_is_open = false; /** * Open an interaction log file. @@ -24,7 +24,7 @@ package com.Microsoft.Z3; **/ public boolean Open(String filename) { - mIsOpen = true; + m_is_open = true; return Native.openLog(filename) == 1; } @@ -33,7 +33,7 @@ package com.Microsoft.Z3; **/ public void Close() { - mIsOpen = false; + m_is_open = false; Native.closeLog(); } @@ -44,7 +44,7 @@ package com.Microsoft.Z3; { - if (!mIsOpen) + if (!m_is_open) throw new Z3Exception("Log cannot be closed."); Native.appendLog(s); } @@ -55,6 +55,6 @@ package com.Microsoft.Z3; **/ public boolean isOpen() { - return mIsOpen; + return m_is_open; } } diff --git a/src/api/java/com/Microsoft/Z3/Model.java b/src/api/java/com/Microsoft/Z3/Model.java index 467d5e566..edd774f56 100644 --- a/src/api/java/com/Microsoft/Z3/Model.java +++ b/src/api/java/com/Microsoft/Z3/Model.java @@ -35,7 +35,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(f); if (f.Arity != 0 || - Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)) == (Integer)Z3SortKind.Z3ARRAYSORT) + Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)) == (long)Z3_sort_kind.Z3_ARRAY_SORT) throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject); @@ -56,13 +56,13 @@ package com.Microsoft.Z3; Context.CheckContextMatch(f); - Z3SortKind sk = (Z3SortKind)Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)); + Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)); if (f.Arity == 0) { IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject); - if (sk == Z3SortKind.Z3ARRAYSORT) + if (sk == Z3_sort_kind.Z3_ARRAY_SORT) { if (n == IntPtr.Zero) return null; @@ -92,7 +92,7 @@ package com.Microsoft.Z3; /** * The number of constants that have an interpretation in the model. **/ - public Integer NumConsts() { return Native.modelGetNumConsts(Context.nCtx, NativeObject); } + public long NumConsts() { return Native.modelGetNumConsts(Context.nCtx, NativeObject); } /** * The function declarations of the constants in the model. @@ -101,17 +101,17 @@ package com.Microsoft.Z3; { - Integer n = NumConsts; + long n = NumConsts; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i)); return res; - } + } /** * The number of function interpretations in the model. **/ - public Integer NumFuncs() { return Native.modelGetNumFuncs(Context.nCtx, NativeObject); } + public long NumFuncs() { return Native.modelGetNumFuncs(Context.nCtx, NativeObject); } /** * The function declarations of the function interpretations in the model. @@ -120,12 +120,12 @@ package com.Microsoft.Z3; { - Integer n = NumFuncs; + long n = NumFuncs; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i)); return res; - } + } /** * All symbols that have an interpretation in the model. @@ -136,14 +136,14 @@ package com.Microsoft.Z3; var nFuncs = NumFuncs; var nConsts = NumConsts; - Integer n = nFuncs + nConsts; + long n = nFuncs + nConsts; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < nConsts; i++) + for (long i = 0; i < nConsts; i++) res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i)); - for (Integer i = 0; i < nFuncs; i++) + for (long i = 0; i < nFuncs; i++) res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i)); return res; - } + } /** * A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. @@ -196,7 +196,7 @@ package com.Microsoft.Z3; /** * The number of uninterpreted sorts that the model has an interpretation for. **/ - public Integer NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); } + public long NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); } /** * The uninterpreted sorts that the model has an interpretation for. @@ -212,12 +212,12 @@ package com.Microsoft.Z3; { - Integer n = NumSorts; + long n = NumSorts; Sort[] res = new Sort[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Sort.Create(Context, Native.modelGetSort(Context.nCtx, NativeObject, i)); return res; - } + } /** * The finite set of distinct values that represent the interpretation for sort . @@ -231,9 +231,9 @@ package com.Microsoft.Z3; ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context.nCtx, NativeObject, s.NativeObject)); - Integer n = nUniv.Size; + long n = nUniv.Size; Expr[] res = new Expr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Expr.Create(Context, nUniv[i].NativeObject); return res; } @@ -267,13 +267,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ModelDRQ.IncAndClear(Context, o); + Context.Model_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ModelDRQ.Add(o); + Context.Model_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Native.java b/src/api/java/com/Microsoft/Z3/Native.java index 564b5cb6f..31ca6f4bc 100644 --- a/src/api/java/com/Microsoft/Z3/Native.java +++ b/src/api/java/com/Microsoft/Z3/Native.java @@ -1,7 +1,10 @@ // Automatically generated file package com.Microsoft.Z3; public final class Native { - static { System.loadLibrary(""); } + public static class IntPtr { public int value; } + public static class LongPtr { public long value; } + public static class StringPtr { public String value; } + static { System.loadLibrary(""); } public static native long mkConfig(); public static native void delConfig(long a0); public static native void setParamValue(long a0, String a1, String a2); @@ -487,8 +490,8 @@ public final class Native { public static native String statisticsToString(long a0); public static native long getContextAssignment(long a0); public static void main(String[] args) { - Integer major = 0, minor = 0, build = 0, revision = 0; + IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr(); getVersion(major, minor, build, revision); - System.out.format("Z3 (for Java) %d.%d.%d%n", major, minor, build); + System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value); } } diff --git a/src/api/java/com/Microsoft/Z3/Numeral.java b/src/api/java/com/Microsoft/Z3/Numeral.java index 5f9291b51..d0ed20dc9 100644 --- a/src/api/java/com/Microsoft/Z3/Numeral.java +++ b/src/api/java/com/Microsoft/Z3/Numeral.java @@ -25,10 +25,10 @@ package com.Microsoft.Z3; public UInt64 UInt64() { UInt64 res = 0; - if (Native.getNumeralInteger64(Context.nCtx, NativeObject, res) == 0) + if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; - } + } /** * Retrieve the int value. @@ -39,7 +39,7 @@ package com.Microsoft.Z3; if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not an int"); return res; - } + } /** * Retrieve the 64-bit int value. @@ -50,18 +50,18 @@ package com.Microsoft.Z3; if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; - } + } /** * Retrieve the int value. **/ - public Integer UInt() + public long UInt() { - Integer res = 0; - if (Native.getNumeralInteger(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a Integer"); + long res = 0; + if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0) + throw new Z3Exception("Numeral is not a long"); return res; - } + } /** * Retrieve the BigInteger value. @@ -69,7 +69,7 @@ package com.Microsoft.Z3; public BigInteger BigInteger() { return BigInteger.Parse(this.toString()); - } + } /** * Returns a string representation of the numeral. @@ -92,6 +92,7 @@ package com.Microsoft.Z3; return new IntNum(Context, Native.getNumerator(Context.nCtx, NativeObject)); } + } /** * The denominator of a rational numeral. @@ -100,6 +101,7 @@ package com.Microsoft.Z3; return new IntNum(Context, Native.getDenominator(Context.nCtx, NativeObject)); } + } /** * Converts the numerator of the rational to a BigInteger @@ -108,7 +110,7 @@ package com.Microsoft.Z3; { IntNum n = Numerator; return BigInteger.Parse(n.toString()); - } + } /** * Converts the denominator of the rational to a BigInteger @@ -117,13 +119,13 @@ package com.Microsoft.Z3; { IntNum n = Denominator; return BigInteger.Parse(n.toString()); - } + } /** * Returns a string representation in decimal notation. * The result has at most decimal places. **/ - public String ToDecimalString(Integer precision) + public String ToDecimalString(long precision) { return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision); } @@ -154,10 +156,10 @@ package com.Microsoft.Z3; public UInt64 UInt64() { UInt64 res = 0; - if (Native.getNumeralInteger64(Context.nCtx, NativeObject, res) == 0) + if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; - } + } /** * Retrieve the int value. @@ -168,7 +170,7 @@ package com.Microsoft.Z3; if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not an int"); return res; - } + } /** * Retrieve the 64-bit int value. @@ -179,18 +181,18 @@ package com.Microsoft.Z3; if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; - } + } /** * Retrieve the int value. **/ - public Integer UInt() + public long UInt() { - Integer res = 0; - if (Native.getNumeralInteger(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a Integer"); + long res = 0; + if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0) + throw new Z3Exception("Numeral is not a long"); return res; - } + } /** * Retrieve the BigInteger value. @@ -198,7 +200,7 @@ package com.Microsoft.Z3; public BigInteger BigInteger() { return BigInteger.Parse(this.toString()); - } + } /** * Returns a string representation of the numeral. @@ -223,7 +225,7 @@ package com.Microsoft.Z3; * the precision of the result * @return A numeral Expr of sort Real **/ - public RatNum ToUpper(Integer precision) + public RatNum ToUpper(long precision) { @@ -237,7 +239,7 @@ package com.Microsoft.Z3; * * @return A numeral Expr of sort Real **/ - public RatNum ToLower(Integer precision) + public RatNum ToLower(long precision) { @@ -248,7 +250,7 @@ package com.Microsoft.Z3; * Returns a string representation in decimal notation. * The result has at most decimal places. **/ - public String ToDecimal(Integer precision) + public String ToDecimal(long precision) { diff --git a/src/api/java/com/Microsoft/Z3/ParamDescrs.java b/src/api/java/com/Microsoft/Z3/ParamDescrs.java index c4e9d4be4..abade80b2 100644 --- a/src/api/java/com/Microsoft/Z3/ParamDescrs.java +++ b/src/api/java/com/Microsoft/Z3/ParamDescrs.java @@ -23,10 +23,10 @@ package com.Microsoft.Z3; /** * Retrieve kind of parameter. **/ - public Z3ParamKind GetKind(Symbol name) + public Z3_param_kind GetKind(Symbol name) { - return (Z3ParamKind)Native.paramDescrsGetKind(Context.nCtx, NativeObject, name.NativeObject); + return (Z3_param_kind)Native.paramDescrsGetKind(Context.nCtx, NativeObject, name.NativeObject); } /** @@ -34,18 +34,18 @@ package com.Microsoft.Z3; **/ public Symbol[] Names() { - Integer sz = Native.paramDescrsSize(Context.nCtx, NativeObject); + long sz = Native.paramDescrsSize(Context.nCtx, NativeObject); Symbol[] names = new Symbol[sz]; - for (Integer i = 0; i < sz; ++i) { + for (long i = 0; i < sz; ++i) { names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context.nCtx, NativeObject, i)); + } return names; - } } /** * The size of the ParamDescrs. **/ - public Integer Size() { return Native.paramDescrsSize(Context.nCtx, NativeObject); } + public long Size() { return Native.paramDescrsSize(Context.nCtx, NativeObject); } /** * Retrieves a string representation of the ParamDescrs. @@ -75,13 +75,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ParamDescrsDRQ.IncAndClear(Context, o); + Context.ParamDescrs_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ParamDescrsDRQ.Add(o); + Context.ParamDescrs_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Params.java b/src/api/java/com/Microsoft/Z3/Params.java index 0dd320778..040b6d67d 100644 --- a/src/api/java/com/Microsoft/Z3/Params.java +++ b/src/api/java/com/Microsoft/Z3/Params.java @@ -24,11 +24,11 @@ package com.Microsoft.Z3; /** * Adds a parameter setting. **/ - public void Add(Symbol name, Integer value) + public void Add(Symbol name, long value) { - Native.paramsSetInteger(Context.nCtx, NativeObject, name.NativeObject, value); + Native.paramsSetLong(Context.nCtx, NativeObject, name.NativeObject, value); } /** @@ -63,9 +63,9 @@ package com.Microsoft.Z3; /** * Adds a parameter setting. **/ - public void Add(String name, Integer value) + public void Add(String name, long value) { - Native.paramsSetInteger(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value); + Native.paramsSetLong(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value); } /** @@ -114,13 +114,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ParamsDRQ.IncAndClear(Context, o); + Context.Params_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ParamsDRQ.Add(o); + Context.Params_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Pattern.java b/src/api/java/com/Microsoft/Z3/Pattern.java index 6bd1ef811..edc772dcf 100644 --- a/src/api/java/com/Microsoft/Z3/Pattern.java +++ b/src/api/java/com/Microsoft/Z3/Pattern.java @@ -17,7 +17,7 @@ package com.Microsoft.Z3; /** * The number of terms in the pattern. **/ - public Integer NumTerms() { return Native.getPatternNumTerms(Context.nCtx, NativeObject); } + public long NumTerms() { return Native.getPatternNumTerms(Context.nCtx, NativeObject); } /** * The terms in the pattern. @@ -26,12 +26,12 @@ package com.Microsoft.Z3; { - Integer n = NumTerms; + long n = NumTerms; Expr[] res = new Expr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Expr.Create(Context, Native.getPattern(Context.nCtx, NativeObject, i)); return res; - } + } /** * A string representation of the pattern. diff --git a/src/api/java/com/Microsoft/Z3/Probe.java b/src/api/java/com/Microsoft/Z3/Probe.java index c651edb86..36f949966 100644 --- a/src/api/java/com/Microsoft/Z3/Probe.java +++ b/src/api/java/com/Microsoft/Z3/Probe.java @@ -60,13 +60,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.ProbeDRQ.IncAndClear(Context, o); + Context.Probe_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.ProbeDRQ.Add(o); + Context.Probe_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Quantifier.java b/src/api/java/com/Microsoft/Z3/Quantifier.java index 1a279aff0..6c7c91be7 100644 --- a/src/api/java/com/Microsoft/Z3/Quantifier.java +++ b/src/api/java/com/Microsoft/Z3/Quantifier.java @@ -24,12 +24,12 @@ package com.Microsoft.Z3; /** * The weight of the quantifier. **/ - public Integer Weight() { return Native.getQuantifierWeight(Context.nCtx, NativeObject); } + public long Weight() { return Native.getQuantifierWeight(Context.nCtx, NativeObject); } /** * The number of patterns. **/ - public Integer NumPatterns() { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); } + public long NumPatterns() { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); } /** * The patterns. @@ -38,17 +38,17 @@ package com.Microsoft.Z3; { - Integer n = NumPatterns; + long n = NumPatterns; Pattern[] res = new Pattern[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context.nCtx, NativeObject, i)); return res; - } + } /** * The number of no-patterns. **/ - public Integer NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context.nCtx, NativeObject); } + public long NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context.nCtx, NativeObject); } /** * The no-patterns. @@ -57,17 +57,17 @@ package com.Microsoft.Z3; { - Integer n = NumNoPatterns; + long n = NumNoPatterns; Pattern[] res = new Pattern[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context.nCtx, NativeObject, i)); return res; - } + } /** * The number of bound variables. **/ - public Integer NumBound() { return Native.getQuantifierNumBound(Context.nCtx, NativeObject); } + public long NumBound() { return Native.getQuantifierNumBound(Context.nCtx, NativeObject); } /** * The symbols for the bound variables. @@ -76,12 +76,12 @@ package com.Microsoft.Z3; { - Integer n = NumBound; + long n = NumBound; Symbol[] res = new Symbol[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context.nCtx, NativeObject, i)); return res; - } + } /** * The sorts of the bound variables. @@ -90,12 +90,12 @@ package com.Microsoft.Z3; { - Integer n = NumBound; + long n = NumBound; Sort[] res = new Sort[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context.nCtx, NativeObject, i)); return res; - } + } /** * The body of the quantifier. @@ -104,9 +104,10 @@ package com.Microsoft.Z3; return new BoolExpr(Context, Native.getQuantifierBody(Context.nCtx, NativeObject)); } + } Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, - Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, + long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null ) { super(ctx); @@ -129,7 +130,7 @@ package com.Microsoft.Z3; if (sorts.Length != names.Length) throw new Z3Exception("Number of sorts does not match number of names"); - IntPtr[] Patterns = AST.ArrayToNative(patterns); + IntPtr[] _patterns = AST.ArrayToNative(patterns); if (noPatterns == null && quantifierID == null && skolemID == null) { @@ -138,7 +139,6 @@ package com.Microsoft.Z3; AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), body.NativeObject); - } else { NativeObject = Native.mkQuantifierEx(ctx.nCtx, (isForall) ? 1 : 0, weight, @@ -152,7 +152,7 @@ package com.Microsoft.Z3; } Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, - Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, + long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null ) { super(ctx); @@ -191,7 +191,7 @@ package com.Microsoft.Z3; void CheckNativeObject(IntPtr obj) { - if ((Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3QUANTIFIERAST) + if ((Z3_ast_kind)Native.getAstKind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a quantifier"); super.CheckNativeObject(obj); } diff --git a/src/api/java/com/Microsoft/Z3/Solver.java b/src/api/java/com/Microsoft/Z3/Solver.java index a28687722..787e115ab 100644 --- a/src/api/java/com/Microsoft/Z3/Solver.java +++ b/src/api/java/com/Microsoft/Z3/Solver.java @@ -19,7 +19,7 @@ package com.Microsoft.Z3; return Native.solverGetHelp(Context.nCtx, NativeObject); - } + } /** * Sets the solver parameters. @@ -30,7 +30,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(value); Native.solverSetParams(Context.nCtx, NativeObject, value.NativeObject); - } + } /** * Retrieves parameter descriptions for solver. @@ -43,7 +43,7 @@ package com.Microsoft.Z3; * * **/ - public Integer NumScopes() { return Native.solverGetNumScopes(Context.nCtx, NativeObject); } + public long NumScopes() { return Native.solverGetNumScopes(Context.nCtx, NativeObject); } /** * Creates a backtracking point. @@ -59,7 +59,7 @@ package com.Microsoft.Z3; * Note that an exception is thrown if is not smaller than NumScopes * **/ - public void Pop(Integer n) + public void Pop(long n) { Native.solverPop(Context.nCtx, NativeObject, n); } @@ -91,11 +91,11 @@ package com.Microsoft.Z3; /** * The number of assertions in the solver. **/ - public Integer NumAssertions() + public long NumAssertions() { ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject)); return ass.Size; - } + } /** * The set of asserted formulas. @@ -105,12 +105,12 @@ package com.Microsoft.Z3; ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject)); - Integer n = ass.Size; + long n = ass.Size; BoolExpr[] res = new BoolExpr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new BoolExpr(Context, ass[i].NativeObject); return res; - } + } /** * Checks whether the assertions in the solver are consistent or not. @@ -122,15 +122,15 @@ package com.Microsoft.Z3; **/ public Status Check(Expr[] assumptions) { - Z3Lboolean r; + Z3_lboolean r; if (assumptions == null) - r = (Z3Lboolean)Native.solverCheck(Context.nCtx, NativeObject); + r = (Z3_lboolean)Native.solverCheck(Context.nCtx, NativeObject); else - r = (Z3Lboolean)Native.solverCheckAssumptions(Context.nCtx, NativeObject, (Integer)assumptions.Length, AST.ArrayToNative(assumptions)); + r = (Z3_lboolean)Native.solverCheckAssumptions(Context.nCtx, NativeObject, (long)assumptions.Length, AST.ArrayToNative(assumptions)); switch (r) { - case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE; - case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE; + case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -149,7 +149,7 @@ package com.Microsoft.Z3; return null; else return new Model(Context, x); - } + } /** * The proof of the last Check. @@ -165,7 +165,7 @@ package com.Microsoft.Z3; return null; else return Expr.Create(Context, x); - } + } /** * The unsat core of the last Check. @@ -180,12 +180,12 @@ package com.Microsoft.Z3; ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context.nCtx, NativeObject)); - Integer n = core.Size; + long n = core.Size; Expr[] res = new Expr[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Expr.Create(Context, core[i].NativeObject); return res; - } + } /** * A brief justification of why the last call to Check returned UNKNOWN. @@ -195,7 +195,7 @@ package com.Microsoft.Z3; return Native.solverGetReasonUnknown(Context.nCtx, NativeObject); - } + } /** * Solver statistics. @@ -205,7 +205,7 @@ package com.Microsoft.Z3; return new Statistics(Context, Native.solverGetStatistics(Context.nCtx, NativeObject)); - } + } /** * A string representation of the solver. @@ -235,13 +235,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.SolverDRQ.IncAndClear(Context, o); + Context.Solver_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.SolverDRQ.Add(o); + Context.Solver_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Sort.java b/src/api/java/com/Microsoft/Z3/Sort.java index f75624f1a..8e4735389 100644 --- a/src/api/java/com/Microsoft/Z3/Sort.java +++ b/src/api/java/com/Microsoft/Z3/Sort.java @@ -53,12 +53,12 @@ package com.Microsoft.Z3; /** * Returns a unique identifier for the sort. **/ - new public Integer Id() { return Native.getSortId(Context.nCtx, NativeObject); } + public long Id() { return Native.getSortId(Context.nCtx, NativeObject); } /** * The kind of the sort. **/ - public Z3_sort_kind SortKind() { return (Z3SortKind)Native.getSortKind(Context.nCtx, NativeObject); } + public Z3_sort_kind SortKind() { return (Z3_sort_kind)Native.getSortKind(Context.nCtx, NativeObject); } /** * The name of the sort @@ -66,6 +66,7 @@ package com.Microsoft.Z3; public Symbol Name() { return Symbol.Create(Context, Native.getSortName(Context.nCtx, NativeObject)); } + } /** * A string representation of the sort. @@ -73,7 +74,6 @@ package com.Microsoft.Z3; public String toString() { return Native.sorttoString(Context.nCtx, NativeObject); - } /** * Sort constructor @@ -83,27 +83,27 @@ package com.Microsoft.Z3; void CheckNativeObject(IntPtr obj) { - if (Native.getAstKind(Context.nCtx, obj) != (Integer)Z3AstKind.Z3SORTAST) + if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_SORT_AST) throw new Z3Exception("Underlying object is not a sort"); super.CheckNativeObject(obj); } - new static Sort Create(Context ctx, IntPtr obj) + static Sort Create(Context ctx, IntPtr obj) { - switch ((Z3SortKind)Native.getSortKind(ctx.nCtx, obj)) + switch ((Z3_sort_kind)Native.getSortKind(ctx.nCtx, obj)) { - case Z3SortKind.Z3ARRAYSORT: return new ArraySort(ctx, obj); - case Z3SortKind.Z3BOOLSORT: return new BoolSort(ctx, obj); - case Z3SortKind.Z3BVSORT: return new BitVecSort(ctx, obj); - case Z3SortKind.Z3DATATYPESORT: return new DatatypeSort(ctx, obj); - case Z3SortKind.Z3INTSORT: return new IntSort(ctx, obj); - case Z3SortKind.Z3REALSORT: return new RealSort(ctx, obj); - case Z3SortKind.Z3UNINTERPRETEDSORT: return new UninterpretedSort(ctx, obj); - case Z3SortKind.Z3FINITEDOMAINSORT: return new FiniteDomainSort(ctx, obj); - case Z3SortKind.Z3RELATIONSORT: return new RelationSort(ctx, obj); + case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj); + case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj); + case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj); + case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj); + case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj); + case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj); + case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj); + case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj); + case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } @@ -165,10 +165,10 @@ package com.Microsoft.Z3; /** * The size of the bit-vector sort. **/ - public Integer Size() { return Native.getBvSortSize(Context.nCtx, NativeObject); } + public long Size() { return Native.getBvSortSize(Context.nCtx, NativeObject); } BitVecSort(Context ctx, IntPtr obj) { super(ctx, obj); } - BitVecSort(Context ctx, Integer size) { super(ctx, Native.mkBvSort(ctx.nCtx, size)); } + BitVecSort(Context ctx, long size) { super(ctx, Native.mkBvSort(ctx.nCtx, size)); } }; /** @@ -183,6 +183,7 @@ package com.Microsoft.Z3; return Sort.Create(Context, Native.getArraySortDomain(Context.nCtx, NativeObject)); } + } /** * The range of the array sort. @@ -191,6 +192,7 @@ package com.Microsoft.Z3; return Sort.Create(Context, Native.getArraySortRange(Context.nCtx, NativeObject)); } + } ArraySort(Context ctx, IntPtr obj) { super(ctx, obj); } ArraySort(Context ctx, Sort domain, Sort range) @@ -198,7 +200,6 @@ package com.Microsoft.Z3; - } }; /** @@ -209,7 +210,7 @@ package com.Microsoft.Z3; /** * The number of constructors of the datatype sort. **/ - public Integer NumConstructors() { return Native.getDatatypeSortNumConstructors(Context.nCtx, NativeObject); } + public long NumConstructors() { return Native.getDatatypeSortNumConstructors(Context.nCtx, NativeObject); } /** * The constructors. @@ -218,12 +219,12 @@ package com.Microsoft.Z3; { - Integer n = NumConstructors; + long n = NumConstructors; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i)); return res; - } + } /** * The recognizers. @@ -232,12 +233,12 @@ package com.Microsoft.Z3; { - Integer n = NumConstructors; + long n = NumConstructors; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context.nCtx, NativeObject, i)); return res; - } + } /** * The constructor accessors. @@ -246,24 +247,24 @@ package com.Microsoft.Z3; { - Integer n = NumConstructors; + long n = NumConstructors; FuncDecl[][] res = new FuncDecl[n][]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) { FuncDecl fd = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i)); - Integer ds = fd.DomainSize; + long ds = fd.DomainSize; FuncDecl[] tmp = new FuncDecl[ds]; - for (Integer j = 0; j < ds; j++) + for (long j = 0; j < ds; j++) tmp[j] = new FuncDecl(Context, Native.getDatatypeSortConstructorAccessor(Context.nCtx, NativeObject, i, j)); res[i] = tmp; + } return res; - } } DatatypeSort(Context ctx, IntPtr obj) { super(ctx, obj); } DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) - { super(ctx, Native.mkDatatype(ctx.nCtx, name.NativeObject, (Integer)constructors.Length, ArrayToNative(constructors))); + { super(ctx, Native.mkDatatype(ctx.nCtx, name.NativeObject, (long)constructors.Length, ArrayToNative(constructors))); @@ -298,11 +299,12 @@ package com.Microsoft.Z3; return new FuncDecl(Context, Native.getTupleSortMkDecl(Context.nCtx, NativeObject)); } + } /** * The number of fields in the tuple. **/ - public Integer NumFields() { return Native.getTupleSortNumFields(Context.nCtx, NativeObject); } + public long NumFields() { return Native.getTupleSortNumFields(Context.nCtx, NativeObject); } /** * The field declarations. @@ -311,14 +313,14 @@ package com.Microsoft.Z3; { - Integer n = NumFields; + long n = NumFields; FuncDecl[] res = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = new FuncDecl(Context, Native.getTupleSortFieldDecl(Context.nCtx, NativeObject, i)); return res; - } + } - TupleSort(Context ctx, Symbol name, Integer numFields, Symbol[] fieldNames, Sort[] fieldSorts) + TupleSort(Context ctx, Symbol name, long numFields, Symbol[] fieldNames, Sort[] fieldSorts) { super(ctx); @@ -341,7 +343,8 @@ package com.Microsoft.Z3; public FuncDecl[] ConstDecls() { - return Constdecls; } + return _constdecls; } + } /** * The constants in the enumeration. @@ -349,7 +352,8 @@ package com.Microsoft.Z3; public Expr[] Consts() { - return Consts; } + return _consts; } + } /** * The test predicates for the constants in the enumeration. @@ -357,8 +361,8 @@ package com.Microsoft.Z3; public FuncDecl[] TesterDecls() { - return Testerdecls; - } + return _testerdecls; + } private void ObjectInvariant() @@ -370,8 +374,8 @@ package com.Microsoft.Z3; - private FuncDecl[] Constdecls = null, Testerdecls = null; - private Expr[] Consts = null; + private FuncDecl[] _constdecls = null, _testerdecls = null; + private Expr[] _consts = null; EnumSort(Context ctx, Symbol name, Symbol[] enumNames) { super(ctx); @@ -380,19 +384,19 @@ package com.Microsoft.Z3; int n = enumNames.Length; - IntPtr[] nConstdecls = new IntPtr[n]; - IntPtr[] nTesters = new IntPtr[n]; - NativeObject = Native.mkEnumerationSort(ctx.nCtx, name.NativeObject, (Integer)n, - Symbol.ArrayToNative(enumNames), nConstdecls, nTesters); - Constdecls = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) - Constdecls[i] = new FuncDecl(ctx, nConstdecls[i]); - Testerdecls = new FuncDecl[n]; - for (Integer i = 0; i < n; i++) - Testerdecls[i] = new FuncDecl(ctx, nTesters[i]); - Consts = new Expr[n]; - for (Integer i = 0; i < n; i++) - Consts[i] = ctx.MkApp(Constdecls[i]); + IntPtr[] n_constdecls = new IntPtr[n]; + IntPtr[] n_testers = new IntPtr[n]; + NativeObject = Native.mkEnumerationSort(ctx.nCtx, name.NativeObject, (long)n, + Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); + _constdecls = new FuncDecl[n]; + for (long i = 0; i < n; i++) + _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); + _testerdecls = new FuncDecl[n]; + for (long i = 0; i < n; i++) + _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); + _consts = new Expr[n]; + for (long i = 0; i < n; i++) + _consts[i] = ctx.MkApp(_constdecls[i]); } }; @@ -415,7 +419,7 @@ package com.Microsoft.Z3; { return nilConst; - } + } /** * The declaration of the isNil function of this list sort. @@ -424,7 +428,7 @@ package com.Microsoft.Z3; { return isNilDecl; - } + } /** * The declaration of the cons function of this list sort. @@ -433,7 +437,7 @@ package com.Microsoft.Z3; { return consDecl; - } + } /** * The declaration of the isCons function of this list sort. @@ -443,7 +447,7 @@ package com.Microsoft.Z3; { return isConsDecl; - } + } /** * The declaration of the head function of this list sort. @@ -452,7 +456,7 @@ package com.Microsoft.Z3; { return headDecl; - } + } /** * The declaration of the tail function of this list sort. @@ -461,7 +465,7 @@ package com.Microsoft.Z3; { return tailDecl; - } + } private void ObjectInvariant() @@ -513,7 +517,7 @@ package com.Microsoft.Z3; /** * The arity of the relation sort. **/ - public Integer Arity() { return Native.getRelationArity(Context.nCtx, NativeObject); } + public long Arity() { return Native.getRelationArity(Context.nCtx, NativeObject); } /** * The sorts of the columns of the relation sort. @@ -522,17 +526,17 @@ package com.Microsoft.Z3; { - if (mColumnSorts != null) - return mColumnSorts; + if (m_columnSorts != null) + return m_columnSorts; - Integer n = Arity; + long n = Arity; Sort[] res = new Sort[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Sort.Create(Context, Native.getRelationColumn(Context.nCtx, NativeObject, i)); return res; - } + } - private Sort[] mColumnSorts = null; + private Sort[] m_columnSorts = null; RelationSort(Context ctx, IntPtr obj) { super(ctx, obj); diff --git a/src/api/java/com/Microsoft/Z3/Statistics.java b/src/api/java/com/Microsoft/Z3/Statistics.java index 0e509a5d9..d9aac9d67 100644 --- a/src/api/java/com/Microsoft/Z3/Statistics.java +++ b/src/api/java/com/Microsoft/Z3/Statistics.java @@ -23,19 +23,19 @@ package com.Microsoft.Z3; /** * The uint-value of the entry. **/ - public Integer UIntValue() { return mInteger; } + public long UIntValue() { return m_long; } /** * The double-value of the entry. **/ - public double DoubleValue() { return mDouble; } + public double DoubleValue() { return m_double; } /** * True if the entry is uint-valued. **/ - public boolean IsUInt() { return mIsInteger; } + public boolean IsUInt() { return m_is_long; } /** * True if the entry is double-valued. **/ - public boolean IsDouble() { return mIsDouble; } + public boolean IsDouble() { return m_is_double; } /** * The string representation of the the entry's value. @@ -45,12 +45,12 @@ package com.Microsoft.Z3; if (IsUInt) - return mInteger.toString(); + return m_long.toString(); else if (IsDouble) - return mDouble.toString(); + return m_double.toString(); else throw new Z3Exception("Unknown statistical entry type"); - } + } /** * The string representation of the Entry. @@ -60,12 +60,12 @@ package com.Microsoft.Z3; return Key + ": " + Value; } - private boolean mIsInteger = false; - private boolean mIsDouble = false; - private Integer mInteger = 0; - private double mDouble = 0.0; - Entry(String k, Integer v) { Key = k; mIsInteger = true; mInteger = v; } - Entry(String k, double v) { Key = k; mIsDouble = true; mDouble = v; } + private boolean m_is_long = false; + private boolean m_is_double = false; + private long m_long = 0; + private double m_double = 0.0; + Entry(String k, long v) { Key = k; m_is_long = true; m_long = v; } + Entry(String k, double v) { Key = k; m_is_double = true; m_double = v; } } /** @@ -79,7 +79,7 @@ package com.Microsoft.Z3; /** * The number of statistical data. **/ - public Integer Size() { return Native.statsSize(Context.nCtx, NativeObject); } + public long Size() { return Native.statsSize(Context.nCtx, NativeObject); } /** * The data entries. @@ -90,21 +90,21 @@ package com.Microsoft.Z3; - Integer n = Size; + long n = Size; Entry[] res = new Entry[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) { Entry e; String k = Native.statsGetKey(Context.nCtx, NativeObject, i); - if (Native.statsIsInteger(Context.nCtx, NativeObject, i) != 0) - e = new Entry(k, Native.statsGetIntegerValue(Context.nCtx, NativeObject, i)); + if (Native.statsIsLong(Context.nCtx, NativeObject, i) != 0) + e = new Entry(k, Native.statsGetLongValue(Context.nCtx, NativeObject, i)); else if (Native.statsIsDouble(Context.nCtx, NativeObject, i) != 0) e = new Entry(k, Native.statsGetDoubleValue(Context.nCtx, NativeObject, i)); else throw new Z3Exception("Unknown data entry value"); res[i] = e; + } return res; - } } /** @@ -114,26 +114,26 @@ package com.Microsoft.Z3; { - Integer n = Size; + long n = Size; String[] res = new String[n]; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) res[i] = Native.statsGetKey(Context.nCtx, NativeObject, i); return res; - } + } /** * The value of a particular statistical counter. * Returns null if the key is unknown. **/ - public Entry this[String key]() + public Entry get(String key) { - Integer n = Size; + long n = Size; Entry[] es = Entries; - for (Integer i = 0; i < n; i++) + for (long i = 0; i < n; i++) if (es[i].Key == key) return es[i]; return null; - } + } Statistics(Context ctx, IntPtr obj) { super(ctx, obj); @@ -155,13 +155,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.StatisticsDRQ.IncAndClear(Context, o); + Context.Statistics_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.StatisticsDRQ.Add(o); + Context.Statistics_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Symbol.java b/src/api/java/com/Microsoft/Z3/Symbol.java index 0023bc670..972999e66 100644 --- a/src/api/java/com/Microsoft/Z3/Symbol.java +++ b/src/api/java/com/Microsoft/Z3/Symbol.java @@ -15,9 +15,9 @@ package com.Microsoft.Z3; /** * The kind of the symbol (int or string) **/ - protected Z3SymbolKind Kind + protected Z3_symbol_kind Kind { - get { return (Z3SymbolKind)Native.getSymbolKind(Context.nCtx, NativeObject); } + get { return (Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, NativeObject); } } /** @@ -25,7 +25,7 @@ package com.Microsoft.Z3; **/ public boolean IsIntSymbol() { - return Kind == Z3SymbolKind.Z3INTSYMBOL; + return Kind == Z3_symbol_kind.Z3_INT_SYMBOL; } /** @@ -33,7 +33,7 @@ package com.Microsoft.Z3; **/ public boolean IsStringSymbol() { - return Kind == Z3SymbolKind.Z3STRINGSYMBOL; + return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL; } /** @@ -61,10 +61,10 @@ package com.Microsoft.Z3; - switch ((Z3SymbolKind)Native.getSymbolKind(ctx.nCtx, obj)) + switch ((Z3_symbol_kind)Native.getSymbolKind(ctx.nCtx, obj)) { - case Z3SymbolKind.Z3INTSYMBOL: return new IntSymbol(ctx, obj); - case Z3SymbolKind.Z3STRINGSYMBOL: return new StringSymbol(ctx, obj); + case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj); + case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj); default: throw new Z3Exception("Unknown symbol kind encountered"); } @@ -85,7 +85,7 @@ package com.Microsoft.Z3; if (!IsIntSymbol()) throw new Z3Exception("Int requested from non-Int symbol"); return Native.getSymbolInt(Context.nCtx, NativeObject); - } + } IntSymbol(Context ctx, IntPtr obj) { super(ctx, obj); @@ -98,7 +98,7 @@ package com.Microsoft.Z3; void CheckNativeObject(IntPtr obj) { - if ((Z3SymbolKind)Native.getSymbolKind(Context.nCtx, obj) != Z3SymbolKind.Z3INTSYMBOL) + if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL) throw new Z3Exception("Symbol is not of integer kind"); super.CheckNativeObject(obj); } @@ -120,7 +120,7 @@ package com.Microsoft.Z3; if (!IsStringSymbol()) throw new Z3Exception("String requested from non-String symbol"); return Native.getSymbolString(Context.nCtx, NativeObject); - } + } StringSymbol(Context ctx, IntPtr obj) { super(ctx, obj); @@ -132,7 +132,7 @@ package com.Microsoft.Z3; void CheckNativeObject(IntPtr obj) { - if ((Z3SymbolKind)Native.getSymbolKind(Context.nCtx, obj) != Z3SymbolKind.Z3STRINGSYMBOL) + if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL) throw new Z3Exception("Symbol is not of String kind"); super.CheckNativeObject(obj); diff --git a/src/api/java/com/Microsoft/Z3/Tactic.java b/src/api/java/com/Microsoft/Z3/Tactic.java index a73d1faa7..ae74c3a6b 100644 --- a/src/api/java/com/Microsoft/Z3/Tactic.java +++ b/src/api/java/com/Microsoft/Z3/Tactic.java @@ -22,7 +22,7 @@ package com.Microsoft.Z3; return Native.tacticGetHelp(Context.nCtx, NativeObject); - } + } /** @@ -52,13 +52,13 @@ package com.Microsoft.Z3; /** * Apply the tactic to a goal. **/ - public ApplyResult this[Goal g]() + public ApplyResult get(Goal g) { return Apply(g); - } + } /** * Creates a solver that is implemented using the given tactic. @@ -69,7 +69,7 @@ package com.Microsoft.Z3; return Context.MkSolver(this); - } + } Tactic(Context ctx, IntPtr obj) { super(ctx, obj); @@ -95,13 +95,13 @@ package com.Microsoft.Z3; void IncRef(IntPtr o) { - Context.TacticDRQ.IncAndClear(Context, o); + Context.Tactic_DRQ.IncAndClear(Context, o); super.IncRef(o); } void DecRef(IntPtr o) { - Context.TacticDRQ.Add(o); + Context.Tactic_DRQ.Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Version.java b/src/api/java/com/Microsoft/Z3/Version.java index c6384df02..8038f02d5 100644 --- a/src/api/java/com/Microsoft/Z3/Version.java +++ b/src/api/java/com/Microsoft/Z3/Version.java @@ -17,42 +17,42 @@ package com.Microsoft.Z3; /** * The major version **/ - public Integer Major() + public long Major() { - Integer major = 0, minor = 0, build = 0, revision = 0; + long major = 0, minor = 0, build = 0, revision = 0; Native.getVersion(major, minor, build, revision); return major; - } + } /** * The minor version **/ - public Integer Minor() + public long Minor() { - Integer major = 0, minor = 0, build = 0, revision = 0; + long major = 0, minor = 0, build = 0, revision = 0; Native.getVersion(major, minor, build, revision); return minor; - } + } /** * The build version **/ - public Integer Build() + public long Build() { - Integer major = 0, minor = 0, build = 0, revision = 0; + long major = 0, minor = 0, build = 0, revision = 0; Native.getVersion(major, minor, build, revision); return build; - } + } /** * The revision **/ - public Integer Revision() + public long Revision() { - Integer major = 0, minor = 0, build = 0, revision = 0; + long major = 0, minor = 0, build = 0, revision = 0; Native.getVersion(major, minor, build, revision); return revision; - } + } /** * A string representation of the version information. @@ -61,7 +61,7 @@ package com.Microsoft.Z3; { - Integer major = 0, minor = 0, build = 0, revision = 0; + long major = 0, minor = 0, build = 0, revision = 0; Native.getVersion(major, minor, build, revision); return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString(); } diff --git a/src/api/java/com/Microsoft/Z3/Z3Object.java b/src/api/java/com/Microsoft/Z3/Z3Object.java index 980f200ef..ca4258980 100644 --- a/src/api/java/com/Microsoft/Z3/Z3Object.java +++ b/src/api/java/com/Microsoft/Z3/Z3Object.java @@ -25,18 +25,18 @@ package com.Microsoft.Z3; **/ public void Dispose() { - if (mNObj != IntPtr.Zero) + if (m_n_obj != IntPtr.Zero) { - DecRef(mNObj); - mNObj = IntPtr.Zero; + DecRef(m_n_obj); + m_n_obj = IntPtr.Zero; } - if (mCtx != null) + if (m_ctx != null) { - mCtx.refCount--; - if (mCtx.refCount == 0) - GC.ReRegisterForFinalize(mCtx); - mCtx = null; + m_ctx.refCount--; + if (m_ctx.refCount == 0) + GC.ReRegisterForFinalize(m_ctx); + m_ctx = null; } GC.SuppressFinalize(this); @@ -49,15 +49,15 @@ package com.Microsoft.Z3; } - private Context mCtx = null; - private IntPtr mNObj = IntPtr.Zero; + private Context m_ctx = null; + private IntPtr m_n_obj = IntPtr.Zero; Z3Object(Context ctx) { ctx.refCount++; - mCtx = ctx; + m_ctx = ctx; } Z3Object(Context ctx, IntPtr obj) @@ -65,9 +65,9 @@ package com.Microsoft.Z3; ctx.refCount++; - mCtx = ctx; + m_ctx = ctx; IncRef(obj); - mNObj = obj; + m_n_obj = obj; } void IncRef(IntPtr o) { } @@ -77,12 +77,12 @@ package com.Microsoft.Z3; IntPtr NativeObject { - get { return mNObj; } + get { return m_n_obj; } set { if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); } - if (mNObj != IntPtr.Zero) { DecRef(mNObj); } - mNObj = value; + if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); } + m_n_obj = value; } } @@ -97,7 +97,7 @@ package com.Microsoft.Z3; get { - return mCtx; + return m_ctx; } } @@ -108,13 +108,13 @@ package com.Microsoft.Z3; if (a == null) return null; IntPtr[] an = new IntPtr[a.Length]; - for (Integer i = 0; i < a.Length; i++) + for (long i = 0; i < a.Length; i++) if (a[i] != null) an[i] = a[i].NativeObject; return an; } - static Integer ArrayLength(Z3Object[] a) + static long ArrayLength(Z3Object[] a) { - return (a == null)?0:(Integer)a.Length; + return (a == null)?0:(long)a.Length; } } diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py index fc69fa9b5..a2cc51274 100644 --- a/src/api/java/mk_java.py +++ b/src/api/java/mk_java.py @@ -30,14 +30,22 @@ def subst_getters(s, getters): def type_replace(s): s = s.replace("bool", "boolean") - s = s.replace("uint", "Integer") + s = s.replace("uint", "long") s = s.replace("string", "String") return s def rename_native(s): - a = re.sub("Native.Z3_(?P\w+)", "Native.\g", s) - lc_callback = lambda pat: pat.group("id").upper() - return re.sub("_(?P\w)", lc_callback, a) + while s.find("Native.Z3") != -1: + i0 = s.find("Native.Z3") + i1 = s.find("(", i0) + c0 = s[:i0] + c1 = s[i0:i1] + c1 = c1.replace("Native.Z3_", "Native.") + c2 = s[i1:] + lc_callback = lambda pat: pat.group("id").upper() + c1 = re.sub("_(?P\w)", lc_callback, c1) + s = c0 + c1 + c2 + return s def translate(filename): @@ -54,6 +62,9 @@ def translate(filename): in_getter_type = "" in_unsupported = 0 getters = [] + in_bracket_op = 0 + in_getter_get = 0 + in_getter_set = 0 for line in fileinput.input(os.path.join(CS, filename)): s = string.rstrip(string.lstrip(line)) if in_javadoc: @@ -97,19 +108,19 @@ def translate(filename): tgt.write("/* " + s + " */\n") elif s.startswith("namespace"): pass - elif s.startswith("public") and s.find("operator") and (s.find("==") != -1 or s.find("!=") != -1): + elif s.startswith("public") and s.find("operator") != -1 and (s.find("==") != -1 or s.find("!=") != -1): t = "" for i in range(0, line.find(s)+1): t += " " tgt.write(t + "/* Overloaded operators are not translated. */\n") in_unsupported = 1; - elif s.startswith("public class") or s.startswith("internal class"): + elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"): a = line.replace(":", "extends").replace("internal ", "") a = a.replace(", IComparable", "") tgt.write(a) in_class = 1 in_static_class = 0 - elif s.startswith("public static class"): + elif s.startswith("public static class") or s.startswith("abstract class"): tgt.write(line.replace(":", "extends").replace("static", "final")) in_class = 1 in_static_class = 1 @@ -119,8 +130,9 @@ def translate(filename): elif skip_brace and s == "{": skip_brace = 0 elif s.find("public") != -1 and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1: + if (s.startswith("new")): + s = s[3:] tokens = s.split(" ") - print "# TOKENS: " + str(len(tokens)) if len(tokens) == 3: in_getter = tokens[2] in_getter_type = type_replace((tokens[0] + " " + tokens[1])) @@ -129,8 +141,14 @@ def translate(filename): lastindent = line.find(s) skip_brace = 1 elif len(tokens) == 4: - in_getter = tokens[3] - in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2]) + if tokens[2].startswith("this["): + in_bracket_op = 1 + in_getter = type_replace(tokens[2]).replace("this[", "get(") + in_getter += " " + tokens[3].replace("]", ")") + in_getter_type = type_replace(tokens[0] + " " + tokens[1]) + else: + in_getter = tokens[3] + in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2]) if in_static_class: in_getter_type = in_getter_type.replace("static", "") lastindent = line.find(s) @@ -156,9 +174,13 @@ def translate(filename): d = line[0:line.find("{ get")] rest = line[line.find("{ get")+5:] rest = rest.replace("} }", "}") + rest = re.sub("Contract.\w+\([\s\S]*\);", "", rest) subst_getters(rest, getters) rest = rename_native(rest) - tgt.write(d + "()" + rest) + if in_bracket_op: + tgt.write(d + rest) + else: + tgt.write(d + "()" + rest) print "ACC: " + s + " --> " + in_getter elif in_getter != "" and s.startswith("get"): t = "" @@ -169,7 +191,12 @@ def translate(filename): subst_getters(rest, getters) rest = type_replace(rest) rest = rename_native(rest) - tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") + if in_bracket_op: + tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n") + else: + tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") + if rest.find("}") == -1: + in_getter_get = 1 elif in_getter != "" and s.startswith("set"): t = "" for i in range(0, lastindent): @@ -182,10 +209,23 @@ def translate(filename): rest = rename_native(rest) ac_acc = in_getter_type[:in_getter_type.find(' ')] ac_type = in_getter_type[in_getter_type.find(' ')+1:] - tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n") - elif in_getter != "" and s == "}": + if in_bracket_op: + in_getter = in_getter.replace("get", "set").replace(")", "") + tgt.write(t + ac_acc + " void " + in_getter + ", " + ac_type + " value) " + rest + "\n") + else: + tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n") + if rest.find("}") == -1: + in_getter_set = 1 + elif in_getter != "" and in_getter_get and s == "}": + tgt.write(line) + in_getter_get = 0 + elif in_getter != "" and in_getter_set and s == "}": + tgt.write(line) + in_getter_set = 0 + elif in_getter != "" and not in_getter_get and not in_getter_set and s == "}": in_getter = "" in_getter_type == "" + in_bracket_op = 0 skip_brace = 0 elif s.startswith("uint ") and s.find("=") == -1: line = line.replace("uint", "Integer", line) @@ -203,25 +243,31 @@ def translate(filename): if line.find("; {") != -1: line = line.replace("; {", ";") else: - skip_brace = 1 + skip_brace = 1 if s.startswith("public"): line = re.sub(" = [\w.]+(?P[,;\)])", "\g", line) - line = re.sub("(?P[\(, ])params ", "\g", line) - line = line.replace("base.", "super.") a = type_replace(line) + a = re.sub("(?P[\(, ])params ", "\g", a) + a = a.replace("base.", "super.") a = re.sub("Contract.\w+\([\s\S]*\);", "", a) a = rename_native(a) a = re.sub("~\w+\(\)", "protected void finalize()", a) a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", "for (\g.Iterator \g = \g.iterator(); \g.hasNext(); )", a) - a = a.replace("readonly private", "private") - a = a.replace("new public", "public") + a = a.replace("readonly ", "") + a = a.replace("const ", "final ") a = a.replace("ToString", "toString") a = a.replace("internal ", "") + a = a.replace("new static", "static") + a = a.replace("new public", "public") a = a.replace("override ", "") a = a.replace("virtual ", "") a = a.replace("o as AST", "(AST) o") a = a.replace("other as AST", "(AST) other") + a = a.replace("o as FuncDecl", "(FuncDecl) o") + a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();") + a = a.replace("out res", "res") + a = a.replace("lock (", "synchronized (") if in_static_class: a = a.replace("static", "") a = re.sub("ref (?P\w+)", "\g", a)