Jakob Rath
f72e30e539
Add BDD utilities; use them for narrowing/propagation of linear equality constraints ( #5192 )
...
* Add a few helper methods for encoding sets of integers as BDDs
* Use BDD functions in solver
* Add bdd::find_int
* Use bdd::find_int in solver
* Add narrowing for linear equality constraints
* Simplify code for linear propagation
* Add test for later
* Narrowing can only handle linear constraints with a single variable
* Need to push_cjust
2021-04-16 08:44:18 -07:00
Nikolaj Bjorner
2fef6dc502
more scaffolding
2021-03-21 11:31:14 -07:00
Nikolaj Bjorner
67c4777514
fix #2548 fix #2530
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-09-13 15:03:04 +02:00
Nuno Lopes
87a96d7bd4
fix mutexes hanging due to access to free'd memory
...
Thanks to Kevin de Vos for reporting the bug & testing the fix
2019-09-03 20:02:21 +01:00
Nuno Lopes
c21f0c2f00
restore most global muxes as heap-allocated to avoid crashes with hard-kills like ctrl-c
2019-06-13 18:42:57 +01:00
Nuno Lopes
cf3e649462
fix crash on Mac due to different destruction order of globals
...
the mutex in memory_manager has to be destroyed after all mem deallocations happen
2019-06-13 11:22:18 +01:00
Nikolaj Bjorner
71c38a08e5
add initialization
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 19:28:08 -07:00
Nuno Lopes
a53ff6f21c
turn locks into no-ops when compiled with -DSINGLE_THREAD
2019-06-05 12:11:27 +01:00
Nikolaj Bjorner
9262908ebb
mux
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Bruce Mitchener
76eb7b9ede
Use nullptr.
2018-02-12 14:05:55 +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
Nuno Lopes
c577ab361b
fix assorted undefined behaviors caught by clang
...
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-05-23 11:45:12 +01:00
Nuno Lopes
6c22edc988
fix assorted compiler warnings
...
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-05-16 11:44:58 +01: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
2c464d413d
Reorganizing source code. Created util dir
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-20 10:19:38 -07:00
