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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-27 16:20:39 -05:00
parent 7db58be904 5d06fa2347
commit 43d9159a74
9 changed files with 253 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
scripts/mk_project.py
View file

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

172
scripts/mk_util.py
View file

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

2
scripts/update_api.py
View file

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

3
src/model/model.cpp
View file

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

12
src/smt/smt_context.cpp
View file

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

15
src/smt/smt_context.h
View file

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

12
src/smt/smt_context_pp.cpp
View file

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

77
src/smt/theory_datatype.cpp
View file

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

16
src/smt/theory_lra.cpp
View file

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