Lev Nachmanson
9434847ce7
bug fixes
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:42 -10:00
Lev Nachmanson
bc2c67c7ea
debug dio with static matrix
2025-02-03 13:30:42 -10:00
Lev Nachmanson
df577eecd6
unifying vectors into eprime_entry
2025-02-03 13:30:42 -10:00
Lev Nachmanson
f3b33888ab
dio with static_matrix initial setup
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
60a38cdd22
do not use conflicts with fresh vars to create branches
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
dc15dbfc31
remove disabling return
2025-02-03 13:30:41 -10:00
Lev Nachmanson
5f0077626e
remove more warnings
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
fdae46fb60
remove a warning
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
2c7c708848
fix ubuntu's build
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
fa907c5e8c
prepare using fresh vars in cuts
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
110593f086
use cuts from proofs, remove gcc warnings
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
4e381609db
enable cuts from proofs
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
c30600c2ef
fixes in dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
5f70eb0524
do not eliminate fresh variables when tightening
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
1769c6059e
fixed dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:41 -10:00
Lev Nachmanson
2ca7b31d13
comment out global_max_change
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
f05d1abccc
debug dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
8d8ee99db3
test tightening with S
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
7d8212646d
handle sat with tightening
2025-02-03 13:30:40 -10:00
Lev Nachmanson
9118abebc7
cosmetics
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
e0185121c5
use u_dependency in eprime_pair
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
b20566a488
work on tighten_with_S
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
a1a9825e43
remove a throw
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
a75eff6525
bug fix
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
0c6dcfedb8
small optimization
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
9ec55de5c6
optimize dio changes
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
7c9cb44c94
less eager dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
4fea4259ec
fix the build
2025-02-03 13:30:40 -10:00
Lev Nachmanson
1a99fa56cb
handle zero rows correctly
2025-02-03 13:30:40 -10:00
Lev Nachmanson
178411ad0c
dio passes regression\smt2 tests with limited functionality
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
dcd80ac95b
fix term_o init
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
c29d04dc3c
debug dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
1cb71b4648
debug dio
2025-02-03 13:30:39 -10:00
Lev Nachmanson
db899fd670
fix in substitution of fresh variables, clean column.h
2025-02-03 13:30:39 -10:00
Lev Nachmanson
5f71604198
bug fix in init and getting explanations
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
0814fa40b0
create a conflict explanation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
53605d4e0a
a version with less pointers: got a conflict
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:00 -10:00
Lev Nachmanson
876cbc527d
in the middle
2025-02-03 13:24:33 -10:00
Lev Nachmanson
778db5e763
use std::list
2025-02-03 13:24:33 -10:00
Lev Nachmanson
c1e577e932
fix the crash
2025-02-03 13:24:33 -10:00
Lev Nachmanson
484af98af6
crash
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:24:33 -10:00
Lev Nachmanson
0eeef3b806
fix the build
2025-02-03 13:24:33 -10:00
Lev Nachmanson
0b9b1c4472
move some functionality from int_solver to int_solver::imp
2025-02-03 13:24:33 -10:00
Lev Nachmanson
66b778cb25
fix the build
2025-02-03 13:24:33 -10:00
Lev Nachmanson
7050589adf
prepare for calling diophantine equations
2025-02-03 13:24:33 -10:00
Lev Nachmanson
049520483f
add parameter to control calling diophantine equations
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:24:33 -10:00
Nikolaj Bjorner
17d47ca8c7
fix #7493
2025-02-02 15:00:31 -08:00
Nikolaj Bjorner
99cbfa715c
Add a sharp throttle to lia2card tactic to control overhead in default tactic mode
...
lia2card was added to qfuflia tactic based on a user scenario, but it overshot: lia2card is by default harmful. It is here tamed to only convert binary variables and throttle on nested ite terms
2025-02-02 13:58:51 -08:00
Nikolaj Bjorner
fd2a8a554d
disable small clause generation for propagation
2025-02-01 20:04:29 -08:00
Nikolaj Bjorner
0ef26983fc
release
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-31 17:31:37 -08:00
