mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove tracing, fix doctext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1ae0769af5
commit
cbe52e298b
|
@ -27,6 +27,7 @@ Revision History:
|
|||
#include "ast/reg_decl_plugins.h"
|
||||
#include "math/realclosure/realclosure.h"
|
||||
|
||||
|
||||
// The install_tactics procedure is automatically generated
|
||||
void install_tactics(tactic_manager & ctx);
|
||||
|
||||
|
@ -383,7 +384,6 @@ extern "C" {
|
|||
if (a) {
|
||||
mk_c(c)->m().dec_ref(to_ast(a));
|
||||
}
|
||||
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
|
|
@ -1630,7 +1630,7 @@ def Xor(a, b, ctx=None):
|
|||
>>> Xor(p, q)
|
||||
Xor(p, q)
|
||||
>>> simplify(Xor(p, q))
|
||||
q == Not(p)
|
||||
q == Not(p)
|
||||
"""
|
||||
ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
|
||||
s = BoolSort(ctx)
|
||||
|
|
|
@ -169,28 +169,6 @@ bool family_manager::has_family(symbol const & s) const {
|
|||
return m_families.contains(s);
|
||||
}
|
||||
|
||||
#if 0
|
||||
static unsigned s_count = 0;
|
||||
void ast::inc_ref() {
|
||||
SASSERT(m_ref_count < UINT_MAX);
|
||||
m_ref_count ++;
|
||||
if (get_id() == 1) {
|
||||
s_count++;
|
||||
if (s_count >= 36530) {
|
||||
TRACE("rc", tout << "inc_ref " << m_ref_count << "\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void ast::dec_ref() {
|
||||
SASSERT(m_ref_count > 0);
|
||||
m_ref_count --;
|
||||
if (get_id() == 1 && s_count >= 36530) {
|
||||
TRACE("rc", tout << "dec_ref " << m_ref_count << "\n";);
|
||||
// IF_VERBOSE(0, verbose_stream() << "dec_rc " << s_count << "\n";);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
|
@ -482,7 +482,6 @@ protected:
|
|||
void * m_mark2_owner;
|
||||
#endif
|
||||
|
||||
#if 1
|
||||
void inc_ref() {
|
||||
SASSERT(m_ref_count < UINT_MAX);
|
||||
m_ref_count ++;
|
||||
|
@ -492,12 +491,6 @@ protected:
|
|||
SASSERT(m_ref_count > 0);
|
||||
m_ref_count --;
|
||||
}
|
||||
#else
|
||||
void inc_ref();
|
||||
|
||||
void dec_ref();
|
||||
|
||||
#endif
|
||||
|
||||
ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
|
||||
DEBUG_CODE({
|
||||
|
|
|
@ -121,9 +121,9 @@ void expr_substitution::erase(expr * c) {
|
|||
}
|
||||
expr * def = nullptr;
|
||||
if (m_subst.find(c, def)) {
|
||||
m_manager.dec_ref(c);
|
||||
m_manager.dec_ref(def);
|
||||
m_subst.erase(c);
|
||||
m_manager.dec_ref(c);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -43,6 +43,8 @@ public:
|
|||
~justified_expr() {
|
||||
m.dec_ref(m_fml);
|
||||
m.dec_ref(m_proof);
|
||||
m_fml = nullptr;
|
||||
m_proof = nullptr;
|
||||
}
|
||||
|
||||
expr* get_fml() const { return m_fml; }
|
||||
|
|
|
@ -107,9 +107,9 @@ struct goal2sat::imp {
|
|||
m_solver.add_clause(l1, l2, m_is_lemma);
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
|
||||
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, bool is_lemma = false) {
|
||||
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
|
||||
m_solver.add_clause(l1, l2, l3, m_is_lemma);
|
||||
m_solver.add_clause(l1, l2, l3, m_is_lemma || is_lemma);
|
||||
}
|
||||
|
||||
void mk_clause(unsigned num, sat::literal * lits) {
|
||||
|
@ -337,8 +337,8 @@ struct goal2sat::imp {
|
|||
mk_clause(l, ~c, ~t);
|
||||
mk_clause(l, c, ~e);
|
||||
if (m_ite_extra) {
|
||||
mk_clause(~t, ~e, l);
|
||||
mk_clause(t, e, ~l);
|
||||
mk_clause(~t, ~e, l, true);
|
||||
mk_clause(t, e, ~l, true);
|
||||
}
|
||||
m_result_stack.shrink(sz-3);
|
||||
if (sign)
|
||||
|
|
|
@ -216,6 +216,11 @@ void asserted_formulas::reset() {
|
|||
m_inconsistent = false;
|
||||
}
|
||||
|
||||
void asserted_formulas::finalize() {
|
||||
reset();
|
||||
m_substitution.cleanup();
|
||||
}
|
||||
|
||||
bool asserted_formulas::check_well_sorted() const {
|
||||
for (justified_expr const& je : m_formulas) {
|
||||
if (!is_well_sorted(m, je.get_fml())) return false;
|
||||
|
|
|
@ -223,6 +223,7 @@ class asserted_formulas {
|
|||
public:
|
||||
asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
|
||||
~asserted_formulas();
|
||||
void finalize();
|
||||
|
||||
void updt_params(params_ref const& p);
|
||||
bool has_quantifiers() const { return m_has_quantifiers; }
|
||||
|
|
|
@ -232,6 +232,7 @@ namespace smt {
|
|||
|
||||
context::~context() {
|
||||
flush();
|
||||
m_asserted_formulas.finalize();
|
||||
}
|
||||
|
||||
void context::copy_plugins(context& src, context& dst) {
|
||||
|
|
Loading…
Reference in a new issue