Nikolaj Bjorner
9293923b8a
Add intblast solver
2023-12-15 13:50:38 -08:00
Nikolaj Bjorner
85f9c7eefa
replace restore_size_trail by more generic restore_vector
...
other updates:
- change signature of advance_qhead to simplify call sites
- have model reconstruction replay work on a tail of dependent_expr state, while adding formulas to the tail.
2022-11-28 11:45:56 +07:00
Bruce Mitchener
5014b1a34d
Use = default for virtual constructors.
2022-08-05 18:11:46 +03:00
Bruce Mitchener
1eb84fe4b9
Mark override methods appropriately. ( #6207 )
2022-07-29 23:29:15 +02:00
Nuno Lopes
9eb566b401
simplify some constructors/destructors
2021-05-23 12:39:49 +01:00
Nikolaj Bjorner
15a7621e27
remove template dependency for trail objects
2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
830f314a3f
fixes to dt_solver and related
2021-02-27 11:03:20 -08:00
Nikolaj Bjorner
a152bb1e80
remove template Context dependency in every trail object
2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
1b768c9b3a
fix #4805
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-20 12:11:38 -08:00
Nikolaj Bjorner
ab199dedf9
debug arith/mbi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-02 12:13:19 -08:00
Nikolaj Bjorner
44679d8f5b
arith_solver ( #4733 )
...
* porting arithmetic solver
* integrating arithmetic
* lp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-16 10:49:46 -07:00
Nikolaj Bjorner
fa58a36b9f
model refactor ( #4723 )
...
* refactor model fixing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing cond macro
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add macros dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* deps and debug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add dependency to normal forms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* compile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix leal regression
* complete model fixer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fold back private functionality to model_finder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* avoid duplicate fixed callbacks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-05 14:13:05 -07:00
Nikolaj Bjorner
6a4261d1af
debugging bv
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-15 15:37:31 -07:00
Nikolaj Bjorner
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
3e9479d01a
a lot of seq churn
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-17 18:21:40 -07:00
Nikolaj Bjorner
b889b110ee
bool_vector, some spacer tidy
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-05 12:59:04 -07:00
Nikolaj Bjorner
1123b47fb7
bapa
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-13 16:15:38 -07:00
Nikolaj Bjorner
c7d0d4e191
add c-cube's recursive function theory
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-17 04:56:58 -07:00
Bruce Mitchener
76eb7b9ede
Use nullptr.
2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc
Use override rather than virtual.
2018-02-10 09:56:33 +07:00
Simon Cruanes
d5e134dd94
wip: add recursive functions
2017-12-25 22:51:39 +01:00
Arie Gurfinkel
88a35119b9
moved obj_equiv_class to ast
2017-08-01 19:24:50 -04: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
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
Nikolaj Bjorner
5dc2afa33f
add bceq experiment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-29 10:59:22 -07:00
