{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/813","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/813/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/813/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/813/events","html_url":"https://github.com/Z3Prover/z3/issues/813","id":192350864,"number":813,"title":"Expose register_variable in fixedpoint API?","user":{"login":"calebvoss","id":1266988,"avatar_url":"https://avatars.githubusercontent.com/u/1266988?v=3","gravatar_id":"","url":"https://api.github.com/users/calebvoss","html_url":"https://github.com/calebvoss","followers_url":"https://api.github.com/users/calebvoss/followers","following_url":"https://api.github.com/users/calebvoss/following{/other_user}","gists_url":"https://api.github.com/users/calebvoss/gists{/gist_id}","starred_url":"https://api.github.com/users/calebvoss/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/calebvoss/subscriptions","organizations_url":"https://api.github.com/users/calebvoss/orgs","repos_url":"https://api.github.com/users/calebvoss/repos","events_url":"https://api.github.com/users/calebvoss/events{/privacy}","received_events_url":"https://api.github.com/users/calebvoss/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-11-29T17:43:58Z","updated_at":"2016-11-29T18:07:18Z","closed_at":null,"body":"I'm invoking Duality through the (OCaml) API, but I can't find one of the API functions that I need.\r\n\r\nIn SMT-LIBv2, we can register our relations and the universally quantified variables using `(declare-rel A)` and `(declare-var x)` respectively. I see `Z3_fixedpoint_register_relation` in `src/api/api_datalog.cpp`, and it is exposed in OCaml as `register_relation` in `src/api/ml/z3.mli`.\r\n\r\nHowever I cannot find a corresponding `Z3_fixedpoint_register_variable` in the API. I tried to write my own. Is this right?\r\n```\r\nvoid Z3_API Z3_fixedpoint_register_variable(Z3_context c, Z3_fixedpoint d, Z3_func_decl f) {\r\n    Z3_TRY;\r\n    to_fixedpoint_ref(d)->ctx().register_variable(to_func_decl(f));\r\n    Z3_CATCH;\r\n}\r\n```\r\n\r\nAnd then, of course, a little extra boilerplate is needed to expose it through the OCaml bindings."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/263649586","html_url":"https://github.com/Z3Prover/z3/issues/813#issuecomment-263649586","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/813","id":263649586,"user":{"login":"wintersteiger","id":10155819,"avatar_url":"https://avatars.githubusercontent.com/u/10155819?v=3","gravatar_id":"","url":"https://api.github.com/users/wintersteiger","html_url":"https://github.com/wintersteiger","followers_url":"https://api.github.com/users/wintersteiger/followers","following_url":"https://api.github.com/users/wintersteiger/following{/other_user}","gists_url":"https://api.github.com/users/wintersteiger/gists{/gist_id}","starred_url":"https://api.github.com/users/wintersteiger/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wintersteiger/subscriptions","organizations_url":"https://api.github.com/users/wintersteiger/orgs","repos_url":"https://api.github.com/users/wintersteiger/repos","events_url":"https://api.github.com/users/wintersteiger/events{/privacy}","received_events_url":"https://api.github.com/users/wintersteiger/received_events","type":"User","site_admin":false},"created_at":"2016-11-29T18:07:18Z","updated_at":"2016-11-29T18:07:18Z","body":"That looks correct to me. @NikolajBjorner: should we add register_variable and register_finite_sort to the API as well?"}}
{"actor":{"display_login":"wintersteiger"}}