Leonardo de Moura
80e23f98c7
feat(kernel/environment): add environment extension objects, the environment can be extended with frontend specific objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-06 19:22:30 -08:00
Soonho Kong
044813615e
fix: add '#include <tuple>'
2013-11-03 13:00:42 -05:00
Leonardo de Moura
aa99ac6618
feat(kernel/value): allow semantic attachments to use coercions when being pretty printed
...
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 11:42:26 -07:00
Leonardo de Moura
7fc87faa8f
feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:07:30 -07:00
Leonardo de Moura
4dd6cead83
refactor(equality): make homogeneous equality the default equality
...
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.
- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
l = nil
will not propagate the type (List Int) to nil.
- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.
Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
521fa1ddb8
style(kernel/metavar): add missing includes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:00:43 -07:00
Leonardo de Moura
7c8daf8974
fix(kernel/metavar): make sure the justification and substitution are always matching each other
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225
fix(kernel/normalizer): do not apply substitutions in the normalizer
...
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:14:48 -07:00
Leonardo de Moura
dbefc91151
fix(kernel/metavar): add normalize assignment justification
...
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976
feat(kernel/expr): add new mk_app template for creating applications using a collection
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558
refactor(assumption_justification): move to the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-26 14:21:29 -07:00
Leonardo de Moura
4bed9f85b0
feat(kernel/for_each): add option for disabling cache of atomic expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:25:17 -07:00
Leonardo de Moura
ce10bfeaf6
perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:19:59 -07:00
Leonardo de Moura
57d9d23bd4
feat(kernel/for_each): allow function F to interrupt for_each search
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:58:02 -07:00
Leonardo de Moura
2dd44bdf1a
perf(kernel/for_each): delay initialization of visited set
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:52:08 -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
471bbd4040
refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:02:19 -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
5812dfcf44
perf(kernel/justification): remove cache from depends_on
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:26:05 -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
66f4834dbc
perf(kernel/metavar): add quick test that catches many cases
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:24:01 -07:00
Leonardo de Moura
f38178311c
perf(kernel/expr_eq): delay hashtable initialization
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:21:47 -07:00
Leonardo de Moura
412bc792c9
fix(style): missing include
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:10:28 -07:00
Leonardo de Moura
0c21f45292
fix(kernel/unification_constraint): memory leak
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:06:21 -07:00
Leonardo de Moura
a5c3829d1b
feat(kernel): add unexpected_metavar_occurrence exception
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:56:44 -07:00
Leonardo de Moura
ca6a6d71e5
fix(kernel/printer): bug when printing let expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 18:05:23 -07:00
Leonardo de Moura
872b698bc3
feat(elaborator): add option m_assume_injectivity for getting more concise solutions
...
We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem
Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
DisjCases H
(fun H1 : _,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
in CongrH AeqC (Symm AeqC))
(fun H1 : _,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
in CongrH AeqC (Symm AeqC))
the elaborator generates
Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
DisjCases
H
(λ H1 : if
Bool
(if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
⊥
⊤,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
(λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))
The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 16:47:50 -07:00
Leonardo de Moura
bbc265ded4
feat(frontends/lean): hook new elaborator in the default frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:14:29 -07:00
Leonardo de Moura
434c33f225
feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda
...
This feature is useful for problems that require higher-order matching and/or unification.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:35:50 -07:00
Leonardo de Moura
873e56844a
refactor(beta_reduction): add function apply_beta
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:03:52 -07:00
Leonardo de Moura
f1e0d6ec29
refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a
feat(replace_visitor): add an abstract class for applying transformations on expressions
...
I also removed replace_using_ctx since it is subsumed by the new class.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e
refactor(kernel): rename trace to justification
...
Motivations:
- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 13:42:17 -07:00
Leonardo de Moura
17b48010b7
fix(unification_constraint): fix printer for max constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 12:00:29 -07:00
Leonardo de Moura
274b11530f
feat(metavar): improve apply_local_context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 11:59:36 -07:00
Leonardo de Moura
b57f492e2d
fix(kernel/printer): improve printer for Type expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 11:58:49 -07:00
Leonardo de Moura
891d22b3de
feat(kernel/context): add method for remove context entries at positions [s, s+n).
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 15:52:24 -07:00
Leonardo de Moura
874f67c605
feat(normalizer): remove normalization rule t == t ==> true
...
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:
Theorem Th : a = a := Refl b
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 14:02:48 -07:00
Leonardo de Moura
c3e87f106f
fix(kernel/trace): fix typo in depends_on
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:37 -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
8663ac550f
feat(kernel/trace): add function depends_on for trace objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7
test(elaborator): add simple test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1
feat(elaborator): add new elaborator interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
827c65b5e9
feat(kernel): add static_assert for update_metavar
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
61ccaf741c
fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
7cf83800c0
refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
1f0eab7a14
test(type_checker): add new tests for type_checker trace objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
fc288929a2
feat(type_checker): add trace objects to justify constraints created by the type checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
5b1b03bafd
refactor(is_convertible): move from normalizer to type_checker class
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
85bfa45e6a
refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
d843d432d3
refactor(kernel): move printer and formatter objects to the kernel
...
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
ddb90d3038
feat(kernel): add unification_constraint and trace objects to the kernel
...
Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.
The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.
Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.
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
0783805671
feat(kernel): add weight to kernel definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 14:50:08 -07:00
Leonardo de Moura
aa5be3262f
fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-01 19:23:55 -07:00
Soonho Kong
e3b762e909
feat(kernel): add static_assert to expr,expr_eq,replace
2013-10-01 16:47:36 -07:00
Soonho Kong
a832173f5f
feat(kernel/expr): add expr::operator() which takes 8 args
2013-10-01 00:19:30 -07:00
Leonardo de Moura
e5d312dc18
fix(kernel): the hash code of expressions was not being used to compare them
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 08:41:20 -07:00
Leonardo de Moura
98b4e09063
refactor(kernel): simplify expr_eq
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 22:09:08 -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
9f0dab1add
fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
...
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include
'library/printer.h', but contains
expr a;
...
std::cout << a << "\n";
...
The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
2013-09-25 17:45:54 -07:00
Leonardo de Moura
ba0528c298
Implement total order on expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-24 12:16:32 -07:00
Leonardo de Moura
46d6c41835
Fix bug in the type checker (when type checking terms with meta-variables).
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-22 19:12:19 -07:00
Leonardo de Moura
1647e44510
Fix memory corruption bug
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-22 18:53:58 -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
c847d27763
Improve higher order unification
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-21 00:41:49 -07:00
Leonardo de Moura
651c5d6751
Fix warnings and bugs related to unused variables.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-19 22:41:07 -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
Leonardo de Moura
2f29ff70d7
Implement higher-order unification
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-18 20:46:00 -07:00
Leonardo de Moura
ad901ce087
Use consistent naming conventions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 14:43:07 -07:00
Leonardo de Moura
3df6149daa
Add support for metavariables in the type checker.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 11:09:59 -07:00
Leonardo de Moura
9f9dcf9a29
Fix bug in the creation of children environments. Remove unnecessary function.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 07:37:33 -07:00
Leonardo de Moura
30b19c314a
Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 07:15:47 -07:00
Leonardo de Moura
a26c7d47f2
Add simplification to add_lift
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 03:14:02 -07:00
Leonardo de Moura
99e8d2feae
Add simplification rule to add_inst
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 02:57:28 -07:00
Leonardo de Moura
21c7a45f67
Relax definition of identity_stack. Fix printer for metavariable contexts.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 02:09:45 -07:00
Leonardo de Moura
d3bce584f4
Add support for new metavariable representation in the normalizer.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-17 01:57:21 -07:00
Leonardo de Moura
da09e7217a
Cleanup meta_entry code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -07:00
Leonardo de Moura
99a163f11d
Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -07:00
Leonardo de Moura
cad562a448
Add support for metavariables in the normalizer.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -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
Leonardo de Moura
f79f046294
Add partial support for metavariables in the normalizer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 21:23:50 -07:00
Leonardo de Moura
2800292947
Add timestamp to metavar_env
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2
Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 19:38:36 -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
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
d54834279e
Use consistent coding style for if-then-else
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:57:40 -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
Leonardo de Moura
2c68117adf
Tag TODOs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:25:21 -07:00
Leonardo de Moura
0c09e4524a
Use consistent names for import functions, and library files.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 08:58:34 -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
572c7ced2a
Add #include<atomic> to expr.h. We need it when #define LEAN_THREAD_UNSAFE_REF_COUNT is used
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
33c4b44b2b
Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 11:15:11 -07:00
Leonardo de Moura
bab11b57ad
Move Symm and Trans back to basic_thms.cpp
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:49:35 -07:00
Leonardo de Moura
c674bb3790
Add castlib as an independent library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:40:47 -07:00