max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
8740 commits 1 branch 0 tags 5.3 GiB
Commit graph

658 commits

Author SHA1 Message Date
Leonardo de Moura
11b63b0fcd fix(util/small_object_allocator): warning 2016-05-13 15:20:32 -07:00
Leonardo de Moura
92bc367c5c feat(util): add small object allocator 2016-05-13 14:41:31 -07:00
Leonardo de Moura
5189a83f57 feat(library/vm): pretty print bytecode 2016-05-11 16:57:56 -07:00
Leonardo de Moura
906c4f86f1 feat(library/vm): add vm_decl(s) 2016-05-10 21:11:07 -07:00
Leonardo de Moura
7641b602ca chore(util): fun_array ==> parray 2016-05-10 16:05:41 -07:00
Leonardo de Moura
6cb8e82fef feat(util/fun_array): add functional array 2016-05-09 17:40:26 -07:00
Leonardo de Moura
889bdec2f7 feat(util/rb_tree): add unsigned_rev_cmp 2016-05-01 19:30:51 -07:00
Leonardo de Moura
a823b0e6ec feat(library/type_context): pop_local for type_context 2016-03-09 10:22:48 -08:00
Leonardo de Moura
c8e5907b70 feat(util/rb_tree,util/rb_map): add back_find_if 2016-03-05 13:29:34 -08:00
Leonardo de Moura
82fb38b440 feat(util/rb_tree): add for_each_greater 2016-03-01 15:42:27 -08:00
Leonardo de Moura
2982db6f80 feat(library/local_context): add new local context type 2016-03-01 13:40:37 -08:00
Lev Nachmanson
23079a75a7 dev(lp): fix build for clang, avoid clang-3.3 bug, cleanup permutation_matrix 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-26 16:07:16 -08:00
Leonardo de Moura
9b15c4c669 feat(util/rb_map): add find_if 2016-02-24 16:02:16 -08:00
Soonho Kong
431ce6ff2d fix(util/lp): instantiate missing functions 
close #1005
 2016-02-22 16:19:28 -05:00
Leonardo de Moura
c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name 2016-02-11 18:05:57 -08:00
Leonardo de Moura
f67181baf3 chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
Leonardo de Moura
6c1c6cbbdd fix(util/lp,tests/util/lp): warning msgs on OSX 2016-02-05 11:51:20 -08:00
Leonardo de Moura
1c8d8da9cf chore(util/lp/lp_primal_core_solver): fix warning 2016-02-05 10:08:32 -08:00
Lev Nachmanson
0e4f98dc47 dev(lp): remove a warning 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:08:24 -08:00
Lev Nachmanson
a7e3befd21 dev(lp): speed up primal with sorted list 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:36 -08:00
Lev Nachmanson
ff8213a6a9 dev(lp): diminish the number of pivots of primal by sorting the columns 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
61eaef0183 dev(lp): improve the dual perormance 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
9482d508df dev(lp): fix bugs in the dual simplex high loop 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
fbe4f56aea chore(lp): remove warnings 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Leonardo de Moura
40d4623219 fix(util/lp/lp_settings): replace fabs with std::abs 2016-02-05 10:04:35 -08:00
Leonardo de Moura
971ec72157 fix(util/lp/numeric_pair): include cmath 2016-02-05 10:04:35 -08:00
Lev Nachmanson
504c603af4 chore(lp): use std::ostream for printing routines 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
fc858d98c0 chore(lp): improve formatting 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
e9cd621855 chore(lp): improve formatting 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
28bf891b7f dev(lp): port to windows (msys2) 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
99dcad0dda dev(lp): performance tuning in find_leaving_on_harris_theta 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:35 -08:00
Lev Nachmanson
d098dfe326 dev(lp): fix infeasibility evidence check 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:34 -08:00
Leonardo de Moura
d9acf90f7b refactor(util/lp): use Lean exception 2016-02-05 10:04:34 -08:00
Leonardo de Moura
8fbf66d01a chore(util/lp): no "using", indentation 2016-02-05 10:04:34 -08:00
Leonardo de Moura
1841d17544 refactor(lp): NDEBUG ==> LEAN_DEBUG 2016-02-05 10:04:34 -08:00
Lev Nachmanson
fbb3ed8911 feat(lp): add LP solver and incremental LU factorization 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-05 10:04:34 -08:00
Leonardo de Moura
f62e22b34c fix(util/sexpr/format): fixes #955 
Lean was crashing because separate_tokes was traversing a DAG as a tree.
Lean was dying without memory (and getting stack overflows) because the procedure was also converting
the DAG into a tree.

This example also suggests we should reduce the limits for the pretty printer.
 2016-02-04 14:55:11 -08:00
Leonardo de Moura
bd52e58294 perf(util/name): use quick_cmp at name_pair_quick_cmp 2016-02-02 13:56:02 -08:00
Leonardo de Moura
cb203c3272 perf(src/util/name): if the hashcodes are equal, then there is a high probability the names are equal 
So, we use == before trying cmp.
Reason: == is much faster.
 2016-02-02 12:52:06 -08:00
Leonardo de Moura
a9cb9ff912 perf(util/name): more inlining 2016-02-02 09:49:50 -08:00
Leonardo de Moura
187bce307e perf(src/util/name): inline hash 2016-02-02 09:21:01 -08:00
Gabriel Ebner
7e11c5cf6e fix(src/util/file_lock): ignore failure to create locks on read-only file systems 
EACCES is already ignored when creating lock files.  In this case we
assume that the file to be locked is part of the system-wide
installation.  On NixOS however, the file system containing system
packages is mounted read-only, and open(2) returns EROFS.
 2016-01-16 11:00:44 -08:00
Soonho Kong
f911747b60 fix(util/file_lock.cpp): add 'include <fcntl.h>' 
@wizardbc found that this is needed while working on lean.js.
I think it's because of the use of O_CREAT in open system call.

Related issue: leanprover/lean.js#10
 2015-12-19 07:51:00 -05:00
Leonardo de Moura
45dbf76df9 refactor(library): add attribute manager 2015-12-17 20:58:15 -08:00
Leonardo de Moura
c07345d47f fix(util/file_lock): handle permission denied at lock creation 
see #925

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-12-15 09:48:20 -08:00
Leonardo de Moura
521657914c chore(util/file_lock): style 2015-12-14 10:20:33 -08:00
Leonardo de Moura
31c9a76777 feat(util/file_lock): add support for Windows 
Remark: the lock are not being erased on Windows.
I tried different solutions based on MoveFileEx and DeleteFile.
None of them worked. The one based on MoveFileEx

        MoveFileEx(m_fname.c_str(), NULL, MOVEFILE_DELAY_UNTIL_REBOOT);

seems to delete the file after REBOOT.
But, this is not very useful.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-12-14 10:07:26 -08:00
Leonardo de Moura
4dc3764a02 feat(util,library,shell): basic locking mechanism 
We still have to test on Windows.
see issue #925
 2015-12-12 21:26:13 -08:00
Leonardo de Moura
cbc3c0cf4f feat(frontends/lean): suppress profiling information for declarations that take less than 0.01 secs to be processed 2015-12-09 10:48:36 -08:00
Leonardo de Moura
370f9a6eec fix(library/trace): use null output channel when trace environment is not set 
This is important when multiple threads are being used, and the trace
environment is not set for a child thread
 2015-12-08 18:37:57 -08:00