Support defining predicates using #[thrust::predicate] attribute with fn statements

[coeff-aij]

This feature recognizes functions annotated with #[thrust::predicate] as predicates and inserts corresponding define-fun definitions—derived from their names and arguments—into the .smt2 file. The first string literal that appears in a function's body is inserted as the predicate body.

Compared with #![thrust::raw_command], Thrust can assign a predicate name automatically and later leverage that name to connect the predicate to relevant traits(for example, SomeTrait::pred -> (define-fun some_trait_pred)).

• Example

If a user writes the following:

#[thrust::predicate]
fn is_double(x: i64, doubled_x: i64) -> bool {
    "(=
        (* x 2)
        doubled_x
    )"; true
}

the appropriate definitions are inserted into the .smt2 file.

(define-fun is_double ((x Int) (doubled_x Int)) Bool (=
        (* x 2)
        doubled_x
    ))

[coord-e]

I think it's natural to use a String directly here, as RawCommand shouldn't serve a different purpose

Suggested change

	body: RawCommand,
	body: String,

[coeff-aij]

I fixed.

[coeff-aij]

I added more details to the PR description.

[coeff-aij]

I think raw‑command definitions and user‑defined predicates should be emitted before the datatype declarations in the generated .smt2 file.

The reason is that raw commands and predicates written by users may refer to previously declared datatypes(ex. access fieleds of structs), whereas datatype definitions emmitted by Thrust will not refer to those commands or predicates.