mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-17 15:05:02 -08:00
parent 9ec59fdb93 b7ecd4fa7a
commit ee7781e602
16 changed files with 330 additions and 147 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/c/test_capi.c
View file

@ -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);

113
scripts/mk_nuget_release.py Normal file
View file

@ -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 = """<?xml version="1.0" encoding="utf-8"?>
<package xmlns="http://schemas.microsoft.com/packaging/2010/07/nuspec.xsd">
<metadata>
<id>Microsoft.Z3.x64</id>
<version>%s</version>
<authors>Microsoft</authors>
<description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</description>
<copyright>Copyright Microsoft Corporation. All rights reserved.</copyright>
<tags>smt constraint solver theorem prover</tags>
<iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg</iconUrl>
<projectUrl>https://github.com/Z3Prover/z3</projectUrl>
<licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt</licenseUrl>
<repository
type="git"
url="https://github.com/Z3Prover/z3.git"
branch="master"
/>
<requireLicenseAcceptance>true</requireLicenseAcceptance>
<language>en</language>
</metadata>
</package>"""
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()

5
scripts/mk_project.py
View file

@ -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'])

16
scripts/mk_unix_dist.py
View file

@ -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 <sudir>, --build=<subdir> 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=<file> sign the .NET assembly with the private key in <file>.")
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

240
scripts/mk_util.py
View file

@ -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=<file> sign the .NET assembly using the private key in <file>.")
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 = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
if VS_X64:
platform = 'x64'
elif VS_ARM:
platform = 'ARM'
else:
platform = 'x86'
version = get_version_string(3)
core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<TargetFramework>netstandard1.4</TargetFramework>
<PlatformTarget>%s</PlatformTarget>
<DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
<DebugType>portable</DebugType>
<AssemblyName>Microsoft.Z3</AssemblyName>
<OutputType>Library</OutputType>
<PackageId>Microsoft.Z3</PackageId>
<RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
<Version>%s</Version>
<GeneratePackageOnBuild>true</GeneratePackageOnBuild>
<Authors>Microsoft</Authors>
<Company>Microsoft</Company>
<Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
<Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
<PackageTags>smt constraint solver theorem prover</PackageTags>
%s
</PropertyGroup>
<ItemGroup>
<Compile Include="..\%s\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
</ItemGroup>
</Project>""" % (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 = """<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<OutputType>Exe</OutputType>
<TargetFramework>netcoreapp2.0</TargetFramework>
<PlatformTarget>%s</PlatformTarget>
</PropertyGroup>
<ItemGroup>
<Compile Include="..\%s/*.cs" />
<Reference Include="Microsoft.Z3">
<HintPath>..\Microsoft.Z3.dll</HintPath>
</Reference>
</ItemGroup>
</Project>""" % (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))

2
scripts/mk_win_dist.py
View file

@ -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

6
src/api/api_solver.cpp
View file

@ -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<sat2goal::mc> mc;
atom2bool_var a2b(m);

2
src/api/z3_api.h
View file

@ -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.

12
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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;
}

2
src/ast/seq_decl_plugin.cpp
View file

@ -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)) {

11
src/parsers/smt2/smt2parser.cpp
View file

@ -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;

47
src/sat/dimacs.cpp
View file

@ -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<typename Buffer>
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<typename Buffer>
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<typename Buffer>
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);
}

2
src/sat/dimacs.h
View file

@ -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_ */

6
src/shell/dimacs_frontend.cpp
View file

@ -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()););

4
src/test/cnf_backbones.cpp
View file

@ -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()););

3
src/test/sat_lookahead.cpp
View file

@ -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);