{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1269","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1269/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1269/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1269/events","html_url":"https://github.com/Z3Prover/z3/issues/1269","id":260392036,"node_id":"MDU6SXNzdWUyNjAzOTIwMzY=","number":1269,"title":"Free variables in interpolants","user":{"login":"kenmcmil","id":8010069,"node_id":"MDQ6VXNlcjgwMTAwNjk=","avatar_url":"https://avatars1.githubusercontent.com/u/8010069?v=4","gravatar_id":"","url":"https://api.github.com/users/kenmcmil","html_url":"https://github.com/kenmcmil","followers_url":"https://api.github.com/users/kenmcmil/followers","following_url":"https://api.github.com/users/kenmcmil/following{/other_user}","gists_url":"https://api.github.com/users/kenmcmil/gists{/gist_id}","starred_url":"https://api.github.com/users/kenmcmil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kenmcmil/subscriptions","organizations_url":"https://api.github.com/users/kenmcmil/orgs","repos_url":"https://api.github.com/users/kenmcmil/repos","events_url":"https://api.github.com/users/kenmcmil/events{/privacy}","received_events_url":"https://api.github.com/users/kenmcmil/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":9,"created_at":"2017-09-25T19:41:37Z","updated_at":"2018-07-12T07:35:50Z","closed_at":"2018-07-05T20:21:23Z","author_association":"CONTRIBUTOR","body":"Free variables come out in interpolants. \r\n\r\nExample:\r\n\r\n`\r\n(declare-const v!0 (Array Int Int))\r\n(declare-const v!1 Int)\r\n(declare-const v!2 Int)\r\n(declare-const v!3 (Array Int Int))\r\n(declare-const v!4 (Array Int Int))\r\n(declare-fun len ((Array Int Int)) Int)\r\n\r\n(compute-interpolant (and (= v!4 v!3)\r\n     (= (len v!4) 2)\r\n     (= (select v!4 0) 4)\r\n     (= (select v!4 1) 4)\r\n     (interp (and (= (len v!3) (- v!2 v!1))\r\n                  (forall ((i Int))\r\n                    (=> (and (>= i v!1) (< i v!2))\r\n                        (= (select v!3 (- i v!1)) (select v!0 i))))\r\n                  (interp (and (= (len v!0) 3)\r\n                               (= (select v!0 0) 1)\r\n                               (= (select v!0 1) 2)\r\n                               (= (select v!0 2) 3)))\r\n                  (interp (and (= v!1 0)))\r\n                  (interp (and (= v!2 2)))))))\r\n`\r\nThis produces the following output:\r\n\r\nunsat\r\n(= 1 (select v!0 0))\r\n(let ((a!1 (= (<= (+ v!1 (* (- 1) (:var 0))) 0) (>= (:var 0) 0))))\r\n  (and a!1 (= 0 v!1)))\r\n(= (<= (+ v!2 (* (- 1) (:var 0))) 0) (>= (:var 0) 2))\r\n(= 1 (select v!3 0))\r\n\r\nThe problem appears to be free variables that are introduced in proofs involving quantifiers and arithmetic. Since these symbols aren't in the vocabulary of the original formula, they could be soundly quantified universally.  However, the reason these variables come out in the interpolant seems to be the rule that the conclusion of a sub-proof in the A vocabulary can be taken as an interpolant. This rule doesn't take into account free variables. \r\n\r\n"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/404418365","html_url":"https://github.com/Z3Prover/z3/issues/1269#issuecomment-404418365","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1269","id":404418365,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNDQxODM2NQ==","user":{"login":"mschwerhoff","id":151203,"node_id":"MDQ6VXNlcjE1MTIwMw==","avatar_url":"https://avatars1.githubusercontent.com/u/151203?v=4","gravatar_id":"","url":"https://api.github.com/users/mschwerhoff","html_url":"https://github.com/mschwerhoff","followers_url":"https://api.github.com/users/mschwerhoff/followers","following_url":"https://api.github.com/users/mschwerhoff/following{/other_user}","gists_url":"https://api.github.com/users/mschwerhoff/gists{/gist_id}","starred_url":"https://api.github.com/users/mschwerhoff/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mschwerhoff/subscriptions","organizations_url":"https://api.github.com/users/mschwerhoff/orgs","repos_url":"https://api.github.com/users/mschwerhoff/repos","events_url":"https://api.github.com/users/mschwerhoff/events{/privacy}","received_events_url":"https://api.github.com/users/mschwerhoff/received_events","type":"User","site_admin":false},"created_at":"2018-07-12T07:35:50Z","updated_at":"2018-07-12T07:35:50Z","author_association":"NONE","body":"Sorry for the confusion: I made up the syntax (Int → Bool) and intended it to denote the type of functions from Int to Bool. The above was meant to say \"forall functions F from Int to Bool, F(X) ==> F(y)\", where F could be any uninterpreted function (e.g. `(declare-fun foo (Int) Bool)`)."}}
{"actor":{"display_login":"mschwerhoff"}}