mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
19353 commits 23 branches 48 tags 157 MiB
Commit graph

19353 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson a737483ba0 fix a bug in dio 2025-02-03 13:33:26 -10:00
Lev Nachmanson c112df5d41 simplify column 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:26 -10:00
Lev Nachmanson 0958806d4a cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:26 -10:00
Lev Nachmanson 90dbc623fd persist dio handler 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:26 -10:00
Lev Nachmanson 7d8e192344 change int_solver to call find_cube and hnf_cut, conditionally 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:26 -10:00
Lev Nachmanson 44d75da7a5 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:26 -10:00
Lev Nachmanson 28bafa301e fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:25 -10:00
Lev Nachmanson b933a0d6e0 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:25 -10:00
Lev Nachmanson e32ebf109b fixes in dio branching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:25 -10:00
Lev Nachmanson 781471aa6f passes z3test 2025-02-03 13:33:25 -10:00
Lev Nachmanson f336b0d599 collect the explanation correctly 2025-02-03 13:33:24 -10:00
Lev Nachmanson ada3be2679 remove dead code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:24 -10:00
Lev Nachmanson 6af8fbb629 cancel bugs fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:24 -10:00
Lev Nachmanson 7f7dc8750f solving regressions/smt2/b1.smt2 2025-02-03 13:33:24 -10:00
Lev Nachmanson 08a1ddf79f work on incremental version 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:24 -10:00
Lev Nachmanson b47a2687ad use var_register in dioph_eq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:23 -10:00
Lev Nachmanson cdb18ac685 document dioph_eq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:23 -10:00
Lev Nachmanson eb0aeab2a3 remove a global debug variable 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:22 -10:00
Lev Nachmanson b99439599b remove redundant m_row_index from entry 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:22 -10:00
Lev Nachmanson 12ceb1ef26 take dependencies from open_ml 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:22 -10:00
Lev Nachmanson 2a81a1f043 fixes in tigthening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:21 -10:00
Lev Nachmanson bb77ff537b check feasibility immediately after tightening a bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:21 -10:00
Lev Nachmanson 0077a689bd implement explain() 2025-02-03 13:33:21 -10:00
Lev Nachmanson 1eecedf8cb add missing explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:20 -10:00
Lev Nachmanson 143f22e0a5 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:20 -10:00
Lev Nachmanson 472306c0b2 use fixed vars to explain tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:33:20 -10:00
Lev Nachmanson 24aeaed50a test that pivoting is correct in dioph_eq.cpp 2025-02-03 13:33:14 -10:00
Lev Nachmanson 09ec973998 print output file name 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:43 -10:00
Lev Nachmanson 594fa7423f fix the build 2025-02-03 13:30:42 -10:00
Lev Nachmanson a3b81b54db init m_e_matrix on terms instead of the tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson 2bda4d1674 throttle dioph equalities 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson 727ac149a7 change type of m_e_matrix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson 282edcfadf add a template instantiotion 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson 4710260ede handle empty rows in m_e_matrix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson b0be4d58c7 vector access bugs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson f5f4c848ec bug fixes with tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
Lev Nachmanson 9c2ec9b47d bug fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:42 -10:00
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