Lev Nachmanson
|
39955f1d04
|
remove a function from lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-05-12 14:02:17 -07:00 |
|
Lev Nachmanson
|
4e56834b76
|
test
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-05-12 14:02:17 -07:00 |
|
Lev Nachmanson
|
a527667fc0
|
shuffle more functionality from lar_solver.h to lar_solver::imp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-05-12 14:02:17 -07:00 |
|
Lev Nachmanson
|
c81eb74c93
|
apply the slack idea in a loop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-05-12 14:02:17 -07:00 |
|
Lev Nachmanson
|
e041fe95bc
|
slack
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-05-12 14:02:17 -07:00 |
|
Nikolaj Bjorner
|
792ffeeda7
|
fix latent sign bug
|
2025-04-23 17:22:57 -07:00 |
|
Nikolaj Bjorner
|
fe1fff3b7e
|
add scaffolding for experiments with slack
|
2025-04-23 17:07:50 -07:00 |
|
Nikolaj Bjorner
|
12ccf59ab9
|
rename fields to compile on c++ platforms
|
2025-04-23 17:06:15 -07:00 |
|
Nikolaj Bjorner
|
e41acd7b50
|
convert m_r_upper and m_r_lower bounds to plain vectors
manage backtracking state together with backtracking of column data.
|
2025-04-23 16:33:38 -07:00 |
|
Nikolaj Bjorner
|
fae60946bf
|
consolidate some bounds references
|
2025-04-23 15:45:44 -07:00 |
|
Nikolaj Bjorner
|
7641393f8a
|
use inlined functions
|
2025-04-23 14:28:31 -07:00 |
|
Nikolaj Bjorner
|
5cc57b8958
|
coalesce updates to bounds
|
2025-04-23 14:05:17 -07:00 |
|
Nikolaj Bjorner
|
d73d104ded
|
remove overwriting x,y,rval
|
2025-04-23 09:17:22 -07:00 |
|
Nikolaj Bjorner
|
ff920ba51b
|
handle root expressions, and checking exponentiation with nlsat
this one is for you @matthai
|
2025-04-22 13:47:47 -07:00 |
|
Lev Nachmanson
|
a1673f2bdd
|
fallback to Gomory cuts and gcd conflicts if dio fails
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-21 17:10:32 -07:00 |
|
Lev Nachmanson
|
ab9f3307d6
|
change the default of running dio to true, and running gcd to false, remove branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
dbde713eb3
|
remove testing code in is_big_term_on_no_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
1131d5294d
|
fix a bug in tracking the changes in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
d289495ca4
|
allow gcd when dio ignores some terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
17af18fe31
|
make gcd call in dio optional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
436eefbce2
|
always remove the tightened term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
dc7185d0a4
|
change the name of m_changed_columns to m_changed_f_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
32e77d8214
|
typo
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
cb1818f4b8
|
reject more terms with big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
1cde40bddb
|
dio_calls_period=4
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
87e2ce8948
|
Update lp_settings.h - m_dio_calls_period = 4
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
59edb81f86
|
Update lp_settings.cpp
white space change
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
8db9f52386
|
add parameter m_dio_calls_period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
ae97ee09d9
|
throttle dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
972f80188a
|
throttle dio for big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Lev Nachmanson
|
3e49d9fcfe
|
reuse dio branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-04-18 18:24:50 -07:00 |
|
Nikolaj Bjorner
|
8035edbe65
|
remove lp_assert
|
2025-04-14 11:10:26 -07:00 |
|
Nikolaj Bjorner
|
a39efbb008
|
fix #7607
|
2025-04-05 11:58:47 -07:00 |
|
Lev Nachmanson
|
e92ccddb23
|
change line breaks
|
2025-03-24 15:38:57 -10:00 |
|
Lev Nachmanson
|
17bd02d1a3
|
change a comment
|
2025-03-24 15:29:19 -10:00 |
|
Nikolaj Bjorner
|
8bbe752d7d
|
remove dead code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 12:47:23 -07:00 |
|
Lev Nachmanson
|
dee3cf8de4
|
remove an unused field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
9302a02a81
|
reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
9a62ed5ab2
|
added some comments
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
c634701b8f
|
formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
f073da9edd
|
cleaning up the inner tightening code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
8c96178c0b
|
avoid the variable mapping to m_ematrix and suppressing redundand constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
29c5c20267
|
use more descriptive functions than casting comparisons
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
7fb40e86eb
|
tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-03-24 07:44:13 -10:00 |
|
Nikolaj Bjorner
|
a41bd38a3a
|
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-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
676a536e9e
|
fix a print out
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
Lev Nachmanson
|
d507d0fdb4
|
attempt to use the gcd of fixed vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-03-24 07:44:13 -10:00 |
|
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 |
|