Commit graph

499 commits

Author SHA1 Message Date
Leonardo de Moura
0d10cba4a0 refactor(util/sexpr/format): minimize the use of recursion, combine be and layout into a single procedure (without creating a temporary potentially big sexpr)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 21:06:24 -08:00
Leonardo de Moura
25b812f1c9 feat(kernel/expr): no overhead optional<expr> template specialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 10:17:29 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 23:21:10 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 15:11:55 -08:00
Leonardo de Moura
d949dfd46d fix(util/stackinfo): compilation warning on cygwin/mingw
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 11:32:39 -08:00
Leonardo de Moura
fa35fd6989 chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly
When LEAN_THREAD_UNSAFE=ON, we:

- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 10:27:22 -08:00
Leonardo de Moura
1a02abf7b2 feat(util/script_state): add a lua hook function that checks for the interrupt flag
This is a very convenient feature for interrupting non-terminating user scripts.
Before this commit, the user had to manually invoke check_interrupt() in potentially expensive loops. Now, this is not needed anymore.

Remark: we still have to check whether this trick works with LuaJIT or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 09:57:36 -08:00
Leonardo de Moura
ef6a27fe84 feat(util/script_state): add join method to Lua threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 09:15:09 -08:00
Leonardo de Moura
def186a9cd fix(util/stackinfo): try to fix incorrect main thread stack size on OSX
This fix tries to fix two failures on our unit tests.
     tests/kernel/normalizer
     tests/kernel/type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 08:56:46 -08:00
Leonardo de Moura
fd9781d58d fix(util/stackinfo): compilation warning on mingw and cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 08:26:50 -08:00
Leonardo de Moura
f80106a895 chore(*): use 'explicit operator bool' everywhere.
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 23:02:45 -08:00
Leonardo de Moura
39b99683a8 fix(util/stackinfo): handle error codes in the Linux version
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 07:56:53 -08:00
Soonho Kong
31b26f53ad fix(util/stackinfo): fix typo 2013-12-02 00:03:57 -05:00
Soonho Kong
7776f4b24b fix(util/stackinfo): fix preprocessor directive 2013-12-01 23:44:58 -05:00
Soonho Kong
4de3b772fd feat(util/stackinfo): implement get_stack_size (Mac OSX version) 2013-12-01 22:24:12 -05:00
Leonardo de Moura
75f8d56eb1 fix(util/stackinfo): memory leak at get_stack_size
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 19:17:28 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 17:19:27 -08:00
Leonardo de Moura
737e634556 fix(util/list): bug in map template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 08:51:24 -08:00
Leonardo de Moura
7ff791eb9f feat(util/name_set): add mk_unique (with respect to a name_set)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 11:28:38 -08:00
Leonardo de Moura
6da13cc245 feat(util/list): map_append template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 11:28:38 -08:00
Leonardo de Moura
fe79bbf2b7 feat(util/list): filter template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 11:28:38 -08:00
Leonardo de Moura
83aaf64318 fix(library/tactic): memory leaks
Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 00:44:39 -08:00
Leonardo de Moura
2372567a6e fix(util/luaref): warnings produced by valgrind
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 00:34:38 -08:00
Leonardo de Moura
a7027a1d00 feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 00:16:39 -08:00
Leonardo de Moura
ff052d41ee chore(*): fix cygwin compilation errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 13:49:18 -08:00
Leonardo de Moura
ce674d2d43 feat(library/tactic): execute Lua tactics using coroutines
This is very important when several Lua tactics are implemented in the
same Lua State object.  In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.

