Incremental search never stops when the solver answers unknown at every depth #113

Since #103, an unknown answer is no longer read as UNSAT. When nothing is found, synthesis() raises SolverError. Without --max-depth, though, the incremental search has no upper bound. A solver that answers unknown at every depth therefore makes MILQ try depth after depth forever, and that error is never reached. #103's description already mentions this.

Minimal example. Here is a fake solver that answers unknown to every (check-sat):

cat > always-unknown <<'X'
#!/bin/sh
while read -r line; do
  case "$line" in *check-sat*) echo unknown;; esac
done
X
chmod +x always-unknown
cat > solvers.toml <<'X'
[solvers.unknown]
path = "./always-unknown"
logics = ["QF_LIA", "QF_NRA"]
X

$ timeout 30 milq benchmarks/ghz/2.qasm -s smt -a unknown --solver-config solvers.toml -o out.qasm --verbose
...
[INFO][synth] Trying depth: 46
[INFO][synth] Trying depth: 47
$ echo $?
124

With a bound, it stops as intended:

$ milq benchmarks/ghz/2.qasm -s smt -a unknown --solver-config solvers.toml -o out.qasm --max-depth 3
synthesis failed: 4 solver call(s) answered unknown: no circuit found, but none was proven not to exist
$ echo $?
1

A real solver hits this too: yices2 2.7.0 doesn't answer some Classic queries in reasonable time (#55's CI), and SMTInterpol answers unknown to nonlinear terms.

Possible fixes:

1. When the input is a circuit whose gates are all in the gate set, bound the search by the input's gate count, since the input itself is a solution at that depth.
2. Otherwise, stop after some number of consecutive depths that all answer unknown, or require --max-depth once an unknown has been seen.

Found on master e5a5216.