Skip to main content

Browse the archive

sort by:
Revision Author Date Message Commit Date
84dab94 Ranjit Jhala 13 February 2019, 01:47:37 UTC only eval partial appls if Ok 13 February 2019, 01:47:37 UTC
aa8ecc6 Ranjit Jhala 13 February 2019, 00:02:39 UTC banging head against mossaka bug 13 February 2019, 00:02:39 UTC
6d17b8a Ranjit Jhala 12 February 2019, 19:24:00 UTC add MJ test 12 February 2019, 19:24:00 UTC
60df75e Anish Tondwalkar 12 February 2019, 09:40:34 UTC make poke use pivars instead of reusing the ebind 12 February 2019, 09:40:34 UTC
4605e7f Ranjit Jhala 12 February 2019, 07:44:37 UTC asd 12 February 2019, 07:44:37 UTC
5096722 Ranjit Jhala 12 February 2019, 07:14:33 UTC temp checkin: missing sort 12 February 2019, 07:14:33 UTC
62e9c57 Ranjit Jhala 12 February 2019, 04:04:53 UTC don't generate equations for data-constructors 12 February 2019, 04:04:53 UTC
43076c4 Ranjit Jhala 12 February 2019, 00:22:18 UTC aha, add binders for ... binders 12 February 2019, 00:22:18 UTC
a7becfd Anish Tondwalkar 11 February 2019, 18:54:31 UTC Add tests from ICFP paper for eliminate=horn 11 February 2019, 18:55:49 UTC
5d3d171 Anish Tondwalkar 10 February 2019, 00:18:41 UTC Pretty Print constraints 11 February 2019, 18:55:49 UTC
e9df778 Anish Tondwalkar 09 February 2019, 23:08:29 UTC Add command line flags for Horn transformations --eliminate=horn now runs eliminate on the NFF HC --eliminate=some is now the default for solveHorn -v --eliminate=horn prints out the uniqified and eliminated NNF HC 11 February 2019, 18:55:49 UTC
b60c46c Anish Tondwalkar 09 February 2019, 05:20:15 UTC implement uniq pass on horn 11 February 2019, 18:55:49 UTC
eec773f Ranjit Jhala 10 February 2019, 02:14:36 UTC Merge pull request #389 from ucsd-progsys/T1371 Update no-eval-ite for mutrec functions 10 February 2019, 02:14:36 UTC
7870d9e Ranjit Jhala 10 February 2019, 01:30:04 UTC update no-eval-ite for mutrec functions 10 February 2019, 01:30:04 UTC
6fb5657 Ranjit Jhala 10 February 2019, 00:06:44 UTC Merge pull request #388 from ucsd-progsys/T1371 T1371 10 February 2019, 00:06:44 UTC
f60841d Ranjit Jhala 09 February 2019, 23:03:00 UTC next: fix StlcBug and T1371 09 February 2019, 23:03:00 UTC
e5737f5 Ranjit Jhala 09 February 2019, 22:37:02 UTC don't eval recursive-funs under unknown guard 09 February 2019, 22:37:02 UTC
27ad9b6 Ranjit Jhala 08 February 2019, 23:23:03 UTC Disable tracpp 08 February 2019, 23:23:03 UTC
7bdce09 Ranjit Jhala 08 February 2019, 20:05:15 UTC temp checkin 08 February 2019, 20:05:15 UTC
1411b21 Ranjit Jhala 08 February 2019, 17:04:50 UTC about to add 'stack' to eval 08 February 2019, 17:04:50 UTC
8c10920 Anish Tondwalkar 08 February 2019, 12:30:02 UTC Fixed substitutions in Horn/elim 08 February 2019, 12:30:02 UTC
54797c1 Anish Tondwalkar 07 February 2019, 23:57:23 UTC Start debugging Horn.elim 07 February 2019, 23:57:23 UTC
0ac8aec Ranjit Jhala 07 February 2019, 23:31:37 UTC don't eval under unknown guard. sigh. 07 February 2019, 23:31:37 UTC
d4ca29f Ranjit Jhala 07 February 2019, 22:03:47 UTC don't eval under unknown guard. sigh. 07 February 2019, 22:03:47 UTC
50ad58d Ranjit Jhala 07 February 2019, 21:50:18 UTC merged in reflect-string 07 February 2019, 21:50:18 UTC
78ac477 Ranjit Jhala 07 February 2019, 21:32:36 UTC yuck 07 February 2019, 21:32:36 UTC
683e85c Ranjit Jhala 07 February 2019, 21:26:27 UTC add minimal test 07 February 2019, 21:26:27 UTC
983264c Ranjit Jhala 07 February 2019, 20:46:38 UTC add minimal test 07 February 2019, 20:46:38 UTC
a91c833 Ranjit Jhala 07 February 2019, 17:34:30 UTC Merge pull request #385 from ucsd-progsys/T1409 T1409 07 February 2019, 17:34:30 UTC
9f4df57 Ranjit Jhala 07 February 2019, 14:31:58 UTC fixes liquidhaskell/#1409 07 February 2019, 14:31:58 UTC
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
back to top