Nikolaj Bjorner
|
566eacd424
|
change handling of weak array mode. Insert weak delay variables into a queue that gets consumed by the next propagation when the array_weak parameter is changed #2686
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-11-19 21:17:36 -08:00 |
|
Nikolaj Bjorner
|
d95b549ff8
|
fix #2707
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-11-16 17:47:29 -08:00 |
|
Nikolaj Bjorner
|
fffc539b40
|
fix #2549
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-13 17:42:29 +02:00 |
|
Nikolaj Bjorner
|
9fa9aa09ff
|
fix #2468, adding assignment phase heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-10 15:25:05 -07:00 |
|
Nikolaj Bjorner
|
0a29002c2f
|
return unknown if m_array_weak was used and result is satisfiable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 00:20:41 +08:00 |
|
Nikolaj Bjorner
|
48fc3d752e
|
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 15:49:19 -07:00 |
|
Nikolaj Bjorner
|
7e2afca2c6
|
add card operator to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-04-20 13:24:07 -07:00 |
|
Nikolaj Bjorner
|
1123b47fb7
|
bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-04-13 16:15:38 -07:00 |
|
nilsbecker
|
ec76efedbe
|
synchronizing with main repository
|
2019-02-22 00:19:43 +01:00 |
|
nilsbecker
|
28c03ed1de
|
logging support for theory axioms
|
2019-02-21 19:29:35 +01:00 |
|
Bruce Mitchener
|
e570940662
|
Prefer using empty rather than size comparisons.
|
2018-11-27 21:42:04 +07:00 |
|
Nikolaj Bjorner
|
16be5b0e7d
|
fix #1816 - m_parent_selects gets updated while accessing an interator, fix is to rely on the size of the vector for iteration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-25 14:04:17 -08:00 |
|
Nikolaj Bjorner
|
fd9fd52271
|
fixing #1847
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-02 17:13:46 -07:00 |
|
Nikolaj Bjorner
|
aaba1b9b15
|
fix sort retrieval for lambdas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 09:18:40 -07:00 |
|
Nikolaj Bjorner
|
520ce9a5ee
|
integrate lambda expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-26 07:23:04 -07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Nikolaj Bjorner
|
2ede4b2c80
|
fixes based on regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-27 09:31:16 -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
|
4685a5f8ba
|
add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-07 16:42:13 -08:00 |
|
Nikolaj Bjorner
|
8d1fa3ae50
|
move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-07 11:50:06 -08:00 |
|
Christoph M. Wintersteiger
|
0cd406ca0b
|
Fixed initialization order and unused variable warnings.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-07-30 09:09:13 +01:00 |
|
Nikolaj Bjorner
|
2d409c6042
|
revert bug introduced to avoid stack overflow in arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-05-29 14:32:24 -07:00 |
|
Nikolaj Bjorner
|
f8e2fa0337
|
fixes issue #93
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-29 11:11:13 -07:00 |
|
Nikolaj Bjorner
|
ed7e0e11a8
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-28 20:55:13 -07:00 |
|
Leonardo de Moura
|
add684d8e9
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-21 13:32:12 -07:00 |
|