diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 98a7c6362..09cfd2b7a 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -14,6 +14,10 @@ import urllib.request import zipfile import sys import os.path +import shutil +import subprocess +import mk_util +import mk_project data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) @@ -27,36 +31,83 @@ def download_installs(): for asset in data['assets']: url = asset['browser_download_url'] name = asset['name'] + if "x64" not in name: + continue print("Downloading ", url) sys.stdout.flush() urllib.request.urlretrieve(url, "packages/%s" % name) -os_names = ["ubuntu-14", "ubuntu-16", "win", "debian", "osx"] +os_info = {"ubuntu-14" : ('so', 'ubuntu.14.04-x64'), + 'ubuntu-16' : ('so', 'ubuntu.16.04-x64'), + 'win' : ('dll', 'win-x64'), + 'debian' : ('so', 'debian.8-x64') } +def classify_package(f): + for os_name in os_info: + if os_name in f: + ext, dst = os_info[os_name] + return os_name, f[:-4], ext, dst + return None + def unpack(): - for f in os.listdir("packages"): - if f.endswith("zip") and "x64" in f: - print(f) - # determine os from os_names - # instead of this string manipulation. - - name = os.path.splitext(f)[0] - os_name = name[name.find("x64")+4:] - os_name = os_name[:os_name.find("-")] - print(os_name) - - zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') - path = "out/%s" % os_name - zip_ref.extract("%s/bin/libz3.so" % name) - # unzip files in packages - pass + # out + # +- runtimes + # +- win-x64 + # +- ubuntu.16.04-x64 + # +- ubuntu.14.04-x64 + # +- debian.8-x64 + # + + for f in os.listdir("packages"): + if f.endswith("zip") and "x64" in f and classify_package(f): + print(f) + os_name, package_dir, ext, dst = classify_package(f) + zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') + zip_ref.extract("%s/bin/libz3.%s" % (package_dir, ext), "tmp") + mk_dir("out/runtimes/%s" % dst) + shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/." % dst) + if "win" in f: + mk_dir("out/lib/netstandard1.4/") + for b in ["Microsoft.Z3.dll"]: + zip_ref.extract("%s/bin/%s" % (package_dir, b), "tmp") + shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.4/%s" % b) + +def create_nuget_spec(): + mk_project.init_version() + contents = """ + + + Microsoft.Z3.x64 + %s + Microsoft + Z3 is a satisfiability modulo theories solver from Microsoft Research. + Copyright Microsoft Corporation. All rights reserved. + smt constraint solver theorem prover + https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg + https://github.com/Z3Prover/z3 + https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt + + true + en + +""" + + with open("out/Microsoft.Z3.x64.nuspec", 'w') as f: + f.write(contents % mk_util.get_version_string(3)) + +def create_nuget_package(): + subprocess.call(["nuget", "pack"], cwd="out") def main(): mk_dir("packages") -# download_installs() -# create_nuget_dir() + download_installs() unpack() -# create_nuget_package() - + create_nuget_spec() + create_nuget_package() + + main() diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 5bd96c0fc..e70a094a0 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -7,9 +7,12 @@ ############################################ from mk_util import * +def init_version(): + set_version(4, 8, 3, 0) + # Z3 Project definition def init_project_def(): - set_version(4, 8, 3, 0) + init_version() add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 00cf3c706..3e4456676 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -23,6 +23,7 @@ VERBOSE=True DIST_DIR='dist' FORCE_MK=False DOTNET_ENABLED=True +DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False @@ -55,6 +56,7 @@ def display_help(): print(" -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).") print(" -f, --force force script to regenerate Makefiles.") print(" --nodotnet do not include .NET bindings in the binary distribution files.") + print(" --dotnetcore build for dotnet core.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") @@ -71,6 +73,7 @@ def parse_options(): 'force', 'nojava', 'nodotnet', + 'dotnetcore', 'dotnet-key=', 'githash', 'nopython' @@ -88,6 +91,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--dotnetcore': + DOTNET_CORE_ENABLED = True elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': @@ -108,7 +113,11 @@ def check_build_dir(path): def mk_build_dir(path): if not check_build_dir(path) or FORCE_MK: opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path, "--staticlib"] - if DOTNET_ENABLED: + if DOTNET_CORE_ENABLED: + opts.append('--dotnetcore') + if not DOTNET_KEY_FILE is None: + opts.append('--dotnet-key=' + DOTNET_KEY_FILE) + elif DOTNET_ENABLED: opts.append('--dotnet') if not DOTNET_KEY_FILE is None: opts.append('--dotnet-key=' + DOTNET_KEY_FILE) @@ -186,7 +195,10 @@ def mk_dist_dir(): build_path = BUILD_DIR dist_path = os.path.join(DIST_DIR, get_z3_name()) mk_dir(dist_path) - mk_util.DOTNET_ENABLED = DOTNET_ENABLED + if DOTNET_CORE_ENABLED: + mk_util.DOTNET_CORE_ENABLED = True + else: + mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9c5b0c9a9..83ae3d455 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -461,7 +461,6 @@ def check_dotnet_core(): r = exec_cmd([DOTNET, '--help']) if r != 0: raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') - pass def check_ml(): t = TempFile('hello.ml') @@ -668,6 +667,7 @@ def display_help(exit_code): if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") print(" --optimize generate optimized code during linking.") + print(" --dotnetcore generate .NET platform bindings.") print(" --dotnet generate .NET bindings.") print(" --dotnet-key= sign the .NET assembly using the private key in .") print(" --java generate Java bindings.") @@ -1627,6 +1627,23 @@ class PythonInstallComponent(Component): def mk_makefile(self, out): return +def set_key_file(self): + global DOTNET_KEY_FILE + # We need to give the assembly a strong name so that it + # can be installed into the GAC with ``make install`` + if not DOTNET_KEY_FILE is None: + self.key_file = DOTNET_KEY_FILE + + if not self.key_file is None: + if os.path.isfile(self.key_file): + self.key_file = os.path.abspath(self.key_file) + elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): + self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) + else: + print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) + self.key_file = None + + class DotNetDLLComponent(Component): def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): Component.__init__(self, name, path, deps) @@ -1688,19 +1705,7 @@ class DotNetDLLComponent(Component): ] ) - # We need to give the assembly a strong name so that it - # can be installed into the GAC with ``make install`` - if not DOTNET_KEY_FILE is None: - self.key_file = DOTNET_KEY_FILE - - if not self.key_file is None: - if os.path.isfile(self.key_file): - self.key_file = os.path.abspath(self.key_file) - elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): - self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) - else: - print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) - self.key_file = None + set_key_file(self) if not self.key_file is None: print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file)) @@ -1829,7 +1834,7 @@ class DotNetDLLComponent(Component): MakeRuleCmd.remove_installed_files(out, pkg_config_file) -# TBD: retool the following for 'dotnet build' +# build for dotnet core class DotNetCoreDLLComponent(Component): def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): Component.__init__(self, name, path, deps) @@ -1841,16 +1846,8 @@ class DotNetCoreDLLComponent(Component): self.assembly_info_dir = assembly_info_dir self.key_file = default_key_file - def mk_nuget_config_file(self): - # TBD revise - """ - Create nuget file for the dot net bindings. These - are needed by Monodevelop. - """ - return def mk_makefile(self, out): - global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): return cs_fp_files = [] @@ -1865,6 +1862,11 @@ class DotNetCoreDLLComponent(Component): out.write(' ') out.write(cs_file) out.write('\n') + + set_key_file(self) + key = "" + if not self.key_file is None: + key = "%s" % self.key_file if VS_X64: platform = 'x64' @@ -1878,14 +1880,13 @@ class DotNetCoreDLLComponent(Component): core_csproj_str = """ - netcoreapp1.0 + netstandard1.4 %s $(DefineConstants);DOTNET_CORE portable Microsoft.Z3 Library Microsoft.Z3 - $(PackageTargetFallback);dnxcore50 1.0.4 %s true @@ -1894,13 +1895,14 @@ class DotNetCoreDLLComponent(Component): Z3 is a satisfiability modulo theories solver from Microsoft Research. Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover + %s -""" % (platform, version, self.to_src_dir) +""" % (platform, version, key, self.to_src_dir) mk_dir(os.path.join(BUILD_DIR, 'dotnet')) csproj = os.path.join('dotnet', 'z3.csproj') @@ -1915,26 +1917,20 @@ class DotNetCoreDLLComponent(Component): else: dotnetCmdLine.extend(['Release']) - - path = os.path.abspath(BUILD_DIR) + path = os.path.join(os.path.abspath(BUILD_DIR), ".") dotnetCmdLine.extend(['-o', path]) - # Now emit the command line MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) - # State that the high-level "dotnet" target depends on the .NET bindings - # dll we just created the build rule for out.write('\n') out.write('%s: %s\n\n' % (self.name, dllfile)) - # Create nuget file - self.mk_nuget_config_file() - return def main_component(self): return is_dotnet_core_enabled() def has_assembly_info(self): + # TBD: is this required for dotnet core given that version numbers are in z3.csproj file? return True def mk_win_dist(self, build_path, dist_path): @@ -1957,51 +1953,13 @@ class DotNetCoreDLLComponent(Component): '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) def mk_install_deps(self, out): - if not is_dotnet_core_enabled(): - return - out.write('%s' % self.name) - - def gac_pkg_name(self): - return "{}.Sharp".format(self.dll_name) - - def _install_or_uninstall_to_gac(self, out, install): - # TBD revise for nuget - gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), - '/root', - '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) - ] - if install: - install_or_uninstall_flag = '-i' - else: - # Note need use ``-us`` here which takes an assembly file name - # rather than ``-u`` which takes an assembly display name (e.g. - # ) - install_or_uninstall_flag = '-us' - MakeRuleCmd.write_cmd(out, '{gacutil} {install_or_uninstall_flag} {assembly_name}.dll -f {flags}'.format( - gacutil=GACUTIL, - install_or_uninstall_flag=install_or_uninstall_flag, - assembly_name=self.dll_name, - flags=' '.join(gacUtilFlags))) + pass def mk_install(self, out): - # TBD revise for nuget - if not is_dotnet_core_enabled(): - return - self._install_or_uninstall_to_gac(out, install=True) - - # Install pkg-config file. Monodevelop needs this to find Z3 - pkg_config_output = os.path.join(self.build_dir, - '{}.pc'.format(self.gac_pkg_name())) - MakeRuleCmd.make_install_directory(out, INSTALL_PKGCONFIG_DIR) - MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR) + pass def mk_uninstall(self, out): - # TBD revise for nuget - if not is_dotnet_core_enabled(): - return - self._install_or_uninstall_to_gac(out, install=False) - pkg_config_file = os.path.join('lib','pkgconfig','{}.pc'.format(self.gac_pkg_name())) - MakeRuleCmd.remove_installed_files(out, pkg_config_file) + pass class JavaDLLComponent(Component): def __init__(self, name, dll_name, package_name, manifest_file, path, deps): @@ -2428,7 +2386,8 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) - proj_path = os.path.join(BUILD_DIR, proj_name) + mk_dir(os.path.join(BUILD_DIR, 'dotnet_example')) + csproj = os.path.join('dotnet_example', proj_name) if VS_X64: platform = 'x64' elif VS_ARM: @@ -2443,18 +2402,18 @@ class DotNetExampleComponent(ExampleComponent): %s - + - Microsoft.Z3.dll + ..\Microsoft.Z3.dll """ % (platform, self.to_ex_dir) - with open(proj_path, 'w') as ous: + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: ous.write(dotnet_proj_str) out.write('\n') - dotnetCmdLine = [DOTNET, "build", proj_name] + dotnetCmdLine = [DOTNET, "build", csproj] dotnetCmdLine.extend(['-c']) if DEBUG_MODE: dotnetCmdLine.extend(['Debug']) @@ -3219,7 +3178,8 @@ def mk_bindings(api_files): if is_dotnet_enabled(): dotnet_output_dir = get_component('dotnet').src_dir elif is_dotnet_core_enabled(): - dotnet_output_dir = get_component('dotnetcore').src_dir + dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet') + mk_dir(dotnet_output_dir) java_output_dir = None java_package_name = None if is_java_enabled(): @@ -3248,10 +3208,10 @@ def mk_bindings(api_files): mk_z3consts_ml(api_files) if is_dotnet_enabled(): check_dotnet() - mk_z3consts_dotnet(api_files) + mk_z3consts_dotnet(api_files, dotnet_output_dir) if is_dotnet_core_enabled(): check_dotnet_core() - mk_z3consts_dotnet(api_files) + mk_z3consts_dotnet(api_files, dotnet_output_dir) # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): @@ -3268,7 +3228,7 @@ def mk_z3consts_py(api_files): print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add .Net definitions -def mk_z3consts_dotnet(api_files): +def mk_z3consts_dotnet(api_files, output_dir): dotnet = get_component(DOTNET_COMPONENT) if not dotnet: dotnet = get_component(DOTNET_CORE_COMPONENT) @@ -3277,7 +3237,7 @@ def mk_z3consts_dotnet(api_files): api_file_c = dotnet.find_file(api_file, dotnet.name) api_file = os.path.join(api_file_c.src_dir, api_file) full_path_api_files.append(api_file) - generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir) + generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir) if VERBOSE: print("Generated '{}".format(generated_file)) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 9e0374192..e61a7714c 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -25,6 +25,7 @@ VERBOSE=True DIST_DIR='dist' FORCE_MK=False DOTNET_ENABLED=True +DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False @@ -62,6 +63,7 @@ def display_help(): print(" -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).") print(" -f, --force force script to regenerate Makefiles.") print(" --nodotnet do not include .NET bindings in the binary distribution files.") + print(" --dotnetcore build for dotnet core.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") @@ -72,7 +74,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -80,6 +82,7 @@ def parse_options(): 'force', 'nojava', 'nodotnet', + 'dotnetcore', 'dotnet-key=', 'githash', 'nopython', @@ -99,6 +102,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--dotnetcore': + DOTNET_CORE_ENABLED = True elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': @@ -124,7 +129,11 @@ def mk_build_dir(path, x64): if not check_build_dir(path) or FORCE_MK: parallel = '--parallel=' + MAKEJOBS opts = ["python", os.path.join('scripts', 'mk_make.py'), parallel, "-b", path] - if DOTNET_ENABLED: + if DOTNET_CORE_ENABLED: + opts.append('--dotnetcore') + if not DOTNET_KEY_FILE is None: + opts.append('--dotnet-key=' + DOTNET_KEY_FILE) + elif DOTNET_ENABLED: opts.append('--dotnet') if not DOTNET_KEY_FILE is None: opts.append('--dotnet-key=' + DOTNET_KEY_FILE) @@ -208,7 +217,10 @@ def mk_dist_dir(x64): build_path = BUILD_X86_DIR dist_path = os.path.join(DIST_DIR, get_z3_name(x64)) mk_dir(dist_path) - mk_util.DOTNET_ENABLED = DOTNET_ENABLED + if DOTNET_CORE_ENABLED: + mk_util.DOTNET_CORE_ENABLED = True + else: + mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ac11022c1..a941f8e86 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -931,6 +931,26 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject)); } + /// + /// Create an expression representing t1 xor t2 xor t3 ... . + /// + public BoolExpr MkXor(IEnumerable ts) + { + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); + CheckContextMatch(ts); + BoolExpr r = null; + foreach (var t in ts) { + if (r == null) + r = t; + else + r = MkXor(r, t); + } + if (r == null) + r = MkTrue(); + return r; + } + /// /// Create an expression representing t[0] and t[1] and .... /// diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index c24516c22..c0cb091b0 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -238,6 +238,14 @@ namespace Microsoft.Z3 return Eval(t, completion); } + /// + /// Evaluate expression to a double, assuming it is a numeral already. + /// + public double Double(Expr t) { + var r = Eval(t, true); + return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject); + } + /// /// The number of uninterpreted sorts that the model has an interpretation for. /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 08d20dfb2..ede494598 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2173,6 +2173,22 @@ public class Context implements AutoCloseable { { checkContextMatch(t); return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t))); + } + + /** + * Create the empty regular expression. + */ + public ReExpr mkEmptyRe(Sort s) + { + return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); + } + + /** + * Create the full regular expression. + */ + public ReExpr mkFullRe(Sort s) + { + return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f68b908e2..70dcb158e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6164,6 +6164,10 @@ class ModelRef(Z3PPObject): def __deepcopy__(self): return self.translate(self.ctx) +def Model(ctx = None): + ctx = _get_ctx(ctx) + return ModelRef(Z3_mk_model(ctx.ref()), ctx) + def is_as_array(n): """Return true if n is a Z3 expression of the form (_ as-array f).""" return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e1359949d..be463b1b0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5579,7 +5579,7 @@ extern "C" { \brief Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically - converted to Booleans either, so the caller intends to + converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded. diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 0b5f20db8..75a42886c 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -108,6 +108,7 @@ private: bool m_pivot_on_cs; // prefer smaller correction set to core. bool m_dump_benchmarks; // display benchmarks (into wcnf format) + std::string m_trace_id; typedef ptr_vector exprs; @@ -152,6 +153,14 @@ public: (m.is_not(l, l) && is_uninterp_const(l)); } + void add(expr_ref_vector const& es) { + for (expr* e : es) add(e); + } + + void add(expr* e) { + s().assert_expr(e); + } + void add_soft(expr* e, rational const& w) { TRACE("opt", tout << mk_pp(e, m) << " |-> " << w << "\n";); expr_ref asum(m), fml(m); @@ -168,7 +177,7 @@ public: else { asum = mk_fresh_bool("soft"); fml = m.mk_iff(asum, e); - s().assert_expr(fml); + add(fml); } new_assumption(asum, w); } @@ -194,11 +203,8 @@ public: if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { TRACE("opt_verbose", - display_vec(tout, m_asms); - s().display(tout); - tout << "\n"; - display(tout); - ); + s().display(tout << m_asms << "\n") << "\n"; + display(tout);); is_sat = check_sat_hill_climb(m_asms); if (m.canceled()) { return l_undef; @@ -206,8 +212,7 @@ public: switch (is_sat) { case l_true: CTRACE("opt", !m_model->is_true(m_asms), - tout << *m_model; - tout << "assumptions: "; + tout << *m_model << "assumptions: "; for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; tout << "\n";); SASSERT(m_model->is_true(m_asms)); @@ -320,6 +325,7 @@ public: void found_optimum() { IF_VERBOSE(1, verbose_stream() << "found optimum\n";); + verify_assumptions(); m_lower.reset(); for (soft& s : m_soft) { s.is_true = m_model->is_true(s.s); @@ -348,7 +354,14 @@ public: st.update("maxres-correction-sets", m_stats.m_num_cs); } - lbool get_cores(vector& cores) { + struct weighted_core { + exprs m_core; + rational m_weight; + weighted_core(exprs const& c, rational const& w): + m_core(c), m_weight(w) {} + }; + + lbool get_cores(vector& cores) { // assume m_s is unsat. lbool is_sat = l_false; cores.reset(); @@ -361,7 +374,7 @@ public: get_mus_model(mdl); is_sat = minimize_core(_core); core.append(_core.size(), _core.c_ptr()); - // verify_core(core); + verify_core(core); ++m_stats.m_num_cores; if (is_sat != l_true) { IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); @@ -373,13 +386,16 @@ public: m_lower = m_upper; return l_true; } + + // 1. remove all core literals from m_asms // 2. re-add literals of higher weight than min-weight. // 3. 'core' stores the core literals that are // re-encoded as assumptions, afterwards + cores.push_back(weighted_core(core, core_weight(core))); + remove_soft(core, m_asms); - split_core(core); - cores.push_back(core); + split_core(core); if (core.size() >= m_max_core_size) break; if (cores.size() >= m_max_num_cores) break; @@ -389,7 +405,7 @@ public: TRACE("opt", tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n"; - for (auto const& c : cores) display_vec(tout, c); + for (auto const& c : cores) display_vec(tout, c.m_core); tout << "num assumptions: " << m_asms.size() << "\n";); return is_sat; @@ -456,7 +472,7 @@ public: } lbool process_unsat() { - vector cores; + vector cores; lbool is_sat = get_cores(cores); if (is_sat != l_true) { return is_sat; @@ -478,9 +494,9 @@ public: return result; } - void process_unsat(vector const& cores) { + void process_unsat(vector const& cores) { for (auto const & c : cores) { - process_unsat(c); + process_unsat(c.m_core, c.m_weight); } } @@ -491,16 +507,15 @@ public: } } - void process_unsat(exprs const& core) { + void process_unsat(exprs const& core, rational w) { IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";); expr_ref fml(m); SASSERT(!core.empty()); - rational w = core_weight(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); - IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); + IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, core.size(), core.c_ptr())); - s().assert_expr(fml); + add(fml); m_lower += w; if (m_st == s_primal_dual) { m_lower = std::min(m_lower, m_upper); @@ -636,10 +651,10 @@ public: else { dd = mk_fresh_bool("d"); fml = m.mk_implies(dd, d); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_implies(dd, b_i); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_and(d, b_i); update_model(dd, fml); @@ -650,7 +665,7 @@ public: fml = m.mk_implies(asum, cls); update_model(asum, cls); new_assumption(asum, w); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); } } @@ -682,7 +697,7 @@ public: d = mk_fresh_bool("d"); fml = m.mk_implies(d, cls); update_model(d, cls); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); } @@ -691,10 +706,10 @@ public: } asum = mk_fresh_bool("a"); fml = m.mk_implies(asum, b_i1); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_implies(asum, cls); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); new_assumption(asum, w); @@ -702,7 +717,7 @@ public: update_model(asum, fml); } fml = m.mk_or(cs.size(), cs.c_ptr()); - s().assert_expr(fml); + add(fml); } void update_assignment(model_ref & mdl) { @@ -747,7 +762,7 @@ public: s.is_true = m_model->is_true(s.s); } - // DEBUG_CODE(verify_assignment();); + verify_assignment(); m_upper = upper; @@ -768,7 +783,7 @@ public: } fml = u.mk_lt(nsoft.size(), weights.c_ptr(), nsoft.c_ptr(), m_upper); TRACE("opt", tout << "block upper bound " << fml << "\n";);; - s().assert_expr(fml); + add(fml); } void remove_soft(exprs const& core, expr_ref_vector& asms) { @@ -819,40 +834,50 @@ public: void commit_assignment() override { if (m_found_feasible_optimum) { TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;); - s().assert_expr(m_defs); - s().assert_expr(m_asms); + add(m_defs); + add(m_asms); } // else: there is only a single assignment to these soft constraints. } void verify_core(exprs const& core) { - IF_VERBOSE(3, verbose_stream() << "verify core\n";); - ref smt_solver = mk_smt_solver(m, m_params, symbol()); - smt_solver->assert_expr(s().get_assertions()); - smt_solver->assert_expr(core); - lbool is_sat = smt_solver->check_sat(0, nullptr); - if (is_sat == l_true) { - IF_VERBOSE(0, verbose_stream() << "not a core\n";); - } + return; + IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); + _solver->assert_expr(core); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << "\n"); + VERIFY(is_sat == l_false); + } + + void verify_assumptions() { + return; + IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); + _solver->assert_expr(m_asms); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";); + VERIFY(is_sat == l_true); } void verify_assignment() { + return; IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); - ref smt_solver = mk_smt_solver(m, m_params, symbol()); - smt_solver->assert_expr(s().get_assertions()); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); expr_ref n(m); for (soft& s : m_soft) { n = s.s; if (!s.is_true) { n = mk_not(m, n); } - smt_solver->assert_expr(n); + _solver->assert_expr(n); } - lbool is_sat = smt_solver->check_sat(0, nullptr); - if (is_sat == l_false) { - IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";); - } - IF_VERBOSE(1, verbose_stream() << "verified\n";); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n"); + VERIFY(is_sat == l_true); } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d9c3457fa..a6f3d8152 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -284,7 +284,9 @@ namespace opt { symbol pri = optp.priority(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); + lbool is_sat = s.check_sat(asms.size(),asms.c_ptr()); + TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); @@ -1565,11 +1567,12 @@ namespace opt { mdl->set_model_completion(true); for (expr * f : fmls) { if (!mdl->is_true(f)) { - //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n")); - IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n")); - IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n"); - IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0)); - IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n"); + IF_VERBOSE(0, + verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n"; + m_fm->display(verbose_stream() << "fm\n"); + m_model_converter->display(verbose_stream() << "mc\n"); + model_smt2_pp(verbose_stream(), m, *mdl, 0); + verbose_stream() << to_string_internal() << "\n"); exit(0); } } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4ca4928d0..f3a3e9238 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -503,7 +503,7 @@ namespace smt { tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); - mk_axiom(eqz, eq, true); + mk_axiom(eqz, eq, false); mk_axiom(eqz, lower, false); mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); rational k; diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 28e6afeca..7431618df 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -36,6 +36,7 @@ void check_sat_result::set_reason_unknown(event_handler& eh) { } } + simple_check_sat_result::simple_check_sat_result(ast_manager & m): m_core(m), m_proof(m) { diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 5474700c3..be6ea8b7a 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -72,10 +72,8 @@ struct bit_blaster_model_converter : public model_converter { } TRACE("blaster_mc", tout << "bits that should not be included in the model:\n"; - obj_hashtable::iterator it = bits.begin(); - obj_hashtable::iterator end = bits.end(); - for (; it != end; ++it) { - tout << (*it)->get_name() << " "; + for (func_decl* f : bits) { + tout << f->get_name() << " "; } tout << "\n";); diff --git a/src/util/params.cpp b/src/util/params.cpp index d7e05cb00..43f53514a 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -161,19 +161,15 @@ struct param_descrs::imp { void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { svector names; - dictionary::iterator it = m_info.begin(); - dictionary::iterator end = m_info.end(); - for (; it != end; ++it) { - names.push_back(it->m_key); + for (auto const& kv : m_info) { + names.push_back(kv.m_key); } std::sort(names.begin(), names.end(), lt()); - svector::iterator it2 = names.begin(); - svector::iterator end2 = names.end(); - for (; it2 != end2; ++it2) { + for (symbol const& name : names) { for (unsigned i = 0; i < indent; i++) out << " "; if (smt2_style) out << ':'; - char const * s = it2->bare_str(); + char const * s = name.bare_str(); unsigned n = static_cast(strlen(s)); for (unsigned i = 0; i < n; i++) { if (smt2_style && s[i] == '_') @@ -186,7 +182,7 @@ struct param_descrs::imp { out << s[i]; } info d; - m_info.find(*it2, d); + m_info.find(name, d); SASSERT(d.m_descr); out << " (" << d.m_kind << ")"; if (include_descr) @@ -198,10 +194,8 @@ struct param_descrs::imp { } void copy(param_descrs & other) { - dictionary::iterator it = other.m_imp->m_info.begin(); - dictionary::iterator end = other.m_imp->m_info.end(); - for (; it != end; ++it) { - insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module); + for (auto const& kv : other.m_imp->m_info) { + insert(kv.m_key, kv.m_value.m_kind, kv.m_value.m_descr, kv.m_value.m_default, kv.m_value.m_module); } } @@ -346,24 +340,22 @@ public: void reset(symbol const & k); void reset(char const * k); - void validate(param_descrs const & p) { - svector::iterator it = m_entries.begin(); - svector::iterator end = m_entries.end(); + void validate(param_descrs const & p) { symbol suffix, prefix; - for (; it != end; ++it) { - param_kind expected = p.get_kind_in_module(it->first); + for (params::entry& e : m_entries) { + param_kind expected = p.get_kind_in_module(e.first); if (expected == CPK_INVALID) { std::stringstream strm; - strm << "unknown parameter '" << it->first.str() << "'\n"; + strm << "unknown parameter '" << e.first.str() << "'\n"; strm << "Legal parameters are:\n"; p.display(strm, 2, false, false); throw default_exception(strm.str()); } - if (it->second.m_kind != expected && - !(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { + if (e.second.m_kind != expected && + !(e.second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { std::stringstream strm; - strm << "Parameter " << it->first.str() << " was given argument of type "; - strm << it->second.m_kind << ", expected " << expected; + strm << "Parameter " << e.first.str() << " was given argument of type "; + strm << e.second.m_kind << ", expected " << expected; throw default_exception(strm.str()); } } @@ -405,28 +397,26 @@ public: void display(std::ostream & out) const { out << "(params"; - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - out << " " << it->first; - switch (it->second.m_kind) { + for (params::entry const& e : m_entries) { + out << " " << e.first; + switch (e.second.m_kind) { case CPK_BOOL: - out << " " << (it->second.m_bool_value?"true":"false"); + out << " " << (e.second.m_bool_value?"true":"false"); break; case CPK_UINT: - out << " " <second.m_uint_value; + out << " " <second.m_double_value; + out << " " << e.second.m_double_value; break; case CPK_NUMERAL: - out << " " << *(it->second.m_rat_value); + out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); break; case CPK_STRING: - out << " " << it->second.m_str_value; + out << " " << e.second.m_str_value; break; default: UNREACHABLE(); @@ -437,31 +427,29 @@ public: } void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const { - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - if (!descrs.contains(it->first)) continue; + for (params::entry const& e : m_entries) { + if (!descrs.contains(e.first)) continue; out << "(set-option :"; out << module << "."; - out << it->first; - switch (it->second.m_kind) { + out << e.first; + switch (e.second.m_kind) { case CPK_BOOL: - out << " " << (it->second.m_bool_value?"true":"false"); + out << " " << (e.second.m_bool_value?"true":"false"); break; case CPK_UINT: - out << " " <second.m_uint_value; + out << " " <second.m_double_value; + out << " " << e.second.m_double_value; break; case CPK_NUMERAL: - out << " " << *(it->second.m_rat_value); + out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); break; case CPK_STRING: - out << " " << it->second.m_str_value; + out << " " << e.second.m_str_value; break; default: UNREACHABLE(); @@ -472,29 +460,27 @@ public: } void display(std::ostream & out, symbol const & k) const { - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - if (it->first != k) + for (params::entry const& e : m_entries) { + if (e.first != k) continue; - switch (it->second.m_kind) { + switch (e.second.m_kind) { case CPK_BOOL: - out << (it->second.m_bool_value?"true":"false"); + out << (e.second.m_bool_value?"true":"false"); return; case CPK_UINT: - out << it->second.m_uint_value; + out << e.second.m_uint_value; return; case CPK_DOUBLE: - out << it->second.m_double_value; + out << e.second.m_double_value; return; case CPK_NUMERAL: - out << *(it->second.m_rat_value); + out << *(e.second.m_rat_value); return; case CPK_SYMBOL: - out << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); return; case CPK_STRING: - out << it->second.m_str_value; + out << e.second.m_str_value; return; default: out << "internal"; @@ -786,6 +772,7 @@ void params::del_values() { return false; \ } + bool params::contains(symbol const & k) const { CONTAINS(k); }