Error MessagesNuts And Bolts

When you hit the SOLVE button, sometimes you get a solution but sometimes you get an error message. There is a great variety of possible errors, and the messages reporting them can be quite obscure. Here are a few remarks on the various error messages and what to do about them. If you really get stuck with an incomprehensible execution failure, go through the following steps:

1. Take a break: go for a walk; eat; sleep; whatever. Then see whether the problem is still impenetrable when you return to it.
2. Ask a friend to check it out. Friendship is a Good Thing, especially when it comes to debugging. If you are in a class of students, you might also ask around to see whether anyone else has relevant experience.
3. If there is still no progress, “Ask John”, using the web form accessible from the front page of this site. Include enough detail to allow the difficulty to be reconstructed – a dump of your input produced by the SAVE button is especially useful. You must also include a return email address, for obvious reasons.

There is a small collection of the more cryptic error messages, with explanations and diagnostics, here.

The possible error messages are as follows:

XXX found where key word … expected
There is a syntax error in the input. Probably there is an extra or missing brace “}” or “{“, or else a misplaced hash (#) character. First thing to try: examine the places where braces are supposed to occur, make sure they do occur and that they match in pairs.

Warning: Passed clause is trivially satisfiable.
Warning: Input clause is trivially satisfiable.
These cannot happen! Report a bug if they do.

Warning: Consequents should be separated by semicolon, not comma
Warning: Antecedents should be separated by comma, not semicolon
Two possibilities: either you have used “;” or “,” on the wrong side of the arrow in a clause, or else something went wrong earlier – usually a missing “.” at the end of the previous clause. Remember that you are not allowed to use “,” in clauses without an arrow.

Included filename must be in parentheses
Cannot open file XXX
Unable to open file XXX
These should not happen. Send email to the author or fill in the bug report form, exactly describing your input, because you have found a bug in the CGI program.

XXX found where integer expected
What it says. There are not many places where the solver expects an integer. One of them is in the cardinality specification of a sort. If it isn’t obvious what has gone wrong, ask a friend to look at your code. If it still isn’t obvious, Ask John.

Missing right parenthesis
Not much to offer in the way of hints about that one!

XXX doubly defined as a sort and a functor
[The program thinks] you are trying to define a function (in the “Vocabulary” box) with the same name as a sort you have already defined (in the “Sorts” box). It shouldn’t be too hard to work out why it thinks that!

XXX given too many argument places
There is a maximum number of arguments a predicate or function can have. In practice, for the logical puzzles, you never need more than three argument places, and very rarely more than two. Unless you really are trying to define a function with a silly number of arguments, the error may be something else really, like missing parentheses or wrong punctuation.

XXX both a variable and a functor
Something has really screwed up if you get this error message. It exists in the source code of the solver, but I have never seen it happen. Ask John.

Injective/surjective/all_different applied to 0-adic function XXX
Row/column injective/surjective applied to non-binary function XXX
You are not allowed to specify symbols as all_different, etc unless they have at least one argument, and some exotic specifications like “left_injective”, “column_bijective”, etc only apply to binary functions.

“,” found where “.” expected
“->” found where “.” expected
“;” found where “.” expected
This is usually seen when working in FOF form, if you have apparently tried to write a multi-literal clause.

Apparently nested arrows in clause
The arrow used to separate antecedents from consequents in a clause may not occur twice in the same clause. Note that the syntax of IMP in first order formulae is different. Check that you didn’t write “->” where you intended to write “→”.

Too many formulae parsed
Clause is too long
There appears to be a clause with thousands of formulae in it. Unless you have done something silly, this is unlikely to be the case, so you may have found a bug. If you can’t see why the solver thinks one of your clauses is ridiculous, Ask John.

Job too big: too many values for too many variables
Each decision variable (e.g. each tuple of arguments for a defined function) has an associated domain of possible values. Each variable-value pair is represented in the solver by a data structure requiring upwards of 100 bytes, and sometimes thousands of bytes. This memory is used even if you add a clause saying the variable does not have that value. For boring reasons of resource management, there is a hard upper limit to the number of variable-value pairs allowed. All problems on the site can be solved well within this limit. If you can’t see how to reduce the size of your job, Ask John.

XXX found where a function symbol was expected
XXX found where a binary operator was expected
Problem in parsing a clause. The parser makes one pass (only) through the clause, from left to right, and reports an error as soon as it encounters a symbol that does not make sense. First things to try: check syntax (commas, parentheses, etc) in the bit to the left of the error; count the number of arguments given to functions; check that the function symbols have all been defined; check that you have not used a sort name in place of a function symbol; check spelling. Spelling errors are the usual culprits, in fact: if you make a typo in a function symbol, the parser may think it is a name, and if a (sub)formula starts with a name, the next symbol can only be a binary operator.

XXX found where a right parenthesis was expected
Why did the parser expect a right parenthesis? [It thinks that] it has just read something of the form “( term binary_operation term “ or else of the form “operation ( term, …, term “. There may be a punctuation error somewhere, or you may have given the operation the wrong number of arguments.

XXX starts numerically but isn’t a number
If a word starts with a numerical digit, it had better be a numeral. Sorry, that’s just the way the language is!

XXX found where a left parenthesis was expected
The arguments of a function should be enclosed in parentheses, except in the case of a binary symbol in infix position. The parser has found a function or predicate symbol apparently in prefix position followed by something other than an opening (left) parenthesis. Well, check your syntax.

XXX found where a comma was expected
Pretty self-explanatory. Commas are used inside formulae to separate the arguments of functions and predicates. [The parser thinks that] one has been omitted. Make sure your functions and predicates have the expected number of arguments. Check spelling.

Missing type for XXX
May be a complicated error. After parsing each clause, the program has to go through it assigning sorts to the variables and so on. For some reason it has failed to do so because the sort of the expression in question cannot be deduced from its position in the formula. This is very unlikely in logical puzzles, except that sometimes MIN and MAX without subscripts can give rise to it. If you get this error message and can’t see what is wrong, Ask John.

Type mismatch with argument of XXX
Type mismatch: arguments of XXX
These are much more likely. Some symbol appears to have been given arguments of the wrong sort according to the type declaration it was born with. One common cause of this error is relying on scope conventions to sort out nested infixed binary operators. Try putting parentheses around everything binary (such as identity statements).

FN_MAX exceeded: too many functors!
VARMAX exceeded: too many variables!
You cannot be serious!

Clause contains no user-defined vocabulary
Every clause should contain at least one occurrence of a symbol defined in the “Vocabulary” box. Otherwise there is nothing the solver can do with the clause, so it prints a warning message. You should try to get rid of the offending constraint and replace it with something more useful. Note that the clausifier can sometimes produce clauses without user-defined vocabulary, even if your input looks sensible, so you may need to refer to the page on clause form reduction to understand the issue.

Incorrectly defined addition function XXX
Incorrectly defined subtraction function XXX
It is nearly impossible to get these messages to appear using the input format enforced by the web form. If you do manage it, well, congratulations: now try writing something less weird!

Aborting on detection of an error…
If the message starts with this incantation, the error was not trapped by the parser and so forth, but caused the solver to crash somehow. Some of the reasons it gives for having crashed are a bit cryptic, but anyhow:

Too many clauses (whew!)
Too many refutations requested
Too many formulas parsed
Too many surjections
Hard limits have been reached. There is no way you should ever see this happen if you are just doing the problems on the puzzle pages. Like many things that should never happen, they may sometimes happen. There is little to be done about it, except to write an encoding without thousands of constraints or whatever!

Attempt to search null space
The solver has been called without a problem to solve. This usually means you have not defined any vocabulary. It does something quite different if asked to solve the null problem (with no constraints) and different again if asked to solve an inconsistent problem (with no solutions).

Ghost in the back field
There is a ghost in the back field! Ask John.

Incorrect sort name transfer
Incorrect function name transfer
These do not apply when the solver is run from the web page. Report a bug if you get one of them.

Constraint is non-Horn
Bad vector position reported
Bad pointer sequence in a clause
Strange verbosity setting
Null refutation
Refutation cardinality not correctly set
Error in refutation
Nonexistent value removed by 1-refutation
Used not reset
Block without back
Back without block
These report bizarre goings-on inside the solver and are almost certainly not your fault. Report a bug if you get any of them, since they mean that something needs to be fixed deep inside the reasoning software.

Not Found: The requested URL XXX was not found on this server.
The problem is with the web server. Not my department (probably). If it persists, report it.

Document contains no data
The solver appears to have crashed before managing to write anything to your web browser. Since it is supposed to crash gracefully once it starts reading input, that means something has fallen over at the system level of the web site. Shouldn’t happen, of course. I bet you are shocked: isn’t that the first time you ever heard of anything actually going wrong with a computer!!! Once again, if the problem persists, report it.