[YICES-HELP] Re: models as an expression

[Bruno Dutertre]

Ali Ebnenasir wrote:
>  
>   Hello,
>    
>   I am using Yices for some program synthesis project and I need to represent all models in a satisfiable context as a Yices expression. This may be too much to ask in terms of computational complexity, but is there a built-in function in the Yices API that does so?
>    
>    
>   Thanks!
>   Ali Ebnenasir
> 
>        

Hi Ali,

There is no support for this in  the API. That's also unlikely to
be implemented in the future, because of the cost.

Bruno