Nikolaj Bjorner
|
f181e3aa81
|
add comment on derivation of bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
dd19b381d8
|
detect more m_terms_to_tighten
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
307af0fd97
|
remove an unused field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
fc1c8c4cc4
|
add public access to bijection key_val iterator
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
8b5510bcd6
|
nit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
7577f6fea0
|
neatify loops
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
f091b6ffdd
|
remove 'unsat' move, we already have 'conflict'. Add display for cancelled
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
1af2474f7b
|
code review updates, tidy pretty printer for column info
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
32028083fb
|
fix bug introduced while absstracting m_conflict_index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
f3b34fd835
|
isolate m_conflict_index functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
ff5ae4d1ed
|
add systematic way to combine lia_move results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
00277ba3cf
|
nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
488c74d3cc
|
print also column values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
22cfab3d42
|
remove term sorting by the span
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
12203fc69a
|
sort terms by weight for tightening
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
0a3c118701
|
more aggressive term tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
50418fa170
|
try another sorting of terms to tighten
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
ec7c61569d
|
separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
7c12a029e2
|
detect non integral terms in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
a62d664ae4
|
testing! disable gomory cut in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
5e2d000369
|
optimize entrry recalculation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
ecfbdbbd23
|
allow bounds tightening on fixed columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
f501aea3eb
|
add comments and renaming
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
a522e81652
|
profile and remove dead code from dioph_eq.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
6f7b749ff9
|
improved dio handler
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
30021dd74f
|
fix #7590 logic alphabet soup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-19 08:57:32 -10:00 |
|
Nikolaj Bjorner
|
03f18c148e
|
some more copilot aided updated
|
2025-03-19 08:57:32 -10:00 |
|
Nikolaj Bjorner
|
2ecf6dc53c
|
add code for free bounds axiom, but keep it disabled
|
2025-03-19 08:57:31 -10:00 |
|
Nikolaj Bjorner
|
99ec42c0d7
|
additional simplifications to seq
|
2025-03-19 08:57:31 -10:00 |
|
LeeYoungJoon
|
c1719e9ffa
|
Fix : typo-in-simplify-tactic (#7587)
|
2025-03-18 13:43:12 -10:00 |
|
Nikolaj Bjorner
|
2e2a2e28df
|
use iterators on goal and other refactoring
|
2025-03-16 20:04:04 -07:00 |
|
Nikolaj Bjorner
|
eb97fcc273
|
mild refactoring
|
2025-03-16 12:24:41 -07:00 |
|
Nikolaj Bjorner
|
0e881e7abb
|
fix #7584
|
2025-03-15 13:33:08 -07:00 |
|
Nikolaj Bjorner
|
7c226f40df
|
fix #4117
|
2025-03-12 20:14:36 -07:00 |
|
Nikolaj Bjorner
|
382bd05d1b
|
gitignore
|
2025-03-12 17:18:37 -07:00 |
|
Nikolaj Bjorner
|
13c098f4b2
|
better equality solving pre-processing with bv
|
2025-03-12 17:18:26 -07:00 |
|
Nikolaj Bjorner
|
d980ac9a05
|
fix #7582
|
2025-03-12 17:17:47 -07:00 |
|
Nikolaj Bjorner
|
fa5a50c4f9
|
fix #7295
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-12 11:43:31 -07:00 |
|
Nikolaj Bjorner
|
021e8558df
|
update minor version to 14.2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-10 19:08:34 -07:00 |
|
Nikolaj Bjorner
|
3c0d786e6e
|
install setup tools for python packaging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-10 15:50:08 -07: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 |
|