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

test(lua): add is_geq (for universe level) tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-17 13:42:01 -07:00
parent d0e7c88ea8
commit 53e02a902c
1 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
tests/lua/level7.lua Normal file
View file

@ -0,0 +1,24 @@
assert(max_univ("l1", "l2"):is_geq("l1"))
assert(max_univ("l1", "l2"):is_geq(max_univ("l2", "l1")))
print(max_univ("l2", "l1", "l3"))
assert(not max_univ("l1", "l2"):is_geq(max_univ("l2", "l1", "l3")))
assert(not imax_univ("l1", "l2"):is_geq("l1"))
assert(imax_univ("l1", "l2"):is_geq("l2"))
print(imax_univ("l1", succ_univ("l2")))
assert(imax_univ("l1", succ_univ("l2")):is_geq(max_univ("l2", "l1")))
assert(max_univ("l1", succ_univ("l2")):is_geq(max_univ("l2", "l1")))
assert(succ_univ("l1"):is_geq("l1"))
assert(succ_univ(succ_univ("l1")):is_geq("l1"))
assert(max_univ(1, 3):is_geq(3))
assert(max_univ(1, 3):is_geq(2))
assert(not max_univ(1, 3):is_geq(5))
local l1 = param_univ("l1")
local l2 = param_univ("l2")
local g = global_univ("g")
assert((g+1):is_geq(g))
assert((g+2):is_geq(g+1))
assert(not g:is_geq(l1))
assert(not max_univ(l1, l2):is_geq(max_univ(l2, l1+1)))
assert((max_univ(l1, l2) + 1):is_geq(max_univ(l2, l1+1)))
assert(max_univ(l1+2, l2, g+1):is_geq(max_univ(g+1, l1+1, l2)))
assert(not max_univ(l1+2, l2, g+1):is_geq(max_univ(g+2, l1+1, l2)))