diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 3003578bf..18d57e729 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('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'])
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0657a2686..6372e87fc 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,14 +692,14 @@ 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:
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")
@@ -731,6 +733,8 @@ def parse_options():
TRACE = True
elif opt in ('-.net', '--dotnet'):
DOTNET_ENABLED = True
+ elif opt in ('--dotnetcore',):
+ DOTNET_CORE_ENABLED = True
elif opt in ('--dotnet-key'):
DOTNET_KEY_FILE = arg
elif opt in ('--staticlib'):
@@ -887,6 +891,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 +1818,159 @@ 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_core_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')
+
+ # 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(['Debug'])
+ else:
+ dotnetCmdLine.extend(['Release'])
+
+ path = os.path.abspath(BUILD_DIR)
+ dotnetCmdLine.extend(['-o', path])
+
+ # Now emit the command line
+ MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
+
+ # State that the high-level "dotnet" target depends on the .NET bindings
+ # dll we just created the build rule for
+ out.write('\n')
+ out.write('%s: %s\n\n' % (self.name, dllfile))
+
+ # Create pkg-config file
+ self.mk_pkg_config_file()
+ return
+
+ def main_component(self):
+ return is_dotnet_core_enabled()
+
+ def has_assembly_info(self):
+ 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 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)
+
+ 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 +2507,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)
@@ -2654,6 +2818,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()
@@ -2979,6 +3145,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():
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)
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
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 15887920a..21af24b32 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -495,7 +495,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++;
@@ -1233,7 +1233,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;
@@ -1242,7 +1242,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))
@@ -1251,7 +1251,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++) {
@@ -1265,7 +1265,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;
}
@@ -4316,7 +4316,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 f628b6e95..6f382a5f6 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1648,6 +1648,21 @@ namespace smt {
return out << "}";
}
+ 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);
};
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];