Nikolaj Bjorner
adad468cd7
allow copy within a user scope #6827
...
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
2023-07-31 19:46:08 -07:00
Nikolaj Bjorner
d263b373ed
update release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:19:33 -08:00
Nikolaj Bjorner
f4e17ecc65
add logging and diagnostics
2022-11-12 18:03:47 -08:00
Nikolaj Bjorner
8da13ae24a
add statistics to verbose output of asserted formulas
2022-11-08 18:37:30 -08:00
Nikolaj Bjorner
ad5fa9433f
add experiment with quot-rem encoding
...
experiment seeks to determine whether quot-rem encoding can substitute the division circuit encoding.
A first test suggests it makes no difference.
2022-10-21 09:25:45 -07:00
Nikolaj Bjorner
876ca2f1a5
fix #6371
2022-09-30 14:51:28 -04:00
Nikolaj Bjorner
616fc2cbd5
fix #6314
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-04 16:23:11 -07: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
32614722ef
fix #6176
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 21:19:20 -07:00
Nuno Lopes
d9fcfdab34
fix debug build
2022-06-17 14:35:33 +01:00
Nikolaj Bjorner
e3c35840bb
remove out
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-20 11:26:16 +01:00
Nikolaj Bjorner
ec57d3b15c
missing switch cases
2022-04-19 16:20:02 +01:00
Nikolaj Bjorner
56d3718cde
add simplification with qe-lite as an option #5767
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-12 03:41:21 -08:00
Nikolaj Bjorner
8ca023d541
expose propagate created
2021-12-17 16:12:47 -08:00
Henrich Lauko
96671cfc73
Add and fix a few general compiler warnings. ( #5628 )
...
* rewriter: fix unused variable warnings
* cmake: make missing non-virtual dtors error
* treewide: add missing virtual destructors
* cmake: add a few more checks
* api: add missing virtual destructor to user_propagator_base
* examples: compile cpp example with compiler warnings
* model: fix unused variable warnings
* rewriter: fix logical-op-parentheses warnings
* sat: fix unused variable warnings
* smt: fix unused variable warnings
2021-10-29 15:42:32 +02:00
Nikolaj Bjorner
3036b88f09
support threading for TRACE mode
2021-10-25 13:35:32 +02:00
Nikolaj Bjorner
a7bc4719c0
fix #5526
...
when propagation claims progress, but is a no-op.
2021-09-01 11:45:21 -07:00
Nikolaj Bjorner
39c3f34a30
remove unused dependency
2021-07-21 09:25:08 -07:00
Nikolaj Bjorner
a8b433e6ac
#5331
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-19 15:58:10 -07:00
Nikolaj Bjorner
4a6083836a
call it data instead of c_ptr for approaching C++11 std::vector convention.
2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
97f560054d
Create CMakeLists.txt
2021-03-17 15:51:50 -07:00
Nikolaj Bjorner
ab0735fde2
separate component for asserted_formulas to break dependency cycles
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-17 15:51:38 -07:00
