b4298e2 | Ranjit Jhala | 07 February 2019, 13:06:07 UTC | dont remove unfolded cands; not FULLY unfolded, cf ple3.fq | 07 February 2019, 13:06:07 UTC |
c34b3e0 | Ranjit Jhala | 07 February 2019, 12:54:30 UTC | asd | 07 February 2019, 12:54:30 UTC |
94c715c | Anish Tondwalkar | 05 February 2019, 11:22:50 UTC | needs scoping to terminate, as written | 05 February 2019, 11:26:06 UTC |
860cfd3 | Anish Tondwalkar | 05 February 2019, 10:48:24 UTC | rewrote Horn Eliminate to use cubes | 05 February 2019, 11:26:06 UTC |
b64b805 | Anish Tondwalkar | 05 February 2019, 09:55:30 UTC | Sketch out Eliminate on Horns | 05 February 2019, 09:55:30 UTC |
29ba825 | Anish Tondwalkar | 05 February 2019, 07:13:45 UTC | Add poke transformation | 05 February 2019, 07:13:45 UTC |
1a3f61a | Anish Tondwalkar | 05 February 2019, 04:47:40 UTC | Update .gitignore | 05 February 2019, 04:48:08 UTC |
624ae6f | Anish Tondwalkar | 05 February 2019, 04:43:48 UTC | Add option parsing to Horn Query files Right now it's just using the sexpr-ified version of the old fq, eg: (fixpoint "--option=value") but that can (should?) be changed to better conform to the smt2 spec | 05 February 2019, 04:48:08 UTC |
7fe3a4f | Anish Tondwalkar | 03 February 2019, 01:11:58 UTC | Add ebinds to Horn format This adds another constructor `Any` that mirrors `All, but is parsed in from an exists instead of a forall, and is translated to fq in the same way, except that variables bouned by `Any` are added to the fq's ebinds to indicate that they're existentially bound. | 03 February 2019, 04:56:56 UTC |
f0cba5f | Ranjit Jhala | 20 December 2018, 04:25:28 UTC | fixes #383 | 20 December 2018, 04:25:28 UTC |
d7d1d64 | Ranjit Jhala | 20 December 2018, 04:15:19 UTC | use fixpoint-loop in PLE | 20 December 2018, 04:15:19 UTC |
bc256f7 | Ranjit Jhala | 19 December 2018, 21:42:27 UTC | add fixpoint-loop to OLD PLE | 19 December 2018, 21:42:27 UTC |
91546f1 | Ranjit Jhala | 19 December 2018, 19:25:24 UTC | add minimal fq test showing ple get set bug | 19 December 2018, 19:25:24 UTC |
95456c1 | Ranjit Jhala | 19 December 2018, 05:01:13 UTC | remove debug | 19 December 2018, 05:01:13 UTC |
5b495e8 | Ranjit Jhala | 19 December 2018, 04:46:26 UTC | check isString when computing sortSmtSort | 19 December 2018, 04:46:26 UTC |
c86dbe4 | Ranjit Jhala | 18 December 2018, 23:55:31 UTC | sigh, declared victory too soon | 18 December 2018, 23:55:31 UTC |
f3a7f69 | Ranjit Jhala | 17 December 2018, 22:27:21 UTC | fix merge bugs | 17 December 2018, 22:27:21 UTC |
03d2a6a | Ranjit Jhala | 17 December 2018, 22:18:59 UTC | add final | 17 December 2018, 22:18:59 UTC |
dfcf0ec | Ranjit Jhala | 17 December 2018, 22:02:18 UTC | asd | 17 December 2018, 22:02:18 UTC |
59410b2 | Ranjit Jhala | 17 December 2018, 22:00:39 UTC | Merge pull request #382 from ucsd-progsys/incr-ple-debug Bug fix for Incr-PLE | 17 December 2018, 22:00:39 UTC |
f76fc0a | Ranjit Jhala | 16 December 2018, 18:12:29 UTC | remove debug | 16 December 2018, 18:12:29 UTC |
95fff16 | Ranjit Jhala | 16 December 2018, 18:08:06 UTC | asd | 16 December 2018, 18:08:06 UTC |
fd3f6d6 | Ranjit Jhala | 14 December 2018, 23:53:59 UTC | asd | 14 December 2018, 23:53:59 UTC |
7d0223f | Ranjit Jhala | 14 December 2018, 21:06:34 UTC | asd Merge branch 'develop' of github.com:ucsd-progsys/liquid-fixpoint into develop | 14 December 2018, 21:06:34 UTC |
d3f36f2 | Ranjit Jhala | 14 December 2018, 20:20:59 UTC | asd | 14 December 2018, 20:20:59 UTC |
68ee9fa | Ranjit Jhala | 14 December 2018, 17:10:14 UTC | asd | 14 December 2018, 17:10:14 UTC |
cd0ebe4 | Ranjit Jhala | 12 December 2018, 23:04:28 UTC | Merge pull request #381 from ucsd-progsys/ple-opt Incremental PLE | 12 December 2018, 23:04:28 UTC |
e9abf9b | Ranjit Jhala | 12 December 2018, 19:17:22 UTC | moved to incremental SMT | 12 December 2018, 19:17:22 UTC |
57a641b | Ranjit Jhala | 12 December 2018, 18:42:27 UTC | IMPL: incremental BGPUSH | 12 December 2018, 18:42:27 UTC |
aff8ebc | Ranjit Jhala | 12 December 2018, 18:18:34 UTC | NEXT: incremental BG-PUSH | 12 December 2018, 18:18:34 UTC |
8d0ed8c | Ranjit Jhala | 12 December 2018, 18:11:50 UTC | tests pass except wierd z3 SEGFAULT on DataBase.hs | 12 December 2018, 18:11:50 UTC |
a61cf93 | Ranjit Jhala | 12 December 2018, 17:27:03 UTC | incrementalPLE seems to also be a win; next use incremental Z3 contexts | 12 December 2018, 17:27:03 UTC |
0a850b4 | Ranjit Jhala | 12 December 2018, 05:36:14 UTC | See broken part | 12 December 2018, 05:36:14 UTC |
f42e2a2 | Ranjit Jhala | 11 December 2018, 18:55:47 UTC | next: tests/todo/ple-WHATSIT.bfq | 11 December 2018, 18:55:47 UTC |
49f0c0a | Ranjit Jhala | 06 December 2018, 20:47:26 UTC | ok, make incr-ple ACTUALLY incremental. | 06 December 2018, 20:47:26 UTC |
5f2eb0b | Ranjit Jhala | 06 December 2018, 20:32:06 UTC | actually do the diff | 06 December 2018, 20:32:06 UTC |
f861512 | Ranjit Jhala | 06 December 2018, 19:08:21 UTC | fp tests pass FWIW | 06 December 2018, 19:08:21 UTC |
cd9dfa3 | Ranjit Jhala | 06 December 2018, 18:26:05 UTC | incr-ple typechecks. | 06 December 2018, 18:26:05 UTC |
54ecfb2 | Ranjit Jhala | 06 December 2018, 17:41:23 UTC | restore the asserts stuff | 06 December 2018, 17:41:23 UTC |
2826877 | Ranjit Jhala | 06 December 2018, 04:43:24 UTC | next, RESTORE that AXIOM stuff.. yuck. | 06 December 2018, 04:43:24 UTC |
b742b0b | Ranjit Jhala | 06 December 2018, 03:49:01 UTC | next, hookup instT | 06 December 2018, 03:49:01 UTC |
ccaacba | Ranjit Jhala | 05 December 2018, 23:36:07 UTC | next, hookup instT | 05 December 2018, 23:36:07 UTC |
cd847dd | Ranjit Jhala | 05 December 2018, 20:58:51 UTC | asd | 05 December 2018, 20:58:51 UTC |
d58bc42 | Niki Vazou | 05 December 2018, 14:14:06 UTC | Merge pull request #380 from ucsd-progsys/smtTimeout add smttimout flag | 05 December 2018, 14:14:06 UTC |
dbf32cc | Niki Vazou | 05 December 2018, 13:49:33 UTC | suppress warning | 05 December 2018, 13:49:33 UTC |
3a6aefb | Ranjit Jhala | 04 December 2018, 22:13:03 UTC | asd | 04 December 2018, 22:13:03 UTC |
202f482 | Niki Vazou | 04 December 2018, 19:10:06 UTC | add smttimout flag | 04 December 2018, 19:10:06 UTC |
fb6740a | Ranjit Jhala | 28 November 2018, 21:11:28 UTC | asd Merge branch 'develop' of github.com:ucsd-progsys/liquid-fixpoint into develop | 28 November 2018, 21:11:28 UTC |
6bc2414 | Niki Vazou | 22 November 2018, 11:04:48 UTC | Merge pull request #379 from ucsd-progsys/ReplacePruneUnsorted add template code that only checks to prune out predicates that match… | 22 November 2018, 11:04:48 UTC |
d3f2e48 | nikivazou | 22 November 2018, 08:32:44 UTC | export filtering function | 22 November 2018, 08:32:44 UTC |
595c15a | nikivazou | 21 November 2018, 18:01:36 UTC | add templates in cabal | 21 November 2018, 18:01:36 UTC |
f120196 | nikivazou | 21 November 2018, 17:52:51 UTC | add template code that only checks to prune out predicates that match the templates | 21 November 2018, 17:52:51 UTC |
b09e490 | Niki Vazou | 27 October 2018, 00:48:22 UTC | Merge pull request #377 from ucsd-progsys/muDataDefinition push mu transformation just before SMT printing | 27 October 2018, 00:48:22 UTC |
52bb642 | nikivazou | 26 October 2018, 22:44:23 UTC | Merge branch 'develop' of https://github.com/ucsd-progsys/liquid-fixpoint into HEAD | 26 October 2018, 22:44:23 UTC |
c125f9d | nikivazou | 26 October 2018, 22:40:19 UTC | push mu transformation just before SMT printing | 26 October 2018, 22:40:19 UTC |
98ae3ba | Ranjit Jhala | 26 October 2018, 19:29:35 UTC | update README | 26 October 2018, 19:29:35 UTC |
a5ab379 | Ranjit Jhala | 26 October 2018, 19:01:07 UTC | update README | 26 October 2018, 19:01:07 UTC |
cfc51fc | Ranjit Jhala | 26 October 2018, 18:42:27 UTC | Merge pull request #376 from ucsd-progsys/nnf Add support for solving Horn/NNF constraints | 26 October 2018, 18:42:27 UTC |
6116e6e | Ranjit Jhala | 26 October 2018, 16:49:06 UTC | add first proper kvar/qual test | 26 October 2018, 16:49:06 UTC |
5f4d80d | Ranjit Jhala | 26 October 2018, 02:56:04 UTC | update circle stuff | 26 October 2018, 02:56:04 UTC |
dcb0d27 | Ranjit Jhala | 26 October 2018, 02:52:46 UTC | some horn-kvar tests pass | 26 October 2018, 02:52:46 UTC |
4faaeb0 | Ranjit Jhala | 25 October 2018, 22:38:05 UTC | yay, some horn/.smt2 style tests pass. | 25 October 2018, 22:38:05 UTC |
d05bd13 | Ranjit Jhala | 25 October 2018, 22:23:45 UTC | ok, does it float? | 25 October 2018, 22:23:45 UTC |
a4e2d7d | Ranjit Jhala | 25 October 2018, 20:59:42 UTC | nuke smt2 | 25 October 2018, 20:59:42 UTC |
a935803 | Ranjit Jhala | 25 October 2018, 19:24:53 UTC | asd | 25 October 2018, 19:24:53 UTC |
498def5 | Ranjit Jhala | 25 October 2018, 18:54:07 UTC | init convert from NNF into plain FInfo | 25 October 2018, 18:54:07 UTC |
d681463 | Ranjit Jhala | 24 October 2018, 22:09:39 UTC | Asd | 24 October 2018, 22:09:39 UTC |
f587bf3 | Ranjit Jhala | 10 October 2018, 16:08:55 UTC | Merge pull request #374 from ucsd-progsys/phadej-ghc-8.4 Phadej ghc 8.4 | 10 October 2018, 16:08:55 UTC |
5fb22d4 | Ranjit Jhala | 09 October 2018, 18:48:21 UTC | remove all tracepp | 09 October 2018, 18:48:21 UTC |
2b1eef3 | Ranjit Jhala | 06 October 2018, 17:05:57 UTC | keep all HO binders around | 06 October 2018, 17:05:57 UTC |
4ded098 | Ranjit Jhala | 27 September 2018, 19:45:56 UTC | asd | 27 September 2018, 19:45:56 UTC |
7e2fd8e | Ranjit Jhala | 12 September 2018, 17:02:34 UTC | Use (Ord Text) instance for comparing Symbol | 12 September 2018, 17:02:34 UTC |
5f84de2 | Ranjit Jhala | 12 September 2018, 07:05:27 UTC | Ord Symbol must be prefix-monotonic | 12 September 2018, 07:05:27 UTC |
3d22296 | Ranjit Jhala | 06 September 2018, 13:24:39 UTC | yay, Fulcrum.hs works | 06 September 2018, 13:24:39 UTC |
2898024 | Ranjit Jhala | 30 August 2018, 18:12:45 UTC | pprint Bspec | 30 August 2018, 18:12:45 UTC |
8652ab7 | Ranjit Jhala | 23 August 2018, 04:24:38 UTC | whoa, changing Subable instance for RType | 23 August 2018, 04:24:38 UTC |
80926e1 | Anish Tondwalkar | 20 August 2018, 23:10:53 UTC | Merge pull request #375 from ucsd-progsys/circle2 Upgrade to circle2 | 20 August 2018, 23:10:53 UTC |
2520646 | Anish Tondwalkar | 14 August 2018, 19:22:26 UTC | Upgrade to circle2 | 14 August 2018, 19:22:26 UTC |
22a8bd4 | Ranjit Jhala | 12 August 2018, 11:45:44 UTC | disable termination till done | 12 August 2018, 11:45:44 UTC |
f290616 | Ranjit Jhala | 11 August 2018, 14:12:33 UTC | cleanup cabal | 11 August 2018, 14:12:33 UTC |
78b28e5 | Ranjit Jhala | 10 August 2018, 12:57:52 UTC | add sets tests | 10 August 2018, 12:57:52 UTC |
5a4c8d6 | Ranjit Jhala | 10 August 2018, 04:06:46 UTC | add sets tests | 10 August 2018, 04:06:46 UTC |
b4dadb7 | Ranjit Jhala | 03 August 2018, 19:38:43 UTC | twiddle | 03 August 2018, 19:38:43 UTC |
58291d2 | Ranjit Jhala | 31 July 2018, 19:46:57 UTC | cleanup cabal | 31 July 2018, 19:46:57 UTC |
914109b | Ranjit Jhala | 31 July 2018, 19:03:27 UTC | merged in phadej edits | 31 July 2018, 19:03:27 UTC |
47934d4 | Ranjit Jhala | 31 July 2018, 18:25:46 UTC | done: lifted measure imports | 31 July 2018, 18:25:46 UTC |
6b31e84 | Oleg Grenrus | 09 June 2018, 11:25:11 UTC | Add Semigroups support Make base >=4.9.1.0 lower bound (GHC-8.0.2) which let us simplify in various places | 30 July 2018, 10:56:10 UTC |
771d615 | Ranjit Jhala | 24 July 2018, 23:18:04 UTC | yay first round of rebare tests pass | 24 July 2018, 23:18:04 UTC |
42c76e7 | Ranjit Jhala | 24 July 2018, 19:10:55 UTC | don't pprint casts | 24 July 2018, 19:10:55 UTC |
1708c26 | Ranjit Jhala | 16 July 2018, 17:07:51 UTC | add gfp examples | 16 July 2018, 17:07:51 UTC |
3e73255 | Ranjit Jhala | 13 July 2018, 20:23:35 UTC | done: nuke Liquid.Model | 13 July 2018, 20:23:35 UTC |
a50055b | Ranjit Jhala | 27 June 2018, 22:35:54 UTC | looks like LF works with 8.4 | 27 June 2018, 22:35:54 UTC |
83a0bc6 | Ranjit Jhala | 27 June 2018, 22:34:48 UTC | looks like LF works with 8.4 | 27 June 2018, 22:34:48 UTC |
6e42a84 | Ranjit Jhala | 27 June 2018, 22:31:39 UTC | onto testparser | 27 June 2018, 22:31:39 UTC |
9d2694a | Ranjit Jhala | 27 June 2018, 15:12:28 UTC | Merge pull request #373 from ucsd-progsys/T1336 Sensible SrcSpan during Elaborate and SortCheck | 27 June 2018, 15:12:28 UTC |
96a8771 | Ranjit Jhala | 26 June 2018, 21:54:53 UTC | track measure-kind to re-establish failing checks | 26 June 2018, 21:54:53 UTC |
03a32b9 | Ranjit Jhala | 26 June 2018, 20:33:01 UTC | twiddle | 26 June 2018, 20:33:01 UTC |
08844db | Ranjit Jhala | 26 June 2018, 19:57:01 UTC | done with fixpoint | 26 June 2018, 19:57:01 UTC |
432cfd4 | Ranjit Jhala | 26 June 2018, 18:30:57 UTC | done with fixpoint | 26 June 2018, 18:30:57 UTC |
d53f697 | Ranjit Jhala | 26 June 2018, 18:14:46 UTC | done with Solver/Solution.hs | 26 June 2018, 18:14:46 UTC |