Cvc5UnknownExplanation

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

enum Cvc5UnknownExplanation

The different reasons for returning an “unknown” result.

Values:

enumerator CVC5_UNKNOWN_EXPLANATION_REQUIRES_FULL_CHECK

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

enumerator CVC5_UNKNOWN_EXPLANATION_INCOMPLETE

Incomplete theory solver.

enumerator CVC5_UNKNOWN_EXPLANATION_TIMEOUT

Time limit reached.

enumerator CVC5_UNKNOWN_EXPLANATION_RESOURCEOUT

Resource limit reached.

enumerator CVC5_UNKNOWN_EXPLANATION_MEMOUT

Memory limit reached.

enumerator CVC5_UNKNOWN_EXPLANATION_INTERRUPTED

Solver was interrupted.

enumerator CVC5_UNKNOWN_EXPLANATION_UNSUPPORTED

Unsupported feature encountered.

enumerator CVC5_UNKNOWN_EXPLANATION_OTHER

Other reason.

enumerator CVC5_UNKNOWN_EXPLANATION_REQUIRES_CHECK_AGAIN

Requires another satisfiability check

enumerator CVC5_UNKNOWN_EXPLANATION_UNKNOWN_REASON

No specific reason given.

enumerator CVC5_UNKNOWN_EXPLANATION_LAST

const char *cvc5_unknown_explanation_to_string(Cvc5UnknownExplanation exp)

Get a string representation of a Cvc5UnknownExplanation.

Parameters:

exp – The unknown explanation.

Returns:

The string representation.