The Output Functions

All output is done in SLP be calling a function in this module. So this the only module which has to be changed, if messages in another language should be produced.

This module can produce HTML-output or ASCII-output, so SLP can run as a CGI-Program or can be directly called under UNIX (it also runs as a Windows Console application). The kind of output depends on the compile-time parameter VER_CGI. If this macro is defined during compilation, HTML output is produced, otherwise ASCII output. Of course, it would be possible to have both options compiled into the executable program, but CGI programs need additional security checks. So it would anyway not be possible to use the same binary as local command and as CGI-program.

Currently, this module is realized as a class out_c with lots of class functions. It is not possible to create instances of this class. This module contains only straightforward code. However, it is ensured that no function crashes if it gets a NIL-pointer for a string parameter.

Of course, open should be called before any of the other functions. However, the implementation is robust and calls open implictly if necessary.

open:

void open();
This function prints the HTML header (if VER_CGI is defined).

close:

void close(void);
If VER_CGI is defined, this function prints the HTML closing sequence.

assertion_failed:

static void assertion_failed(str_t filename, int line, str_t msg);
This function is called if it becomes obvious that the program contains a bug. It prints the given source filename and line number of the failed assertion, a short explanation msg, and a contact email address.

exception:

static void exception(int sig_no, str_t sig_name);
This function is called if the program received an exception like "segmentation violation". So there is not much difference to assertion_failed. The name and the number of the signal are printed (the name can be "unexpected signal" if no more specific name is available).

open_failed:

static void open_failed(str_t filename, str_t syserr);
This function is called, if the input file filename cannot be opened. syserr is the explanation returned by the operating system, e.g. "no such file or directory".

read_failed:

static void read_failed(str_t filename, str_t syserr);
This function is called in the unlikely case that a read operation failed.

close_failed:

static void close_failed(str_t filename, str_t syserr);
This function is called in the unlikely case that the operating system detected an error while closing an input file.

null_char:

static void null_char(str_t filename, int lineno);
This function is called if the input file contains a null character. Probably it is a binary file and not a text file. The processing will be terminated (the lexical scanner cannot handle null characters). If the filename is STR_NIL (e.g. for CGI-input), only the line number is printed.

line_too_long:

static void line_too_long(str_t filename, int lineno);
This function is called if the input file contains a very long line. This situation can also not be handled by the lexical scanner. Again, if the filename is STR_NIL (e.g. for CGI-input), only the line number is printed.

mem_limit:

static void mem_limit(int max_kilobytes);
The memory manager has currently a fixed limit of the number of memory blocks it can allocate. If more memory is needed, this function is called and then the program is terminated. The parameter max_kilobytes contains the current limit of the memory manager.

insufficient_memory:

static void insufficient_memory(int allocated_kilobytes);
This function is called if the operating system has no more memory, i.e. a call to malloc has failed. The parameter allocated_kilobytes contains the size of the already allocated dynamic memory.

too_many_args:

static void too_many_args(void);
The program was called with too many command line arguments. Currently, it can process only 0 or 1 arguments.

too_many_head_lit:

static void too_many_head_lit(int max);
A rule or conditional fact generated during the computation had more head literals than would fit into an array used in the program. This is a fatal error. However, one can set the constant VER_MAX_HEAD_LIT in ver.h higher, recompile the program, and try it again. The parameter max is the current setting for VER_MAX_HEAD_LIT. The reason why I used a fixed size array here is that generated conditional facts must first be tested for redundancy, and often they will be immediately thrown away. I felt that this is not worth the effort of dynamic memory management, or at least it can be deferred to a later version. The decision is not so clear, because a conditional fact may also later turn out to be redundant.

too_many_cond_neg:

static void too_many_cond_neg(int max);
A rule or conditional fact generated during the computation had more default negations than would fit into an array used in the program. This is a fatal error. However, one can set the constant VER_MAX_COND_NEG in ver.h higher, recompile the program, and try it again. The parameter max is the current setting for VER_MAX_COND_NEG.

too_many_neg_lit:

static void too_many_neg_lit(int max);
A rule or conditional fact generated during the computation had more default negations or literals inside default negations than would fit in an array used in the program. This is a fatal error. The size is controlled by VER_MAX_NEG_SIZE in ver.h and should be easy to change. The parameter max is simply the current setting for VER_MAX_NEG_SIZE. Note that each default negation counts one and each negated literal also counts one. So if the max is e.g. 256, there could be at most 128 default negations of one literal each.

