]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/paramodulation/README
Bug fixed in injection: lifting was not performed correctly, but it worked
[helm.git] / components / tactics / paramodulation / README
1 make saturate per compilare l'eseguibile da riga di comando (make saturate.opt per la versione ottimizzata)
2
3 ./saturate -h per vedere una lista di parametri:
4
5 ./saturate: unknown option `-h'.
6 Usage:
7   -full Enable full mode
8   -f Enable/disable full-reduction strategy (default: enabled)
9   -r Weight-Age equality selection ratio (default: 4)
10   -s symbols-based selection ratio (relative to the weight ratio, default: 0)
11   -c Configuration file (for the db connection)
12   -o Term ordering. Possible values are:
13         kbo: Knuth-Bendix ordering
14         nr-kbo: Non-recursive variant of kbo (default)
15         lpo: Lexicographic path ordering
16   -l Time limit in seconds (default: no limit)
17   -w Maximal width (default: 3)
18   -d Maximal depth (default: 3)
19   -retrieve retrieve only
20   -help  Display this list of options
21   --help  Display this list of options
22
23
24 ./saturate -l 10 -demod-equalities
25
26 dove -l 10 e` il timeout in secondi.
27
28 Il programma legge da standard input il teorema, per esempio
29
30 \forall n:nat.n + n = 2 * n
31 \forall n:R.n + n = 2 * n
32 \forall n:R.n+n=n+n
33
34 l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
35
36 In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
37 active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
38 su file, per esempio usando tee:
39
40 ./saturate -l 10 -demod-equalities | tee output.txt
41
42 Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
43 funzione Inference.string_of_equality)
44
45