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)