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.