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

avoid repeated internalization of lambda #4169

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-30 13:24:26 -07:00
parent 7ae20476c2
commit 799b6131f2
8 changed files with 88 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params.cpp
View file

@ -26,6 +26,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_random_seed = p.random_seed();
m_relevancy_lvl = p.relevancy();
m_ematching = p.ematching();
m_induction = p.induction();
m_clause_proof = p.clause_proof();
m_phase_selection = static_cast<phase_selection>(p.phase_selection());
if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral");
@ -111,6 +112,7 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_display_features);
DISPLAY_PARAM(m_new_core2th_eq);
DISPLAY_PARAM(m_ematching);
DISPLAY_PARAM(m_induction);
DISPLAY_PARAM(m_clause_proof);
DISPLAY_PARAM(m_case_split_strategy);

2
src/smt/params/smt_params.h
View file

@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params,
bool m_display_features;
bool m_new_core2th_eq;
bool m_ematching;
bool m_induction;
bool m_clause_proof;
// -----------------------------------
@ -262,6 +263,7 @@ struct smt_params : public preprocessor_params,
m_display_features(false),
m_new_core2th_eq(true),
m_ematching(true),
m_induction(false),
m_clause_proof(false),
m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
m_rel_case_split_order(0),

1
src/smt/params/smt_params_helper.pyg
View file

