mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-11-29 17:10:53 -05:00
parent 3e53d00f81 d7042c234f
commit b581ab70ed
53 changed files with 777 additions and 532 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/CMakeLists.txt
View file

@ -59,6 +59,7 @@ endif()
add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
COMMAND
"${PYTHON_EXECUTABLE}" "${MK_API_DOC_SCRIPT}"
--build "${CMAKE_BINARY_DIR}"
--doxygen-executable "${DOXYGEN_EXECUTABLE}"
--output-dir "${DOC_DEST_DIR}"
--temp-dir "${DOC_TEMP_DIR}"

8
doc/mk_api_doc.py
View file

@ -288,6 +288,14 @@ try:
# Put z3py at the beginning of the search path to try to avoid picking up
# an installed copy of Z3py.
sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH))
if sys.version < '3':
import __builtin__
__builtin__.Z3_LIB_DIRS = [ BUILD_DIR ]
else:
import builtins
builtins.Z3_LIB_DIRS = [ BUILD_DIR ]
for modulename in (
'z3',
'z3.z3consts',

64
scripts/mk_util.py
View file

@ -1240,9 +1240,9 @@ def get_so_ext():
sysname = os.uname()[0]
if sysname == 'Darwin':
return 'dylib'
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
return 'so'
elif sysname == 'CYGWIN':
elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
return 'dll'
else:
assert(False)
@ -2072,7 +2072,6 @@ class ExampleComponent(Component):
def is_example(self):
return True
class CppExampleComponent(ExampleComponent):
def __init__(self, name, path):
ExampleComponent.__init__(self, name, path)
@ -2119,6 +2118,30 @@ class CExampleComponent(CppExampleComponent):
def src_files(self):
return get_c_files(self.ex_dir)
def mk_makefile(self, out):
dll_name = get_component(Z3_DLL_COMPONENT).dll_name
dll = '%s$(SO_EXT)' % dll_name
objfiles = ''
for cfile in self.src_files():
objfile = '%s$(OBJ_EXT)' % (cfile[:cfile.rfind('.')])
objfiles = objfiles + ('%s ' % objfile)
out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cfile)));
out.write('\t%s $(CFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(C_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
out.write(' %s' % os.path.join(self.to_ex_dir, cfile))
out.write('\n')
exefile = '%s$(EXE_EXT)' % self.name
out.write('%s: %s %s\n' % (exefile, dll, objfiles))
out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
if IS_WINDOWS:
out.write('%s.lib' % dll_name)
else:
out.write(dll)
out.write(' $(LINK_EXTRA_FLAGS)\n')
out.write('_ex_%s: %s\n\n' % (self.name, exefile))
class DotNetExampleComponent(ExampleComponent):
def __init__(self, name, path):
ExampleComponent.__init__(self, name, path)
@ -2320,6 +2343,7 @@ def mk_config():
'CC=cl\n'
'CXX=cl\n'
'CXX_OUT_FLAG=/Fo\n'
'C_OUT_FLAG=/Fo\n'
'OBJ_EXT=.obj\n'
'LIB_EXT=.lib\n'
'AR=lib\n'
@ -2397,7 +2421,7 @@ def mk_config():
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
config.write('CFLAGS=$(CXXFLAGS)\n')
# End of Windows VS config.mk
if is_verbose():
@ -2418,6 +2442,8 @@ def mk_config():
CXX = find_cxx_compiler()
CC = find_c_compiler()
SLIBEXTRAFLAGS = ''
EXE_EXT = ''
LIB_EXT = '.a'
if GPROF:
CXXFLAGS = '%s -pg' % CXXFLAGS
LDFLAGS = '%s -pg' % LDFLAGS
@ -2447,18 +2473,19 @@ def mk_config():
if DEBUG_MODE:
CXXFLAGS = '%s -g -Wall' % CXXFLAGS
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
CXXFLAGS = '%s -O3' % CXXFLAGS
if GPROF:
CXXFLAGS = '%s -O3 -D _EXTERNAL_RELEASE' % CXXFLAGS
else:
CXXFLAGS = '%s -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer' % CXXFLAGS
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
if is_CXX_clangpp():
CXXFLAGS = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
sysname, _, _, _, machine = os.uname()
if sysname == 'Darwin':
SO_EXT = '.dylib'
SLIBFLAGS = '-dynamiclib'
elif sysname == 'Linux' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
elif sysname == 'Linux':
CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
OS_DEFINES = '-D_LINUX_'
SO_EXT = '.so'
@ -2477,15 +2504,22 @@ def mk_config():
OS_DEFINES = '-D_OPENBSD_'
SO_EXT = '.so'
SLIBFLAGS = '-shared'
elif sysname[:6] == 'CYGWIN':
elif sysname.startswith('CYGWIN'):
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
OS_DEFINES = '-D_CYGWIN'
SO_EXT = '.dll'
SLIBFLAGS = '-shared'
elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
CXXFLAGS = '%s -D_MINGW' % CXXFLAGS
OS_DEFINES = '-D_MINGW'
SO_EXT = '.dll'
SLIBFLAGS = '-shared'
EXE_EXT = '.exe'
LIB_EXT = '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
if is64():
if sysname[:6] != 'CYGWIN':
if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
CXXFLAGS = '%s -fPIC' % CXXFLAGS
CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS
if sysname == 'Linux':
@ -2494,10 +2528,6 @@ def mk_config():
CXXFLAGS = '%s -m32' % CXXFLAGS
LDFLAGS = '%s -m32' % LDFLAGS
SLIBFLAGS = '%s -m32' % SLIBFLAGS
if DEBUG_MODE:
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
if TRACE or DEBUG_MODE:
CPPFLAGS = '%s -D_TRACE' % CPPFLAGS
if is_cygwin_mingw():
@ -2512,14 +2542,16 @@ def mk_config():
config.write('CC=%s\n' % CC)
config.write('CXX=%s\n' % CXX)
config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
config.write('CFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS.replace('-std=c++11', '')))
config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
config.write('CXX_OUT_FLAG=-o \n')
config.write('C_OUT_FLAG=-o \n')
config.write('OBJ_EXT=.o\n')
config.write('LIB_EXT=.a\n')
config.write('LIB_EXT=%s\n' % LIB_EXT)
config.write('AR=%s\n' % AR)
config.write('AR_FLAGS=rcs\n')
config.write('AR_OUTFLAG=\n')
config.write('EXE_EXT=\n')
config.write('EXE_EXT=%s\n' % EXE_EXT)
config.write('LINK=%s\n' % CXX)
config.write('LINK_FLAGS=\n')
config.write('LINK_OUT_FLAG=-o \n')

170
scripts/update_api.py
View file

@ -240,7 +240,7 @@ def param2javaw(p):
if k == OUT:
return "jobject"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
if param_type(p) == INT or param_type(p) == UINT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "jintArray"
else:
return "jlongArray"
@ -258,7 +258,7 @@ def param2pystr(p):
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64:
return "int"
elif param_type(p) == STRING:
return "string"
@ -279,8 +279,8 @@ def mk_py_binding(name, result, params):
global _API2PY
_API2PY.append((name, result, params))
if result != VOID:
core_py.write(" _lib.%s.restype = %s\n" % (name, type2pystr(result)))
core_py.write(" _lib.%s.argtypes = [" % name)
core_py.write("_lib.%s.restype = %s\n" % (name, type2pystr(result)))
core_py.write("_lib.%s.argtypes = [" % name)
first = True
for p in params:
if first:
@ -311,8 +311,32 @@ def display_args_to_z3(params):
core_py.write("a%s" % i)
i = i + 1
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
def mk_py_wrappers():
core_py.write("\n")
core_py.write("""
class Elementaries:
def __init__(self, f):
self.f = f
self.get_error_code = _lib.Z3_get_error_code
self.get_error_message = _lib.Z3_get_error_msg
self.OK = Z3_OK
self.Exception = Z3Exception
def Check(self, ctx):
err = self.get_error_code(ctx)
if err != self.OK:
raise self.Exception(self.get_error_message(ctx, err))
def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handler)):
ceh = _error_handler_type(hndlr)
_elems.f(ctx, ceh)
_elems.Check(ctx)
return ceh
""")
for sig in _API2PY:
name = sig[0]
result = sig[1]
@ -320,25 +344,20 @@ def mk_py_wrappers():
num = len(params)
core_py.write("def %s(" % name)
display_args(num)
core_py.write("):\n")
core_py.write(" _lib = lib()\n")
core_py.write(" if _lib is None or _lib.%s is None:\n" % name)
core_py.write(" return\n")
if result != VOID:
core_py.write(" r = _lib.%s(" % name)
else:
core_py.write(" _lib.%s(" % name)
comma = ", " if num != 0 else ""
core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name))
lval = "r = " if result != VOID else ""
core_py.write(" %s_elems.f(" % lval)
display_args_to_z3(params)
core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT:
core_py.write(" err = _lib.Z3_get_error_code(a0)\n")
core_py.write(" if err != Z3_OK:\n")
core_py.write(" raise Z3Exception(_lib.Z3_get_error_msg(a0, err))\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped:
core_py.write(" _elems.Check(a0)\n")
if result == STRING:
core_py.write(" return _to_pystr(r)\n")
elif result != VOID:
core_py.write(" return r\n")
core_py.write("\n")
core_py
## .NET API native interface
@ -391,10 +410,6 @@ def mk_dotnet(dotnet):
dotnet.write(');\n\n')
dotnet.write(' }\n')
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
def mk_dotnet_wrappers(dotnet):
global Type2Str
dotnet.write("\n")
@ -476,7 +491,7 @@ def java_method_name(name):
# Return the type of the java array elements
def java_array_element_type(p):
if param_type(p) == INT or param_type(p) == UINT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return 'jint'
else:
return 'jlong'
@ -638,7 +653,7 @@ def mk_java(java_dir, package_name):
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:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
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))
@ -648,7 +663,7 @@ def mk_java(java_dir, package_name):
type2str(param_type(param)),
param_array_capacity_pos(param),
type2str(param_type(param))))
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
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))
@ -687,19 +702,19 @@ def mk_java(java_dir, package_name):
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
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:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
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:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
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')
@ -942,7 +957,7 @@ def def_API(name, result, params):
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)
exe_c.write("in.get_uint_array(%s)" % i)
elif ty == INT:
elif ty == INT or ty == BOOL:
log_c.write("U(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)
@ -1605,35 +1620,79 @@ def write_exe_c_preamble(exe_c):
def write_core_py_post(core_py):
core_py.write("""
# Clean up
del _lib
del _default_dirs
del _all_dirs
del _ext
""")
def write_core_py_preamble(core_py):
core_py.write('# Automatically generated file\n')
core_py.write('import sys, os\n')
core_py.write('import ctypes\n')
core_py.write('import pkg_resources\n')
core_py.write('from .z3types import *\n')
core_py.write('from .z3consts import *\n')
core_py.write(
"""
# Automatically generated file
import sys, os
import ctypes
import pkg_resources
from .z3types import *
from .z3consts import *
_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
_lib = None
_default_dirs = ['.',
os.path.dirname(os.path.abspath(__file__)),
pkg_resources.resource_filename('z3', 'lib'),
os.path.join(sys.prefix, 'lib'),
None]
_all_dirs = []
def lib():
global _lib
if _lib is None:
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
break
except:
pass
if _lib is None:
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
return _lib
if sys.version < '3':
import __builtin__
if hasattr(__builtin__, "Z3_LIB_DIRS"):
_all_dirs = __builtin__.Z3_LIB_DIRS
else:
import builtins
if hasattr(builtins, "Z3_LIB_DIRS"):
_all_dirs = builtins.Z3_LIB_DIRS
for v in ('Z3_LIBRARY_PATH', 'PATH'):
if v in os.environ:
lp = os.environ[v];
lds = lp.split(';') if sys.platform in ('win32') else lp.split(':')
_all_dirs.extend(lds)
_all_dirs.extend(_default_dirs)
for d in _all_dirs:
try:
d = os.path.realpath(d)
if os.path.isdir(d):
d = os.path.join(d, 'libz3.%s' % _ext)
if os.path.isfile(d):
_lib = ctypes.CDLL(d)
break
except:
pass
if _lib is None:
# If all else failed, ask the system to find it.
try:
_lib = ctypes.CDLL('libz3.%s' % _ext)
except:
pass
if _lib is None:
print("Could not find libz3.%s; consider adding the directory containing it to" % _ext)
print(" - your system's PATH environment variable,")
print(" - the Z3_LIBRARY_PATH environment variable, or ")
print(" - to the custom Z3_LIBRARY_DIRS Python-builtin before importing the z3 module, e.g. via")
if sys.version < '3':
print(" import __builtin__")
print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
else:
print(" import builtins")
print(" builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
raise Z3Exception("libz3.%s not found." % _ext)
def _to_ascii(s):
if isinstance(s, str):
@ -1653,16 +1712,11 @@ else:
else:
return ""
def init(PATH):
if PATH:
PATH = os.path.realpath(PATH)
if os.path.isdir(PATH):
PATH = os.path.join(PATH, 'libz3.%s' % _ext)
else:
PATH = 'libz3.%s' % _ext
_error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
_lib.Z3_set_error_handler.restype = None
_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
global _lib
_lib = ctypes.CDLL(PATH)
"""
)

13
src/api/api_numeral.cpp
View file

@ -387,4 +387,17 @@ extern "C" {
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
Z3_TRY;
LOG_Z3_mk_bv_numeral(c, sz, bits);
RESET_ERROR_CODE();
rational r(0);
for (unsigned i = 0; i < sz; ++i) {
if (bits[i]) r += rational::power_of_two(i);
}
ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
};

26
src/api/c++/z3++.h
View file

@ -301,6 +301,7 @@ namespace z3 {
expr bv_val(__int64 n, unsigned sz);
expr bv_val(__uint64 n, unsigned sz);
expr bv_val(char const * n, unsigned sz);
expr bv_val(unsigned n, bool const* bits);
expr string_val(char const* s);
expr string_val(std::string const& s);
@ -964,6 +965,13 @@ namespace z3 {
friend expr operator|(expr const & a, expr const & b);
friend expr operator|(expr const & a, int b);
friend expr operator|(int a, expr const & b);
friend expr nand(expr const& a, expr const& b);
friend expr nor(expr const& a, expr const& b);
friend expr xnor(expr const& a, expr const& b);
expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
friend expr operator~(expr const & a);
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
@ -1332,6 +1340,10 @@ namespace z3 {
inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
@ -1406,11 +1418,18 @@ namespace z3 {
inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed reminder operator for bitvectors
\brief signed remainder operator for bitvectors
*/
inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed modulus operator for bitvectors
*/
inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief unsigned reminder operator for bitvectors
@ -2455,6 +2474,11 @@ namespace z3 {
inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(unsigned n, bool const* bits) {
array<Z3_bool> _bits(n);
for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
}
inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }

14
src/api/dotnet/Context.cs
View file

@ -3127,6 +3127,20 @@ namespace Microsoft.Z3
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
/// <summary>
/// Create a bit-vector numeral.
/// </summary>
/// <param name="bits">An array of bits representing the bit-vector. Least signficant bit is at position 0.</param>
public BitVecNum MkBV(bool[] bits)
{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
int[] _bits = new int[bits.Length];
for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;
return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
}
#endregion
#endregion // Numerals

32
src/api/dotnet/Optimize.cs
View file

@ -124,7 +124,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve a lower bound for the objective handle.
/// </summary>
public ArithExpr Lower
public Expr Lower
{
get { return opt.GetLower(handle); }
}
@ -132,7 +132,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve an upper bound for the objective handle.
/// </summary>
public ArithExpr Upper
public Expr Upper
{
get { return opt.GetUpper(handle); }
}
@ -140,7 +140,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve the value of an objective.
/// </summary>
public ArithExpr Value
public Expr Value
{
get { return Lower; }
}
@ -148,7 +148,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve a lower bound for the objective handle.
/// </summary>
public ArithExpr[] LowerAsVector
public Expr[] LowerAsVector
{
get { return opt.GetLowerAsVector(handle); }
}
@ -156,7 +156,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve an upper bound for the objective handle.
/// </summary>
public ArithExpr[] UpperAsVector
public Expr[] UpperAsVector
{
get { return opt.GetUpperAsVector(handle); }
}
@ -240,8 +240,9 @@ namespace Microsoft.Z3
/// Declare an arithmetical maximization objective.
/// Return a handle to the objective. The handle is used as
/// to retrieve the values of objectives after calling Check.
/// The expression can be either an arithmetical expression or bit-vector.
/// </summary>
public Handle MkMaximize(ArithExpr e)
public Handle MkMaximize(Expr e)
{
return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
}
@ -250,45 +251,46 @@ namespace Microsoft.Z3
/// Declare an arithmetical minimization objective.
/// Similar to MkMaximize.
/// </summary>
public Handle MkMinimize(ArithExpr e)
public Handle MkMinimize(Expr e)
{
return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
}
/// <summary>
/// Retrieve a lower bound for the objective handle.
/// </summary>
private ArithExpr GetLower(uint index)
private Expr GetLower(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
return Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
}
/// <summary>
/// Retrieve an upper bound for the objective handle.
/// </summary>
private ArithExpr GetUpper(uint index)
private Expr GetUpper(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
}
/// <summary>
/// Retrieve a lower bound for the objective handle.
/// </summary>
private ArithExpr[] GetLowerAsVector(uint index)
private Expr[] GetLowerAsVector(uint index)
{
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray();
return v.ToExprArray();
}
/// <summary>
/// Retrieve an upper bound for the objective handle.
/// </summary>
private ArithExpr[] GetUpperAsVector(uint index)
private Expr[] GetUpperAsVector(uint index)
{
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray();
return v.ToExprArray();
}
/// <summary>

32
src/api/java/Optimize.java
View file

@ -89,7 +89,7 @@ public class Optimize extends Z3Object {
/**
* Retrieve a lower bound for the objective handle.
**/
public ArithExpr getLower()
public Expr getLower()
{
return opt.GetLower(handle);
}
@ -97,7 +97,7 @@ public class Optimize extends Z3Object {
/**
* Retrieve an upper bound for the objective handle.
**/
public ArithExpr getUpper()
public Expr getUpper()
{
return opt.GetUpper(handle);
}
@ -110,7 +110,7 @@ public class Optimize extends Z3Object {
* and otherwise is represented by the expression {@code value + eps * EPSILON},
* where {@code EPSILON} is an arbitrarily small real number.
*/
public ArithExpr[] getUpperAsVector()
public Expr[] getUpperAsVector()
{
return opt.GetUpperAsVector(handle);
}
@ -120,7 +120,7 @@ public class Optimize extends Z3Object {
*
* <p>See {@link #getUpperAsVector()} for triple semantics.
*/
public ArithExpr[] getLowerAsVector()
public Expr[] getLowerAsVector()
{
return opt.GetLowerAsVector(handle);
}
@ -128,7 +128,7 @@ public class Optimize extends Z3Object {
/**
* Retrieve the value of an objective.
**/
public ArithExpr getValue()
public Expr getValue()
{
return getLower();
}
@ -214,7 +214,7 @@ public class Optimize extends Z3Object {
* Return a handle to the objective. The handle is used as
* to retrieve the values of objectives after calling Check.
**/
public Handle MkMaximize(ArithExpr e)
public Handle MkMaximize(Expr e)
{
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
}
@ -223,7 +223,7 @@ public class Optimize extends Z3Object {
* Declare an arithmetical minimization objective.
* Similar to MkMaximize.
**/
public Handle MkMinimize(ArithExpr e)
public Handle MkMinimize(Expr e)
{
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
}
@ -231,17 +231,17 @@ public class Optimize extends Z3Object {
/**
* Retrieve a lower bound for the objective handle.
**/
private ArithExpr GetLower(int index)
private Expr GetLower(int index)
{
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
}
/**
* Retrieve an upper bound for the objective handle.
**/
private ArithExpr GetUpper(int index)
private Expr GetUpper(int index)
{
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
}
/**
@ -249,7 +249,7 @@ public class Optimize extends Z3Object {
*
* <p>See {@link Handle#getUpperAsVector}.
*/
private ArithExpr[] GetUpperAsVector(int index) {
private Expr[] GetUpperAsVector(int index) {
return unpackObjectiveValueVector(
Native.optimizeGetUpperAsVector(
getContext().nCtx(), getNativeObject(), index
@ -262,7 +262,7 @@ public class Optimize extends Z3Object {
*
* <p>See {@link Handle#getLowerAsVector}.
*/
private ArithExpr[] GetLowerAsVector(int index) {
private Expr[] GetLowerAsVector(int index) {
return unpackObjectiveValueVector(
Native.optimizeGetLowerAsVector(
getContext().nCtx(), getNativeObject(), index
@ -270,12 +270,12 @@ public class Optimize extends Z3Object {
);
}
private ArithExpr[] unpackObjectiveValueVector(long nativeVec) {
private Expr[] unpackObjectiveValueVector(long nativeVec) {
ASTVector vec = new ASTVector(
getContext(), nativeVec
);
return new ArithExpr[] {
(ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2)
return new Expr[] {
(Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
};
}

74
src/api/python/z3/z3.py
View file

@ -112,8 +112,6 @@ def _symbol2py(ctx, s):
else:
return Z3_get_symbol_string(ctx.ref(), s)
_error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
# Hack for having nary functions that can receive one argument that is the
# list of arguments.
def _get_args(args):
@ -127,13 +125,6 @@ def _get_args(args):
except: # len is not necessarily defined when args is not a sequence (use reflection?)
return args
def _Z3python_error_handler_core(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
_Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
def _to_param_value(val):
if isinstance(val, bool):
if val == True:
@ -143,6 +134,11 @@ def _to_param_value(val):
else:
return str(val)
def z3_error_handler(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
class Context:
"""A Context manages all other Z3 objects, global configuration options, etc.
@ -168,17 +164,15 @@ class Context:
else:
Z3_set_param_value(conf, str(prev), _to_param_value(a))
prev = None
self.lib = lib()
self.ctx = Z3_mk_context_rc(conf)
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
lib().Z3_set_error_handler.restype = None
lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
Z3_del_config(conf)
def __del__(self):
self.lib.Z3_del_context(self.ctx)
Z3_del_context(self.ctx)
self.ctx = None
self.eh = None
def ref(self):
"""Return a reference to the actual C pointer to the Z3 context."""
@ -3999,6 +3993,58 @@ def BVRedOr(a):
_z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
def BVAddNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector addition does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVAddNoUnderflow(a, b):
"""A predicate the determines that signed bit-vector addition does not underflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSubNoOverflow(a, b):
"""A predicate the determines that bit-vector subtraction does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSubNoUnderflow(a, b, signed):
"""A predicate the determines that bit-vector subtraction does not underflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVSDivNoOverflow(a, b):
"""A predicate the determines that bit-vector signed division does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSNegNoOverflow(a):
"""A predicate the determines that bit-vector unary negation does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Argument should be a bit-vector")
return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
def BVMulNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector multiplication does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVMulNoUnderflow(a, b):
"""A predicate the determines that bit-vector signed multiplication does not underflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
#########################################
#
# Arrays

8
src/api/z3_api.h
View file

@ -3248,6 +3248,14 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty);
/**
\brief create a bit-vector numeral from a vector of Booleans.
\sa Z3_mk_numeral
def_API('Z3_mk_bv_numeral', AST, (_in(CONTEXT), _in(UINT), _in_array(1, BOOL)))
*/
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits);
/*@}*/
/** @name Sequences and regular expressions */

2
src/ast/arith_decl_plugin.cpp
View file

@ -539,7 +539,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("to_int",OP_TO_INT));
op_names.push_back(builtin_name("is_int",OP_IS_INT));
op_names.push_back(builtin_name("abs", OP_ABS));
if (logic == symbol::null) {
if (logic == symbol::null || logic == symbol("ALL")) {
op_names.push_back(builtin_name("^", OP_POWER));
op_names.push_back(builtin_name("sin", OP_SIN));
op_names.push_back(builtin_name("cos", OP_COS));

2
src/ast/array_decl_plugin.cpp
View file

@ -524,7 +524,7 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
op_names.push_back(builtin_name("store",OP_STORE));
op_names.push_back(builtin_name("select",OP_SELECT));
if (logic == symbol::null || logic == symbol("HORN")) {
if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
// none of the SMT2 logics support these extensions
op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
op_names.push_back(builtin_name("map",OP_ARRAY_MAP));

13
src/ast/ast.cpp
View file

@ -1684,22 +1684,9 @@ ast * ast_manager::register_node_core(ast * n) {
CASSERT("nondet_bug", contains || slow_not_contains(n));
#endif
#if 0
static unsigned counter = 0;
counter++;
if (counter % 100000 == 0)
verbose_stream() << "[ast-table] counter: " << counter << " collisions: " << m_ast_table.collisions() << " capacity: " << m_ast_table.capacity() << " size: " << m_ast_table.size() << "\n";
#endif
ast * r = m_ast_table.insert_if_not_there(n);
SASSERT(r->m_hash == h);
if (r != n) {
#if 0
static unsigned reused = 0;
reused++;
if (reused % 100000 == 0)
verbose_stream() << "[ast-table] reused: " << reused << "\n";
#endif
SASSERT(contains);
SASSERT(m_ast_table.contains(n));
if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {

4
src/ast/bv_decl_plugin.cpp
View file

@ -670,7 +670,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const {
}
void bv_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
if (logic == symbol::null)
if (logic == symbol::null || logic == symbol("ALL"))
sort_names.push_back(builtin_name("bv", BV_SORT));
sort_names.push_back(builtin_name("BitVec", BV_SORT));
}
@ -717,7 +717,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT));
op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
if (logic == symbol::null) {
if (logic == symbol::null || logic == symbol("ALL")) {
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));

2
src/ast/datatype_decl_plugin.cpp
View file

@ -458,7 +458,7 @@ namespace datatype {
void plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.push_back(builtin_name("is", OP_DT_IS));
if (logic == symbol::null) {
if (logic == symbol::null || logic == symbol("ALL")) {
op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD));
}
}

2
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -297,7 +297,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
// The BV model may have multiple equivalent entries using different
// representations of NaN. We can only keep one and we check that
// the results for all those entries are the same.
if (ft_fres != fe->get_result())
if (m_fpa_util.is_float(rng) && ft_fres != fe->get_result())
throw default_exception("BUG: UF function entries disagree with each other");
}
}

6
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -3093,8 +3093,10 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int();
unsigned sbits = f->get_domain()[0]->get_parameter(1).get_int();
if (m_hi_fp_unspecified)
mk_nan(f->get_range(), result);
if (m_hi_fp_unspecified) {
mk_nan(f->get_domain()[0], result);
join_fp(result, result);
}
else {
expr * n = args[0];
expr_ref n_bv(m);

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -843,6 +843,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
continue;
if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) == arg_v)
continue;
if (m().is_ite(arg))
continue;
// found target for rewriting
break;
}

2
src/ast/rewriter/poly_rewriter_def.h
View file

@ -687,7 +687,7 @@ br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args,
}
set_curr_sort(m().get_sort(args[0]));
expr_ref minus_one(mk_numeral(numeral(-1)), m());
ptr_buffer<expr> new_args;
expr_ref_buffer new_args(m());
new_args.push_back(args[0]);
for (unsigned i = 1; i < num_args; i++) {
if (is_zero(args[i])) continue;

1
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1645,6 +1645,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
ls.swap(rs);
std::swap(head1, head2);
}
if (l == r) {
++head1;

2
src/interp/iz3interp.cpp
View file

@ -550,7 +550,7 @@ void interpolation_options_struct::apply(iz3base &b){
// On linux and mac, unlimit stack space so we get recursion
#if defined(_WINDOWS) || defined(_CYGWIN)
#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW)
#else

2
src/interp/iz3translate.cpp
View file

@ -155,7 +155,7 @@ public:
return res;
}
void scan_skolems(const ast &proof){
void scan_skolems(const ast &proof) {
hash_map<ast,int> memo;
scan_skolems_rec(memo,proof, INT_MAX);
}

19
src/muz/base/dl_util.cpp
View file

@ -277,16 +277,21 @@ namespace datalog {
return get_max_var(has_var);
}
void del_rule(horn_subsume_model_converter* mc, rule& r) {
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) {
if (mc) {
ast_manager& m = mc->get_manager();
expr_ref_vector body(m);
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i)));
}
else {
body.push_back(r.get_tail(i));
if (unreachable) {
body.push_back(m.mk_false());
}
else {
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i)));
}
else {
body.push_back(r.get_tail(i));
}
}
}
TRACE("dl_dr",

2
src/muz/base/dl_util.h
View file

@ -354,7 +354,7 @@ namespace datalog {
unsigned get_max_rule_var(const rule& r);
};
void del_rule(horn_subsume_model_converter* mc, rule& r);
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable);
void resolve_rule(rule_manager& rm,
replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,

26
src/muz/pdr/pdr_context.cpp
View file

@ -149,30 +149,27 @@ namespace pdr {
}
datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
TRACE("pdr_verbose",
datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
for (; it != end; ++it) {
expr* pred = it->m_key;
for (auto const& kv : m_tag2rule) {
expr* pred = kv.m_key;
tout << mk_pp(pred, m) << ":\n";
if (it->m_value) rm.display_smt2(*it->m_value, tout) << "\n";
if (kv.m_value) rm.display_smt2(*kv.m_value, tout) << "\n";
}
);
it = m_tag2rule.begin();
if (m_tag2rule.size() == 1) {
return *it->m_value;
return *m_tag2rule.begin()->m_value;
}
expr_ref vl(m);
for (; it != end; ++it) {
expr* pred = it->m_key;
for (auto const& kv : m_tag2rule) {
expr* pred = kv.m_key;
if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) {
return *it->m_value;
return *kv.m_value;
}
}
UNREACHABLE();
return *((datalog::rule*)0);
throw default_exception("could not find rule");
}
void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& preds) const {
@ -201,7 +198,7 @@ namespace pdr {
void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) {
goal_ref g(alloc(goal, m, false, false, false));
for (unsigned j = 0; j < v.size(); ++j) g->assert_expr(v[j].get());
for (expr* e : v) g->assert_expr(e);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
@ -216,9 +213,8 @@ namespace pdr {
void pred_transformer::simplify_formulas() {
tactic_ref us = mk_unit_subsumption_tactic(m);
simplify_formulas(*us, m_invariants);
for (unsigned i = 0; i < m_levels.size(); ++i) {
simplify_formulas(*us, m_levels[i]);
}
for (auto & fmls : m_levels)
simplify_formulas(*us, fmls);
}
expr_ref pred_transformer::get_formulas(unsigned level, bool add_axioms) {

3
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -607,6 +607,9 @@ namespace datalog {
rule_set * res = alloc(rule_set, m_context);
if (transform_rules(source, *res)) {
res->inherit_predicates(source);
TRACE("dl",
source.display(tout);
res->display(tout););
} else {
dealloc(res);
res = 0;

16
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -426,7 +426,7 @@ namespace datalog {
for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
rule* r = m_inlined_rules.get_rule(i);
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, true);
}
}
@ -465,7 +465,7 @@ namespace datalog {
}
}
if (modified) {
datalog::del_rule(m_mc, *r0);
datalog::del_rule(m_mc, *r0, true);
}
return modified;
@ -488,9 +488,9 @@ namespace datalog {
}
if (something_done && m_mc) {
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
if (inlining_allowed(orig, (*rit)->get_decl())) {
datalog::del_rule(m_mc, **rit);
for (rule* r : orig) {
if (inlining_allowed(orig, r->get_decl())) {
datalog::del_rule(m_mc, *r, true);
}
}
}
@ -580,7 +580,7 @@ namespace datalog {
// nothing unifies with the tail atom, therefore the rule is unsatisfiable
// (we can say this because relation pred doesn't have any ground facts either)
res = 0;
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, false);
return true;
}
if (!is_oriented_rewriter(inlining_candidate, strat)) {
@ -590,7 +590,7 @@ namespace datalog {
goto process_next_tail;
}
if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, false);
res = 0;
}
return true;
@ -823,7 +823,7 @@ namespace datalog {
if (num_tail_unifiers == 1) {
TRACE("dl", tout << "setting invalid: " << j << "\n";);
valid.set(j, false);
datalog::del_rule(m_mc, *r2);
datalog::del_rule(m_mc, *r2, true);
del_rule(r2, j);
}

27
src/muz/transforms/dl_mk_slice.cpp
View file

@ -426,8 +426,8 @@ namespace datalog {
bool change = true;
while (change) {
change = false;
for (unsigned i = 0; i < src.get_num_rules(); ++i) {
change = prune_rule(*src.get_rule(i)) || change;
for (rule* r : src) {
change = prune_rule(*r) || change;
}
}
}
@ -457,18 +457,19 @@ namespace datalog {
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) {
expr* e = conjs[j].get();
for (expr * e : conjs) {
expr_ref r(m);
unsigned v;
if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
add_var(v);
if (!m_solved_vars[v].get()) {
TRACE("dl", tout << v << " is solved\n";);
add_free_vars(parameter_vars, r);
m_solved_vars[v] = r;
}
else {
TRACE("dl", tout << v << " is used\n";);
// variables can only be solved once.
add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get());
@ -508,10 +509,9 @@ namespace datalog {
//
uint_set used_vars, parameter_vars;
solve_vars(r, used_vars, parameter_vars);
uint_set::iterator it = used_vars.begin(), end = used_vars.end();
for (; it != end; ++it) {
if (*it < m_var_is_sliceable.size()) {
m_var_is_sliceable[*it] = false;
for (unsigned uv : used_vars) {
if (uv < m_var_is_sliceable.size()) {
m_var_is_sliceable[uv] = false;
}
}
//
@ -533,6 +533,9 @@ namespace datalog {
if (m_solved_vars[i].get()) {
m_var_is_sliceable[i] = false;
}
if (parameter_vars.contains(i)) {
m_var_is_sliceable[i] = false;
}
}
else if (is_output) {
if (parameter_vars.contains(i)) {
@ -687,11 +690,9 @@ namespace datalog {
}
void mk_slice::display(std::ostream& out) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin();
obj_map<func_decl, bit_vector>::iterator end = m_sliceable.end();
for (; it != end; ++it) {
out << it->m_key->get_name() << " ";
bit_vector const& bv = it->m_value;
for (auto const& kv : m_sliceable) {
out << kv.m_key->get_name() << " ";
bit_vector const& bv = kv.m_value;
for (unsigned i = 0; i < bv.size(); ++i) {
out << (bv.get(i)?"1":"0");
}

53
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -24,8 +24,10 @@ Revision History:
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "muz/transforms/dl_mk_subsumption_checker.h"
#include "muz/base/fixedpoint_params.hpp"
#include "tactic/extension_model_converter.h"
namespace datalog {
@ -37,26 +39,28 @@ namespace datalog {
bool mk_subsumption_checker::is_total_rule(const rule * r) {
if(r->get_tail_size()!=0) { return false; }
if (r->get_tail_size() != 0) {
return false;
}
unsigned pt_len = r->get_positive_tail_size();
if(pt_len!=r->get_uninterpreted_tail_size()) {
//we dont' expect rules with negative tails to be total
if(pt_len != r->get_uninterpreted_tail_size()) {
// we dont' expect rules with negative tails to be total
return false;
}
for(unsigned i=0; i<pt_len; i++) {
for (unsigned i = 0; i < pt_len; i++) {
func_decl * tail_pred = r->get_tail(i)->get_decl();
if(!m_total_relations.contains(tail_pred)) {
//this rule has a non-total predicate in the tail
if (!m_total_relations.contains(tail_pred)) {
// this rule has a non-total predicate in the tail
return false;
}
}
unsigned t_len = r->get_positive_tail_size();
for(unsigned i=pt_len; i<t_len; i++) {
for(unsigned i = pt_len; i < t_len; i++) {
SASSERT(!r->is_neg_tail(i)); //we assume interpreted tail not to be negated
if(!m.is_true(r->get_tail(i))) {
if (!m.is_true(r->get_tail(i))) {
//this rule has an interpreted tail which is not constant true
return false;
}
@ -183,20 +187,15 @@ namespace datalog {
rule_ref_vector orig_rules(m_context.get_rule_manager());
orig_rules.append(orig.get_num_rules(), orig.begin());
rule * * rbegin = orig_rules.c_ptr();
rule * * rend = rbegin + orig_rules.size();
//before traversing we sort rules so that the shortest are in the beginning.
//this will help make subsumption checks more efficient
std::sort(rbegin, rend, rule_size_comparator);
std::sort(orig_rules.c_ptr(), orig_rules.c_ptr() + orig_rules.size(), rule_size_comparator);
for(rule_set::iterator rit = rbegin; rit!=rend; ++rit) {
rule * r = *rit;
for (rule * r : orig_rules) {
func_decl * head_pred = r->get_decl();
if(m_total_relations.contains(head_pred)) {
if(!orig.is_output_predicate(head_pred) ||
if (m_total_relations.contains(head_pred)) {
if (!orig.is_output_predicate(head_pred) ||
total_relations_with_included_rules.contains(head_pred)) {
//We just skip definitions of total non-output relations as
//we'll eliminate them from the problem.
@ -205,8 +204,7 @@ namespace datalog {
modified = true;
continue;
}
rule * defining_rule;
VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
rule * defining_rule = m_total_relation_defining_rules.find(head_pred);
if (defining_rule) {
rule_ref totality_rule(m_context.get_rule_manager());
VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
@ -224,24 +222,31 @@ namespace datalog {
}
rule_ref new_rule(m_context.get_rule_manager());
if(!transform_rule(r, subs_index, new_rule)) {
if (!transform_rule(r, subs_index, new_rule)) {
modified = true;
continue;
}
if(m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
if (m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
on_discovered_total_relation(head_pred, new_rule.get());
}
if(subs_index.is_subsumed(new_rule)) {
if (subs_index.is_subsumed(new_rule)) {
modified = true;
continue;
}
if(new_rule.get()!=r) {
if (new_rule.get()!=r) {
modified = true;
}
tgt.add_rule(new_rule);
subs_index.add(new_rule);
}
tgt.inherit_predicates(orig);
if (!m_total_relations.empty() && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (func_decl* p : m_total_relations) {
mc0->insert(p, m.mk_true());
}
m_context.add_model_converter(mc0);
}
TRACE("dl",
tout << "original set size: "<<orig.get_num_rules()<<"\n"
<< "reduced set size: "<<tgt.get_num_rules()<<"\n"; );

31
src/qe/qe_lite.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include "qe/qe_lite.h"
#include "ast/expr_abstract.h"
#include "ast/used_vars.h"
#include "ast/occurs.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
@ -39,6 +38,30 @@ Revision History:
#include "qe/qe_vartest.h"
namespace eq {
bool occurs_var(unsigned idx, expr* e) {
ptr_buffer<expr> todo;
todo.push_back(e);
ast_mark mark;
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (mark.is_marked(e)) continue;
mark.mark(e, true);
if (is_var(e)) {
if (to_var(e)->get_idx() == idx) return true;
}
else if (is_app(e)) {
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
if (occurs_var(idx + q->get_num_decls(), q->get_expr())) return true;
}
}
return false;
}
class der {
ast_manager & m;
arith_util a;
@ -65,7 +88,7 @@ namespace eq {
for (unsigned i = 0; i < definitions.size(); i++) {
var * v = vars[i];
expr * t = definitions[i];
if (t == 0 || has_quantifiers(t) || occurs(v, t))
if (t == 0 || has_quantifiers(t) || occurs_var(v->get_idx(), t))
definitions[i] = 0;
else
found = true; // found at least one candidate
@ -679,9 +702,9 @@ namespace eq {
}
bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
bool occ = occurs(x, t);
bool occ = occurs_var(x->get_idx(), t);
for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
occ = (i != j) && occurs(x, conjs[j]);
occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
}
return !occ;
}

5
src/qe/qsat.cpp
View file

@ -626,6 +626,9 @@ namespace qe {
SASSERT(validate_assumptions(*m_model.get(), asms));
SASSERT(validate_model(asms));
TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
if (m_level == 0) {
m_model_save = m_model;
}
push();
if (m_level == 1 && m_mode == qsat_maximize) {
maximize_model();
@ -1274,7 +1277,7 @@ namespace qe {
in->inc_depth();
result.push_back(in.get());
if (in->models_enabled()) {
mc = model2model_converter(m_model.get());
mc = model2model_converter(m_model_save.get());
mc = concat(m_pred_abs.fmc(), mc.get());
}
break;

10
src/smt/smt_b_justification.h
View file

@ -93,6 +93,16 @@ namespace smt {
const b_justification null_b_justification(static_cast<clause*>(0));
inline std::ostream& operator<<(std::ostream& out, b_justification::kind k) {
switch (k) {
case b_justification::CLAUSE: return out << "clause";
case b_justification::BIN_CLAUSE: return out << "bin_clause";
case b_justification::AXIOM: return out << "axiom";
case b_justification::JUSTIFICATION: return out << "theory";
}
return out;
}
typedef std::pair<literal, b_justification> justified_literal;
};

92
src/smt/smt_conflict_resolution.cpp
View file

@ -257,10 +257,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
r = std::max(r, m_ctx.get_assign_level(*it));
for (literal lit : antecedents)
r = std::max(r, m_ctx.get_assign_level(lit));
return r;
}
@ -315,8 +313,8 @@ namespace smt {
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
m_ctx.set_mark(var);
m_ctx.inc_bvar_activity(var);
@ -330,11 +328,11 @@ namespace smt {
if (get_manager().has_trace_stream()) {
get_manager().trace_stream() << "[resolve-lit] " << m_conflict_lvl - lvl << " ";
m_ctx.display_literal(get_manager().trace_stream(), ~antecedent);
get_manager().trace_stream() << "\n";
m_ctx.display_literal(get_manager().trace_stream(), ~antecedent) << "\n";
}
if (lvl == m_conflict_lvl) {
TRACE("conflict", m_ctx.display_literal(tout << "marking:", antecedent) << "\n";);
num_marks++;
}
else {
@ -392,7 +390,7 @@ namespace smt {
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
tout << "js.kind: " << js.get_kind() << "\n";
tout << "consequent: " << consequent << ": ";
m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
m_ctx.display_literal_verbose(tout, consequent) << "\n";
m_ctx.display(tout, js); tout << "\n";
);
@ -431,32 +429,16 @@ namespace smt {
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict",
tout << "before minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";);
TRACE("conflict_verbose",
tout << "before minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";);
if (m_params.m_minimize_lemmas)
minimize_lemma();
TRACE("conflict",
tout << "after minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",
tout << "after minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict_bug",
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "after minimization:\n", m_lemma) << "\n";);
TRACE("conflict_verbose", m_ctx.display_literals_verbose(tout << "after minimization:\n", m_lemma) << "\n";);
TRACE("conflict_bug", m_ctx.display_literals_verbose(tout, m_lemma) << "\n";);
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
@ -514,7 +496,8 @@ namespace smt {
get_manager().trace_stream() << "\n";
}
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent);
m_ctx.display_literal_verbose(tout, consequent) << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);
@ -566,8 +549,10 @@ namespace smt {
if (m_ctx.is_marked(l.var()))
break;
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";);
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: ";
tout << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";
tout << "num marks: " << num_marks << "\n";);
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
// it may also be an (out-of-order) asserted literal
m_ctx.get_assign_level(l) == m_ctx.get_base_level());
@ -606,10 +591,8 @@ namespace smt {
*/
level_approx_set conflict_resolution::get_lemma_approx_level_set() {
level_approx_set result;
literal_vector::const_iterator it = m_lemma.begin();
literal_vector::const_iterator end = m_lemma.end();
for(; it != end; ++it)
result.insert(m_ctx.get_assign_level(*it));
for (literal l : m_lemma)
result.insert(m_ctx.get_assign_level(l));
return result;
}
@ -660,10 +643,8 @@ namespace smt {
// The method unmark_justifications must be invoked to reset these caches.
// Remark: The method reset_unmark_and_justifications invokes unmark_justifications.
justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
if (!process_antecedent_for_minimization(*it))
for (literal l : antecedents)
if (!process_antecedent_for_minimization(l))
return false;
return true;
}
@ -1063,10 +1044,8 @@ namespace smt {
m_eq2proof.reset();
m_lit2proof.reset();
m_js2proof.reset();
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it)
m_ctx.set_mark((*it).var());
for (literal lit : m_lemma)
m_ctx.set_mark(lit.var());
}
bool conflict_resolution::visit_b_justification(literal l, b_justification js) {
@ -1246,12 +1225,9 @@ namespace smt {
SASSERT(conflict.get_kind() != b_justification::BIN_CLAUSE);
SASSERT(conflict.get_kind() != b_justification::AXIOM);
SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::JUSTIFICATION);
TRACE("mk_conflict_proof", tout << "lemma literals: ";
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it) {
m_ctx.display_literal(tout, *it);
tout << " ";
TRACE("mk_conflict_proof", tout << "lemma literals:";
for (literal lit : m_lemma) {
m_ctx.display_literal(tout << " ", lit);
}
tout << "\n";);
init_mk_proof();
@ -1328,12 +1304,10 @@ namespace smt {
pr = m_manager.mk_unit_resolution(2, prs);
}
expr_ref_buffer lits(m_manager);
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it) {
m_ctx.unset_mark((*it).var());
for (literal lit : m_lemma) {
m_ctx.unset_mark(lit.var());
expr_ref l_expr(m_manager);
m_ctx.literal2expr(*it, l_expr);
m_ctx.literal2expr(lit, l_expr);
lits.push_back(l_expr);
}
expr * fact = 0;
@ -1369,10 +1343,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
process_antecedent_for_unsat_core(*it);
for (literal lit : antecedents)
process_antecedent_for_unsat_core(lit);
}
void conflict_resolution::mk_unsat_core(b_justification conflict, literal not_l) {

56
src/smt/smt_context.cpp
View file

@ -285,7 +285,6 @@ namespace smt {
d.set_justification(j);
}
void context::assign_core(literal l, b_justification j, bool decision) {
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
@ -902,7 +901,7 @@ namespace smt {
}
/**
\brief Propabate the boolean assignment when two equivalence classes are merged.
\brief Propagate the boolean assignment when two equivalence classes are merged.
*/
void context::propagate_bool_enode_assignment(enode * r1, enode * r2, enode * n1, enode * n2) {
SASSERT(n1->is_bool());
@ -1615,11 +1614,9 @@ namespace smt {
\brief Return set of assigned literals as expressions.
*/
void context::get_assignments(expr_ref_vector& assignments) {
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
for (literal lit : m_assigned_literals) {
expr_ref e(m_manager);
literal2expr(*it, e);
literal2expr(lit, e);
assignments.push_back(e);
}
}
@ -1694,10 +1691,8 @@ namespace smt {
}
bool context::propagate_theories() {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->propagate();
for (theory * t : m_theory_set) {
t->propagate();
if (inconsistent())
return false;
}
@ -1733,10 +1728,8 @@ namespace smt {
}
bool context::can_theories_propagate() const {
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
if ((*it)->can_propagate()) {
for (theory* t : m_theory_set) {
if (t->can_propagate()) {
return true;
}
}
@ -1821,7 +1814,7 @@ namespace smt {
}
void context::rescale_bool_var_activity() {
TRACE("case_split", tout << "rescale\n";);
TRACE("case_split", tout << "rescale\n";);
svector<double>::iterator it = m_activity.begin();
svector<double>::iterator end = m_activity.end();
for (; it != end; ++it)
@ -1968,10 +1961,8 @@ namespace smt {
m_case_split_queue->push_scope();
m_asserted_formulas.push_scope();
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->push_scope_eh();
for (theory* t : m_theory_set)
t->push_scope_eh();
CASSERT("context", check_invariant());
}
@ -2146,10 +2137,7 @@ namespace smt {
}
for (unsigned i = new_scope_lvl; i <= lim; i++) {
clause_vector & v = m_clauses_to_reinit[i];
clause_vector::iterator it = v.begin();
clause_vector::iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause* cls : v) {
cache_generation(cls, new_scope_lvl);
}
}
@ -2246,10 +2234,7 @@ namespace smt {
}
for (unsigned i = m_scope_lvl+1; i <= lim; i++) {
clause_vector & v = m_clauses_to_reinit[i];
clause_vector::iterator it = v.begin();
clause_vector::iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause* cls : v) {
if (cls->deleted()) {
cls->release_atoms(m_manager);
cls->m_reinit = false;
@ -2922,10 +2907,8 @@ namespace smt {
TRACE("flush", tout << "m_scope_lvl: " << m_scope_lvl << "\n";);
m_relevancy_propagator = 0;
m_model_generator->reset();
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->flush_eh();
for (theory* t : m_theory_set)
t->flush_eh();
undo_trail_stack(0);
m_qmanager = 0;
del_clauses(m_aux_clauses, 0);
@ -3183,10 +3166,8 @@ namespace smt {
}
void context::reset_assumptions() {
literal_vector::iterator it = m_assumptions.begin();
literal_vector::iterator end = m_assumptions.end();
for (; it != end; ++it)
get_bdata(it->var()).m_assumption = false;
for (literal lit : m_assumptions)
get_bdata(lit.var()).m_assumption = false;
m_assumptions.reset();
}
@ -4373,7 +4354,7 @@ namespace smt {
void context::add_rec_funs_to_model() {
ast_manager& m = m_manager;
SASSERT(m_model);
for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
expr* e = m_asserted_formulas.get_formula(i);
if (is_quantifier(e)) {
TRACE("context", tout << mk_pp(e, m) << "\n";);
@ -4385,8 +4366,9 @@ namespace smt {
SASSERT(is_app(fn));
// reverse argument order so that variable 0 starts at the beginning.
expr_ref_vector subst(m);
unsigned idx = 0;
for (expr* arg : *to_app(fn)) {
subst.push_back(arg);
subst.push_back(m.mk_var(idx++, m.get_sort(arg)));
}
expr_ref bodyr(m);
var_subst sub(m, true);

27
src/smt/smt_context.h
View file

@ -209,7 +209,12 @@ namespace smt {
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.add_rec_funs_to_model();
try {
m_ctx.add_rec_funs_to_model();
}
catch (...) {
// no op
}
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}
@ -1230,24 +1235,24 @@ namespace smt {
void display_asserted_formulas(std::ostream & out) const;
void display_literal(std::ostream & out, literal l) const;
std::ostream& display_literal(std::ostream & out, literal l) const;
void display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); }
std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); return out; }
void display_literal_info(std::ostream & out, literal l) const;
void display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const;
std::ostream& display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const;
void display_literals(std::ostream & out, literal_vector const& lits) const {
display_literals(out, lits.size(), lits.c_ptr());
std::ostream& display_literals(std::ostream & out, literal_vector const& lits) const {
return display_literals(out, lits.size(), lits.c_ptr());
}
void display_literal_verbose(std::ostream & out, literal lit) const;
std::ostream& display_literal_verbose(std::ostream & out, literal lit) const;
void display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
void display_literals_verbose(std::ostream & out, literal_vector const& lits) const {
display_literals_verbose(out, lits.size(), lits.c_ptr());
std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
std::ostream& display_literals_verbose(std::ostream & out, literal_vector const& lits) const {
return display_literals_verbose(out, lits.size(), lits.c_ptr());
}
void display_watch_list(std::ostream & out, literal l) const;

60
src/smt/smt_context_pp.cpp
View file

@ -71,11 +71,9 @@ namespace smt {
case NUM_CONFLICTS: r = "max-conflicts-reached"; break;
case THEORY: {
r = "(incomplete (theory";
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
for (; it != end; ++it) {
for (theory* t : m_incomplete_theories) {
r += " ";
r += (*it)->get_name();
r += t->get_name();
}
r += "))";
break;
@ -91,20 +89,20 @@ namespace smt {
m_asserted_formulas.display_ll(out, get_pp_visited());
}
void context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr());
std::ostream& context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr()); return out;
}
void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_compact(out, num_lits, lits, m_bool_var2expr.c_ptr());
std::ostream& context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_compact(out, num_lits, lits, m_bool_var2expr.c_ptr()); return out;
}
void context::display_literal_verbose(std::ostream & out, literal lit) const {
display_literals_verbose(out, 1, &lit);
std::ostream& context::display_literal_verbose(std::ostream & out, literal lit) const {
return display_literals_verbose(out, 1, &lit);
}
void context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n");
std::ostream& context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n"); return out;
}
void context::display_literal_info(std::ostream & out, literal l) const {
@ -136,10 +134,8 @@ namespace smt {
}
void context::display_enode_defs(std::ostream & out) const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
for (enode * x : m_enodes) {
expr * n = x->get_owner();
ast_def_ll_pp(out, m_manager, n, get_pp_visited(), true, false);
}
}
@ -169,10 +165,8 @@ namespace smt {
}
void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
ptr_vector<clause>::const_iterator it = v.begin();
ptr_vector<clause>::const_iterator end = v.end();
for (; it != end; ++it) {
display_clause(out, *it);
for (clause* cp : v) {
display_clause(out, cp);
out << "\n";
}
}
@ -207,12 +201,10 @@ namespace smt {
void context::display_assignment(std::ostream & out) const {
if (!m_assigned_literals.empty()) {
out << "current assignment:\n";
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
display_literal(out, *it);
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
out << ": ";
display_verbose(out, m_manager, 1, &*it, m_bool_var2expr.c_ptr());
display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";
}
}
@ -223,11 +215,9 @@ namespace smt {
pp.set_benchmark_name("lemma");
pp.set_status("unknown");
pp.set_logic(logic);
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
for (literal lit : m_assigned_literals) {
expr_ref n(m_manager);
literal2expr(*it, n);
literal2expr(lit, n);
pp.add_assumption(n);
}
pp.display_smt2(out, m_manager.mk_true());
@ -235,11 +225,9 @@ namespace smt {
void context::display_eqc(std::ostream & out) const {
bool first = true;
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
expr * r = (*it)->get_root()->get_owner();
for (enode * x : m_enodes) {
expr * n = x->get_owner();
expr * r = x->get_root()->get_owner();
if (n != r) {
if (first) {
out << "equivalence classes:\n";
@ -610,10 +598,10 @@ namespace smt {
break;
}
case b_justification::JUSTIFICATION: {
out << "justification ";
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits.size(), lits.c_ptr());
display_literals(out, lits);
break;
}
default:

5
src/smt/smt_model_checker.cpp
View file

@ -32,6 +32,7 @@ namespace smt {
model_checker::model_checker(ast_manager & m, qi_params const & p, model_finder & mf):
m(m),
m_params(p),
m_autil(m),
m_qm(0),
m_context(0),
m_root2value(0),
@ -205,13 +206,13 @@ namespace smt {
}
void model_checker::operator()(expr *n) {
if (m.is_model_value(n)) {
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
throw is_model_value();
}
}
bool model_checker::contains_model_value(expr* n) {
if (m.is_model_value(n)) {
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
return true;
}
if (is_app(n) && to_app(n)->get_num_args() == 0) {

2
src/smt/smt_model_checker.h
View file

@ -22,6 +22,7 @@ Revision History:
#define SMT_MODEL_CHECKER_H_
#include "ast/ast.h"
#include "ast/array_decl_plugin.h"
#include "util/obj_hashtable.h"
#include "smt/params/qi_params.h"
#include "smt/params/smt_params.h"
@ -39,6 +40,7 @@ namespace smt {
class model_checker {
ast_manager & m; // _manager;
qi_params const & m_params;
array_util m_autil;
// copy of smt_params for auxiliary context.
// the idea is to use a different configuration for the aux context (e.g., disable relevancy)
scoped_ptr<smt_params> m_fparams;

8
src/smt/smt_model_finder.cpp
View file

@ -643,12 +643,8 @@ namespace smt {
return t_result;
}
bool is_infinite(sort * s) const {
// we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
return
!m.is_uninterp(s) &&
s->is_infinite();
}
// we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
bool is_infinite(sort * s) const { return !m.is_uninterp(s) && s->is_infinite(); }
/**
\brief Return a fresh constant k that is used as a witness for elements that must be different from

11
src/smt/smt_quantifier.cpp
View file

@ -127,10 +127,8 @@ namespace smt {
out << " #" << bindings[i]->get_owner_id();
}
out << " ;";
ptr_vector<enode>::const_iterator it = used_enodes.begin();
ptr_vector<enode>::const_iterator end = used_enodes.end();
for (; it != end; ++it)
out << " #" << (*it)->get_owner_id();
for (enode* n : used_enodes)
out << " #" << n->get_owner_id();
out << "\n";
}
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@ -150,10 +148,7 @@ namespace smt {
void init_search_eh() {
m_num_instances = 0;
ptr_vector<quantifier>::iterator it2 = m_quantifiers.begin();
ptr_vector<quantifier>::iterator end2 = m_quantifiers.end();
for (; it2 != end2; ++it2) {
quantifier * q = *it2;
for (quantifier * q : m_quantifiers) {
get_stat(q)->reset_num_instances_curr_search();
}
m_qi_queue.init_search_eh();

2
src/smt/theory_arith.h
View file

@ -603,7 +603,7 @@ namespace smt {
void internalize_is_int(app * n);
theory_var internalize_numeral(app * n);
theory_var internalize_term_core(app * n);
void mk_axiom(expr * n1, expr * n2);
void mk_axiom(expr * n1, expr * n2, bool simplify_conseq = true);
void mk_idiv_mod_axioms(expr * dividend, expr * divisor);
void mk_div_axiom(expr * dividend, expr * divisor);
void mk_rem_axiom(expr * dividend, expr * divisor);

33
src/smt/theory_arith_core.h
View file

@ -443,7 +443,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq) {
void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq, bool simplify_conseq) {
ast_manager & m = get_manager();
context & ctx = get_context();
th_rewriter & s = ctx.get_rewriter();
@ -459,7 +459,8 @@ namespace smt {
literal l_ante = ctx.get_literal(s_ante);
if (negated) l_ante.neg();
s(conseq, s_conseq);
s_conseq = conseq;
if (simplify_conseq) s(conseq, s_conseq);
if (ctx.get_cancel_flag()) return;
negated = m.is_not(s_conseq, s_conseq_n);
if (negated) s_conseq = s_conseq_n;
@ -507,26 +508,30 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
if (!m_util.is_zero(divisor)) {
// if divisor is zero, then idiv and mod are uninterpreted functions.
ast_manager & m = get_manager();
expr_ref div(m), mod(m), zero(m), abs_divisor(m);
bool is_numeral = m_util.is_numeral(divisor);
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
th_rewriter & s = get_context().get_rewriter();
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_numeral(rational(0), true);
abs_divisor = m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor);
zero = m_util.mk_int(0);
one = m_util.mk_int(1);
abs_divisor = m_util.mk_sub(m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor), one);
s(abs_divisor);
eqz = m.mk_eq(divisor, zero);
eq = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
lower = m_util.mk_le(zero, mod);
upper = m_util.mk_lt(mod, abs_divisor);
lower = m_util.mk_ge(mod, zero);
upper = m_util.mk_le(mod, abs_divisor);
TRACE("div_axiom_bug",
tout << "eqz: " << mk_pp(eqz, m) << "\neq: " << mk_pp(eq, m) << "\n";
tout << "lower: " << mk_pp(lower, m) << "\n";
tout << "upper: " << mk_pp(upper, m) << "\n";);
tout << "eqz: " << eqz << " neq: " << eq << "\n";
tout << "lower: " << lower << "\n";
tout << "upper: " << upper << "\n";);
mk_axiom(eqz, eq);
mk_axiom(eqz, lower);
mk_axiom(eqz, upper);
mk_axiom(eqz, eq, !is_numeral);
mk_axiom(eqz, lower, !is_numeral);
mk_axiom(eqz, upper, !is_numeral);
rational k;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) {

190
src/smt/theory_seq.cpp
View file

@ -1228,18 +1228,25 @@ bool theory_seq::is_solved() {
return true;
}
void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
/**
\brief while extracting dependency literals ensure that they have all been asserted on the context.
*/
bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
context & ctx = get_context();
DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); );
bool asserted = true;
svector<assumption> assumptions;
const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
for (unsigned i = 0; i < assumptions.size(); ++i) {
assumption const& a = assumptions[i];
for (assumption const& a : assumptions) {
if (a.lit != null_literal) {
lits.push_back(a.lit);
asserted &= ctx.get_assignment(a.lit) == l_true;
}
if (a.n1 != 0) {
eqs.push_back(enode_pair(a.n1, a.n2));
}
}
return asserted;
}
@ -1257,7 +1264,8 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
ctx.mark_as_relevant(lit);
enode_pair_vector eqs;
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq",
tout << "assert:";
ctx.display_detailed_literal(tout, lit);
@ -1276,7 +1284,8 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
context& ctx = get_context();
enode_pair_vector eqs;
literal_vector lits(_lits);
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq", display_deps(tout << "assert conflict:", lits, eqs););
m_new_propagation = true;
ctx.set_conflict(
@ -1292,7 +1301,8 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
context& ctx = get_context();
literal_vector lits;
enode_pair_vector eqs;
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq",
tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
display_deps(tout, dep);
@ -1756,10 +1766,10 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
literal li_ge_ls = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal _lits[4] = { i_ge_0, i_lt_len_s, li_ge_ls, l_ge_zero };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true &&
@ -1776,8 +1786,8 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
// has length 1 if 0 <= i < len(s)
expr_ref zero(m_autil.mk_int(0), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal _lits[2] = { i_ge_0, i_lt_len_s};
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
@ -1790,8 +1800,8 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
else if (is_pre(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal _lits[2] = { i_ge_0, i_lt_len_s };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
@ -1803,8 +1813,8 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
else if (is_post(e, s, l)) {
expr_ref zero(m_autil.mk_int(0), m);
literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
literal l_le_len_s = mk_literal(m_autil.mk_ge(mk_sub(m_util.str.mk_length(s), l), zero));
literal l_ge_0 = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(m_util.str.mk_length(s), l), zero));
literal _lits[2] = { l_ge_0, l_le_len_s };
if (ctx.get_assignment(l_ge_0) == l_true &&
ctx.get_assignment(l_le_len_s) == l_true) {
@ -1843,12 +1853,12 @@ bool theory_seq::solve_ne(unsigned idx) {
ne const& n = m_nqs[idx];
unsigned num_undef_lits = 0;
for (unsigned i = 0; i < n.lits().size(); ++i) {
switch (ctx.get_assignment(n.lits(i))) {
for (literal lit : n.lits()) {
switch (ctx.get_assignment(lit)) {
case l_false:
TRACE("seq", display_disequation(tout << "has false literal\n", n);
ctx.display_literal_verbose(tout, n.lits(i));
tout << "\n" << n.lits(i) << " " << ctx.is_relevant(n.lits(i)) << "\n";
ctx.display_literal_verbose(tout, lit);
tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
);
return true;
case l_true:
@ -1952,8 +1962,7 @@ bool theory_seq::solve_ne(unsigned idx) {
if (num_undef_lits == 1 && new_ls.empty()) {
literal_vector lits;
literal undef_lit = null_literal;
for (unsigned i = 0; i < new_lits.size(); ++i) {
literal lit = new_lits[i];
for (literal lit : new_lits) {
switch (ctx.get_assignment(lit)) {
case l_true:
lits.push_back(lit);
@ -1978,10 +1987,13 @@ bool theory_seq::solve_ne(unsigned idx) {
dependency* deps1 = 0;
if (explain_eq(n.l(), n.r(), deps1)) {
new_lits.reset();
new_lits.push_back(~mk_eq(n.l(), n.r(), false));
new_deps = deps1;
TRACE("seq", tout << "conflict explained\n";);
literal diseq = mk_eq(n.l(), n.r(), false);
if (ctx.get_assignment(diseq) == l_false) {
new_lits.reset();
new_lits.push_back(~diseq);
new_deps = deps1;
TRACE("seq", tout << "conflict explained\n";);
}
}
set_conflict(new_deps, new_lits);
SASSERT(m_new_propagation);
@ -2344,7 +2356,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
if (!get_num_value(e, val)) {
literal l = mk_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
TRACE("seq", tout << l << " " << ctx.get_assignment(l) << "\n";
ctx.display(tout););
@ -2388,6 +2400,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
num = m_autil.mk_add(nums.size(), nums.c_ptr());
ctx.get_rewriter()(num);
lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom;
m_new_propagation = true;
@ -2559,8 +2572,8 @@ void theory_seq::display_disequations(std::ostream& out) const {
}
void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
for (unsigned j = 0; j < e.lits().size(); ++j) {
out << e.lits(j) << " ";
for (literal lit : e.lits()) {
out << lit << " ";
}
if (e.lits().size() > 0) {
out << "\n";
@ -3027,6 +3040,8 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
enode* n1 = ctx.get_enode(num);
enode* n2 = ctx.get_enode(e1);
res = m_util.str.mk_string(symbol(val.to_string().c_str()));
#if 1
// TBD remove this: using roots is unsound for propagation.
if (n1->get_root() == n2->get_root()) {
result = res;
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
@ -3037,6 +3052,12 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
result = e;
}
#else
TRACE("seq", tout << "add axiom\n";);
add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false));
add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
result = e;
#endif
}
else {
result = e;
@ -3084,7 +3105,6 @@ void theory_seq::propagate() {
}
void theory_seq::enque_axiom(expr* e) {
TRACE("seq", tout << "add axioms for: " << mk_pp(e, m) << "\n";);
if (!m_axiom_set.contains(e)) {
m_axioms.push_back(e);
m_axiom_set.insert(e);
@ -3094,6 +3114,7 @@ void theory_seq::enque_axiom(expr* e) {
}
void theory_seq::deque_axiom(expr* n) {
TRACE("seq", tout << "deque: " << mk_pp(n, m) << "\n";);
if (m_util.str.is_length(n)) {
add_length_axiom(n);
}
@ -3139,11 +3160,24 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
}
/*
// index of s in t starting at offset.
[[str.indexof]](w, w2, i) is the smallest n such that for some some w1, w3
- w = w1w2w3
- i <= n = |w1|
if [[str.contains]](w, w2) = true, |w2| > 0 and i >= 0.
[[str.indexof]](w,w2,i) = -1 otherwise.
let i = Index(t, s, offset):
// index of s in t starting at offset.
offset >= len(t) => i = -1
|t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
|t| = 0 & |s| = 0 => indexof(t,s,offset) = 0
offset >= len(t) => |s| = 0 or i = -1
len(t) != 0 & !contains(t, s) => i = -1
@ -3173,32 +3207,45 @@ void theory_seq::add_indexof_axiom(expr* i) {
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal i_eq_m1 = mk_eq(i, minus_one, false);
add_axiom(cnt, i_eq_m1);
literal i_eq_0 = mk_eq(i, zero, false);
literal s_eq_empty = mk_eq_empty(s);
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), i_eq_m1);
literal t_eq_empty = mk_eq_empty(t);
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
// ~contains(t,s) => indexof(t,s,offset) = -1
add_axiom(cnt, i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
expr_ref x = mk_skolem(m_indexof_left, t, s);
expr_ref y = mk_skolem(m_indexof_right, t, s);
xsy = mk_concat(x, s, y);
expr_ref lenx(m_util.str.mk_length(x), m);
// |s| = 0 => indexof(t,s,0) = 0
// contains(t,s) & |s| != 0 => t = xsy & indexof(t,s,0) = |x|
add_axiom(~s_eq_empty, i_eq_0);
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
tightest_prefix(s, x);
}
else {
// offset >= len(t) => indexof(s, t, offset) = -1
// offset >= len(t) => |s| = 0 or indexof(t, s, offset) = -1
// offset > len(t) => indexof(t, s, offset) = -1
// offset = len(t) & |s| = 0 => indexof(t, s, offset) = offset
expr_ref len_t(m_util.str.mk_length(t), m);
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
add_axiom(~offset_ge_len, mk_eq(i, minus_one, false));
literal offset_ge_len = mk_simplified_literal(m_autil.mk_ge(m_autil.mk_sub(offset, len_t), zero));
literal offset_le_len = mk_simplified_literal(m_autil.mk_le(m_autil.mk_sub(offset, len_t), zero));
literal i_eq_offset = mk_eq(i, offset, false);
add_axiom(~offset_ge_len, s_eq_empty, i_eq_m1);
add_axiom(offset_le_len, i_eq_m1);
add_axiom(~offset_ge_len, ~offset_le_len, ~s_eq_empty, i_eq_offset);
expr_ref x = mk_skolem(m_indexof_left, t, s, offset);
expr_ref y = mk_skolem(m_indexof_right, t, s, offset);
expr_ref indexof0(m_util.str.mk_index(y, s, zero), m);
expr_ref offset_p_indexof0(m_autil.mk_add(offset, indexof0), m);
literal offset_ge_0 = mk_literal(m_autil.mk_ge(offset, zero));
literal offset_ge_0 = mk_simplified_literal(m_autil.mk_ge(offset, zero));
// 0 <= offset & offset < len(t) => t = xy
// 0 <= offset & offset < len(t) => len(x) = offset
@ -3211,10 +3258,10 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(~offset_ge_0, offset_ge_len,
~mk_eq(indexof0, minus_one, false), i_eq_m1);
add_axiom(~offset_ge_0, offset_ge_len,
~mk_literal(m_autil.mk_ge(indexof0, zero)),
~mk_simplified_literal(m_autil.mk_ge(indexof0, zero)),
mk_eq(offset_p_indexof0, i, false));
// offset < 0 => -1 = i
// offset < 0 => -1 = i
add_axiom(offset_ge_0, i_eq_m1);
}
}
@ -3557,11 +3604,19 @@ bool theory_seq::get_length(expr* e, rational& val) const {
let e = extract(s, i, l)
0 <= i <= |s| -> prefix(xe,s)
i is start index, l is length of substring starting at index.
i < 0 => e = ""
i >= |s| => e = ""
l <= 0 => e = ""
0 <= i < |s| & l > 0 => s = xey, |x| = i, |e| = min(l, |s|-i)
this translates to:
0 <= i <= |s| -> s = xey
0 <= i <= |s| -> len(x) = i
0 <= i <= |s| & 0 <= l <= |s| - i -> |e| = l
0 <= i <= |s| & |s| < l + i -> |e| = |s| - i
0 <= i <= |s| & l < 0 -> |e| = 0
i >= |s| => |e| = 0
i < 0 => |e| = 0
l <= 0 => |e| = 0
@ -3573,6 +3628,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
*/
void theory_seq::add_extract_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
expr* s = 0, *i = 0, *l = 0;
VERIFY(m_util.str.is_extract(e, s, i, l));
if (is_tail(s, i, l)) {
@ -3601,13 +3657,13 @@ void theory_seq::add_extract_axiom(expr* e) {
expr_ref xey = mk_concat(x, e, y);
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal ls_le_i = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero));
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
literal ls_le_0 = mk_literal(m_autil.mk_le(ls, zero));
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal ls_le_i = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
literal li_ge_ls = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_zero = mk_simplified_literal(m_autil.mk_le(l, zero));
literal ls_le_0 = mk_simplified_literal(m_autil.mk_le(ls, zero));
// add_axiom(~i_ge_0, ~ls_le_i, mk_literal(m_util.str.mk_prefix(xe, s)));
add_axiom(~i_ge_0, ~ls_le_i, mk_seq_eq(xey, s));
add_axiom(~i_ge_0, ~ls_le_i, mk_eq(lx, i, false));
add_axiom(~i_ge_0, ~ls_le_i, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false));
@ -3667,14 +3723,15 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
0 <= l <= len(s) => s = ey & l = len(e)
*/
void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
expr_ref le(m_util.str.mk_length(e), m);
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref ls_minus_l(mk_sub(ls, l), m);
expr_ref y(mk_skolem(m_post, s, ls_minus_l), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref ey = mk_concat(e, y);
literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero));
literal l_ge_0 = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(l, ls), zero));
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
@ -3689,8 +3746,8 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref xe = mk_concat(x, e);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_le_s = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero));
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));
add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx, false));
}
@ -3716,8 +3773,8 @@ void theory_seq::add_at_axiom(expr* e) {
expr_ref len_x(m_util.str.mk_length(x), m);
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
@ -3736,7 +3793,7 @@ void theory_seq::propagate_step(literal lit, expr* step) {
expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
VERIFY(is_step(step, s, idx, re, i, j, acc));
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
propagate_lit(0, 1, &lit, mk_literal(acc));
propagate_lit(0, 1, &lit, mk_simplified_literal(acc));
rational lo;
rational _idx;
if (lower_bound(s, lo) && lo.is_unsigned() && m_autil.is_numeral(idx, _idx) && lo >= _idx) {
@ -3773,6 +3830,12 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
propagate_eq(lit, s, conc, true);
}
literal theory_seq::mk_simplified_literal(expr * _e) {
expr_ref e(_e, m);
m_rewrite(e);
return mk_literal(e);
}
literal theory_seq::mk_literal(expr* _e) {
expr_ref e(_e, m);
context& ctx = get_context();
@ -3797,11 +3860,11 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
}
expr_ref_vector concats(m);
m_util.str.get_concat(e, concats);
for (unsigned i = 0; i < concats.size(); ++i) {
if (m_util.str.is_unit(concats[i].get())) {
for (expr* c : concats) {
if (m_util.str.is_unit(c)) {
return false_literal;
}
if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) {
if (m_util.str.is_string(c, s) && s.length() > 0) {
return false_literal;
}
}
@ -3822,7 +3885,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); }
TRACE("seq", ctx.display_literals_verbose(tout << "assert: ", lits); tout << "\n";);
TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits); tout << "\n";);
m_new_propagation = true;
++m_stats.m_add_axiom;
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
@ -3872,8 +3935,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
literal_vector lits(_lits);
enode_pair_vector eqs;
linearize(deps, eqs, lits);
if (!linearize(deps, eqs, lits))
return;
if (add_to_eqs) {
deps = mk_join(deps, _lits);
new_eq_eh(deps, n1, n2);

3
src/smt/theory_seq.h
View file

@ -431,7 +431,7 @@ namespace smt {
bool explain_empty(expr_ref_vector& es, dependency*& dep);
// asserting consequences
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
bool linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
void propagate_eq(dependency* dep, enode* n1, enode* n2);
@ -509,6 +509,7 @@ namespace smt {
expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_simplified_literal(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
literal mk_seq_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x);

61
src/smt/theory_str.cpp
View file

@ -47,6 +47,8 @@ namespace smt {
sLevel(0),
finalCheckProgressIndicator(false),
m_trail(m),
m_factory(nullptr),
m_unused_id(0),
m_delayed_axiom_setup_terms(m),
tmpStringVarCount(0),
tmpXorVarCount(0),
@ -61,8 +63,8 @@ namespace smt {
cacheHitCount(0),
cacheMissCount(0),
m_fresh_id(0),
m_find(*this),
m_trail_stack(*this)
m_trail_stack(*this),
m_find(*this)
{
initialize_charset();
}
@ -279,7 +281,7 @@ namespace smt {
} else {
theory_var v = theory::mk_var(n);
m_find.mk_var();
TRACE("str", tout << "new theory var v#" << v << std::endl;);
TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n);
return v;
@ -1075,13 +1077,14 @@ namespace smt {
void theory_str::instantiate_axiom_CharAt(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr* arg0, *arg1;
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("str", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
VERIFY(u.str.is_at(expr, arg0, arg1));
TRACE("str", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;);
@ -1090,28 +1093,20 @@ namespace smt {
expr_ref ts2(mk_str_var("ts2"), m);
expr_ref cond(m.mk_and(
m_autil.mk_ge(expr->get_arg(1), mk_int(0)),
// REWRITE for arithmetic theory:
// m_autil.mk_lt(expr->get_arg(1), mk_strlen(expr->get_arg(0)))
mk_not(m, m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0)))
), m);
m_autil.mk_ge(arg1, mk_int(0)),
m_autil.mk_lt(arg1, mk_strlen(arg0))), m);
expr_ref_vector and_item(m);
and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2))));
and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0)));
and_item.push_back(ctx.mk_eq_atom(arg0, mk_concat(ts0, mk_concat(ts1, ts2))));
and_item.push_back(ctx.mk_eq_atom(arg1, mk_strlen(ts0)));
and_item.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_int(1)));
expr_ref thenBranch(m.mk_and(and_item.size(), and_item.c_ptr()), m);
expr_ref thenBranch(::mk_and(and_item));
expr_ref elseBranch(ctx.mk_eq_atom(ts1, mk_string("")), m);
expr_ref axiom(m.mk_ite(cond, thenBranch, elseBranch), m);
expr_ref reductionVar(ctx.mk_eq_atom(expr, ts1), m);
SASSERT(axiom);
SASSERT(reductionVar);
expr_ref finalAxiom(m.mk_and(axiom, reductionVar), m);
SASSERT(finalAxiom);
get_context().get_rewriter()(finalAxiom);
assert_axiom(finalAxiom);
}
@ -1903,8 +1898,8 @@ namespace smt {
// support for user_smt_theory-style EQC handling
app * theory_str::get_ast(theory_var i) {
return get_enode(i)->get_owner();
app * theory_str::get_ast(theory_var v) {
return get_enode(v)->get_owner();
}
theory_var theory_str::get_var(expr * n) const {
@ -4648,14 +4643,20 @@ namespace smt {
// We only check m_find for a string constant.
expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
expr * curr = n;
do {
if (u.str.is_string(curr)) {
hasEqcValue = true;
return curr;
}
curr = get_eqc_next(curr);
} while (curr != n);
theory_var curr = get_var(n);
if (curr != null_theory_var) {
curr = m_find.find(curr);
theory_var first = curr;
do {
expr* a = get_ast(curr);
if (u.str.is_string(a)) {
hasEqcValue = true;
return a;
}
curr = m_find.next(curr);
}
while (curr != first && curr != null_theory_var);
}
hasEqcValue = false;
return n;
}
@ -10584,7 +10585,9 @@ namespace smt {
return alloc(expr_wrapper_proc, val);
} else {
TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**")));
std::ostringstream unused;
unused << "**UNUSED**" << (m_unused_id++);
return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
}
}

6
src/smt/theory_str.h
View file

@ -267,6 +267,10 @@ protected:
str_value_factory * m_factory;
// Unique identifier appended to unused variables to ensure that model construction
// does not introduce equalities when they weren't enforced.
unsigned m_unused_id;
// terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms;
@ -358,8 +362,8 @@ protected:
// cache mapping each string S to Length(S)
obj_map<expr, app*> length_ast_map;
th_union_find m_find;
th_trail_stack m_trail_stack;
th_union_find m_find;
theory_var get_var(expr * n) const;
expr * get_eqc_next(expr * n);
app * get_ast(theory_var i);

1
src/solver/solver_pool.cpp
View file

@ -143,7 +143,6 @@ public:
}
out << ")\n";
m_base->display(out, num_assumptions, assumptions);
bool first = true;
out << "(check-sat";
for (unsigned i = 0; i < num_assumptions; ++i) {
out << " " << mk_pp(assumptions[i], m);

4
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -95,13 +95,13 @@ class diff_neq_tactic : public tactic {
if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
var x = mk_var(lhs);
int _k = static_cast<int>(k.get_int64());
m_upper[x] = _k;
m_upper[x] = std::min(m_upper[x], _k);
}
else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) {
var x = mk_var(rhs);
int _k = static_cast<int>(k.get_int64());
m_lower[x] = _k;
m_lower[x] = std::max(m_lower[x], _k);
}
else {
throw_not_supported();

5
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -42,10 +42,7 @@ struct quasi_pb_probe : public probe {
bound_manager bm(g.m());
bm(g);
rational l, u; bool st;
bound_manager::iterator it = bm.begin();
bound_manager::iterator end = bm.end();
for (; it != end; ++it) {
expr * t = *it;
for (expr * t : bm) {
if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one()))
continue;
if (found_non_01)

66
src/util/checked_int64.h
View file

@ -116,58 +116,48 @@ public:
const checked_int64 operator--(int) { checked_int64 tmp(*this); --(*this); return tmp; }
checked_int64& operator+=(checked_int64 const& other) {
if (CHECK && m_value > 0 && other.m_value > 0 &&
(m_value > INT_MAX || other.m_value > INT_MAX)) {
rational r(r64(m_value) + r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
if (CHECK) {
uint64 x = static_cast<uint64>(m_value);
uint64 y = static_cast<uint64>(other.m_value);
int64 r = static_cast<int64>(x + y);
if (m_value > 0 && other.m_value > 0 && r <= 0) throw overflow_exception();
if (m_value < 0 && other.m_value < 0 && r >= 0) throw overflow_exception();
m_value = r;
}
if (CHECK && m_value < 0 && other.m_value < 0 &&
(m_value < INT_MIN || other.m_value < INT_MIN)) {
rational r(r64(m_value) + r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
else {
m_value += other.m_value;
}
m_value += other.m_value;
return *this;
}
checked_int64& operator-=(checked_int64 const& other) {
if (CHECK && m_value > 0 && other.m_value < 0 &&
(m_value > INT_MAX || other.m_value < INT_MIN)) {
rational r(r64(m_value) - r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
if (CHECK) {
uint64 x = static_cast<uint64>(m_value);
uint64 y = static_cast<uint64>(other.m_value);
int64 r = static_cast<int64>(x - y);
if (m_value > 0 && other.m_value < 0 && r <= 0) throw overflow_exception();
if (m_value < 0 && other.m_value > 0 && r >= 0) throw overflow_exception();
m_value = r;
}
if (CHECK && m_value < 0 && other.m_value > 0 &&
(m_value < INT_MIN || other.m_value > INT_MAX)) {
rational r(r64(m_value) - r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
else {
m_value -= other.m_value;
}
m_value -= other.m_value;
return *this;
}
checked_int64& operator*=(checked_int64 const& other) {
if (CHECK) {
rational r(r64(m_value) * r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
if (INT_MIN < m_value && m_value <= INT_MAX && INT_MIN < other.m_value && other.m_value <= INT_MAX) {
m_value *= other.m_value;
}
// TBD: could be tuned by using known techniques or 128-bit arithmetic.
else {
rational r(r64(m_value) * r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
}
m_value = r.get_int64();
}
else {
m_value *= other.m_value;

2
src/util/lp/lar_solver.h
View file

@ -1157,7 +1157,7 @@ public:
bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
#ifdef Z3DEBUG
lconstraint_kind kind;
lconstraint_kind kind = EQ; // initialize it just to avoid a warning
SASSERT(the_relations_are_of_same_type(explanation, kind));
SASSERT(the_left_sides_sum_to_zero(explanation));
mpq rs = sum_of_right_sides_of_explanation(explanation);

1
src/util/union_find.h
View file

@ -102,6 +102,7 @@ public:
unsigned find(unsigned v) const {
while (true) {
SASSERT(v < m_find.size());
unsigned new_v = m_find[v];
if (new_v == v)
return v;