Encode unknown generic type parameters with (declare-forall-sort)

[coeff-aij]

This PR introduces an extension to SMT-LIB2 to encode unknown type parameters (like T in f<T: PartialOrd>()) as a universally quantified sort.

For example, a universally quantified sort a0 is first declared using (declare-forall-sort a0) and then used everywhere like a normal sort.
This feature lays the groundwork for the future verification of generic functions involving unknown types.

Example

• Input:

#[thrust_macros::context]
trait A {
    #[thrust_macros::requires(Self::p(x))]
    #[thrust_macros::ensures(Self::p(result))]
    fn f(&self, x: i64) -> i64;

    #[thrust_macros::predicate]
    fn p(x: i64) -> bool;
}

#[thrust_macros::requires(T::p(x))]
#[thrust_macros::ensures(T::p(result))]
fn target<T: A>(a: &T, x: i64) -> i64 {
    let mut v = x;
    let mut i = 0;
    while i < 3 {
        v = a.f(v);
        i += 1;
    }

    v
}

fn main() {}

• output:

(set-logic HORN)

(declare-forall-sort a0)

; span=refine_fn_def 
(declare-fun p0 (Int a0) Bool)

; span=refine_fn_def 
(declare-fun p1 (Int a0 Int) Bool)

... (snip)

[coeff-aij]

forall_sorts is actually redundant because we know it only contains the range 0..num_forall_sort_idx.