{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1627","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1627/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1627/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1627/events","html_url":"https://github.com/Z3Prover/z3/issues/1627","id":324333649,"number":1627,"title":"Parse smt file and use already defined symbol of it from API","user":{"login":"SylvainCecchetto","id":11562279,"avatar_url":"https://avatars0.githubusercontent.com/u/11562279?v=4","gravatar_id":"","url":"https://api.github.com/users/SylvainCecchetto","html_url":"https://github.com/SylvainCecchetto","followers_url":"https://api.github.com/users/SylvainCecchetto/followers","following_url":"https://api.github.com/users/SylvainCecchetto/following{/other_user}","gists_url":"https://api.github.com/users/SylvainCecchetto/gists{/gist_id}","starred_url":"https://api.github.com/users/SylvainCecchetto/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SylvainCecchetto/subscriptions","organizations_url":"https://api.github.com/users/SylvainCecchetto/orgs","repos_url":"https://api.github.com/users/SylvainCecchetto/repos","events_url":"https://api.github.com/users/SylvainCecchetto/events{/privacy}","received_events_url":"https://api.github.com/users/SylvainCecchetto/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-05-18T09:21:43Z","updated_at":"2018-05-21T15:43:05Z","closed_at":null,"author_association":"NONE","body":"Hi,\r\n\r\nLet's say I have a SMT file foo.smt2 like this:\r\n```\r\n(set-logic QF_ABV)\r\n(set-info :smt-lib-version 2.0)\r\n(define-fun res () (_ BitVec 32) (_ bv1 32))\r\n(define-fun edi () (_ BitVec 32) res)\r\n```\r\n\r\nI use the C++ API function `parse_file` in order to load my SMT file:\r\n```\r\ncontext c;\r\nexpr a = c.parse_file(\"foo.smt2\");\r\n```\r\n\r\nI already know that `edi` is defined in the smt file, so I want to compute something like that:\r\n```\r\ncontext c;\r\nexpr a = c.parse_file(\"foo.smt2\");\r\nexpr b = c.bv_const(\"toto\", 32);\r\nsolver s(c);\r\n```\r\n\r\nBut it didn't work... Maybe I miss something?\r\n\r\nThanks for help.\r\n\r\nEDIT: My original goal is to build a context object  once and for all from an initial SMT file (because in my SMT file there is only declarations and no assert). Then from this context object I want to check different things. (You can see a pseudo code bellow that explain what I want to do):\r\n\r\n```\r\ncontext c; // The only context object that I want to use to work\r\nfunction_that_initialize_the_context_with_all_declarations_from_my_smt_file;\r\n\r\n// Then now a lot of computation with existing objects from my smt file\r\nsolver s(c);\r\ns.add(toto == titi);\r\ns.check;\r\n\r\nsolver s2(c);\r\ns2.add(abc != def);\r\ns2.check;\r\n\r\n[...]\r\n```"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/390693543","html_url":"https://github.com/Z3Prover/z3/issues/1627#issuecomment-390693543","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1627","id":390693543,"user":{"login":"NikolajBjorner","id":3085284,"avatar_url":"https://avatars2.githubusercontent.com/u/3085284?v=4","gravatar_id":"","url":"https://api.github.com/users/NikolajBjorner","html_url":"https://github.com/NikolajBjorner","followers_url":"https://api.github.com/users/NikolajBjorner/followers","following_url":"https://api.github.com/users/NikolajBjorner/following{/other_user}","gists_url":"https://api.github.com/users/NikolajBjorner/gists{/gist_id}","starred_url":"https://api.github.com/users/NikolajBjorner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NikolajBjorner/subscriptions","organizations_url":"https://api.github.com/users/NikolajBjorner/orgs","repos_url":"https://api.github.com/users/NikolajBjorner/repos","events_url":"https://api.github.com/users/NikolajBjorner/events{/privacy}","received_events_url":"https://api.github.com/users/NikolajBjorner/received_events","type":"User","site_admin":false},"created_at":"2018-05-21T15:43:05Z","updated_at":"2018-05-21T15:43:05Z","author_association":"CONTRIBUTOR","body":"> But, if I understand, it doesn't work because the foo expr is empty because there is no assertion in foo.smt2. That's right?\r\nThe current version of the API returns an expression that is the conjunction of all assertions. So if there are no assertions, the conjunction is empty and the expression is \"true\".\r\nI am going to change this API to return a _vector_ of assertions. In this case the vector is empty. So same deal. There is no real difference between the solutions you propose, other than some use extra variables. \r\n"}}
{"actor":{"display_login":"NikolajBjorner"}}