Skip to content

Printing should conform to current output mode #731

@mezpusz

Description

@mezpusz

Vampire supports multiple output modes for CASC, SMTCOMP, etc. that have their own rules about extra (non-proof) lines in the output.

We should make sure that these rules are followed when outputting e.g. warnings, errors, stats, and so on.

For example, in TPTP output mode, every non-proof line should start with % to indicate that it is a comment and the various systems in the TPTP ecosystem won't try to interpret these lines.

The task is to make a wrapper for printing that knows about the current output mode, use this wrapper everywhere, and maybe even ban any other printing in the future.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions