Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 154 insertions, 0 deletions

diff --git a/test/spass/small_problem.dfg b/test/spass/small_problem.dfg
new file mode 100644
index 0000000..f0b1a6d
--- /dev/null
+++ b/test/spass/small_problem.dfg
@@ -0,0 +1,154 @@
+%------------------------------------------------------------------------------
+% File     : SET002+4 : TPTP v3.1.0. Released v2.2.0.
+% Domain   : Set Theory (Naive)
+% Problem  : Idempotency of union
+% Version  : [Pas99] axioms.
+% English  :
+
+% Refs     : [Pas99] Pastre (1999), Email to G. Sutcliffe
+% Source   : [Pas99]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.36 v3.1.0, 0.56 v2.7.0, 0.33 v2.6.0, 0.57 v2.5.0, 0.50 v2.4.0, 0.25 v2.3.0, 0.00 v2.2.1
+% Syntax   : Number of formulae    :   12 (   2 unit)
+%            Number of atoms       :   30 (   3 equality)
+%            Maximal formula depth :    7 (   5 average)
+%            Number of connectives :   20 (   2 ~  ;   2  |;   4  &)
+%                                         (  10 <=>;   2 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    4 (   0 propositional; 2-2 arity)
+%            Number of functors    :    9 (   1 constant; 0-2 arity)
+%            Number of variables   :   29 (   0 singleton;  28 !;   1 ?)
+%            Maximal term depth    :    2 (   1 average)
+
+% Comments : 
+%          : tptp2X -f dfg -t rm_equality:rstfp SET002+4.p 
+%------------------------------------------------------------------------------
+
+begin_problem(TPTP_Problem).
+
+list_of_descriptions.
+name({*[ File     : SET002+4 : TPTP v3.1.0. Released v2.2.0.],[ Names    :]*}).
+author({*[ Source   : [Pas99]]*}).
+status(unknown).
+description({*[ Refs     : [Pas99] Pastre (1999), Email to G. Sutcliffe]*}).
+end_of_list.
+
+list_of_symbols.
+functions[(difference,2), (empty_set,0), (intersection,2), (power_set,1), (product,1), (singleton,1), (sum,1), (union,2), (unordered_pair,2)].
+predicates[(equal_set,2), (member,2), (subset,2)].
+end_of_list.
+
+list_of_formulae(axioms).
+
+formula(
+ forall([A,B],
+  equiv(
+   subset(A,B),
+   forall([X],
+    implies(
+     member(X,A),
+     member(X,B))))),
+subset ).
+
+formula(
+ forall([A,B],
+  equiv(
+   equal_set(A,B),
+   and(
+    subset(A,B),
+    subset(B,A)))),
+equal_set ).
+
+formula(
+ forall([X,A],
+  equiv(
+   member(X,power_set(A)),
+   subset(X,A))),
+power_set ).
+
+formula(
+ forall([X,A,B],
+  equiv(
+   member(X,intersection(A,B)),
+   and(
+    member(X,A),
+    member(X,B)))),
+intersection ).
+
+formula(
+ forall([X,A,B],
+  equiv(
+   member(X,union(A,B)),
+   or(
+    member(X,A),
+    member(X,B)))),
+union ).
+
+formula(
+ forall([X],
+  not(
+   member(X,empty_set))),
+empty_set ).
+
+formula(
+ forall([B,A,E],
+  equiv(
+   member(B,difference(E,A)),
+   and(
+    member(B,E),
+    not(
+     member(B,A))))),
+difference ).
+
+formula(
+ forall([X,A],
+  equiv(
+   member(X,singleton(A)),
+   equal(X,A))),
+singleton ).
+
+formula(
+ forall([X,A,B],
+  equiv(
+   member(X,unordered_pair(A,B)),
+   or(
+    equal(X,A),
+    equal(X,B)))),
+unordered_pair ).
+
+formula(
+ forall([X,A],
+  equiv(
+   member(X,sum(A)),
+   exists([Y],
+    and(
+     member(Y,A),
+     member(X,Y))))),
+sum ).
+
+formula(
+ forall([X,A],
+  equiv(
+   member(X,product(A)),
+   forall([Y],
+    implies(
+     member(Y,A),
+     member(X,Y))))),
+product ).
+
+end_of_list.
+
+%----NOTE WELL: conjecture has been negated
+list_of_formulae(conjectures).
+
+formula(  %(conjecture)
+ forall([A],
+  equal_set(union(A,A),A)),
+thI14 ).
+
+end_of_list.
+
+end_problem.
+%------------------------------------------------------------------------------