Nikolaj Bjorner
9293923b8a
Add intblast solver
2023-12-15 13:50:38 -08:00
Nikolaj Bjorner
08599177d0
fix #6808
...
remove bv_eq_axioms as an external option to toggle.
Diseqalities have to be enforced for extensionality.
There are no internal code paths where the option is set to false.
2023-07-13 10:47:55 -07:00
Nuno Lopes
d30cb55bae
don't flush stream when printing param vals
2023-01-03 09:35:17 +00:00
Nikolaj Bjorner
48b13291d1
add bv-size reduce #6137
...
- add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
2022-08-16 16:35:14 -07:00
Nikolaj Bjorner
964e513353
re-add bv_eq_axioms, fix #5842
2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
6202cd5394
fix #5842
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-16 17:38:19 +02:00
Nikolaj Bjorner
7c2bdfe3fb
delay internalization, relevancy ( #4707 )
...
* delay evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update bv_solver.cpp
* delay internalize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove gc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add bv delay option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-23 17:12:01 -07:00
Nikolaj Bjorner
b9cbb08858
shuffle dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 09:51:39 -07:00
Nikolaj Bjorner
ca3ec22b7a
handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-16 23:29:24 -07:00
Nikolaj Bjorner
f20e95184e
remove old_simplify dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 13:29:51 -07:00
Nikolaj Bjorner
2b82fd5d0c
updated include directives
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-01 10:51:47 -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
Christoph M. Wintersteiger
8bde7b8a4c
Added facilities for dumping smt_params for debugging purposes
2016-06-23 19:31:00 +01:00
Leonardo de Moura
1c96a7d52f
Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option .
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-04-03 15:51:09 -07:00
Leonardo de Moura
773f82a44c
connected smt_params with new parameter infrastructure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 14:47:34 -08:00
