diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index 2f8ee0dc5..b097126d3 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -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}" diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index ab4d32d39..a944f2c65 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -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', diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d44e8f416..b155fd7c2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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') diff --git a/scripts/update_api.py b/scripts/update_api.py index 67a1b8a33..45ea9be23 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -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) """ ) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 95bc0bef9..9a778d6e0 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -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); + } + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 23a7bd22e..4b5e9d04e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -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 _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); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 27711be81..914cee615 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3127,6 +3127,20 @@ namespace Microsoft.Z3 return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } + + /// + /// Create a bit-vector numeral. + /// + /// An array of bits representing the bit-vector. Least signficant bit is at position 0. + public BitVecNum MkBV(bool[] bits) + { + Contract.Ensures(Contract.Result() != 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 diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 9d0636425..29e5e869a 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -124,7 +124,7 @@ namespace Microsoft.Z3 /// /// Retrieve a lower bound for the objective handle. /// - public ArithExpr Lower + public Expr Lower { get { return opt.GetLower(handle); } } @@ -132,7 +132,7 @@ namespace Microsoft.Z3 /// /// Retrieve an upper bound for the objective handle. /// - public ArithExpr Upper + public Expr Upper { get { return opt.GetUpper(handle); } } @@ -140,7 +140,7 @@ namespace Microsoft.Z3 /// /// Retrieve the value of an objective. /// - public ArithExpr Value + public Expr Value { get { return Lower; } } @@ -148,7 +148,7 @@ namespace Microsoft.Z3 /// /// Retrieve a lower bound for the objective handle. /// - public ArithExpr[] LowerAsVector + public Expr[] LowerAsVector { get { return opt.GetLowerAsVector(handle); } } @@ -156,7 +156,7 @@ namespace Microsoft.Z3 /// /// Retrieve an upper bound for the objective handle. /// - 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. /// - 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. /// - public Handle MkMinimize(ArithExpr e) + public Handle MkMinimize(Expr e) { return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); } + /// /// Retrieve a lower bound for the objective handle. /// - 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)); } /// /// Retrieve an upper bound for the objective handle. /// - 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)); } /// /// Retrieve a lower bound for the objective handle. /// - 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(); } /// /// Retrieve an upper bound for the objective handle. /// - 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(); } /// diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 3edbff73e..a434b6e9f 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -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 { * *

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 { * *

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 { * *

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) }; } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a521c5169..1f050d3bd 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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 diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9f155b45e..cf1c8fca7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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 */ diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 03ee77458..85c54d1fa 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -539,7 +539,7 @@ void arith_decl_plugin::get_op_names(svector& 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)); diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 0cc4f6031..1e789b7e5 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -524,7 +524,7 @@ void array_decl_plugin::get_sort_names(svector& sort_names, symbol void array_decl_plugin::get_op_names(svector& 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)); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 98c1bdfed..e7d808b2b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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()) { diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 093d0f548..28c3d5f5d 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -670,7 +670,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const { } void bv_decl_plugin::get_sort_names(svector & 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 & 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)); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 566487e60..91e636ed7 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -458,7 +458,7 @@ namespace datatype { void plugin::get_op_names(svector & 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)); } } diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 2f5a7c3c1..d87929864 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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"); } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 220295dad..d2a946e0c 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 631e1d8f3..acc3b889f 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -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; } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 3bb963a7f..71a9079a0 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -687,7 +687,7 @@ br_status poly_rewriter::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 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; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 13cb52df1..fa95278b4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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; diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index f9bf03951..c1c4588cc 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -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 diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index e4730ea63..ce2249a88 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -155,7 +155,7 @@ public: return res; } - void scan_skolems(const ast &proof){ + void scan_skolems(const ast &proof) { hash_map memo; scan_skolems_rec(memo,proof, INT_MAX); } diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index f0439a55c..fad424b90 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -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", diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index c560ee28e..6b689fd17 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -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, diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 37d80e2d6..1d3232deb 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -149,30 +149,27 @@ namespace pdr { } datalog::rule const& pred_transformer::find_rule(model_core const& model) const { - obj_map::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& 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) { diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 7bd35b4ef..8421a99ba 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -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; diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 30ff330ab..f1a4eb32b 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -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); } diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index c094e5520..dc11935e3 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -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::iterator it = m_sliceable.begin(); - obj_map::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"); } diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index e26f105c6..c6bb2864b 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -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; iget_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; iis_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: "< 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; } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 713ecfe77..2419d1c77 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -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; diff --git a/src/smt/smt_b_justification.h b/src/smt/smt_b_justification.h index 700c41807..55669a7ef 100644 --- a/src/smt/smt_b_justification.h +++ b/src/smt/smt_b_justification.h @@ -93,6 +93,16 @@ namespace smt { const b_justification null_b_justification(static_cast(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 justified_literal; }; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 80168df18..a6432c960 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -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(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) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7b508c7d8..3b69d4846 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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::iterator it = m_theory_set.begin(); - ptr_vector::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::const_iterator it = m_theory_set.begin(); - ptr_vector::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::iterator it = m_activity.begin(); svector::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::iterator it = m_theory_set.begin(); - ptr_vector::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::iterator it = m_theory_set.begin(); - ptr_vector::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); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3cc577b29..e50c03c8a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 6d66368ff..f5ba52128 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -71,11 +71,9 @@ namespace smt { case NUM_CONFLICTS: r = "max-conflicts-reached"; break; case THEORY: { r = "(incomplete (theory"; - ptr_vector::const_iterator it = m_incomplete_theories.begin(); - ptr_vector::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::const_iterator it = m_enodes.begin(); - ptr_vector::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 const & v) const { - ptr_vector::const_iterator it = v.begin(); - ptr_vector::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::const_iterator it = m_enodes.begin(); - ptr_vector::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(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals(out, lits.size(), lits.c_ptr()); + display_literals(out, lits); break; } default: diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index f72485d0e..cd59014aa 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -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) { diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 778f913c3..dd63940b7 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -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 m_fparams; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 0536c200d..11202d58a 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -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 diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 1d58e2bb3..c6f83c611 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -127,10 +127,8 @@ namespace smt { out << " #" << bindings[i]->get_owner_id(); } out << " ;"; - ptr_vector::const_iterator it = used_enodes.begin(); - ptr_vector::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::iterator it2 = m_quantifiers.begin(); - ptr_vector::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(); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 5f4e58a1b..806b2a05b 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index aa512a2be..b00648c36 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -443,7 +443,7 @@ namespace smt { } template - void theory_arith::mk_axiom(expr * ante, expr * conseq) { + void theory_arith::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 void theory_arith::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)) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d55484384..ca6ab048c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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 assumptions; const_cast(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); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2ad257fd7..d4686c835 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -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); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a1f0f9777..7936b581c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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()))); } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index acac8cad1..03fd31162 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -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 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); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index c6c85ec29..c8899e365 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -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); diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 651000297..c66483750 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -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(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(k.get_int64()); - m_lower[x] = _k; + m_lower[x] = std::max(m_lower[x], _k); } else { throw_not_supported(); diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 248829c49..de542f3c4 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -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) diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h index a9087e1c2..8a2eb124d 100644 --- a/src/util/checked_int64.h +++ b/src/util/checked_int64.h @@ -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(m_value); + uint64 y = static_cast(other.m_value); + int64 r = static_cast(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(m_value); + uint64 y = static_cast(other.m_value); + int64 r = static_cast(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; diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 6d2cbea7d..1f1054bb6 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -1157,7 +1157,7 @@ public: bool explanation_is_correct(const vector>& 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); diff --git a/src/util/union_find.h b/src/util/union_find.h index 7a99b149e..416b653af 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -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;