Nikolaj Bjorner
|
abc0cf3775
|
fix offset bug in explain
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-12 10:04:52 -08:00 |
|
Nikolaj Bjorner
|
f5aec6ecdf
|
bugbash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-03 13:12:42 -08:00 |
|
Nikolaj Bjorner
|
21236dc80a
|
working on viable explanations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-02 16:20:13 -08:00 |
|
Nikolaj Bjorner
|
b706434282
|
bugfixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-02 14:30:09 -08:00 |
|
Nikolaj Bjorner
|
d91820fe51
|
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-01 16:24:15 -08:00 |
|
Nikolaj Bjorner
|
172d0ea685
|
merge again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-16 17:07:19 -08:00 |
|
Nikolaj Bjorner
|
0353177fe0
|
import master branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-16 16:56:09 -08:00 |
|
Nikolaj Bjorner
|
f388f58a4b
|
b-and, stats, reinsert variable to heap, debugging
|
2023-12-16 16:32:28 -08:00 |
|
Nikolaj Bjorner
|
d0a59f3740
|
intblast with lazy expansion of shl, ashr, lshr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-16 15:12:57 -08:00 |
|
Bruce Mitchener
|
50e0fd3ba6
|
Use noexcept more. (#7058)
|
2023-12-16 12:14:53 +00:00 |
|
Nikolaj Bjorner
|
9293923b8a
|
Add intblast solver
|
2023-12-15 13:50:38 -08:00 |
|
Nikolaj Bjorner
|
922358b9ba
|
import pdd updates from polysat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-15 08:59:05 -08:00 |
|
Nikolaj Bjorner
|
0520558fc0
|
port updated pdd from polysat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-15 08:54:03 -08:00 |
|
Bruce Mitchener
|
e90a844508
|
Use override more. (#7059)
|
2023-12-15 08:44:57 +00:00 |
|
Nikolaj Bjorner
|
f91655ce15
|
fix divergence reported by Guido Martinez
|
2023-12-13 20:04:47 -08:00 |
|
Nikolaj Bjorner
|
5dfe86fc2d
|
bugfixes in intblast solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-13 14:13:16 -08:00 |
|
Lev Nachmanson
|
536f4f84bb
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2023-12-12 15:23:43 -10:00 |
|
Nikolaj Bjorner
|
c72780d9b9
|
b-and, stats, reinsert variable to heap, debugging
|
2023-12-11 20:22:23 -08:00 |
|
Nikolaj Bjorner
|
4d1d067d42
|
fix divergence reported by Guido Martinez
|
2023-12-07 13:34:35 -08:00 |
|
Nikolaj Bjorner
|
4a9b38e531
|
clean up nla_grobner
|
2023-12-04 17:08:17 -08:00 |
|
Lev Nachmanson
|
fc23a498c4
|
a simple version of choosing a column for gomory cut
|
2023-12-04 15:06:50 -10:00 |
|
Nikolaj Bjorner
|
de75692cb0
|
install importlib-resources for ubuntu doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-04 10:32:02 -08:00 |
|
Nikolaj Bjorner
|
f7415bb677
|
install importlib-resources for ubuntu doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-04 10:32:02 -08:00 |
|
Nikolaj Bjorner
|
f06e07ad0a
|
fix cone of influence computation for terms with nested variables
exposed by #7027, but generally missing. It is less likely to be exposed if input is normalized by distributing multiplication over addition.
|
2023-12-03 12:42:42 -08:00 |
|
Nikolaj Bjorner
|
25dd29907b
|
refine no-effect predicate to include value of ret
|
2023-12-03 12:41:21 -08:00 |
|
Nikolaj Bjorner
|
585d027668
|
remove assert #7032
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-12-02 14:12:41 -08:00 |
|
Nikolaj Bjorner
|
7eab26e3ef
|
try with missed bounds
|
2023-12-02 10:48:40 -08:00 |
|
Lev Nachmanson
|
5784c2da79
|
remove an unnecessary if
|
2023-11-30 08:59:05 -10:00 |
|
Nikolaj Bjorner
|
26440ed3d8
|
deal with ubuntu/clang warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-11-29 15:45:19 -08:00 |
|
Nikolaj Bjorner
|
41a3196c89
|
fix #7024
|
2023-11-29 13:35:30 -08:00 |
|
Christoph M. Wintersteiger
|
16753e43f1
|
Add accessors for RCF numeral internals (#7013)
|
2023-11-23 17:54:23 +01:00 |
|
Nikolaj Bjorner
|
ac105b7d8c
|
remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-11-19 11:47:00 -08:00 |
|
Nikolaj Bjorner
|
4350bd77ac
|
check cancel flag to avoid unsound conflicts
|
2023-11-19 11:43:52 -08:00 |
|
Nikolaj Bjorner
|
35bc522dae
|
#7003
minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
|
2023-11-19 09:59:44 -08:00 |
|
Nikolaj Bjorner
|
5b9fdcf462
|
fix #6997
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-11-15 18:08:48 -08:00 |
|
Nikolaj Bjorner
|
8a4e857294
|
#6523
regressions from changes inside math/lp/int_solver
|
2023-11-13 14:28:03 -08:00 |
|
Nikolaj Bjorner
|
3de5af3cb0
|
fix bug in bound simplification in Gomory for mixed integer linear cuts, enable fixed variable redution after bugfix, add notes that rewriting bounds does not work
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-11-10 16:39:04 +01:00 |
|
EyalBrilling
|
aa9c7912dc
|
fixed possible undefined variable assigment (#6985)
|
2023-11-10 11:36:24 +01:00 |
|
Nikolaj Bjorner
|
bd4d580b17
|
fix #6986
|
2023-11-08 13:49:30 +01:00 |
|
Nikolaj Bjorner
|
e6385f8c85
|
disable bound validation in debug mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-11-07 20:49:26 +01:00 |
|
Nikolaj Bjorner
|
3d99ed9dd4
|
Gomory cut / branch and bound improvements
Improve fairness of cut generation by switching to find_infeasible_int_var with cascading priorities, allow stronger cuts by inlining terms.
|
2023-11-07 19:59:02 +01:00 |
|
Nikolaj Bjorner
|
9f0b3cdc25
|
Add utility to expand sub-terms
|
2023-11-07 19:58:32 +01:00 |
|
Nikolaj Bjorner
|
fb95760137
|
remove template
|
2023-11-07 19:57:50 +01:00 |
|
Nikolaj Bjorner
|
77dab53e9e
|
track number of Gomory cuts
|
2023-11-07 19:57:49 +01:00 |
|
Lev Nachmanson
|
14312ef8a3
|
remove some warnings with clang
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-11-02 15:34:41 -07:00 |
|
Lev Nachmanson
|
08d3a82ce0
|
simplify the jump on entering
|
2023-11-02 11:09:01 -07:00 |
|
Lev Nachmanson
|
bdf1fcf5c1
|
remove an assert
|
2023-11-02 09:59:03 -07:00 |
|
Lev Nachmanson
|
ca6cb0af95
|
add changes in lp with validate_bound and maximize_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-11-02 09:59:03 -07:00 |
|
Nikolaj Bjorner
|
49a071988c
|
remove temporary algebraic numbers from upper layers, move to owner module
|
2023-11-01 03:52:20 -07:00 |
|
Nikolaj Bjorner
|
f97dd34028
|
tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-30 14:54:04 -07:00 |
|