With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 13:09:33 -08:00
Leonardo de Moura
6cb8300076 doc(lua): add S-expression documentation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 10:33:32 -08:00
Leonardo de Moura
09bc7ddf91 feat(library/tactic): add support for migratic tactic framework object between Lua states
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 08:03:05 -08:00
Leonardo de Moura
b4a8418d38 feat(library/tactic): expose tactics in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 17:47:29 -08:00
Leonardo de Moura
55f86f79a8 fix(util/optional): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 16:57:29 -08:00
Leonardo de Moura
a2aa90ae66 refactor(util/script_state): replace std::recursive_mutex with std::mutex, and use unlock_guard
The unlock_guard and exec_unprotected will be useful also for implementing the Lua tactic API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 15:40:41 -08:00
Leonardo de Moura
b038636ff5 refactor(util/script_state): remove unsafe unguarded_apply
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 15:14:26 -08:00
Leonardo de Moura
f7e8545e97 refactor(frontends/lua): rename leanlua_state to script_state, and move it to util
This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 14:57:36 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 12:25:29 -08:00
Leonardo de Moura
a6f6f49b5f refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular
copy_values is not a big if-then-else anymore.
Before this change, whenever we added a new kind of userdata, we would have to update copy_values.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 10:32:19 -08:00
Leonardo de Moura
4c5ec53a44 chore(util/lua): remove dead code
I removed lua_module helper class because it does not work.
The problem is that the linker may eliminate ignore a object file that contains a lua_module global object used for initialization. When this happens, the associated Lua bindings will not be exposed in the Lua API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 19:36:32 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 19:15:56 -08:00
Leonardo de Moura
e29a2f4d11 chore(util/interrupt): improve comment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-25 17:23:36 -08:00
Leonardo de Moura
4eb62fef91 fix(util/interrupt): fix nasty bug on interruptible_thread, it seems to occur only on cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-25 17:14:22 -08:00
Leonardo de Moura
500ed7a05b refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-25 10:39:40 -08:00
Leonardo de Moura
8e87ef5da8 feat(util/lazy_list): add repeat and repeat_at_most templates for lazy_lists
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-24 11:16:37 -08:00
Leonardo de Moura
b74aeb1216 fix(util/lazy_list): par template missing case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-24 00:38:31 -08:00
Leonardo de Moura
4e24dfd5a6 fix(util/optional): move constructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-24 00:22:02 -08:00
Leonardo de Moura
40a2f0a588 refactor(util/lazy_list): polish lazy_list API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 17:45:01 -08:00
Leonardo de Moura
bcd88cac08 style(util): missing includes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 17:05:46 -08:00
Leonardo de Moura
924187b055 feat(util/lazy_list): add par template for lazy lists)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 16:51:17 -08:00
Leonardo de Moura
157a2b36db feat(lazy_list): add timeout template for lazy_lists
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 16:27:36 -08:00
Leonardo de Moura
cb3c685fb1 feat(util/lazy_list): check for interruption between pulls
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 15:54:32 -08:00
Leonardo de Moura
f19944cf09 refactor(util/lazy_list): 'lazier' lazy_lists
In the new implementation, even the head of the lazy list is computed on demand.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 15:33:30 -08:00
Leonardo de Moura
9eb6da2a31 feat(util): add optional template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-23 13:27:22 -08:00
Leonardo de Moura
a776c8b158 feat(util/interrupt): add sleep_for, and simplify request_interrupt
The Lean sleep_for checks the interrupt flag from time to time.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-22 11:32:12 -08:00
Leonardo de Moura
1f225d2752 feat(util/lazy_list): add useful lazy_list function templates
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-22 09:40:56 -08:00
Leonardo de Moura
ca74d069b9 feat(util/interrupt): reset interrupt flag before throwing exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
8515821d56 feat(util/list): add map_filter template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
f6bfd11aed chore(util/list_fn): fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
df04dbe096 chore(util): use && when appropriate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
b0a4d60174 fix(util/interval): add missing explicit template instantiation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-20 09:56:19 -08:00
Leonardo de Moura
eba31a0516 test(util/interval): add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 19:07:09 -08:00
Leonardo de Moura
2265ef78c4 feat(util/list): add emplace_front
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 16:27:31 -08:00
Leonardo de Moura
e10d17a0f4 feat(util/sexpr): avoid recursion when destructing sexpr's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 17:46:53 -08:00
Leonardo de Moura
64379a5a10 perf(util/list): use buffer of cells instead of buffer of T
T may be a big object. We minimize the ammount of copying using buffer of (pointers to) cells.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 17:12:02 -08:00
Leonardo de Moura
76252816ac perf(util/list): avoid recursion in map and destructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 16:47:52 -08:00
Leonardo de Moura
d67bf995ed feat(util/list): avoid recursion at for_each template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 15:52:31 -08:00
Leonardo de Moura
adf4856f88 feat(util/list): add map_reuse template
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 15:32:02 -08:00
Leonardo de Moura
80fccc5533 fix(util/realpath): style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:55:16 -08:00
Leonardo de Moura
e0c23e5984 fix(kernel/environment): compilation problem on Windows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:52:47 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:13:34 -08:00
Leonardo de Moura
9398ea5a59 feat(util/shared_mutex): add support for recursive lock at shared_mutex
We need support for recursive locks. The main user of this class is
the environment object. This commit adds a test that demonstrates that
the shared_lock of the environment object may be recursively requested.
Before this fix, the Lean was deadlocking in this example.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 22:01:11 -08:00
Leonardo de Moura
bd1e9c7548 feat(lua): throw an exception if the user tries to create a thread and Lean was compiled without multi-threading support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 19:06:36 -08:00
Leonardo de Moura
64cce595a5 feat(lua): add splay_maps to the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 13:35:36 -08:00
Leonardo de Moura
e2efce6b62 style(util/sexpr): name convetion for enumeration types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 11:50:12 -08:00
Leonardo de Moura
c4c548dc5d feat(*): simplify interrupt propagation
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 21:45:48 -08:00
Leonardo de Moura
b31233e8c2 feat(util/interrupt): restore interrupt module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 21:16:10 -08:00
Leonardo de Moura
ac6c18321a fix(lua): make sure environment objects can be safely accessed/updated from current threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 20:29:53 -08:00
Leonardo de Moura
596e4aeb57 feat(util/shared_mutex): add shared_mutex object, this is a temporary replacement for std::shared_mutex that will be available in C++11
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 20:00:21 -08:00
Leonardo de Moura
f158b0b311 fix(util/memory): make sure realloc behaves like free when sz == 0
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 13:42:22 -08:00
Leonardo de Moura
31abc00db8 chore(*): add LCOV_EXCL_LINE to lean_unreachable statements
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 09:19:38 -08:00
Leonardo de Moura
7683188ab0 chore(emplace_back): use emplace_back when appropriate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
c5207489fd fix(memory): realloc must behave like malloc when ptr is nullptr
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 10:31:57 -08:00
Leonardo de Moura
2d88922543 feat(frontends/lean/elaborator): solve easy overloads at preprocessing time
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 10:07:15 -07:00
Leonardo de Moura
1d18f60dd5 fix(numerics): add missing numeric_traits<float>::zero()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:47:23 -07:00
Leonardo de Moura
c3c66b6c90 feat(make): add THREAD_SAFE build option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:50:35 -07:00
Leonardo de Moura
5e34f410b3 refactor(splay_map): modify splay_find signature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:47:15 -07:00
Leonardo de Moura
2b5c951de3 perf(name): add quick_cmp for hierarchical names
It first compare names using hash codes.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:58:06 -07:00
Leonardo de Moura
449454efdb fix(debug): remove typeid information from assertion, the names are mangled and are not very useful
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:41:51 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
59914a36f3 refactor(metavar): reorganize and simplify metavariables
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
3387c300a0 feat(polynomial): add multivariate polynomials
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-21 18:22:14 -07:00
Leonardo de Moura
f18d35555e refactor(interval): organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-21 18:15:27 -07:00
Leonardo de Moura
e208309abd refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-21 17:23:56 -07:00
Leonardo de Moura
f1d9312521 feat(numerics/zpz): add numeric_traits for zpz numerals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-18 14:41:18 -07:00
Leonardo de Moura
1429cc9df2 feat(numerics): add finite field Z/pZ
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-18 13:27:28 -07:00
Leonardo de Moura
cf2c0f8ebb feat(numerics): add gcd and extended gcd templates (for primitive types)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 18:18:20 -07:00
Leonardo de Moura
39f68ed0d6 feat(numerics): add is_prime function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 17:25:08 -07:00
Leonardo de Moura
1097bbfb22 fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 17:04:39 -07:00
Leonardo de Moura
105f55c68b feat(numerics): add zero() method to all numeric_traits
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 16:55:17 -07:00
Leonardo de Moura
467eff4662 add(numerics): add prime number generator/iterator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 16:05:45 -07:00
Soonho Kong
b823c7d779 feat(util): add static_assert to {scoped,splay}_{map,set} 2013-10-01 16:47:28 -07:00
Soonho Kong
a726f5fbb7 feat(util/list): add static_asserts for map/for_each/compare 2013-10-01 09:05:53 -07:00
Soonho Kong
3381df0150 fix(util/list_fn): rename iter to for_each 2013-10-01 09:03:07 -07:00
Soonho Kong
1a3ea26032 feat(util/list_fn): add iter function 2013-10-01 00:18:55 -07:00
Leonardo de Moura
15979ab991 fix(lean): fix warnings produced by cppcheck
Fix (relevant) warnings produced by http://cppcheck.sourceforge.net.
Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-30 21:38:55 -07:00
Leonardo de Moura
8d3ae665e7 fix(splay_map): fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:30:08 -07:00
Leonardo de Moura
21f9699661 test(splay_tree): add missing test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:28:10 -07:00
Leonardo de Moura
3c8dff9085 feat(lazy_list): implement ML-like lazy lists
We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 12:35:26 -07:00
Soonho Kong
841a1fb20c fix(debug): print type in lean_assert, print bool correctly
- use typeinfo to print out a type of value when an assertion fails.
   need to use "c++filt --types" to demangle names for non-basic types.
 - use std::boolalpha and std::noboolalpha to control the printed values
   for "true" and "false"
2013-09-28 23:38:21 -07:00
Soonho Kong
4602dfd209 test(util/numerics): more tests to improve coverage 2013-09-28 23:38:17 -07:00
Soonho Kong
6307beedc9 feat(scoped_map): add operator<< to scoped_map for debugging 2013-09-27 01:42:11 -07:00
Soonho Kong
3a5a565594 feat(splay_map): add operator<< to splay_map for debugging 2013-09-26 20:44:20 -07:00
Soonho Kong
60157aa92a fix(splay_map): add 'const' to coersion operator of ref class
[skip ci]
2013-09-26 19:09:37 -07:00
Leonardo de Moura
54e63fd4de feat(splay_tree): add fold and for_each templates for splay_tree and splay_map
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 18:18:20 -07:00
Leonardo de Moura
1aca1d2d77 refactor(list): improve append function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 18:18:20 -07:00
Leonardo de Moura
24c173a519 feat(debug): add assert_ne (not equal) macro
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 18:18:20 -07:00
Leonardo de Moura
d7ed1560a9 feat(name_generator): add name_generator for unique names modulo a prefix
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 18:18:06 -07:00
Leonardo de Moura
a24dbc3527 test(buffer): add tests for improving coverage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 08:35:13 -07:00
Soonho Kong
a2a5a77a44 fix(memory): increase memory counters by the actual size of reallocated memory
On OSX, we had a test failure on memory module. The problem was in
the realloc function (line 38):

    void * realloc(void * ptr, size_t sz) {
        size_t old_sz = malloc_size(ptr);
        g_global_memory.dec(old_sz);
        g_global_memory.inc(sz);
        g_thread_memory.dec(old_sz);
        g_thread_memory.inc(sz);
        void * r = realloc_core(ptr, sz);
        if (r || sz == 0)
            return r;
        else
            ...

The size of r could be bigger than sz. For instance,

    |ptr| = 40 but |r| = 48

In the current code, here we only increase counters by 40.
But later when we free it, we decrease them by 48, and this
caused the problem, underflow of an unsigned counter in
g_global_memory.
2013-09-26 00:33:56 -07:00
Leonardo de Moura
6477708d78 refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 21:27:20 -07:00
Leonardo de Moura
44a16cab6a test(exception): add new tests exception and parser_exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 20:57:53 -07:00
Leonardo de Moura
1452e9319e feat(debug): improve lean_assert macro
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 17:29:00 -07:00
Soonho Kong
0ef633a3c5 Fix to be compiled by clang++-3.4
Clang++-3.4 is starting to enforce the following item of C++11 standard,
thus it's making lean not compiling:

It's illegal in C++11: §8.3.6.4 [dcl.fct.default]
"If a friend declaration specifies a default argument expression, that
declaration shall be a definition and shall be the only declaration of
the function or function template in the translation unit."
2013-09-24 21:30:56 -07:00
Leonardo de Moura
e23813f15d Add support for creating unique internal names.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-24 11:01:30 -07:00
Leonardo de Moura
1779b29355 Implement map using splay_trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-24 01:44:46 -07:00
Leonardo de Moura
b78b2e0585 Add remaining splay tree methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-24 01:04:02 -07:00
Leonardo de Moura
d31f3facac Implement splay trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-23 22:31:18 -07:00
Leonardo de Moura
16a6a54df1 Fix abuse of operator-> overload
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-22 16:41:51 -07:00
Leonardo de Moura
d29ec9ab6f Add tests for memory.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-20 22:37:13 -07:00
Soonho Kong
bef44899c8 Suppress style warning on util/memory.cpp 2013-09-20 18:07:12 -07:00
Soonho Kong
9226c46358 Add support OSX's malloc_size 2013-09-20 17:48:55 -07:00
Leonardo de Moura
3971265bcb Add support for _msize
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-20 14:14:57 -07:00
Leonardo de Moura
dae654e4c6 Track memory usage. Add new CMake option TRACK_MEMORY_USAGE (It is ON by default).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-20 12:32:12 -07:00
Leonardo de Moura
16dc056abc Remove invalid use of register
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-19 22:59:39 -07:00
Soonho Kong
49e87ccbb1 Enable "-Wextra" compiler option and fix code to remove warnings
"-Wextra" option turns on the following warnings:
 -Wclobbered
 -Wempty-body
 -Wignored-qualifiers
 -Wmissing-field-initializers
 -Wmissing-parameter-type (C only)
 -Wold-style-declaration (C only)
 -Woverride-init
 -Wsign-compare
 -Wtype-limits
 -Wuninitialized
 -Wunused-parameter (only with -Wunused or -Wall)
 -Wunused-but-set-parameter (only with -Wunused or -Wall)
2013-09-19 22:52:52 -07:00
Soonho Kong
ab6ca82e6f Update to suppress unused-parameter warnings 2013-09-19 22:40:34 -07:00
Leonardo de Moura
80a1b96925 Remove duplicate solutions in the higher order matching module. Simplify solutions when higher-order matching is used, and we don't have a residue.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-19 18:59:28 -07:00
Soonho Kong
27d5ae13d7 Move src/interval to src/util/interval 2013-09-17 14:10:53 -07:00
Leonardo de Moura
df054477eb Remove unnecessary TODOs.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 13:33:52 -07:00
Leonardo de Moura
1be2a30c8c Fix bug in normalizer. We must create a scope whenever we extend the value stack.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -07:00
Soonho Kong
01339a93a3 Fix cpplint warning in util/safe_arith.cpp 2013-09-16 19:12:12 -07:00
Soonho Kong
13401d534c Add static assertion to util/safe_arith.cpp 2013-09-16 18:17:05 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 12:09:01 -07:00
Soonho Kong
dcc917a6b4 Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf" 2013-09-15 01:38:21 -07:00
Soonho Kong
60903d3cea Fix cygwin build which was failed due to snprintf 2013-09-14 17:11:37 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
bcc3827a99 Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 13:46:22 -07:00
Leonardo de Moura
8c735f1daa Use consistent coding style for spaces after ','
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:49:03 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 20:04:10 -07:00
Leonardo de Moura
c655e9fe7b Move sexpr_funcs to sexpr_fn. Using consistent file name conventions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 18:27:46 -07:00
Leonardo de Moura
bc69e7803f 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>
2013-09-12 11:18:26 -07:00
Leonardo de Moura
74b8a4f0ac 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>
2013-09-12 11:12:02 -07:00
Leonardo de Moura
f972cc9aae Fix bugs in pvector. Improve test driver
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 11:01:40 -07:00
Leonardo de Moura
55ff49d2d5 Replace queue.h with pdeque.h
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 10:09:54 -07:00
Leonardo de Moura
cd5e45bae2 Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 08:28:24 -07:00
Leonardo de Moura
f7196e05ff Add 'persistent' vectors. We should use the same approach for queues.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
ef0e0ad382 Add (optional) performance tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
ed15a2df9b Use split_reverse_second instead of split and then reverse in queue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
37498f9fb8 Add persistent queues
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:54 -07:00
Leonardo de Moura
3657320edb Add basic list functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:54 -07:00
Soonho Kong
fae6c29237 Fix memory leaks in mpfp.h 2013-09-10 13:26:14 -07:00
Leonardo de Moura
adfbba6447 Fix problem reported by Soonho
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 23:10:33 -07:00
Leonardo de Moura
1cee392483 Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 22:33:18 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
887f696f66 Factor duplicate code. Add more comments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 23:27:58 -07:00
Leonardo de Moura
a154f4e439 Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 11:07:28 -07:00
Leonardo de Moura
544229e5d3 Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 10:11:45 -07:00
Leonardo de Moura
45d89ace65 Fix name clash problem when pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-30 13:25:12 -07:00
Leonardo de Moura
fc6cc17925 Improve lean pretty printer support for implicit argument annotations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-26 19:19:56 -07:00
Leonardo de Moura
25e47a8a2f Add check_interrupted 'macro'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-25 11:03:09 -07:00
Leonardo de Moura
dc91a7adb8 Add Ctrl-C support for interrupting Lean shell.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-24 16:11:35 -07:00
Leonardo de Moura
0b112b6637 Add sstream to simplify the generation of exception messages.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-24 11:55:17 -07:00
Leonardo de Moura
be1ea2ddc7 Add name_set typedef
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-23 19:34:10 -07:00
Leonardo de Moura
198fd46fc2 Track recursion depth at normalizer. Add fluid let template.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-23 09:42:49 -07:00
Leonardo de Moura
42a7094ca2 Fix bug in display_decimal. Add more mpq tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-23 09:42:49 -07:00
Leonardo de Moura
fbd25cac9f Add hierarchical names tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-22 08:48:52 -07:00
Leonardo de Moura
1b5fcb80ee Add sexpr tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-22 08:30:52 -07:00
Leonardo de Moura
6272408f12 Add format tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-22 08:20:42 -07:00
Leonardo de Moura
3c5f993191 Fix bugs in options module. Add more tests.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-22 08:08:55 -07:00
Leonardo de Moura
eb4315baab Add small trick to improve pretty printer performance. Now, deep.lean takes 0.140secs to be processed.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 22:54:58 -07:00
Leonardo de Moura
56d2d2a112 Improve pretty printer performance for deep formulas and formats with long lines. Add example that demonstrates performance problem (before: 13 secs, after: 1 sec).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 22:45:48 -07:00
Leonardo de Moura
31460aa5b8 Add option declarations. Add Help.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 17:02:09 -07:00
Leonardo de Moura
ce470f57db Add set options to lean_parser. Add support for disabling unicode output. Use channels in lean_parser.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-21 12:42:55 -07:00
Leonardo de Moura
6f36611010 Fix clang++ error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-20 20:16:02 -07:00
Leonardo de Moura
3f5a2a83cc Add methods for setting options. Add string output channel.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-20 20:16:02 -07:00
Leonardo de Moura
4fa2468a85 Add output_channel and state abstractions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-20 20:16:02 -07:00
Leonardo de Moura
f6ea9fca7d Remove interrupt.cpp. We changed the way we will handle interruptions in Lean.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-19 20:05:56 -07:00
Leonardo de Moura
b964edfb3e Add interrupt method to type checker.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-19 20:05:56 -07:00
Leonardo de Moura
eba4172a0c Remove verbosity.cpp, verbosity message channel should not be a global.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-19 20:05:56 -07:00
Leonardo de Moura
de80db3985 Add support for pretty printing Dags. Find unused prefix for naming shared expressions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-19 12:04:40 -07:00
Leonardo de Moura
90ad0ba3b3 Add is_prefix_of for hierarchical names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-19 11:43:46 -07:00
Leonardo de Moura
65b4845fbc Add more tests to improve coverage. Fix bug in mpz.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-18 00:28:50 -07:00
Leonardo de Moura
6edae938b7 Improve list iterator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-17 11:31:36 -07:00
Leonardo de Moura
c41b3dc4d8 Add kernel_exceptions. The idea is to avoid expression formatting in the kernel. It also allows different frontends to display the error messages is a different way.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-16 12:51:12 -07:00
Leonardo de Moura
790d4a4447 Move pretty printer to frontend. Add support for mixfix pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Leonardo de Moura
5395ced0e5 Improve comments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Leonardo de Moura
e9106f7512 Delete obsolete function continue_on_violation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Leonardo de Moura
577256fedc Add highlight_keyword, highlight_builtin, highlight_command for consistent formatting
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Soonho Kong
a6f3122146 Fix cygwin error caused by the use of thread_local in numerics/float class 2013-08-15 13:49:15 -07:00
Soonho Kong
eb29a67395 Fix mpfp::operator^= to resolve operator overloading problem 2013-08-14 23:49:26 -07:00
Leonardo de Moura
2d74ff5fe0 Cache results of the normalizer. Add example that demonstrates the exponential performance improvement.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-14 23:18:50 -07:00
Leonardo de Moura
f604be760d Add helper function for maps.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-14 18:17:18 -07:00
Leonardo de Moura
913fd14549 Add operator== to list
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-14 18:17:18 -07:00
Soonho Kong
43b25a0231 Add operator<(mpq, double) to mpq 2013-08-14 13:45:29 -07:00
Soonho Kong
70f383eb82 Add unary minus operator overloadings to mpq & mpfp 2013-08-14 00:01:03 -07:00
Soonho Kong
5f143f164e Fix numeric_traits<mpfp>::pi constants 2013-08-13 20:09:06 -07:00
Soonho Kong
02900e2c83 Add abs/floor/ceil to double/float/mpq/mpfp 2013-08-13 20:09:06 -07:00
Leonardo de Moura
392b347f53 Add expr_formatter and expr_locator. Add better error messages. Improve simple printer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 19:16:40 -07:00
Leonardo de Moura
3bcbdf7c7b Add options to customize formatter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 16:19:30 -07:00
Leonardo de Moura
11a9cac5d6 Refactor kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 15:13:54 -07:00
Leonardo de Moura
00c06839a4 Fix scanner. Add scanner tests. Add itera to list::iterator. Add parser_exce.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 10:55:41 -07:00
Leonardo de Moura
0a4e03efc5 Remove option name::separator, it can't be configured during runtime
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 08:18:01 -07:00
Leonardo de Moura
963afa4861 Add missing files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 07:07:14 -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
Soonho Kong
e123dd8e58 Use numeric_traits<mpfp>::get_mpfp_rnd() as a default rounding mode in mpfp operations 2013-08-13 00:35:14 -07:00
Leonardo de Moura
50cf3e42f1 Add operator_info
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 19:12:44 -07:00
Leonardo de Moura
fb56869aae Fix cygwin problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 15:22:08 -07:00
Soonho Kong
71e10a0336 Add missing initialization of numeric_traits<mpfp>::rnd 2013-08-12 14:58:17 -07:00
Leonardo de Moura
2ad9c89684 Fix memory leak in mpfp. Add mpfp finalizer to avoid Valgrind warnings.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 11:36:15 -07:00
Soonho Kong
99df36f747 Add missing header <numeric> to format.h 2013-08-12 10:58:07 -07:00
Leonardo de Moura
e07830d0f5 Fix nasty crash that only happens when using cygwin.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-11 14:35:58 -07:00
Leonardo de Moura
7ebaac62a8 Add scoped_map. Cache type checker results.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 19:27:56 -07:00
Leonardo de Moura
19440bc103 Fix clang warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 16:58:15 -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
3d9f9a12d1 Enable automatic coercion from 'char const *' to hierachical name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
c6d0afcc40 Rename sexpr eqp to is_eqp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Soonho Kong
375bc817cc Add more to mpfp 2013-08-09 22:41:07 -07:00
Soonho Kong
40bdd1a36b Fix typos in format.h (error messages) 2013-08-09 22:41:07 -07:00
Leonardo de Moura
e5fe016a44 Add pretty printer for s-expressions and options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-08 18:38:18 -07:00
Leonardo de Moura
33e8e4af23 Add initializer list constructor for hierarchical names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-08 18:38:18 -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
Leonardo de Moura
b50d9df784 Add options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-08 18:38:18 -07:00
Soonho Kong
635407ca4a Fix sexpr_text_length function to handle quotation in string 2013-08-08 12:24:42 -07:00
Soonho Kong
9516d9f88f Restructure format, and fix bugs 2013-08-08 12:24:19 -07:00
Soonho Kong
fe9d2147d2 Improve performance of format by using "space_upto_line_break" instead of "fits" 2013-08-08 10:34:15 -07:00
Leonardo de Moura
bede62e2f7 Fix bug in sexpr operator <<.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 21:53:19 -07:00
Soonho Kong
0f48f73e14 Add constants and transcendental functions to mpfp 2013-08-07 19:32:15 -07:00
Soonho Kong
03dc15868b Add more operator overloadings to mpfp 2013-08-07 19:32:15 -07:00
Soonho Kong
93b99cf1ec Add constants(Pi, 1/2Pi, 2Pi) to double, float, and mpq 2013-08-07 19:32:03 -07:00
Soonho Kong
2a8c9e9c06 Reformat mpfp.h 2013-08-07 19:32:03 -07:00
Soonho Kong
d3dbcadf8b Add placeholders for transcendental functions in mpbq & mpq 2013-08-07 19:32:02 -07:00
Leonardo de Moura
2670e94398 Add pretty printer for Lean environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 19:10:12 -07:00
Leonardo de Moura
f8e3563034 Add scoped sets
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 13:54:18 -07:00
Leonardo de Moura
84de625ee4 Rename pp functions (that do not use format lib) to print
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 12:10:10 -07:00
Leonardo de Moura
722e2b0ed4 Reformat code (make formating more consistent)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 08:17:33 -07:00
Soonho Kong
5efd2fdd6f Update util/numerics/CMakeLists.txt to add mpfp, double, float 2013-08-06 20:01:09 -07:00
Soonho Kong
fb41a4f5a3 Add numeric_traits for double and float 2013-08-06 20:00:37 -07:00
Soonho Kong
d22b4bc9f1 Add mpfp, a wrapper for MPFR 2013-08-06 19:59:58 -07:00
Leonardo de Moura
30513398bb Add basic definitions and axioms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-05 20:06:42 -07:00
Leonardo de Moura
2986f0543e Simplify how universe variable constraints are represented in the kernel. Allow universe variable to be created without an environment.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-05 20:06:42 -07:00