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