From d2c5e0e76acdd64df548533c740a12488fb8b0fb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 16:36:47 +0000 Subject: [PATCH 01/50] Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989. --- scripts/update_api.py | 140 ++++++++++++++++++++++++++-------------- src/api/python/z3/z3.py | 13 +--- 2 files changed, 94 insertions(+), 59 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 67a1b8a33..8e876d2fd 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -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,30 @@ 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)): + _elems.f(ctx, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)(hndlr)) + _elems.Check(ctx) + +""") + for sig in _API2PY: name = sig[0] result = sig[1] @@ -320,25 +342,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 +408,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") @@ -1605,35 +1618,71 @@ 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 + +if 'Z3_LIBRARY_PATH' in os.environ: + lp = os.environ['Z3_LIBRARY_PATH']; + 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: + 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 +1702,9 @@ 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 +_lib.Z3_set_error_handler.restype = None +_lib.Z3_set_error_handler.argtypes = [ContextObj, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)] - global _lib - _lib = ctypes.CDLL(PATH) """ ) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a521c5169..21ac695db 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,11 @@ 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): +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 -_Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core) - def _to_param_value(val): if isinstance(val, bool): if val == True: @@ -168,16 +164,13 @@ 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) 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_set_error_handler(self.ctx, z3_error_handler) Z3_del_config(conf) def __del__(self): - self.lib.Z3_del_context(self.ctx) + Z3_del_context(self.ctx) self.ctx = None def ref(self): From ef800d7b931b46fa8dffed3e36698506f654655b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 17:20:25 +0000 Subject: [PATCH 02/50] Fixed library path order in Python API. --- scripts/update_api.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8e876d2fd..8c0c895d9 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1653,10 +1653,11 @@ else: if hasattr(builtins, "Z3_LIB_DIRS"): _all_dirs = builtins.Z3_LIB_DIRS -if 'Z3_LIBRARY_PATH' in os.environ: - lp = os.environ['Z3_LIBRARY_PATH']; - lds = lp.split(';') if sys.platform in ('win32') else lp.split(':') - _all_dirs.extend(lds) +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) From bf563bbd5ffcba75f7a24d6a8b1095040884ca3a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 17:29:40 +0000 Subject: [PATCH 03/50] Fixed default library path order in Python API. --- scripts/update_api.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8c0c895d9..7d43b70ce 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1672,6 +1672,13 @@ for d in _all_dirs: 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,") From a8b52419f58d1d17a046941e96e3b43f35b997df Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 18:14:42 +0000 Subject: [PATCH 04/50] Fixed C example build. --- scripts/mk_util.py | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d44e8f416..1a1833534 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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) @@ -2512,6 +2535,7 @@ 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('OBJ_EXT=.o\n') From bec6c3f9e23ce509a10be74276b4670f8f8fc8ff Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 18:22:17 +0000 Subject: [PATCH 05/50] Fixed C example build. --- scripts/mk_util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1a1833534..e6de3019c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2343,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' @@ -2538,6 +2539,7 @@ def mk_config(): 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('AR=%s\n' % AR) From 17bcb37cf1f0560a6af8a2bed3bc1d6ec6bb77fb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 20:09:09 +0000 Subject: [PATCH 06/50] Fixed error handlers in Python API. --- scripts/update_api.py | 20 ++++++++++++-------- src/api/python/z3/z3.py | 15 ++++++++------- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 7d43b70ce..2828a63f8 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -324,14 +324,16 @@ class Elementaries: self.OK = Z3_OK self.Exception = Z3Exception - def Check(self, ctx): + 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)): - _elems.f(ctx, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)(hndlr)) + ceh = _error_handler_type(hndlr) + _elems.f(ctx, ceh) _elems.Check(ctx) + return ceh """) @@ -1637,10 +1639,10 @@ 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'), +_default_dirs = ['.', + os.path.dirname(os.path.abspath(__file__)), + pkg_resources.resource_filename('z3', 'lib'), + os.path.join(sys.prefix, 'lib'), None] _all_dirs = [] @@ -1667,7 +1669,7 @@ for d in _all_dirs: if os.path.isdir(d): d = os.path.join(d, 'libz3.%s' % _ext) if os.path.isfile(d): - _lib = ctypes.CDLL(d) + _lib = ctypes.CDLL(d) break except: pass @@ -1710,8 +1712,10 @@ else: else: return "" +_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, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)] +_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type] """ ) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 21ac695db..a247d0a3a 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -125,11 +125,6 @@ def _get_args(args): except: # len is not necessarily defined when args is not a sequence (use reflection?) return args -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 - def _to_param_value(val): if isinstance(val, bool): if val == True: @@ -139,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. @@ -165,13 +165,14 @@ class Context: Z3_set_param_value(conf, str(prev), _to_param_value(a)) prev = None 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) - Z3_set_error_handler(self.ctx, z3_error_handler) Z3_del_config(conf) def __del__(self): - 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.""" From 2d221155b3091afef3a38dd280084dd25fd96bab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 20:52:48 +0000 Subject: [PATCH 07/50] Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349. --- src/ast/fpa/fpa2bv_converter.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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); From 19f43713c9380fd744cdc54917440b6652c0db96 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Nov 2017 21:16:03 +0000 Subject: [PATCH 08/50] Fixed Windows build of C example. --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e6de3019c..a5c9068db 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2421,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(): From a173b0faf7db1c27b87065e47ba9d59f5eb14fce Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 9 Nov 2017 13:34:32 +0000 Subject: [PATCH 09/50] Fixed API doc build --- doc/mk_api_doc.py | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index ab4d32d39..3a2343803 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -288,6 +288,7 @@ 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)) + sys.path.insert(0, os.path.dirname(BUILD_DIR)) for modulename in ( 'z3', 'z3.z3consts', From d44d91841444f5cda70fc79680663ba932a3b6aa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 11 Nov 2017 14:19:38 +0000 Subject: [PATCH 10/50] API doc build fix. Related to #1350. --- doc/mk_api_doc.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 3a2343803..a944f2c65 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -288,7 +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)) - sys.path.insert(0, os.path.dirname(BUILD_DIR)) + + 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', From 45975bec65ad3cad95a6eae8abeaa1f90502c90c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 11 Nov 2017 15:11:54 +0000 Subject: [PATCH 11/50] Improved support for MSYS/MINGW. Fixes #969. --- scripts/mk_util.py | 34 ++++++++++++++++++++-------------- 1 file changed, 20 insertions(+), 14 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a5c9068db..ce83f58e5 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) @@ -2442,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 @@ -2471,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' @@ -2501,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' % CXXFLAGS + OS_DEFINES = '' + 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': @@ -2518,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(): @@ -2541,11 +2547,11 @@ def mk_config(): 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') From 7c63a5cc1ddf20e769a6d9abb1a43f561ca1ddf5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 11 Nov 2017 16:38:53 +0000 Subject: [PATCH 12/50] Fixed MSYS/MinGW build. Fixes #1335. --- scripts/mk_util.py | 4 ++-- src/interp/iz3interp.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ce83f58e5..b155fd7c2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2510,8 +2510,8 @@ def mk_config(): SO_EXT = '.dll' SLIBFLAGS = '-shared' elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): - CXXFLAGS = '%s' % CXXFLAGS - OS_DEFINES = '' + CXXFLAGS = '%s -D_MINGW' % CXXFLAGS + OS_DEFINES = '-D_MINGW' SO_EXT = '.dll' SLIBFLAGS = '-shared' EXE_EXT = '.exe' 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 From dbb35b951c3260c628e178fc509384893577f46b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Nov 2017 08:51:16 -0800 Subject: [PATCH 13/50] make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Optimize.cs | 32 +++++++++++++++++--------------- src/api/java/Optimize.java | 32 ++++++++++++++++---------------- 2 files changed, 33 insertions(+), 31 deletions(-) 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) }; } From 195d81ebefad9ea8b38d0bf049a268ee3012f50c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Nov 2017 13:49:03 -0800 Subject: [PATCH 14/50] fix rewriter loop reported in #1354 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 ++ src/interp/iz3translate.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) 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/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); } From 1a0bff7480f0145a5f9bd1adf59d05d6dfd2aa9a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 11 Nov 2017 22:49:14 +0000 Subject: [PATCH 15/50] [CMake] When invoking `mk_api_doc.py` pass the build directory. This change was requested by @wintersteiger as an alternative way to unbreak the TravisCI builds. --- doc/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) 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}" From 116094022fa5d67a1eb9c9319c87bf3504a71511 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 09:10:15 -0800 Subject: [PATCH 16/50] insert total relations in model converter. #1291 Signed-off-by: Nikolaj Bjorner --- .../dl_mk_interp_tail_simplifier.cpp | 3 ++ .../transforms/dl_mk_subsumption_checker.cpp | 53 ++++++++++--------- 2 files changed, 32 insertions(+), 24 deletions(-) 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_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: "< Date: Wed, 15 Nov 2017 11:46:28 -0800 Subject: [PATCH 17/50] include information whether rule is reachable in del_rule model converter for simpler model presentation #1241 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_util.cpp | 19 ++++++++++++------- src/muz/base/dl_util.h | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 16 ++++++++-------- 3 files changed, 21 insertions(+), 16 deletions(-) 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/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); } From 795e0c641a6a44362b47707c5885f921a07265e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 14:44:59 -0800 Subject: [PATCH 18/50] add method to create bit-vectors directly from an array of Booleans Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_numeral.cpp | 14 ++++++++++++++ src/api/c++/z3++.h | 6 ++++++ src/api/dotnet/Context.cs | 14 ++++++++++++++ src/api/z3_api.h | 8 ++++++++ src/ast/ast.cpp | 14 +------------- src/ast/rewriter/poly_rewriter_def.h | 2 +- 7 files changed, 45 insertions(+), 15 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 2828a63f8..2096e00ba 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -957,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) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 95bc0bef9..effa5f411 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -387,4 +387,18 @@ 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), two(2), one(1); + for (unsigned i = 0; i < sz; ++i) { + r *= two; + if (bits[i]) r += one; + } + 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..df385db78 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); @@ -2455,6 +2456,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/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/ast.cpp b/src/ast/ast.cpp index 98c1bdfed..d0921c8de 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -26,6 +26,7 @@ Revision History: #include "util/string_buffer.h" #include "ast/ast_util.h" #include "ast/ast_smt2_pp.h" +#include "ast/bv_decl_plugin.h" // ----------------------------------- // @@ -1684,22 +1685,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/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; From 7f13cf13f286fad9bc6d8e50bb9537f41bf15b72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 15:00:11 -0800 Subject: [PATCH 19/50] clean up bv_numeral code and fix bug in how they are initialized Signed-off-by: Nikolaj Bjorner --- src/api/api_numeral.cpp | 5 ++--- src/ast/ast.cpp | 1 - 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index effa5f411..9a778d6e0 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -391,10 +391,9 @@ extern "C" { Z3_TRY; LOG_Z3_mk_bv_numeral(c, sz, bits); RESET_ERROR_CODE(); - rational r(0), two(2), one(1); + rational r(0); for (unsigned i = 0; i < sz; ++i) { - r *= two; - if (bits[i]) r += one; + 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)); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d0921c8de..e7d808b2b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -26,7 +26,6 @@ Revision History: #include "util/string_buffer.h" #include "ast/ast_util.h" #include "ast/ast_smt2_pp.h" -#include "ast/bv_decl_plugin.h" // ----------------------------------- // From 61d149a724ca17970bae3b1525e4cf1a17825340 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 16:18:18 -0800 Subject: [PATCH 20/50] fix java build problem with bool arrays Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 2096e00ba..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" @@ -491,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' @@ -653,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)) @@ -663,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)) @@ -702,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') From cde41cf16ca9d95acd95d66a24a136b0cddb09da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 16:39:09 -0800 Subject: [PATCH 21/50] fix slicer for unsoundness. #1304 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_slice.cpp | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) 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"); } From 58be77730746a357bf3d7123df9d5ceac49cc40f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 20:32:37 -0800 Subject: [PATCH 22/50] fix #1358 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/diff_neq_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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(); From c3f67f3b5f77bb7ea984baf2fa6117874d5aff44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 21:17:00 -0800 Subject: [PATCH 23/50] fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/smt_context.h | 7 ++++++- src/smt/theory_str.cpp | 19 +++++++++++++------ src/smt/theory_str.h | 4 ++++ 4 files changed, 24 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7b508c7d8..2e65fddc9 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4373,7 +4373,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";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3cc577b29..c6cca2c43 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. } } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a1f0f9777..17f889946 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), @@ -4648,14 +4650,17 @@ 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; + theory_var curr = m_find.find(get_var(n)); + theory_var first = curr; do { - if (u.str.is_string(curr)) { + expr* a = get_ast(curr); + if (u.str.is_string(a)) { hasEqcValue = true; - return curr; + return a; } - curr = get_eqc_next(curr); - } while (curr != n); + curr = m_find.next(curr); + } + while (curr != first && curr != null_theory_var); hasEqcValue = false; return n; } @@ -10584,7 +10589,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..b478808d2 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; From c3364f17fa5058903ce4e606da21a9d0e781d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 21:19:22 -0800 Subject: [PATCH 24/50] fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 17f889946..2ed8c578f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4652,15 +4652,17 @@ namespace smt { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { theory_var curr = m_find.find(get_var(n)); 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); + if (curr != null_theory_var) { + 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; } From 2e6ae8cfd24bea46bbc9c2fd54ce7eb611d12caa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 23:06:05 -0800 Subject: [PATCH 25/50] fix crash Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 15 ++++++++------- src/smt/theory_str.h | 2 +- src/util/union_find.h | 1 + 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2ed8c578f..ed926a50d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -63,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(); } @@ -281,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; @@ -1905,8 +1905,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 { @@ -4650,9 +4650,10 @@ namespace smt { // We only check m_find for a string constant. expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { - theory_var curr = m_find.find(get_var(n)); - theory_var first = curr; + 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)) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index b478808d2..03fd31162 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -362,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/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; From 07031798ecf70edf76175195b55fef849d7099f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 01:43:35 -0800 Subject: [PATCH 26/50] fix occurs function used in qe_lite #1241 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_lite.cpp | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 257331161..01806bc24 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -20,7 +20,6 @@ Revision History: #include "qe/qe_lite.h" #include "ast/expr_abstract.h" #include "ast/used_vars.h" -#include "ast/occurs.h" #include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" @@ -39,6 +38,30 @@ Revision History: #include "qe/qe_vartest.h" namespace eq { + + bool occurs_var(unsigned idx, expr* e) { + ptr_buffer 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; } From 2efcd5b78901a0635c4f0dc977a8ef06817913c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 08:55:40 -0800 Subject: [PATCH 27/50] additional bit-vector operators over C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index df385db78..3d39cdb74 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -965,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); } @@ -1333,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); } From a68d5131c7b91b841289f25044511f76f8232eaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 09:00:14 -0800 Subject: [PATCH 28/50] add bvsmod Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3d39cdb74..4b5e9d04e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1418,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 From 62cf6aace75f9dd74d17f4fb2d0d980b447a2207 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 16 Nov 2017 10:20:21 -0800 Subject: [PATCH 29/50] avoid a warning Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From f5ff9fae3477850d849d217193857f37c2ee5e0d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 17 Nov 2017 21:15:30 +0000 Subject: [PATCH 30/50] Fixed bug check in bv2fpa converter. Fixes #1291. --- src/ast/fpa/bv2fpa_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"); } } From 620bd812690228eda0462e78ec209d4749590e9f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Nov 2017 20:41:42 -0800 Subject: [PATCH 31/50] avoid rationals for addition in checked_int64 Signed-off-by: Nikolaj Bjorner --- src/util/checked_int64.h | 66 +++++++++++++++++----------------------- 1 file changed, 28 insertions(+), 38 deletions(-) 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; From 33e8113c9e623d5b9099dc16482487a4487b882c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Nov 2017 16:51:17 -0800 Subject: [PATCH 32/50] adding instrumentation to debug #1233 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 26 +++++------ src/smt/smt_conflict_resolution.cpp | 70 +++++++++++++++-------------- src/smt/smt_context.cpp | 48 +++++++------------- src/smt/smt_context.h | 18 ++++---- src/smt/smt_context_pp.cpp | 58 ++++++++++-------------- src/solver/solver_pool.cpp | 1 - 6 files changed, 94 insertions(+), 127 deletions(-) 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/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 80168df18..6188c8b1a 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; } @@ -335,6 +333,7 @@ namespace smt { } if (lvl == m_conflict_lvl) { + TRACE("conflict", m_ctx.display_literal(tout << "marking:", antecedent) << "\n";); num_marks++; } else { @@ -486,6 +485,20 @@ namespace smt { } bool conflict_resolution::resolve(b_justification conflict, literal not_l) { + +#if 0 + // for debugging #1233 + if (not_l == to_literal(22267)) { + std::cout << not_l << "\n"; + enable_trace("conflict"); + enable_trace("conflict_verbose"); + TRACE("conflict", + unsigned idx = 0; + for (literal lit : m_assigned_literals) { + m_ctx.display_literal(tout << (idx++) << ":", lit); tout << "\n"; + }); + } +#endif b_justification js; literal consequent; @@ -514,7 +527,7 @@ 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: " << idx << " "; m_ctx.display_literal_verbose(tout, consequent); tout << "\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 +579,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 +621,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 +673,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 +1074,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 +1255,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 +1334,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 +1373,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 2e65fddc9..30979fc4b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1615,11 +1615,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 +1692,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 +1729,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 +1815,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 +1962,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 +2138,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 +2235,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 +2908,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 +3167,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(); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index c6cca2c43..d55e36f44 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1235,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()); } 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..f2fb1084b 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,7 +598,7 @@ 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()); 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); From c5f231acdfab2a8032201fb213d169f818ac0cef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 08:16:41 -0800 Subject: [PATCH 33/50] debugging #1233 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 38 +++++++++-------------------- src/smt/smt_context.cpp | 9 ++++++- src/smt/smt_context.h | 2 +- src/smt/theory_seq.cpp | 23 +++++++++++++++++ 4 files changed, 43 insertions(+), 29 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 6188c8b1a..02c38a2bd 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -313,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); @@ -328,8 +328,7 @@ 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) { @@ -391,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"; ); @@ -430,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(); @@ -527,7 +510,8 @@ namespace smt { get_manager().trace_stream() << "\n"; } - TRACE("conflict", tout << "processing consequent: " << idx << " "; 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); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 30979fc4b..8819e37b6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -287,6 +287,13 @@ namespace smt { void context::assign_core(literal l, b_justification j, bool decision) { +#if 0 + // for debugging #1233 + if (l.var() == 11133 && l.sign()) { + std::cout << l << "\n"; + UNREACHABLE(); + } +#endif TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); @@ -902,7 +909,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()); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d55e36f44..e50c03c8a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1237,7 +1237,7 @@ namespace smt { 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; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d55484384..caba4e92e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1298,6 +1298,21 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { display_deps(tout, dep); ); +#if 0 + //std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; + //display_deps(std::cout, dep); + + for (literal lit : lits) { + SASSERT(ctx.get_assignment(lit) == l_true); + } + for (enode_pair p : eqs) { + if (p.first->get_root() != p.second->get_root()) { + std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n"; + } + SASSERT(p.first->get_root() == p.second->get_root()); + } +#endif + justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); @@ -3027,6 +3042,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 +3054,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; From d520557ad95bba6a084b876b98d7f4327885c286 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 11:52:15 -0800 Subject: [PATCH 34/50] fix #1233 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_b_justification.h | 10 +++++ src/smt/smt_conflict_resolution.cpp | 14 ------- src/smt/smt_context.cpp | 8 ---- src/smt/smt_context_pp.cpp | 2 +- src/smt/theory_seq.cpp | 63 +++++++++++++---------------- src/smt/theory_seq.h | 2 +- 6 files changed, 41 insertions(+), 58 deletions(-) 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 02c38a2bd..a6432c960 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -468,20 +468,6 @@ namespace smt { } bool conflict_resolution::resolve(b_justification conflict, literal not_l) { - -#if 0 - // for debugging #1233 - if (not_l == to_literal(22267)) { - std::cout << not_l << "\n"; - enable_trace("conflict"); - enable_trace("conflict_verbose"); - TRACE("conflict", - unsigned idx = 0; - for (literal lit : m_assigned_literals) { - m_ctx.display_literal(tout << (idx++) << ":", lit); tout << "\n"; - }); - } -#endif b_justification js; literal consequent; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 8819e37b6..62a569e2b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -285,15 +285,7 @@ namespace smt { d.set_justification(j); } - void context::assign_core(literal l, b_justification j, bool decision) { -#if 0 - // for debugging #1233 - if (l.var() == 11133 && l.sign()) { - std::cout << l << "\n"; - UNREACHABLE(); - } -#endif TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index f2fb1084b..f5ba52128 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -601,7 +601,7 @@ namespace smt { 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/theory_seq.cpp b/src/smt/theory_seq.cpp index caba4e92e..6f7cf1b5e 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,27 +1301,13 @@ 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); ); -#if 0 - //std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; - //display_deps(std::cout, dep); - - for (literal lit : lits) { - SASSERT(ctx.get_assignment(lit) == l_true); - } - for (enode_pair p : eqs) { - if (p.first->get_root() != p.second->get_root()) { - std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n"; - } - SASSERT(p.first->get_root() == p.second->get_root()); - } -#endif - justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); @@ -1858,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: @@ -1967,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); @@ -2574,8 +2568,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"; @@ -3820,11 +3814,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; } } @@ -3895,8 +3889,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..e08c0588e 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); From 18200f55edf14e5360c9095736710ae689032f6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 15:14:49 -0800 Subject: [PATCH 35/50] add bit-vector over/underflow checks to Python API, #1364 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 59 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a247d0a3a..5ccab92dd 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3993,6 +3993,65 @@ 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""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) + +def BVAddNoUnderflow(a, b, signed): + """A predicate the determines that signed bit-vector addition does not underflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + 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""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + 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""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + 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""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + 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), "Arguments should be bit-vectors") + 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""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) + + +def BVMulNoUnderflow(a, b, signed): + """A predicate the determines that bit-vector signed multiplication does not underflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + + ######################################### # # Arrays From 2597ac67568f6709351d5fd2324e1b2a209b0b06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 15:44:15 -0800 Subject: [PATCH 36/50] fix argument validation to new overflow/underflow functions #1364 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 37 +++++++++++++++---------------------- 1 file changed, 15 insertions(+), 22 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5ccab92dd..17e5bbff8 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3995,59 +3995,52 @@ def BVRedOr(a): def BVAddNoOverflow(a, b, signed): """A predicate the determines that bit-vector addition does not overflow""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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, signed): """A predicate the determines that signed bit-vector addition does not underflow""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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), "Arguments should be bit-vectors") + _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""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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, signed): """A predicate the determines that bit-vector signed multiplication does not underflow""" - if __debug__: - _z3_assert(is_bv(a), "Arguments should be bit-vectors") - _z3_assert(is_bv(b), "Arguments should be bit-vectors") + _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) From 56cc0a9018424409adb55b8aba75f92f2ac66d2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 15:47:27 -0800 Subject: [PATCH 37/50] remove redundant argument #1364 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 17e5bbff8..1f050d3bd 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3999,7 +3999,7 @@ def BVAddNoOverflow(a, b, signed): 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, signed): +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) @@ -4037,7 +4037,7 @@ def BVMulNoOverflow(a, b, signed): return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) -def BVMulNoUnderflow(a, b, signed): +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) From 357b4b20fd0ee83e38ba52328ca16b30bc2e5a0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Nov 2017 11:17:41 -0800 Subject: [PATCH 38/50] fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_checker.cpp | 5 +++-- src/smt/smt_model_checker.h | 2 ++ src/smt/smt_model_finder.cpp | 8 ++------ src/smt/smt_quantifier.cpp | 11 +++-------- 4 files changed, 10 insertions(+), 16 deletions(-) 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(); From 1c5f798cbe473b5508ea295356bed7b97c05adbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 12:03:47 -0800 Subject: [PATCH 39/50] expose extra symbols for logic ALL, requested in #1364 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 2 +- src/ast/array_decl_plugin.cpp | 2 +- src/ast/bv_decl_plugin.cpp | 4 ++-- src/ast/datatype_decl_plugin.cpp | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) 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/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)); } } From 77b74ddb8855b9f174cc70c34e046c0ae16b0d56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 17:55:20 -0800 Subject: [PATCH 40/50] fix #1366 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 122 +++++++++++++++++++++++++++-------------- src/smt/theory_seq.h | 1 + 2 files changed, 83 insertions(+), 40 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6f7cf1b5e..1286fa85d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1766,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 && @@ -1786,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) { @@ -1800,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) { @@ -1813,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) { @@ -2353,7 +2353,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);); @@ -3101,7 +3101,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); @@ -3111,6 +3110,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); } @@ -3156,11 +3156,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 @@ -3190,32 +3203,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(offset, len_t)); + literal offset_le_len = mk_simplified_literal(m_autil.mk_le(offset, len_t)); + 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 @@ -3228,10 +3254,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); } } @@ -3574,11 +3600,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 @@ -3590,6 +3624,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)) { @@ -3618,13 +3653,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)); @@ -3684,14 +3719,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)); @@ -3706,8 +3742,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)); } @@ -3733,8 +3769,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)); @@ -3753,7 +3789,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) { @@ -3790,6 +3826,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(); @@ -3839,7 +3881,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()); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index e08c0588e..d4686c835 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -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); From 841c48e04df40c0b91f7eabfbdc32b3a80173891 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 18:24:45 -0800 Subject: [PATCH 41/50] fix break Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1286fa85d..fb8f36c59 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3230,8 +3230,8 @@ void theory_seq::add_indexof_axiom(expr* i) { // 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_simplified_literal(m_autil.mk_ge(offset, len_t)); - literal offset_le_len = mk_simplified_literal(m_autil.mk_le(offset, len_t)); + 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); From 7d693a5f9f3a535317ea22c37a67388a367c1fa7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 20:01:14 -0800 Subject: [PATCH 42/50] fix different bug reported on #1366 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fb8f36c59..131d1fd1b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1987,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); From 4520fafa8c2b15abf35074551cf49ab47512ed44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Nov 2017 19:13:35 -0800 Subject: [PATCH 43/50] fix #1368 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_core.h | 33 +++++++++++++++------------ src/tactic/smtlogics/qflia_tactic.cpp | 5 +--- 3 files changed, 21 insertions(+), 19 deletions(-) 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/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) From bfe6260c58c740c7efda919861ab3d4e5c8f70d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 08:39:20 -0800 Subject: [PATCH 44/50] fix #1376 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 131d1fd1b..ca6ab048c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2400,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; From 2b3ee995ffdf03f67c6e05586d1ebbc1081b9181 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 09:03:52 -0800 Subject: [PATCH 45/50] fix #1375 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ed926a50d..7936b581c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1077,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;); @@ -1092,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); } From 36e5d4dec9c01f87e6d6c5f2de3c202d84b2e92a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 11:01:44 -0800 Subject: [PATCH 46/50] fix #1377 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 13cb52df1..41b08a5d9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1572,6 +1572,8 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ bool lchange = false; SASSERT(lhs.empty()); TRACE("seq", tout << ls << "\n"; tout << rs << "\n";); + //std::cout << ls << "\n"; + //std::cout << rs << "\n"; // solve from back while (true) { while (!rs.empty() && m_util.str.is_empty(rs.back())) { @@ -1645,6 +1647,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; From 81ec5bae9500756bd7ea28a1da28afcdb0ca848f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 11:02:48 -0800 Subject: [PATCH 47/50] fix #1377 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 41b08a5d9..fa95278b4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1572,8 +1572,6 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ bool lchange = false; SASSERT(lhs.empty()); TRACE("seq", tout << ls << "\n"; tout << rs << "\n";); - //std::cout << ls << "\n"; - //std::cout << rs << "\n"; // solve from back while (true) { while (!rs.empty() && m_util.str.is_empty(rs.back())) { From 103ce78c29a4a2933637e0e6d4d5cb1fa5e6c08c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2017 08:53:06 -0800 Subject: [PATCH 48/50] save model from level 0, fix #1380 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter_def.h | 3 +++ src/qe/qsat.cpp | 5 ++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 2abd6d467..31f7d4849 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -190,6 +190,9 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { else if (m().is_false(cond)) { arg = t->get_arg(2); } + else { + std::cout << mk_ismt2_pp(cond, m()) << "\n"; + } if (arg) { result_stack().shrink(fr.m_spos); result_stack().push_back(arg); 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; From 5a35d0076682cb0cf6b61d0c0dbecf034aa01539 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2017 08:55:45 -0800 Subject: [PATCH 49/50] remove std::cout Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter_def.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 31f7d4849..2abd6d467 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -190,9 +190,6 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { else if (m().is_false(cond)) { arg = t->get_arg(2); } - else { - std::cout << mk_ismt2_pp(cond, m()) << "\n"; - } if (arg) { result_stack().shrink(fr.m_spos); result_stack().push_back(arg); From d7042c234f32607c01324da7a3bbf74384d0aaab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2017 09:34:44 -0800 Subject: [PATCH 50/50] fix #1371 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 62a569e2b..3b69d4846 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4366,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);