Cython `cdef` classes without an explicit `__init__` constructor have an
implicit `__init__` that accepts any number of arguments. (Python
classes, by contrast, default to an `__init__` that takes no arguments.)
This can lead to confusing situations where arguments appear to be
accepted but are discarded. This PR fixes the issue by adding explicit
`__init__` methods to the Cython classes.
Additionally, this PR removes some unnecessary field initializations in
the Cython classes.
Due to previous refactoring, the SMT solver called by the SyGuS solver no longer answers unsat when the synthesis problem has a valid solution.
This PR makes it so that unsat from the underlying SMT solver is now interpreted as "infeasible" and is officially returned as such by the SyGuS solver. Note that we return unsat when e.g. a CEGIS refinement lemma is equivalent to false. On the other hand, we do not yet answer unsat when we run out of terms (e.g. for finite grammars), as this is still guarded. A followup PR will address this.
To make the SMT solver answer unsat for infeasible conjectures, we do not guard CEGIS lemmas with the "feasible guard", instead we use the conjecture itself, similar to quantifier instantiation lemmas.
This further removes the "feasible guard" from the internal sygus solver, which was used as a way to prevent unsat due to the infeasibility of CEGIS refinement lemmas.
Also extends to non-trivial unit test of SynthResult.
Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.
