few_examples
The following examples are from the distribution that accompanies the paper: Size-Change Termination in Polynomial Time (Ben-Amram, Amir M. and Lee, Chin Soon), ACM TOPLAS, 29:1 (2007).
| ex01.pl | : Ackerman function. |
| ex02.pl | : nonterminating. |
| ex03.pl | : multiset descent. |
| ex04.pl | : multiset descent. |
| ex05.pl | : multiset descent. |
| ex06.pl | |
| ex07.pl | : example with a non-strongly connected CFG. One SCC is nonterminating. |
| ex08.pl | : demonstrates tags. |
| ex09.pl | |
| ex10.pl | |
| ex11.pl | |
| ex12.pl | : non-SCNP example. |
| ex13.pl | : nonterminating. |
| ex14.pl | |
| ex15.pl | |
| ex16.pl | |
| ex17.pl | |
| ex18.pl |
few_more_examples
| a000.pl | |
| a00.pl | |
| a01.pl | |
| a02.pl | |
| a031.pl | |
| a03.pl | |
| a04.pl | |
| a05.pl | |
| a06.pl | |
| a07.pl | |
| a08.pl | |
| a09.pl | |
| a10.pl | |
| a11.pl | |
| a12.pl | |
| a13.pl |
flat_trs
These 4062 sets of scg;s were generated when AProVE was proving termination for the TPDB version 4.0 using size change termination with dependency pairs with the underlying embedding ordering.
scnp_paper
examples from the paper: "A SAT-Based Approach to Size Change Termination with Global Ranking Functions"
| example1.pl | |
| example5.pl | |
| example7.pl |
scp_paper
The following are the 123 examples from the benchmarks of the paper: Size-Change Termination in Polynomial Time (Ben-Amram, Amir M. and Lee, Chin Soon), ACM TOPLAS, 29:1 (2007). These programs originate from a logic programming context and were collected from various sources by Naomi Lindenstrauss. For every file, its origin is listed (which program from the benchmark collection and what query). The source programs are also available in the SCP distribution. The programs with ".csl" are those that CSL changed from NL's source.
| scgs0001.pl | : dds/dds1.1 append(b,b,f) |
| scgs0002.pl | : dds/dds1.1 append(f,f,b) |
| scgs0003.pl | : dds/dds1.1 append(f,b,f) |
| scgs0004.pl | : dds/dds1.2 permute(b,f) |
| scgs0005.pl | : dds/dds3.8 reverse(b,f,b) |
| scgs0006.pl | : dds/dds3.13 duplicate(b,f) |
| scgs0007.pl | : dds/dds3.14 sum(b,b,f) |
| scgs0008.pl | : dds/dds3.15 merge(b,b,f) |
| scgs0009.pl | : dds/dds3.17 dis(b) |
| scgs0010.pl | : dds/dds3.17 con(b) |
| scgs0011.pl | : plumer/pl1.1 append(b,b,f) |
| scgs0012.pl | : plumer/pl1.1 append(f,f,b) |
| scgs0013.pl | : plumer/pl1.1 append(f,b,f) |
| scgs0014.pl | : plumer/pl1.2.csl perm(b,f) |
| scgs0015.pl | : plumer/pl1.2_t.csl perm(b,f) |
| scgs0016.pl | : plumer/pl2.3.1 p(f,b) |
| scgs0017.pl | : plumer/pl3.5.6 p(f) |
| scgs0018.pl | : plumer/pl3.5.6a p(f) |
| scgs0019.pl | : plumer/pl4.01 append3(b,b,b,f) |
| scgs0020.pl | : plumer/pl4.01 append3(f,b,b,b) |
| scgs0021.pl | : plumer/pl4.4.3 merge(b,b,f) |
| scgs0022.pl | : plumer/pl4.4.6a perm(b,f) |
| scgs0023.pl | : plumer/pl4.5.2 s(b,f) |
| scgs0024.pl | : plumer/pl4.5.3a p(b) |
| scgs0025.pl | : plumer/pl4.5.3b goal |
| scgs0026.pl | : plumer/pl4.5.3c goal |
| scgs0027.pl | : plumer/pl5.2.2 turing(b,b,b,f) |
| scgs0028.pl | : plumer/pl6.1.1 qsort(b,f) |
| scgs0029.pl | : plumer/pl7.2.9 mult(b,b,f) |
| scgs0030.pl | : plumer/pl7.6.2a reach(b,b,b) |
| scgs0031.pl | : plumer/pl7.6.2b reach(b,b,b,b) |
| scgs0032.pl | : plumer/pl7.6.2c reach(b,b,b,b) |
| scgs0033.pl | : plumer/pl8.2.1 mergesort(b,f) |
| scgs0034.pl | : plumer/pl8.2.1a mergesort(b,f) |
| scgs0035.pl | : plumer/mergesort_t mergesort(b,f) |
| scgs0036.pl | : plumer/pl8.3.1 minsort(b,f) |
| scgs0037.pl | : plumer/pl8.3.1a minsort(b,f) |
| scgs0038.pl | : plumer/pl8.4.1 even(b) |
| scgs0039.pl | : plumer/pl8.4.1 odd(b) |
| scgs0040.pl | : plumer/pl8.4.2 e(b,f) |
| scgs0041.pl | : apt/list list(b) |
| scgs0042.pl | : apt/member member(f,b) |
| scgs0043.pl | : apt/subset subset(b,b) |
| scgs0044.pl | : apt/subset subset(f,b) |
| scgs0045.pl | : apt/append app(b,f,f) |
| scgs0046.pl | : apt/append app(f,f,b) |
| scgs0047.pl | : apt/select select(f,b,f) |
| scgs0048.pl | : apt/sum sum(f,b,f) |
| scgs0049.pl | : apt/sum sum(f,f,b) |
| scgs0050.pl | : apt/lte goal |
| scgs0051.pl | : apt/naive_rev reverse(b,f) |
| scgs0052.pl | : apt/dc_schema dcsolve(b,f) |
| scgs0053.pl | : apt/permutation.csl perm(b,f) |
| scgs0054.pl | : apt/quicksort qs(b,f) |
| scgs0055.pl | : apt/overlap overlap(b,b) |
| scgs0056.pl | : apt/mergesort mergesort(b,f) |
| scgs0057.pl | : apt/mergesort_ap mergesort(b,f,b) |
| scgs0058.pl | : apt/curry_ap type(b,b,f) |
| scgs0059.pl | : apt/map map(b,f) |
| scgs0060.pl | : apt/gtsolve gtsolve(b,f) |
| scgs0061.pl | : apt/ordered ordered(b) |
| scgs0062.pl | : apt/fold fold(b,b,f) |
| scgs0063.pl | : apt/SS_map_t test_color(b,f) |
| scgs0064.pl | : maria/aiakl.pl init_vars(b,b,f,f) |
| scgs0065.pl | : maria/ann.pl go(b) |
| scgs0066.pl | : maria/bid.pl bid(b,f,f,f) |
| scgs0067.pl | : maria/boyer.pl tautology(b) |
| scgs0068.pl | : maria/browse.pl main |
| scgs0069.pl | : maria/deriv.pl d(b,b,f) |
| scgs0070.pl | : maria/fib_t fib(b,f) |
| scgs0071.pl | : maria/grammar.pl goal |
| scgs0072.pl | : maria/hanoiapp.suc shanoi(b,b,b,b,f) |
| scgs0073.pl | : maria/mmatrix.pl mmultiply(b,b,f) |
| scgs0074.pl | : maria/mmatrix.pl trans_m(b,f) |
| scgs0075.pl | : maria/money.pl money(f,f,f,f,f,f,f,f) |
| scgs0076.pl | : maria/occur.pl occurall(b,b,f) |
| scgs0077.pl | : maria/peephole.pl peephole_opt(b,f) |
| scgs0078.pl | : maria/progeom.pl pds(b,f) |
| scgs0079.pl | : maria/qplan.pl qplan(b,f) |
| scgs0080.pl | : maria/qsortapp.pl qsort(b,f) |
| scgs0081.pl | : maria/query.pl query(f) |
| scgs0082.pl | : maria/rdtok.pl goal |
| scgs0083.pl | : maria/read.pl goal |
| scgs0084.pl | : maria/serialize.pl serialize0(b,f) |
| scgs0085.pl | : maria/tak.pl tak(b,b,b,f) |
| scgs0086.pl | : maria/tictactoe.pl play(f) |
| scgs0087.pl | : maria/warplan.pl test2 |
| scgs0088.pl | : maria/zebra.pl zebra(f,f,f,f,f,f,f) |
| scgs0089.pl | : maria/zebra.pt houses(f) |
| scgs0090.pl | : various/p p |
| scgs0091.pl | : various/sublist sublist(b,b) |
| scgs0092.pl | : various/sicstus1 concatenate(b,b,f) |
| scgs0093.pl | : various/sicstus1 concatenate(b,f,f) |
| scgs0094.pl | : various/sicstus1 concatenate(f,f,b) |
| scgs0095.pl | : various/sicstus1 member(f,b) |
| scgs0096.pl | : various/sicstus1 reverse(b,f) |
| scgs0097.pl | : various/sicstus1 concatenate(f,b,f) |
| scgs0098.pl | : various/sicstus1 member(b,f) |
| scgs0099.pl | : various/sicstus1 reverse(f,b) |
| scgs0100.pl | : various/sicstus2 descendant(b,b) |
| scgs0101.pl | : various/sicstus3 put_assoc(b,b,b,f) |
| scgs0102.pl | : various/sicstus3 get_assoc(b,b,f) |
| scgs0103.pl | : various/sicstus4 d(b,b,f) |
| scgs0104.pl | : various/ack ack(b,b,f) |
| scgs0105.pl | : various/pql p(b,f) |
| scgs0106.pl | : various/pql.csl q(b,f) |
| scgs0107.pl | : various/pql q(f,b) |
| scgs0108.pl | : various/pql p(f,b) |
| scgs0109.pl | : various/pql q(f,f) |
| scgs0110.pl | : various/vangelder q(b,b) |
| scgs0111.pl | : various/deep_rev deep(b,f) |
| scgs0112.pl | : various/huffman huffman(b,f) |
| scgs0113.pl | : various/huffman code(b,f,f) |
| scgs0114.pl | : various/queens queens(b,f) |
| scgs0115.pl | : various/arit_exp e(b) |
| scgs0116.pl | : various/associative normal_form(b,f) |
| scgs0117.pl | : various/game win(b) |
| scgs0118.pl | : various/yale_s_p holds(b,b) |
| scgs0119.pl | : various/yale_s_p holds(f,b) |
| scgs0120.pl | : various/yale_s_p holds(b,f) |
| scgs0121.pl | : various/plan transform(b,b,f) |
| scgs0122.pl | : various/blocks tower(b,b,b,f) |
| scgs0123.pl | : various/credit credit(b,f) |