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
_______________________________________________
llvm-commits mailing list
llvm-commits@cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits
