Commit graph

137 commits

Author SHA1 Message Date
Leonardo de Moura
f08c06d582 Add head_beta tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-23 09:42:49 -07:00
Soonho Kong
ca779265e5 Update src/CMakeLists.txt to increase stack size for windows build
[skip ci]
2013-08-22 21:16:57 -07:00
Leonardo de Moura
0f6a7e4a95 Rename exprlib to library. Name was misleading, it is more than a library for manipulating expressions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-22 10:26:52 -07:00
Leonardo de Moura
bd3b422158 Add support for READLINE. Remark: it is not enabled by default. Rename tcmalloc option to TCMALLOC (using consistent name convention for cmake parameters).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 19:08:44 -07:00
Leonardo de Moura
d750469667 Move frontend to frontends/lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 09:04:49 -07:00
Soonho Kong
3b0a7a2d96 Update src/CMakeLists.txt to include 'TESTCOV' build 2013-08-17 20:58:05 -07:00
Leonardo de Moura
d6d221b992 Move auxiliary files away from kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Leonardo de Moura
2ea7479ee9 Move sexpr/format/options to util/sexpr (reason: circular dependency between util and numerics lib), now numerics depend on util, and sexpr depends on numerics and util. Add scanner to frontend.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 03:40:51 -07:00
Leonardo de Moura
ac38937241 Remove parsers directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 01:25:42 -07:00
Soonho Kong
30e34528f6 Use lowercases in src/CMakeLists.txt 2013-08-13 00:35:14 -07:00
Leonardo de Moura
68ca5d84e2 Remove unnecessary '--' in status messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 15:37:36 -07:00
Leonardo de Moura
7778541422 Send status messages to standard output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 14:56:40 -07:00
Soonho Kong
2b6d8a4d01 Update CMakeLists.txt to support OSX + Clang 2013-08-12 10:58:07 -07:00
Leonardo de Moura
6cb46d9de7 Remove Flex/Bison requirement, we will not use them.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-11 18:09:47 -07:00
Leonardo de Moura
f79c0d3546 Add support for cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
9fbe99bf58 Rename define_uv -> add_uvar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
f18149934b Move sexpr to util directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-08 18:38:18 -07:00
Soonho Kong
59ec8357f4 Require GMP version 5.0.5 2013-08-06 19:55:34 -07:00
Soonho Kong
8dab224137 Fix CMakeLists.txt 2013-08-05 19:16:52 -07:00
Soonho Kong
a6f825caa5 Add MPFR & restructure cmake directory 2013-08-05 17:58:54 -07:00
Leonardo de Moura
b979436c40 Add basic semantic attachments for arithmetic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 19:57:06 -07:00
Leonardo de Moura
b67a92cf10 Add scanner base class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:10:20 -07:00
Leonardo de Moura
ae697ddda7 Update CMakeLists.txt: bison++ and flex
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-02 07:56:18 -07:00
Leonardo de Moura
c2ebe42ca8 Move numerics and sexpr to util
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-24 14:57:51 -07:00
Leonardo de Moura
c32dfe22b6 Add expressions (dependent type theory)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-22 12:46:11 -07:00
Leonardo de Moura
05991c827b Add S-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-20 17:22:13 -07:00
Leonardo de Moura
63e596885c Add support for (soft) interrupts
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-19 19:12:55 -07:00
Leonardo de Moura
a0908ba3c5 Add missing library, the interval library contains the explicit instantiation of interval<mpq> and interval<double>
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-19 14:18:18 -07:00
Leonardo de Moura
4e3dc83621 have separate cmake files for GMP and Tcmalloc
Conflicts:
	src/CMakeLists.txt
2013-07-19 10:04:00 -07:00
Leonardo de Moura
5063c8cfa1 Add interval template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-19 10:01:53 -07:00
Leonardo de Moura
5de8b3a8ee Add support for tcmalloc
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-19 10:01:32 -07:00
Leonardo de Moura
8353181fd1 Add basic mpq tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-18 11:10:15 -07:00
Leonardo de Moura
e559bf73a9 Add basic testing infrastructure using CTest
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-18 09:12:07 -07:00
Leonardo de Moura
4ccf770b64 Move mpz, mpq and mpbq to numerics directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-17 14:33:00 -07:00
Leonardo de Moura
c0f9f06d70 Set clang++ as default compiler. Add -pthread as a linker flag
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-17 12:41:28 -07:00
Leonardo de Moura
501f63e27d Add build instructions. Improve build.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-16 22:32:21 -07:00
Leonardo de Moura
139f4f2a7f Add simple build system based on cmake
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-16 22:10:51 -07:00