[llvm-commits] CVS: llvm-test/MultiSource/Applications/SPASS/small_problem.dfg Makefile

[Lauro Ramos Venancio]

Changes in directory llvm-test/MultiSource/Applications/SPASS:

small_problem.dfg added (r1.1)
Makefile updated: 1.7 -> 1.8
---
Log message:

Implement SMALL_PROBLEM_SIZE.


---
Diffs of the changes:  (+158 -0)

 Makefile          |    4 +
 small_problem.dfg |  154 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 158 insertions(+)


Index: llvm-test/MultiSource/Applications/SPASS/small_problem.dfg
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/small_problem.dfg:1.1
*** /dev/null	Thu May  3 11:55:56 2007
--- llvm-test/MultiSource/Applications/SPASS/small_problem.dfg	Thu May  3 11:55:46 2007
***************
*** 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.
+ %------------------------------------------------------------------------------


Index: llvm-test/MultiSource/Applications/SPASS/Makefile
diff -u llvm-test/MultiSource/Applications/SPASS/Makefile:1.7 llvm-test/MultiSource/Applications/SPASS/Makefile:1.8
--- llvm-test/MultiSource/Applications/SPASS/Makefile:1.7	Thu Sep  1 13:55:05 2005
+++ llvm-test/MultiSource/Applications/SPASS/Makefile	Thu May  3 11:55:46 2007
@@ -4,6 +4,10 @@
 CPPFLAGS = -DCLOCK_NO_TIMING -fno-strict-aliasing -w
 LDFLAGS  = -lm
 
+ifdef SMALL_PROBLEM_SIZE
+RUN_OPTIONS="$(PROJ_SRC_DIR)/small_problem.dfg"
+else
 RUN_OPTIONS="$(PROJ_SRC_DIR)/problem.dfg"
+endif
 
 include ../../Makefile.multisrc