From 70f0d2f423f32d6a7ef23e6d9b202d3355d2ddd4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 11 Dec 2012 13:37:02 +0000 Subject: [PATCH] Beginnings of a new ML API Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_project.py | 1 + scripts/mk_util.py | 36 +- scripts/update_api.py | 207 ++++++++++ src/api/ml/README | 3 + .../ml/{ => old}/add_error_checking.V3.sed | 0 src/api/ml/{ => old}/add_error_checking.sed | 0 src/api/ml/{ => old}/build-lib.cmd | 0 src/api/ml/{ => old}/build-lib.sh | 0 src/api/ml/{ => old}/build-test.cmd | 0 src/api/ml/{ => old}/build-test.sh | 0 src/api/ml/{ => old}/build.cmd | 0 src/api/ml/{ => old}/clean.cmd | 0 src/api/ml/{ => old}/cleantmp.cmd | 0 src/api/ml/{ => old}/compile_mlapi.cmd | 0 src/api/ml/{ => old}/error_handling.idl | 0 src/api/ml/{ => old}/exec.cmd | 0 src/api/ml/{ => old}/exec.sh | 0 src/api/ml/{ => old}/generate_mlapi.cmd | 0 src/api/ml/{ => old}/generate_mlapi.sh | 0 src/api/ml/{ => old}/import.cmd | 0 src/api/ml/{ => old}/mlx_get_app_args.idl | 0 src/api/ml/{ => old}/mlx_get_array_sort.idl | 0 .../ml/{ => old}/mlx_get_datatype_sort.idl | 0 src/api/ml/{ => old}/mlx_get_domains.idl | 0 src/api/ml/{ => old}/mlx_get_error_msg.idl | 0 .../ml/{ => old}/mlx_get_pattern_terms.idl | 0 src/api/ml/{ => old}/mlx_get_tuple_sort.idl | 0 src/api/ml/{ => old}/mlx_mk_context_x.idl | 0 src/api/ml/{ => old}/mlx_mk_datatypes.idl | 0 src/api/ml/{ => old}/mlx_mk_numeral.idl | 0 src/api/ml/{ => old}/mlx_mk_sort.idl | 0 src/api/ml/{ => old}/mlx_mk_symbol.idl | 0 src/api/ml/{ => old}/mlx_model.idl | 0 src/api/ml/{ => old}/mlx_numeral_refine.idl | 0 src/api/ml/{ => old}/mlx_parse_smtlib.idl | 0 src/api/ml/{ => old}/mlx_sort_refine.idl | 0 src/api/ml/{ => old}/mlx_statistics.idl | 0 src/api/ml/{ => old}/mlx_symbol_refine.idl | 0 src/api/ml/{ => old}/mlx_term_refine.idl | 0 src/api/ml/{ => old}/postprocess.sed | 0 src/api/ml/{ => old}/preprocess.sed | 0 src/api/ml/{ => old}/queen.ml | 0 src/api/ml/{ => old}/queen.regress.err | 0 src/api/ml/{ => old}/queen.regress.out | 0 src/api/ml/{ => old}/reverse.sed | 0 src/api/ml/{ => old}/test_mlapi.cmd | 0 src/api/ml/{ => old}/test_theory.ml | 0 src/api/ml/{ => old}/update-ml-doc.cmd | 0 src/api/ml/{ => old}/x3V3.ml | 0 src/api/ml/{ => old}/x3V3.mli | 0 src/api/ml/{ => old}/z3.0.idl | 0 src/api/ml/test_capi.regress.err | 5 - src/api/ml/test_capi.regress.out | 386 ------------------ src/api/ml/test_mlapi.regress.err | 0 src/api/ml/test_mlapi.regress.out | 32 -- src/api/ml/test_mlapiV3.regress.err | 5 - src/api/ml/test_mlapiV3.regress.out | 315 -------------- 57 files changed, 245 insertions(+), 745 deletions(-) create mode 100644 src/api/ml/README rename src/api/ml/{ => old}/add_error_checking.V3.sed (100%) rename src/api/ml/{ => old}/add_error_checking.sed (100%) rename src/api/ml/{ => old}/build-lib.cmd (100%) rename src/api/ml/{ => old}/build-lib.sh (100%) rename src/api/ml/{ => old}/build-test.cmd (100%) rename src/api/ml/{ => old}/build-test.sh (100%) rename src/api/ml/{ => old}/build.cmd (100%) rename src/api/ml/{ => old}/clean.cmd (100%) rename src/api/ml/{ => old}/cleantmp.cmd (100%) rename src/api/ml/{ => old}/compile_mlapi.cmd (100%) rename src/api/ml/{ => old}/error_handling.idl (100%) rename src/api/ml/{ => old}/exec.cmd (100%) rename src/api/ml/{ => old}/exec.sh (100%) rename src/api/ml/{ => old}/generate_mlapi.cmd (100%) rename src/api/ml/{ => old}/generate_mlapi.sh (100%) rename src/api/ml/{ => old}/import.cmd (100%) rename src/api/ml/{ => old}/mlx_get_app_args.idl (100%) rename src/api/ml/{ => old}/mlx_get_array_sort.idl (100%) rename src/api/ml/{ => old}/mlx_get_datatype_sort.idl (100%) rename src/api/ml/{ => old}/mlx_get_domains.idl (100%) rename src/api/ml/{ => old}/mlx_get_error_msg.idl (100%) rename src/api/ml/{ => old}/mlx_get_pattern_terms.idl (100%) rename src/api/ml/{ => old}/mlx_get_tuple_sort.idl (100%) rename src/api/ml/{ => old}/mlx_mk_context_x.idl (100%) rename src/api/ml/{ => old}/mlx_mk_datatypes.idl (100%) rename src/api/ml/{ => old}/mlx_mk_numeral.idl (100%) rename src/api/ml/{ => old}/mlx_mk_sort.idl (100%) rename src/api/ml/{ => old}/mlx_mk_symbol.idl (100%) rename src/api/ml/{ => old}/mlx_model.idl (100%) rename src/api/ml/{ => old}/mlx_numeral_refine.idl (100%) rename src/api/ml/{ => old}/mlx_parse_smtlib.idl (100%) rename src/api/ml/{ => old}/mlx_sort_refine.idl (100%) rename src/api/ml/{ => old}/mlx_statistics.idl (100%) rename src/api/ml/{ => old}/mlx_symbol_refine.idl (100%) rename src/api/ml/{ => old}/mlx_term_refine.idl (100%) rename src/api/ml/{ => old}/postprocess.sed (100%) rename src/api/ml/{ => old}/preprocess.sed (100%) rename src/api/ml/{ => old}/queen.ml (100%) rename src/api/ml/{ => old}/queen.regress.err (100%) rename src/api/ml/{ => old}/queen.regress.out (100%) rename src/api/ml/{ => old}/reverse.sed (100%) rename src/api/ml/{ => old}/test_mlapi.cmd (100%) rename src/api/ml/{ => old}/test_theory.ml (100%) rename src/api/ml/{ => old}/update-ml-doc.cmd (100%) rename src/api/ml/{ => old}/x3V3.ml (100%) rename src/api/ml/{ => old}/x3V3.mli (100%) rename src/api/ml/{ => old}/z3.0.idl (100%) delete mode 100644 src/api/ml/test_capi.regress.err delete mode 100644 src/api/ml/test_capi.regress.out delete mode 100644 src/api/ml/test_mlapi.regress.err delete mode 100644 src/api/ml/test_mlapi.regress.out delete mode 100644 src/api/ml/test_mlapiV3.regress.err delete mode 100644 src/api/ml/test_mlapiV3.regress.out diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b30bba609..e2b003d21 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -87,6 +87,7 @@ def init_project_def(): 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_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest') + add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') # Examples diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4641a7b1b..cb6b17cce 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -65,6 +65,7 @@ VS_PROJ = False TRACE = False DOTNET_ENABLED=False JAVA_ENABLED=False +ML_ENABLED=False STATIC_LIB=False VER_MAJOR=None VER_MINOR=None @@ -476,13 +477,13 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH + global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=']) + 'githash=', 'ml']) except: print("ERROR: Invalid command line option") display_help(1) @@ -535,6 +536,8 @@ def parse_options(): GPROF = True elif opt == '--githash': GIT_HASH=arg + elif opt in ('', '--ml'): + ML_ENABLED = True else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -621,6 +624,9 @@ def is_verbose(): def is_java_enabled(): return JAVA_ENABLED +def is_ml_enabled(): + return ML_ENABLED + def is_compiler(given, expected): """ Return True if the 'given' compiler is the expected one. @@ -1268,6 +1274,26 @@ class JavaDLLComponent(Component): shutil.copy(os.path.join(build_path, 'libz3java.%s' % so), os.path.join(dist_path, 'bin', 'libz3java.%s' % so)) +class MLComponent(Component): + def __init__(self, name, lib_name, path, deps): + Component.__init__(self, name, path, deps) + if lib_name == None: + lib_name = name + self.lib_name = lib_name + + def mk_makefile(self, out): + if is_ml_enabled(): + mk_dir(os.path.join(BUILD_DIR, 'api', 'ml')) + libfile = '%s$(LIB_EXT)' % self.lib_name + out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'z3_native.c'))) + out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) %s/z3_native.c\n' % self.to_src_dir) + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'z3_native')) + out.write('ml: %s\n' % libfile) + out.write('\n') + + def main_component(self): + return is_ml_enabled() + class ExampleComponent(Component): def __init__(self, name, path): Component.__init__(self, name, path, []) @@ -1430,6 +1456,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps) reg_component(name, c) +def add_ml_lib(name, deps=[], path=None, lib_name=None): + c = MLComponent(name, lib_name, path, deps) + reg_component(name, c) + def add_cpp_example(name, path=None): c = CppExampleComponent(name, path) reg_component(name, c) @@ -1513,6 +1543,7 @@ def mk_config(): # End of Windows VS config.mk if is_verbose(): print('64-bit: %s' % is64()) + print('ML API: %s' % is_ml_enabled()) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -1631,6 +1662,7 @@ def mk_config(): if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) + print('ML API: %s' % is_ml_enabled()) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) diff --git a/scripts/update_api.py b/scripts/update_api.py index 2fbf42cca..9ef0ce9a2 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -155,6 +155,10 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I STRING : 'jstring', STRING_PTR : 'jobject', BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'} +# Mapping to ML types +Type2ML = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', + STRING : 'char*', STRING_PTR : 'char**', + BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int' } next_type_id = FIRST_OBJ_ID @@ -205,6 +209,13 @@ def type2javaw(ty): else: return Type2JavaW[ty] +def type2ml(ty): + global Type2ML + if (ty >= FIRST_OBJ_ID): + return 'long' + else: + return Type2ML[ty] + def _in(ty): return (IN, ty); @@ -313,6 +324,24 @@ def param2pystr(p): else: return type2pystr(param_type(p)) +def param2ml(p): + k = param_kind(p) + if k == OUT: + if param_type(p) == INT or param_type(p) == UINT: + return "int*" + elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: + return "long*" + elif param_type(p) == STRING: + return "char*" + else: + print "ERROR: unreachable code" + assert(False) + exit(1) + if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + return "%s[]" % type2ml(param_type(p)) + else: + return type2ml(param_type(p)) + # Save name, result, params to generate wrapper _API2PY = [] @@ -1039,6 +1068,183 @@ def mk_bindings(): exe_c.write(" in.register_cmd(%s, exec_%s);\n" % (key, val)) exe_c.write("}\n") +def ml_method_name(name): + result = '' + name = name[3:] # Remove Z3_ + return result + +def mk_ml(): + if not is_ml_enabled(): + return + ml_dir = get_component('ml').src_dir + ml_nativef = os.path.join(ml_dir, 'z3_native.ml') + ml_wrapperf = os.path.join(ml_dir, 'z3_native.c') + ml_native = open(ml_nativef, 'w') + ml_native.write('// Automatically generated file\n') + ml_native.write('\n') + for name, result, params in _dotnet_decls: + ml_native.write(' external %s : (' % ml_method_name(name)) + first = True + i = 0; + for param in params: + if first: + first = False + else: + ml_native.write(', ') + ml_native.write('%s a%d' % (param2ml(param), i)) + i = i + 1 + ml_native.write('%s)\n' % (type2ml(result))) + # ml_native.write(' = "NATIVE_%s"' % ml_method_name(name)) + # ml_native.write('\n\n') + # # Exception wrappers + # for name, result, params in _dotnet_decls: + # java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) + # first = True + # i = 0; + # for param in params: + # if first: + # first = False + # else: + # java_native.write(', ') + # java_native.write('%s a%d' % (param2java(param), i)) + # i = i + 1 + # java_native.write(')') + # if len(params) > 0 and param_type(params[0]) == CONTEXT: + # java_native.write(' throws Z3Exception') + # java_native.write('\n') + # java_native.write(' {\n') + # java_native.write(' ') + # if result != VOID: + # java_native.write('%s res = ' % type2java(result)) + # java_native.write('INTERNAL%s(' % (java_method_name(name))) + # first = True + # i = 0; + # for param in params: + # if first: + # first = False + # else: + # java_native.write(', ') + # java_native.write('a%d' % i) + # i = i + 1 + # java_native.write(');\n') + # if len(params) > 0 and param_type(params[0]) == CONTEXT: + # java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + # java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + # java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + # if result != VOID: + # java_native.write(' return res;\n') + # java_native.write(' }\n\n') + # java_native.write('}\n') + ml_wrapper = open(ml_wrapperf, 'w') + ml_wrapper.write('// Automatically generated file\n\n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#ifdef Custom_tag\n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#include \n') + ml_wrapper.write('#endif\n') + # for name, result, params in _dotnet_decls: + # java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) + # i = 0; + # for param in params: + # java_wrapper.write(', ') + # java_wrapper.write('%s a%d' % (param2javaw(param), i)) + # i = i + 1 + # java_wrapper.write(') {\n') + # # preprocess arrays, strings, in/out arguments + # i = 0 + # for param in params: + # k = param_kind(param) + # if k == OUT or k == INOUT: + # java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) + # elif k == IN_ARRAY or k == INOUT_ARRAY: + # if param_type(param) == INT or param_type(param) == UINT: + # java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i)) + # else: + # java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i)) + # elif k == OUT_ARRAY: + # java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), + # i, + # type2str(param_type(param)), + # param_array_capacity_pos(param), + # type2str(param_type(param)))) + # if param_type(param) == INT or param_type(param) == UINT: + # java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + # else: + # java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) + # elif k == IN and param_type(param) == STRING: + # java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) + # i = i + 1 + # # invoke procedure + # java_wrapper.write(' ') + # if result != VOID: + # java_wrapper.write('%s result = ' % type2str(result)) + # java_wrapper.write('%s(' % name) + # i = 0 + # first = True + # for param in params: + # if first: + # first = False + # else: + # java_wrapper.write(', ') + # k = param_kind(param) + # if k == OUT or k == INOUT: + # java_wrapper.write('&_a%s' % i) + # elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: + # java_wrapper.write('_a%s' % i) + # elif k == IN and param_type(param) == STRING: + # java_wrapper.write('_a%s' % i) + # else: + # java_wrapper.write('(%s)a%i' % (param2str(param), i)) + # i = i + 1 + # java_wrapper.write(');\n') + # # cleanup + # i = 0 + # for param in params: + # k = param_kind(param) + # if k == OUT_ARRAY: + # if param_type(param) == INT or param_type(param) == UINT: + # java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + # else: + # java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i)) + # java_wrapper.write(' free(_a%s);\n' % i) + # elif k == IN_ARRAY or k == OUT_ARRAY: + # if param_type(param) == INT or param_type(param) == UINT: + # java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i)) + # else: + # java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i)) + + # elif k == OUT or k == INOUT: + # if param_type(param) == INT or param_type(param) == UINT: + # java_wrapper.write(' {\n') + # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n') + # java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i)) + # java_wrapper.write(' }\n') + # else: + # java_wrapper.write(' {\n') + # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') + # java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) + # java_wrapper.write(' }\n') + # i = i + 1 + # # return + # if result == STRING: + # java_wrapper.write(' return jenv->NewStringUTF(result);\n') + # elif result != VOID: + # java_wrapper.write(' return (%s) result;\n' % type2javaw(result)) + # java_wrapper.write('}\n') + # java_wrapper.write('#ifdef __cplusplus\n') + # java_wrapper.write('}\n') + # java_wrapper.write('#endif\n') + if is_verbose(): + print "Generated '%s'" % ml_nativef + # Collect API(...) commands from def def_APIs(): pat1 = re.compile(" *def_API.*") @@ -1063,6 +1269,7 @@ mk_py_wrappers() mk_dotnet() mk_dotnet_wrappers() mk_java() +mk_ml() log_h.close() log_c.close() diff --git a/src/api/ml/README b/src/api/ml/README new file mode 100644 index 000000000..925fced59 --- /dev/null +++ b/src/api/ml/README @@ -0,0 +1,3 @@ +This directory is work in progress. + +We are currently working on a brand new ML API. diff --git a/src/api/ml/add_error_checking.V3.sed b/src/api/ml/old/add_error_checking.V3.sed similarity index 100% rename from src/api/ml/add_error_checking.V3.sed rename to src/api/ml/old/add_error_checking.V3.sed diff --git a/src/api/ml/add_error_checking.sed b/src/api/ml/old/add_error_checking.sed similarity index 100% rename from src/api/ml/add_error_checking.sed rename to src/api/ml/old/add_error_checking.sed diff --git a/src/api/ml/build-lib.cmd b/src/api/ml/old/build-lib.cmd similarity index 100% rename from src/api/ml/build-lib.cmd rename to src/api/ml/old/build-lib.cmd diff --git a/src/api/ml/build-lib.sh b/src/api/ml/old/build-lib.sh similarity index 100% rename from src/api/ml/build-lib.sh rename to src/api/ml/old/build-lib.sh diff --git a/src/api/ml/build-test.cmd b/src/api/ml/old/build-test.cmd similarity index 100% rename from src/api/ml/build-test.cmd rename to src/api/ml/old/build-test.cmd diff --git a/src/api/ml/build-test.sh b/src/api/ml/old/build-test.sh similarity index 100% rename from src/api/ml/build-test.sh rename to src/api/ml/old/build-test.sh diff --git a/src/api/ml/build.cmd b/src/api/ml/old/build.cmd similarity index 100% rename from src/api/ml/build.cmd rename to src/api/ml/old/build.cmd diff --git a/src/api/ml/clean.cmd b/src/api/ml/old/clean.cmd similarity index 100% rename from src/api/ml/clean.cmd rename to src/api/ml/old/clean.cmd diff --git a/src/api/ml/cleantmp.cmd b/src/api/ml/old/cleantmp.cmd similarity index 100% rename from src/api/ml/cleantmp.cmd rename to src/api/ml/old/cleantmp.cmd diff --git a/src/api/ml/compile_mlapi.cmd b/src/api/ml/old/compile_mlapi.cmd similarity index 100% rename from src/api/ml/compile_mlapi.cmd rename to src/api/ml/old/compile_mlapi.cmd diff --git a/src/api/ml/error_handling.idl b/src/api/ml/old/error_handling.idl similarity index 100% rename from src/api/ml/error_handling.idl rename to src/api/ml/old/error_handling.idl diff --git a/src/api/ml/exec.cmd b/src/api/ml/old/exec.cmd similarity index 100% rename from src/api/ml/exec.cmd rename to src/api/ml/old/exec.cmd diff --git a/src/api/ml/exec.sh b/src/api/ml/old/exec.sh similarity index 100% rename from src/api/ml/exec.sh rename to src/api/ml/old/exec.sh diff --git a/src/api/ml/generate_mlapi.cmd b/src/api/ml/old/generate_mlapi.cmd similarity index 100% rename from src/api/ml/generate_mlapi.cmd rename to src/api/ml/old/generate_mlapi.cmd diff --git a/src/api/ml/generate_mlapi.sh b/src/api/ml/old/generate_mlapi.sh similarity index 100% rename from src/api/ml/generate_mlapi.sh rename to src/api/ml/old/generate_mlapi.sh diff --git a/src/api/ml/import.cmd b/src/api/ml/old/import.cmd similarity index 100% rename from src/api/ml/import.cmd rename to src/api/ml/old/import.cmd diff --git a/src/api/ml/mlx_get_app_args.idl b/src/api/ml/old/mlx_get_app_args.idl similarity index 100% rename from src/api/ml/mlx_get_app_args.idl rename to src/api/ml/old/mlx_get_app_args.idl diff --git a/src/api/ml/mlx_get_array_sort.idl b/src/api/ml/old/mlx_get_array_sort.idl similarity index 100% rename from src/api/ml/mlx_get_array_sort.idl rename to src/api/ml/old/mlx_get_array_sort.idl diff --git a/src/api/ml/mlx_get_datatype_sort.idl b/src/api/ml/old/mlx_get_datatype_sort.idl similarity index 100% rename from src/api/ml/mlx_get_datatype_sort.idl rename to src/api/ml/old/mlx_get_datatype_sort.idl diff --git a/src/api/ml/mlx_get_domains.idl b/src/api/ml/old/mlx_get_domains.idl similarity index 100% rename from src/api/ml/mlx_get_domains.idl rename to src/api/ml/old/mlx_get_domains.idl diff --git a/src/api/ml/mlx_get_error_msg.idl b/src/api/ml/old/mlx_get_error_msg.idl similarity index 100% rename from src/api/ml/mlx_get_error_msg.idl rename to src/api/ml/old/mlx_get_error_msg.idl diff --git a/src/api/ml/mlx_get_pattern_terms.idl b/src/api/ml/old/mlx_get_pattern_terms.idl similarity index 100% rename from src/api/ml/mlx_get_pattern_terms.idl rename to src/api/ml/old/mlx_get_pattern_terms.idl diff --git a/src/api/ml/mlx_get_tuple_sort.idl b/src/api/ml/old/mlx_get_tuple_sort.idl similarity index 100% rename from src/api/ml/mlx_get_tuple_sort.idl rename to src/api/ml/old/mlx_get_tuple_sort.idl diff --git a/src/api/ml/mlx_mk_context_x.idl b/src/api/ml/old/mlx_mk_context_x.idl similarity index 100% rename from src/api/ml/mlx_mk_context_x.idl rename to src/api/ml/old/mlx_mk_context_x.idl diff --git a/src/api/ml/mlx_mk_datatypes.idl b/src/api/ml/old/mlx_mk_datatypes.idl similarity index 100% rename from src/api/ml/mlx_mk_datatypes.idl rename to src/api/ml/old/mlx_mk_datatypes.idl diff --git a/src/api/ml/mlx_mk_numeral.idl b/src/api/ml/old/mlx_mk_numeral.idl similarity index 100% rename from src/api/ml/mlx_mk_numeral.idl rename to src/api/ml/old/mlx_mk_numeral.idl diff --git a/src/api/ml/mlx_mk_sort.idl b/src/api/ml/old/mlx_mk_sort.idl similarity index 100% rename from src/api/ml/mlx_mk_sort.idl rename to src/api/ml/old/mlx_mk_sort.idl diff --git a/src/api/ml/mlx_mk_symbol.idl b/src/api/ml/old/mlx_mk_symbol.idl similarity index 100% rename from src/api/ml/mlx_mk_symbol.idl rename to src/api/ml/old/mlx_mk_symbol.idl diff --git a/src/api/ml/mlx_model.idl b/src/api/ml/old/mlx_model.idl similarity index 100% rename from src/api/ml/mlx_model.idl rename to src/api/ml/old/mlx_model.idl diff --git a/src/api/ml/mlx_numeral_refine.idl b/src/api/ml/old/mlx_numeral_refine.idl similarity index 100% rename from src/api/ml/mlx_numeral_refine.idl rename to src/api/ml/old/mlx_numeral_refine.idl diff --git a/src/api/ml/mlx_parse_smtlib.idl b/src/api/ml/old/mlx_parse_smtlib.idl similarity index 100% rename from src/api/ml/mlx_parse_smtlib.idl rename to src/api/ml/old/mlx_parse_smtlib.idl diff --git a/src/api/ml/mlx_sort_refine.idl b/src/api/ml/old/mlx_sort_refine.idl similarity index 100% rename from src/api/ml/mlx_sort_refine.idl rename to src/api/ml/old/mlx_sort_refine.idl diff --git a/src/api/ml/mlx_statistics.idl b/src/api/ml/old/mlx_statistics.idl similarity index 100% rename from src/api/ml/mlx_statistics.idl rename to src/api/ml/old/mlx_statistics.idl diff --git a/src/api/ml/mlx_symbol_refine.idl b/src/api/ml/old/mlx_symbol_refine.idl similarity index 100% rename from src/api/ml/mlx_symbol_refine.idl rename to src/api/ml/old/mlx_symbol_refine.idl diff --git a/src/api/ml/mlx_term_refine.idl b/src/api/ml/old/mlx_term_refine.idl similarity index 100% rename from src/api/ml/mlx_term_refine.idl rename to src/api/ml/old/mlx_term_refine.idl diff --git a/src/api/ml/postprocess.sed b/src/api/ml/old/postprocess.sed similarity index 100% rename from src/api/ml/postprocess.sed rename to src/api/ml/old/postprocess.sed diff --git a/src/api/ml/preprocess.sed b/src/api/ml/old/preprocess.sed similarity index 100% rename from src/api/ml/preprocess.sed rename to src/api/ml/old/preprocess.sed diff --git a/src/api/ml/queen.ml b/src/api/ml/old/queen.ml similarity index 100% rename from src/api/ml/queen.ml rename to src/api/ml/old/queen.ml diff --git a/src/api/ml/queen.regress.err b/src/api/ml/old/queen.regress.err similarity index 100% rename from src/api/ml/queen.regress.err rename to src/api/ml/old/queen.regress.err diff --git a/src/api/ml/queen.regress.out b/src/api/ml/old/queen.regress.out similarity index 100% rename from src/api/ml/queen.regress.out rename to src/api/ml/old/queen.regress.out diff --git a/src/api/ml/reverse.sed b/src/api/ml/old/reverse.sed similarity index 100% rename from src/api/ml/reverse.sed rename to src/api/ml/old/reverse.sed diff --git a/src/api/ml/test_mlapi.cmd b/src/api/ml/old/test_mlapi.cmd similarity index 100% rename from src/api/ml/test_mlapi.cmd rename to src/api/ml/old/test_mlapi.cmd diff --git a/src/api/ml/test_theory.ml b/src/api/ml/old/test_theory.ml similarity index 100% rename from src/api/ml/test_theory.ml rename to src/api/ml/old/test_theory.ml diff --git a/src/api/ml/update-ml-doc.cmd b/src/api/ml/old/update-ml-doc.cmd similarity index 100% rename from src/api/ml/update-ml-doc.cmd rename to src/api/ml/old/update-ml-doc.cmd diff --git a/src/api/ml/x3V3.ml b/src/api/ml/old/x3V3.ml similarity index 100% rename from src/api/ml/x3V3.ml rename to src/api/ml/old/x3V3.ml diff --git a/src/api/ml/x3V3.mli b/src/api/ml/old/x3V3.mli similarity index 100% rename from src/api/ml/x3V3.mli rename to src/api/ml/old/x3V3.mli diff --git a/src/api/ml/z3.0.idl b/src/api/ml/old/z3.0.idl similarity index 100% rename from src/api/ml/z3.0.idl rename to src/api/ml/old/z3.0.idl diff --git a/src/api/ml/test_capi.regress.err b/src/api/ml/test_capi.regress.err deleted file mode 100644 index 0c383b409..000000000 --- a/src/api/ml/test_capi.regress.err +++ /dev/null @@ -1,5 +0,0 @@ -WARNING: invalid function application, sort mismatch on argument at position 1 -WARNING: (define iff Bool Bool Bool) applied to: -x of sort Int -y of sort Bool - diff --git a/src/api/ml/test_capi.regress.out b/src/api/ml/test_capi.regress.out deleted file mode 100644 index 48870057c..000000000 --- a/src/api/ml/test_capi.regress.out +++ /dev/null @@ -1,386 +0,0 @@ -Z3 4.2.0.0 - -simple_example -CONTEXT: -(solver)END OF CONTEXT - -DeMorgan -DeMorgan is valid - -find_model_example1 -model for: x xor y -sat -y -> false -x -> true - - -find_model_example2 -model for: x < y + 1, x > 2 -sat -y -> 3 -x -> 3 - -model for: x < y + 1, x > 2, not(x = y) -sat -y -> 4 -x -> 3 - - -prove_example1 -prove: x = y implies g(x) = g(y) -valid -disprove: x = y implies g(g(x)) = g(y) -invalid -counterexample: -y -> U!val!0 -x -> U!val!0 -g -> { - U!val!0 -> U!val!1 - U!val!1 -> U!val!2 - else -> U!val!1 -} - - -prove_example2 -prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 -valid -disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1 -invalid -counterexample: -z -> (- 1) -y -> (- 7719) -x -> (- 7719) -g -> { - (- 7719) -> 0 - 0 -> 2 - (- 1) -> 3 - else -> 0 -} - - -push_pop_example1 -assert: x >= 'big number' -push -number of scopes: 1 -assert: x <= 3 -unsat -pop -number of scopes: 0 -sat -x = 1000000000000000000000000000000000000000000000000000000:int -function interpretations: -assert: y > x -sat -y = 1000000000000000000000000000000000000000000000000000001:int -x = 1000000000000000000000000000000000000000000000000000000:int -function interpretations: - -quantifier_example1 -pattern: {(f #0 #1)} - -assert axiom: -(forall (k!0 Int) (k!1 Int) (= (inv!0 (f k!1 k!0)) k!0) :pat {(f k!1 k!0)}) -prove: f(x, y) = f(w, v) implies y = v -valid -disprove: f(x, y) = f(w, v) implies x = w -that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable -unknown -potential model: -w = 2:int -v = 1:int -y = 1:int -x = 0:int -function interpretations: -f = {(else|->(define f!52 Int Int Int)[(define k!50 Int Int)[#unknown], (define k!51 Int Int)[#unknown]])} -#51 = {(2:int|->2:int), (1:int|->1:int), (15:int|->15:int), (11:int|->11:int), (0:int|->0:int), (19:int|->19:int), (else|->2:int)} -f!52 = {(0:int, 1:int|->3:int), (2:int, 1:int|->3:int), (0:int, 0:int|->4:int), (2:int, 0:int|->5:int), (6:int, 2:int|->7:int), (2:int, 2:int|->8:int), (0:int, 2:int|->9:int), (6:int, 0:int|->10:int), (0:int, 11:int|->12:int), (2:int, 11:int|->13:int), (6:int, 11:int|->14:int), (0:int, 15:int|->16:int), (2:int, 15:int|->17:int), (6:int, 15:int|->18:int), (0:int, 19:int|->20:int), (6:int, 19:int|->21:int), (2:int, 19:int|->22:int), (else|->3:int)} -inv!0 = {(3:int|->1:int), (4:int|->0:int), (5:int|->0:int), (7:int|->2:int), (8:int|->2:int), (9:int|->2:int), (10:int|->0:int), (12:int|->11:int), (13:int|->11:int), (14:int|->11:int), (16:int|->15:int), (17:int|->15:int), (18:int|->15:int), (20:int|->19:int), (21:int|->19:int), (22:int|->19:int), (else|->2:int)} -#50 = {(2:int|->2:int), (6:int|->6:int), (0:int|->0:int), (else|->2:int)} -reason for last failure: 7 (7 = quantifiers) - -array_example1 -prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) -(=> (= (store a1 i1 v1) (store a2 i2 v2)) - (or (= i1 i3) (= i2 i3) (= (select a1 i3) (select a2 i3)))) -valid - -array_example2 -n = 2 -(distinct k!0 k!1) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -function interpretations: -#0 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#1 = {((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 3 -(distinct k!0 k!1 k!2) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -#2 = (define as-array[k!2] (Array Bool Bool)) -function interpretations: -#0 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))} -#1 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#2 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 4 -(distinct k!0 k!1 k!2 k!3) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -#2 = (define as-array[k!2] (Array Bool Bool)) -#3 = (define as-array[k!3] (Array Bool Bool)) -function interpretations: -#0 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define true Bool)), (else|->(define false Bool))} -#1 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))} -#2 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#3 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 5 -(distinct k!0 k!1 k!2 k!3 k!4) -unsat - -array_example3 -domain: int -range: bool - -tuple_example1 -tuple_sort: (real, real) -prove: get_x(mk_pair(x, y)) = 1 implies x = 1 -valid -disprove: get_x(mk_pair(x, y)) = 1 implies y = 1 -invalid -counterexample: -y -> 0 -x -> 1 - -prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2 -valid -disprove: get_x(p1) = get_x(p2) implies p1 = p2 -invalid -counterexample: -p1 -> (mk_pair 1 0) -p2 -> (mk_pair 1 2) - -prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10 -valid -disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10 -invalid -counterexample: -p2 -> (mk_pair 10 1) -p1 -> (mk_pair 0 1) - - -bitvector_example1 -disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers -invalid -counterexample: -x -> bv2147483656[32] - - -bitvector_example2 -find values of x and y, such that x ^ y - 103 == x * y -sat -y -> bv3905735879[32] -x -> bv3787456528[32] - - -eval_example1 -MODEL: -y -> 4 -x -> 3 - -evaluating x+y -result = 7:int - -two_contexts_example1 -k!0 - -error_code_example1 -last call succeeded. -last call failed. - -error_code_example2 -before Z3_mk_iff -Z3 error: type error. - -parser_example1 -formula 0: (> x y) -formula 1: (> x 0) -sat -y -> 0 -x -> 1 - - -parser_example2 -formula: (> x y) -sat -y -> (- 1) -x -> 0 - - -parser_example3 -assert axiom: -(forall (x Int) (y Int) (= (g x y) (g y x)) :qid {k!1}) -formula: (forall (x Int) (y Int) (=> (= x y) (= (g x 0) (g 0 y))) :qid {k!1}) -valid - -parser_example4 -declaration 0: (define y Int) -declaration 1: (define sk_hack Bool Bool) -declaration 2: (define x Int) -assumption 0: (= x 20) -formula 0: (> x y) -formula 1: (> x 0) - -parser_example5 -Z3 error: parser error. -Error message: 'ERROR: line 1 column 41: could not find sort symbol 'y'. -'. - -numeral_example -Numerals n1:1/2 n2:1/2 -valid -Numerals n1:(- 1/3) n2:(- 33333333333333333333333333333333333333333333333333/100000000000000000000000000000000000000000000000000) -valid - -ite_example -term: (if false 1 0) - -list_example -valid -valid -valid -valid -valid -valid -valid -Formula (=> (is_cons u) (= u (cons (head u) (tail u)))) -valid -invalid -counterexample: -u -> nil - - -tree_example -valid -valid -valid -valid -valid -Formula (=> (is_cons u) (= u (cons (car u) (cdr u)))) -valid -invalid -counterexample: -u -> nil - - -forest_example -valid -valid -valid -valid -valid -valid - -binary_tree_example -valid -valid -valid -valid -valid - -enum_example -(define apple[fruit:0] fruit) -(define banana[fruit:1] fruit) -(define orange[fruit:2] fruit) -(define is_apple[fruit:0] fruit Bool) -(define is_banana[fruit:1] fruit Bool) -(define is_orange[fruit:2] fruit Bool) -valid -valid -invalid -counterexample: - -valid -valid - -unsat_core_and_proof_example -unsat -proof: [unit-resolution - [def-axiom (or (or (not PredA) PredB (not PredC)) (not PredB))] - [unit-resolution - [def-axiom (or (or (not PredA) (not PredB) (not PredC)) PredB)] - [unit-resolution - [mp - [asserted (or (and PredA PredB PredC) P1)] - [monotonicity - [rewrite - (iff (and PredA PredB PredC) - (not (or (not PredA) (not PredB) (not PredC))))] - (iff (or (and PredA PredB PredC) P1) - (or (not (or (not PredA) (not PredB) (not PredC))) P1))] - (or (not (or (not PredA) (not PredB) (not PredC))) P1)] - [asserted (not P1)] - (not (or (not PredA) (not PredB) (not PredC)))] - PredB] - [unit-resolution - [mp - [asserted (or (and PredA (not PredB) PredC) P2)] - [monotonicity - [rewrite - (iff (and PredA (not PredB) PredC) - (not (or (not PredA) PredB (not PredC))))] - (iff (or (and PredA (not PredB) PredC) P2) - (or (not (or (not PredA) PredB (not PredC))) P2))] - (or (not (or (not PredA) PredB (not PredC))) P2)] - [asserted (not P2)] - (not (or (not PredA) PredB (not PredC)))] - false] - -core: -(not P1) -(not P2) - - -get_implied_equalities example -Class a |-> 0 -Class b |-> 0 -Class c |-> 0 -Class d |-> 3 -Class (f a) |-> 0 -Class (f b) |-> 0 -Class (f c) |-> 0 -asserting f(a) <= b -Class a |-> 0 -Class b |-> 0 -Class c |-> 0 -Class d |-> 3 -Class (f a) |-> 0 -Class (f b) |-> 0 -Class (f c) |-> 0 - -incremental_example1 -unsat core: 0 2 3 -unsat -sat -unsat core: 0 2 3 -unsat -unsat core: 0 2 3 -unsat -sat - -reference_counter_example -model for: x xor y -sat -y -> false -x -> true - - -smt2parser_example -formulas: (and (bvuge a bv16[8]) (bvule a bv240[8])) - -substitute_example -substitution result: (f (f a 0) 1) - -substitute_vars_example -substitution result: (f (f a (g b)) a) diff --git a/src/api/ml/test_mlapi.regress.err b/src/api/ml/test_mlapi.regress.err deleted file mode 100644 index e69de29bb..000000000 diff --git a/src/api/ml/test_mlapi.regress.out b/src/api/ml/test_mlapi.regress.out deleted file mode 100644 index 1fb6289c7..000000000 --- a/src/api/ml/test_mlapi.regress.out +++ /dev/null @@ -1,32 +0,0 @@ -datatype created: -sort: tree -constructor: (define leaf[tree:0] Int tree) recognizer: (define is_leaf[tree:0] tree Bool) accessors: (define data[tree:0:0] tree Int) -constructor: (define node[tree:1] forest tree) recognizer: (define is_node[tree:1] tree Bool) accessors: (define children[tree:1:0] tree forest) -sort: forest -constructor: (define nil[forest:0] forest) recognizer: (define is_nil[forest:0] forest Bool) accessors: -constructor: (define cons[forest:1] tree forest forest) recognizer: (define is_cons[forest:1] forest Bool) accessors: (define hd[forest:1:0] forest tree) (define tl[forest:1:1] forest forest) - -t1: (node (cons (leaf 1) (cons (leaf 2) nil))) -t2: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 3) nil))) -t3: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) - (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil))) -t4: (node (cons (leaf 4) (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil))) -f1: (cons (leaf 0) nil) -f2: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil) -f3: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 0) nil)) -t1: (node (cons (leaf 1) (cons (leaf 2) nil))) -t2: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 3) nil))) -t3: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) - (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil))) -t4: (node (cons (leaf 4) (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil))) -f1: (cons (leaf 0) nil) -f2: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil) -f3: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 0) nil)) -valid -valid -l1: (cons x u) -l2: (cons y v) -valid -valid -valid -valid diff --git a/src/api/ml/test_mlapiV3.regress.err b/src/api/ml/test_mlapiV3.regress.err deleted file mode 100644 index 0c383b409..000000000 --- a/src/api/ml/test_mlapiV3.regress.err +++ /dev/null @@ -1,5 +0,0 @@ -WARNING: invalid function application, sort mismatch on argument at position 1 -WARNING: (define iff Bool Bool Bool) applied to: -x of sort Int -y of sort Bool - diff --git a/src/api/ml/test_mlapiV3.regress.out b/src/api/ml/test_mlapiV3.regress.out deleted file mode 100644 index efcc4388d..000000000 --- a/src/api/ml/test_mlapiV3.regress.out +++ /dev/null @@ -1,315 +0,0 @@ -Z3 4.2.0.0 - -simple_example -CONTEXT: -(solver)END OF CONTEXT - -DeMorgan -DeMorgan is valid - -find_model_example1 -model for: x xor y -sat -y -> false -x -> true - - -find_model_example2 -model for: x < y + 1, x > 2 -sat -y -> 3 -x -> 3 - -model for: x < y + 1, x > 2, not(x = y) -sat -y -> 4 -x -> 3 - - -prove_example1 -prove: x = y implies g(x) = g(y) -valid -disprove: x = y implies g(g(x)) = g(y) -invalid -counterexample: -y -> U!val!0 -x -> U!val!0 -g -> { - U!val!0 -> U!val!1 - U!val!1 -> U!val!2 - else -> U!val!1 -} - - -prove_example2 -prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 -valid -disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1 -invalid -counterexample: -z -> (- 1) -y -> (- 7719) -x -> (- 7719) -g -> { - (- 7719) -> 0 - 0 -> 2 - (- 1) -> 3 - else -> 0 -} - - -push_pop_example1 -assert: x >= 'big number' -push -number of scopes: 1 -assert: x <= 3 -unsat -pop -number of scopes: 0 -sat -x = 1000000000000000000000000000000000000000000000000000000:int -function interpretations: -assert: y > x -sat -y = 1000000000000000000000000000000000000000000000000000001:int -x = 1000000000000000000000000000000000000000000000000000000:int -function interpretations: - -quantifier_example1 -pattern: {(f #0 #1)} - -assert axiom: -(forall (k!0 Int) (k!1 Int) (= (inv!0 (f k!1 k!0)) k!0) :pat {(f k!1 k!0)}) -prove: f(x, y) = f(w, v) implies y = v -valid -disprove: f(x, y) = f(w, v) implies x = w -that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable -unknown -potential model: -w = 2:int -v = 1:int -y = 1:int -x = 0:int -function interpretations: -f = {(else|->(define f!52 Int Int Int)[(define k!50 Int Int)[#unknown], (define k!51 Int Int)[#unknown]])} -#51 = {(2:int|->2:int), (1:int|->1:int), (15:int|->15:int), (11:int|->11:int), (0:int|->0:int), (19:int|->19:int), (else|->2:int)} -f!52 = {(0:int, 1:int|->3:int), (2:int, 1:int|->3:int), (0:int, 0:int|->4:int), (2:int, 0:int|->5:int), (6:int, 2:int|->7:int), (2:int, 2:int|->8:int), (0:int, 2:int|->9:int), (6:int, 0:int|->10:int), (0:int, 11:int|->12:int), (2:int, 11:int|->13:int), (6:int, 11:int|->14:int), (0:int, 15:int|->16:int), (2:int, 15:int|->17:int), (6:int, 15:int|->18:int), (0:int, 19:int|->20:int), (6:int, 19:int|->21:int), (2:int, 19:int|->22:int), (else|->3:int)} -inv!0 = {(3:int|->1:int), (4:int|->0:int), (5:int|->0:int), (7:int|->2:int), (8:int|->2:int), (9:int|->2:int), (10:int|->0:int), (12:int|->11:int), (13:int|->11:int), (14:int|->11:int), (16:int|->15:int), (17:int|->15:int), (18:int|->15:int), (20:int|->19:int), (21:int|->19:int), (22:int|->19:int), (else|->2:int)} -#50 = {(2:int|->2:int), (6:int|->6:int), (0:int|->0:int), (else|->2:int)} -reason for last failure: 7 (7 = quantifiers) - -array_example1 -prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) -(=> (= (store a1 i1 v1) (store a2 i2 v2)) - (or (= i1 i3) (= i2 i3) (= (select a1 i3) (select a2 i3)))) -valid - -array_example2 -n = 2 -(distinct k!0 k!1) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -function interpretations: -#0 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#1 = {((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 3 -(distinct k!0 k!1 k!2) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -#2 = (define as-array[k!2] (Array Bool Bool)) -function interpretations: -#0 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))} -#1 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#2 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 4 -(distinct k!0 k!1 k!2 k!3) -sat -#0 = (define as-array[k!0] (Array Bool Bool)) -#1 = (define as-array[k!1] (Array Bool Bool)) -#2 = (define as-array[k!2] (Array Bool Bool)) -#3 = (define as-array[k!3] (Array Bool Bool)) -function interpretations: -#0 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define true Bool)), (else|->(define false Bool))} -#1 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))} -#2 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define true Bool)), (else|->(define true Bool))} -#3 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))} -n = 5 -(distinct k!0 k!1 k!2 k!3 k!4) -unsat - -array_example3 -domain: int -range: bool - -tuple_example1 -tuple_sort: (real, real) -prove: get_x(mk_pair(x, y)) = 1 implies x = 1 -valid -disprove: get_x(mk_pair(x, y)) = 1 implies y = 1 -invalid -counterexample: -y -> 0 -x -> 1 - -prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2 -valid -disprove: get_x(p1) = get_x(p2) implies p1 = p2 -invalid -counterexample: -p1 -> (mk_pair 1 0) -p2 -> (mk_pair 1 2) - -prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10 -valid -disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10 -invalid -counterexample: -p2 -> (mk_pair 10 1) -p1 -> (mk_pair 0 1) - - -bitvector_example1 -disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers -invalid -counterexample: -x -> bv2147483656[32] - - -bitvector_example2 -find values of x and y, such that x ^ y - 103 == x * y -sat -y -> bv3905735879[32] -x -> bv3787456528[32] - - -eval_example1 -MODEL: -y -> 4 -x -> 3 - -evaluating x+y -result = 7:int - -two_contexts_example1 -k!0 - -error_code_example1 -last call succeeded. -last call failed. - -error_code_example2 -before Z3_mk_iff -Z3 error: type error. - -parser_example1 -formula 0: (> x y) -formula 1: (> x 0) -sat -y -> 0 -x -> 1 - - -parser_example2 -formula: (> x y) -sat -y -> (- 1) -x -> 0 - - -parser_example3 -assert axiom: -(forall (x Int) (y Int) (= (g x y) (g y x)) :qid {k!1}) -formula: (forall (x Int) (y Int) (=> (= x y) (= (g x 0) (g 0 y))) :qid {k!1}) -valid - -parser_example4 -declaration 0: (define y Int) -declaration 1: (define sk_hack Bool Bool) -declaration 2: (define x Int) -assumption 0: (= x 20) -formula 0: (> x y) -formula 1: (> x 0) - -parser_example5 -Z3 error: parser error. -Error message: 'ERROR: line 1 column 41: could not find sort symbol 'y'. -'. - -ite_example -term: (if false 1 0) - -enum_example -(define apple[fruit:0] fruit) -(define banana[fruit:1] fruit) -(define orange[fruit:2] fruit) -(define is_apple[fruit:0] fruit Bool) -(define is_banana[fruit:1] fruit Bool) -(define is_orange[fruit:2] fruit Bool) -valid -valid -invalid -counterexample: - -valid -valid - -unsat_core_and_proof_example -unsat -proof: [unit-resolution - [def-axiom (or (or (not PredA) PredC (not PredB)) (not PredC))] - [unit-resolution - [def-axiom (or (or (not PredA) (not PredB) (not PredC)) PredC)] - [unit-resolution - [mp - [asserted (or (and PredA PredB PredC) P1)] - [monotonicity - [rewrite - (iff (and PredA PredB PredC) - (not (or (not PredA) (not PredB) (not PredC))))] - (iff (or (and PredA PredB PredC) P1) - (or (not (or (not PredA) (not PredB) (not PredC))) P1))] - (or (not (or (not PredA) (not PredB) (not PredC))) P1)] - [asserted (not P1)] - (not (or (not PredA) (not PredB) (not PredC)))] - PredC] - [unit-resolution - [mp - [asserted (or (and PredA (not PredC) PredB) P2)] - [monotonicity - [rewrite - (iff (and PredA (not PredC) PredB) - (not (or (not PredA) PredC (not PredB))))] - (iff (or (and PredA (not PredC) PredB) P2) - (or (not (or (not PredA) PredC (not PredB))) P2))] - (or (not (or (not PredA) PredC (not PredB))) P2)] - [asserted (not P2)] - (not (or (not PredA) PredC (not PredB)))] - false] - -core: -(not P2) -(not P1) - - -abstract_example -formula: (> x y) -abstracted formula: (> #0 y) - -get_implied_equalities example -Class a |-> 0 -Class b |-> 0 -Class c |-> 0 -Class d |-> 3 -Class (f a) |-> 0 -Class (f b) |-> 0 -Class (f c) |-> 0 -asserting f(a) <= b -Class a |-> 0 -Class b |-> 0 -Class c |-> 0 -Class d |-> 3 -Class (f a) |-> 0 -Class (f b) |-> 0 -Class (f c) |-> 0