{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/209","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/209/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/209/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/209/events","html_url":"https://github.com/Z3Prover/z3/issues/209","id":104165012,"number":209,"title":"Forking/Serializing a z3 Solver","user":{"login":"ltfish","id":5071575,"avatar_url":"https://avatars.githubusercontent.com/u/5071575?v=3","gravatar_id":"","url":"https://api.github.com/users/ltfish","html_url":"https://github.com/ltfish","followers_url":"https://api.github.com/users/ltfish/followers","following_url":"https://api.github.com/users/ltfish/following{/other_user}","gists_url":"https://api.github.com/users/ltfish/gists{/gist_id}","starred_url":"https://api.github.com/users/ltfish/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ltfish/subscriptions","organizations_url":"https://api.github.com/users/ltfish/orgs","repos_url":"https://api.github.com/users/ltfish/repos","events_url":"https://api.github.com/users/ltfish/events{/privacy}","received_events_url":"https://api.github.com/users/ltfish/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-09-01T01:26:13Z","updated_at":"2015-09-03T08:57:21Z","closed_at":null,"body":"We are a bunch of people working on a symbolic execution engine, and we are intensively depending on Z3 (needless to say, it's really good :-) ). Now we are looking into possibilities of forking Z3 solvers. Basically we'd like to use the incremental solving support in Z3, instead of solving all constraints again once an execution path branches. We looked into code, and found out much effort is required to make Z3 do what we need. What do you think the best option is?\r\n\r\nI'm wondering if you will support forking or serializing a Z3 solver soon, or any similar solution is in your future plan. If not, and in case we go ahead and implement the serializing support, what are the chances of merging it in to `master`? Maintaining a big bunch of code by ourselves is suboptimal."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/137383312","html_url":"https://github.com/Z3Prover/z3/issues/209#issuecomment-137383312","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/209","id":137383312,"user":{"login":"ltfish","id":5071575,"avatar_url":"https://avatars.githubusercontent.com/u/5071575?v=3","gravatar_id":"","url":"https://api.github.com/users/ltfish","html_url":"https://github.com/ltfish","followers_url":"https://api.github.com/users/ltfish/followers","following_url":"https://api.github.com/users/ltfish/following{/other_user}","gists_url":"https://api.github.com/users/ltfish/gists{/gist_id}","starred_url":"https://api.github.com/users/ltfish/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ltfish/subscriptions","organizations_url":"https://api.github.com/users/ltfish/orgs","repos_url":"https://api.github.com/users/ltfish/repos","events_url":"https://api.github.com/users/ltfish/events{/privacy}","received_events_url":"https://api.github.com/users/ltfish/received_events","type":"User","site_admin":false},"created_at":"2015-09-03T08:57:21Z","updated_at":"2015-09-03T08:57:21Z","body":"@NikolajBjorner I didn't make it clear in my previous posts, and let me try to rephrase that.\r\n\r\nI believe the gain in caching internalized formulae and lemmas is completely not comparable with the overhead of searching the result space. What I care about is retaining the searching result of the old solver in the newly-forked solver, so we don't have to search again (for all previously added clauses) when a new assertion is added to the new solver - instead, we only search a smaller space. I believe this is what incremental solving in Z3 is about. Let me know if I made a mistake here.\r\n\r\n> Cloning it seems rather error prone to program because you would want to maintain the associating between expressions and internal representations ...\r\n\r\nAfter reading more code, I believe you are absolutely right. Almost every class under `smt/` will be changed if I want to add support of solver cloning (while keeping its entire internal state)."}}