4
5cchelp :-
6 nl,
7 write(' Use help(topic) to access help for a specific topic.'),nl,
8 write(' Help is available on the following topics:'),nl,
9 nl,
10 write(' loadf -- read input theory from a file'),nl,
11 write(' sat -- determine whether theory is satisfiable'),nl,
12 write(' query -- find a plan containing given facts'),nl,
13 write(' nmquery -- find a plan satisfying a given nonmonotonic query'),nl,
14 write(' options -- commands to configure user options'), nl.
15
16cchelp(loadf) :-
17 nl,
18 write(' loadf \'Filename\':'), nl,
19 write(' Reads a causal theory from a given input file, and writes the literal'), nl,
20 write(' completion of the theory (in clausal form) to a file. The input file may be'), nl,
21 write(' in either action language C+ or the language of causal theories. The'), nl,
22 write(' completion is written to a file in DIMACS format, which can be used by most'), nl,
23 write(' current satisfiability solvers.'), nl.
24
25cchelp(query) :-
26 nl,
27 write(' query:'), nl,
28 write(' Used after a domain description in history or transition mode has been'), nl,
29 write(' loaded with \'loadf\'. Prompts the user for a set of rules, e.g. facts'), nl,
30 write(' specifying an initial and goal state, then finds and displays plans which'), nl,
31 write(' satisfy the union of these rules with the domain description. This is a'), nl,
32 write(' monotonic query; that is, the clauses generated by the rules in the query'), nl,
33 write(' are simply appended to the clauses generated by literal completion from the'), nl,
34 write(' domain description. See \'nmquery\' for nonmonotonic queries.'), nl,
35 nl,
36 write(' query Label:'), nl,
37 write(' Similar to \'query\', but instead of prompting the user for query rules, it'), nl,
38 write(' uses a predefined query from the input file, selected by its label. If the'), nl,
39 write(' queries in an input file are unlabeled, they are assigned integer labels'), nl,
40 write(' beginning with 0 (so that "query 0." will execute the first query in the'), nl,
41 write(' input file). Note that queries and nmqueries have separate name spaces,'), nl,
42 write(' so that a query and an nmquery in the same file may have the same label,'), nl,
43 write(' and a \'query Label\' command will not execute an nmquery with that label'), nl,
44 write(' and vice versa.'), nl.
45
46
47cchelp(nmquery) :-
48 nl,
49 write(' nmquery:'), nl,
50 write(' Executes a nonmonotonic query after a domain description in history or'), nl,
51 write(' transition mode has been loaded with \'loadf\'. Prompts the user for a set'), nl,
52 write(' of rules, then finds models which satisy both the literal completion of the'), nl,
53 write(' rules and the literal completion of the domain description. The nmqueries'), nl,
54 write(' are nonmonotonic; rules in the nmquery can "override" rules in the domain'), nl,
55 write(' description, since literal completion is performed separately on each set of'), nl,
56 write(' rules.'), nl,
57 nl,
58 write(' nmquery Label:'), nl,
59 write(' Similar to \'nmquery\', but instead of prompting the user for rules, it'), nl,
60 write(' uses a predefined nmquery from the input file, selected by its label. If'), nl,
61 write(' the nmqueries in an input file are unlabeled, they are assigned integer'), nl,
62 write(' labels beginning with 0 (so that "nmquery 0." will execute the first nmquery'), nl,
63 write(' in the input file). Note that queries and nmqueries have separate name'), nl,
64 write(' spaces, so that a query and an nmquery in the same file may have the same'), nl,
65 write(' label, and a \'query Label\' command will not execute an nmquery with that'), nl,
66 write(' label and vice versa.'), nl.
67
68cchelp(sat) :-
69 nl,
70 write(' sat:'),nl,
71 write(' In basic mode, this command instructs CCalc to find satisfying'), nl,
72 write(' interpretations of the input theory. In history or transition mode, CCalc'), nl,
73 write(' will find satisfying interpretations of the initial state only (time step'), nl,
74 write(' zero).'), nl.
75
76cchelp(options) :-
77 nl,
78 write(' CCalc has several user-definable options. Three commands are used to'), nl,
79 write(' access these options:'),nl,
80 nl,
81 write(' set(Option,Value):'),nl,
82 write(' Sets the given option to the given value. CCalc performs some checks to'), nl,
83 write(' ensure that the value is a legal one; see the options listed below for more'), nl,
84 write(' details.'), nl,
85 nl,
86 write(' show_options:'), nl,
87 write(' Lists the current values for all user options.'),nl,
88 nl,
89 write(' reset_options:'), nl,
90 write(' Sets all user options to default values.'), nl,
91 nl,
92 write(' Default values for the options are contained in the file \'options.std\'.'), nl,
93 write(' This file must be present in the CCalc installation directory, and also'), nl,
94 write(' may optionally be present in the user\'s current working directory. When'), nl,
95 write(' CCalc is first loaded, and again whenever the reset_options command is'), nl,
96 write(' executed, CCalc will first load \'options.std\' from the CCalc directory, and'), nl,
97 write(' then load the copy from the user\'s working directory if there is one.'), nl,
98 write(' Values specified in the latter will override those from the former. This'), nl,
99 write(' allows the system administrator to set default values for all users, but'), nl,
100 write(' permits each user to specify his own defaults if he chooses, or even to have'), nl,
101 write(' a different set of defaults for each of his input files by storing each in a'), nl,
102 write(' directory with a different copy of \'options.std\'.'), nl,
103 nl,
104 write(' The options are listed below, and further help is available on each:'), nl,
105 nl,
106 write(' solver -- which satisfiability solver to use'), nl,
107 write(' solver_opts -- command-line arguments to pass to the solver'), nl,
108 write(' num -- the maximum number of models desired'), nl,
109 write(' dir -- the base directory for input files'), nl,
110 write(' file_io -- whether to use files instead of pipes'), nl,
111 write(' timed -- whether to display time messages'), nl,
112 write(' verbose -- whether to display extra information'), nl,
116 write(' compact -- whether to compact the clauses before solving'), nl,
117 write(' optimize -- whether to shorten clauses with auxiliary atoms'), nl,
118 write(' eliminate_tautologies -- whether to remove tautologies from the theory'), nl,
119 nl,
120 write(' Note that for all of the options which require true/false values (everything'), nl,
121 write(' after \'dir\' in the list above), yes/no, on/off, and t/f are also acceptable'), nl,
122 write(' values.'), nl.
123
124cchelp(solver) :-
125 nl,
126 write(' The "solver" option establishes which satisfiability solver CCalc will'), nl,
127 write(' call. Valid values are:'), nl,
128 nl,
129 write(' grasp -- GRASP, Feb. 2000 version, by João Marques Silva'), nl,
130 write(' mchaff -- mChaff version spelt3, by Matthew Moskewicz'), nl,
131 write(' relsat -- relsat version 2.02, by Roberto Bayardo'), nl,
132 write(' relsat_old -- relsat version 1.1.2, by Roberto Bayardo'), nl,
133 write(' sato -- SATO version 3.2, by Hantao Zhang'), nl,
134 write(' sato_old -- SATO version 3.1.2, by Hantao Zhang'), nl,
135 write(' satz -- Satz215.2, by Chu-Min Li'), nl,
136 write(' satz-rand -- satz-rand 4.9, by Henry Kautz'), nl,
137 write(' walksat -- WalkSAT version 41, by Henry Kautz and Bart Selman'), nl,
138 write(' zchaff -- zChaff, by Lintao Zhang'), nl.
139
140
141cchelp(solver_opts) :-
142 nl,
143 write(' The \"solver_opts\" option is used to pass command-line arguments to the SAT'), nl,
144 write(' solver. Each solver has a separate option \"solver_opts(Solver)\",'), nl,
145 write(' and its value will only be used when calling that particular solver. Legal'), nl,
146 write(' values are any string enclosed in single quotes; this string will be'), nl,
147 write(' inserted into the command line when CCalc calls the SAT solver. Note that'), nl,
148 write(' some command-line arguments, such as those which control the solver\'s'), nl,
149 write(' output, are required by CCalc and are always present in the command line'), nl,
150 write(' regardless of the value of solver_opts.'), nl.
151
152cchelp(num) :-
153 nl,
154 write(' The \"num\" option determines the number of models to request from the SAT'), nl,
155 write(' request from the solver.'), nl,
156 nl,
157 write(' When the solver is set to grasp, mchaff, or relsat, the value of num may'), nl,
158 write(' be any positive integer or \'all\', the latter indicating that the solver'), nl,
159 write(' should return all solutions to the problem.'), nl,
160 nl,
161 write(' For solvers sato, sato_old, and walksat, the value of this option may be'), nl,
162 write(' any positive integer. These solvers cannot return \'all\' solutions; the'), nl,
163 write(' user must specify a number of interpretations at least as large as the'), nl,
164 write(' number of solutions to obtain all solutions. Note that these solvers are'), nl,
165 write(' incomplete. SATO may find fewer than N models even when N exist, though it'), nl,
166 write(' will always find at least one if the theory is satisfiable, and WalkSAT is'), nl,
167 write(' stochastic and may not find any models of a satisfiable theory.'), nl,
168 nl,
169 write(' For other solvers, num must be set to 1. Only the solvers listed above'), nl,
170 write(' are capable of returning multiple models.'), nl.
171
172cchelp(dir) :-
173 nl,
174 write(' The \"dir\" option specifies the directory which contains the user\'s input'), nl,
175 write(' files. When CCalc tries to load a file, it will first try the directory'), nl,
176 write(' specified this option. If it fails to find the requested file there, it'), nl,
177 write(' will then search other directories, including the current working directory'), nl,
178 write(' and the CCalc installation directory. Thus, the user does not need to set'), nl,
179 write(' this option if she simply changes to the correct directory each time she'), nl,
180 write(' loads a file.'), nl.
181
182cchelp(timed) :-
183 nl,
184 write(' The "timed" option determines whether CCalc will display time messages.'), nl,
185 write(' When it is set to \'true\', CCalc will report the time it takes for'), nl,
186 write(' grounding, completion, and finding the solution. If the "compact"'), nl,
187 write(' option is on, CCalc will also report the compaction time; and if the'), nl,
188 write(' "verbose" option is on, CCalc will also report the time taken for some of'), nl,
189 write(' the additional steps reported. When \"timed\" is set to \'false\', CCalc'), nl,
190 write(' will not report any time information.'), nl.
191
192cchelp(verbose) :-
193 nl,
194 write(' The "verbose" option determines the amount of information CCalc produces'), nl,
195 write(' when processing a command. If the option is set to \'false\', CCalc will'), nl,
196 write(' provide minimal information. If it is set to \'true\', CCalc will provide'), nl,
197 write(' additional information, such as reporting what it is doing at each step.'), nl,
198 write(' If the "timed" option is also on, CCalc will report the time taken by'), nl,
199 write(' some of these additional steps reported as well.'), nl.
200
201
202cchelp(file_io) :-
203 nl,
204
205 write(' The "file_io" option determines whether CCalc uses files or pipes to'), nl,
206 write(' communicate with the SAT solver. When this option is set to \'false\', CCalc'), nl,
207 write(' will use named pipes. When it is set to true, CCalc will use files'), nl,
208 write(' ccsat.in, ccsat.out, etc.) instead. This allows the user to inspect the SAT'), nl,
209 write(' solver\'s input and output, and is also useful if the user\'s system does not'), nl,
210 write(' support the system calls CCalc uses to create the pipes.'), nl.
211
226
227cchelp(compact) :-
228 nl,
229 write(' Setting the "compact" option to \'true\' will cause CCalc to call'), nl,
230 write(' James Crawford\'s "compact" program on the input file to the satisfiability'), nl,
231 write(' solver. Compaction reduces the size of the theory by employing a \"failed'), nl,
232 write(' literal rule\": for each literal L, if performing unit clause propagation'), nl,
233 write(' on the union of the theory and {L} resolves to a contradiction, then the'), nl,
234 write(' complement of L is added to the theory and unit clause propagation is'), nl,
235 write(' performed on that literal. This can dramatically reduce the number of'), nl,
236 write(' atoms and clauses in the theory passed to the satisfiability solver.'), nl,
237 write(' If the option is set to \'false\', the input will not be compacted.'), nl.
238
239cchelp(optimize) :-
240 nl,
241 write(' When \"optimize\" is set to \'true\', CCalc will introduce new atoms'), nl,
242 write(' during the clausification of rules, to avoid the combinatorial clause'), nl,
243 write(' explosion that can result from distributing conjunction over disjunction'), nl,
244 write(' or vice versa. This increases the number of atoms, but can greatly '), nl,
245 write(' decrease the number of clauses and the computation time required to ground'), nl,
246 write(' the input theory.'), nl.
247
248cchelp(eliminate_tautologies) :-
249 nl,
250 write(' When "eliminate_tautologies" is set to \'true\', CCalc will eliminate'), nl,
251 write(' tautological clauses generated during completion rather than including them'), nl,
252 write(' in the theory. This will generally lead to improved performance for the SAT'), nl,
253 write(' solver, though sometimes leaving the tautologies in the theory may guide the'), nl,
254 write(' solver\'s search in a beneficial way.'), nl