mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 00:43:18 +00:00
Code Activity

fix #1522

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-07 14:26:38 -08:00
parent eb1122c5cb
commit 246941f2d3
5 changed files with 58 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/ast/ast.cpp
View file

@ -1536,34 +1536,35 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
// assigned in the order that they are created, this can result in differing // assigned in the order that they are created, this can result in differing
// family ids. To avoid this, we first assign all family ids and only then inherit plugins. // family ids. To avoid this, we first assign all family ids and only then inherit plugins.
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
symbol fid_name = from.get_family_name(fid); symbol fid_name = from.get_family_name(fid);
if (!m_family_manager.has_family(fid)) { if (!m_family_manager.has_family(fid)) {
family_id new_fid = mk_family_id(fid_name); family_id new_fid = mk_family_id(fid_name);
(void)new_fid; (void)new_fid;
TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
} }
} }
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid)); SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid)); SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
symbol fid_name = from.get_family_name(fid); symbol fid_name = from.get_family_name(fid);
TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid (void)fid_name;
<< ", target has_family: " << m_family_manager.has_family(fid) << "\n"; TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";); << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";); if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
SASSERT(fid == get_family_id(fid_name)); TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
if (from.has_plugin(fid) && !has_plugin(fid)) { SASSERT(fid == get_family_id(fid_name));
decl_plugin * new_p = from.get_plugin(fid)->mk_fresh(); if (from.has_plugin(fid) && !has_plugin(fid)) {
register_plugin(fid, new_p); decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
SASSERT(new_p->get_family_id() == fid); register_plugin(fid, new_p);
SASSERT(has_plugin(fid)); SASSERT(new_p->get_family_id() == fid);
} SASSERT(has_plugin(fid));
if (from.has_plugin(fid)) { }
get_plugin(fid)->inherit(from.get_plugin(fid), trans); if (from.has_plugin(fid)) {
} get_plugin(fid)->inherit(from.get_plugin(fid), trans);
SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid)); }
SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name)); SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
SASSERT(!from.has_plugin(fid) || has_plugin(fid)); SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
SASSERT(!from.has_plugin(fid) || has_plugin(fid));
} }
} }

7
src/ast/ast_pp_util.cpp
View file

@ -46,13 +46,18 @@ void ast_pp_util::display_decls(std::ostream& out) {
n = coll.get_num_decls(); n = coll.get_num_decls();
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
func_decl* f = coll.get_func_decls()[i]; func_decl* f = coll.get_func_decls()[i];
if (f->get_family_id() == null_family_id) { if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
ast_smt2_pp(out, f, env); ast_smt2_pp(out, f, env);
out << "\n"; out << "\n";
} }
} }
} }
void ast_pp_util::remove_decl(func_decl* f) {
m_removed.insert(f);
}
void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) { void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
if (neat) { if (neat) {
smt2_pp_environment_dbg env(m); smt2_pp_environment_dbg env(m);

4
src/ast/ast_pp_util.h
View file

@ -20,9 +20,11 @@ Revision History:
#define AST_PP_UTIL_H_ #define AST_PP_UTIL_H_
#include "ast/decl_collector.h" #include "ast/decl_collector.h"
#include "util/obj_hashtable.h"
class ast_pp_util { class ast_pp_util {
ast_manager& m; ast_manager& m;
obj_hashtable<func_decl> m_removed;
public: public:
decl_collector coll; decl_collector coll;
@ -35,6 +37,8 @@ class ast_pp_util {
void collect(expr_ref_vector const& es); void collect(expr_ref_vector const& es);
void remove_decl(func_decl* f);
void display_decls(std::ostream& out); void display_decls(std::ostream& out);
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true); void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);

32
src/muz/base/dl_context.cpp
View file

@ -1106,6 +1106,16 @@ namespace datalog {
names.push_back(m_rule_names[i]); names.push_back(m_rule_names[i]);
} }
} }
static std::ostream& display_symbol(std::ostream& out, symbol const& nm) {
if (is_smt2_quoted_symbol(nm)) {
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
return out;
}
void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) { void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
ast_manager& m = get_manager(); ast_manager& m = get_manager();
@ -1148,13 +1158,13 @@ namespace datalog {
if (!use_fixedpoint_extensions) { if (!use_fixedpoint_extensions) {
out << "(set-logic HORN)\n"; out << "(set-logic HORN)\n";
} }
for (func_decl * f : rels)
visitor.remove_decl(f);
visitor.display_decls(out); visitor.display_decls(out);
func_decl_set::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) { for (func_decl * f : rels)
func_decl* f = *it;
display_rel_decl(out, f); display_rel_decl(out, f);
}
if (use_fixedpoint_extensions && do_declare_vars) { if (use_fixedpoint_extensions && do_declare_vars) {
declare_vars(rules, fresh_names, out); declare_vars(rules, fresh_names, out);
@ -1185,13 +1195,7 @@ namespace datalog {
nm = symbol(s.str().c_str()); nm = symbol(s.str().c_str());
} }
fresh_names.add(nm); fresh_names.add(nm);
if (is_smt2_quoted_symbol(nm)) { display_symbol(out, nm) << ")";
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
out << ")";
} }
out << ")\n"; out << ")\n";
} }
@ -1219,7 +1223,8 @@ namespace datalog {
PP(qfn); PP(qfn);
out << ")\n"; out << ")\n";
} }
out << "(query " << fn->get_name() << ")\n"; out << "(query ";
display_symbol(out, fn->get_name()) << ")\n";
} }
} }
else { else {
@ -1238,7 +1243,8 @@ namespace datalog {
void context::display_rel_decl(std::ostream& out, func_decl* f) { void context::display_rel_decl(std::ostream& out, func_decl* f) {
smt2_pp_environment_dbg env(m); smt2_pp_environment_dbg env(m);
out << "(declare-rel " << f->get_name() << " ("; out << "(declare-rel ";
display_symbol(out, f->get_name()) << " (";
for (unsigned i = 0; i < f->get_arity(); ++i) { for (unsigned i = 0; i < f->get_arity(); ++i) {
ast_smt2_pp(out, f->get_domain(i), env); ast_smt2_pp(out, f->get_domain(i), env);
if (i + 1 < f->get_arity()) { if (i + 1 < f->get_arity()) {

2
src/test/quant_elim.cpp
View file

@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
#if 0
static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) { static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
// enable_trace("bit2int"); // enable_trace("bit2int");
@ -48,6 +49,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
//exit(-1); //exit(-1);
} }
} }
#endif
static void test_formula(lbool expected_outcome, char const* fml) { static void test_formula(lbool expected_outcome, char const* fml) {
ast_manager m; ast_manager m;