Better docs for AST nodes

[matth2k]

For example, ite has no docs at all. I am not as familiar with the internals of Z3 and SMTLIB, so I need to do a lot of jumping around to external documentation.

z3.rs/z3/src/ast/bool.rs

Lines 57 to 73 in cb655ca

	// This doesn't quite fit the trinop! macro because of the generic argty
	pub fn ite<T>(&self, a: &T, b: &T) -> T
	where
	T: Ast,
	{
	unsafe {
	T::wrap(&self.ctx, {
	Z3_mk_ite(
	self.ctx.z3_ctx.0,
	self.z3_ast,
	a.get_z3_ast(),
	b.get_z3_ast(),
	)
	.unwrap()
	})
	}
	}

Mind if I propose doc changes as I work alongside my personal project? For example:

    /// if-then-else operator for [Bool]. Takes on the value `then` when `self` evaluates to true
    pub fn ite<T>(&self, then: &T, else: &T) -> T
    where
        T: Ast,
    {
        unsafe {
            T::wrap(&self.ctx, {
                Z3_mk_ite(
                    self.ctx.z3_ctx.0,
                    self.z3_ast,
                    then.get_z3_ast(),
                    else.get_z3_ast(),
                )
                .unwrap()
            })
        }
    }

Eventually #![warn(missing_docs, unreachable_pub)] should be the goal.

[toolCHAINZ]

Absolutely! Please feel free to open some PRs!

Note that the low level bindings have documentation copied from the z3 header file. While not exactly ideal for the high level bindings that can be a good starting point.

While making high level API docs I also like to include doc tests where applicable.

Yes turning on that lint would be ideal. Maybe if we get full coverage in parts of the codebase we can enable it per module.

[matth2k]

Sounds good. I see there are some macros for these operations as well:

z3.rs/z3/src/ast/bool.rs

Lines 75 to 86 in cb655ca

	varop! {
	and(Z3_mk_and, Self);
	or(Z3_mk_or, Self);
	}
	binop! {
	xor(Z3_mk_xor, Self);
	iff(Z3_mk_iff, Self);
	implies(Z3_mk_implies, Self);
	}
	unop! {
	not(Z3_mk_not, Self);
	}

so I will try to plumb the doclines through the macros.

[toolCHAINZ]

That's a good point. We'll likely want to augment those macros to also match on a doc comment attribute and decorate the final impl with it

[toolCHAINZ]

I'm going to close this and convert it to a discussion; as stated, please feel free to open PRs for any missing docs!

[toolCHAINZ]

Even better! Looking at the macro, it already does handle attributes on functions! So you should be able to just place doc comments as usual.