diff --git a/CMakeLists.txt b/CMakeLists.txt
index a9e121d02..5fef02be9 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -198,7 +198,9 @@ elseif (CMAKE_SYSTEM_NAME MATCHES "GNU")
message(STATUS "Platform: GNU/Hurd")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_")
elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
- # Does macOS really not need any special flags?
+ if (TARGET_ARCHITECTURE STREQUAL "arm64")
+ set(CMAKE_OSX_ARCHITECTURES "arm64")
+ endif()
message(STATUS "Platform: Darwin")
elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
message(STATUS "Platform: FreeBSD")
diff --git a/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp
index 0a2d0f3e6..379b5817e 100644
--- a/cmake/target_arch_detect.cpp
+++ b/cmake/target_arch_detect.cpp
@@ -5,6 +5,8 @@
#error CMAKE_TARGET_ARCH_i686
#elif defined(__x86_64__) || defined(_M_X64)
#error CMAKE_TARGET_ARCH_x86_64
+#elif defined(__ARM_ARCH_ISA_A64)
+#error CMAKE_TARGET_ARCH_arm64
#elif defined(__ARM_ARCH)
#error CMAKE_TARGET_ARCH_arm
#else
diff --git a/doc/website.dox.in b/doc/website.dox.in
index 69395492e..f4caa1277 100644
--- a/doc/website.dox.in
+++ b/doc/website.dox.in
@@ -4,7 +4,7 @@
Z3 is a high-performance theorem prover being developed at Microsoft Research.
- The Z3 website is at http://github.com/z3prover..
+ The Z3 website is at http://github.com/z3prover.
This website hosts the automatically generated documentation for the Z3 APIs.
diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py
index 28d68a01b..97de725e9 100644
--- a/scripts/mk_unix_dist.py
+++ b/scripts/mk_unix_dist.py
@@ -56,6 +56,7 @@ def display_help():
print(" -f, --force force script to regenerate Makefiles.")
print(" --nodotnet do not include .NET bindings in the binary distribution files.")
print(" --dotnet-key= sign the .NET assembly with the private key in .")
+ print(" --arch= set architecture (to arm64) to force arm64 build")
print(" --nojava do not include Java bindings in the binary distribution files.")
print(" --nopython do not include Python bindings in the binary distribution files.")
print(" --githash include git hash in the Zip file.")
@@ -72,6 +73,7 @@ def parse_options():
'nojava',
'nodotnet',
'dotnet-key=',
+ 'arch=',
'githash',
'nopython'
])
@@ -96,6 +98,11 @@ def parse_options():
JAVA_ENABLED = False
elif opt == '--githash':
GIT_HASH = True
+ elif opt == '--arch':
+ if arg == "arm64":
+ mk_util.IS_ARCH_ARM64 = True
+ else:
+ raise MKException("Invalid architecture directive '%s'. Legal directives: arm64" % arg)
else:
raise MKException("Invalid command line option '%s'" % opt)
set_build_dir(path)
@@ -119,6 +126,8 @@ def mk_build_dir(path):
opts.append('--git-describe')
if PYTHON_ENABLED:
opts.append('--python')
+ if mk_util.IS_ARCH_ARM64:
+ opts.append('--arm64=true')
if subprocess.call(opts) != 0:
raise MKException("Failed to generate build directory at '%s'" % path)
@@ -172,7 +181,9 @@ def get_os_name():
def get_z3_name():
major, minor, build, revision = get_version()
- if sys.maxsize >= 2**32:
+ if mk_util.IS_ARCH_ARM64:
+ platform = "arm64"
+ elif sys.maxsize >= 2**32:
platform = "x64"
else:
platform = "x86"
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 1fca64f29..761de8b26 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -69,6 +69,7 @@ IS_WINDOWS=False
IS_LINUX=False
IS_HURD=False
IS_OSX=False
+IS_ARCH_ARM64=False
IS_FREEBSD=False
IS_NETBSD=False
IS_OPENBSD=False
@@ -278,10 +279,13 @@ def test_gmp(cc):
def test_fpmath(cc):
- global FPMATH_FLAGS
+ global FPMATH_FLAGS, IS_ARCH_ARM64, IS_OSX
if FPMATH_ENABLED == "False":
FPMATH_FLAGS=""
return "Disabled"
+ if IS_ARCH_ARM64 and IS_OSX:
+ FPMATH_FLAGS = ""
+ return "Disabled-ARM64"
if is_verbose():
print("Testing floating point support...")
t = TempFile('tstsse.cpp')
@@ -620,8 +624,12 @@ elif os.name == 'posix':
LINUX_X64=True
else:
LINUX_X64=False
-
+
+if os.name == 'posix' and os.uname()[4] == 'arm64':
+ IS_ARCH_ARM64 = True
+
+
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
print("This script generates the Makefile for the Z3 theorem prover.")
@@ -644,6 +652,7 @@ def display_help(exit_code):
print(" -x, --x64 create 64 binary when using Visual Studio.")
else:
print(" --x86 force 32-bit x86 build on x64 systems.")
+ print(" --arm64= forcearm64 bit build on/off (supported for Darwin).")
print(" -m, --makefiles generate only makefiles.")
if IS_WINDOWS:
print(" -v, --vsproj generate Visual Studio Project Files.")
@@ -686,11 +695,11 @@ def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
- global GUARD_CF, ALWAYS_DYNAMIC_BASE
+ global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
- 'b:df:sxhmcvtnp:gj',
- ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
+ 'b:df:sxa:hmcvtnp:gj',
+ ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
except:
@@ -713,6 +722,8 @@ def parse_options():
VS_X64 = True
elif opt in ('--x86'):
LINUX_X64=False
+ elif opt in ('--arm64'):
+ IS_ARCH_ARM64 = arg in ('true','on','True','TRUE')
elif opt in ('-h', '--help'):
display_help(0)
elif opt in ('-m', '--makefiles'):
@@ -2431,7 +2442,7 @@ def mk_config():
if ONLY_MAKEFILES:
return
config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
- global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED
+ global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64
if IS_WINDOWS:
CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++17'
config.write(
@@ -2636,6 +2647,11 @@ def mk_config():
LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
CXXFLAGS = '%s -fpic' % CXXFLAGS
+ if IS_OSX and IS_ARCH_ARM64:
+ print("Setting arm64")
+ CXXFLAGS = '%s -arch arm64' % CXXFLAGS
+ LDFLAGS = '%s -arch arm64' % LDFLAGS
+ SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS
config.write('PREFIX=%s\n' % PREFIX)
config.write('CC=%s\n' % CC)
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index 20ebb0137..8590c96e9 100644
--- a/scripts/nightly.yaml
+++ b/scripts/nightly.yaml
@@ -4,7 +4,6 @@ variables:
Minor: '8'
Patch: '16'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
- MacFlags: 'CXXFLAGS="-arch x86_64" LINK_EXTRA_FLAGS="-arch x86_64" SLINK_EXTRA_FLAGS="-arch x86_64"'
stages:
- stage: Build
@@ -15,7 +14,7 @@ stages:
pool:
vmImage: "macOS-latest"
steps:
- - script: $(MacFlags) python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+ - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
- script: git clone https://github.com/z3prover/z3test z3test
- script: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
@@ -25,6 +24,20 @@ stages:
targetPath: $(Build.ArtifactStagingDirectory)
+ - job: MacArm64
+ displayName: "Mac ARM64 Build"
+ pool:
+ vmImage: "macOS-latest"
+ steps:
+ - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
+ - script: git clone https://github.com/z3prover/z3test z3test
+ - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
+ - task: PublishPipelineArtifact@1
+ inputs:
+ artifactName: 'MacArm64'
+ targetPath: $(Build.ArtifactStagingDirectory)
+
+
- job: Ubuntu
displayName: "Ubuntu build"
pool:
@@ -166,6 +179,11 @@ stages:
inputs:
artifact: 'Mac'
path: $(Agent.TempDirectory)\package
+ - task: DownloadPipelineArtifact@2
+ displayName: 'Download macOS Arm64 Build'
+ inputs:
+ artifact: 'MacArm64'
+ path: $(Agent.TempDirectory)\package
- task: NuGetToolInstaller@0
inputs:
versionSpec: 5.x
@@ -381,7 +399,12 @@ stages:
inputs:
artifactName: 'Mac'
targetPath: $(Agent.TempDirectory)
- - script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip
+ - task: DownloadPipelineArtifact@2
+ inputs:
+ artifactName: 'MacArm64'
+ targetPath: $(Agent.TempDirectory)
+ - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
+ - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
- script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
@@ -391,7 +414,8 @@ stages:
- script: cd src/api/python; echo $(Agent.TempDirectory)/linux-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
+ - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
+ - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'Python packages'
@@ -421,6 +445,11 @@ stages:
inputs:
artifactName: 'Mac'
targetPath: tmp
+ - task: DownloadPipelineArtifact@2
+ displayName: "Download MacArm64"
+ inputs:
+ artifactName: 'MacArm64'
+ targetPath: tmp
- task: DownloadPipelineArtifact@2
displayName: "Download Ubuntu"
inputs:
diff --git a/scripts/update_api.py b/scripts/update_api.py
index ab1b4d6fd..d4d1ab0e0 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1820,8 +1820,8 @@ _error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
_lib.Z3_set_error_handler.restype = None
_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
-push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
-pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
+push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
+pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index d5de6b5fb..9f9039378 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -164,7 +164,7 @@ extern "C" {
return;
}
recfun_replace replace(m);
- p.set_definition(replace, pd, true, n, _vars.data(), abs_body);
+ p.set_definition(replace, pd, false, n, _vars.data(), abs_body);
Z3_CATCH;
}
@@ -355,7 +355,7 @@ extern "C" {
return mk_c(c)->mk_external_string(buffer.str());
}
else {
- return mk_c(c)->mk_external_string(_s.bare_str());
+ return mk_c(c)->mk_external_string(_s.str());
}
Z3_CATCH_RETURN("");
}
@@ -1329,6 +1329,9 @@ extern "C" {
}
}
+ if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
+ return Z3_OP_RECURSIVE;
+
return Z3_OP_UNINTERPRETED;
Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
}
diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp
index c1864ae8c..ed5f68e8a 100644
--- a/src/api/api_log.cpp
+++ b/src/api/api_log.cpp
@@ -88,7 +88,7 @@ void Sy(Z3_symbol sym) {
*g_z3_log << "# " << s.get_num();
}
else {
- *g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|';
+ *g_z3_log << "$ |" << ll_escaped{s.str().c_str()} << '|';
}
*g_z3_log << std::endl;
}
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 99d332724..948064af6 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -883,8 +883,8 @@ extern "C" {
Z3_TRY;
RESET_ERROR_CODE();
init_solver(c, s);
- user_propagator::push_eh_t _push = push_eh;
- user_propagator::pop_eh_t _pop = pop_eh;
+ user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh;
+ user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh;
user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) {
ast_context_params params;
params.set_foreign_manager(&m);
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 45073cdb1..f67a373dd 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -331,8 +331,8 @@ extern "C" {
if (idx >= mk_c(c)->num_tactics()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return "";
- }
- return mk_c(c)->get_tactic(idx)->get_name().bare_str();
+ }
+ return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str());
Z3_CATCH_RETURN("");
}
@@ -352,7 +352,7 @@ extern "C" {
SET_ERROR_CODE(Z3_IOB, nullptr);
return "";
}
- return mk_c(c)->get_probe(idx)->get_name().bare_str();
+ return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str());
Z3_CATCH_RETURN("");
}
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 4d60de433..101fa04a3 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -3964,18 +3964,23 @@ namespace z3 {
}
};
- static void push_eh(void* p) {
+ static void push_eh(void* _p, Z3_solver_callback cb) {
+ user_propagator_base* p = static_cast(_p);
+ scoped_cb _cb(p, cb);
static_cast(p)->push();
}
- static void pop_eh(void* p, unsigned num_scopes) {
- static_cast(p)->pop(num_scopes);
+ static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
+ user_propagator_base* p = static_cast(_p);
+ scoped_cb _cb(p, cb);
+ static_cast(_p)->pop(num_scopes);
}
- static void* fresh_eh(void* p, Z3_context ctx) {
+ static void* fresh_eh(void* _p, Z3_context ctx) {
+ user_propagator_base* p = static_cast(_p);
context* c = new context(ctx);
- static_cast(p)->subcontexts.push_back(c);
- return static_cast(p)->fresh(*c);
+ p->subcontexts.push_back(c);
+ return p->fresh(*c);
}
static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index e791a2f11..067a25e8c 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -42,8 +42,6 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
- # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
- "${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating z3core.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml
new file mode 100644
index 000000000..a9f2676a7
--- /dev/null
+++ b/src/api/python/pyproject.toml
@@ -0,0 +1,3 @@
+[build-system]
+requires = ["setuptools>=46.4.0", "wheel", "cmake"]
+build-backend = "setuptools.build_meta"
diff --git a/src/api/python/setup.py b/src/api/python/setup.py
index 8c73c29e6..5309142f2 100644
--- a/src/api/python/setup.py
+++ b/src/api/python/setup.py
@@ -154,16 +154,10 @@ def _copy_bins():
_clean_bins()
- python_dir = None
- if RELEASE_DIR is not None:
- python_dir = os.path.join(RELEASE_DIR, 'bin', 'python')
- elif SRC_DIR == SRC_DIR_LOCAL:
- python_dir = os.path.join(SRC_DIR, 'src', 'api', 'python')
- if python_dir is not None:
- py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3')
- root_z3_dir = os.path.join(ROOT_DIR, 'z3')
- shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir)
- shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir)
+ py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3')
+ root_z3_dir = os.path.join(ROOT_DIR, 'z3')
+ shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir)
+ shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir)
# STEP 2: Copy the shared library, the executable and the headers
@@ -279,8 +273,10 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
osver = RELEASE_METADATA[3]
if osver.count('.') > 1:
osver = '.'.join(osver.split('.')[:2])
- if arch == 'x64':
+ if arch == 'x64':
plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
+ elif arch == 'arm64':
+ plat_name ='macosx_%s_arm64' % osver.replace('.', '_')
else:
raise Exception(f"idk how os {distos} {osver} works. what goes here?")
else:
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 6f4dcf430..223b3e038 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2279,6 +2279,9 @@ class ArithSortRef(SortRef):
"""
return self.kind() == Z3_INT_SORT
+ def is_bool(self):
+ return False
+
def subsort(self, other):
"""Return `True` if `self` is a subsort of `other`."""
return self.is_int() and is_arith_sort(other) and other.is_real()
@@ -11237,12 +11240,16 @@ def ensure_prop_closures():
_prop_closures = PropClosures()
-def user_prop_push(ctx):
- _prop_closures.get(ctx).push()
+def user_prop_push(ctx, cb):
+ prop = _prop_closures.get(ctx)
+ prop.cb = cb
+ prop.push()
-def user_prop_pop(ctx, num_scopes):
- _prop_closures.get(ctx).pop(num_scopes)
+def user_prop_pop(ctx, cb, num_scopes):
+ prop = _prop_closures.get(ctx)
+ prop.cb = cb
+ pop(num_scopes)
def user_prop_fresh(id, ctx):
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index d7dd0a332..1388d0ab1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -996,6 +996,8 @@ typedef enum
information is exposed. Tools may use the string representation of the
function declaration to obtain more information.
+ - Z3_OP_RECURSIVE: function declared as recursive
+
- Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
*/
typedef enum {
@@ -1320,6 +1322,7 @@ typedef enum {
Z3_OP_FPA_BV2RM,
Z3_OP_INTERNAL,
+ Z3_OP_RECURSIVE,
Z3_OP_UNINTERPRETED
} Z3_decl_kind;
@@ -1434,8 +1437,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e));
/**
\brief callback functions for user propagator.
*/
-Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx));
-Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, unsigned num_scopes));
+Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx, Z3_solver_callback cb));
+Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes));
Z3_DECLARE_CLOSURE(Z3_fresh_eh, void*, (void* ctx, Z3_context new_context));
Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value));
Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 9854195a4..59f9ecda6 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -47,18 +47,14 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo
len = static_cast(str.length());
return mk_string(m, str);
}
- else if (s.is_numerical()) {
- std::string str = s.str();
- len = static_cast(str.length());
- return mk_string(m, str);
- }
- else if (!s.bare_str()) {
+ else if (s.is_null()) {
len = 4;
return mk_string(m, "null");
}
else {
- len = static_cast(strlen(s.bare_str()));
- return mk_string(m, s.bare_str());
+ std::string str = s.str();
+ len = static_cast(str.length());
+ return mk_string(m, str);
}
}
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index d4797b507..10e6c694c 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -90,11 +90,11 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) {
if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") {
- op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
- op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
- op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
- op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
- op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
+ op_names.push_back(builtin_name(m_at_most_sym.str(), OP_AT_MOST_K));
+ op_names.push_back(builtin_name(m_at_least_sym.str(), OP_AT_LEAST_K));
+ op_names.push_back(builtin_name(m_pble_sym.str(), OP_PB_LE));
+ op_names.push_back(builtin_name(m_pbge_sym.str(), OP_PB_GE));
+ op_names.push_back(builtin_name(m_pbeq_sym.str(), OP_PB_EQ));
}
}
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 073885c21..1fdd7bd14 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2803,6 +2803,21 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
return BR_FAILED;
}
+br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
+ if (num_args <= 1) {
+ result = m().mk_true();
+ return BR_DONE;
+ }
+ unsigned sz = get_bv_size(args[0]);
+ // check if num_args > 2^sz
+ if (sz >= 32)
+ return BR_FAILED;
+ if (num_args <= 1u << sz)
+ return BR_FAILED;
+ result = m().mk_false();
+ return BR_DONE;
+}
+
br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) {
SASSERT(num == 2);
unsigned bv_sz;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 7f0c67540..88d952c06 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -180,7 +180,8 @@ public:
bool is_urem_any(expr * e, expr * & dividend, expr * & divisor);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
- br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul);
+ br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
+ br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);
bool hi_div0() const { return m_hi_div0; }
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 22d6a83b7..9cf9fc810 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -60,7 +60,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_substitution * m_subst = nullptr;
unsigned long long m_max_memory; // in bytes
bool m_new_subst = false;
- unsigned m_max_steps = UINT_MAX;
+ unsigned m_max_steps = UINT_MAX;
bool m_pull_cheap_ite = true;
bool m_flat = true;
bool m_cache_all = false;
@@ -180,7 +180,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = args[0]->get_sort()->get_family_id();
- if (s_fid == m_a_rw.get_fid())
+ if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_eq_core(args[0], args[1], result);
@@ -193,10 +193,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
- return st;
- }
- if (k == OP_EQ) {
- SASSERT(num == 2);
+ return st;
st = apply_tamagotchi(args[0], args[1], result);
if (st != BR_FAILED)
return st;
@@ -210,16 +207,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return st;
}
if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
- st = m_seq_rw.mk_bool_app(f, num, args, result);
+ st = m_seq_rw.mk_bool_app(f, num, args, result);
if (st != BR_FAILED)
return st;
}
- if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
+ if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
+ if (k == OP_DISTINCT && num > 0 && m_bv_rw.is_bv(args[0])) {
+ st = m_bv_rw.mk_distinct(num, args, result);
+ if (st != BR_FAILED)
+ return st;
+ }
return m_b_rw.mk_app_core(f, num, args, result);
}
@@ -250,7 +252,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (fid == m_seq_rw.get_fid())
return m_seq_rw.mk_app_core(f, num, args, result);
if (fid == m_char_rw.get_fid())
- return m_char_rw.mk_app_core(f, num, args, result);
+ return m_char_rw.mk_app_core(f, num, args, result);
if (fid == m_rec_rw.get_fid())
return m_rec_rw.mk_app_core(f, num, args, result);
return BR_FAILED;
diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp
index 5dc5f32fe..7ed5e8346 100644
--- a/src/ast/special_relations_decl_plugin.cpp
+++ b/src/ast/special_relations_decl_plugin.cpp
@@ -61,11 +61,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) {
if (logic == symbol::null) {
- op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO));
- op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
- op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
- op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
- op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC));
+ op_names.push_back(builtin_name(m_po.str(), OP_SPECIAL_RELATION_PO));
+ op_names.push_back(builtin_name(m_lo.str(), OP_SPECIAL_RELATION_LO));
+ op_names.push_back(builtin_name(m_plo.str(), OP_SPECIAL_RELATION_PLO));
+ op_names.push_back(builtin_name(m_to.str(), OP_SPECIAL_RELATION_TO));
+ op_names.push_back(builtin_name(m_tc.str(), OP_SPECIAL_RELATION_TC));
}
}
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index afe800af6..f3bd0ed57 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -58,7 +58,7 @@ public:
cmd * c = ctx.find_cmd(s);
if (c == nullptr) {
std::string err_msg("unknown command '");
- err_msg = err_msg + s.bare_str() + "'";
+ err_msg = err_msg + s.str() + "'";
throw cmd_exception(std::move(err_msg));
}
m_cmds.push_back(s);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 89efc439f..580cc2de4 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1636,6 +1636,7 @@ void cmd_context::pop(unsigned n) {
restore_aux_pdecls(s.m_aux_pdecls_lim);
restore_assertions(s.m_assertions_lim);
restore_psort_inst(s.m_psort_inst_stack_lim);
+ m_dt_eh.get()->reset();
m_mcs.shrink(m_mcs.size() - n);
m_scopes.shrink(new_lvl);
if (!m_global_decls)
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 4f9d80a8d..60a6e930b 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -267,6 +267,7 @@ protected:
cmd_context & m_owner;
datatype_util m_dt_util;
public:
+ void reset() { m_dt_util.reset(); }
dt_eh(cmd_context & owner);
~dt_eh() override;
void operator()(sort * dt, pdecl* pd) override;
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 7a93382e9..2bf21de3a 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -156,8 +156,8 @@ public:
return false;
return m_sort == static_cast(other)->m_sort;
}
- void display(std::ostream & out) const override {
- out << m_sort->get_name();
+ std::ostream& display(std::ostream & out) const override {
+ return out << m_sort->get_name();
}
};
@@ -180,8 +180,8 @@ public:
get_num_params() == other->get_num_params() &&
m_idx == static_cast(other)->m_idx;
}
- void display(std::ostream & out) const override {
- out << "s_" << m_idx;
+ std::ostream& display(std::ostream & out) const override {
+ return out << "s_" << m_idx;
}
unsigned idx() const { return m_idx; }
};
@@ -254,7 +254,7 @@ public:
}
return true;
}
- void display(std::ostream & out) const override {
+ std::ostream& display(std::ostream & out) const override {
if (m_args.empty()) {
out << m_decl->get_name();
}
@@ -267,6 +267,7 @@ public:
}
out << ")";
}
+ return out;
}
};
@@ -342,12 +343,12 @@ void display_sort_args(std::ostream & out, unsigned num_params) {
out << ") ";
}
-void psort_user_decl::display(std::ostream & out) const {
+std::ostream& psort_user_decl::display(std::ostream & out) const {
out << "(declare-sort " << m_name;
display_sort_args(out, m_num_params);
if (m_def)
m_def->display(out);
- out << ")";
+ return out << ")";
}
// -------------------
@@ -364,8 +365,8 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
return m.instantiate_datatype(this, m_name, n, s);
}
-void psort_dt_decl::display(std::ostream & out) const {
- out << "(datatype-sort " << m_name << ")";
+std::ostream& psort_dt_decl::display(std::ostream & out) const {
+ return out << "(datatype-sort " << m_name << ")";
}
// -------------------
@@ -410,8 +411,8 @@ sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned c
}
}
-void psort_builtin_decl::display(std::ostream & out) const {
- out << "(declare-builtin-sort " << m_name << ")";
+std::ostream& psort_builtin_decl::display(std::ostream & out) const {
+ return out << "(declare-builtin-sort " << m_name << ")";
}
void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const {
@@ -615,7 +616,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
}
-void pdatatype_decl::display(std::ostream & out) const {
+std::ostream& pdatatype_decl::display(std::ostream & out) const {
out << "(declare-datatype " << m_name;
display_sort_args(out, m_num_params);
bool first = true;
@@ -631,7 +632,7 @@ void pdatatype_decl::display(std::ostream & out) const {
}
first = false;
}
- out << ")";
+ return out << ")";
}
bool pdatatype_decl::commit(pdecl_manager& m) {
@@ -645,9 +646,11 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.data(), sorts);
+ m.notify_mk_datatype(m_name);
if (is_ok && m_num_params == 0) {
m.notify_new_dt(sorts.get(0), this);
}
+
return is_ok;
}
@@ -722,6 +725,7 @@ void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* co
void pdecl_manager::push() {
m_notified_lim.push_back(m_notified_trail.size());
+ m_datatypes_lim.push_back(m_datatypes_trail.size());
}
void pdecl_manager::pop(unsigned n) {
@@ -732,6 +736,16 @@ void pdecl_manager::pop(unsigned n) {
}
m_notified_trail.shrink(new_sz);
m_notified_lim.shrink(m_notified_lim.size() - n);
+
+ new_sz = m_datatypes_lim[m_datatypes_lim.size() - n];
+ if (new_sz != m_datatypes_trail.size()) {
+ datatype_util util(m());
+ for (unsigned i = m_datatypes_trail.size(); i-- > new_sz; )
+ util.plugin().remove(m_datatypes_trail[i]);
+ }
+ m_datatypes_trail.shrink(new_sz);
+ m_datatypes_lim.shrink(m_datatypes_lim.size() - n);
+
}
bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
@@ -751,16 +765,24 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.data(), 0, nullptr, sorts);
if (is_ok) {
+ for (pdatatype_decl* d : m_datatypes) {
+ m.notify_mk_datatype(d->get_name());
+ }
for (unsigned i = 0; i < m_datatypes.size(); ++i) {
pdatatype_decl* d = m_datatypes[i];
- if (d->get_num_params() == 0) {
+ if (d->get_num_params() == 0)
m.notify_new_dt(sorts.get(i), this);
- }
}
}
+
return is_ok;
}
+void pdecl_manager::notify_mk_datatype(symbol const& name) {
+ m_datatypes_trail.push_back(name);
+}
+
+
struct pdecl_manager::sort_info {
psort_decl * m_decl;
@@ -985,16 +1007,19 @@ void pdecl_manager::del_decl_core(pdecl * p) {
}
void pdecl_manager::del_decl(pdecl * p) {
- TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);
+ TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);
if (p->is_psort()) {
psort * _p = static_cast(p);
if (_p->is_sort_wrapper()) {
- m_sort2psort.erase(static_cast(_p)->get_sort());
+ sort* s = static_cast(_p)->get_sort();
+ m_sort2psort.erase(s);
}
else {
m_table.erase(_p);
}
+
}
+
del_decl_core(p);
}
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 3a1db06c1..4f9c56825 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -45,7 +45,7 @@ public:
unsigned get_id() const { return m_id; }
unsigned get_ref_count() const { return m_ref_count; }
unsigned hash() const { return m_id; }
- virtual void display(std::ostream & out) const {}
+ virtual std::ostream& display(std::ostream & out) const { return out;}
virtual void reset_cache(pdecl_manager& m) {}
};
@@ -123,7 +123,7 @@ protected:
~psort_user_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
- void display(std::ostream & out) const override;
+ std::ostream& display(std::ostream & out) const override;
};
class psort_builtin_decl : public psort_decl {
@@ -137,7 +137,7 @@ protected:
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override;
- void display(std::ostream & out) const override;
+ std::ostream& display(std::ostream & out) const override;
};
class psort_dt_decl : public psort_decl {
@@ -148,7 +148,7 @@ protected:
~psort_dt_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
- void display(std::ostream & out) const override;
+ std::ostream& display(std::ostream & out) const override;
};
@@ -198,7 +198,7 @@ class paccessor_decl : public pdecl {
ptype const & get_type() const { return m_type; }
~paccessor_decl() override {}
public:
- void display(std::ostream & out) const override { pdecl::display(out); }
+ std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};
@@ -219,7 +219,7 @@ class pconstructor_decl : public pdecl {
constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pconstructor_decl() override {}
public:
- void display(std::ostream & out) const override { pdecl::display(out); }
+ std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};
@@ -237,7 +237,7 @@ class pdatatype_decl : public psort_decl {
~pdatatype_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
- void display(std::ostream & out) const override;
+ std::ostream& display(std::ostream & out) const override;
bool has_missing_refs(symbol & missing) const;
bool has_duplicate_accessors(symbol & repeated) const;
bool commit(pdecl_manager& m);
@@ -289,6 +289,8 @@ class pdecl_manager {
obj_hashtable m_notified;
ptr_vector m_notified_trail;
unsigned_vector m_notified_lim;
+ svector m_datatypes_trail;
+ unsigned_vector m_datatypes_lim;
void init_list();
void del_decl_core(pdecl * p);
@@ -319,6 +321,7 @@ public:
sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s);
sort * instantiate(psort * s, unsigned num, sort * const * args);
void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s);
+ void notify_mk_datatype(symbol const& name);
void push();
void pop(unsigned n);
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index 899ec497c..030d88d71 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -777,6 +777,7 @@ protected:
// Sym ::= String | NUM | Var
//
dtoken parse_infix(dtoken tok1, char const* td, app_ref& pred) {
+ std::string td1_(td);
symbol td1(td);
expr_ref v1(m), v2(m);
sort* s = nullptr;
@@ -793,12 +794,12 @@ protected:
if (tok1 == TK_ID) {
expr* _v1 = nullptr;
- m_vars.find(td1.bare_str(), _v1);
+ m_vars.find(td1_, _v1);
v1 = _v1;
}
if (tok3 == TK_ID) {
expr* _v2 = nullptr;
- m_vars.find(td2.bare_str(), _v2);
+ m_vars.find(td, _v2);
v2 = _v2;
}
if (!v1 && !v2) {
@@ -950,18 +951,19 @@ protected:
break;
}
case TK_ID: {
- symbol data (m_lexer->get_token_data());
- if (is_var(data.bare_str())) {
+ char const* d = m_lexer->get_token_data();
+ symbol data (d);
+ if (is_var(d)) {
unsigned idx = 0;
expr* v = nullptr;
- if (!m_vars.find(data.bare_str(), v)) {
+ if (!m_vars.find(d, v)) {
idx = m_num_vars++;
v = m.mk_var(idx, s);
- m_vars.insert(data.bare_str(), v);
+ m_vars.insert(d, v);
}
else if (s != v->get_sort()) {
throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n",
- s->get_name().bare_str(), v->get_sort()->get_name().bare_str());
+ s->get_name().str().c_str(), v->get_sort()->get_name().str().c_str());
}
args.push_back(v);
}
@@ -1075,21 +1077,21 @@ protected:
}
sort * register_finite_sort(symbol name, uint64_t domain_size, context::sort_kind k) {
- if(m_sort_dict.contains(name.bare_str())) {
- throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
+ if(m_sort_dict.contains(name.str().c_str())) {
+ throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str());
}
sort * s = m_decl_util.mk_sort(name, domain_size);
m_context.register_finite_sort(s, k);
- m_sort_dict.insert(name.bare_str(), s);
+ m_sort_dict.insert(name.str(), s);
return s;
}
sort * register_int_sort(symbol name) {
- if(m_sort_dict.contains(name.bare_str())) {
- throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
+ if(m_sort_dict.contains(name.str().c_str())) {
+ throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str());
}
sort * s = m_arith.mk_int();
- m_sort_dict.insert(name.bare_str(), s);
+ m_sort_dict.insert(name.str(), s);
return s;
}
@@ -1105,8 +1107,8 @@ protected:
app * res;
if(m_arith.is_int(s)) {
uint64_t val;
- if (!string_to_uint64(name.bare_str(), val)) {
- throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.bare_str());
+ if (!string_to_uint64(name.str().c_str(), val)) {
+ throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.str().c_str());
}
res = m_arith.mk_numeral(rational(val, rational::ui64()), s);
}
@@ -1288,7 +1290,7 @@ private:
uint64_set & sort_content = *e->get_data().m_value;
if(!sort_content.contains(num)) {
warning_msg("symbol number %I64u on line %d in file %s does not belong to sort %s",
- num, m_current_line, m_current_file.c_str(), s->get_name().bare_str());
+ num, m_current_line, m_current_file.c_str(), s->get_name().str().c_str());
return false;
}
if(!m_use_map_names) {
@@ -1366,7 +1368,7 @@ private:
func_decl * pred = m_context.try_get_predicate_decl(predicate_name);
if(!pred) {
throw default_exception(default_exception::fmt(), "tuple file %s for undeclared predicate %s",
- m_current_file.c_str(), predicate_name.bare_str());
+ m_current_file.c_str(), predicate_name.str().c_str());
}
unsigned pred_arity = pred->get_arity();
sort * const * arg_sorts = pred->get_domain();
@@ -1531,9 +1533,9 @@ private:
if(m_use_map_names) {
auto const & value = m_number_names.insert_if_not_there(num, el_name);
- if (value!=el_name) {
+ if (value != el_name) {
warning_msg("mismatch of number names on line %d in file %s. old: \"%s\" new: \"%s\"",
- m_current_line, fname.c_str(), value.bare_str(), el_name.bare_str());
+ m_current_line, fname.c_str(), value.str().c_str(), el_name.str().c_str());
}
}
}
diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp
index 8a4b86e6d..07921a3be 100644
--- a/src/muz/rel/dl_finite_product_relation.cpp
+++ b/src/muz/rel/dl_finite_product_relation.cpp
@@ -64,7 +64,7 @@ namespace datalog {
}
symbol finite_product_relation_plugin::get_name(relation_plugin & inner_plugin) {
- std::string str = std::string("fpr_")+inner_plugin.get_name().bare_str();
+ std::string str = std::string("fpr_")+inner_plugin.get_name().str();
return symbol(str.c_str());
}
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 0df03172f..63846e7d5 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -213,10 +213,10 @@ namespace datalog {
return true;
}
void make_annotations(execution_context & ctx) override {
- ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str());
+ ctx.set_register_annotation(m_reg, m_pred->get_name().str().c_str());
}
std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
- const char * rel_name = m_pred->get_name().bare_str();
+ auto rel_name = m_pred->get_name();
if (m_store) {
return out << "store " << m_reg << " into " << rel_name;
}
@@ -378,7 +378,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported join operation on relations of kinds %s and %s",
- r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
+ r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str());
}
store_fn(r1, r2, fn);
}
@@ -441,7 +441,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported filter_equal operation on a relation of kind %s",
- r.get_plugin().get_name().bare_str());
+ r.get_plugin().get_name().str().c_str());
}
store_fn(r, fn);
}
@@ -490,7 +490,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported filter_identical operation on a relation of kind %s",
- r.get_plugin().get_name().bare_str());
+ r.get_plugin().get_name().str().c_str());
}
store_fn(r, fn);
}
@@ -537,7 +537,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported filter_interpreted operation on a relation of kind %s",
- r.get_plugin().get_name().bare_str());
+ r.get_plugin().get_name().str().c_str());
}
store_fn(r, fn);
}
@@ -594,7 +594,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s",
- reg.get_plugin().get_name().bare_str());
+ reg.get_plugin().get_name().str().c_str());
}
store_fn(reg, fn);
}
@@ -837,7 +837,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported join-project operation on relations of kinds %s and %s",
- r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
+ r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str());
}
store_fn(r1, r2, fn);
}
@@ -910,7 +910,7 @@ namespace datalog {
if (!fn) {
throw default_exception(default_exception::fmt(),
"trying to perform unsupported select_equal_and_project operation on a relation of kind %s",
- r.get_plugin().get_name().bare_str());
+ r.get_plugin().get_name().str().c_str());
}
store_fn(r, fn);
}
@@ -1076,7 +1076,7 @@ namespace datalog {
return true;
}
std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
- return out << "mark_saturated " << m_pred->get_name().bare_str();
+ return out << "mark_saturated " << m_pred->get_name();
}
void make_annotations(execution_context & ctx) override {
}
diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp
index de55998f8..8a69f8f85 100644
--- a/src/muz/rel/dl_table_relation.cpp
+++ b/src/muz/rel/dl_table_relation.cpp
@@ -33,7 +33,7 @@ namespace datalog {
// -----------------------------------
symbol table_relation_plugin::create_plugin_name(const table_plugin &p) {
- std::string name = std::string("tr_") + p.get_name().bare_str();
+ std::string name = std::string("tr_") + p.get_name().str();
return symbol(name.c_str());
}
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 957c85adb..76411a290 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -157,7 +157,7 @@ namespace datalog {
//IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream()););
if (m_context.print_aig().is_non_empty_string()) {
- const char *filename = m_context.print_aig().bare_str();
+ std::string filename = m_context.print_aig().str();
aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts);
std::ofstream strm(filename, std::ios_base::binary);
aig(strm);
diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt
index d88d11c0f..c652bcaea 100644
--- a/src/opt/CMakeLists.txt
+++ b/src/opt/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(opt
opt_lns.cpp
opt_pareto.cpp
opt_parse.cpp
+ opt_preprocess.cpp
optsmt.cpp
opt_solver.cpp
pb_sls.cpp
diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 46c7104d5..fa97359d0 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -26,15 +26,15 @@ Author:
namespace opt {
- bool is_maxlex(weights_t & _ws) {
- vector ws(_ws);
- std::sort(ws.begin(), ws.end());
+ bool is_maxlex(vector const & _ws) {
+ vector ws(_ws);
+ std::sort(ws.begin(), ws.end(), [&](soft const& s1, soft const& s2) { return s1.weight < s2.weight; });
ws.reverse();
rational sum(0);
- for (rational const& w : ws) {
+ for (auto const& [e, w, t] : ws) {
sum += w;
}
- for (rational const& w : ws) {
+ for (auto const& [e, w, t] : ws) {
if (sum > w + w) return false;
sum -= w;
}
@@ -185,8 +185,8 @@ namespace opt {
public:
- maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
- maxsmt_solver_base(c, ws, s),
+ maxlex(maxsat_context& c, unsigned id, vector& s):
+ maxsmt_solver_base(c, s, id),
m(c.get_manager()),
m_c(c) {
// ensure that soft constraints are sorted with largest soft constraints first.
@@ -210,8 +210,8 @@ namespace opt {
}
};
- maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) {
- return alloc(maxlex, c, id, ws, soft);
+ maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector& soft) {
+ return alloc(maxlex, c, id, soft);
}
}
diff --git a/src/opt/maxlex.h b/src/opt/maxlex.h
index b5c1a6e20..fc30b1fd8 100644
--- a/src/opt/maxlex.h
+++ b/src/opt/maxlex.h
@@ -21,9 +21,9 @@ Notes:
namespace opt {
- bool is_maxlex(weights_t & ws);
+ bool is_maxlex(vector const & ws);
- maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+ maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector& soft);
};
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 27b3b7260..135e0f80e 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -95,7 +95,6 @@ private:
expr_ref_vector const& soft() override { return i.m_asms; }
};
- unsigned m_index;
stats m_stats;
expr_ref_vector m_B;
expr_ref_vector m_asms;
@@ -129,11 +128,10 @@ private:
typedef ptr_vector exprs;
public:
- maxres(maxsat_context& c, unsigned index,
- weights_t& ws, expr_ref_vector const& soft,
+ maxres(maxsat_context& c, unsigned index,
+ vector& soft,
strategy_t st):
- maxsmt_solver_base(c, ws, soft),
- m_index(index),
+ maxsmt_solver_base(c, soft, index),
m_B(m), m_asms(m), m_defs(m),
m_new_core(m),
m_mus(c.get_solver()),
@@ -791,11 +789,10 @@ public:
improve_model(mdl);
mdl->set_model_completion(true);
unsigned correction_set_size = 0;
- for (expr* a : m_asms) {
- if (mdl->is_false(a)) {
+ for (expr* a : m_asms)
+ if (mdl->is_false(a))
++correction_set_size;
- }
- }
+
if (!m_csmodel.get() || correction_set_size < m_correction_set_size) {
m_csmodel = mdl;
m_correction_set_size = correction_set_size;
@@ -810,22 +807,22 @@ public:
return;
}
- if (!m_c.verify_model(m_index, mdl.get(), upper)) {
+ if (!m_c.verify_model(m_index, mdl.get(), upper))
return;
- }
+ unsigned num_assertions = s().get_num_assertions();
m_model = mdl;
m_c.model_updated(mdl.get());
TRACE("opt", tout << "updated upper: " << upper << "\n";);
- for (soft& s : m_soft) {
+ for (soft& s : m_soft)
s.set_value(m_model->is_true(s.s));
- }
verify_assignment();
- m_upper = upper;
+ if (num_assertions == s().get_num_assertions())
+ m_upper = upper;
trace();
@@ -876,17 +873,10 @@ public:
}
lbool init_local() {
- m_lower.reset();
m_trail.reset();
lbool is_sat = l_true;
- obj_map new_soft;
- is_sat = find_mutexes(new_soft);
- if (is_sat != l_true) {
- return is_sat;
- }
- for (auto const& kv : new_soft) {
- add_soft(kv.m_key, kv.m_value);
- }
+ for (auto const& [e, w, t] : m_soft)
+ add_soft(e, w);
m_max_upper = m_upper;
m_found_feasible_optimum = false;
m_last_index = 0;
@@ -954,12 +944,12 @@ public:
};
opt::maxsmt_solver_base* opt::mk_maxres(
- maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
- return alloc(maxres, c, id, ws, soft, maxres::s_primal);
+ maxsat_context& c, unsigned id, vector& soft) {
+ return alloc(maxres, c, id, soft, maxres::s_primal);
}
opt::maxsmt_solver_base* opt::mk_primal_dual_maxres(
- maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
- return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual);
+ maxsat_context& c, unsigned id, vector& soft) {
+ return alloc(maxres, c, id, soft, maxres::s_primal_dual);
}
diff --git a/src/opt/maxres.h b/src/opt/maxres.h
index 85c83efba..25ef9bf05 100644
--- a/src/opt/maxres.h
+++ b/src/opt/maxres.h
@@ -21,9 +21,9 @@ Notes:
namespace opt {
- maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+ maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector& soft);
- maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+ maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector& soft);
};
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 6a8a2ee35..a3d5f2f45 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -28,29 +28,34 @@ Notes:
#include "opt/wmax.h"
#include "opt/opt_params.hpp"
#include "opt/opt_context.h"
+#include "opt/opt_preprocess.h"
#include "smt/theory_wmaxsat.h"
#include "smt/theory_pb.h"
namespace opt {
- maxsmt_solver_base::maxsmt_solver_base(
- maxsat_context& c, vector const& ws, expr_ref_vector const& softs):
+ maxsmt_solver_base::maxsmt_solver_base(maxsat_context& c, vector& s, unsigned index):
m(c.get_manager()),
m_c(c),
+ m_index(index),
+ m_soft(s),
m_assertions(m),
m_trail(m) {
c.get_base_model(m_model);
SASSERT(m_model);
updt_params(c.params());
- for (unsigned i = 0; i < ws.size(); ++i) {
- m_soft.push_back(soft(expr_ref(softs.get(i), m), ws[i], false));
- }
}
void maxsmt_solver_base::updt_params(params_ref& p) {
m_params.copy(p);
- }
+ }
+
+ void maxsmt_solver_base::reset_upper() {
+ m_upper = m_lower;
+ for (soft& s : m_soft)
+ m_upper += s.weight;
+ }
solver& maxsmt_solver_base::s() {
return m_c.get_solver();
@@ -82,14 +87,24 @@ namespace opt {
m_upper.reset();
for (soft& s : m_soft) {
s.set_value(m.is_true(s.s));
- if (!s.is_true()) m_upper += s.weight;
+ if (!s.is_true())
+ m_upper += s.weight;
}
+
+ // return true;
+
+ preprocess pp(s());
+ rational lower(0);
+ bool r = pp(m_soft, lower);
+
+ m_c.add_offset(m_index, lower);
+ m_upper -= lower;
TRACE("opt",
- tout << "upper: " << m_upper << " assignments: ";
+ tout << "lower " << lower << " upper: " << m_upper << " assignments: ";
for (soft& s : m_soft) tout << (s.is_true()?"T":"F");
tout << "\n";);
- return true;
+ return r;
}
void maxsmt_solver_base::set_mus(bool f) {
@@ -153,80 +168,15 @@ namespace opt {
void maxsmt_solver_base::trace_bounds(char const * solver) {
IF_VERBOSE(1,
- rational l = m_adjust_value(m_lower);
- rational u = m_adjust_value(m_upper);
+ rational l = m_c.adjust(m_index, m_lower);
+ rational u = m_c.adjust(m_index, m_upper);
if (l > u) std::swap(l, u);
verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);
}
- lbool maxsmt_solver_base::find_mutexes(obj_map& new_soft) {
- m_lower.reset();
- expr_ref_vector fmls(m);
- for (soft& s : m_soft) {
- new_soft.insert(s.s, s.weight);
- fmls.push_back(s.s);
- }
- vector mutexes;
- lbool is_sat = s().find_mutexes(fmls, mutexes);
- if (is_sat != l_true) {
- return is_sat;
- }
- for (auto& mux : mutexes) {
- process_mutex(mux, new_soft);
- }
- return l_true;
- }
-
- struct maxsmt_compare_soft {
- obj_map const& m_soft;
- maxsmt_compare_soft(obj_map const& soft): m_soft(soft) {}
- bool operator()(expr* a, expr* b) const {
- return m_soft.find(a) > m_soft.find(b);
- }
- };
-
- void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map& new_soft) {
- TRACE("opt",
- for (expr* e : mutex) {
- tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
- });
- if (mutex.size() <= 1) {
- return;
- }
- maxsmt_compare_soft cmp(new_soft);
- ptr_vector _mutex(mutex.size(), mutex.data());
- std::sort(_mutex.begin(), _mutex.end(), cmp);
- mutex.reset();
- mutex.append(_mutex.size(), _mutex.data());
-
- rational weight(0), sum1(0), sum2(0);
- vector weights;
- for (expr* e : mutex) {
- rational w = new_soft.find(e);
- weights.push_back(w);
- sum1 += w;
- new_soft.remove(e);
- }
- for (unsigned i = mutex.size(); i-- > 0; ) {
- expr_ref soft(m.mk_or(i+1, mutex.data()), m);
- m_trail.push_back(soft);
- rational w = weights[i];
- weight = w - weight;
- m_lower += weight*rational(i);
- IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
- sum2 += weight*rational(i+1);
- new_soft.insert(soft, weight);
- for (; i > 0 && weights[i-1] == w; --i) {}
- weight = w;
- }
- SASSERT(sum1 == sum2);
- }
-
-
maxsmt::maxsmt(maxsat_context& c, unsigned index):
- m(c.get_manager()), m_c(c), m_index(index),
- m_soft_constraints(m), m_answer(m) {}
+ m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {}
lbool maxsmt::operator()() {
lbool is_sat = l_undef;
@@ -235,30 +185,29 @@ namespace opt {
symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
- if (optp.maxlex_enable() && is_maxlex(m_weights)) {
- m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
+ if (optp.maxlex_enable() && is_maxlex(m_soft)) {
+ m_msolver = mk_maxlex(m_c, m_index, m_soft);
}
- else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
- m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+ else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
+ m_msolver = mk_maxres(m_c, m_index, m_soft);
}
else if (maxsat_engine == symbol("pd-maxres")) {
- m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
+ m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft);
}
else if (maxsat_engine == symbol("wmax")) {
- m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
+ m_msolver = mk_wmax(m_c, m_soft, m_index);
}
else if (maxsat_engine == symbol("sortmax")) {
- m_msolver = mk_sortmax(m_c, m_weights, m_soft_constraints);
+ m_msolver = mk_sortmax(m_c, m_soft, m_index);
}
else {
auto str = maxsat_engine.str();
warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str());
- m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+ m_msolver = mk_maxres(m_c, m_index, m_soft);
}
if (m_msolver) {
m_msolver->updt_params(m_params);
- m_msolver->set_adjust_value(m_adjust_value);
is_sat = l_undef;
try {
is_sat = (*m_msolver)();
@@ -282,14 +231,13 @@ namespace opt {
return is_sat;
}
- void maxsmt::set_adjust_value(adjust_value& adj) {
- m_adjust_value = adj;
+ void maxsmt::reset_upper() {
if (m_msolver) {
- m_msolver->set_adjust_value(m_adjust_value);
+ m_msolver->reset_upper();
+ m_upper = m_msolver->get_upper();
}
}
-
void maxsmt::verify_assignment() {
// TBD: have to use a different solver
// because we don't push local scope any longer.
@@ -311,7 +259,7 @@ namespace opt {
rational q = m_msolver->get_lower();
if (q > r) r = q;
}
- return m_adjust_value(r);
+ return m_c.adjust(m_index, r);
}
rational maxsmt::get_upper() const {
@@ -320,7 +268,7 @@ namespace opt {
rational q = m_msolver->get_upper();
if (q < r) r = q;
}
- return m_adjust_value(r);
+ return m_c.adjust(m_index, r);
}
void maxsmt::update_lower(rational const& r) {
@@ -348,39 +296,32 @@ namespace opt {
SASSERT(w.is_pos());
unsigned index = 0;
if (m_soft_constraint_index.find(f, index)) {
- m_weights[index] += w;
+ m_soft[index].weight += w;
}
else {
- m_soft_constraint_index.insert(f, m_weights.size());
- m_soft_constraints.push_back(f);
- m_weights.push_back(w);
+ m_soft_constraint_index.insert(f, m_soft.size());
+ m_soft.push_back(soft(expr_ref(f, m), w, false));
}
m_upper += w;
}
struct cmp_first {
bool operator()(std::pair const& x, std::pair const& y) const {
- return x.first < y.first;
+ return x.second < y.second;
}
};
void maxsmt::display_answer(std::ostream& out) const {
- vector> sorted_weights;
- unsigned n = m_weights.size();
- for (unsigned i = 0; i < n; ++i) {
- sorted_weights.push_back(std::make_pair(i, m_weights[i]));
- }
- std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first());
- sorted_weights.reverse();
- for (unsigned i = 0; i < n; ++i) {
- unsigned idx = sorted_weights[i].first;
- expr* e = m_soft_constraints[idx];
+
+ unsigned idx = 0;
+ for (auto const & [_e, w, t] : m_soft) {
+ expr* e = _e.get();
bool is_not = m.is_not(e, e);
- out << m_weights[idx] << ": " << mk_pp(e, m)
+ out << w << ": " << mk_pp(e, m)
<< ((is_not != get_assignment(idx))?" |-> true ":" |-> false ")
<< "\n";
-
- }
+ ++idx;
+ }
}
@@ -420,6 +361,7 @@ namespace opt {
model_ref m_model;
ref m_fm;
symbol m_maxsat_engine;
+ vector m_offsets;
public:
solver_maxsat_context(params_ref& p, solver* s, model * m):
m_params(p),
@@ -444,6 +386,14 @@ namespace opt {
bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; };
void set_model(model_ref& _m) override { m_model = _m; }
void model_updated(model* mdl) override { } // no-op
+ rational adjust(unsigned id, rational const& r) override {
+ m_offsets.reserve(id+1);
+ return r + m_offsets[id];
+ }
+ void add_offset(unsigned id, rational const& r) override {
+ m_offsets.reserve(id+1);
+ m_offsets[id] += r;
+ }
};
lbool maxsmt_wrapper::operator()(vector>& soft) {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index ad355cc9e..b0ae5eeb1 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -34,8 +34,6 @@ namespace opt {
class maxsat_context;
class maxsmt_solver {
- protected:
- adjust_value m_adjust_value;
public:
virtual ~maxsmt_solver() {}
virtual lbool operator()() = 0;
@@ -45,28 +43,30 @@ namespace opt {
virtual void collect_statistics(statistics& st) const = 0;
virtual void get_model(model_ref& mdl, svector& labels) = 0;
virtual void updt_params(params_ref& p) = 0;
- void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
};
// ---------------------------------------------
// base class with common utilities used
// by maxsmt solvers
- //
+ //
+
+ struct soft {
+ expr_ref s;
+ rational weight;
+ lbool value;
+ void set_value(bool t) { value = t?l_true:l_undef; }
+ void set_value(lbool t) { value = t; }
+ bool is_true() const { return value == l_true; }
+ soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
+ };
+
class maxsmt_solver_base : public maxsmt_solver {
protected:
- struct soft {
- expr_ref s;
- rational weight;
- lbool value;
- void set_value(bool t) { value = t?l_true:l_undef; }
- void set_value(lbool t) { value = t; }
- bool is_true() const { return value == l_true; }
- soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
- };
ast_manager& m;
- maxsat_context& m_c;
- vector m_soft;
+ maxsat_context& m_c;
+ unsigned m_index;
+ vector& m_soft;
expr_ref_vector m_assertions;
expr_ref_vector m_trail;
rational m_lower;
@@ -76,8 +76,8 @@ namespace opt {
params_ref m_params; // config
public:
- maxsmt_solver_base(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft);
-
+ maxsmt_solver_base(maxsat_context& c, vector& soft, unsigned index);
+
~maxsmt_solver_base() override {}
rational get_lower() const override { return m_lower; }
rational get_upper() const override { return m_upper; }
@@ -102,16 +102,13 @@ namespace opt {
smt::theory_wmaxsat& operator()();
};
- lbool find_mutexes(obj_map& new_soft);
+ void reset_upper();
protected:
void enable_sls(bool force);
void trace_bounds(char const* solver);
- void process_mutex(expr_ref_vector& mutex, obj_map& new_soft);
-
-
};
/**
@@ -124,13 +121,11 @@ namespace opt {
maxsat_context& m_c;
unsigned m_index;
scoped_ptr m_msolver;
- expr_ref_vector m_soft_constraints;
+ vector m_soft;
obj_map m_soft_constraint_index;
expr_ref_vector m_answer;
- vector m_weights;
rational m_lower;
rational m_upper;
- adjust_value m_adjust_value;
model_ref m_model;
svector m_labels;
params_ref m_params;
@@ -139,10 +134,9 @@ namespace opt {
lbool operator()();
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
- void set_adjust_value(adjust_value& adj);
- unsigned size() const { return m_soft_constraints.size(); }
- expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
- rational weight(unsigned idx) const { return m_weights[idx]; }
+ unsigned size() const { return m_soft.size(); }
+ expr* operator[](unsigned idx) const { return m_soft[idx].s; }
+ rational weight(unsigned idx) const { return m_soft[idx].weight; }
void commit_assignment();
rational get_lower() const;
rational get_upper() const;
@@ -153,6 +147,7 @@ namespace opt {
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;
void model_updated(model* mdl);
+ void reset_upper();
private:
bool is_maxsat_problem(weights_t& ws) const;
void verify_assignment();
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 3551686f7..25982e89e 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -185,17 +185,36 @@ namespace opt {
}
void context::set_hard_constraints(expr_ref_vector const& fmls) {
- if (m_scoped_state.set(fmls)) {
+ if (m_calling_on_model) {
+ for (expr* f : fmls)
+ add_hard_constraint(f);
+ return;
+ }
+ if (m_scoped_state.set(fmls))
+ clear_state();
+ }
+
+ void context::add_hard_constraint(expr* f) {
+ if (m_calling_on_model) {
+ get_solver().assert_expr(f);
+ for (auto const& [k, v] : m_maxsmts)
+ v->reset_upper();
+ for (unsigned i = 0; i < num_objectives(); ++i) {
+ auto const& o = m_scoped_state.m_objectives[i];
+ if (o.m_type != O_MAXSMT)
+ m_optsmt.update_upper(o.m_index, inf_eps::infinity());
+ }
+ }
+ else {
+ m_scoped_state.add(f);
clear_state();
}
}
-
- void context::add_hard_constraint(expr* f) {
- m_scoped_state.add(f);
- clear_state();
- }
+
void context::add_hard_constraint(expr* f, expr* t) {
+ if (m_calling_on_model)
+ throw default_exception("adding soft constraints is not supported during callbacks");
m_scoped_state.m_asms.push_back(t);
m_scoped_state.add(m.mk_implies(t, f));
clear_state();
@@ -379,7 +398,7 @@ namespace opt {
}
void context::set_model(model_ref& m) {
- m_model = m;
+ m_model = m;
opt_params optp(m_params);
if (optp.dump_models() && m) {
model_ref md = m->copy();
@@ -389,6 +408,7 @@ namespace opt {
model_ref md = m->copy();
if (!m_model_fixed.contains(md.get()))
fix_model(md);
+ flet _calling(m_calling_on_model, true);
m_on_model_eh(m_on_model_ctx, md);
m_model_fixed.pop_back();
}
@@ -910,7 +930,8 @@ namespace opt {
bool context::is_maxsat(expr* fml, expr_ref_vector& terms,
vector& weights, rational& offset,
bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
- if (!is_app(fml)) return false;
+ if (!is_app(fml))
+ return false;
neg = false;
orig_term = nullptr;
index = 0;
@@ -1085,8 +1106,7 @@ namespace opt {
obj.m_weights.append(weights);
obj.m_adjust_value.set_offset(offset);
obj.m_adjust_value.set_negate(neg);
- m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
- TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";
+ TRACE("opt", tout << "maxsat: " << neg << " " << id << " offset: " << offset << "\n";
tout << terms << "\n";);
}
else if (is_maximize(fml, tr, orig_term, index)) {
@@ -1138,7 +1158,14 @@ namespace opt {
#endif
}
+ rational context::adjust(unsigned id, rational const& v) {
+ return m_objectives[id].m_adjust_value(v);
+ }
+ void context::add_offset(unsigned id, rational const& o) {
+ m_objectives[id].m_adjust_value.add_offset(o);
+ }
+
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
app_ref term = m_objectives[index].m_term;
@@ -1321,24 +1348,21 @@ namespace opt {
break;
}
case O_MAXSMT: {
- bool ok = true;
- for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) {
+ for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
val = (*m_model)(obj.m_terms[j]);
TRACE("opt", tout << mk_pp(obj.m_terms[j], m) << " " << val << "\n";);
- if (!m.is_true(val)) {
+ if (!m.is_true(val))
r += obj.m_weights[j];
- }
}
- if (ok) {
- maxsmt& ms = *m_maxsmts.find(obj.m_id);
- if (is_lower) {
- ms.update_upper(r);
- TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";);
- }
- else {
- ms.update_lower(r);
- TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";);
- }
+
+ maxsmt& ms = *m_maxsmts.find(obj.m_id);
+ if (is_lower) {
+ ms.update_upper(r);
+ TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";);
+ }
+ else {
+ ms.update_lower(r);
+ TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";);
}
break;
}
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index dd717c392..c02689a38 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -57,6 +57,8 @@ namespace opt {
virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
virtual unsigned num_objectives() = 0;
virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
+ virtual rational adjust(unsigned id, rational const& v) = 0;
+ virtual void add_offset(unsigned id, rational const& o) = 0;
virtual void set_model(model_ref& _m) = 0;
virtual void model_updated(model* mdl) = 0;
};
@@ -93,7 +95,7 @@ namespace opt {
app_ref m_term; // for maximize, minimize term
expr_ref_vector m_terms; // for maxsmt
vector m_weights; // for maxsmt
- adjust_value m_adjust_value;
+ adjust_value m_adjust_value;
symbol m_id; // for maxsmt
unsigned m_index; // for maximize/minimize index
@@ -165,6 +167,7 @@ namespace opt {
ast_manager& m;
on_model_t m_on_model_ctx;
std::function m_on_model_eh;
+ bool m_calling_on_model = false;
arith_util m_arith;
bv_util m_bv;
expr_ref_vector m_hard_constraints;
@@ -268,11 +271,14 @@ namespace opt {
void model_updated(model* mdl) override;
+ rational adjust(unsigned id, rational const& v) override;
+
+ void add_offset(unsigned id, rational const& o) override;
+
void register_on_model(on_model_t& ctx, std::function& on_model) {
m_on_model_ctx = ctx;
m_on_model_eh = on_model;
}
-
void collect_timer_stats(statistics& st) const {
if (m_time != 0)
diff --git a/src/opt/opt_mux.h b/src/opt/opt_mux.h
new file mode 100644
index 000000000..b093026f0
--- /dev/null
+++ b/src/opt/opt_mux.h
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+ opt_mux.h
+
+Abstract:
+
+ Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+ class mux {
+ ast_manager& m;
+ solver& s;
+
+ public:
+ mux(solver& s);
+ lbool operator()(vector& soft, rational& bound);
+ };
+};
diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp
new file mode 100644
index 000000000..f65d5d09b
--- /dev/null
+++ b/src/opt/opt_preprocess.cpp
@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+ opt_preprocess.cpp
+
+Abstract:
+
+ Pre-processing for MaxSMT
+
+ Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/opt_preprocess.h"
+
+namespace opt {
+
+ bool preprocess::find_mutexes(vector& softs, rational& lower) {
+ expr_ref_vector fmls(m);
+ obj_map new_soft;
+ for (soft& sf : softs) {
+ m_trail.push_back(sf.s);
+ if (new_soft.contains(sf.s))
+ new_soft[sf.s] += sf.weight;
+ else
+ new_soft.insert(sf.s, sf.weight);
+ fmls.push_back(sf.s);
+ }
+ vector mutexes;
+ lbool is_sat = s.find_mutexes(fmls, mutexes);
+ if (is_sat == l_false)
+ return true;
+ if (is_sat == l_undef)
+ return false;
+ for (auto& mux : mutexes)
+ process_mutex(mux, new_soft, lower);
+ softs.reset();
+ for (auto const& [k, v] : new_soft)
+ softs.push_back(soft(expr_ref(k, m), v, false));
+ m_trail.reset();
+ return true;
+ }
+
+ struct maxsmt_compare_soft {
+ obj_map const& m_soft;
+ maxsmt_compare_soft(obj_map const& soft): m_soft(soft) {}
+ bool operator()(expr* a, expr* b) const {
+ return m_soft.find(a) > m_soft.find(b);
+ }
+ };
+
+ void preprocess::process_mutex(expr_ref_vector& mutex, obj_map& new_soft, rational& lower) {
+ TRACE("opt",
+ for (expr* e : mutex) {
+ tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
+ });
+ if (mutex.size() <= 1)
+ return;
+
+ maxsmt_compare_soft cmp(new_soft);
+ ptr_vector _mutex(mutex.size(), mutex.data());
+ std::sort(_mutex.begin(), _mutex.end(), cmp);
+ mutex.reset();
+ mutex.append(_mutex.size(), _mutex.data());
+
+ rational weight(0), sum1(0), sum2(0);
+ vector weights;
+ for (expr* e : mutex) {
+ rational w = new_soft.find(e);
+ weights.push_back(w);
+ sum1 += w;
+ new_soft.remove(e);
+ }
+ for (unsigned i = mutex.size(); i-- > 0; ) {
+ expr_ref soft(m.mk_or(i+1, mutex.data()), m);
+ m_trail.push_back(soft);
+ rational w = weights[i];
+ weight = w - weight;
+ lower += weight*rational(i);
+ IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
+ sum2 += weight*rational(i+1);
+ new_soft.insert(soft, weight);
+ for (; i > 0 && weights[i-1] == w; --i) {}
+ weight = w;
+ }
+ SASSERT(sum1 == sum2);
+ }
+
+ preprocess::preprocess(solver& s): m(s.get_manager()), s(s), m_trail(m) {}
+
+ bool preprocess::operator()(vector& soft, rational& lower) {
+ return find_mutexes(soft, lower);
+ }
+};
diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h
new file mode 100644
index 000000000..8918e5e89
--- /dev/null
+++ b/src/opt/opt_preprocess.h
@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+ opt_preprocess.h
+
+Abstract:
+
+ Pre-processing for MaxSMT
+
+ Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+ class preprocess {
+ ast_manager& m;
+ solver& s;
+ expr_ref_vector m_trail;
+
+ bool find_mutexes(vector& softs, rational& lower);
+ void process_mutex(expr_ref_vector& mutex, obj_map& new_soft, rational& lower);
+
+ public:
+ preprocess(solver& s);
+ bool operator()(vector& soft, rational& lower);
+ };
+};
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index caac008fd..47fe86f94 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -48,6 +48,7 @@ namespace opt {
void set_offset(rational const& o) { m_offset = o; }
void set_negate(bool neg) { m_negate = neg; }
rational const& get_offset() const { return m_offset; }
+ void add_offset(rational const& o) { if (m_negate) m_offset -= o; else m_offset += o; }
bool get_negate() { return m_negate; }
inf_eps operator()(inf_eps const& r) const {
inf_eps result = r;
diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp
index c6a2f04a9..962369bf2 100644
--- a/src/opt/sortmax.cpp
+++ b/src/opt/sortmax.cpp
@@ -36,34 +36,27 @@ namespace opt {
expr_ref_vector m_trail;
func_decl_ref_vector m_fresh;
ref m_filter;
- sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
- maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {}
+ sortmax(maxsat_context& c, vector& s, unsigned index):
+ maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {}
~sortmax() override {}
lbool operator()() override {
- obj_map soft;
- if (!init()) {
- return l_false;
- }
- lbool is_sat = find_mutexes(soft);
- if (is_sat != l_true) {
- return is_sat;
- }
+ if (!init())
+ return l_undef;
+
+ lbool is_sat = l_true;
m_filter = alloc(generic_model_converter, m, "sortmax");
- rational offset = m_lower;
- m_upper = offset;
expr_ref_vector in(m);
expr_ref tmp(m);
ptr_vector out;
- obj_map::iterator it = soft.begin(), end = soft.end();
- for (; it != end; ++it) {
- if (!it->m_value.is_unsigned()) {
+ for (auto const & [e, w, t] : m_soft) {
+ if (!w.is_unsigned()) {
throw default_exception("sortmax can only handle unsigned weights. Use a different heuristic.");
}
- unsigned n = it->m_value.get_unsigned();
+ unsigned n = w.get_unsigned();
while (n > 0) {
- in.push_back(it->m_key);
+ in.push_back(e);
--n;
}
}
@@ -71,19 +64,15 @@ namespace opt {
// initialize sorting network outputs using the initial assignment.
unsigned first = 0;
- it = soft.begin();
- for (; it != end; ++it) {
- if (m_model->is_true(it->m_key)) {
- unsigned n = it->m_value.get_unsigned();
+ for (auto const & [e, w, t] : m_soft) {
+ if (t == l_true) {
+ unsigned n = w.get_unsigned();
while (n > 0) {
s().assert_expr(out[first]);
++first;
--n;
}
}
- else {
- m_upper += it->m_value;
- }
}
while (l_true == is_sat && first < out.size() && m_lower < m_upper) {
trace_bounds("sortmax");
@@ -149,8 +138,8 @@ namespace opt {
};
- maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
- return alloc(sortmax, c, ws, soft);
+ maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s, unsigned index) {
+ return alloc(sortmax, c, s, index);
}
}
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 22a660799..1fbd26cb8 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -44,8 +44,8 @@ namespace opt {
}
public:
- wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
- maxsmt_solver_base(c, ws, soft),
+ wmax(maxsat_context& c, vector& s, unsigned index):
+ maxsmt_solver_base(c, s, index),
m_trail(m),
m_defs(m) {}
@@ -54,22 +54,18 @@ namespace opt {
lbool operator()() override {
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);
- obj_map soft;
reset();
- lbool is_sat = find_mutexes(soft);
- if (is_sat != l_true) {
- return is_sat;
- }
- m_upper = m_lower;
+ if (init())
+ return l_undef;
+
+ lbool is_sat = l_true;
+
expr_ref_vector asms(m);
vector cores;
- for (auto const& kv : soft) {
- assert_weighted(wth(), kv.m_key, kv.m_value);
- if (!is_true(kv.m_key)) {
- m_upper += kv.m_value;
- }
- }
+ for (auto const& [k, w, t] : m_soft)
+ assert_weighted(wth(), k, w);
+
wth().init_min_cost(m_upper - m_lower);
trace_bounds("wmax");
@@ -308,8 +304,8 @@ namespace opt {
};
- maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
- return alloc(wmax, c, ws, soft);
+ maxsmt_solver_base* mk_wmax(maxsat_context& c, vector & s, unsigned index) {
+ return alloc(wmax, c, s, index);
}
}
diff --git a/src/opt/wmax.h b/src/opt/wmax.h
index 6cc3ed46b..7f5b26ac6 100644
--- a/src/opt/wmax.h
+++ b/src/opt/wmax.h
@@ -22,8 +22,8 @@ Notes:
#include "opt/maxsmt.h"
namespace opt {
- maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+ maxsmt_solver_base* mk_wmax(maxsat_context& c, vector& s, unsigned index);
- maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+ maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s, unsigned index);
}
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5505cfa70..4a254ac06 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3818,6 +3818,8 @@ namespace sat {
void solver::move_to_front(bool_var b) {
if (b >= num_vars())
return;
+ if (m_case_split_queue.empty())
+ return;
bool_var next = m_case_split_queue.min_var();
auto next_act = m_activity[next];
set_activity(b, next_act + 1);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 5a102fa14..e02a42979 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -549,13 +549,14 @@ namespace arith {
found_compatible = false;
for (; it != end; ++it) {
api_bound* a2 = *it;
- if (a1 == a2) continue;
- if (a2->get_bound_kind() != kind) continue;
+ if (a1 == a2)
+ continue;
+ if (a2->get_bound_kind() != kind)
+ continue;
rational const& k2(a2->get_value());
found_compatible = true;
- if (k1 < k2) {
+ if (k1 < k2)
return it;
- }
}
return end;
}
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 116621dcc..045b92c99 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -312,6 +312,7 @@ namespace euf {
}
}
else if (m.is_distinct(e)) {
+ // TODO - add lazy case for large values of sz.
expr_ref_vector eqs(m);
unsigned sz = n->num_args();
for (unsigned i = 0; i < sz; ++i) {
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 456525c42..cdea60d23 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -184,6 +184,8 @@ namespace q {
for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
expr* t = n->get_arg(idx)->get_expr();
values.push_back(mdl(t));
+ if (!m.is_value(values.back()))
+ return expr_ref(m.mk_var(idx, srt), m);
md->v2t.insert(values.back(), t);
md->t2v.insert(t, values.back());
}
@@ -299,6 +301,10 @@ namespace q {
auto term = [&](unsigned j) {
return md->v2t[md->values[j]];
};
+
+ for (unsigned j = 0; j < sz; ++j)
+ std::cout << mk_pp(md->values[j], m) << "\n";
+
expr* arg = t->get_arg(i);
diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp
index 6b3eb6718..d24af253e 100644
--- a/src/sat/smt/user_solver.cpp
+++ b/src/sat/smt/user_solver.cpp
@@ -88,7 +88,7 @@ namespace user_solver {
void solver::push_core() {
th_euf_solver::push_core();
m_prop_lim.push_back(m_prop.size());
- m_push_eh(m_user_context);
+ m_push_eh(m_user_context, this);
}
void solver::pop_core(unsigned num_scopes) {
@@ -96,7 +96,7 @@ namespace user_solver {
unsigned old_sz = m_prop_lim.size() - num_scopes;
m_prop.shrink(m_prop_lim[old_sz]);
m_prop_lim.shrink(old_sz);
- m_pop_eh(m_user_context, num_scopes);
+ m_pop_eh(m_user_context, this, num_scopes);
}
void solver::propagate_consequence(prop_info const& prop) {
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 7c53aa8eb..f783f22fb 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -25,6 +25,7 @@ using namespace smt;
theory_user_propagator::theory_user_propagator(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())),
m_var2expr(ctx.get_manager()),
+ m_push_popping(false),
m_to_add(ctx.get_manager())
{}
@@ -38,7 +39,7 @@ void theory_user_propagator::force_push() {
theory::push_scope_eh();
m_prop_lim.push_back(m_prop.size());
m_to_add_lim.push_back(m_to_add.size());
- m_push_eh(m_user_context);
+ m_push_eh(m_user_context, this);
}
}
@@ -122,7 +123,8 @@ final_check_status theory_user_propagator::final_check_eh() {
if (!(bool)m_final_eh)
return FC_DONE;
force_push();
- unsigned sz = m_prop.size();
+ unsigned sz1 = m_prop.size();
+ unsigned sz2 = m_expr2var.size();
try {
m_final_eh(m_user_context, this);
}
@@ -130,7 +132,8 @@ final_check_status theory_user_propagator::final_check_eh() {
throw default_exception("Exception thrown in \"final\"-callback");
}
propagate();
- bool done = (sz == m_prop.size()) && !ctx.inconsistent();
+ // check if it became inconsistent or something new was propagated/registered
+ bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
return done ? FC_DONE : FC_CONTINUE;
}
@@ -169,11 +172,11 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
old_sz = m_to_add_lim.size() - num_scopes;
m_to_add.shrink(m_to_add_lim[old_sz]);
m_to_add_lim.shrink(old_sz);
- m_pop_eh(m_user_context, num_scopes);
+ m_pop_eh(m_user_context, this, num_scopes);
}
bool theory_user_propagator::can_propagate() {
- return m_qhead < m_prop.size() || !m_to_add.empty();
+ return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size();
}
void theory_user_propagator::propagate_consequence(prop_info const& prop) {
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 52df38247..0c304aa3f 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -143,10 +143,9 @@ public:
tactic_ref t;
if (tp.default_tactic() != symbol::null &&
!tp.default_tactic().is_numerical() &&
- tp.default_tactic().bare_str() &&
- tp.default_tactic().bare_str()[0]) {
+ tp.default_tactic().str()[0]) {
cmd_context ctx(false, &m, l);
- std::istringstream is(tp.default_tactic().bare_str());
+ std::istringstream is(tp.default_tactic().str());
char const* file_name = "";
sexpr_ref se = parse_sexpr(ctx, is, p, file_name);
if (se) {
diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index 07270ffe6..02a027762 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -17,13 +17,13 @@ namespace user_propagator {
virtual ~context_obj() = default;
};
- typedef std::function final_eh_t;
- typedef std::function fixed_eh_t;
- typedef std::function eq_eh_t;
+ typedef std::function final_eh_t;
+ typedef std::function fixed_eh_t;
+ typedef std::function eq_eh_t;
typedef std::function fresh_eh_t;
- typedef std::function push_eh_t;
- typedef std::function pop_eh_t;
- typedef std::function created_eh_t;
+ typedef std::function push_eh_t;
+ typedef std::function pop_eh_t;
+ typedef std::function created_eh_t;
class plugin : public decl_plugin {
diff --git a/src/util/params.cpp b/src/util/params.cpp
index aefe4e074..1745e56fd 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -24,15 +24,14 @@ Notes:
params_ref params_ref::g_empty_params_ref;
-std::string norm_param_name(char const * n) {
- if (n == nullptr)
- return "_";
+std::string norm_param_name(char const* n) {
if (*n == ':')
n++;
std::string r = n;
unsigned sz = static_cast(r.size());
if (sz == 0)
return "_";
+
for (unsigned i = 0; i < sz; i++) {
char curr = r[i];
if ('A' <= curr && curr <= 'Z')
@@ -44,6 +43,8 @@ std::string norm_param_name(char const * n) {
}
std::string norm_param_name(symbol const & n) {
+ if (n.is_null())
+ return "_";
return norm_param_name(n.bare_str());
}
@@ -156,8 +157,8 @@ struct param_descrs::imp {
return m_names[idx];
}
- struct lt {
- bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; }
+ struct symlt {
+ bool operator()(symbol const & s1, symbol const & s2) const { return ::lt(s1, s2); }
};
void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
@@ -165,13 +166,13 @@ struct param_descrs::imp {
for (auto const& kv : m_info) {
names.push_back(kv.m_key);
}
- std::sort(names.begin(), names.end(), lt());
+ std::sort(names.begin(), names.end(), symlt());
for (symbol const& name : names) {
for (unsigned i = 0; i < indent; i++) out << " ";
if (smt2_style)
out << ':';
- char const * s = name.bare_str();
- unsigned n = static_cast(strlen(s));
+ std::string s = name.str();
+ unsigned n = static_cast(s.length());
for (unsigned i = 0; i < n; i++) {
if (smt2_style && s[i] == '_')
out << '-';