too_many_compar:

static void too_many_compar(long max);
In order to find duplicate literals in default negations and conditional fact heads and duplicate default negations in conditional fact bodies, the value of a counter is stored in each literal/negation used. If this counter may not overflow, so at least then the program is aborted (although it might be possible to reset all counters in literals and default negations to 0 and start again from 1). However, limiting the possible values of the counter (i.e. the number of duplicate checks) is also a method for excluding very difficult inputs that would take a lot of CPU time. This is e.g. important when this program is used via a web interface. The maximal value for the counter is VER_MAX_COMPAR in ver.h and should be easy to change. The parameter max is simply the current setting for VER_MAX_COMPAR.

too_many_crit_neg:

static void too_many_crit_neg(int max);
The residual program contained too many distinct default negations. The algorithm used after the computation of the residual program is unfortunately more than exponential in this number (it considers all possible interpretations of these default negation literals and computes minimal models for each). The current implementation is restricted to 32 (the number of bits in a long int), but it might be sensible to further restrict it (at least for the web-interface). The size is controlled by VER_MAX_CRIT_NEG in ver.h and should be easy to change (up to the limit of 32). The parameter max is simply the current setting for VER_MAX_CRIT_NEG.

backtrack_point_stack_overflow:

static void backtrack_point_stack_overflow(int max);
There was a stack overflow for the backtrack point stack in the model generator. The stack size is VER_BACKTRACK_POINTS in ver.h and should be easy to change. The parameter max is simply the current setting for VER_BACKTRACK_POINTS.

comp_ax_too_large:

static void comp_ax_too_large(int max);
The current implementation of the stable model semantics generates Clark's completion of the residual program. The completion axioms generated for a fact p contains one literal from each conditional fact in which p appears in the head. A array of size VER_MAX_CAX_LIT is used during the generation of the completion axiom. This message is printed when the array is too small, i.e. a fact appears in too many conditional facts. The array size VER_MAX_CAX_LIT is defined in ver.h and should be easy to change. The parameter max is simply the current setting for VER_MAX_CAX_LIT. This function is only defined if VER_SEM_STABLE is defined.

cgi_security:

static void cgi_security(str_t filename);
When this program is compiled for use as a CGI-program, it checks that only a given selection of files can be opened. For instance, it would be bad, if a hacker would try /etc/passwd. This error message is printed if the input file is not allowed.

bad_request_method:

static void bad_request_method(void);
The program was compiled in CGI-mode, but the environment variable REQUEST_METHOD is either not defined or doesn't have the value "POST".

bad_content_type:

static void bad_content_type(void);
The program was compiled in CGI-mode, but the environment variable CONTENT_TYPE is either not defined or doesn't have the value "application/x-www-form-urlencoded".

bad_content_length:

static void bad_content_length(void);
The program was compiled in CGI-mode, but the environment variable CONTENT_LENGTH is either not defined or is not a non-negative number.

bad_cgi_hex:

static void bad_cgi_hex(void);
The program was compiled in CGI-mode, but the input was not correctly CGI-encoded: A percent sign was not followed by two hexadecimal digits.

cgi_premature_eof:

static void cgi_premature_eof(void);
The end-of-file was reached in the standard input before CONTENT_LENGTH characters were read. This violates the CGI specification.

cgi_null_char:

static void cgi_null_char(void);
The input to the CGI program contained a null character (either directly or encoded). The CGI specification allows an encoded null character ("%00"), but SLP cannot work with null characters in the input.

cgi_field_not_terminated:

