{"action":"created","issue":{"url":"https://api.github.com/repos/SRI-CSL/yices2/issues/86","repository_url":"https://api.github.com/repos/SRI-CSL/yices2","labels_url":"https://api.github.com/repos/SRI-CSL/yices2/issues/86/labels{/name}","comments_url":"https://api.github.com/repos/SRI-CSL/yices2/issues/86/comments","events_url":"https://api.github.com/repos/SRI-CSL/yices2/issues/86/events","html_url":"https://github.com/SRI-CSL/yices2/issues/86","id":319105838,"number":86,"title":"Python EF solving","user":{"login":"umangm","id":1497644,"avatar_url":"https://avatars3.githubusercontent.com/u/1497644?v=4","gravatar_id":"","url":"https://api.github.com/users/umangm","html_url":"https://github.com/umangm","followers_url":"https://api.github.com/users/umangm/followers","following_url":"https://api.github.com/users/umangm/following{/other_user}","gists_url":"https://api.github.com/users/umangm/gists{/gist_id}","starred_url":"https://api.github.com/users/umangm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/umangm/subscriptions","organizations_url":"https://api.github.com/users/umangm/orgs","repos_url":"https://api.github.com/users/umangm/repos","events_url":"https://api.github.com/users/umangm/events{/privacy}","received_events_url":"https://api.github.com/users/umangm/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-05-01T03:34:05Z","updated_at":"2018-05-01T14:31:56Z","closed_at":null,"author_association":"NONE","body":"Is there support for exists-forall (linear real arithmetic) solving using the Python API?\r\nIf so, can you please point me to some examples?"},"comment":{"url":"https://api.github.com/repos/SRI-CSL/yices2/issues/comments/385684989","html_url":"https://github.com/SRI-CSL/yices2/issues/86#issuecomment-385684989","issue_url":"https://api.github.com/repos/SRI-CSL/yices2/issues/86","id":385684989,"user":{"login":"ianamason","id":3421676,"avatar_url":"https://avatars2.githubusercontent.com/u/3421676?v=4","gravatar_id":"","url":"https://api.github.com/users/ianamason","html_url":"https://github.com/ianamason","followers_url":"https://api.github.com/users/ianamason/followers","following_url":"https://api.github.com/users/ianamason/following{/other_user}","gists_url":"https://api.github.com/users/ianamason/gists{/gist_id}","starred_url":"https://api.github.com/users/ianamason/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ianamason/subscriptions","organizations_url":"https://api.github.com/users/ianamason/orgs","repos_url":"https://api.github.com/users/ianamason/repos","events_url":"https://api.github.com/users/ianamason/events{/privacy}","received_events_url":"https://api.github.com/users/ianamason/received_events","type":"User","site_admin":false},"created_at":"2018-05-01T14:31:56Z","updated_at":"2018-05-01T14:31:56Z","author_association":"OWNER","body":"You would have to implement the EF solver in python using the API. I am unclear on the benefits of this, though I suppose it would make rapid prototyping tweaks to the algorithm somewhat simpler.\r\n\r\nI guess start with Bruno's [paper](http://yices.csl.sri.com/papers/smt2015.pdf) and then grok the [code](https://github.com/SRI-CSL/yices2/tree/master/src/exists_forall)\r\n"}}
{"actor":{"display_login":"ianamason"}}