Nikolaj Bjorner
|
01ba749a5d
|
focused query to optimize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-13 10:01:34 -08:00 |
|
Nikolaj Bjorner
|
a003139704
|
update description
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-13 09:59:17 -08:00 |
|
Nikolaj Bjorner
|
45f3ea3bf4
|
add treesitter functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-13 09:57:26 -08:00 |
|
Lev Nachmanson
|
bedc95c4c7
|
use static_cast to avoid the warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-13 07:07:12 -10:00 |
|
Phil Clayton
|
e6a089e63d
|
Fix build when Z3_API macro is non-empty (#7553)
API function definitions are updated to be consistent with header files.
|
2025-02-13 08:46:08 -08:00 |
|
Nikolaj Bjorner
|
d10efa667a
|
stub for treesitter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-12 19:56:33 -08:00 |
|
Nikolaj Bjorner
|
5c18ce8cea
|
genai testing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-12 19:55:39 -08:00 |
|
Nikolaj Bjorner
|
4e51af1167
|
update instructions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-11 22:05:19 -08:00 |
|
Nikolaj Bjorner
|
94d3c591b5
|
make sure ackermann works with arrays that have more than one argument
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-11 21:28:31 -08:00 |
|
Nikolaj Bjorner
|
a3739aa934
|
add mycop in addition to code complete
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-11 20:04:52 -08:00 |
|
Nikolaj Bjorner
|
9ea921ba8e
|
update spacer projection for arrays to allow ackerman reduction for non-integer arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-02-11 17:38:56 -08:00 |
|
Lev Nachmanson
|
e920291393
|
fixing the default parameters of dio and rename m_gomory_cuts to m_cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
957b177c64
|
set arith.lp.dio_cuts_enable_gomory to False by default
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5ec10e0250
|
address the review
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
8a9edd1aa7
|
fix the test build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
79e3f8ab39
|
disabling dio handler by default, and fix a print out
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
2131e9b4e4
|
more accurate work with Markovich number
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bdb8f54150
|
Revert "revert the term sorting"
This reverts commit c79d4708cb.
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5ebee24850
|
revert the term sorting
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
f2c1fd4c14
|
try markovich number
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
cec8dc2e6e
|
try markovich number
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3f2d2e8348
|
test
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
b6701d57f9
|
try another sort in tightening
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5b0b224a5c
|
try sorting terms before tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
dcd5783232
|
remove the fresh definition when removing its column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
17d68c18aa
|
comment change
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
d90b94d0e2
|
stricter is_in_sync paying attenion to m_row2fresh_defs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
134bed826a
|
throttle the branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bd8cf29df7
|
ignore large changed_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3ac11cd136
|
fix assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
cf4e402a0f
|
avoid usisg indexed_vector for term operations
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
440d78f237
|
disallow duplicates in a queue
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
7e02dfe484
|
add stats on m_dio_branching_conflicts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
0bf3ca87e7
|
call normalize_e_by_gcd() only when moving an entry from F to S
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
99538567a7
|
rebase with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
a19e10912f
|
make dio less aggressive, allow other cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
fee707842d
|
register m_added_terms in m_changed_terms
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
21f67ef942
|
out of bounds fixes
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3b3d8cee03
|
use m_chandedNterms to tighten terms
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
65bdd58d3e
|
remove struct entry
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
a9098a5785
|
optimise l terms addition
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3e7e903d19
|
use the trail to undo add_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
9c510018b3
|
fix the debug build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
058b9e4a6d
|
optimise rewrite_eqs to avoid fresh variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ed3df333b3
|
make rewrite_eq boolean, and relax an ASSERT
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ca7c128d3f
|
clean up fresh definitions on a pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
b027761845
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bb869fd020
|
don't store fresh definitions in m_e_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
e5ffc3cfae
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
d7de7eb732
|
remove recalculated entries from S
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|