{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/68","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/68/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/68/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/68/events","html_url":"https://github.com/Z3Prover/z3/issues/68","id":72932646,"number":68,"title":"fp.min/fp.max does not work correctly for -0/+0","user":{"login":"LeventErkok","id":549449,"avatar_url":"https://avatars.githubusercontent.com/u/549449?v=3","gravatar_id":"","url":"https://api.github.com/users/LeventErkok","html_url":"https://github.com/LeventErkok","followers_url":"https://api.github.com/users/LeventErkok/followers","following_url":"https://api.github.com/users/LeventErkok/following{/other_user}","gists_url":"https://api.github.com/users/LeventErkok/gists{/gist_id}","starred_url":"https://api.github.com/users/LeventErkok/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/LeventErkok/subscriptions","organizations_url":"https://api.github.com/users/LeventErkok/orgs","repos_url":"https://api.github.com/users/LeventErkok/repos","events_url":"https://api.github.com/users/LeventErkok/events{/privacy}","received_events_url":"https://api.github.com/users/LeventErkok/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":14,"created_at":"2015-05-04T06:20:26Z","updated_at":"2015-09-21T20:17:13Z","closed_at":"2015-05-04T12:47:43Z","body":"For inputs `+0/-0`, `fp.min` and `fp.max` seem to be doing the \"wrong\" thing currently.\r\n\r\nFor the following benchmark:\r\n```\r\n; Automatically generated by SBV. Do not edit.\r\n(set-option :produce-models true)\r\n(set-logic QF_FP)\r\n; --- uninterpreted sorts ---\r\n; --- literal constants ---\r\n(define-fun s_2 () Bool false)\r\n(define-fun s_1 () Bool true)\r\n; --- skolem constants ---\r\n(declare-fun s0 () (_ FloatingPoint 11 53)) ; tracks user variable \"r\"\r\n(declare-fun s1 () (_ FloatingPoint 11 53)) ; tracks user variable \"a\"\r\n(declare-fun s2 () (_ FloatingPoint 11 53)) ; tracks user variable \"b\"\r\n; --- constant tables ---\r\n; --- skolemized tables ---\r\n; --- arrays ---\r\n; --- uninterpreted constants ---\r\n; --- user given axioms ---\r\n; --- formula ---\r\n(assert ; no quantifiers\r\n   (let ((s3 (fp.isZero s1)))\r\n   (let ((s4 (fp.isNegative s1)))\r\n   (let ((s5 (and s3 s4)))\r\n   (let ((s6 (fp.isZero s2)))\r\n   (let ((s7 (fp.isPositive s2)))\r\n   (let ((s8 (and s6 s7)))\r\n   (let ((s9 (fp.min s1 s2)))\r\n   (let ((s10 (= s0 s9)))\r\n   (and s5 s8 s10))))))))))\r\n(check-sat)\r\n(get-value (s0))\r\n(get-value (s1))\r\n(get-value (s2))\r\n```\r\n\r\nZ3 responds:\r\n\r\n```\r\nsat\r\n((s0 (_ +zero 11 53)))\r\n((s1 (_ -zero 11 53)))\r\n((s2 (_ +zero 11 53)))\r\n```\r\n\r\nWhich suggests `+0, -0, +0` are solutions; but the result should actually be `-0, -0, +0`\r\n\r\nA parallel benchmark for fp.max exhibits the same problem:\r\n\r\n```\r\n; Automatically generated by SBV. Do not edit.\r\n(set-option :produce-models true)\r\n(set-logic QF_FP)\r\n; --- uninterpreted sorts ---\r\n; --- literal constants ---\r\n(define-fun s_2 () Bool false)\r\n(define-fun s_1 () Bool true)\r\n; --- skolem constants ---\r\n(declare-fun s0 () (_ FloatingPoint 11 53)) ; tracks user variable \"r\"\r\n(declare-fun s1 () (_ FloatingPoint 11 53)) ; tracks user variable \"a\"\r\n(declare-fun s2 () (_ FloatingPoint 11 53)) ; tracks user variable \"b\"\r\n; --- constant tables ---\r\n; --- skolemized tables ---\r\n; --- arrays ---\r\n; --- uninterpreted constants ---\r\n; --- user given axioms ---\r\n; --- formula ---\r\n(assert ; no quantifiers\r\n   (let ((s3 (fp.isZero s2)))\r\n   (let ((s4 (fp.isNegative s2)))\r\n   (let ((s5 (and s3 s4)))\r\n   (let ((s6 (fp.isZero s1)))\r\n   (let ((s7 (fp.isPositive s1)))\r\n   (let ((s8 (and s6 s7)))\r\n   (let ((s9 (fp.max s1 s2)))\r\n   (let ((s10 (= s0 s9)))\r\n   (and s5 s8 s10))))))))))\r\n(check-sat)\r\n(get-value (s0))\r\n(get-value (s1))\r\n(get-value (s2))\r\n```\r\n\r\nZ3 responds:\r\n\r\n```\r\nsat\r\n((s0 (_ -zero 11 53)))\r\n((s1 (_ +zero 11 53)))\r\n((s2 (_ -zero 11 53)))\r\n```\r\n\r\nWhich suggests the solution is `-0, +0, -0`; which should actually be `+0, +0, -0`."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/142097010","html_url":"https://github.com/Z3Prover/z3/issues/68#issuecomment-142097010","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/68","id":142097010,"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":"2015-09-21T20:17:13Z","updated_at":"2015-09-21T20:17:13Z","body":"> \"From the standard, it's clear...\"\r\n\r\nNo it's not, that's exactly the point, regardless of which of the 3 involved standards you refer to. \r\n\r\nPart of the SMT FP standard is to avoid as many unspecified results as possible - those create big problems for solver developers and only tiny benefits for the users. Unspecifiedness can always be recovered on the application level by guarding unspecified functions, e.g., fp.min, with an if-then-else that catches those special cases, so when we push that onto the end-user, they are responsible for picking a solver that supports uninterpreted functions; if for some reason they can't choose such a solver, then they can't have general unspecifiedness. \r\n\r\nI had brought the min/max +-0.0 case up with them before, but so far they haven't delivered a clear solution yet, and they may well have forgotten about it. Before the current SMT FP standard was released we used a google group to discuss all these issues, it's been quiet recently but I think it's the best place to bring this one up again, The group is called [smt-fp](https://groups.google.com/d/forum/smt-fp) and it might require getting permissions from the owners (should be quick though). \r\n\r\nI've taken a quick glance at BTRW14 again, and it seems like they did update the min/max paragraph to what appears like unspecifiedness, I'll confirm with them that this is indeed their intent. "}}