Skip to content

Integrate Diophantine handler #7548

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 147 commits into from
Feb 11, 2025
Merged

Integrate Diophantine handler #7548

merged 147 commits into from
Feb 11, 2025

Conversation

levnach
Copy link
Contributor

@levnach levnach commented Feb 10, 2025

No description provided.

levnach added 30 commits February 3, 2025 13:24
@levnach
add parameter to control calling diophantine equations
0495204 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
prepare for calling diophantine equations
7050589
@levnach
fix the build
66b778c
@levnach
move some functionality from int_solver to int_solver::imp
0b9b1c4
@levnach
fix the build
0eeef3b
@levnach
crash
484af98 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
fix the crash
c1e577e
@levnach
use std::list
778db5e
@levnach
in the middle
876cbc5
@levnach
a version with less pointers: got a conflict
53605d4 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
create a conflict explanation
0814fa4 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
bug fix in init and getting explanations
5f71604 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
fix in substitution of fresh variables, clean column.h
db899fd
@levnach
debug dio
1cb71b4
@levnach
debug dio
c29d04d 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
fix term_o init
dcd80ac 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
dio passes regression\smt2 tests with limited functionality
178411a 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
handle zero rows correctly
1a99fa5
@levnach
fix the build
4fea425
@levnach
less eager dio
7c9cb44 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
optimize dio changes
9ec55de 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
small optimization
0c6dcfe 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
bug fix
a75eff6 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
remove a throw
a1a9825 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
work on tighten_with_S
b20566a 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
use u_dependency in eprime_pair
e018512 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
cosmetics
9118abe 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
handle sat with tightening
7d82126
@levnach
test tightening with S
8d8ee99 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
debug dio
f05d1ab 
Signed-off-by: Lev Nachmanson <[email protected]>
levnach added 21 commits February 3, 2025 19:21
@levnach
rebase with master
4a953eb 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
call normalize_e_by_gcd() only when moving an entry from F to S
f5150ec
@levnach
add stats on m_dio_branching_conflicts
e419e58 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
disallow duplicates in a queue
30064d4 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
avoid usisg indexed_vector for term operations
46a7ad6
@levnach
fix assert
78fea66 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
ignore large changed_columns
f64edb6 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
throttle the branching in dio
28cc740 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
stricter is_in_sync paying attenion to m_row2fresh_defs
df88e3a 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
comment change
67318e2 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
remove the fresh definition when removing its column
470ea5e 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
try sorting terms before tightening
c12625d 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
try another sort in tightening
ac48ff5
@levnach
test
9c4327a
@levnach
try markovich number
07a1a88 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
try markovich number
86e39f3 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
revert the term sorting
c79d470 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
Revert "revert the term sorting"
5f74fda 
This reverts commit c79d470.
@levnach
more accurate work with Markovich number
4bc14d7 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
disabling dio handler by default, and fix a print out
2c7509a 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach
fix the test build
86b1f9e 
Signed-off-by: Lev Nachmanson <[email protected]>
@levnach levnach merged commit e920291 into master Feb 11, 2025
25 checks passed
@levnach levnach deleted the reb_dio branch February 11, 2025 22:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NikolajBjorner NikolajBjorner NikolajBjorner left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@levnach @NikolajBjorner