fdc9f6a | Anish Tondwalkar | 16 February 2019, 21:09:57 UTC | Horn solve ebs - sketch/build out control flow - fix poke and sides - add elimPis, elimKs - start work on QE | 16 February 2019, 21:09:57 UTC |
46dfead | Ranjit Jhala | 13 February 2019, 05:18:55 UTC | Merge pull request #390 from ucsd-progsys/missing-sort Two bug fixes | 13 February 2019, 05:18:55 UTC |
d370604 | Ranjit Jhala | 13 February 2019, 04:58:34 UTC | TODO: add mossaka.fq test | 13 February 2019, 04:58:34 UTC |
13a0a7e | Ranjit Jhala | 13 February 2019, 03:20:22 UTC | only eval partial appls if Ok | 13 February 2019, 03:20:22 UTC |
7ae5906 | Ranjit Jhala | 13 February 2019, 03:13:49 UTC | only eval partial appls if Ok | 13 February 2019, 03:13:49 UTC |
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 |