Lev Nachmanson
|
6776575b00
|
remove an unused field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-22 08:59:38 -07:00 |
|
Lev Nachmanson
|
c42c61254d
|
reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-21 15:35:14 -07:00 |
|
Nikolaj Bjorner
|
5260fb5077
|
added some comments
|
2025-03-20 18:07:25 -10:00 |
|
Nikolaj Bjorner
|
281512809d
|
formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-20 17:16:51 -10:00 |
|
Lev Nachmanson
|
feeb3b47e9
|
cleaning up the inner tightening code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-20 17:22:23 -07:00 |
|
Lev Nachmanson
|
924daa0579
|
avoid the variable mapping to m_ematrix and suppressing redundand constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-20 09:57:26 -07:00 |
|
Nikolaj Bjorner
|
e12271ee8f
|
use more descriptive functions than casting comparisons
|
2025-03-19 21:03:36 -10:00 |
|
Nikolaj Bjorner
|
873b8e7e65
|
tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-19 17:57:52 -10:00 |
|
Nikolaj Bjorner
|
ddbf6e1a67
|
use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-19 17:40:43 -10:00 |
|
Lev Nachmanson
|
238e7fd6dd
|
fix a print out
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-19 19:55:36 -07:00 |
|
Lev Nachmanson
|
48430a19bc
|
attempt to use the gcd of fixed vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-19 13:56:55 -07:00 |
|
Nikolaj Bjorner
|
0a618445bc
|
add comment on derivation of bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-18 17:39:59 -10:00 |
|
Lev Nachmanson
|
b2d4790b42
|
detect more m_terms_to_tighten
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-18 10:28:43 -07:00 |
|
Lev Nachmanson
|
a57a389eef
|
remove an unused field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-18 10:08:02 -07:00 |
|
Lev Nachmanson
|
c451a360f1
|
add public access to bijection key_val iterator
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-18 09:54:02 -07:00 |
|
Nikolaj Bjorner
|
ff685d5eb5
|
nit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 20:48:32 -07:00 |
|
Nikolaj Bjorner
|
c47d053781
|
neatify loops
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 20:41:07 -07:00 |
|
Nikolaj Bjorner
|
cb0131f6dc
|
remove 'unsat' move, we already have 'conflict'. Add display for cancelled
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 19:14:29 -07:00 |
|
Nikolaj Bjorner
|
0e8ba37015
|
code review updates, tidy pretty printer for column info
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 18:44:40 -07:00 |
|
Nikolaj Bjorner
|
87810c6ad9
|
fix bug introduced while absstracting m_conflict_index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 10:42:41 -07:00 |
|
Nikolaj Bjorner
|
14c672ff7d
|
isolate m_conflict_index functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 10:34:30 -07:00 |
|
Nikolaj Bjorner
|
0b3ef828d5
|
add systematic way to combine lia_move results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-16 10:24:44 -07:00 |
|
Nikolaj Bjorner
|
beee2182dd
|
nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-15 18:17:27 -07:00 |
|
Nikolaj Bjorner
|
78d66b9251
|
print also column values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-15 17:01:18 -07:00 |
|
Lev Nachmanson
|
c1b1a8c3ab
|
remove term sorting by the span
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-15 12:33:09 -10:00 |
|
Lev Nachmanson
|
e532308b92
|
sort terms by weight for tightening
|
2025-03-15 06:18:42 -10:00 |
|
Lev Nachmanson
|
ae30e2c49f
|
more aggressive term tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-14 16:38:37 -10:00 |
|
Lev Nachmanson
|
e846c2ac8b
|
try another sorting of terms to tighten
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-14 09:30:32 -07:00 |
|
Lev Nachmanson
|
364abb656e
|
separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-14 05:31:50 -10:00 |
|
Lev Nachmanson
|
62435b15bb
|
detect non integral terms in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-14 05:17:33 -10:00 |
|
Lev Nachmanson
|
0c24536096
|
testing! disable gomory cut in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-13 19:52:11 -10:00 |
|
Lev Nachmanson
|
6cce535f83
|
optimize entrry recalculation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-13 19:22:44 -07:00 |
|
Lev Nachmanson
|
699049f1dc
|
allow bounds tightening on fixed columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-12 17:31:34 -07:00 |
|
Lev Nachmanson
|
e08a0cc29e
|
add comments and renaming
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-12 10:10:03 -10:00 |
|
Lev Nachmanson
|
3238d94813
|
profile and remove dead code from dioph_eq.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-10 14:58:19 -10:00 |
|
Lev Nachmanson
|
64901a4e4f
|
improved dio handler
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-10 07:06:36 -10:00 |
|
Nikolaj Bjorner
|
e05f75d74c
|
switch to ubuntu 24 for python packaging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-09 20:53:36 -07:00 |
|
Nikolaj Bjorner
|
07fa36e37a
|
fix #7466
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-09 18:50:07 -07:00 |
|
Nikolaj Bjorner
|
ab0323c22b
|
update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-09 17:19:02 -07:00 |
|
Nikolaj Bjorner
|
ea1360ee46
|
fix #7578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-09 17:01:42 -07:00 |
|
Nikolaj Bjorner
|
c002c77e5a
|
fix #7569
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-07 11:53:01 -08:00 |
|
Nikolaj Bjorner
|
54c6b11621
|
Update README.md
redist license pointer
|
2025-03-07 11:47:32 -08:00 |
|
Nikolaj Bjorner
|
80f00f191a
|
fix #7572 and fix #7574
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-07 10:46:29 -08:00 |
|
Nikolaj Bjorner
|
8df45b442b
|
try ubuntu 24
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-05 13:58:39 -08:00 |
|
Nikolaj Bjorner
|
b47ec2074b
|
try version 75
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-05 11:26:12 -08:00 |
|
Nikolaj Bjorner
|
3e7f4839d1
|
68
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-04 17:14:10 -08:00 |
|
Nikolaj Bjorner
|
dedfe9019d
|
remove downlevel setup in nightly.yaml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-04 07:38:28 -08:00 |
|
Nikolaj Bjorner
|
f698dea2b0
|
downlevel setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-03 18:25:20 -08:00 |
|
Nikolaj Bjorner
|
e6855bb299
|
disable setup tool install
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-03 16:01:45 -08:00 |
|
Nikolaj Bjorner
|
d714f1b6c5
|
update path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-03 14:23:33 -08:00 |
|