1 make saturate per compilare l'eseguibile da riga di comando (make saturate.opt per la versione ottimizzata)
3 ./saturate -h per vedere una lista di parametri:
5 ./saturate: unknown option `-h'.
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
24 ./saturate -l 10 -demod-equalities
26 dove -l 10 e` il timeout in secondi.
28 Il programma legge da standard input il teorema, per esempio
30 \forall n:nat.n + n = 2 * n
32 l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
34 In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
35 active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
36 su file, per esempio usando tee:
38 ./saturate -l 10 -demod-equalities | tee output.txt
40 Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
41 funzione Inference.string_of_equality)