michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(library/unifier): minimize the number of constraints generated in the flex_rigid 'imitation' step

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-17 06:32:21 +01:00
parent 8798fa4419
commit a78fb8f013
1 changed files with 43 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/library/unifier.cpp
View file

@ -983,6 +983,39 @@ struct unifier_fn {
return new_mtype;
}
/**
\see mk_flex_rigid_app_cnstrs
When using "imitation" for solving a constraint
?m l_1 ... l_k =?= f a_1 ... a_n
We say argument a_i is "easy" if
1) it is a local constant
2) there is only one l_j equal to a_i.
3) none of the l_j's is of the form (?m ...)
In our experiments, the vast majority (> 2/3 of all cases) of the arguments are easy.
margs contains l_1 ... l_k
arg is the argument we are testing
Result: none if it is not an easy argument, and variable #k-i-1 if it is easy.
The variable is the "solution".
*/
optional<expr> is_easy_flex_rigid_arg(buffer<expr> const & margs, expr const & arg) {
if (!is_local(arg))
return none_expr();
optional<expr> v;
unsigned num_margs = margs.size();
for (unsigned j = 0; j < num_margs; j++) {
if (is_meta(margs[j]))
return none_expr();
if (is_local(margs[j]) && mlocal_name(arg) == mlocal_name(margs[j])) {
if (v)
return none_expr(); // failed, there is more than one possibility
v = mk_var(num_margs - j - 1);
}
}
return v;
}
/**
\brief Given
m := a metavariable ?m
@ -994,6 +1027,9 @@ struct unifier_fn {
(?m_n a_1 ... a_k) =?= b_n
?m =?= fun (x_1 ... x_k), f (?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k)
Remark: we try to minimize the number of constraints (?m_i a_1 ... a_k) =?= b_i by detecting "easy" cases
that can be solved immediately. See \c is_easy_flex_rigid_arg
Remark: The term f is:
- g (if g is a constant), OR
- variable (if g is a local constant equal to a_i)
@ -1012,9 +1048,13 @@ struct unifier_fn {
get_app_args(rhs, rargs);
buffer<expr> sargs;
for (expr const & rarg : rargs) {
expr maux = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
sargs.push_back(mk_app_vars(maux, margs.size()));
if (auto v = is_easy_flex_rigid_arg(margs, rarg)) {
sargs.push_back(*v);
} else {
expr maux = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
sargs.push_back(mk_app_vars(maux, margs.size()));
}
}
expr v = mk_app(f, sargs);
v = mk_lambda_for(mtype, v);