mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

small updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-30 19:31:39 -07:00
parent 397bf2dec6
commit 5b6255e3d1
2 changed files with 24 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/smt/smt_induction.cpp
View file

@ -160,6 +160,13 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) {
return result; return result;
} }
void create_induction_lemmas::abstract1(enode* n, enode* t, expr* x, abstractions& result) {
expr_safe_replace rep(m);
rep.insert(t->get_owner(), x);
expr_ref e(n->get_owner(), m);
rep(e);
result.push_back(abstraction(e));
}
/** /**
* abstraction candidates for replacing different occurrence of t in n by x * abstraction candidates for replacing different occurrence of t in n by x
@ -172,14 +179,14 @@ void create_induction_lemmas::abstract(enode* n, enode* t, expr* x, abstractions
std::cout << "abs: " << result.size() << ": " << mk_pp(n->get_owner(), m) << "\n"; std::cout << "abs: " << result.size() << ": " << mk_pp(n->get_owner(), m) << "\n";
if (n->get_root() == t->get_root()) { if (n->get_root() == t->get_root()) {
result.push_back(abstraction(m, x, n->get_owner(), t->get_owner())); result.push_back(abstraction(m, x, n->get_owner(), t->get_owner()));
}
#if 0
// check if n is a s
if (is_skolem(n->get_owner())) {
result.push_back(abstraction(m, n->get_owner()));
return; return;
} }
#endif func_decl* f = n->get_owner()->get_decl();
// check if n is a s
if (f->is_skolem()) {
expr_ref e(n->get_owner(), m);
result.push_back(abstraction(e));
}
abstraction_args r1, r2; abstraction_args r1, r2;
r1.push_back(abstraction_arg(m)); r1.push_back(abstraction_arg(m));
@ -330,19 +337,6 @@ literal create_induction_lemmas::mk_literal(expr* e) {
return ctx.get_literal(e); return ctx.get_literal(e);
} }
func_decl* create_induction_lemmas::mk_skolem(sort* s) {
func_decl* f = nullptr;
if (!m_sort2skolem.find(s, f)) {
sort* domain[3] = { m_a.mk_int(), s, m.mk_bool_sort() };
f = m.mk_fresh_func_decl("sk", 3, domain, s);
m_pinned.push_back(f);
m_pinned.push_back(s);
m_sort2skolem.insert(s, f);
}
return f;
}
bool create_induction_lemmas::operator()(literal lit) { bool create_induction_lemmas::operator()(literal lit) {
unsigned num = m_num_lemmas; unsigned num = m_num_lemmas;
enode* r = ctx.bool_var2enode(lit.var()); enode* r = ctx.bool_var2enode(lit.var());
@ -350,12 +344,12 @@ bool create_induction_lemmas::operator()(literal lit) {
for (enode* n : induction_positions(r)) { for (enode* n : induction_positions(r)) {
expr* t = n->get_owner(); expr* t = n->get_owner();
sort* s = m.get_sort(t); sort* s = m.get_sort(t);
expr_ref sk(m.mk_app(mk_skolem(s), m_a.mk_int(position), t, r->get_owner()), m); expr_ref sk(m.mk_fresh_const("sk", s), m);
std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n"; std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n";
abstractions abs; abstractions abs;
abstract(r, n, sk, abs); abstract1(r, n, sk, abs);
abs.pop_back(); // last position has no generalizations // if (ab.size() > 1) abs.pop_back(); // last position has no generalizations
filter_abstractions(lit.sign(), abs); if (abs.size() > 1) filter_abstractions(lit.sign(), abs);
for (abstraction& a : abs) { for (abstraction& a : abs) {
create_lemmas(t, sk, a, lit); create_lemmas(t, sk, a, lit);
} }
@ -371,7 +365,6 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v
vs(vs), vs(vs),
m_dt(m), m_dt(m),
m_a(m), m_a(m),
m_pinned(m),
m_num_lemmas(0) m_num_lemmas(0)
{} {}

18
src/smt/smt_induction.h
View file

@ -49,21 +49,17 @@ namespace smt {
* Synthesize induction lemmas from induction candidates * Synthesize induction lemmas from induction candidates
*/ */
class create_induction_lemmas { class create_induction_lemmas {
context& ctx; context& ctx;
ast_manager& m; ast_manager& m;
value_sweep& vs; value_sweep& vs;
datatype::util m_dt; datatype::util m_dt;
arith_util m_a; arith_util m_a;
obj_map<sort, func_decl*> m_sort2skolem; unsigned m_num_lemmas;
ast_ref_vector m_pinned;
unsigned m_num_lemmas;
typedef svector<std::pair<expr*,expr*>> expr_pair_vector; typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
func_decl* mk_skolem(sort* s);
struct abstraction { struct abstraction {
expr_ref m_term; expr_ref m_term;
expr_pair_vector m_eqs; expr_pair_vector m_eqs;
abstraction(expr_ref& e): m_term(e) {} abstraction(expr_ref& e): m_term(e) {}
abstraction(ast_manager& m, expr* e, expr* n1, expr* n2): m_term(e, m) { abstraction(ast_manager& m, expr* e, expr* n1, expr* n2): m_term(e, m) {
@ -71,8 +67,7 @@ namespace smt {
} }
abstraction(ast_manager& m, expr* e, expr_pair_vector const& eqs): abstraction(ast_manager& m, expr* e, expr_pair_vector const& eqs):
m_term(e, m), m_eqs(eqs) { m_term(e, m), m_eqs(eqs) {
} }
}; };
typedef vector<abstraction> abstractions; typedef vector<abstraction> abstractions;
@ -90,6 +85,7 @@ namespace smt {
bool is_induction_candidate(enode* n); bool is_induction_candidate(enode* n);
enode_vector induction_positions(enode* n); enode_vector induction_positions(enode* n);
void abstract(enode* n, enode* t, expr* x, abstractions& result); void abstract(enode* n, enode* t, expr* x, abstractions& result);
void abstract1(enode* n, enode* t, expr* x, abstractions& result);
void filter_abstractions(bool sign, abstractions& abs); void filter_abstractions(bool sign, abstractions& abs);
void create_lemmas(expr* t, expr* sk, abstraction& a, literal lit); void create_lemmas(expr* t, expr* sk, abstraction& a, literal lit);
literal mk_literal(expr* e); literal mk_literal(expr* e);