SynthResult 

This class represents a cvc5::Solver SyGus synthesis result.

• class cvc5::SynthResult

• std::ostream& cvc5::operator<< (std::ostream& out, const SynthResult& r)

class SynthResult 

Encapsulation of a solver synth result.

This is the return value of the API functions:

• Solver::checkSynth()

• Solver::checkSynthNext()

which we call “synthesis queries”. This class indicates whether the synthesis query has a solution, has no solution, or is unknown.

Public Functions

SynthResult ( ) 

Constructor.

bool isNull ( ) const 

Determine if a given synthesis result is empty (a nullary result) and not an actual result returned from a synthesis query.

Returns :

True if SynthResult is null, i.e., not a SynthResult returned from a synthesis query.

bool hasSolution ( ) const 

Returns :

True if the synthesis query has a solution.

bool hasNoSolution ( ) const 

Returns :

True if the synthesis query has no solution. In this case, it was determined that there was no solution.

bool isUnknown ( ) const 

Returns :

True if the result of the synthesis query could not be determined.

bool operator == ( const SynthResult & r ) const 

Operator overloading for equality of two synthesis results.

Parameters :

r – The synthesis result to compare to for equality.

Returns :

True if the synthesis results are equal.

bool operator != ( const SynthResult & r ) const 

Operator overloading for disequality of two synthesis results.

Parameters :

r – The synthesis result to compare to for disequality.

Returns :

True if the synthesis results are disequal.

std :: string toString ( ) const 

Returns :

A string representation of this synthesis result.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const SynthResult & r ) 

Serialize a SynthResult to given stream.

Parameters :

• out – The output stream.

• r – The result to be serialized to the given output stream.

Returns :

The output stream.