@ -37,6 +37,7 @@ def_module_params(module_name='smt',
('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
('induction', BOOL, False, 'enable generation of induction lemmas'),
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),

90
src/smt/smt_induction.cpp
View file

@ -55,6 +55,8 @@ literal_vector collect_induction_literals::pre_select() {
continue;
result.push_back(lit);
}
TRACE("induction", ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n"););
ctx.push_trail(value_trail<context, unsigned>(m_literal_index));
m_literal_index = ctx.assigned_literals().size();
return result;
@ -68,11 +70,6 @@ void collect_induction_literals::model_sweep_filter(literal_vector& candidates)
vector<expr_ref_vector> values;
vs(terms, values);
unsigned j = 0;
IF_VERBOSE(1,
verbose_stream() << "terms: " << terms << "\n";
for (auto const& vec : values) {
verbose_stream() << "assignment: " << vec << "\n";
});
for (unsigned i = 0; i < terms.size(); ++i) {
literal lit = candidates[i];
bool is_viable_candidate = true;
@ -109,14 +106,26 @@ literal_vector collect_induction_literals::operator()() {
// create_induction_lemmas
bool create_induction_lemmas::is_induction_candidate(enode* n) {
expr* e = n->get_owner();
app* e = n->get_owner();
if (m.is_value(e))
return false;
// TBD: filter if n is equivalent to a value.
bool in_good_context = false;
for (enode* p : n->get_parents()) {
app* o = p->get_owner();
if (o->get_family_id() != m.get_basic_family_id())
in_good_context = true;
}
if (!in_good_context)
return false;
// avoid recursively unfolding skolem terms.
if (e->get_num_args() > 0 && e->get_family_id() == null_family_id) {
return false;
}
sort* s = m.get_sort(e);
if (m_dt.is_datatype(s) && m_dt.is_recursive(s))
return true;
// potentially also induction on integers, sequences
// m_arith.is_int(s)
// return true;
@ -160,14 +169,24 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) {
* TDD: add depth throttle.
*/
void create_induction_lemmas::abstract(enode* n, enode* t, expr* x, abstractions& result) {
std::cout << "abs: " << result.size() << ": " << mk_pp(n->get_owner(), m) << "\n";
if (n->get_root() == t->get_root()) {
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;
}
#endif
abstraction_args r1, r2;
r1.push_back(abstraction_arg(m));
for (enode* arg : enode::args(n)) {
unsigned n = result.size();
abstract(arg, t, x, result);
std::cout << result.size() << "\n";
for (unsigned i = n; i < result.size(); ++i) {
abstraction& a = result[i];
for (auto const& v : r1) {
@ -193,7 +212,9 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs)
vector<expr_ref_vector> values;
expr_ref_vector fmls(m);
for (auto & a : abs) fmls.push_back(a.m_term);
std::cout << "sweep\n";
vs(fmls, values);
std::cout << "done sweep\n";
unsigned j = 0;
for (unsigned i = 0; i < fmls.size(); ++i) {
bool all_cex = true;
@ -207,15 +228,17 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs)
abs[j++] = abs.get(i);
}
}
std::cout << "resulting size: " << j << " down from " << abs.size() << "\n";
abs.shrink(j);
}
/*
* Create simple induction lemmas of the form:
*
* lit & a.eqs() & is-c(t) => is-c(sk);
* lit & a.eqs() => alpha
* lit & a.eqs() & is-c(t) => ~beta
* alpha & is-c(sk) => ~beta
*
* alpha & is-c(t) => is-c(sk);
*
* where
* lit = is a formula containing t
@ -242,6 +265,7 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l
return;
expr_ref alpha = a.m_term;
auto const& eqs = a.m_eqs;
literal alpha_lit = null_literal;
literal_vector common_literals;
for (func_decl* c : *m_dt.get_datatype_constructors(s)) {
func_decl* is_c = m_dt.get_constructor_recognizer(c);
@ -249,43 +273,51 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l
for (func_decl* acc : *m_dt.get_constructor_accessors(c)) {
if (acc->get_range() != s)
continue;
if (common_literals.empty()) {
common_literals.push_back(~lit);
for (auto const& p : eqs) {
common_literals.push_back(~mk_literal(m.mk_eq(p.first, p.second)));
}
if (alpha_lit == null_literal) {
alpha_lit = mk_literal(alpha);
if (lit.sign()) alpha_lit.neg();
}
has_1recursive = true;
literal_vector lits(common_literals);
lits.push_back(~mk_literal(m.mk_app(is_c, t)));
expr_ref beta(alpha);
expr_safe_replace rep(m);
rep.insert(sk, m.mk_app(acc, sk));
rep(beta);
literal b_lit = mk_literal(beta);
if (lit.sign()) b_lit.neg();
// alpha & is_c(sk) => ~beta
literal_vector lits;
lits.push_back(~alpha_lit);
lits.push_back(~mk_literal(m.mk_app(is_c, sk)));
lits.push_back(~b_lit);
add_th_lemma(lits);
}
// alpha & is_c(t) => is_c(sk)
if (has_1recursive) {
literal_vector lits(common_literals);
literal_vector lits;
lits.push_back(~alpha_lit);
lits.push_back(~mk_literal(m.mk_app(is_c, t)));
lits.push_back(mk_literal(m.mk_app(is_c, sk)));
add_th_lemma(lits);
}
}
if (!common_literals.empty()) {
literal_vector lits(common_literals);
literal a_lit = mk_literal(alpha);
if (lit.sign()) a_lit.neg();
lits.push_back(a_lit);
// phi & eqs => alpha
if (alpha_lit != null_literal) {
literal_vector lits;
lits.push_back(~lit);
for (auto const& p : eqs) {
lits.push_back(~mk_literal(m.mk_eq(p.first, p.second)));
}
lits.push_back(alpha_lit);
add_th_lemma(lits);
}
}
void create_induction_lemmas::add_th_lemma(literal_vector const& lits) {
IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n");
ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_LEMMA);
ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_AXIOM); // CLS_TH_LEMMA, but then should re-instance if GC'ed
++m_num_lemmas;
}
@ -301,8 +333,8 @@ literal create_induction_lemmas::mk_literal(expr* e) {
func_decl* create_induction_lemmas::mk_skolem(sort* s) {
func_decl* f = nullptr;
if (!m_sort2skolem.find(s, f)) {
sort* domain[2] = { s, m.mk_bool_sort() };
f = m.mk_fresh_func_decl("sk", 2, domain, s);
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);
@ -314,10 +346,11 @@ func_decl* create_induction_lemmas::mk_skolem(sort* s) {
bool create_induction_lemmas::operator()(literal lit) {
unsigned num = m_num_lemmas;
enode* r = ctx.bool_var2enode(lit.var());
unsigned position = 0;
for (enode* n : induction_positions(r)) {
expr* t = n->get_owner();
sort* s = m.get_sort(t);
expr_ref sk(m.mk_app(mk_skolem(s), t, r->get_owner()), m);
expr_ref sk(m.mk_app(mk_skolem(s), m_a.mk_int(position), t, r->get_owner()), m);
std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n";
abstractions abs;
abstract(r, n, sk, abs);
@ -326,6 +359,8 @@ bool create_induction_lemmas::operator()(literal lit) {
for (abstraction& a : abs) {
create_lemmas(t, sk, a, lit);
}
std::cout << "lemmas created\n";
++position;
}
return m_num_lemmas > num;
}
@ -335,6 +370,7 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v
m(m),
vs(vs),
m_dt(m),
m_a(m),
m_pinned(m),
m_num_lemmas(0)
{}

2
src/smt/smt_induction.h
View file

@ -20,6 +20,7 @@
#include "smt/smt_types.h"
#include "ast/rewriter/value_sweep.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
namespace smt {
@ -52,6 +53,7 @@ namespace smt {
ast_manager& m;
value_sweep& vs;
datatype::util m_dt;
arith_util m_a;
obj_map<sort, func_decl*> m_sort2skolem;
ast_ref_vector m_pinned;
unsigned m_num_lemmas;

3
src/smt/smt_internalizer.cpp
View file

@ -558,6 +558,9 @@ namespace smt {
void context::internalize_lambda(quantifier * q) {
TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";);
SASSERT(is_lambda(q));
if (e_internalized(q)) {
return;
}
app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m);
app_ref eq(m), lam_app(m);
expr_ref_vector vars(m);

18
src/smt/theory_recfun.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
#include "smt/theory_recfun.h"
#include "smt/params/smt_params_helper.hpp"
#define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
@ -357,6 +356,7 @@ namespace smt {
literal_vector preds;
auto & vars = e.m_def->get_vars();
unsigned max_depth = 0;
for (recfun::case_def const & c : e.m_def->get_cases()) {
// applied predicate to `args`
app_ref pred_applied = c.apply_case_predicate(e.m_args);
@ -376,15 +376,25 @@ namespace smt {
}
else if (!is_enabled_guard(pred_applied)) {
disable_guard(pred_applied, guards);
max_depth = std::max(depth, max_depth);
continue;
}
activate_guard(pred_applied, guards);
}
// the disjunction of branches is asserted
// to close the available cases.
std::function<literal_vector(void)> fn2 = [&]() { return preds; };
scoped_trace_stream _tr2(*this, fn2);
ctx().mk_th_axiom(get_id(), preds);
{
scoped_trace_stream _tr2(*this, preds);
ctx().mk_th_axiom(get_id(), preds);
}
(void)max_depth;
// add_induction_lemmas(max_depth);
}
void theory_recfun::add_induction_lemmas(unsigned depth) {
if (depth > 4 && ctx().get_fparams().m_induction && induction::should_try(ctx())) {
ctx().get_induction()();
}
}
void theory_recfun::activate_guard(expr* pred_applied, expr_ref_vector const& guards) {

1
src/smt/theory_recfun.h
View file

@ -127,6 +127,7 @@ namespace smt {
void assert_body_axiom(body_expansion & e);
literal mk_literal(expr* e);
void add_induction_lemmas(unsigned depth);
void disable_guard(expr* guard, expr_ref_vector const& guards);
unsigned get_depth(expr* e);
void set_depth(unsigned d, expr* e);