UnknownExplanation

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



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

std :: string std :: to_string ( cvc5 :: UnknownExplanation exp )