mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Lev Nachmanson 2020-04-01 12:31:49 -07:00
commit 5e2927aa96
15 changed files with 60 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/ast.cpp
View file

@ -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, 70);
//track_id(n, 1354);
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
@ -1920,19 +1920,6 @@ ast * ast_manager::register_node_core(ast * n) {
break;
}
#if 0
// std::cout << n->m_id << " " << n->hash() << "\n";
if (n->m_id == 1523) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
}
if (n->m_id == 1524) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
VERIFY(false);
}
if (n->m_id == 1525) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
}
#endif
return n;
}

2
src/ast/expr_substitution.cpp
View file

@ -66,6 +66,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr);
SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(0) == c);
SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(1) == def);
if (entry->get_data().m_value == nullptr) {
// new entry
m_manager.inc_ref(c);

10
src/ast/rewriter/rewriter.cpp
View file

@ -42,6 +42,16 @@ void rewriter_core::del_cache_stack() {
}
}
bool rewriter_core::rewrites_from(expr* t, proof* p) {
return !p || (to_app(m().get_fact(p))->get_arg(0) == t);
}
bool rewriter_core::rewrites_to(expr* t, proof* p) {
return !p || (to_app(m().get_fact(p))->get_arg(1) == t);
}
void rewriter_core::cache_shifted_result(expr * k, unsigned offset, expr * v) {
#if 0
// trace for tracking cache usage

2
src/ast/rewriter/rewriter.h
View file

@ -87,6 +87,8 @@ protected:
push_frame_core(t, must_cache(t), st);
}
bool rewrites_to(expr* t, proof* p);
bool rewrites_from(expr* t, proof* p);
void init_cache_stack();
void del_cache_stack();
void reset_cache();

21
src/ast/rewriter/rewriter_def.h
View file

