Experiments of Program Inversion by REPIUS and Completion

last modified: Dec 01, 2008

example	TRS	inverse TRS	completion with a fixed LPO	result (cycles)	call AProVE	time	result (cycles)	call AProVE	time	inverse program
				modified completion with AProVE 1.2			simplified completion with AProVE 1.2
du (primitive)	du.trs	du.trs	success	fail (1 cycle)	1 time	0.71 s	success (0 cycle)	1 time	0.71 s	du.sml
snoc.fct	snoc.trs	invsnoc.trs	success	success (1 cycle)	2 times	2.08 s	success (1 cycle)	2 times	2.07 s	invsnoc.sml
snocrev.fct	snocrev.trs	invsnocrev.trs	---	success (2 cycles)	3 times	4.29 s	success (2 cycles)	3 times	4.28 s	invsnocrev.sml
double.fct	double.trs	invdouble.trs	---	fail (2 cycles)	2 times	2.84 s	success (1 cycle)	2 times	2.83 s	invdouble.sml
mirror.fct	mirror.trs	invmirror.trs	---	fail (3 cycles)	3 times	5.97 s	success (2 cycles)	3 times	5.96 s	invmirror.sml
zip.fct	zip.trs	invzip.trs	success	success (0 cycle)	1 time	1.04 s	success (0 cycle)	1 time	1.03 s	invzip.sml
inc.fct	inc.trs	invinc.trs	success	success (1 cycle)	2 times	2.80 s	success (1 cycle)	2 times	2.80 s	invinc.sml
octbin.fct	octbin.trs	invoctbin.trs	success	success (0 cycle)	1 time	7.33 s	success (0 cycle)	1 time	7.33 s	invoctbin.sml
treelist.fct	treelist.trs	invtreelist.trs	---	success (4 cycles)	5 times	159.02 s	fail (2 cycles)	2 times	67.43 s	invtreelist.sml
print-sexp.fct	print-sexp.trs	invprint-sexp.trs	---	success (6 cycles)	7 times	28.20 s	success (6 cycles)	7 times	28.28 s	invprint-sexp.sml
print-xml.fct	print-xml.trs	invprint-xml.trs	---	fail (3 cycles)	3 times	9.49 s	success (2 cycles)	3 times	9.47 s	invprint-xml.sml

Produced by N.Nishida (nishida @ is.nagoya-u.ac.jp)