Insert raw definition into .smt2 file with #![raw_definie()] attribute

[coeff-aij]

This attribute allows users to inject arbitrary string literals directly into the generated .smt2 files using crate-level inner attributes.

• Usage
  By adding an inner attribute to the crate root, such as:

#![feature(custom_inner_attributes)]
#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool
    (=
        (* x 2)
        doubled_x
    )
)")]

// -- snip --

The attached string literal will be inserted into the head of the generated SMT-LIB2 file:

(set-logic HORN)

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

; -- snip --

• Motivation
  This feature is intended for debugging and testing. It enables the manual injection of SMT-LIB logic, serving as a workaround until a dedicated parser is implemented.

[coeff-aij]

Probably I have to add some more tests and documentation comments.

[coeff-aij]

How can I test that the Thrust panics with a specific error message? I tried using //@error-in-other-file, but I might be misunderstanding its purpose.

[coord-e]

I think testing panic messages is not possible with the current testing framework (ui_test https://docs.rs/ui_test/). However, I don't think we want tests for panicking cases anyway; it would be beneficial if we supported reporting rustc diagnostics for parse errors, but it's out of scope for now.

[coeff-aij]

parseg_raw_definition() is implemented on annot::AnnotParser and it's new() requires any Resolver instance, which isn't actually used in parsing of raw definitions.
I might have to fix so that no Resolver is required for this analysis.

[coord-e]

I don't think it needs to be implemented in AnnotParser. How about extracting the string from the annotation in a method within crate_::Analyzer?

[coord-e]

How about just using self.inner.raw_definitions here instead of copying raw_definitions to FormatContext?

[coord-e]

I think this feature could also be used to insert non-definitions into the resulting SMT-LIB2, such as set-option or set-info, so how about naming it something like thrust::raw_command or just thrust::raw? The same applies to RawDefinition and related data structures/functions.

[coord-e]

I don't think it needs to be implemented in AnnotParser. How about extracting the string from the annotation in a method within crate_::Analyzer?

[coord-e]

I think testing panic messages is not possible with the current testing framework (ui_test https://docs.rs/ui_test/). However, I don't think we want tests for panicking cases anyway; it would be beneficial if we supported reporting rustc diagnostics for parse errors, but it's out of scope for now.

[coord-e]

nit

Suggested change

	// Insert definitions written in SMT-LIB2 format into .smt file directly.
	// Insert definitions written in SMT-LIB2 format into .smt2 file directly.

[coord-e]

If you plan to uncomment this in a future PR, please add a note about it in the comments.