@ -100,6 +100,8 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
case BR_DONE:
result_stack().push_back(m_r.get());
if (ProofGen) {
SASSERT(rewrites_from(t0, m_pr));
SASSERT(rewrites_to(m_r, m_pr));
if (m_pr)
result_pr_stack().push_back(m_pr);
else
@ -139,6 +141,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
SASSERT(m().get_sort(t) == m().get_sort(new_t));
result_stack().push_back(new_t);
set_new_child_flag(t, new_t);
SASSERT(rewrites_from(t, new_t_pr));
SASSERT(rewrites_to(new_t, new_t_pr));
if (ProofGen)
result_pr_stack().push_back(new_t_pr);
return true;
@ -167,6 +171,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
if (ProofGen) {
proof * pr = get_cached_pr(t);
result_pr_stack().push_back(pr);
SASSERT(rewrites_from(t, pr));
SASSERT(rewrites_to(r, pr));
}
return true;
}
@ -286,14 +292,20 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
else {
new_t = m().mk_app(f, new_num_args, new_args);
m_pr = m().mk_congruence(t, new_t, num_prs, result_pr_stack().c_ptr() + fr.m_spos);
SASSERT(rewrites_from(t, m_pr));
SASSERT(rewrites_to(new_t, m_pr));
}
}
br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
CTRACE("reduce_app", st != BR_FAILED,
tout << mk_bounded_pp(t, m()) << "\n";
tout << "st: " << st;
if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
tout << "\n";);
tout << mk_bounded_pp(t, m()) << "\n";
tout << "st: " << st;
if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
tout << "\n";
if (m_pr2) tout << mk_bounded_pp(m_pr2, m()) << "\n";
);
SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2));
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
if (st != BR_FAILED) {
result_stack().shrink(fr.m_spos);
@ -491,6 +503,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
}
}
template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {

6
src/ast/rewriter/th_rewriter.cpp
View file

@ -571,7 +571,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
}
void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
family_id fid = f->get_family_id();
if (fid == m_b_rw.get_fid()) {
decl_kind k = f->get_decl_kind();
@ -587,8 +587,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
app_ref tmp(m());
tmp = m().mk_app(f, num, args);
m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
if (m().proofs_enabled())
result_pr = m().mk_rewrite(tmp, result);
tmp = m().mk_eq(tmp, result);
m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
@ -618,7 +616,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
br_status st = reduce_app_core(f, num, args, result);
if (st != BR_FAILED && m().has_trace_stream()) {
log_rewrite_axiom_instantiation(f, num, args, result, result_pr);
log_rewrite_axiom_instantiation(f, num, args, result);
}
if (st != BR_DONE && st != BR_FAILED) {

2
src/math/lp/lar_solver.h
View file

@ -578,7 +578,7 @@ public:
}
void subs_term_columns(lar_term& t) {
vector<std::pair<unsigned,unsigned>> columns_to_subs;
svector<std::pair<unsigned,unsigned>> columns_to_subs;
for (const auto & m : t) {
unsigned tj = adjust_column_index_to_term_index(m.var().index());
if (tj == m.var().index()) continue;

14
src/model/model_evaluator.cpp
View file

@ -158,26 +158,28 @@ struct evaluator_cfg : public default_rewriter_cfg {
br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr;
family_id fid = f->get_family_id();
bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
br_status st = BR_FAILED;
if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)) {
if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
expr * val = m_model.get_const_interp(f);
func_decl* g = nullptr;
if (val != nullptr) {
result = val;
st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
TRACE("model_evaluator", tout << result << "\n";);
return st;
}
else if (m_model_completion && !m_ar.is_as_array(f)) {
if (!m_model_completion)
return BR_FAILED;
if (!m_ar.is_as_array(f, g) || g->get_family_id() == null_family_id) {
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
m_model.register_decl(f, val);
result = val;
return BR_DONE;
}
else {
return BR_FAILED;
}
return BR_FAILED;
}

2
src/opt/opt_context.cpp
View file

@ -374,7 +374,7 @@ namespace opt {
void context::set_model(model_ref& m) {
m_model = m;
opt_params optp(m_params);
if (optp.dump_models()) {
if (optp.dump_models() && m) {
model_ref md = m->copy();
fix_model(md);
}

1
src/sat/sat_solver.cpp
View file

@ -1729,6 +1729,7 @@ namespace sat {
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
set_external(lit.var());
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign_scoped(lit);

6
src/smt/tactic/smt_tactic.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "util/debug.h"
#include "ast/rewriter/rewriter_types.h"
#include "ast/ast_util.h"
#include "ast/ast_ll_pp.h"
#include "smt/smt_kernel.h"
#include "smt/params/smt_params.h"
#include "smt/params/smt_params_helper.hpp"
@ -249,8 +250,11 @@ public:
lcore = m.mk_join(lcore, m.mk_leaf(d));
}
}
if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
if (m.proofs_enabled() && !pr) pr = m.mk_asserted(m.mk_false()); // bail out
if (pr && m.get_fact(pr) != m.mk_false()) pr = m.mk_asserted(m.mk_false()); // could happen in clause_proof mode
in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get());
return;
}

9
src/smt/tactic/unit_subsumption_tactic.cpp
View file

@ -40,7 +40,9 @@ struct unit_subsumption_tactic : public tactic {
void cleanup() override {}
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result) override {
/* out */ goal_ref_buffer & result) override {
tactic_report report("unit-subsume-simplify", *in);
fail_if_proof_generation("unit-subsume-simplify", in);
reduce_core(in, result);
}
@ -75,7 +77,8 @@ struct unit_subsumption_tactic : public tactic {
void assert_clauses(goal_ref const& g) {
for (unsigned i = 0; i < g->size(); ++i) {
m_context.assert_expr(m.mk_iff(new_clause(), g->form(i)));
expr_ref fml(m.mk_iff(new_clause(), g->form(i)), m);
m_context.assert_expr(fml);
}
}
@ -106,7 +109,7 @@ struct unit_subsumption_tactic : public tactic {
}
void insert_result(goal_ref& result) {
for (auto d : m_deleted) result->update(d, m.mk_true()); // TBD proof?
for (auto d : m_deleted) result->update(d, m.mk_true());
}
void init(goal_ref const& g) {

2
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -184,7 +184,7 @@ public:
m_bounds(*g);
if (m_bounds.inconsistent()) {
if (m_bounds.inconsistent() || g->proofs_enabled()) {
g->inc_depth();
result.push_back(g.get());
return;

4
src/tactic/core/propagate_values_tactic.cpp
View file

@ -60,13 +60,13 @@ class propagate_values_tactic : public tactic {
if (m.is_value(arg1) && is_shared(arg2)) {
lhs = arg2;
value = arg1;
inverted = false;
inverted = true;
return true;
}
if (m.is_value(arg2) && is_shared(arg1)) {
lhs = arg1;
value = arg2;
inverted = true;
inverted = false;
return true;
}
return false;

2
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -75,7 +75,7 @@ class quasi_macros_tactic : public tactic {
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(forms.get(i),
produce_proofs ? proofs.get(i) : nullptr,
produce_unsat_cores ? deps.get(i) : nullptr);
produce_unsat_cores ? deps.get(i, nullptr) : nullptr);
generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager(), "quasi_macros");
unsigned num = mm.get_num_macros();