diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 14e403826..dbcd0e82a 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -379,6 +379,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) Z3_sort t; Z3_symbol f_name, t_name; Z3_ast_vector q; + unsigned i; t = Z3_get_range(ctx, f); @@ -399,7 +400,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) 1, &t_name, &t, 1, &f_name, &f); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q)); - for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { + for (i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i)); } } @@ -1644,6 +1645,7 @@ void parser_example2() Z3_symbol names[2]; Z3_func_decl decls[2]; Z3_ast_vector f; + unsigned i; printf("\nparser_example2\n"); LOG_MSG("parser_example2"); @@ -1668,7 +1670,7 @@ void parser_example2() 2, names, decls); printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f)); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f)); - for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { + for (i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i)); } check(ctx, s, Z3_L_TRUE); diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py new file mode 100644 index 000000000..09cfd2b7a --- /dev/null +++ b/scripts/mk_nuget_release.py @@ -0,0 +1,113 @@ +# +# Copyright (c) 2018 Microsoft Corporation +# + +# 1. download releases from github +# 2. copy over libz3.dll for the different architectures +# 3. copy over Microsoft.Z3.dll from suitable distribution +# 4. copy nuspec file from packages +# 5. call nuget pack + +import json +import os +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()) + +version_str = data['tag_name'] + +def mk_dir(d): + if not os.path.exists(d): + os.makedirs(d) + +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_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(): + # unzip files in packages + # 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() + unpack() + 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 261890922..83ae3d455 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,10 +456,11 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): - # r = exec_cmd([DOTNET]) - # if r != 0: - # raise ... - pass + if not IS_WINDOWS: + return + r = exec_cmd([DOTNET, '--help']) + if r != 0: + raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') def check_ml(): t = TempFile('hello.ml') @@ -562,6 +563,11 @@ def set_version(major, minor, build, revision): def get_version(): return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) +def get_version_string(n): + if n == 3: + return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD) + return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_REVISION) + def build_static_lib(): return STATIC_LIB @@ -661,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.") @@ -1620,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) @@ -1639,11 +1663,7 @@ class DotNetDLLComponent(Component): pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) substitutions = { 'PREFIX': PREFIX, 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) + 'VERSION': get_version_string(4) } pkg_config_output = os.path.join(BUILD_DIR, self.build_dir, @@ -1685,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)) @@ -1826,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) @@ -1838,31 +1846,8 @@ class DotNetCoreDLLComponent(Component): self.assembly_info_dir = assembly_info_dir self.key_file = default_key_file - def mk_pkg_config_file(self): - """ - Create pkgconfig file for the dot net bindings. These - are needed by Monodevelop. - """ - pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) - substitutions = { 'PREFIX': PREFIX, - 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) - } - pkg_config_output = os.path.join(BUILD_DIR, - self.build_dir, - '{}.pc'.format(self.gac_pkg_name())) - - # FIXME: Why isn't the build directory available? - mk_dir(os.path.dirname(pkg_config_output)) - # Configure file that will be installed by ``make install``. - configure_file(pkg_config_template, pkg_config_output, substitutions) - + def mk_makefile(self, out): - global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): return cs_fp_files = [] @@ -1877,38 +1862,75 @@ 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' + elif VS_ARM: + platform = 'ARM' + else: + platform = 'x86' + + version = get_version_string(3) + + core_csproj_str = """ + + + netstandard1.4 + %s + $(DefineConstants);DOTNET_CORE + portable + Microsoft.Z3 + Library + Microsoft.Z3 + 1.0.4 + %s + true + Microsoft + Microsoft + Z3 is a satisfiability modulo theories solver from Microsoft Research. + Copyright Microsoft Corporation. All rights reserved. + smt constraint solver theorem prover + %s + + + + + + +""" % (platform, version, key, self.to_src_dir) + + mk_dir(os.path.join(BUILD_DIR, 'dotnet')) + csproj = os.path.join('dotnet', 'z3.csproj') + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: + ous.write(core_csproj_str) - csproj = os.path.join(self.to_src_dir, "core", "core.csproj") dotnetCmdLine = [DOTNET, "build", csproj] - # TBD: select build configurations also based on architecture - # Debug|x86, Debug|x64, Debug|arm - # Release|x86, Release|x64, Release|arm dotnetCmdLine.extend(['-c']) if DEBUG_MODE: dotnetCmdLine.extend(['Debug']) 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 pkg-config file - self.mk_pkg_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): @@ -1916,8 +1938,8 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) if DEBUG_MODE: shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) @@ -1927,52 +1949,17 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%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): - 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): - 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): - 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): @@ -2393,7 +2380,47 @@ class DotNetExampleComponent(ExampleComponent): out.write('\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) if is_dotnet_core_enabled(): - print("TBD: build script for dotnet_example on core") + proj_name = 'dotnet_example.csproj' + out.write('_ex_%s:' % self.name) + for csfile in get_cs_files(self.ex_dir): + out.write(' ') + out.write(os.path.join(self.to_ex_dir, csfile)) + + 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: + platform = 'ARM' + else: + platform = 'x86' + + dotnet_proj_str = """ + + Exe + netcoreapp2.0 + %s + + + + + ..\Microsoft.Z3.dll + + +""" % (platform, self.to_ex_dir) + + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: + ous.write(dotnet_proj_str) + + out.write('\n') + dotnetCmdLine = [DOTNET, "build", csproj] + dotnetCmdLine.extend(['-c']) + if DEBUG_MODE: + dotnetCmdLine.extend(['Debug']) + else: + dotnetCmdLine.extend(['Release']) + MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) + out.write('\n') class JavaExampleComponent(ExampleComponent): def __init__(self, name, path): @@ -3151,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(): @@ -3180,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): @@ -3200,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) @@ -3209,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..10865676d 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -208,7 +208,7 @@ 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 + mk_util.DOTNET_CORE_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/api_solver.cpp b/src/api/api_solver.cpp index cb4ae19db..a5ad7b525 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -183,8 +183,12 @@ extern "C" { } else if (ext && std::string("dimacs") == ext) { ast_manager& m = to_solver_ref(s)->get_manager(); + std::stringstream err; sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); - parse_dimacs(is, solver); + if (!parse_dimacs(is, err, solver)) { + SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str()); + return; + } sat2goal s2g; ref mc; atom2bool_var a2b(m); 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/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dad485d94..82607452f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -561,6 +561,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu zstring s; rational pos, len; + TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";); bool constantBase = m_util.str.is_string(a, s); bool constantPos = m_autil.is_numeral(b, pos); bool constantLen = m_autil.is_numeral(c, len); @@ -599,6 +600,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu SASSERT(_len > 0); expr_ref_vector as(m()), bs(m()); m_util.str.get_concat(a, as); + if (as.empty()) { + result = a; + return BR_DONE; + } for (unsigned i = 0; i < as.size() && _len > 0; ++i) { if (m_util.str.is_unit(as[i].get())) { if (_pos == 0) { @@ -613,7 +618,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu return BR_FAILED; } } - result = m_util.str.mk_concat(bs); + if (bs.empty()) { + result = m_util.str.mk_empty(m().get_sort(a)); + } + else { + result = m_util.str.mk_concat(bs); + } return BR_DONE; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 06f30cbdf..737213477 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -899,7 +899,7 @@ bool seq_decl_plugin::are_distinct(app* a, app* b) const { } if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) { - return true; + return m_manager->are_distinct(a->get_arg(0), b->get_arg(0)); } if (is_app_of(a, m_family_id, OP_SEQ_EMPTY) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 106a77c0e..64f9c36fd 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -346,7 +346,8 @@ namespace smt2 { // consume garbage // return true if managed to recover from the error... bool sync_after_error() { - while (true) { + unsigned num_errors = 0; + while (num_errors < 100) { try { while (curr_is_rparen()) next(); @@ -374,8 +375,10 @@ namespace smt2 { catch (scanner_exception & ex) { SASSERT(ex.has_pos()); error(ex.line(), ex.pos(), ex.msg()); + ++num_errors; } } + return false; } void check_next(scanner::token t, char const * msg) { @@ -3117,7 +3120,7 @@ namespace smt2 { bool operator()() { m_num_bindings = 0; - bool found_errors = false; + unsigned found_errors = 0; try { scan_core(); @@ -3126,7 +3129,7 @@ namespace smt2 { error(ex.msg()); if (!sync_after_error()) return false; - found_errors = true; + found_errors++; } while (true) { @@ -3138,7 +3141,7 @@ namespace smt2 { parse_cmd(); break; case scanner::EOF_TOKEN: - return !found_errors; + return found_errors == 0; default: throw parser_exception("invalid command, '(' expected"); break; diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp index 463418b23..970e682b3 100644 --- a/src/sat/dimacs.cpp +++ b/src/sat/dimacs.cpp @@ -21,6 +21,8 @@ Revision History: #undef min #include "sat/sat_solver.h" +struct lex_error {}; + class stream_buffer { std::istream & m_stream; int m_val; @@ -67,7 +69,7 @@ void skip_line(Buffer & in) { } template -int parse_int(Buffer & in) { +int parse_int(Buffer & in, std::ostream& err) { int val = 0; bool neg = false; skip_whitespace(in); @@ -81,9 +83,8 @@ int parse_int(Buffer & in) { } if (*in < '0' || *in > '9') { - std::cerr << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n"; - exit(3); - exit(ERR_PARSER); + err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n"; + throw lex_error(); } while (*in >= '0' && *in <= '9') { @@ -95,14 +96,14 @@ int parse_int(Buffer & in) { } template -void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) { +void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) { int parsed_lit; int var; lits.reset(); while (true) { - parsed_lit = parse_int(in); + parsed_lit = parse_int(in, err); if (parsed_lit == 0) break; var = abs(parsed_lit); @@ -114,24 +115,30 @@ void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) } template -void parse_dimacs_core(Buffer & in, sat::solver & solver) { +bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) { sat::literal_vector lits; - while (true) { - skip_whitespace(in); - if (*in == EOF) { - break; - } - else if (*in == 'c' || *in == 'p') { - skip_line(in); - } - else { - read_clause(in, solver, lits); - solver.mk_clause(lits.size(), lits.c_ptr()); + try { + while (true) { + skip_whitespace(in); + if (*in == EOF) { + break; + } + else if (*in == 'c' || *in == 'p') { + skip_line(in); + } + else { + read_clause(in, err, solver, lits); + solver.mk_clause(lits.size(), lits.c_ptr()); + } } } + catch (lex_error) { + return false; + } + return true; } -void parse_dimacs(std::istream & in, sat::solver & solver) { +bool parse_dimacs(std::istream & in, std::ostream& err, sat::solver & solver) { stream_buffer _in(in); - parse_dimacs_core(_in, solver); + return parse_dimacs_core(_in, err, solver); } diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h index 50ebec0c8..4c5d51502 100644 --- a/src/sat/dimacs.h +++ b/src/sat/dimacs.h @@ -21,7 +21,7 @@ Revision History: #include "sat/sat_types.h" -void parse_dimacs(std::istream & s, sat::solver & solver); +bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver); #endif /* DIMACS_PARSER_H_ */ diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 3a2af72cf..738566ce2 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -136,7 +136,7 @@ void verify_solution(char const * file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + parse_dimacs(in, std::cerr, solver); sat::model const & m = g_solver->get_model(); for (unsigned i = 1; i < m.size(); i++) { @@ -178,10 +178,10 @@ unsigned read_dimacs(char const * file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + parse_dimacs(in, std::cerr, solver); } else { - parse_dimacs(std::cin, solver); + parse_dimacs(std::cin, std::cerr, solver); } IF_VERBOSE(20, solver.display_status(verbose_stream());); diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 50584c90c..10f3e56a7 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -238,10 +238,10 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + if (!parse_dimacs(in, std::cerr, solver)) return; } else { - parse_dimacs(std::cin, solver); + if (!parse_dimacs(std::cin, std::cerr, solver)) return; } IF_VERBOSE(20, solver.display_status(verbose_stream());); diff --git a/src/test/sat_lookahead.cpp b/src/test/sat_lookahead.cpp index fccbe8eed..23c4a4738 100644 --- a/src/test/sat_lookahead.cpp +++ b/src/test/sat_lookahead.cpp @@ -34,7 +34,8 @@ void tst_sat_lookahead(char ** argv, int argc, int& i) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + if (!parse_dimacs(in, std::cerr, solver)) + return; } sat::lookahead lh(solver);