{"push_id":843396620,"size":3,"distinct_size":3,"ref":"refs/heads/master","head":"c5c921ec7408a1c1264df5a4cb257c96db2905de","before":"7c4c7b655f7b9d4373bd7c12017fdfc350d4a8c0","commits":[{"sha":"54f7815f4fcbb4c1e2c3ac987a21208879d050d2","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"refactor(constraint): ode_constraint get a vector<shared_ptr<forallt_constraint>>","distinct":true,"url":"https://api.github.com/repos/soonhokong/dreal3/commits/54f7815f4fcbb4c1e2c3ac987a21208879d050d2"},{"sha":"1b9dc8a195e652d054a48f225b82a75b21cea3db","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"refactor(contractor/contractor_capd4.cpp): have a list of ctcs for invariants\n\nPreviously, we create a contractor for mode invariants when a CAPD4\ncontractor is created. This turns out to be problematic because there\nare unasserted/asserted forallt literals and we need to get the\ninformation when we do *check*.\n\nIn the new code, we prepare a list of contractors for each forallt\nconstrains in construction time. Then, when we check, we lookup the\npolarity of each forallt literal and only used the asserted ones.","distinct":true,"url":"https://api.github.com/repos/soonhokong/dreal3/commits/1b9dc8a195e652d054a48f225b82a75b21cea3db"},{"sha":"c5c921ec7408a1c1264df5a4cb257c96db2905de","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"test(nra_ode): add mode_inv_01.smt2","distinct":true,"url":"https://api.github.com/repos/soonhokong/dreal3/commits/c5c921ec7408a1c1264df5a4cb257c96db2905de"}]}