From 81a92edb61e6438961ddaa998592c25381175d08 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 10:59:51 -0700
Subject: [PATCH 1/8] prepare to retool
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 1 +
scripts/mk_util.py | 220 ++++++++++++++++++++++++++++-
src/api/dotnet/Microsoft.Z3.csproj | 1 -
src/api/dotnet/core/project.json | 22 ---
4 files changed, 220 insertions(+), 24 deletions(-)
delete mode 100644 src/api/dotnet/core/project.json
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index d94089a9c..174b498e7 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -84,6 +84,7 @@ def init_project_def():
export_files=API_files,
staging_link='python')
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
+ add_dot_net_core_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 97e2b65f2..e5173931d 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -37,6 +37,7 @@ OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
OCAML_LIB=getenv("OCAML_LIB", None)
OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
CSC=getenv("CSC", None)
+DOTNET="dotnet"
GACUTIL=getenv("GACUTIL", 'gacutil')
# Standard install directories relative to PREFIX
INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
@@ -87,6 +88,7 @@ VS_PROJ = False
TRACE = False
PYTHON_ENABLED=False
DOTNET_ENABLED=False
+DOTNET_CORE_ENABLED=False
DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
JAVA_ENABLED=False
ML_ENABLED=False
@@ -690,7 +692,7 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
- global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
+ global DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC
global GUARD_CF, ALWAYS_DYNAMIC_BASE
try:
@@ -731,6 +733,9 @@ def parse_options():
TRACE = True
elif opt in ('-.net', '--dotnet'):
DOTNET_ENABLED = True
+ elif opt in ('--dotnetcore'):
+ DOTNET_ENABLED = True
+ DOTNET_CORE_ENABLED = True
elif opt in ('--dotnet-key'):
DOTNET_KEY_FILE = arg
elif opt in ('--staticlib'):
@@ -887,6 +892,9 @@ def is_js_enabled():
def is_dotnet_enabled():
return DOTNET_ENABLED
+def is_dotnet_core_enabled():
+ return DOTNET_CORE_ENABLED
+
def is_python_enabled():
return PYTHON_ENABLED
@@ -1811,6 +1819,212 @@ class DotNetDLLComponent(Component):
pkg_config_file = os.path.join('lib','pkgconfig','{}.pc'.format(self.gac_pkg_name()))
MakeRuleCmd.remove_installed_files(out, pkg_config_file)
+
+# TBD: retool the following for 'dotnet build'
+class DotNetCoreDLLComponent(Component):
+ def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file):
+ Component.__init__(self, name, path, deps)
+ if dll_name is None:
+ dll_name = name
+ if assembly_info_dir is None:
+ assembly_info_dir = "."
+ self.dll_name = dll_name
+ 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_enabled():
+ return
+ cs_fp_files = []
+ cs_files = []
+ for cs_file in get_cs_files(self.src_dir):
+ cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
+ cs_files.append(cs_file)
+ if self.assembly_info_dir != '.':
+ for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
+ cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
+ cs_files.append(os.path.join(self.assembly_info_dir, cs_file))
+ dllfile = '%s.dll' % self.dll_name
+ out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
+ for cs_file in cs_fp_files:
+ out.write(' ')
+ out.write(cs_file)
+ out.write('\n')
+
+ cscCmdLine = [DOTNET]
+ if IS_WINDOWS:
+ # Using these flags under the mono compiler results in build errors.
+ cscCmdLine.extend( [# What is the motivation for this?
+ '/noconfig',
+ '/nostdlib+',
+ '/reference:mscorlib.dll',
+ ]
+ )
+
+ # 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
+
+ if not self.key_file is None:
+ print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
+ if (self.key_file.find(' ') != -1):
+ self.key_file = '"' + self.key_file + '"'
+ cscCmdLine.append('/keyfile:{}'.format(self.key_file))
+
+ cscCmdLine.extend( ['/unsafe+',
+ '/nowarn:1701,1702',
+ '/errorreport:prompt',
+ '/warn:4',
+ '/reference:System.Core.dll',
+ '/reference:System.dll',
+ '/reference:System.Numerics.dll',
+ '/filealign:512', # Why!?
+ '/out:{}.dll'.format(self.dll_name),
+ '/target:library',
+ '/doc:{}.xml'.format(self.dll_name),
+ ]
+ )
+ if DEBUG_MODE:
+ cscCmdLine.extend( ['"/define:DEBUG;TRACE"', # Needs to be quoted due to ``;`` being a shell command separator
+ '/debug+',
+ '/debug:full',
+ '/optimize-'
+ ]
+ )
+ else:
+ cscCmdLine.extend(['/optimize+'])
+
+ if IS_WINDOWS:
+ if VS_X64:
+ cscCmdLine.extend(['/platform:x64'])
+ elif VS_ARM:
+ cscCmdLine.extend(['/platform:arm'])
+ else:
+ cscCmdLine.extend(['/platform:x86'])
+ else:
+ # Just use default platform for now.
+ # If the dlls are run using mono then it
+ # ignores what the platform is set to anyway.
+ pass
+
+ for cs_file in cs_files:
+ cscCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file)))
+
+ # Now emit the command line
+ MakeRuleCmd.write_cmd(out, ' '.join(cscCmdLine))
+
+ # 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):
+ return True
+
+ def mk_win_dist(self, build_path, dist_path):
+ if is_dotnet_core_enabled():
+ 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))
+ 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))
+
+ def mk_unix_dist(self, build_path, dist_path):
+ if is_dotnet_core_enabled():
+ 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))
+
+ 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)))
+
+ def mk_install(self, out):
+ if not DOTNET_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)
+
+ 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)
+
class JavaDLLComponent(Component):
def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
Component.__init__(self, name, path, deps)
@@ -2347,6 +2561,10 @@ def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=N
c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
reg_component(name, c)
+def add_dot_net_core_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None):
+ c = DotNetCoreDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
+ reg_component(name, c)
+
def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None):
c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
reg_component(name, c)
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
index cde8b78c9..9aaa70821 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj
+++ b/src/api/dotnet/Microsoft.Z3.csproj
@@ -360,7 +360,6 @@
<Compile Include="FuncDecl.cs" />
<Compile Include="FuncInterp.cs" />
<Compile Include="Goal.cs" />
- <Compile Include="InterpolationContext.cs" />
<Compile Include="IntExpr.cs" />
<Compile Include="IntNum.cs" />
<Compile Include="IntSort.cs" />
diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json
deleted file mode 100644
index d54b6877b..000000000
--- a/src/api/dotnet/core/project.json
+++ /dev/null
@@ -1,22 +0,0 @@
-{
- "version": "1.0.0-*",
- "buildOptions": {
- "debugType": "portable",
- "emitEntryPoint": false,
- "outputName": "Microsoft.Z3",
- "compile": [ "../*.cs", "*.cs" ],
- "define": ["DOTNET_CORE"]
- },
- "dependencies": { },
- "frameworks": {
- "netcoreapp1.0": {
- "dependencies": {
- "Microsoft.NETCore.App": {
- "type": "platform",
- "version": "1.0.1"
- }
- },
- "imports": "dnxcore50"
- }
- }
-}
From 163e1e3e55bff7e839b3528676e65b79ef44a9cf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 11:03:41 -0700
Subject: [PATCH 2/8] avoid name clash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 8c037f2e5..18d57e729 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -84,7 +84,7 @@ def init_project_def():
export_files=API_files,
staging_link='python')
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
- add_dot_net_core_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
+ add_dot_net_core_dll('dotnetcore', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
From 7c043dee7de6270a9c4248750967445d6a3e1348 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 11:07:17 -0700
Subject: [PATCH 3/8] more prep for dotnetcore
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_util.py | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 5b4d31d3e..baf258c90 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -699,7 +699,7 @@ def parse_options():
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
- 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
+ 'trace', 'dotnet', 'dotnetcore', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync'])
except:
print("ERROR: Invalid command line option")
@@ -733,7 +733,7 @@ def parse_options():
TRACE = True
elif opt in ('-.net', '--dotnet'):
DOTNET_ENABLED = True
- elif opt in ('--dotnetcore'):
+ elif opt in ('--dotnetcore',):
DOTNET_ENABLED = True
DOTNET_CORE_ENABLED = True
elif opt in ('--dotnet-key'):
From 4616ddf103c9688adcccaac124b5e407a0ec2933 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 11:50:07 -0700
Subject: [PATCH 4/8] more prep for dotnet core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_util.py | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index baf258c90..b11505ad2 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -734,7 +734,6 @@ def parse_options():
elif opt in ('-.net', '--dotnet'):
DOTNET_ENABLED = True
elif opt in ('--dotnetcore',):
- DOTNET_ENABLED = True
DOTNET_CORE_ENABLED = True
elif opt in ('--dotnet-key'):
DOTNET_KEY_FILE = arg
@@ -893,6 +892,7 @@ def is_dotnet_enabled():
return DOTNET_ENABLED
def is_dotnet_core_enabled():
+ print("core %s" % DOTNET_CORE_ENABLED)
return DOTNET_CORE_ENABLED
def is_python_enabled():
@@ -1857,7 +1857,7 @@ class DotNetCoreDLLComponent(Component):
def mk_makefile(self, out):
global DOTNET_KEY_FILE
- if not is_dotnet_enabled():
+ if not is_dotnet_core_enabled():
return
cs_fp_files = []
cs_files = []
@@ -2008,7 +2008,7 @@ class DotNetCoreDLLComponent(Component):
flags=' '.join(gacUtilFlags)))
def mk_install(self, out):
- if not DOTNET_ENABLED:
+ if not is_dotnet_core_enabled():
return
self._install_or_uninstall_to_gac(out, install=True)
@@ -2872,6 +2872,8 @@ def mk_config():
if is_dotnet_enabled():
print('C# Compiler: %s' % CSC)
print('GAC utility: %s' % GACUTIL)
+ if is_dotnet_core_enabled():
+ print('C# Compiler: %s' % DOTNET)
config.close()
@@ -3197,6 +3199,8 @@ def mk_bindings(api_files):
dotnet_output_dir = None
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
java_output_dir = None
java_package_name = None
if is_java_enabled():
From 540922766d0b07fb90d0b5a2ce3a0a26ec2f1350 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 12:15:54 -0700
Subject: [PATCH 5/8] more dotnetcore preparation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_util.py | 22 +++++++++++-----------
1 file changed, 11 insertions(+), 11 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index b11505ad2..00bc20e29 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1875,10 +1875,10 @@ class DotNetCoreDLLComponent(Component):
out.write(cs_file)
out.write('\n')
- cscCmdLine = [DOTNET]
+ dotnetCmdLine = [DOTNET]
if IS_WINDOWS:
# Using these flags under the mono compiler results in build errors.
- cscCmdLine.extend( [# What is the motivation for this?
+ dotnetCmdLine.extend( [# What is the motivation for this?
'/noconfig',
'/nostdlib+',
'/reference:mscorlib.dll',
@@ -1903,9 +1903,9 @@ class DotNetCoreDLLComponent(Component):
print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
if (self.key_file.find(' ') != -1):
self.key_file = '"' + self.key_file + '"'
- cscCmdLine.append('/keyfile:{}'.format(self.key_file))
+ dotnetCmdLine.append('/keyfile:{}'.format(self.key_file))
- cscCmdLine.extend( ['/unsafe+',
+ dotnetCmdLine.extend( ['/unsafe+',
'/nowarn:1701,1702',
'/errorreport:prompt',
'/warn:4',
@@ -1919,22 +1919,22 @@ class DotNetCoreDLLComponent(Component):
]
)
if DEBUG_MODE:
- cscCmdLine.extend( ['"/define:DEBUG;TRACE"', # Needs to be quoted due to ``;`` being a shell command separator
+ dotnetCmdLine.extend( ['"/define:DEBUG;TRACE"', # Needs to be quoted due to ``;`` being a shell command separator
'/debug+',
'/debug:full',
'/optimize-'
]
)
else:
- cscCmdLine.extend(['/optimize+'])
+ dotnetCmdLine.extend(['/optimize+'])
if IS_WINDOWS:
if VS_X64:
- cscCmdLine.extend(['/platform:x64'])
+ dotnetCmdLine.extend(['/platform:x64'])
elif VS_ARM:
- cscCmdLine.extend(['/platform:arm'])
+ dotnetCmdLine.extend(['/platform:arm'])
else:
- cscCmdLine.extend(['/platform:x86'])
+ dotnetCmdLine.extend(['/platform:x86'])
else:
# Just use default platform for now.
# If the dlls are run using mono then it
@@ -1942,10 +1942,10 @@ class DotNetCoreDLLComponent(Component):
pass
for cs_file in cs_files:
- cscCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file)))
+ dotnetCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file)))
# Now emit the command line
- MakeRuleCmd.write_cmd(out, ' '.join(cscCmdLine))
+ 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
From 52801db3fdc7a39df212ec8579c92deffd6f2d01 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Oct 2018 16:28:01 -0700
Subject: [PATCH 6/8] more dotnet core prepration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_util.py | 80 +++++++------------------------------------
scripts/update_api.py | 2 +-
2 files changed, 14 insertions(+), 68 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 00bc20e29..6372e87fc 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -892,7 +892,6 @@ def is_dotnet_enabled():
return DOTNET_ENABLED
def is_dotnet_core_enabled():
- print("core %s" % DOTNET_CORE_ENABLED)
return DOTNET_CORE_ENABLED
def is_python_enabled():
@@ -1875,75 +1874,22 @@ class DotNetCoreDLLComponent(Component):
out.write(cs_file)
out.write('\n')
- dotnetCmdLine = [DOTNET]
- if IS_WINDOWS:
- # Using these flags under the mono compiler results in build errors.
- dotnetCmdLine.extend( [# What is the motivation for this?
- '/noconfig',
- '/nostdlib+',
- '/reference:mscorlib.dll',
- ]
- )
-
- # 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
-
- if not self.key_file is None:
- print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
- if (self.key_file.find(' ') != -1):
- self.key_file = '"' + self.key_file + '"'
- dotnetCmdLine.append('/keyfile:{}'.format(self.key_file))
-
- dotnetCmdLine.extend( ['/unsafe+',
- '/nowarn:1701,1702',
- '/errorreport:prompt',
- '/warn:4',
- '/reference:System.Core.dll',
- '/reference:System.dll',
- '/reference:System.Numerics.dll',
- '/filealign:512', # Why!?
- '/out:{}.dll'.format(self.dll_name),
- '/target:library',
- '/doc:{}.xml'.format(self.dll_name),
- ]
- )
+ # TBD: can this be replaced by running "dotnet new classlib"?
+ 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( ['"/define:DEBUG;TRACE"', # Needs to be quoted due to ``;`` being a shell command separator
- '/debug+',
- '/debug:full',
- '/optimize-'
- ]
- )
+ dotnetCmdLine.extend(['Debug'])
else:
- dotnetCmdLine.extend(['/optimize+'])
-
- if IS_WINDOWS:
- if VS_X64:
- dotnetCmdLine.extend(['/platform:x64'])
- elif VS_ARM:
- dotnetCmdLine.extend(['/platform:arm'])
- else:
- dotnetCmdLine.extend(['/platform:x86'])
- else:
- # Just use default platform for now.
- # If the dlls are run using mono then it
- # ignores what the platform is set to anyway.
- pass
-
- for cs_file in cs_files:
- dotnetCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file)))
+ dotnetCmdLine.extend(['Release'])
+ path = os.path.abspath(BUILD_DIR)
+ dotnetCmdLine.extend(['-o', path])
+
# Now emit the command line
MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 917df94a2..e04e37332 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1868,7 +1868,7 @@ def generate_files(api_files,
mk_dotnet_wrappers(dotnet_file)
if mk_util.is_verbose():
print("Generated '{}'".format(dotnet_file.name))
-
+
if java_output_dir:
mk_java(java_output_dir, java_package_name)
From 184ae7211e8f51f39f6bc9e540221684f7912cbd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 Oct 2018 10:00:57 -0700
Subject: [PATCH 7/8] fix #1897
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 14 +++----
src/smt/smt_context.h | 16 ++++++++
src/smt/smt_context_pp.cpp | 12 ++++++
src/smt/theory_datatype.cpp | 77 +++++++++++++++++++------------------
src/smt/theory_lra.cpp | 16 ++++----
5 files changed, 82 insertions(+), 53 deletions(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 17a7ce3a3..41f11dca2 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -494,7 +494,7 @@ namespace smt {
try {
TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
- TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n";
+ TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
tout << "kind: " << js.get_kind() << "\n";);
m_stats.m_num_add_eq++;
@@ -1232,7 +1232,7 @@ namespace smt {
if (depth == 0)
return false;
if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
- TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
+ TRACE("is_ext_diseq", tout << enode_pp(n1, *this) << " " << enode_pp(n2, *this) << " " << depth << "\n";);
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
@@ -1241,7 +1241,7 @@ namespace smt {
if (!p1->is_cgr())
continue;
func_decl * f = p1->get_decl();
- TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
+ TRACE("is_ext_diseq", tout << "p1: " << enode_pp(p1, *this) << "\n";);
unsigned num_args = p1->get_num_args();
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
@@ -1250,7 +1250,7 @@ namespace smt {
continue;
if (!p2->is_cgr())
continue;
- TRACE("is_ext_diseq", tout << "p2: " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";);
+ TRACE("is_ext_diseq", tout << "p2: " << enode_pp(p2, *this) << "\n";);
if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) {
unsigned j = 0;
for (j = 0; j < num_args; j++) {
@@ -1264,7 +1264,7 @@ namespace smt {
break;
}
if (j == num_args) {
- TRACE("is_ext_diseq", tout << "found parents: " << mk_bounded_pp(p1->get_owner(), m_manager) << " " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";);
+ TRACE("is_ext_diseq", tout << "found parents: " << enode_pp(p1, *this) << " " << enode_pp(p2, *this) << "\n";);
if (is_ext_diseq(p1, p2, depth - 1))
return true;
}
@@ -1770,7 +1770,7 @@ namespace smt {
void context::set_conflict(const b_justification & js, literal not_l) {
if (!inconsistent()) {
- TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
+ TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); );
m_conflict = js;
m_not_l = not_l;
}
@@ -4290,7 +4290,7 @@ namespace smt {
for (enode * parent : enode::parents(n)) {
family_id fid = parent->get_owner()->get_family_id();
if (fid != th_id && fid != m_manager.get_basic_family_id()) {
- TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);
+ TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";);
return true;
}
}
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 5733829a3..d0c9cc776 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1609,6 +1609,22 @@ namespace smt {
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
};
+ struct enode_eq_pp {
+ context const& ctx;
+ enode_pair const& p;
+ enode_eq_pp(enode_pair const& p, context const& ctx): ctx(ctx), p(p) {}
+ };
+
+ std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p);
+
+ struct enode_pp {
+ context const& ctx;
+ enode* n;
+ enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
+ };
+
+ std::ostream& operator<<(std::ostream& out, enode_pp const& p);
+
};
#endif /* SMT_CONTEXT_H_ */
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index fb67d91d6..5dea80f5e 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -603,5 +603,17 @@ namespace smt {
display(out, j);
}
+ std::ostream& operator<<(std::ostream& out, enode_pp const& p) {
+ ast_manager& m = p.ctx.get_manager();
+ enode* n = p.n;
+ return out << "[#" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "]";
+ }
+
+ std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {
+ return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n";
+ }
+
+
+
};
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 049555297..6aa49efae 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -365,7 +365,7 @@ namespace smt {
if (!is_recognizer(n))
return;
TRACE("datatype", tout << "assigning recognizer: #" << n->get_owner_id() << " is_true: " << is_true << "\n"
- << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
+ << enode_pp(n, ctx) << "\n";);
SASSERT(n->get_num_args() == 1);
enode * arg = n->get_arg(0);
theory_var tv = arg->get_th_var(get_id());
@@ -393,11 +393,10 @@ namespace smt {
}
void theory_datatype::relevant_eh(app * n) {
- TRACE("datatype", tout << "relevant_eh: " << mk_bounded_pp(n, get_manager()) << "\n";);
context & ctx = get_context();
+ TRACE("datatype", tout << "relevant_eh: " << mk_pp(n, get_manager()) << "\n";);
SASSERT(ctx.relevancy());
if (is_recognizer(n)) {
- TRACE("datatype", tout << "relevant_eh: #" << n->get_id() << "\n" << mk_bounded_pp(n, get_manager()) << "\n";);
SASSERT(ctx.e_internalized(n));
enode * e = ctx.get_enode(n);
theory_var v = e->get_arg(0)->get_th_var(get_id());
@@ -483,31 +482,41 @@ namespace smt {
SASSERT(app->get_root() == root->get_root());
if (app != root)
m_used_eqs.push_back(enode_pair(app, root));
+
+ TRACE("datatype",
+ tout << "occurs_check\n";
+ for (enode_pair const& p : m_used_eqs) {
+ tout << enode_eq_pp(p, get_context());
+ });
}
// start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) {
- oc_mark_on_stack(app);
- theory_var v = app->get_root()->get_th_var(get_id());
- if (v != null_theory_var) {
- v = m_find.find(v);
- var_data * d = m_var_data[v];
- if (d->m_constructor) {
- for (enode * arg : enode::args(d->m_constructor)) {
- if (oc_cycle_free(arg)) {
- continue;
- }
- if (oc_on_stack(arg)) {
- // arg was explored before app, and is still on the stack: cycle
- occurs_check_explain(app, arg);
- return true;
- }
- // explore `arg` (with parent `app`)
- if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
- m_parent.insert(arg->get_root(), app);
- oc_push_stack(arg);
- }
- }
+ app = app->get_root();
+ theory_var v = app->get_th_var(get_id());
+ if (v == null_theory_var) {
+ return false;
+ }
+ v = m_find.find(v);
+ var_data * d = m_var_data[v];
+ if (!d->m_constructor) {
+ return false;
+ }
+ enode * parent = d->m_constructor;
+ oc_mark_on_stack(parent);
+ for (enode * arg : enode::args(parent)) {
+ if (oc_cycle_free(arg)) {
+ continue;
+ }
+ if (oc_on_stack(arg)) {
+ // arg was explored before app, and is still on the stack: cycle
+ occurs_check_explain(parent, arg);
+ return true;
+ }
+ // explore `arg` (with paren)
+ if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
+ m_parent.insert(arg->get_root(), parent);
+ oc_push_stack(arg);
}
}
return false;
@@ -521,7 +530,7 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
- TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
+ TRACE("datatype", tout << "occurs check: " << enode_pp(n, get_context()) << "\n";);
m_stats.m_occurs_check++;
bool res = false;
@@ -535,7 +544,7 @@ namespace smt {
if (oc_cycle_free(app)) continue;
- TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";);
+ TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, get_context()) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) {
case ENTER:
@@ -553,12 +562,6 @@ namespace smt {
context & ctx = get_context();
region & r = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
- TRACE("datatype",
- tout << "occurs_check: true\n";
- for (enode_pair const& p : m_used_eqs) {
- tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
- tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
- });
}
return res;
}
@@ -613,7 +616,7 @@ namespace smt {
var_data * d = m_var_data[v];
out << "v" << v << " #" << get_enode(v)->get_owner_id() << " -> v" << m_find.find(v) << " ";
if (d->m_constructor)
- out << mk_bounded_pp(d->m_constructor->get_owner(), get_manager());
+ out << enode_pp(d->m_constructor, get_context());
else
out << "(null)";
out << "\n";
@@ -778,11 +781,11 @@ namespace smt {
SASSERT(!lits.empty());
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
- for (unsigned i = 0; i < lits.size(); i++) {
- ctx.display_detailed_literal(tout, lits[i]); tout << "\n";
+ for (literal l : lits) {
+ ctx.display_detailed_literal(tout, l); tout << "\n";
}
- for (unsigned i = 0; i < eqs.size(); i++) {
- tout << mk_ismt2_pp(eqs[i].first->get_owner(), get_manager()) << " = " << mk_ismt2_pp(eqs[i].second->get_owner(), get_manager()) << "\n";
+ for (auto const& p : eqs) {
+ tout << enode_eq_pp(p, ctx);
});
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr())));
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 4a04fdaaf..0b25aa626 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1361,8 +1361,7 @@ public:
}
enode* n2 = get_enode(other);
if (n1->get_root() != n2->get_root()) {
- TRACE("arith", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
- tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
+ TRACE("arith", tout << enode_eq_pp(enode_pair(n1, n2), ctx());
tout << "v" << v << " = " << "v" << other << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(v, other));
result = true;
@@ -2800,15 +2799,15 @@ public:
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith",
- for (unsigned i = 0; i < m_core.size(); ++i) {
- ctx().display_detailed_literal(tout, m_core[i]);
+ for (literal c : m_core) {
+ ctx().display_detailed_literal(tout, c);
tout << "\n";
}
- for (unsigned i = 0; i < m_eqs.size(); ++i) {
- tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
+ for (enode_pair const& p : m_eqs) {
+ tout << enode_eq_pp(p, ctx());
}
tout << " ==> ";
- tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
+ tout << enode_pp(x, ctx()) << " = " << enode_pp(y, ctx()) << "\n";
);
// parameters are TBD.
@@ -3371,8 +3370,7 @@ public:
break;
}
case equality_source:
- out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = "
- << mk_pp(m_equalities[idx].second->get_owner(), m) << "\n";
+ out << enode_eq_pp(m_equalities[idx], ctx());
break;
case definition_source: {
theory_var v = m_definitions[idx];
From 5d06fa23479d33fa81ba0751d4cd9e8aad94ea14 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Oct 2018 17:29:09 -0500
Subject: [PATCH 8/8] fix #1901
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/model/model.cpp | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 60441054c..2efc39db8 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -410,8 +410,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
}
else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) &&
fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
- var_subst vs(m);
- // ? TBD args.reverse();
+ var_subst vs(m, false);
new_t = vs(fi->get_interp(), args.size(), args.c_ptr());
}
#if 0