Nikolaj Bjorner
7151c5ac6e
fixes to finite domain arrays
...
- relevancy could be off and array solver doesn't compensate, #7544
- enforce equalities across store for small domain axioms #8065
2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
e4697fe18e
remove set cardinality operators from array theory. Make final-check use priority levels
...
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
2026-02-18 20:56:51 -08:00
Nikolaj Bjorner
c387b20ac6
move smt params to params directory, update release.yml
2025-06-09 10:47:22 -07:00
Nuno Lopes
97c70ba501
remove some uneeded constructors
2024-12-22 15:06:58 +00:00
Nikolaj Bjorner
fb5bbb8074
read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0
2024-12-22 14:07:29 +01:00
Nikolaj Bjorner
05e28e4344
fix #5812
2022-02-04 13:08:52 -08:00
Nikolaj Bjorner
15a7621e27
remove template dependency for trail objects
2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
becf423c77
remove level of indirection for context and ast_manager in smt_theory ( #4253 )
...
* remove level of indirection for context and ast_manager in smt_theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add request by #4252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move to def
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 16:46:03 -07:00
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
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
4fcc4d07ae
fix #2277 fix #2221
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-14 19:05:40 +02:00
Bruce Mitchener
7167fda1dc
Use override rather than virtual.
2018-02-10 09:56:33 +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
d4c98c1ab4
Corrected fix to #354 : The parameters got shared between the MBQI checker and main context, overriding m_array_laziness to 0 which caused missing propagations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-11 09:38:05 -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
4bc044c982
update header guards to be C++ style. Fixes issue #9
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Leonardo de Moura
add684d8e9
checkpoint
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-21 13:32:12 -07:00
