SynthResult
This class represents a
cvc5::Solver
SyGus synthesis result.
-
class
SynthResult
-
Encapsulation of a solver synth result.
This is the return value of the API functions:
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.
-
std
::
string
toString
(
)
const
-
- Returns :
-
A string representation of this synthesis result.
-
SynthResult
(
)
-
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.