{"action":"created","comment":{"url":"https://api.github.com/repos/CVC4/CVC4/pulls/comments/240394557","pull_request_review_id":183416658,"id":240394557,"node_id":"MDI0OlB1bGxSZXF1ZXN0UmV2aWV3Q29tbWVudDI0MDM5NDU1Nw==","diff_hunk":"@@ -0,0 +1,566 @@\n+; LRAT Proof signature\n+; LRAT format detailed in \"Efficient Certified RAT Verification\"\n+; Author: aozdemir\n+; Depends On: sat.plf\n+\n+\n+; A general note about the design of the side conditions:\n+;  Some side-conditions make use of a _global assignment_ encoded in\n+;  0 (true) / 1 (false) marks on variables.\n+\n+; A list of clauses, CNF if interpretted as a formula,\n+; but also sometimes just a list\n+(declare cnf type)\n+(declare cnfn cnf)\n+(declare cnfc (! h clause (! t cnf cnf)))\n+\n+; Unit\n+(declare Unit type)\n+(declare unit Unit)\n+\n+; Boolean operator (not short-circuiting)\n+(program bool_or ((l bool) (r bool)) bool (match l (ff r) (tt tt)))\n+(program bool_and ((l bool) (r bool)) bool (match l (tt r) (ff ff)))\n+(program bool_not ((b bool)) bool (match b (tt ff) (ff tt)))\n+\n+; =================== ;\n+; Working CNF formula ;\n+; =================== ;\n+\n+; Represents a CNF formula as a map from clause indices to clauses\n+; Should be sorted ascending, always!\n+(declare CMap type)\n+(declare CMapn CMap)\n+(declare CMapc (! i mpz (! c clause (! r CMap CMap))))\n+\n+; ================= ;\n+; LRAT Proof Format ;\n+; ================= ;\n+\n+; CI lists are lists of clause indices.\n+; They represent clauses to delete.\n+; They must be sorted.\n+(declare CIList type)\n+(declare CIListn CIList)\n+(declare CIListc (! z mpz (! zs CIList CIList)))\n+\n+; Traces are a list of clause indices into the working CNF formula\n+; They represent the clauses that will be unit in a unit propegation to bottom\n+; Thus their elements are *not* in value order.\n+(declare Trace type)\n+(declare Tracen Trace)\n+(declare Tracec (! z mpz (! zs Trace Trace)))\n+\n+; RAT Hint list\n+; Each hint is\n+;   * An index indicating a clause in the working CNF formula to resolve with\n+;   * A trace indicating how UP should be done after that resolution\n+(declare RATHints type)\n+(declare RATHintsn RATHints)\n+(declare RATHintsc\n+         (! target mpz\n+            (! trace Trace\n+               (! rest RATHints\n+                  RATHints))))\n+\n+; LRAT proof\n+(declare LRATProof type)\n+(declare LRATProofn LRATProof)\n+; Deletion (includes a list of clause indices to delete)\n+(declare LRATProofd (! cis CIList (! rest LRATProof LRATProof)))\n+; Addition: a clause index, a clause, RUP trace for that clause, and hints for\n+; what resolutions should happen then, and how those resolutions imply bottom\n+; via UP.\n+; If the list of hints is empty, then bottom is already implied.\n+(declare LRATProofa\n+         (! ci mpz\n+            (! c clause\n+               (! t Trace\n+                  (! h RATHints\n+                     (! rest LRATProof\n+                        LRATProof))))))\n+\n+; ========================================== ;\n+; Functional programs for manipulating types ;\n+; ========================================== ;\n+\n+; Subtract two integers\n+(program lrat_mpz_sub ((a mpz) (b mpz)) mpz\n+         (mp_add a (mp_neg b)))\n+\n+; Flip the polarity of the literal\n+(program lit_flip ((l lit)) lit\n+         (match l\n+                ((pos v) (neg v))\n+                ((neg v) (pos v))))\n+\n+; Compute the variable  in the literal\n+(program lit_var ((l lit)) lit\n+         (match l\n+                ((pos v) v)\n+                ((neg v) v)))\n+\n+; Are two literal equal?\n+(program lit_eq ((l1 lit) (l2 lit)) bool\n+         (match l1\n+                ((pos v1) (match l2\n+                                 ((pos v2) (ifequal v1 v2 tt ff))\n+                                 ((neg v2) ff)))\n+                ((neg v1) (match l2\n+                                 ((pos v2) ff)\n+                                 ((neg v2) (ifequal v1 v2 tt ff))))))\n+\n+; Remove **all** occurences of a literal from clause\n+(program clause_remove_all ((l lit) (c clause)) clause\n+         (match c\n+                (cln cln)\n+                ((clc l' c')\n+                 (let rest_res (clause_remove_all l c')\n+                   (match (lit_eq l l')\n+                          (tt rest_res)\n+                          (ff (clc l' rest_res)))))))\n+\n+; Return the clause's first  literal\n+; fails on an empty clause\n+(program clause_head ((c clause)) lit\n+         (match c\n+                (cln (fail lit))\n+                ((clc l c') l)))\n+\n+; append two clauses\n+(program clause_concat ((c1 clause) (c2 clause)) clause\n+    (match c1\n+        (cln c2)\n+        ((clc l c1') (clc l (clause_concat c1' c2)))))\n+\n+; Does a clause contain some literal?\n+(program clause_contains_lit ((c clause) (l lit)) bool\n+         (match c\n+                ((clc l' c') (match (lit_eq l l')\n+                                    (tt tt)\n+                                    (ff (clause_contains_lit c' l))))\n+                (cln ff)))\n+\n+; Append two traces\n+(program Trace_concat ((t1 Trace) (t2 Trace)) Trace\n+         (match t1\n+                (Tracen t2)\n+                ((Tracec h1 r1) (Tracec h1 (Trace_concat r1 t2)))))\n+\n+; Return whether a list of RAT hits is empty\n+(program RATHints_is_empty ((h RATHints)) bool\n+         (match h\n+                (RATHintsn tt)\n+                ((RATHintsc a b c) ff)))\n+\n+; Insert into a CMap, preserving order\n+(program CMap_insert ((i mpz) (c clause) (cs CMap)) CMap\n+         (match cs\n+                (CMapn (CMapc i c CMapn))\n+                ((CMapc i' c' r)\n+                 (mp_ifneg (lrat_mpz_sub i i')\n+                        (CMapc i c cs)\n+                        (CMapc i' c' (CMap_insert i c r))))))\n+\n+; Get from a CMap\n+(program CMap_get ((i mpz) (cs CMap)) clause\n+         (match cs\n+                (CMapn (fail clause))\n+                ((CMapc i' c r)\n+                 (mp_ifzero (lrat_mpz_sub i i')\n+                        c\n+                        (CMap_get i r)))))\n+\n+; Remove from CMap. Only removes one element.\n+(program CMap_remove ((i mpz) (cs CMap)) CMap\n+         (match cs\n+                (CMapn CMapn)\n+                ((CMapc i' c r)\n+                 (mp_ifzero (lrat_mpz_sub i i')\n+                        r\n+                        (CMapc i' c (CMap_remove i r))))))\n+\n+; Remove many indices from a CMap. Asuumes the input list is sorted.\n+(program CMap_remove_many ((is CIList) (cs CMap)) CMap\n+         (match\n+           is\n+           (CIListn cs)\n+           ((CIListc i is')\n+            (match\n+              cs\n+              (CMapn (fail CMap)) ; All deletion indices must be valid!\n+              ((CMapc ci c cs')\n+               (mp_ifzero (lrat_mpz_sub i ci)\n+                       (CMap_remove_many is' cs')\n+                       (CMapc ci c (CMap_remove_many is cs'))))))))\n+\n+; Given a map of clauses and a literal, return all indices in the map\n+; corresponsing to clauses that could resolve against that literal. i.e. for x,\n+; return the indices of all clauses containing ~x.\n+(program collect_resolution_targets_w_lit ((cs CMap) (l lit)) CIList\n+         (match cs\n+                (CMapn CIListn)\n+                ((CMapc i c cs')\n+                 (let rest_solution (collect_resolution_targets_w_lit cs' l)\n+                   (match (clause_contains_lit c l)\n+                        (tt (CIListc i rest_solution))\n+                        (ff rest_solution))))))\n+\n+; Given a clause and a maps of clauses, return all indices in the map\n+; corresponding to clauses which could resolve with this one on its first\n+; literal\n+(program collect_resolution_targets ((cs CMap) (c clause)) CIList\n+         (collect_resolution_targets_w_lit cs (lit_flip (clause_head c))))\n+\n+; ===================================================================== ;\n+; Programs for manipulating and querying the global variable assignment ;\n+; ===================================================================== ;\n+\n+; This assignment marks values of type `var`.\n+; It marks a variable with 1 if that variable is true\n+; It marks a variable with 2 if that variable is false\n+; A variable should not be marked with both!\n+; A variable may be marked with neither, indicating that variable is presently\n+; unassigned.\n+\n+; Mark the variable within to satisfy this literal.\n+; fails is the literal is already UNSAT\n+(program lit_mk_sat ((l lit)) Unit\n+         (match l\n+                ((pos v) (ifmarked2 v\n+                                    (fail Unit)\n+                                    (ifmarked1 v unit (do (markvar1 v) unit))))\n+                ((neg v) (ifmarked1 v\n+                                    (fail Unit)\n+                                    (ifmarked2 v unit (do (markvar2 v) unit))))))\n+\n+; Mark the variable within to falsify this literal.\n+; fails is the literal is already UNSAT\n+(program lit_mk_unsat ((l lit)) Unit\n+         (match l\n+                ((neg v) (ifmarked2 v\n+                                    (fail Unit)\n+                                    (ifmarked1 v unit (do (markvar1 v) unit))))\n+                ((pos v) (ifmarked1 v\n+                                    (fail Unit)\n+                                    (ifmarked2 v unit (do (markvar2 v) unit))))))\n+\n+; Unmarks the variable within a satified literal to render it neither satified nor falsified\n+; fails if the literal is not already satisfied\n+(program lit_un_mk_sat ((l lit)) Unit\n+         (match l\n+                ((pos v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit)))\n+                ((neg v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit)))))\n+\n+; Unmarks the variable within a falsified literal to render it neither satified nor falsified\n+; fails if the literal is not already falsified\n+(program lit_un_mk_unsat ((l lit)) Unit\n+         (match l\n+                ((pos v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit)))\n+                ((neg v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit)))))\n+\n+;  Is a literal presently satisfied?\n+(program lit_is_sat ((l lit)) bool\n+         (match l\n+                ((pos v) (ifmarked1 v tt ff))\n+                ((neg v) (ifmarked2 v tt ff))))\n+\n+;  Is a literal presently falsified?\n+(program lit_is_unsat ((l lit)) bool\n+         (match l\n+                ((pos v) (ifmarked2 v tt ff))\n+                ((neg v) (ifmarked1 v tt ff))))\n+\n+;  Is a  literal presently neither satisfied nor falsified?\n+(program lit_is_floating ((l lit)) bool\n+         (bool_not (bool_or (lit_is_sat l) (lit_is_unsat l))))\n+\n+; Does this clause contain a floating literal?\n+(program clause_has_floating ((c clause)) bool\n+         (match c\n+                (cln ff)\n+                ((clc l c') (match (lit_is_floating l)\n+                                   (tt tt)\n+                                   (ff (clause_has_floating c'))))))\n+\n+; Is this clause falsified? i.e. are all its clauses falsified?\n+(program clause_is_unsat ((c clause)) bool\n+         (match c\n+                (cln tt)\n+                ((clc l c') (match (lit_is_unsat l)\n+                                   (tt (clause_is_unsat c'))\n+                                   (ff ff)))))\n+\n+; Is this clause presently satisfied?\n+(program clause_is_sat ((c clause)) bool\n+         (match c\n+                (cln ff)\n+                ((clc l c') (match (lit_is_sat l)\n+                                   (tt tt)\n+                                   (ff (clause_is_sat c'))))))\n+\n+; Falsify **all** contained literals.\n+; Fails on a tautological clause\n+(program clause_mk_all_unsat ((c clause)) Unit\n+         (match c\n+                (cln unit)\n+                ((clc l c') (do\n+                              (lit_mk_unsat l)\n+                              (clause_mk_all_unsat c')))))\n+\n+; Unfalsifies **all** contained literals\n+; Fails on a clause with duplicate literals\n+(program clause_un_mk_all_unsat ((c clause)) Unit\n+         (match c\n+                (cln unit)\n+                ((clc l c') (do\n+                              (lit_un_mk_unsat l)\n+                              (clause_un_mk_all_unsat c')))))\n+\n+; Get the first floating literal out of this clause.\n+; fails if there are no floating literals\n+(program clause_first_floating ((c clause)) lit\n+         (match c\n+                (cln (fail lit))\n+                ((clc l c') (match (lit_is_floating l)\n+                                   (tt l)\n+                                   (ff (clause_first_floating c'))))))\n+\n+; ===================================== ;\n+; High-Level Programs for LRAT Checking ;\n+; ===================================== ;\n+\n+; The return type for verifying that a clause is unit and modifying the global\n+; assignment to satisfy it\n+(declare MarkResult type)\n+; The clause is unit, and this is the (previoiusly floating) literal that is now satified.\n+(declare MRUnit (! l lit MarkResult))\n+; The clause was unsat!\n+(declare MRUnsat MarkResult)\n+; The clauss was already satisfied.\n+(declare MRSat MarkResult)\n+; The clause had multiple floating literals.\n+(declare MRNotUnit MarkResult)\n+\n+; Determine wether this clause is unit, and if so, modify global assignment to\n+; satisfy it.\n+;\n+; Will never fail.\n+;\n+; Given a TAUT, where the TAUT variable is the sole floating one, marks that\n+; var to satisify its first literal\n+(program clause_verify_unit_and_mark ((c clause)) MarkResult\n+         (match (clause_is_sat c)\n+                (tt MRSat)\n+                (ff (match (clause_is_unsat c)\n+                           (tt MRUnsat)\n+                           (ff ; Dedent\n+         (match (clause_has_floating c)\n+                (tt (let first (clause_first_floating c)\n+                      (do (lit_mk_sat first)\n+                        (match (clause_has_floating c)\n+                               (tt (do (lit_un_mk_sat first) MRNotUnit))\n+                               (ff (MRUnit first))))))\n+                ; Unreachable. If clause is not floating it must have been SAT or UNSAT.\n+                (ff (fail MarkResult))\n+                ))))))\n+\n+; The return type for the process of Trace-guided unit propegation\n+(declare UPResult type)\n+; The trace guided unit propegation correctly, but that unit propegation did not end in an empty clause\n+(declare UPR_Ok UPResult)\n+; The trace guided unit propegation correctly to an empty clause\n+(declare UPR_Bottom UPResult)\n+; The trace was malformed,\n+;; i.e. at some point indicates that a non-unit, non-empty clause should be examined\n+(declare UPR_Broken UPResult)\n+\n+; Execute the unit propegation  indicated by the trace. Report whether that\n+; unit propegation succeeds and produces bottom, fails, or succeeds but does\n+; not produce bottom.\n+; Will never fail.\n+; If a TAUT is present, will in some cases allow a TAUT to propegate on of the\n+; variables its TAUT on, to SAT that variables first literal.\n+(program do_up ((cs CMap) (t Trace)) UPResult\n+         (match\n+           t\n+           (Tracen UPR_Ok)\n+           ((Tracec i r) (match (clause_verify_unit_and_mark (CMap_get i cs))\n+                                ((MRUnit l)\n+                                 (let res (do_up cs r)\n+                                   (do (lit_un_mk_sat l) res)))\n+                                (MRUnsat UPR_Bottom)\n+                                (MRSat UPR_Broken)\n+                                (MRNotUnit UPR_Broken)))))\n+\n+\n+; Determine whether a list of indices agrees with the list of indices latent in\n+; a list of hints. Both lists should be sorted.\n+(program resolution_targets_match (\n+                                   (computed CIList)\n+                                   (given RATHints)) bool\n+         (match given\n+                (RATHintsn\n+                  (match computed\n+                         (CIListn tt)\n+                         ((CIListc a b) ff)))\n+                ((RATHintsc hint_idx t given')\n+                 (match computed\n+                        ((CIListc comp_idx computed')","path":"proofs/signatures/lrat.plf","position":409,"original_position":409,"commit_id":"8d244c933a853b8483819d1b73ef5941e46cc96a","original_commit_id":"a6f606d262036d138942478450493290626bcc91","user":{"login":"alex-ozdemir","id":5809398,"node_id":"MDQ6VXNlcjU4MDkzOTg=","avatar_url":"https://avatars2.githubusercontent.com/u/5809398?v=4","gravatar_id":"","url":"https://api.github.com/users/alex-ozdemir","html_url":"https://github.com/alex-ozdemir","followers_url":"https://api.github.com/users/alex-ozdemir/followers","following_url":"https://api.github.com/users/alex-ozdemir/following{/other_user}","gists_url":"https://api.github.com/users/alex-ozdemir/gists{/gist_id}","starred_url":"https://api.github.com/users/alex-ozdemir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/alex-ozdemir/subscriptions","organizations_url":"https://api.github.com/users/alex-ozdemir/orgs","repos_url":"https://api.github.com/users/alex-ozdemir/repos","events_url":"https://api.github.com/users/alex-ozdemir/events{/privacy}","received_events_url":"https://api.github.com/users/alex-ozdemir/received_events","type":"User","site_admin":false},"body":"Good catch. It should return `ff`.","created_at":"2018-12-10T21:52:35Z","updated_at":"2018-12-10T21:52:36Z","html_url":"https://github.com/CVC4/CVC4/pull/2731#discussion_r240394557","pull_request_url":"https://api.github.com/repos/CVC4/CVC4/pulls/2731","author_association":"CONTRIBUTOR","_links":{"self":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/comments/240394557"},"html":{"href":"https://github.com/CVC4/CVC4/pull/2731#discussion_r240394557"},"pull_request":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/2731"}},"in_reply_to_id":240357014},"pull_request":{"url":"https://api.github.com/repos/CVC4/CVC4/pulls/2731","id":235231083,"node_id":"MDExOlB1bGxSZXF1ZXN0MjM1MjMxMDgz","html_url":"https://github.com/CVC4/CVC4/pull/2731","diff_url":"https://github.com/CVC4/CVC4/pull/2731.diff","patch_url":"https://github.com/CVC4/CVC4/pull/2731.patch","issue_url":"https://api.github.com/repos/CVC4/CVC4/issues/2731","number":2731,"state":"open","locked":false,"title":"LRAT signature","user":{"login":"alex-ozdemir","id":5809398,"node_id":"MDQ6VXNlcjU4MDkzOTg=","avatar_url":"https://avatars2.githubusercontent.com/u/5809398?v=4","gravatar_id":"","url":"https://api.github.com/users/alex-ozdemir","html_url":"https://github.com/alex-ozdemir","followers_url":"https://api.github.com/users/alex-ozdemir/followers","following_url":"https://api.github.com/users/alex-ozdemir/following{/other_user}","gists_url":"https://api.github.com/users/alex-ozdemir/gists{/gist_id}","starred_url":"https://api.github.com/users/alex-ozdemir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/alex-ozdemir/subscriptions","organizations_url":"https://api.github.com/users/alex-ozdemir/orgs","repos_url":"https://api.github.com/users/alex-ozdemir/repos","events_url":"https://api.github.com/users/alex-ozdemir/events{/privacy}","received_events_url":"https://api.github.com/users/alex-ozdemir/received_events","type":"User","site_admin":false},"body":"Added an LRAT signature. It is almost entirely side-conditions, but it\r\nworks.\r\n\r\nThere is also a collection of tests for it. You can run them by invoking\r\n\r\n```\r\nlfscc sat.plf smt.plf lrat.plf lrat_test.plf\r\n```","created_at":"2018-12-02T01:38:09Z","updated_at":"2018-12-10T21:52:36Z","closed_at":null,"merged_at":null,"merge_commit_sha":"319bffc0bfaeaae080da825d29ce48219c55f4b0","assignee":{"login":"yoni206","id":12624708,"node_id":"MDQ6VXNlcjEyNjI0NzA4","avatar_url":"https://avatars2.githubusercontent.com/u/12624708?v=4","gravatar_id":"","url":"https://api.github.com/users/yoni206","html_url":"https://github.com/yoni206","followers_url":"https://api.github.com/users/yoni206/followers","following_url":"https://api.github.com/users/yoni206/following{/other_user}","gists_url":"https://api.github.com/users/yoni206/gists{/gist_id}","starred_url":"https://api.github.com/users/yoni206/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yoni206/subscriptions","organizations_url":"https://api.github.com/users/yoni206/orgs","repos_url":"https://api.github.com/users/yoni206/repos","events_url":"https://api.github.com/users/yoni206/events{/privacy}","received_events_url":"https://api.github.com/users/yoni206/received_events","type":"User","site_admin":false},"assignees":[{"login":"yoni206","id":12624708,"node_id":"MDQ6VXNlcjEyNjI0NzA4","avatar_url":"https://avatars2.githubusercontent.com/u/12624708?v=4","gravatar_id":"","url":"https://api.github.com/users/yoni206","html_url":"https://github.com/yoni206","followers_url":"https://api.github.com/users/yoni206/followers","following_url":"https://api.github.com/users/yoni206/following{/other_user}","gists_url":"https://api.github.com/users/yoni206/gists{/gist_id}","starred_url":"https://api.github.com/users/yoni206/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yoni206/subscriptions","organizations_url":"https://api.github.com/users/yoni206/orgs","repos_url":"https://api.github.com/users/yoni206/repos","events_url":"https://api.github.com/users/yoni206/events{/privacy}","received_events_url":"https://api.github.com/users/yoni206/received_events","type":"User","site_admin":false}],"requested_reviewers":[],"requested_teams":[],"labels":[{"id":717338434,"node_id":"MDU6TGFiZWw3MTczMzg0MzQ=","url":"https://api.github.com/repos/CVC4/CVC4/labels/moderate","name":"moderate","color":"88ccf5","default":false},{"id":671891100,"node_id":"MDU6TGFiZWw2NzE4OTExMDA=","url":"https://api.github.com/repos/CVC4/CVC4/labels/normal","name":"normal","color":"ededed","default":false}],"milestone":null,"commits_url":"https://api.github.com/repos/CVC4/CVC4/pulls/2731/commits","review_comments_url":"https://api.github.com/repos/CVC4/CVC4/pulls/2731/comments","review_comment_url":"https://api.github.com/repos/CVC4/CVC4/pulls/comments{/number}","comments_url":"https://api.github.com/repos/CVC4/CVC4/issues/2731/comments","statuses_url":"https://api.github.com/repos/CVC4/CVC4/statuses/8d244c933a853b8483819d1b73ef5941e46cc96a","head":{"label":"alex-ozdemir:lrat-sig","ref":"lrat-sig","sha":"8d244c933a853b8483819d1b73ef5941e46cc96a","user":{"login":"alex-ozdemir","id":5809398,"node_id":"MDQ6VXNlcjU4MDkzOTg=","avatar_url":"https://avatars2.githubusercontent.com/u/5809398?v=4","gravatar_id":"","url":"https://api.github.com/users/alex-ozdemir","html_url":"https://github.com/alex-ozdemir","followers_url":"https://api.github.com/users/alex-ozdemir/followers","following_url":"https://api.github.com/users/alex-ozdemir/following{/other_user}","gists_url":"https://api.github.com/users/alex-ozdemir/gists{/gist_id}","starred_url":"https://api.github.com/users/alex-ozdemir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/alex-ozdemir/subscriptions","organizations_url":"https://api.github.com/users/alex-ozdemir/orgs","repos_url":"https://api.github.com/users/alex-ozdemir/repos","events_url":"https://api.github.com/users/alex-ozdemir/events{/privacy}","received_events_url":"https://api.github.com/users/alex-ozdemir/received_events","type":"User","site_admin":false},"repo":{"id":151121518,"node_id":"MDEwOlJlcG9zaXRvcnkxNTExMjE1MTg=","name":"CVC4","full_name":"alex-ozdemir/CVC4","private":false,"owner":{"login":"alex-ozdemir","id":5809398,"node_id":"MDQ6VXNlcjU4MDkzOTg=","avatar_url":"https://avatars2.githubusercontent.com/u/5809398?v=4","gravatar_id":"","url":"https://api.github.com/users/alex-ozdemir","html_url":"https://github.com/alex-ozdemir","followers_url":"https://api.github.com/users/alex-ozdemir/followers","following_url":"https://api.github.com/users/alex-ozdemir/following{/other_user}","gists_url":"https://api.github.com/users/alex-ozdemir/gists{/gist_id}","starred_url":"https://api.github.com/users/alex-ozdemir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/alex-ozdemir/subscriptions","organizations_url":"https://api.github.com/users/alex-ozdemir/orgs","repos_url":"https://api.github.com/users/alex-ozdemir/repos","events_url":"https://api.github.com/users/alex-ozdemir/events{/privacy}","received_events_url":"https://api.github.com/users/alex-ozdemir/received_events","type":"User","site_admin":false},"html_url":"https://github.com/alex-ozdemir/CVC4","description":"CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.","fork":true,"url":"https://api.github.com/repos/alex-ozdemir/CVC4","forks_url":"https://api.github.com/repos/alex-ozdemir/CVC4/forks","keys_url":"https://api.github.com/repos/alex-ozdemir/CVC4/keys{/key_id}","collaborators_url":"https://api.github.com/repos/alex-ozdemir/CVC4/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/alex-ozdemir/CVC4/teams","hooks_url":"https://api.github.com/repos/alex-ozdemir/CVC4/hooks","issue_events_url":"https://api.github.com/repos/alex-ozdemir/CVC4/issues/events{/number}","events_url":"https://api.github.com/repos/alex-ozdemir/CVC4/events","assignees_url":"https://api.github.com/repos/alex-ozdemir/CVC4/assignees{/user}","branches_url":"https://api.github.com/repos/alex-ozdemir/CVC4/branches{/branch}","tags_url":"https://api.github.com/repos/alex-ozdemir/CVC4/tags","blobs_url":"https://api.github.com/repos/alex-ozdemir/CVC4/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/alex-ozdemir/CVC4/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/alex-ozdemir/CVC4/git/refs{/sha}","trees_url":"https://api.github.com/repos/alex-ozdemir/CVC4/git/trees{/sha}","statuses_url":"https://api.github.com/repos/alex-ozdemir/CVC4/statuses/{sha}","languages_url":"https://api.github.com/repos/alex-ozdemir/CVC4/languages","stargazers_url":"https://api.github.com/repos/alex-ozdemir/CVC4/stargazers","contributors_url":"https://api.github.com/repos/alex-ozdemir/CVC4/contributors","subscribers_url":"https://api.github.com/repos/alex-ozdemir/CVC4/subscribers","subscription_url":"https://api.github.com/repos/alex-ozdemir/CVC4/subscription","commits_url":"https://api.github.com/repos/alex-ozdemir/CVC4/commits{/sha}","git_commits_url":"https://api.github.com/repos/alex-ozdemir/CVC4/git/commits{/sha}","comments_url":"https://api.github.com/repos/alex-ozdemir/CVC4/comments{/number}","issue_comment_url":"https://api.github.com/repos/alex-ozdemir/CVC4/issues/comments{/number}","contents_url":"https://api.github.com/repos/alex-ozdemir/CVC4/contents/{+path}","compare_url":"https://api.github.com/repos/alex-ozdemir/CVC4/compare/{base}...{head}","merges_url":"https://api.github.com/repos/alex-ozdemir/CVC4/merges","archive_url":"https://api.github.com/repos/alex-ozdemir/CVC4/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/alex-ozdemir/CVC4/downloads","issues_url":"https://api.github.com/repos/alex-ozdemir/CVC4/issues{/number}","pulls_url":"https://api.github.com/repos/alex-ozdemir/CVC4/pulls{/number}","milestones_url":"https://api.github.com/repos/alex-ozdemir/CVC4/milestones{/number}","notifications_url":"https://api.github.com/repos/alex-ozdemir/CVC4/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/alex-ozdemir/CVC4/labels{/name}","releases_url":"https://api.github.com/repos/alex-ozdemir/CVC4/releases{/id}","deployments_url":"https://api.github.com/repos/alex-ozdemir/CVC4/deployments","created_at":"2018-10-01T16:36:43Z","updated_at":"2018-12-07T21:34:46Z","pushed_at":"2018-12-10T21:40:27Z","git_url":"git://github.com/alex-ozdemir/CVC4.git","ssh_url":"git@github.com:alex-ozdemir/CVC4.git","clone_url":"https://github.com/alex-ozdemir/CVC4.git","svn_url":"https://github.com/alex-ozdemir/CVC4","homepage":null,"size":49989,"stargazers_count":0,"watchers_count":0,"language":"SMT","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":0,"license":{"key":"other","name":"Other","spdx_id":"NOASSERTION","url":null,"node_id":"MDc6TGljZW5zZTA="},"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"CVC4:master","ref":"master","sha":"41b38de8b059d346764cd5ca112740aa09e1d163","user":{"login":"CVC4","id":2973223,"node_id":"MDEyOk9yZ2FuaXphdGlvbjI5NzMyMjM=","avatar_url":"https://avatars0.githubusercontent.com/u/2973223?v=4","gravatar_id":"","url":"https://api.github.com/users/CVC4","html_url":"https://github.com/CVC4","followers_url":"https://api.github.com/users/CVC4/followers","following_url":"https://api.github.com/users/CVC4/following{/other_user}","gists_url":"https://api.github.com/users/CVC4/gists{/gist_id}","starred_url":"https://api.github.com/users/CVC4/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/CVC4/subscriptions","organizations_url":"https://api.github.com/users/CVC4/orgs","repos_url":"https://api.github.com/users/CVC4/repos","events_url":"https://api.github.com/users/CVC4/events{/privacy}","received_events_url":"https://api.github.com/users/CVC4/received_events","type":"Organization","site_admin":false},"repo":{"id":7040894,"node_id":"MDEwOlJlcG9zaXRvcnk3MDQwODk0","name":"CVC4","full_name":"CVC4/CVC4","private":false,"owner":{"login":"CVC4","id":2973223,"node_id":"MDEyOk9yZ2FuaXphdGlvbjI5NzMyMjM=","avatar_url":"https://avatars0.githubusercontent.com/u/2973223?v=4","gravatar_id":"","url":"https://api.github.com/users/CVC4","html_url":"https://github.com/CVC4","followers_url":"https://api.github.com/users/CVC4/followers","following_url":"https://api.github.com/users/CVC4/following{/other_user}","gists_url":"https://api.github.com/users/CVC4/gists{/gist_id}","starred_url":"https://api.github.com/users/CVC4/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/CVC4/subscriptions","organizations_url":"https://api.github.com/users/CVC4/orgs","repos_url":"https://api.github.com/users/CVC4/repos","events_url":"https://api.github.com/users/CVC4/events{/privacy}","received_events_url":"https://api.github.com/users/CVC4/received_events","type":"Organization","site_admin":false},"html_url":"https://github.com/CVC4/CVC4","description":"CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.","fork":false,"url":"https://api.github.com/repos/CVC4/CVC4","forks_url":"https://api.github.com/repos/CVC4/CVC4/forks","keys_url":"https://api.github.com/repos/CVC4/CVC4/keys{/key_id}","collaborators_url":"https://api.github.com/repos/CVC4/CVC4/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/CVC4/CVC4/teams","hooks_url":"https://api.github.com/repos/CVC4/CVC4/hooks","issue_events_url":"https://api.github.com/repos/CVC4/CVC4/issues/events{/number}","events_url":"https://api.github.com/repos/CVC4/CVC4/events","assignees_url":"https://api.github.com/repos/CVC4/CVC4/assignees{/user}","branches_url":"https://api.github.com/repos/CVC4/CVC4/branches{/branch}","tags_url":"https://api.github.com/repos/CVC4/CVC4/tags","blobs_url":"https://api.github.com/repos/CVC4/CVC4/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/CVC4/CVC4/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/CVC4/CVC4/git/refs{/sha}","trees_url":"https://api.github.com/repos/CVC4/CVC4/git/trees{/sha}","statuses_url":"https://api.github.com/repos/CVC4/CVC4/statuses/{sha}","languages_url":"https://api.github.com/repos/CVC4/CVC4/languages","stargazers_url":"https://api.github.com/repos/CVC4/CVC4/stargazers","contributors_url":"https://api.github.com/repos/CVC4/CVC4/contributors","subscribers_url":"https://api.github.com/repos/CVC4/CVC4/subscribers","subscription_url":"https://api.github.com/repos/CVC4/CVC4/subscription","commits_url":"https://api.github.com/repos/CVC4/CVC4/commits{/sha}","git_commits_url":"https://api.github.com/repos/CVC4/CVC4/git/commits{/sha}","comments_url":"https://api.github.com/repos/CVC4/CVC4/comments{/number}","issue_comment_url":"https://api.github.com/repos/CVC4/CVC4/issues/comments{/number}","contents_url":"https://api.github.com/repos/CVC4/CVC4/contents/{+path}","compare_url":"https://api.github.com/repos/CVC4/CVC4/compare/{base}...{head}","merges_url":"https://api.github.com/repos/CVC4/CVC4/merges","archive_url":"https://api.github.com/repos/CVC4/CVC4/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/CVC4/CVC4/downloads","issues_url":"https://api.github.com/repos/CVC4/CVC4/issues{/number}","pulls_url":"https://api.github.com/repos/CVC4/CVC4/pulls{/number}","milestones_url":"https://api.github.com/repos/CVC4/CVC4/milestones{/number}","notifications_url":"https://api.github.com/repos/CVC4/CVC4/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/CVC4/CVC4/labels{/name}","releases_url":"https://api.github.com/repos/CVC4/CVC4/releases{/id}","deployments_url":"https://api.github.com/repos/CVC4/CVC4/deployments","created_at":"2012-12-06T18:45:04Z","updated_at":"2018-12-10T16:37:19Z","pushed_at":"2018-12-10T21:40:28Z","git_url":"git://github.com/CVC4/CVC4.git","ssh_url":"git@github.com:CVC4/CVC4.git","clone_url":"https://github.com/CVC4/CVC4.git","svn_url":"https://github.com/CVC4/CVC4","homepage":null,"size":49496,"stargazers_count":239,"watchers_count":239,"language":"SMT","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":91,"mirror_url":null,"archived":false,"open_issues_count":225,"license":{"key":"other","name":"Other","spdx_id":"NOASSERTION","url":null,"node_id":"MDc6TGljZW5zZTA="},"forks":91,"open_issues":225,"watchers":239,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/2731"},"html":{"href":"https://github.com/CVC4/CVC4/pull/2731"},"issue":{"href":"https://api.github.com/repos/CVC4/CVC4/issues/2731"},"comments":{"href":"https://api.github.com/repos/CVC4/CVC4/issues/2731/comments"},"review_comments":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/2731/comments"},"review_comment":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/CVC4/CVC4/pulls/2731/commits"},"statuses":{"href":"https://api.github.com/repos/CVC4/CVC4/statuses/8d244c933a853b8483819d1b73ef5941e46cc96a"}},"author_association":"CONTRIBUTOR"}}
{"actor":{"display_login":"alex-ozdemir"}}