From 7b4b862faa1fc2515100d6a62b6f227b6533e9f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 May 2014 12:16:24 -0700 Subject: [PATCH] test(lua): add justification API tests Signed-off-by: Leonardo de Moura --- tests/lua/jst1.lua | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/lua/jst1.lua diff --git a/tests/lua/jst1.lua b/tests/lua/jst1.lua new file mode 100644 index 000000000..b23731b0f --- /dev/null +++ b/tests/lua/jst1.lua @@ -0,0 +1,33 @@ +assert(is_justification(justification())) +assert(justification():is_none()) +assert(justification("simple"):is_asserted()) +local env = empty_environment() +local f = Const("f") +local g = Const("g") +local a = Const("a") +local j1 = justification("expression must be a type", env, f(f(a))) +assert(j1:is_asserted()) +print(j1:pp()) +local m = mk_metavar("m", Bool) +local j2 = justification("expresion must be a Proposition", env, g(m)) +print(j2:pp()) +local s = substitution() +s = s:assign(m, f(a)) +print(j2:pp(s)) +local j3 = assumption_justification(1) +assert(not j2:depends_on(1)) +assert(j3:depends_on(1)) +assert(not j3:depends_on(2)) +local j4 = assumption_justification(2) +assert(j4:depends_on(2)) +assert(not j4:depends_on(1)) +assert(j4:is_assumption()) +assert(not j4:main_expr()) +assert(j4:assumption_idx() == 2) +local j5 = mk_composite_justification(mk_composite_justification(j1, j4), j3) +assert(j5:depends_on(1)) +assert(j5:depends_on(2)) +assert(not j5:depends_on(3)) +assert(j5:is_composite()) +assert(j5:child2():is_eqp(j3)) +assert(j5:child1():child2():is_eqp(j4))