Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Replace queue.h with pdeque.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix bugs in pvector. Improve test driver

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add support for writing a[i] = v instead of a.set(i, v) in the pvector class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix warnings

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Move sexpr_funcs to sexpr_fn. Using consistent file name conventions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Use fullpath in #include directives.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Rename lean frontend files. The prefix lean_ is not necessary anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Update README.md

put http://build.leanprover.net
[skip ci]
Update .travis.yml

move triggers from 1st conf. to 4th conf to balance loads
[skip ci]
Use fullpath in #include directives, add missing STL headers
Rename arith library files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Use consistent names for import functions, and library files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Rename import_all. The idea is to use consistent name for library files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Rename numtype.h to num_type.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Update .travis.yml

trigger only if the repo is blessed one
[skip ci]