Add bindings for global params

[Shatur]

Resubmit of #199.

[Pat-Lafon]

Hi, I was curious, what happens when you call https://z3prover.github.io/api/html/group__capi.html#ga9162ac23461bc67d1a0cde7c71f53111 with some bad string(Out of range chars or incorrect use of delimitation)?

Does it panic or just silently fail? Do we expect these bindings to enforce the precondition or is it up to Z3?

[Shatur]

with some bad string

But we pass str, Rust already ensures that the string is valid. Unless you use unsafe 😄
The same code already used in Z3 for Config.

[Pat-Lafon]

Here by bad string I meant something that violated the parameter naming assumption of Z3, as I linked to this line: The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. The character '.' is a delimiter (more later).

Fair, maybe this also applies for Config but the Z3 docs don't have a similar line and I don't think support the '.' delimiter thing.

[Shatur]

Got it. Tested with invalid characters, nothing happens.

[Shatur]

A bit off-topic question, but do you know a way to set "global" parameters for specific context?
I tried setting sat.euf via Params or via Z3_update_param_value, but only global params have any effect.

[Pat-Lafon]

Sorry, I don't know too much about this. Just fyi, if this is all through the Rust bindings, the Z3 error handler gets disabled so it might be silently failing when you are trying to set the parameter. #235 (comment) If that's your issue, then re-enabling it should shed light on the situation.

[Shatur]

Thanks for the info!

[Shatur]

@Pat-Lafon figured it out:

        let tactic = Tactic::new(&ctx, "sat");
        let solver = tactic.solver();
        let mut params = Params::new(&ctx);
        params.set_bool("sat.euf", true);
        solver.set_params(&params);

But it's unrelated to the PR, I think it's ready for merge.

[Pat-Lafon]

Maybe worth pinging @waywardmonkeys to put this on his radar though I'm not sure how much time he has these days.

[waywardmonkeys]

Ready for merge? Here we go!

[Shatur]

@waywardmonkeys could you draft a new release?

[waywardmonkeys]

Let's see in 24 hours ... I'm away from home, so I won't be able to tomorrow. I just pushed some other changes that I had hanging around as well, so CI is backed up for a while.