Leonardo de Moura
4c28cb933b
Fix bug in is_convertible
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 16:44:22 -07:00
Leonardo de Moura
3ff3eb6444
Add Eta axiom
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 14:47:13 -07:00
Leonardo de Moura
68d092f5ef
Prove congr1, congr2 and congr theorems. Add xtrans theorem.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 14:37:30 -07:00
Leonardo de Moura
ab915fb3f0
Add add_theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 12:24:20 -07:00
Leonardo de Moura
9d6b421be9
Add theorems Truth, EqMP and EqTElim
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 12:17:55 -07:00
Leonardo de Moura
84f4a32c0e
Change name convention for creating Lean expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 11:27:14 -07:00
Leonardo de Moura
33d2dd2d8b
Add subst proof rule. Define symm and trans using subst.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-06 02:03:22 -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
8aee11e538
Fix test failure when using clang++ and release mode
...
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
Leonardo de Moura
7e2d7dcf3d
Add more builtin constants
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-05 20:06:42 -07:00
Leonardo de Moura
f6057e2b28
Add more environment tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-05 20:06:42 -07:00
Leonardo de Moura
0c610e0a77
Fix bug in type checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-05 20:06:42 -07:00
Soonho Kong
8dab224137
Fix CMakeLists.txt
2013-08-05 19:16:52 -07:00
Soonho Kong
52232f37cb
Add numeric_traits<double> and numeric_traits<float> which are using MPFR
2013-08-05 18:57:09 -07:00
Soonho Kong
a6f825caa5
Add MPFR & restructure cmake directory
2013-08-05 17:58:54 -07:00
Leonardo de Moura
70de591934
Add definitions and facts
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 20:52:14 -07:00
Leonardo de Moura
5f77a2367f
Allow Boolean expressions (aka propositions) to be used as types.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 18:26:01 -07:00
Leonardo de Moura
4b5d60f2b2
Add get_uvar method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 17:47:54 -07:00
Leonardo de Moura
c97db1f0cf
Add children environments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 16:07:37 -07:00
Leonardo de Moura
95447deea3
Add normalization a = b for values (aka semantic attachments)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 14:54:33 -07:00
Leonardo de Moura
f0ccb2a03e
Rename eqp --> is_eqp. The name is too similar to heterogeneous equality constructor eq.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 09:41:49 -07:00
Leonardo de Moura
3f789ce2b7
Add let and heterogeneous equality. Add bool_type and bool_value.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-04 09:37:52 -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
15a4152ce8
Fix merge problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:13:56 -07:00
Leonardo de Moura
0a679074f0
Add support for semantic attachments. Remove expr_numeral
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
1fec8b0d5b
Rename (stack) value to svalue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
0b8fa3b167
Remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
cce469119f
Flip order of the arguments for instance and abstract. Simplify type_checker.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
190855ad1b
Add (relaxed) version of instantiate that can substitute terms containing free variables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
2972bdfec3
Rename abst_type to abst_domain
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:12 -07:00
Leonardo de Moura
e1e3e6b2d6
Add instantiate tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:10:20 -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
Soonho Kong
bac75541dc
Add static_asserts to template funcs in expr.h & replace.h
2013-08-02 20:00:40 -07:00
Soonho Kong
fd7f0e9658
Update format test
2013-08-02 20:00:40 -07:00
Soonho Kong
83edc38fa1
Change folddoc to fold_right, add static_asserts for template functions
2013-08-02 19:48:11 -07:00
Soonho Kong
5f10d47035
Change operators in format:
...
f1 + f2 = f1 <> f2
f1 ^ f2 = f1 <> " " <> f2
2013-08-02 19:17:29 -07:00
Soonho Kong
bddecd7d9c
Roll back to flatten(line) == " "
2013-08-02 19:16:19 -07:00
Soonho Kong
4ebb96d7cd
Add static_asserts to sexpr_funcs.h
2013-08-02 18:26:51 -07:00
Soonho Kong
cda969187a
Add one small test to expr
2013-08-02 10:34:46 -07:00
Soonho Kong
faf3f20480
Disable doxygen generation on travis-ci since it causes time-out.
2013-08-02 10:11:33 -07:00
Soonho Kong
5aeacfee60
Add bison++ & flex to .travis.yml
2013-08-02 10:08:47 -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
a8c77ff40e
Disable eta-reduction for now.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 23:19:34 -07:00
Leonardo de Moura
c13b9a792a
Add small example
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 22:07:28 -07:00
Leonardo de Moura
3ef9d21875
Fix bugs in type checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 21:40:39 -07:00
Leonardo de Moura
7b00561a94
Normalize level expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 21:40:39 -07:00
Leonardo de Moura
e220d7c525
Add type checker. Fix normalization with non-empty context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 21:40:36 -07:00
Leonardo de Moura
bed5f09907
Rename normalize context to local_context. Create context. Fix bug in name.cpp
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-01 21:39:02 -07:00
Soonho Kong
3cef072cca
Update .travis.yml to fix email a notification setting.
...
- It seems that googlegroups doesn't accept emails from travis-ci
directly. I set up an email-forwarding on my account to pass emails
from travis to the mailing list.
2013-08-01 20:07:20 -07:00