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