recfun decl plugin does not get copied so recursive functions are lost when cloning.
Fix is risky and use case is limited to threads + recursive definitions
Adding new API object to maintain state between calls to parser.
The state is incremental: all declarations of sorts and functions are valid in the next parse. The parser produces an ast-vector of assertions that are parsed in the current calls.
The following is a unit test:
```
from z3 import *
pc = ParserContext()
A = DeclareSort('A')
pc.add_sort(A)
print(pc.from_string("(declare-const x A) (declare-const y A) (assert (= x y))"))
print(pc.from_string("(declare-const z A) (assert (= x z))"))
print(parse_smt2_string("(declare-const x Int) (declare-const y Int) (assert (= x y))"))
s = Solver()
s.from_string("(declare-sort A)")
s.from_string("(declare-const x A)")
s.from_string("(declare-const y A)")
s.from_string("(assert (= x y))")
print(s.assertions())
s.from_string("(declare-const z A)")
print(s.assertions())
s.from_string("(assert (= x z))")
print(s.assertions())
```
It produces results of the form
```
[x == y]
[x == z]
[x == y]
[x == y]
[x == y]
[x == y, x == z]
```
Thus, the set of assertions returned by a parse call is just the set of assertions added.
The solver maintains state between parser calls so that declarations made in a previous call are still available when declaring the constant 'z'.
The same holds for the parser_context_from_string function: function and sort declarations either added externally or declared using SMTLIB2 command line format as strings are valid for later calls.
remove option for uzers (users who are in reality fuzzers) to toggle flat option. The legacy arithmetic solver bakes in assumptions about flat format so it isn't helpful to expose this to fuzzers, I mean uzers.
* make JS api more idiomatic
* make JS api type-safe by default
* use strings, not symbols, for results
* add toString
* add miracle sudoku example
* ints should be ints
* add error handling
* add missing Cond to Context
* fewer side-effecting getters
