Ken McMillan
49c72abb2d
new interpolation fixes; re-added fixedpoint-push/pop
2013-11-05 12:17:09 -08:00
Ken McMillan
3a0947b3ba
merged with unstable
2013-10-18 17:26:41 -07:00
Ken McMillan
b27abc501e
set proof mode by default to avoid crash on pop if we set it later in duality
2013-05-27 19:22:19 -07:00
Ken McMillan
e939dd2bc5
still integrating duality
2013-04-30 13:07:49 -07:00
Nuno Lopes
7ce88d4da9
fix a few compilation warnings
...
- remove unused variables and class fields
- add support for gcc 4.5 & clang's __builtin_unreachable
- fix 2 bugs related to strict aliasing
- remove a few unused function parameters
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-21 14:36:39 -07:00
Nuno Lopes
adc8224dba
use svector instead of vector where appropriate
...
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-16 09:02:40 -07:00
Ken McMillan
78848f3ddd
working on smt2 and api
2013-03-26 17:25:54 -07:00
Leonardo de Moura
d2651f1afc
Keep consistent error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-13 18:53:37 -08:00
Nikolaj Bjorner
ff03da9e67
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
2013-02-12 15:44:32 -08:00
Leonardo de Moura
3a15db5244
Fix uninterpreted sort definition. There was a mismatch in the behavior of the API and SMT front-ends. The SMT front-ends were using user_sorts to be able to support parametric uninterpreted sorts. After this fix, the API also creates user_sorts.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-12 14:34:31 -08:00
Nikolaj Bjorner
3ad43c60a9
working on pdr gen
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-02-08 16:54:05 -08:00
Leonardo de Moura
8e5581b4fe
Retract changes in the commit 39a614559c. The fix was affecting benchmarks using the array theory map construct.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-04 08:19:33 -08:00
Leonardo de Moura
39a614559c
Add partial solution for the uneeded disambiguation issue raised by David Cok
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-03 15:55:36 -08:00
Leonardo de Moura
d92efeb0c5
Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-18 17:14:25 -08:00
Leonardo de Moura
3ddb1a85f1
Add basic_recognizers and array_recognizers
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-18 15:00:16 -08:00
Leonardo de Moura
cec328cfdc
Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-18 14:44:51 -08:00
Leonardo de Moura
c011b05b61
exposing algebraic numbers in the API (working in progress)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 17:48:57 -08:00
Leonardo de Moura
a07b459fdf
Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 12:53:51 -08:00
Leonardo de Moura
288a96610f
ported VCC trace streams
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 09:08:47 -08:00
Nikolaj Bjorner
2d1a6bf270
fix regression for simplifying tails with quantifiers, add some more handling for quantified tails
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-30 15:58:06 -08:00
Leonardo de Moura
ead39ea6c5
Fixed bug reported by Nuno Lopes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-23 10:49:58 -08:00
Leonardo de Moura
73a13f209b
fixed bug detected in regression tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-07 10:46:00 -08:00
Nikolaj Bjorner
f44631ce73
fix bugs encountered by regression tests
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-10-30 16:13:27 -07:00
Leonardo de Moura
641db30660
Isolating reg_decl_plugins
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-24 11:27:50 -07:00
Leonardo de Moura
8a6997960a
Reorganizing code. Added script for generating VS project files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-20 15:16:37 -07:00
