Quantifier param/var difference/usage

[Skarrabor]

Hi,

i was wondering why you need 2 kinds of variables (var/param) for quantifier?

Is there a way to reuse a boolector_param in another node (formula)?

If i, for example, want to use a param in a quantifier and after that the same param in another.

thank you for your help and have a nice day,

Daniel

[Mathias Preiner]

Hi,

The main reason is because it's easier to handle it internally and does
not require additional checks. Params are essentially bound variables
that can be bound by quantifiers or functions. As soon as a parameter is
bound you can't use it anymore for constructing terms.

HTH,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/92dd2787-cdcf-4955-86d1-d88967e58449%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/92dd2787-cdcf-4955-86d1-d88967e58449%40googlegroups.com?utm_medium=email&utm_source=footer>.