mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 03:15:50 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
102d23f780
16 changed files with 327 additions and 227 deletions
|
|
@ -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 = """<?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()
|
||||
# create_nuget_dir()
|
||||
download_installs()
|
||||
unpack()
|
||||
# create_nuget_package()
|
||||
|
||||
create_nuget_spec()
|
||||
create_nuget_package()
|
||||
|
||||
|
||||
main()
|
||||
|
|
|
|||
|
|
@ -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'])
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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=<file> sign the .NET assembly using the private key in <file>.")
|
||||
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 = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
|
||||
|
||||
if VS_X64:
|
||||
platform = 'x64'
|
||||
|
|
@ -1878,14 +1880,13 @@ class DotNetCoreDLLComponent(Component):
|
|||
core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
|
||||
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netcoreapp1.0</TargetFramework>
|
||||
<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>
|
||||
<PackageTargetFallback>$(PackageTargetFallback);dnxcore50</PackageTargetFallback>
|
||||
<RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
|
||||
<Version>%s</Version>
|
||||
<GeneratePackageOnBuild>true</GeneratePackageOnBuild>
|
||||
|
|
@ -1894,13 +1895,14 @@ class DotNetCoreDLLComponent(Component):
|
|||
<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, self.to_src_dir)
|
||||
</Project>""" % (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):
|
|||
<PlatformTarget>%s</PlatformTarget>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="%s/*.cs" />
|
||||
<Compile Include="..\%s/*.cs" />
|
||||
<Reference Include="Microsoft.Z3">
|
||||
<HintPath>Microsoft.Z3.dll</HintPath>
|
||||
<HintPath>..\Microsoft.Z3.dll</HintPath>
|
||||
</Reference>
|
||||
</ItemGroup>
|
||||
</Project>""" % (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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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 <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.")
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -931,6 +931,26 @@ namespace Microsoft.Z3
|
|||
return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create an expression representing <c>t1 xor t2 xor t3 ... </c>.
|
||||
/// </summary>
|
||||
public BoolExpr MkXor(IEnumerable<BoolExpr> ts)
|
||||
{
|
||||
Debug.Assert(ts != null);
|
||||
Debug.Assert(ts.All(a => a != null));
|
||||
CheckContextMatch<BoolExpr>(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;
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create an expression representing <c>t[0] and t[1] and ...</c>.
|
||||
/// </summary>
|
||||
|
|
|
|||
|
|
@ -238,6 +238,14 @@ namespace Microsoft.Z3
|
|||
return Eval(t, completion);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Evaluate expression to a double, assuming it is a numeral already.
|
||||
/// </summary>
|
||||
public double Double(Expr t) {
|
||||
var r = Eval(t, true);
|
||||
return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The number of uninterpreted sorts that the model has an interpretation for.
|
||||
/// </summary>
|
||||
|
|
|
|||
|
|
@ -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()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -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())
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<exprs>& 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<weighted_core>& 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<exprs> cores;
|
||||
vector<weighted_core> 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<exprs> const& cores) {
|
||||
void process_unsat(vector<weighted_core> 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<solver> 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> _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> _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<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
|
||||
smt_solver->assert_expr(s().get_assertions());
|
||||
ref<solver> _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);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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<func_decl>::iterator it = bits.begin();
|
||||
obj_hashtable<func_decl>::iterator end = bits.end();
|
||||
for (; it != end; ++it) {
|
||||
tout << (*it)->get_name() << " ";
|
||||
for (func_decl* f : bits) {
|
||||
tout << f->get_name() << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
|
|
|
|||
|
|
@ -161,19 +161,15 @@ struct param_descrs::imp {
|
|||
|
||||
void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
|
||||
svector<symbol> names;
|
||||
dictionary<info>::iterator it = m_info.begin();
|
||||
dictionary<info>::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<symbol>::iterator it2 = names.begin();
|
||||
svector<symbol>::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<unsigned>(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<info>::iterator it = other.m_imp->m_info.begin();
|
||||
dictionary<info>::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<params::entry>::iterator it = m_entries.begin();
|
||||
svector<params::entry>::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<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::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 << " " <<it->second.m_uint_value;
|
||||
out << " " <<e.second.m_uint_value;
|
||||
break;
|
||||
case CPK_DOUBLE:
|
||||
out << " " << it->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<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::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 << " " <<it->second.m_uint_value;
|
||||
out << " " <<e.second.m_uint_value;
|
||||
break;
|
||||
case CPK_DOUBLE:
|
||||
out << " " << it->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<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::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);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue