diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c00c78b7e..454f14261 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1796,11 +1796,11 @@ bool ast_manager::slow_not_contains(ast const * n) { #if 0 static unsigned s_count = 0; -static void track_id(ast* n, unsigned id) { +static void track_id(ast_manager& m, ast* n, unsigned id) { if (n->get_id() != id) return; ++s_count; - std::cout << s_count << "\n"; - //SASSERT(s_count != 1); + std::cout << &m << " " << s_count << "\n"; + SASSERT(s_count != 240); } #endif @@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - // track_id(n, 77); + // track_id(*this, n, 254); TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 10e7bc367..04bf40b5e 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -21,6 +21,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" #include "ast/ast_translation.h" @@ -353,6 +354,7 @@ namespace datatype { } #define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function " #_pred_); +#define VALIDATE_PARAM_PP(_pred_, _msg_) if (!(_pred_)) m_manager->raise_exception(_msg_); func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -368,8 +370,10 @@ namespace datatype { func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) { ast_manager& m = *m_manager; - VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[1].is_symbol() && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); + VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[1].is_symbol()); + VALIDATE_PARAM(parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); VALIDATE_PARAM(u().is_datatype(domain[0])); + VALIDATE_PARAM(to_func_decl(parameters[0].get_ast())->get_range()== domain[0]) // blindly trust that parameter is a constructor sort* range = m_manager->mk_bool_sort(); func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters); @@ -382,6 +386,7 @@ namespace datatype { ast_manager& m = *m_manager; VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); VALIDATE_PARAM(u().is_datatype(domain[0])); + VALIDATE_PARAM_PP(domain[0] == to_func_decl(parameters[0].get_ast())->get_range(), "invalid sort argument passed to recognizer"); // blindly trust that parameter is a constructor sort* range = m_manager->mk_bool_sort(); func_decl_info info(m_family_id, OP_DT_IS, num_parameters, parameters); @@ -537,10 +542,15 @@ namespace datatype { sort_ref_vector ps(*m_manager); for (symbol const& s : m_def_block) { new_sorts.push_back(m_defs[s]->instantiate(ps)); - if (m_manager->has_trace_stream()) { - log_axiom_definitions(s, new_sorts.back()); + } + if (m_manager->has_trace_stream()) { + for (unsigned i = 0; i < m_def_block.size(); ++i) { + symbol const& s = m_def_block[i]; + sort* srt = new_sorts.get(i); + log_axiom_definitions(s, srt); } } + return true; } diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 051684dce..4d98f0665 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -16,6 +16,7 @@ Author: Revision History: --*/ +#include "ast/ast_pp.h" #include "smt/smt_context.h" #include "smt/smt_enode.h" diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 2d558e29e..ea0c4ccc7 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -127,30 +127,34 @@ namespace smt { where acc_i are the accessors of constructor c. */ void theory_datatype::assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent) { - TRACE("datatype_bug", tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n" << mk_pp(n->get_owner(), get_manager()) << "\n";); + ast_manager& m = get_manager(); + app* e = n->get_owner(); + TRACE("datatype_bug", tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n" + << mk_pp(c, m) << " " << mk_pp(e, m) << "\n";); m_stats.m_assert_cnstr++; SASSERT(m_util.is_constructor(c)); - SASSERT(m_util.is_datatype(get_manager().get_sort(n->get_owner()))); - ast_manager & m = get_manager(); + SASSERT(m_util.is_datatype(get_manager().get_sort(e))); + + SASSERT(c->get_range() == m.get_sort(e)); ptr_vector args; - ptr_vector const & accessors = *m_util.get_constructor_accessors(c); + ptr_vector const & accessors = *m_util.get_constructor_accessors(c); SASSERT(c->get_arity() == accessors.size()); for (func_decl * d : accessors) { SASSERT(d->get_arity() == 1); - expr * acc = m.mk_app(d, n->get_owner()); - args.push_back(acc); + args.push_back(m.mk_app(d, e)); } - expr_ref mk(m.mk_app(c, args.size(), args.c_ptr()), m); - if (m.has_trace_stream()) { + expr_ref mk(m.mk_app(c, args), m); + + std::function fn = [&]() { app_ref body(m); - body = m.mk_eq(n->get_owner(), mk); + body = m.mk_eq(e, mk); if (antecedent != null_literal) { body = m.mk_implies(get_context().bool_var2expr(antecedent.var()), body); } log_axiom_instantiation(body, 1, &n); - } + }; + scoped_trace_stream _st(m, fn); assert_eq_axiom(n, mk, antecedent); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } /** @@ -228,6 +232,7 @@ namespace smt { func_decl * rec = m_util.get_constructor_is(con); ptr_vector const & accessors = *m_util.get_constructor_accessors(con); app_ref rec_app(m.mk_app(rec, arg1), m); + app_ref acc_app(m); ctx.internalize(rec_app, false); literal is_con(ctx.get_bool_var(rec_app)); for (func_decl* acc1 : accessors) { @@ -236,7 +241,7 @@ namespace smt { arg = n->get_arg(1); } else { - app* acc_app = m.mk_app(acc1, arg1); + acc_app = m.mk_app(acc1, arg1); ctx.internalize(acc_app, false); arg = ctx.get_enode(acc_app); } @@ -907,7 +912,7 @@ namespace smt { if (!r) { ptr_vector const & constructors = *m_util.get_datatype_constructors(dt); func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]); - app * rec_app = get_manager().mk_app(rec, n->get_owner()); + app_ref rec_app(get_manager().mk_app(rec, n->get_owner()), get_manager()); ctx.internalize(rec_app, false); consequent = literal(ctx.get_bool_var(rec_app)); } @@ -989,7 +994,7 @@ namespace smt { } } SASSERT(r != nullptr); - app * r_app = m.mk_app(r, n->get_owner()); + app_ref r_app(m.mk_app(r, n->get_owner()), m); TRACE("datatype", tout << "creating split: " << mk_pp(r_app, m) << "\n";); ctx.internalize(r_app, false); bool_var bv = ctx.get_bool_var(r_app); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 349ad104d..2199c46c0 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -813,8 +813,8 @@ theory_var theory_diff_logic::mk_var(enode* n) { } template -theory_var theory_diff_logic::set_sort(exir* n) { - if (m_util.is_int(n->get_owner())) { +void theory_diff_logic::set_sort(expr* n) { + if (m_util.is_int(n)) { if (m_lia_or_lra == is_lra) { throw default_exception("difference logic does not work with mixed sorts"); }