%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% cchelp : help messages %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% cchelp :- nl, write(' Use help(topic) to access help for a specific topic.'),nl, write(' Help is available on the following topics:'),nl, nl, write(' loadf -- read input theory from a file'),nl, write(' sat -- determine whether theory is satisfiable'),nl, write(' query -- find a plan containing given facts'),nl, write(' nmquery -- find a plan satisfying a given nonmonotonic query'),nl, write(' options -- commands to configure user options'), nl. cchelp(loadf) :- nl, write(' loadf \'Filename\':'), nl, write(' Reads a causal theory from a given input file, and writes the literal'), nl, write(' completion of the theory (in clausal form) to a file. The input file may be'), nl, write(' in either action language C+ or the language of causal theories. The'), nl, write(' completion is written to a file in DIMACS format, which can be used by most'), nl, write(' current satisfiability solvers.'), nl. cchelp(query) :- nl, write(' query:'), nl, write(' Used after a domain description in history or transition mode has been'), nl, write(' loaded with \'loadf\'. Prompts the user for a set of rules, e.g. facts'), nl, write(' specifying an initial and goal state, then finds and displays plans which'), nl, write(' satisfy the union of these rules with the domain description. This is a'), nl, write(' monotonic query; that is, the clauses generated by the rules in the query'), nl, write(' are simply appended to the clauses generated by literal completion from the'), nl, write(' domain description. See \'nmquery\' for nonmonotonic queries.'), nl, nl, write(' query Label:'), nl, write(' Similar to \'query\', but instead of prompting the user for query rules, it'), nl, write(' uses a predefined query from the input file, selected by its label. If the'), nl, write(' queries in an input file are unlabeled, they are assigned integer labels'), nl, write(' beginning with 0 (so that "query 0." will execute the first query in the'), nl, write(' input file). Note that queries and nmqueries have separate name spaces,'), nl, write(' so that a query and an nmquery in the same file may have the same label,'), nl, write(' and a \'query Label\' command will not execute an nmquery with that label'), nl, write(' and vice versa.'), nl. cchelp(nmquery) :- nl, write(' nmquery:'), nl, write(' Executes a nonmonotonic query after a domain description in history or'), nl, write(' transition mode has been loaded with \'loadf\'. Prompts the user for a set'), nl, write(' of rules, then finds models which satisy both the literal completion of the'), nl, write(' rules and the literal completion of the domain description. The nmqueries'), nl, write(' are nonmonotonic; rules in the nmquery can "override" rules in the domain'), nl, write(' description, since literal completion is performed separately on each set of'), nl, write(' rules.'), nl, nl, write(' nmquery Label:'), nl, write(' Similar to \'nmquery\', but instead of prompting the user for rules, it'), nl, write(' uses a predefined nmquery from the input file, selected by its label. If'), nl, write(' the nmqueries in an input file are unlabeled, they are assigned integer'), nl, write(' labels beginning with 0 (so that "nmquery 0." will execute the first nmquery'), nl, write(' in the input file). Note that queries and nmqueries have separate name'), nl, write(' spaces, so that a query and an nmquery in the same file may have the same'), nl, write(' label, and a \'query Label\' command will not execute an nmquery with that'), nl, write(' label and vice versa.'), nl. cchelp(sat) :- nl, write(' sat:'),nl, write(' In basic mode, this command instructs CCalc to find satisfying'), nl, write(' interpretations of the input theory. In history or transition mode, CCalc'), nl, write(' will find satisfying interpretations of the initial state only (time step'), nl, write(' zero).'), nl. cchelp(options) :- nl, write(' CCalc has several user-definable options. Three commands are used to'), nl, write(' access these options:'),nl, nl, write(' set(Option,Value):'),nl, write(' Sets the given option to the given value. CCalc performs some checks to'), nl, write(' ensure that the value is a legal one; see the options listed below for more'), nl, write(' details.'), nl, nl, write(' show_options:'), nl, write(' Lists the current values for all user options.'),nl, nl, write(' reset_options:'), nl, write(' Sets all user options to default values.'), nl, nl, write(' Default values for the options are contained in the file \'options.std\'.'), nl, write(' This file must be present in the CCalc installation directory, and also'), nl, write(' may optionally be present in the user\'s current working directory. When'), nl, write(' CCalc is first loaded, and again whenever the reset_options command is'), nl, write(' executed, CCalc will first load \'options.std\' from the CCalc directory, and'), nl, write(' then load the copy from the user\'s working directory if there is one.'), nl, write(' Values specified in the latter will override those from the former. This'), nl, write(' allows the system administrator to set default values for all users, but'), nl, write(' permits each user to specify his own defaults if he chooses, or even to have'), nl, write(' a different set of defaults for each of his input files by storing each in a'), nl, write(' directory with a different copy of \'options.std\'.'), nl, nl, write(' The options are listed below, and further help is available on each:'), nl, nl, write(' solver -- which satisfiability solver to use'), nl, write(' solver_opts -- command-line arguments to pass to the solver'), nl, write(' num -- the maximum number of models desired'), nl, write(' dir -- the base directory for input files'), nl, write(' file_io -- whether to use files instead of pipes'), nl, write(' timed -- whether to display time messages'), nl, write(' verbose -- whether to display extra information'), nl, /* temporarily (?) disabled *jc* write(' sorted -- whether to sort the clauses before solving'), nl, */ write(' compact -- whether to compact the clauses before solving'), nl, write(' optimize -- whether to shorten clauses with auxiliary atoms'), nl, write(' eliminate_tautologies -- whether to remove tautologies from the theory'), nl, nl, write(' Note that for all of the options which require true/false values (everything'), nl, write(' after \'dir\' in the list above), yes/no, on/off, and t/f are also acceptable'), nl, write(' values.'), nl. cchelp(solver) :- nl, write(' The "solver" option establishes which satisfiability solver CCalc will'), nl, write(' call. Valid values are:'), nl, nl, write(' grasp -- GRASP, Feb. 2000 version, by João Marques Silva'), nl, write(' mchaff -- mChaff version spelt3, by Matthew Moskewicz'), nl, write(' relsat -- relsat version 2.02, by Roberto Bayardo'), nl, write(' relsat_old -- relsat version 1.1.2, by Roberto Bayardo'), nl, write(' sato -- SATO version 3.2, by Hantao Zhang'), nl, write(' sato_old -- SATO version 3.1.2, by Hantao Zhang'), nl, write(' satz -- Satz215.2, by Chu-Min Li'), nl, write(' satz-rand -- satz-rand 4.9, by Henry Kautz'), nl, write(' walksat -- WalkSAT version 41, by Henry Kautz and Bart Selman'), nl, write(' zchaff -- zChaff, by Lintao Zhang'), nl. cchelp(solver_opts) :- nl, write(' The \"solver_opts\" option is used to pass command-line arguments to the SAT'), nl, write(' solver. Each solver has a separate option \"solver_opts(Solver)\",'), nl, write(' and its value will only be used when calling that particular solver. Legal'), nl, write(' values are any string enclosed in single quotes; this string will be'), nl, write(' inserted into the command line when CCalc calls the SAT solver. Note that'), nl, write(' some command-line arguments, such as those which control the solver\'s'), nl, write(' output, are required by CCalc and are always present in the command line'), nl, write(' regardless of the value of solver_opts.'), nl. cchelp(num) :- nl, write(' The \"num\" option determines the number of models to request from the SAT'), nl, write(' request from the solver.'), nl, nl, write(' When the solver is set to grasp, mchaff, or relsat, the value of num may'), nl, write(' be any positive integer or \'all\', the latter indicating that the solver'), nl, write(' should return all solutions to the problem.'), nl, nl, write(' For solvers sato, sato_old, and walksat, the value of this option may be'), nl, write(' any positive integer. These solvers cannot return \'all\' solutions; the'), nl, write(' user must specify a number of interpretations at least as large as the'), nl, write(' number of solutions to obtain all solutions. Note that these solvers are'), nl, write(' incomplete. SATO may find fewer than N models even when N exist, though it'), nl, write(' will always find at least one if the theory is satisfiable, and WalkSAT is'), nl, write(' stochastic and may not find any models of a satisfiable theory.'), nl, nl, write(' For other solvers, num must be set to 1. Only the solvers listed above'), nl, write(' are capable of returning multiple models.'), nl. cchelp(dir) :- nl, write(' The \"dir\" option specifies the directory which contains the user\'s input'), nl, write(' files. When CCalc tries to load a file, it will first try the directory'), nl, write(' specified this option. If it fails to find the requested file there, it'), nl, write(' will then search other directories, including the current working directory'), nl, write(' and the CCalc installation directory. Thus, the user does not need to set'), nl, write(' this option if she simply changes to the correct directory each time she'), nl, write(' loads a file.'), nl. cchelp(timed) :- nl, write(' The "timed" option determines whether CCalc will display time messages.'), nl, write(' When it is set to \'true\', CCalc will report the time it takes for'), nl, write(' grounding, completion, and finding the solution. If the "compact"'), nl, write(' option is on, CCalc will also report the compaction time; and if the'), nl, write(' "verbose" option is on, CCalc will also report the time taken for some of'), nl, write(' the additional steps reported. When \"timed\" is set to \'false\', CCalc'), nl, write(' will not report any time information.'), nl. cchelp(verbose) :- nl, write(' The "verbose" option determines the amount of information CCalc produces'), nl, write(' when processing a command. If the option is set to \'false\', CCalc will'), nl, write(' provide minimal information. If it is set to \'true\', CCalc will provide'), nl, write(' additional information, such as reporting what it is doing at each step.'), nl, write(' If the "timed" option is also on, CCalc will report the time taken by'), nl, write(' some of these additional steps reported as well.'), nl. cchelp(file_io) :- nl, write(' The "file_io" option determines whether CCalc uses files or pipes to'), nl, write(' communicate with the SAT solver. When this option is set to \'false\', CCalc'), nl, write(' will use named pipes. When it is set to true, CCalc will use files'), nl, write(' ccsat.in, ccsat.out, etc.) instead. This allows the user to inspect the SAT'), nl, write(' solver\'s input and output, and is also useful if the user\'s system does not'), nl, write(' support the system calls CCalc uses to create the pipes.'), nl. /* temporarily (?) disabled *jc* cchelp(sorted) :- nl, write(' The \"sorted\" option determines whether CCalc sorts the clauses in the'), nl, write(' input file to the satisfiability solver. If the option is set to \'true\','), nl, write(' CCalc will sort the clauses in increasing order of the number of literals'), nl, write(' per clause. This may improve the performance of some satisfiability'), nl, write(' solvers, but usually has little effect, so the option is \'false\' by'), nl, write(' default.'), nl, nl, write(' Like all of the boolean-valued options, \'yes\', \'y\', and \'on\' are'), nl, write(' permitted in place of \'true\', and \'no\', \'n\', and \'off\' may be used'), nl, write(' instead of \'false\'.'), nl. */ cchelp(compact) :- nl, write(' Setting the "compact" option to \'true\' will cause CCalc to call'), nl, write(' James Crawford\'s "compact" program on the input file to the satisfiability'), nl, write(' solver. Compaction reduces the size of the theory by employing a \"failed'), nl, write(' literal rule\": for each literal L, if performing unit clause propagation'), nl, write(' on the union of the theory and {L} resolves to a contradiction, then the'), nl, write(' complement of L is added to the theory and unit clause propagation is'), nl, write(' performed on that literal. This can dramatically reduce the number of'), nl, write(' atoms and clauses in the theory passed to the satisfiability solver.'), nl, write(' If the option is set to \'false\', the input will not be compacted.'), nl. cchelp(optimize) :- nl, write(' When \"optimize\" is set to \'true\', CCalc will introduce new atoms'), nl, write(' during the clausification of rules, to avoid the combinatorial clause'), nl, write(' explosion that can result from distributing conjunction over disjunction'), nl, write(' or vice versa. This increases the number of atoms, but can greatly '), nl, write(' decrease the number of clauses and the computation time required to ground'), nl, write(' the input theory.'), nl. cchelp(eliminate_tautologies) :- nl, write(' When "eliminate_tautologies" is set to \'true\', CCalc will eliminate'), nl, write(' tautological clauses generated during completion rather than including them'), nl, write(' in the theory. This will generally lead to improved performance for the SAT'), nl, write(' solver, though sometimes leaving the tautologies in the theory may guide the'), nl, write(' solver\'s search in a beneficial way.'), nl.