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

feat(library/expr_lt): make sure the total order on terms is monotonic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-20 13:06:30 -08:00
parent ac9f8f340d
commit 6a63ef3bc5
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/expr_lt.cpp
View file

@ -17,10 +17,14 @@ static bool is_lt(optional<expr> const & a, optional<expr> const & b, bool use_h
bool is_lt(expr const & a, expr const & b, bool use_hash) {
if (is_eqp(a, b)) return false;
unsigned a_sz = get_size(a);
unsigned b_sz = get_size(b);
if (a_sz < b_sz) return true;
if (a_sz > b_sz) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
if (use_hash) {
if (a.hash() < b.hash()) return true;
if (a.hash() > b.hash()) return false;
if (a.hash() < b.hash()) return true;
if (a.hash() > b.hash()) return false;
}
if (a == b) return false;
if (is_var(a)) return var_idx(a) < var_idx(b);

6
src/library/kernel_bindings.cpp
View file

@ -636,6 +636,11 @@ static int expr_size(lua_State * L) {
return 1;
}
static int expr_is_lt(lua_State * L) {
lua_pushboolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false));
return 1;
}
static const struct luaL_Reg expr_m[] = {
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
@ -674,6 +679,7 @@ static const struct luaL_Reg expr_m[] = {
{"occurs", safe_function<expr_occurs>},
{"has_metavar", safe_function<expr_has_metavar>},
{"is_eqp", safe_function<expr_is_eqp>},
{"is_lt", safe_function<expr_is_lt>},
{"hash", safe_function<expr_hash>},
{"is_not", safe_function<expr_is_not>},
{"is_and", safe_function<expr_is_and>},