Commit Graph

10 Commits

Author SHA1 Message Date
kr.angelov
1e44fdb3d3 fixes in the C and Python API to make them closer to the Haskell API 2013-08-16 12:44:37 +00:00
kr.angelov
c0a0859566 C runtime: fix the debug modes in the parser and in the reasoner after the changes in the printer 2013-06-27 11:00:26 +00:00
kr.angelov
a2af8e216f an optimization in the jitter for generating more compact code 2013-06-26 09:03:51 +00:00
kr.angelov
d553cb165a Now there is a just-in-time compiler which generates native code for proof search. This is already used by the exhaustive generator. The time to generate 10000 abstract trees with ParseEng went down from 4.43 sec to 0.29 sec. 2013-06-25 19:22:42 +00:00
kr.angelov
aad274022a a trivial refactoring of the reasoner in the C runtime 2013-04-23 06:40:14 +00:00
kr.angelov
90c3304147 remove the pgf2yaml tool which was both broken and redundant. The declarations for generic programming from data.c are removed as well 2013-02-11 13:51:12 +00:00
kr.angelov
2c169406fc a new reasoner in the C runtime. It supports tabling which makes it decideable for propositional logic. dependent types and high-order types are not supported yet. The generation is still in decreasing probability order 2013-01-07 12:50:32 +00:00
kr.angelov
d12c604f9a debugging infrastructure in the reasoner 2012-12-14 21:25:00 +00:00
kr.angelov
16a2c38f38 bugfix for the reasoner in the C runtime 2012-12-14 21:24:17 +00:00
kr.angelov
20aaa4a989 The first prototype for exhaustive generation in the C runtime. The trees are always listed in decreasing probability order. There is also an API for generation from Python 2012-12-14 15:32:49 +00:00