From f67b5c4d0029fa6848ea8fad6c012dc52f6e9ee9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jan 2014 13:50:35 -0800
Subject: [PATCH] test(tests/lua): more to_ceqs tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lua/ceq1.lua | 52 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua
index e08a1be0b..5ed6b651d 100644
--- a/tests/lua/ceq1.lua
+++ b/tests/lua/ceq1.lua
@@ -31,4 +31,56 @@ test_ceq("Ax2", 1)
 test_ceq("Ax3", 4)
 test_ceq("Ax4", 0)
 test_ceq("Ax5", 1)
+-- test_ceq("eta", 1)
+test_ceq("not_not_eq", 1)
+test_ceq("or_comm", 1)
+test_ceq("or_assoc", 1)
+test_ceq("or_id", 1)
+test_ceq("or_falsel", 1)
+test_ceq("or_falser", 1)
+test_ceq("or_truel", 1)
+test_ceq("or_truer", 1)
+test_ceq("or_tauto", 1)
+test_ceq("and_comm", 1)
+test_ceq("and_assoc", 1)
+test_ceq("and_id", 1)
+test_ceq("and_falsel", 1)
+test_ceq("and_falser", 1)
+test_ceq("and_truel", 1)
+test_ceq("and_truer", 1)
+test_ceq("and_absurd", 1)
+test_ceq("imp_truer", 1)
+test_ceq("imp_truel", 1)
+test_ceq("imp_falser", 1)
+test_ceq("imp_falsel", 1)
+test_ceq("not_and", 1)
+test_ceq("not_or", 1)
+test_ceq("not_iff", 1)
+test_ceq("not_implies", 1)
+test_ceq("or_left_comm", 1)
+test_ceq("and_left_comm", 1)
+test_ceq("forall_or_distributer", 1)
+test_ceq("forall_or_distributel", 1)
+test_ceq("forall_and_distribute", 1)
+test_ceq("exists_and_distributer", 1)
+test_ceq("exists_and_distributel", 1)
+test_ceq("exists_or_distribute", 1)
+test_ceq({"Nat", "add_zeror"}, 1)
+test_ceq({"Nat", "add_zerol"}, 1)
+test_ceq({"Nat", "add_comm"}, 1)
+test_ceq({"Nat", "add_assoc"}, 1)
+test_ceq({"Nat", "mul_zerol"}, 1)
+test_ceq({"Nat", "mul_zeror"}, 1)
+test_ceq({"Nat", "mul_onel"}, 1)
+test_ceq({"Nat", "mul_oner"}, 1)
+test_ceq({"Nat", "mul_comm"}, 1)
+test_ceq({"Nat", "mul_assoc"}, 1)
+test_ceq({"Nat", "add_comm"}, 1)
+test_ceq({"Nat", "add_assoc"}, 1)
+test_ceq({"Nat", "distributer"}, 1)
+test_ceq({"Nat", "distributel"}, 1)
+test_ceq({"Nat", "le_refl"}, 1)
+test_ceq({"Nat", "le_zero"}, 1)
+test_ceq({"Nat", "not_lt_0"}, 1)
+test_ceq({"Nat", "lt_nrefl"}, 1)