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

cleaned up lemma instantiation code

Browse source
This commit is contained in:
Arie Gurfinkel 2017-08-07 11:51:21 +02:00
parent 6917aa3eb9
commit e8befc072c
2 changed files with 46 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/muz/spacer/spacer_context.cpp
View file

@ -1248,27 +1248,59 @@ void lemma::update_cube (pob_ref const &p, expr_ref_vector &cube) {
if (m_cube.empty()) {m_cube.push_back(m.mk_true());} if (m_cube.empty()) {m_cube.push_back(m.mk_true());}
} }
void lemma::mk_insts(expr_ref_vector &out, expr* e) bool lemma::has_binding(app_ref_vector const &binding) {
{ expr *lem = get_expr();
unsigned num_decls = to_quantifier(lem)->get_num_decls();
SASSERT(bindings.size() == num_decls);
for (unsigned off = 0, sz = m_bindings.size(); off < sz; off += num_decls) {
unsigned i = 0;
for (; i < num_decls; ++i) {
if (m_bindings.get(off + i) != binding.get(i)) {
break;
}
}
if (i == num_decls) return true;
}
return false;
}
void lemma::add_binding(app_ref_vector const &binding) {
if (!has_binding(binding)) {
m_bindings.append(binding);
TRACE("spacer",
tout << "new binding: ";
for (unsigned i = 0; i < binding.size(); i++)
tout << mk_pp(binding.get(i), m) << " ";
tout << "\n";);
}
}
void lemma::instantiate(expr * const * exprs, expr_ref &result, expr *e) {
expr *lem = e == nullptr ? get_expr() : e; expr *lem = e == nullptr ? get_expr() : e;
if (!is_quantifier (lem) || m_bindings.empty()) {return;} if (!is_quantifier (lem) || m_bindings.empty()) {return;}
expr *body = to_quantifier(lem)->get_expr(); expr *body = to_quantifier(lem)->get_expr();
unsigned num_decls = to_quantifier(lem)->get_num_decls(); unsigned num_decls = to_quantifier(lem)->get_num_decls();
expr_ref inst(m);
var_subst vs(m, false); var_subst vs(m, false);
for (unsigned i = 0, vs(body, num_decls, exprs, result);
sz = m_bindings.size() / num_decls, }
off = 0;
i < sz; void lemma::mk_insts(expr_ref_vector &out, expr* e)
++i, off += num_decls) { {
inst.reset(); expr *lem = e == nullptr ? get_expr() : e;
vs.reset(); if (!is_quantifier (lem) || m_bindings.empty()) {return;}
vs(body, num_decls, (expr**) m_bindings.c_ptr() + off, inst);
unsigned num_decls = to_quantifier(lem)->get_num_decls();
expr_ref inst(m);
for (unsigned off = 0, sz = m_bindings.size(); off < sz; off += num_decls) {
instantiate((expr * const *) m_bindings.c_ptr() + off, inst, e);
out.push_back(inst); out.push_back(inst);
inst.reset();
} }
} }
bool pred_transformer::frames::add_lemma(lemma *lem) bool pred_transformer::frames::add_lemma(lemma *lem)
{ {
TRACE("spacer", tout << "add-lemma: " << pp_level(lem->level()) << " " TRACE("spacer", tout << "add-lemma: " << pp_level(lem->level()) << " "

4
src/muz/spacer/spacer_context.h
View file

@ -135,7 +135,9 @@ public:
unsigned level () const {return m_lvl;} unsigned level () const {return m_lvl;}
void set_level (unsigned lvl) {m_lvl = lvl;} void set_level (unsigned lvl) {m_lvl = lvl;}
app_ref_vector& get_bindings() {return m_bindings;} app_ref_vector& get_bindings() {return m_bindings;}
void add_binding(app_ref_vector const &binding) {m_bindings.append(binding);} bool has_binding(app_ref_vector const &binding);
void add_binding(app_ref_vector const &binding);
void instantiate(expr * const * exprs, expr_ref &result, expr *e = nullptr);
void mk_insts(expr_ref_vector& inst, expr* e = nullptr); void mk_insts(expr_ref_vector& inst, expr* e = nullptr);
bool is_ground () {return !is_quantifier (get_expr());} bool is_ground () {return !is_quantifier (get_expr());}