[YICES-HELP] About C API for applying quantification logic

[Bruno Dutertre]

Mohammad Ashiqur Rahman wrote:
> Hi,
> 
> Is there any way to use quantifier (forall, exists) using C API? I did not
> find any function to use these quantifiers in the logic. Especially I want
> to define a function, e.g., (IsLink a b) which is true for all a and b if
> they satisfies some constraints. For such kind of definition, 'forall' is
> required. But I cannot find any way to solve this issue. Is there any way.
> 
> 

Hi Ashiq,

There's not explicit function for building forall/exists in the API,
but you can do this use 'yices_parse_expression' to do it.

Bruno