mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix #3555

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 14:37:38 -07:00
parent b9dd18483c
commit fe81de6d39
3 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.cpp
View file

@ -813,13 +813,13 @@ func_decl * basic_decl_plugin::mk_proof_decl(
return m_manager->mk_func_decl(symbol(name), num_parents+1, domain.c_ptr(), m_proof_sort, info);
}
func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents) {
func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, bool inc_ref) {
ptr_buffer<sort> domain;
for (unsigned i = 0; i < num_parents; i++)
domain.push_back(m_proof_sort);
domain.push_back(m_bool_sort);
func_decl * d = m_manager->mk_func_decl(symbol(name), num_parents+1, domain.c_ptr(), m_proof_sort, func_decl_info(m_family_id, k));
m_manager->inc_ref(d);
if (inc_ref) m_manager->inc_ref(d);
return d;
}
@ -837,7 +837,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k,
cache.resize(num_parents+1, nullptr);
}
if (!cache[num_parents]) {
cache[num_parents] = mk_proof_decl(name, k, num_parents);
cache[num_parents] = mk_proof_decl(name, k, num_parents, true);
}
return cache[num_parents];
}
@ -865,7 +865,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_param
func_decl * basic_decl_plugin::mk_proof_decl(char const* name, basic_op_kind k, unsigned num_parents, func_decl*& fn) {
if (!fn) {
fn = mk_proof_decl(name, k, num_parents);
fn = mk_proof_decl(name, k, num_parents, true);
}
return fn;
}
@ -919,7 +919,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_TH_ASSUMPTION_ADD: return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl);
case PR_TH_LEMMA_ADD: return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl);
case PR_REDUNDANT_DEL: return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl);
case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents);
case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents, false);
default:
UNREACHABLE();
return nullptr;
@ -1794,13 +1794,13 @@ bool ast_manager::slow_not_contains(ast const * n) {
}
#endif
#if 0
#if 1
static unsigned s_count = 0;
static void track_id(ast* n, unsigned id) {
if (n->get_id() != id) return;
++s_count;
std::cout << s_count << "\n";
//SASSERT(s_count != 23);
SASSERT(s_count != 1);
}
#endif
@ -1834,6 +1834,8 @@ 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, 2147483792);
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
// increment reference counters

2
src/ast/ast.h
View file

@ -1180,7 +1180,7 @@ protected:
func_decl * mk_bool_op_decl(char const * name, basic_op_kind k, unsigned num_args = 0,
bool asooc = false, bool comm = false, bool idempotent = false, bool flat_associative = false, bool chainable = false);
func_decl * mk_implies_decl();
func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents);
func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, bool inc_ref);
func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, func_decl*& fn);
func_decl * mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache);
func_decl * mk_compressed_proof_decl(char const * name, basic_op_kind k, unsigned num_parents);

3
src/smt/smt_clause_proof.cpp
View file

@ -141,7 +141,8 @@ namespace smt {
break;
}
}
return proof_ref(m.mk_clause_trail(ps.size(), ps.c_ptr()), m);
proof_ref result(m.mk_clause_trail(ps.size(), ps.c_ptr()), m);
return result;
}
std::ostream& operator<<(std::ostream& out, clause_proof::status st) {