3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-14 16:36:39 +00:00
Commit graph

16 commits

Author SHA1 Message Date
Nikolaj Bjorner
1dca6402fb move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
Nikolaj Bjorner
d0e20e44ff booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
589db2052a fix #3064
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-21 20:26:57 -08:00
Nikolaj Bjorner
0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-17 14:51:13 -08: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
9c099d6b1b fix mb maximization logic, so far not accessible
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-20 16:39:03 -07:00
Nikolaj Bjorner
c725fe7698 tune lra optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-22 17:03:29 -07:00
Nikolaj Bjorner
1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-19 13:04:20 -07:00
Nikolaj Bjorner
5b31f54501 max/min
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-05 14:11:13 -07:00
Nikolaj Bjorner
e29adbf304 fix issues #581: nested timeouts canceled each-other
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-30 11:18:34 -07:00
Nikolaj Bjorner
2428bf18f1 add model correction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-29 19:08:10 -07:00
Nikolaj Bjorner
68c7d64d00 adding model-based opt facility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-27 11:18:20 -07:00
Nikolaj Bjorner
a1aa166ef5 adding local optimization to qsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-26 17:15:24 -07:00
Nikolaj Bjorner
fd6fe87c5d enable qe-lite for UFNIA benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-22 15:41:21 -07:00
Nikolaj Bjorner
3dc2028925 adding min/max
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 09:20:57 -07:00
Nikolaj Bjorner
20bbdfe31a moving remaining qsat functionality over
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 15:35:26 -07:00