mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
Beginnings of a new ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
9790784488
commit
70f0d2f423
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 <stddef.h>\n')
|
||||
ml_wrapper.write('#include <string.h>\n')
|
||||
ml_wrapper.write('#include <caml/mlvalues.h>\n')
|
||||
ml_wrapper.write('#include <caml/memory.h>\n')
|
||||
ml_wrapper.write('#include <caml/alloc.h>\n')
|
||||
ml_wrapper.write('#include <caml/fail.h>\n')
|
||||
ml_wrapper.write('#include <caml/callback.h>\n')
|
||||
ml_wrapper.write('#ifdef Custom_tag\n')
|
||||
ml_wrapper.write('#include <caml/custom.h>\n')
|
||||
ml_wrapper.write('#include <caml/bigarray.h>\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()
|
||||
|
|
|
|||
3
src/api/ml/README
Normal file
3
src/api/ml/README
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
This directory is work in progress.
|
||||
|
||||
We are currently working on a brand new ML API.
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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)
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
Loading…
Reference in a new issue