static void cgi_field_not_terminated(void);
The input to a CGI-program is a sequence of name/value pairs. Each name must be terminated by a `=', but this was not found.

cgi_duplicate_program:

static void cgi_duplicate_program(void);
More than one program-field was contained in the CGI input.

cgi_no_program:

static void cgi_no_program(void);
No program-field was contained in the input.

These functions are used to print lines from the user's input file (usually in syntax error messages). The main purpose is to switch to <pre> if we are running as a cgi-program.

show_input:

static void show_input(void);
This function starts the printing of a line of code.

show_char:

static void show_char(char c);
This function prints a single character. show_input must have been called before.

show_newline:

static void show_newline(void);
This function prints a newline. It is only needed if more than one line of code should be printed (which is the case in the current error message format, because in the second line a marker for the current input position will be printed).

show_eof:

static void show_eof(void);
This function prints the "end of file" marker.

show_end:

static void show_end(void);
This function ends the printing of code.

err_begin:

static void err_begin(void);
This function is called once before the first syntax error message. In CGI mode, it starts an unordered list. It could also print a headline like "Syntax Errors".

err_end:

static void err_end(int num_errs);
This function is called when parsing is complete if errors were printed, i.e. if err_begin was called earlier. In CGI mode, it closes the unordered list. It can also print a summary: num_errs is the number of errors. The value -1 means that there were too many errors, so the parsing was aborted.

err_syntax:

static void err_syntax(str_t file, int line, out_syn_t msg);
This function prints syntax error message. It does not print the newline after the message, this must be done by calling err_newline (see below). In this way, arguments of the error message can be added. After err_newline, ussually the show-functions are called to print the current input line. The parameter msg determines the detailed message for a syntax error, e.g. "term expected". Since there are quite a lot of different such messages, there is an enumeration type for syntax error messages defined in this module (remember that all other modules, including the parser, should be language-independent). The enumeration type out_syn_t has the following values:

• OUT_ILLEGAL_CHAR: "Illegal character"
• OUT_BAD_LESS: "< is only legal as first character of <-"
• OUT_BAD_GREATER: "> is only legal in -> or <->"
• OUT_BAD_MINUS: "- must be followed by > or digits"
• OUT_MISSING_QUOTE: "Missing quote (quoted atom is not closed)"
• OUT_EMPTY_ATOM: "The empty atom is not allowed"
• OUT_MISSING_SPACE: "A space or newline is required after '.'"
• OUT_INT_OVERFLOW: "Integer constant too large"
• OUT_RESERVED_PRED: "Illegal use of reserved predicate"
• OUT_EMPTY_CMD: "Illegal empty command"
• OUT_UNKNOWN_CMD: "Unknown command"
• OUT_PRED_EXPECTED: "Atom (predicate) expected"
• OUT_TERM_EXPECTED: "Term (predicate argument) expected"
• OUT_COMMA_OR_RPAREN_EXPECTED: "',' or ')' expected"
• OUT_ARGLIST_BINOP_OR_FULLSTOP_EXPECTED: "Argument list/binary operator/'.' expected"
• OUT_ARGLIST_BINOP_OR_RPAREN_EXPECTED: "Argument list/binary operator/')' expected"
• OUT_RPAREN_EXPECTED: "')' expected"
• OUT_BINOP_OR_RPAREN_EXPECTED: "Binary operator or ')' expected"
• OUT_BINOP_OR_FULLSTOP_EXPECTED: "Binary operator or '.' expected"
• OUT_FORMULA_EXPECTED: "Formula expected"
• OUT_FORMULA_OR_VARLIST_EXPECTED: "Query formula or variable list expected"
• OUT_COMMA_OR_COLON_EXPECTED: "Comma or colon expected"
• OUT_VAR_EXPECTED: "Variable expected"
• OUT_STACK_OVERFLOW: "Formula too complicated, operator stack overflow"
• OUT_OPERATOR_NOT_ASSOCIATIVE: "Operator not associative, use parentheses"
• OUT_NOT_CANNOT_BE_NESTED: "Default negation cannot be nested"
• OUT_OP_ILLEGAL_WITHIN_NOT: "Only & and | can be used inside default negation"
• OUT_ANON_WITHIN_NOT: "Anonymous variables are not allowed inside not"
• OUT_NO_OPS_INSIDE_NOT: "With $a, not can be applied only to atoms" (defined only for VER_SEM_STABLE)
• OUT_OPS_INSIDE_NOT_WERE_USED: "not was already applied to structured formulas" (defined only for VER_SEM_STABLE)
• OUT_FULLSTOP_EXPECTED: "Fullstop expected ('.' followed by white space)"
• OUT_TOO_MANY_VARS: "Too many non-anonymous variables in formula"
• OUT_TOO_MANY_ARGS: "Too many arguments of atomic formula (literal)"
• OUT_OVERFLOW_DURING_CONVERSION: "Array overflow during conversion into clause form"
• OUT_TOO_MANY_HEAD_LITS: "Clause contains too many head literals"
• OUT_TOO_MANY_BODY_LITS: "Clause contains too many positive body literals"
• OUT_TOO_MANY_NEG_LITS: "Clause contains too many/too large default negations"
• OUT_ONLY_ONE_QUERY_PERMITTED: "The input can contain only one query"

err_note_v:

static void err_note_v(void);
It happened to me several times that I got a syntax error because I used "v" as a normal atom (e.g. as a predicate) although it is actually a reserved word and means disjunction. Therefore I decided to add a special note to syntax error messages if the current token is the reserved word "v". This note is printed by err_note_v.

err_anon_head:

static void err_anon_head(str_t filename, int line_no);
This function prints an error message for anonymous variables in head literals. The printed text ends with a colon and without a newline. It is expected that the offending literal will be printed next followed by a call to err_newline.

err_neg_head:

static void err_neg_head(str_t filename, int line_no);
This function prints an error message for default negation used in the head (i.e. in positive context). The printed text ends with a colon and without a newline. It is expected that the offending negated formula will be printed next followed by a call to err_newline.

err_unbound_var:

static void err_unbound_var(str_t filename, int line_no);
This function prints an error message for unbound variables, i.e. variables which do not appear in a positive body literal. Such variables violate the allowedness/safety/range-restriction condition which allows grounding of the program without depending on the domain. The printed text ends with a colon and without a newline. It is expected that the offending variables will be printed next followed by a call to err_newline.

err_newline:

static void err_newline(void);
This function prints the fullstop and newline after a syntax error message which was printed with err_syntax (see above). The two functions are divided because some syntax error messages have parameters (such as a head literal containing anonymous variables). These parameters cannot be directly passed to functions of the module out_c since this would generate cycles in the dependency relation between the modules.

err_input_empty:

static void err_input_empty(void);
This function is called at the end of the parsing step if there were no syntax errors, but still not a single formula was read.

The functions in this section are used for printing data, e.g. formulas. Data originates from the input, and does not have to be translated if SLP is translated to another language. So it would be a mistake to use the following functions for printing error messages etc.

print_str:

static void print_str(str_t str);
This prints the null-terminated string str. In CGI mode, the characters < >, and & are replaced by the corresponding entity references.

print_char:

static void print_char(char c);
This prints the character c. In CGI mode, the characters < >, and & are replaced by the corresponding entity references.

print_int:

static void print_int(int i);
This prints the integer i.

print_bool:

static void print_bool(int b);
This prints the boolean value b (true or false).

print_nl:

static void print_nl(void);
This starts a new line in the output.

input_formulas:

static void input_formulas(void);
This prints a headline "Input Formulas:" for echoing the parsed input.

list_begin:

static void list_begin(void);
This begins an unordered list (e.g. for the input formulas). In CGI-Mode, it prints "<UL>". In normal mode, it does nothing.

list_item:

static void list_item(void);
This function should be called at the beginning of each list item. In CGI-Mode, it prints "<LI>". In normal mode, it does nothing.

list_end:

static void list_end(void);
This ends the list which was started with list_begin. In CGI-Mode, it prints "</UL>". In normal mode, it does nothing.

initial_cond_facts:

static void initial_cond_facts(void);
This prints the headline "Initial Set of Conditional Facts".

hyperres_verbose:

static void hyperres_verbose(void);
This prints the headline "Hyperresolution (Verbose Output):".

hyperres_round:

static void hyperres_round(int round);
This prints the subheadline (i.e. H3) "Hyperresolution - Iteration Round n:", where n is replaced by the value of the parameter round. It is used in the verbose output for the hyperresolution.

no_match:

static void no_match(void);
This is called during the verbose hyperresolution output if no rule was applied in this hyperresolution round (i.e. no new matching facts were found). It prints the text "(no match found)".

hyperres_curr_cf:

static void hyperres_curr_cf(void);
This prints the subheadline (i.e. H3) "Current set of conditional facts:". It is used in the verbose output for the hyperresolution.

hyperres_fixpoint:

static void hyperres_fixpoint(void);
This prints the headline "Implied Conditional Facts (Hyperresolution Fixpoint)".

residual_program:

static void residual_program(void);
This prints the headline "Residual Program".

no_cond_facts:

static void no_cond_facts(void);
Inform the user that the set of conditional facts is empty. In CGI mode, the text is printed bold (STRONG).

rules:

static void rules(void);
This prints the headline "Rules".

no_rules:

static void no_rules(void);
Inform the user that the set of rules is empty. In CGI mode, the text is printed bold (STRONG).

no_default_neg:

static void no_default_neg(void);
Inform the user that the set of default negations is empty. In CGI mode, the text is printed bold (STRONG).

no_disjunctions:

static void no_disjunctions(void);
The set of model generator disjunctions is empty (no disjunctions remain to be satisfied). In CGI mode, the text is printed as an unodered list in order to make it look like the other sets of disjunctions.

inconsistent:

static void inconsistent(void);
The set of model generator disjunctions contains the empty clause FALSE (i.e. is inconsistent). In CGI mode, the text is printed as an unodered list in order to make it look like the other sets of disjunctions.

empty_defneg_interpretation:

static void empty_defneg_interpretation(void);
This function is called when an interpretation of the critical default negations has to be printed and there are no critical default negations. This is no error, but there is only one empty interpretation. Probably the computation will be stopped earlier, so this function will never be called, but I thought it would be safer to handle this case somehow ("Defensive Programming").

fixpoint_computation:

static void fixpoint_computation(int round);
This prints a headline for each round of the fixpoint computation of the static semantics (interpretations for default negations). The current text is "Fixpoint Computation - Round (round):". In HTML mode, it is a second level headline.

fixpoint_case:

static void fixpoint_case(int no);
This prints a headline for each default negation interpretation for which minimal models are computed. The current text is "Case (no):". In HTML mode, it is a third level headline.

result:

static void result(void);
This prints a headline at the end of each round of the fixpoint computation before all still possible default negation interpretations are listed. The current text is "Result:". In HTML mode, it is a third level headline.

defneg_interpretation:

static void defneg_interpretation(void);
This prints the text "Default Negation Interpretation:".

disjunctions:

static void disjunctions(void);
This prints the text "Disjunctions:". It is used in the output for the fixpoint computation of the static semantics.

minimal_model:

static void minimal_model(void);
This prints the text "Minimal Model for Critical Facts:". It is used in the output for the fixpoint computation of the static semantics.

no_min_mod:

static void no_min_mod(void);
This prints the text "The set of minimal models is empty.". It is used in the output for the fixpoint computation of the static semantics.

static_fixpoint:

static void static_fixpoint(void);
This prints the text "Static Interpretations for Critical Negations:". It is called when the main fixpoint computation of the static semantics is finished. In CGI mode, it is printed as a second level headline.

completion:

static void completion(void);
This prints the headline for Clark's completion, which is used for computing stable models. In CGI mode, it is printed as a second level headline. This function is defined only if VER_SEM_STABLE is defined.

stable_models:

static void stable_models(void);
This prints the headline for the list of stable models. In CGI mode, it is printed as a second level headline. This function is defined only if VER_SEM_STABLE is defined.

stable_model_no:

static void stable_model_no(int no);
This prints the subheadline for the n-th stable model. In CGI mode, it is printed as a third level headline. This function is defined only if VER_SEM_STABLE is defined.

all_facts_are_false:

static void all_facts_are_false(void);
This prints "All ground literals are false." This function is defined only if VER_SEM_STABLE is defined.

no_stable_models:

static void no_stable_models(void);
This prints the text "This program has no stable models". It is called if the stable semantics is inconsistent, but the given input program is not logically inconsistent. In CGI mode, it is printed as a third level headline. This function is defined only if VER_SEM_STABLE is defined.

prompt:

static void prompt(void);
This function prints a prompt during interactive input from the keyboard ("SLP> "). Currently, there is only one prompt, but later we should make a difference whether a new command is expected or a continuation for an incomplete command.

input_is_inconsistent:

static void input_is_inconsistent(void);
A logical inconsistency was detected. The text "Input is inconsistent." is printed as a second-level headline.

static_is_inconsistent:

static void static_is_inconsistent(void);
The residual program is inconsistent or the static fixpoint computation ended up with the empty set. The program is not logically inconsistent, but the static semantics of it is inconsistent. The text "Program is inconsistent under the Static semantics." is printed as a second-level headline.

answer:

static void answer(void);
This is the headline for printing the query answer.

not_provable:

static void not_provable(void);
No answer was found. The text "Not provable." is printed in boldface.

yes:

static void yes(void);
This is the positive answer to a boolean query. The text "Yes (query proven)." is printed in boldface.

print_or:

static void print_or(void);
This prints the string " or " between parts of a disjunctive answer.

• Header File (out.h)
• Source File (out.cxx)