[YICES-HELP] About C API for applying quantification logic
bruno at csl.sri.com
Thu Mar 8 10:20:05 PST 2012
Mohammad Ashiqur Rahman wrote:
> 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.
There's not explicit function for building forall/exists in the API,
but you can do this use 'yices_parse_expression' to do it.
More information about the YICES-HELP