different CN/solver interaction for SMT counter models

[cp526]

CN used to create a new solver instance for each model. This means solver models can be passed around as values and interacted with later, but also complicates the Solver module. With this change, CN models are just references to the current solver state (so creating a model no longer creates a new solver instance). This means the timing of when CN queries the model matters, and type error reports including countermodel information have to be produced when the model is still "live". This change temporarily disables the CheckPredicates logic, which relies on asking new solver queries, which then override the present model -- to be fixed.

[cp526]

The remaining problem is lazy variable declarations in the translation of expressions.

CN's original SMT solver module was based on the Z3 OCaml api, which allowed creating SMT expressions without first declaring the sorts and variables involved in the expression. The current smtlib-based interface still has this flavour, meaning CN creates SMT expressions and lazily declares variables as needed.

For this current PR this creates a problem when CN has asked the solver for a model ((get-model)) and subsequently translates an expression that requires (lazy) declaration of new variables: a (declare-fun ...) following (get-model) "breaks" the model in CVC5 (though z3 seems to tolerate this).

[cp526]

For addressing this we should have CN explicitly declare variables in the SMT problem when they are added to the proof context rather than relying on lazy declarations during expression translation.

However, it is less clear how to translate default: in the absence of support for polymorphic functions in current SMT solvers, default<bt> is now translated to a unique uninterpreted constant for each basetype bt; for doing this without lazy declarations we might need a global scan that lists, ahead of solving-time, all the base types in the problem.