mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
More Java API. This is still under heavy construction and cannot be used.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
c702454f6c
commit
520bcaf720
42 changed files with 2353 additions and 667 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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 <paramref name="ctx"/>.
|
||||
|
|
@ -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");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
|||
* <param name="i">Index</param>
|
||||
* @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 <paramref name="newSize"/>.
|
||||
* <param name="newSize">The new size of the vector.</param>
|
||||
**/
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 <paramref name="i"/> into a model for the original
|
||||
* goal <code>g</code>, that the ApplyResult was obtained from.
|
||||
* @return A model for <code>g</code>
|
||||
**/
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<String, String>.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.</param>
|
||||
**/
|
||||
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;
|
|||
* <param name="sortRefs"></param>
|
||||
* @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;
|
|||
* <param name="index">The de-Bruijn index of the variable</param>
|
||||
* <param name="ty">The sort of the variable</param>
|
||||
**/
|
||||
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 <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
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 <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
public BitVecExpr MkSignExt(Integer i, BitVecExpr t)
|
||||
public BitVecExpr MkSignExt(long i, BitVecExpr t)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -1538,7 +1547,7 @@ package com.Microsoft.Z3;
|
|||
* The argument <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
public BitVecExpr MkZeroExt(Integer i, BitVecExpr t)
|
||||
public BitVecExpr MkZeroExt(long i, BitVecExpr t)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -1553,7 +1562,7 @@ package com.Microsoft.Z3;
|
|||
* The argument <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
public BitVecExpr MkRepeat(Integer i, BitVecExpr t)
|
||||
public BitVecExpr MkRepeat(long i, BitVecExpr t)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -1640,7 +1649,7 @@ package com.Microsoft.Z3;
|
|||
* The argument <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
public BitVecExpr MkBVRotateLeft(Integer i, BitVecExpr t)
|
||||
public BitVecExpr MkBVRotateLeft(long i, BitVecExpr t)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -1656,7 +1665,7 @@ package com.Microsoft.Z3;
|
|||
* The argument <paramref name="t"/> must have a bit-vector sort.
|
||||
* </remarks>
|
||||
**/
|
||||
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.
|
||||
* </remarks>
|
||||
**/
|
||||
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;
|
|||
* <param name="ty">Sort of the numeral</param>
|
||||
* @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
|
||||
**/
|
||||
public Expr MkNumeral(Integer v, Sort ty)
|
||||
public Expr MkNumeral(long v, Sort ty)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2286,7 +2295,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* @return A Term with value <paramref name="v"/> and sort Real
|
||||
**/
|
||||
public RatNum MkReal(Integer v)
|
||||
public RatNum MkReal(long v)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2345,7 +2354,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* @return A Term with value <paramref name="v"/> and sort Integer
|
||||
**/
|
||||
public IntNum MkInt(Integer v)
|
||||
public IntNum MkInt(long v)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2381,7 +2390,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">A string representing the value in decimal notation.</param>
|
||||
* <param name="size">the size of the bit-vector</param>
|
||||
**/
|
||||
public BitVecNum MkBV(String v, Integer size)
|
||||
public BitVecNum MkBV(String v, long size)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2393,7 +2402,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* <param name="size">the size of the bit-vector</param>
|
||||
**/
|
||||
public BitVecNum MkBV(int v, Integer size)
|
||||
public BitVecNum MkBV(int v, long size)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2405,7 +2414,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* <param name="size">the size of the bit-vector</param>
|
||||
**/
|
||||
public BitVecNum MkBV(Integer v, Integer size)
|
||||
public BitVecNum MkBV(long v, long size)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2417,7 +2426,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* * <param name="size">the size of the bit-vector</param>
|
||||
**/
|
||||
public BitVecNum MkBV(long v, Integer size)
|
||||
public BitVecNum MkBV(long v, long size)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2429,7 +2438,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="v">value of the numeral.</param>
|
||||
* <param name="size">the size of the bit-vector</param>
|
||||
**/
|
||||
public BitVecNum MkBV(ulong v, Integer size)
|
||||
public BitVecNum MkBV(ulong v, long size)
|
||||
{
|
||||
|
||||
|
||||
|
|
@ -2456,7 +2465,7 @@ package com.Microsoft.Z3;
|
|||
* <param name="quantifierID">optional symbol to track quantifier.</param>
|
||||
* <param name="skolemID">optional symbol to track skolem constants.</param>
|
||||
**/
|
||||
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.
|
||||
* <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
|
||||
**/
|
||||
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;
|
|||
* <seealso cref="FuncDecl.ToString()"/>
|
||||
* <seealso cref="Sort.ToString()"/>
|
||||
**/
|
||||
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 <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
**/
|
||||
public Integer NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); }
|
||||
public long NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); }
|
||||
|
||||
/**
|
||||
* The formulas parsed by the last call to <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
|
|
@ -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 <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
**/
|
||||
public Integer NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); }
|
||||
public long NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); }
|
||||
|
||||
/**
|
||||
* The assumptions parsed by the last call to <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
|
|
@ -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 <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
**/
|
||||
public Integer NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); }
|
||||
public long NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); }
|
||||
|
||||
/**
|
||||
* The declarations parsed by the last call to <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
|
|
@ -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 <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
**/
|
||||
public Integer NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); }
|
||||
public long NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); }
|
||||
|
||||
/**
|
||||
* The declarations parsed by the last call to <code>ParseSMTLIBString</code> or <code>ParseSMTLIBFile</code>.
|
||||
|
|
@ -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 <paramref name="t"/> does not terminate within <paramref name="ms"/> milliseconds, then it fails.
|
||||
* </remarks>
|
||||
**/
|
||||
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 <paramref name="t"/> until the goal is not
|
||||
* modified anymore or the maximum number of iterations <paramref name="max"/> 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.
|
||||
///// </remarks>
|
||||
//public delegate void ErrorHandler(Context ctx, Z3ErrorCode errorCode, String errorString);
|
||||
//public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, String errorString);
|
||||
|
||||
///// <summary>
|
||||
///// 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<AST.DecRefQueue>() != null); return mASTDRQ; }
|
||||
ASTMap.DecRefQueue ASTMap_DRQ () { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return mASTMapDRQ; }
|
||||
ASTVector.DecRefQueue ASTVector_DRQ () { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return mASTVectorDRQ; }
|
||||
ApplyResult.DecRefQueue ApplyResult_DRQ () { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return mApplyResultDRQ; }
|
||||
FuncInterp.Entry.DecRefQueue FuncEntry_DRQ () { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return mFuncEntryDRQ; }
|
||||
FuncInterp.DecRefQueue FuncInterp_DRQ () { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return mFuncInterpDRQ; }
|
||||
Goal.DecRefQueue Goal_DRQ () { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return mGoalDRQ; }
|
||||
Model.DecRefQueue Model_DRQ () { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return mModelDRQ; }
|
||||
Params.DecRefQueue Params_DRQ () { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return mParamsDRQ; }
|
||||
ParamDescrs.DecRefQueue ParamDescrs_DRQ () { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return mParamDescrsDRQ; }
|
||||
Probe.DecRefQueue Probe_DRQ () { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return mProbeDRQ; }
|
||||
Solver.DecRefQueue Solver_DRQ () { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return mSolverDRQ; }
|
||||
Statistics.DecRefQueue Statistics_DRQ () { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return mStatisticsDRQ; }
|
||||
Tactic.DecRefQueue Tactic_DRQ () { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return mTacticDRQ; }
|
||||
Fixedpoint.DecRefQueue Fixedpoint_DRQ () { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != 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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<IntPtr> mQueue = new List<IntPtr>();
|
||||
const Integer mMoveLimit = 1024;
|
||||
protected Object m_lock = new Object();
|
||||
protected List<IntPtr> m_queue = new List<IntPtr>();
|
||||
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)
|
||||
{
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
|||
19
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
Normal file
19
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
Normal file
|
|
@ -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),
|
||||
}
|
||||
|
||||
|
|
@ -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),
|
||||
}
|
||||
|
||||
164
src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
Normal file
164
src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
Normal file
|
|
@ -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),
|
||||
}
|
||||
|
||||
|
|
@ -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),
|
||||
}
|
||||
|
||||
16
src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
Normal file
16
src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
Normal file
|
|
@ -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),
|
||||
}
|
||||
|
||||
15
src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
Normal file
15
src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
Normal file
|
|
@ -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),
|
||||
}
|
||||
|
||||
|
|
@ -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),
|
||||
}
|
||||
|
||||
|
|
@ -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),
|
||||
}
|
||||
|
||||
22
src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
Normal file
22
src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
Normal file
|
|
@ -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),
|
||||
}
|
||||
|
||||
|
|
@ -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),
|
||||
}
|
||||
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
* <seealso cref="Arity"/>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
/* 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.</summary>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
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.</summary>
|
||||
**/
|
||||
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;
|
|||
* <param name="args"></param>
|
||||
* @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.
|
||||
|
|
|
|||
|
|
@ -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<Entry[]>().Length,
|
||||
j => Contract.Result<Entry[]>()[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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
* </remarks>
|
||||
**/
|
||||
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 <paramref name="constraints"/> to the given goal.
|
||||
|
|
@ -69,7 +69,7 @@ package com.Microsoft.Z3;
|
|||
* This tracks how many transformations were applied to it.
|
||||
* </remarks>
|
||||
**/
|
||||
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);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 <paramref name="s"/>.
|
||||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,7 +1,10 @@
|
|||
// Automatically generated file
|
||||
package com.Microsoft.Z3;
|
||||
public final class Native {
|
||||
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0240DCD8>"); }
|
||||
public static class IntPtr { public int value; }
|
||||
public static class LongPtr { public long value; }
|
||||
public static class StringPtr { public String value; }
|
||||
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0251B738>"); }
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
|
||||
**/
|
||||
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;
|
|||
* <param name="precision">the precision of the result</param>
|
||||
* @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;
|
|||
* <param name="precision"></param>
|
||||
* @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.
|
||||
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
|
||||
**/
|
||||
public String ToDecimal(Integer precision)
|
||||
public String ToDecimal(long precision)
|
||||
{
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
|||
* <seealso cref="Pop"/>
|
||||
* <seealso cref="Push"/>
|
||||
**/
|
||||
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;
|
|||
* <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <code>NumScopes</code></remarks>
|
||||
* <seealso cref="Push"/>
|
||||
**/
|
||||
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 <code>Check</code>.
|
||||
|
|
@ -165,7 +165,7 @@ package com.Microsoft.Z3;
|
|||
return null;
|
||||
else
|
||||
return Expr.Create(Context, x);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* The unsat core of the last <code>Check</code>.
|
||||
|
|
@ -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 <code>Check</code> returned <code>UNKNOWN</code>.
|
||||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
* <remarks>Returns null if the key is unknown.</remarks>
|
||||
**/
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<id>\w+)", "Native.\g<id>", s)
|
||||
lc_callback = lambda pat: pat.group("id").upper()
|
||||
return re.sub("_(?P<id>\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<id>\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<d>[,;\)])", "\g<d>", line)
|
||||
line = re.sub("(?P<d>[\(, ])params ", "\g<d>", line)
|
||||
line = line.replace("base.", "super.")
|
||||
a = type_replace(line)
|
||||
a = re.sub("(?P<d>[\(, ])params ", "\g<d>", 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<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
|
||||
"for (\g<t>.Iterator \g<i> = \g<w>.iterator(); \g<i>.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<id>\w+)", "\g<id>", a)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue