{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/265","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/265/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/265/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/265/events","html_url":"https://github.com/Z3Prover/z3/issues/265","id":113573957,"number":265,"title":"How to translate the Expr(Const number) in Z3 to be an object in MPQ/MPFR","user":{"login":"gingeredder","id":13713114,"avatar_url":"https://avatars.githubusercontent.com/u/13713114?v=3","gravatar_id":"","url":"https://api.github.com/users/gingeredder","html_url":"https://github.com/gingeredder","followers_url":"https://api.github.com/users/gingeredder/followers","following_url":"https://api.github.com/users/gingeredder/following{/other_user}","gists_url":"https://api.github.com/users/gingeredder/gists{/gist_id}","starred_url":"https://api.github.com/users/gingeredder/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gingeredder/subscriptions","organizations_url":"https://api.github.com/users/gingeredder/orgs","repos_url":"https://api.github.com/users/gingeredder/repos","events_url":"https://api.github.com/users/gingeredder/events{/privacy}","received_events_url":"https://api.github.com/users/gingeredder/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-10-27T12:40:16Z","updated_at":"2015-10-28T03:43:55Z","closed_at":null,"body":"When I use the Z3-opt(Ocaml version) to solve some planning problem, and I get a result from Z3 like this:\r\n\r\n(+ (/ 31.0 10.0) (* (to_real (- 1)) epsilon))\r\n\r\nAnd this result is of type of Z3.Expr. I want to know how to translate this result(of Z3.Expr) to anther common data-type object(for example, MPQ/MPFR).Does the Z3-opt(Ocaml version) provide the ocaml interface to this?\r\nThe result like (+ (/ 31.0 10.0) (* (to_real (- 1)) epsilon)) is to complex. \r\nI could not use this in my project. How could I get the rational number it represents?\r\n\r\nMany thanks."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/151714170","html_url":"https://github.com/Z3Prover/z3/issues/265#issuecomment-151714170","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/265","id":151714170,"user":{"login":"gingeredder","id":13713114,"avatar_url":"https://avatars.githubusercontent.com/u/13713114?v=3","gravatar_id":"","url":"https://api.github.com/users/gingeredder","html_url":"https://github.com/gingeredder","followers_url":"https://api.github.com/users/gingeredder/followers","following_url":"https://api.github.com/users/gingeredder/following{/other_user}","gists_url":"https://api.github.com/users/gingeredder/gists{/gist_id}","starred_url":"https://api.github.com/users/gingeredder/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gingeredder/subscriptions","organizations_url":"https://api.github.com/users/gingeredder/orgs","repos_url":"https://api.github.com/users/gingeredder/repos","events_url":"https://api.github.com/users/gingeredder/events{/privacy}","received_events_url":"https://api.github.com/users/gingeredder/received_events","type":"User","site_admin":false},"created_at":"2015-10-28T03:43:55Z","updated_at":"2015-10-28T03:43:55Z","body":"When I pass None. I just get the Expr of string \"(+ (/ 31.0 10.0) (* (- 1.0) |0.01|))\".  How could I get the result as a constant?"}}