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