UnknownExplanation ¶

enum 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 UNKNOWN_REASON ¶

No specific reason given.