We want the search component to accept a less restrictive format of .sas files as input.
- Allow variables with just one domain value.
- Components need not be sorted by variable, see also issue1158.
- Support trivially solvable and unsolvable tasks, see issue1160.
- Allow operators with no effect.

This involves updating three different "specifications" of the file format:

- the quite strict definition in src/translate/sas_tasks.py (comments and assertions, I think)
- the public documentation in docs/translator-output-format.md
- what is checked by the search component in src/search/tasks/root_task.{h,cc}

We didn't add a motivation for this, so let me do this for the record:

We have discussed two conflicting viewpoints of what the translator output format is. 

In the old view, it was an internal file format not meant to be used externally, and therefore the main considerations were simplicity and efficiency of code. Hence considerations that make the implementation simpler and/or allow us to use sometimes useful assumptions in the search code, such as: all conditions appear in sorted order, there is at least one goal.

But then more and more people started using the file format for other purposes, and for this it would make a lot more sense for the file format to be more convenient (for example not requiring sorting) and reflect the full generality of how one would mathematically define these planning tasks (for example in our formal definitions it is certainly possible to have 0 goals).

We have now shifted from the first viewpoint to the second in terms of what we *want*, but the implementation and various specifications (on the Fast Downward website, in the assertions in the translator, in the checks in the search code) are still largely based on the first viewpoint.

This issue is about changing this, so that we follow the second viewpoint.

Thanks for starting this.

Now that we've started going down this path, I think we should remove all restrictions that don't have a strong justification.

Other examples of restrictions without strong justification are not allowing duplicate conditions, requiring conditions to be grouped by variable and not allowing contradictory conditions. (You mention dropping this restriction for the goal, but I would then also drop it for preconditions, effect conditions and axioms.)

An example of a justified restriction is the semantic restriction that mutexes must indeed be mutexes because we cannot efficiently verify this.