UnknownExplanation

This enum class represents the explanation for an unknown solver result (see Result).

• enum class cvc5::UnknownExplanation

• std::ostream& cvc5::operator<< (std::ostream& out, UnknownExplanation e)

enum class cvc5::UnknownExplanation

The different reasons for returning an “unknown” result.

Values:

enumerator REQUIRES_FULL_CHECK

Full satisfiability check required (e.g., if only preprocessing was performed).

enumerator INCOMPLETE

Incomplete theory solver.

enumerator TIMEOUT

Time limit reached.

enumerator RESOURCEOUT

Resource limit reached.

enumerator MEMOUT

Memory limit reached.

enumerator INTERRUPTED

Solver was interrupted.

enumerator UNSUPPORTED

Unsupported feature encountered.

enumerator OTHER

Other reason.

enumerator REQUIRES_CHECK_AGAIN

Requires another satisfiability check

enumerator UNKNOWN_REASON

No specific reason given.

std::ostream &cvc5::operator<<(std::ostream &out, UnknownExplanation e)

Serialize an UnknownExplanation to given stream.

Parameters:

• out – The output stream

• e – The explanation to be serialized to the given output stream

Returns:

The output stream