Nikolaj Bjorner
|
f306f75e36
|
harness internalization and API for #1776
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-02 20:18:27 -07:00 |
|
Nikolaj Bjorner
|
77d68409c2
|
handle null declarations for kind
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-01 08:43:32 -07:00 |
|
Nikolaj Bjorner
|
124e963b10
|
revert bit-resize issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-31 16:26:41 -07:00 |
|
Nikolaj Bjorner
|
4b00d6aef2
|
move mk-bits to mk-var
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-31 16:13:25 -07:00 |
|
Nikolaj Bjorner
|
22a5687e16
|
supply bits on demand
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-31 15:52:21 -07:00 |
|
Nikolaj Bjorner
|
64e570f159
|
fix #1766
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-29 02:22:28 -07:00 |
|
Nikolaj Bjorner
|
1cb3f7c792
|
fixing #1520
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-28 18:03:13 -07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Bruce Mitchener
|
7167fda1dc
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
Nikolaj Bjorner
|
2897b98ed2
|
remove simplify dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-26 00:37:22 -07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Nikolaj Bjorner
|
d14f2af5ae
|
deal with subtraction that manages to sneak in. Issue #996
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-01 15:22:06 -07:00 |
|
Nikolaj Bjorner
|
25d839ed10
|
fix bug in simplifier of bv2int over concatentations exposed by #948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-03-22 10:55:55 -07:00 |
|
Nikolaj Bjorner
|
c1480b4389
|
handle model generation from issue #748. Deal with warnings from #836
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-12 00:40:52 +01:00 |
|
Nikolaj Bjorner
|
6559fd817d
|
Fix bit-blasting discrepancy. #690
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-20 10:53:53 -07:00 |
|
Nikolaj Bjorner
|
96e157e201
|
fix warnings for unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-17 13:54:22 -07:00 |
|
Nikolaj Bjorner
|
5994c5a948
|
fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-07 16:42:29 -08:00 |
|
Nikolaj Bjorner
|
2a65503235
|
fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-04 22:35:02 +00:00 |
|
Nikolaj Bjorner
|
3d01246f71
|
Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-08 08:17:18 -08:00 |
|
Nikolaj Bjorner
|
8e26c97782
|
tuning bit-vector operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-21 13:09:03 +02:00 |
|
Nikolaj Bjorner
|
5eb23e1e7a
|
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-10 19:20:16 -08:00 |
|
Nikolaj Bjorner
|
b4cb51cdb3
|
working on Forking/Serializing a z3 Solver #209
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-06 17:29:24 -08:00 |
|
Nikolaj Bjorner
|
feba64b739
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 10:18:25 -08:00 |
|
Nikolaj Bjorner
|
8438ac6e21
|
fix internalization bug when bit2bool is applied to numeral
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-10-06 15:43:24 -07:00 |
|
Nikolaj Bjorner
|
dd786bb5bf
|
fix quantifier elimination bugs reported by Berdine and Bornat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-07-14 15:41:03 +02:00 |
|
Nikolaj Bjorner
|
e4dedbbefc
|
fix quantifier elimination bugs reported by Berdine and Bornat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-07-14 15:38:22 +02:00 |
|
Nikolaj Bjorner
|
2e7f5303eb
|
address incompleteness bug in axiomatization of int2bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-09-23 04:56:38 +03: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
|
add684d8e9
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-21 13:32:12 -07:00 |
|