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

Add max_sharing tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-20 22:01:40 -07:00
parent d34cfe3f8a
commit 7ac94ee976
2 changed files with 53 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/library/CMakeLists.txt
View file

@ -7,3 +7,6 @@ add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier)
add_executable(formatter formatter.cpp)
target_link_libraries(formatter ${EXTRA_LIBS})
add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter)
add_executable(max_sharing max_sharing.cpp)
target_link_libraries(max_sharing ${EXTRA_LIBS})
add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing)

50
src/tests/library/max_sharing.cpp Normal file
View file

@ -0,0 +1,50 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <iostream>
#include "util/test.h"
#include "kernel/abstract.h"
#include "library/max_sharing.h"
#include "library/printer.h"
using namespace lean;
static void tst1() {
max_sharing_fn max_fn;
expr a1 = Const("a");
expr a2 = Const("a");
expr F1 = Eq(a1, a2);
lean_assert(!is_eqp(eq_lhs(F1), eq_rhs(F1)));
expr F2 = max_fn(F1);
lean_assert(is_eqp(eq_lhs(F2), eq_rhs(F2)));
expr x = Const("x");
expr y = Const("y");
expr f = Const("f");
expr N = Const("N");
F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y)));
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1);
std::cout << F2 << "\n";
lean_assert(is_eqp(arg(F2, 1), arg(F2, 2)));
max_fn.clear();
meta_ctx ctx{mk_lift(1, 1), mk_inst(0, a1)};
expr m1 = mk_metavar(0, ctx);
expr m2 = mk_metavar(0, ctx);
F1 = f(m1, m2);
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1);
std::cout << F2 << "\n";
lean_assert(is_eqp(arg(F2, 1), arg(F2, 2)));
F1 = f(Let({x, f(a1)}, f(x, x)), Let({y, f(a1)}, f(y, y)));
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1);
std::cout << F2 << "\n";
lean_assert(is_eqp(arg(F2, 1), arg(F2, 2)));
}
int main() {
tst1();
return has_violations() ? 1 : 0;
}