3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00

Commit graph

  • abac52e1d7 remove var_register_dio.h Lev Nachmanson 2025-01-20 07:33:33 -1000
  • 89eec4cc80 test dio Lev Nachmanson 2025-01-20 07:31:30 -1000
  • 5a72117528 debug dio Lev Nachmanson 2025-01-16 14:17:53 -1000
  • 0027ae21e8 bug fixes Lev Nachmanson 2025-01-05 17:00:54 -1000
  • 5158797233 refine trail iterations with lar.m_terms Lev Nachmanson 2025-01-05 16:22:55 -1000
  • 9a9ccf19c5 introdure lar_term.ext_coeffs(), dio passes some tests Lev Nachmanson 2025-01-04 07:34:07 -1000
  • 083926c658 debug dio Lev Nachmanson 2025-01-03 12:34:51 -1000
  • a0ece6dd2c cleanup Lev Nachmanson 2025-01-01 11:21:16 -1000
  • ceeece6770 debug dio Lev Nachmanson 2025-01-01 09:02:20 -1000
  • ac5c50f179 fix ubuntu build in dio Lev Nachmanson 2024-12-29 13:33:37 -1000
  • c1ece49694 track changed columns in dio\ Lev Nachmanson 2024-12-29 13:22:47 -1000
  • 008e9229a5 use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp Lev Nachmanson 2024-12-24 12:49:53 -1000
  • 57b665d075 work on incremental dio Lev Nachmanson 2024-12-24 07:32:49 -1000
  • 28556ce625 cleanup Lev Nachmanson 2024-12-24 06:32:25 -1000
  • 862dc91cb2 work on incremental dio Lev Nachmanson 2024-12-23 18:01:57 -1000
  • fd3bd088a4 remove some warnings Lev Nachmanson 2024-12-20 13:59:43 -1000
  • 9a96aa94e6 test Lev Nachmanson 2024-12-20 13:52:38 -1000
  • bef313f7a0 test Lev Nachmanson 2024-12-20 12:40:59 -1000
  • 7ecac27335 fix a bug in dio Lev Nachmanson 2024-12-20 12:37:07 -1000
  • b0383da8f2 fix a bug in dio Lev Nachmanson 2024-12-20 12:28:17 -1000
  • 7fe703e229 simplify column Lev Nachmanson 2024-12-20 10:37:23 -1000
  • 8d747865ae cosmetics Lev Nachmanson 2024-12-16 12:36:52 -1000
  • deac00ada3 persist dio handler Lev Nachmanson 2024-11-26 19:34:52 -0800
  • 2c8a6f83e4 change int_solver to call find_cube and hnf_cut, conditionally Lev Nachmanson 2024-11-21 19:33:40 -0800
  • 39da4f6dbd remove an assert Lev Nachmanson 2024-11-19 11:58:49 -0800
  • 28d41783b8 fix the build Lev Nachmanson 2024-11-19 11:51:46 -0800
  • 397fdf657d fix the build Lev Nachmanson 2024-11-19 11:50:24 -0800
  • 63980f3bfd fixes in dio branching Lev Nachmanson 2024-11-19 11:49:14 -0800
  • 6bc7662580 passes z3test Lev Nachmanson 2024-11-18 21:28:50 -0800
  • 174185582a collect the explanation correctly Lev Nachmanson 2024-11-18 19:17:53 -0800
  • bc0fdfe158 remove dead code Lev Nachmanson 2024-11-18 10:19:25 -0800
  • c300843585 cancel bugs fixes Lev Nachmanson 2024-11-17 19:54:52 -0800
  • e4f3b5753f solving regressions/smt2/b1.smt2 Lev Nachmanson 2024-11-17 14:32:04 -0800
  • 71c433908c work on incremental version Lev Nachmanson 2024-11-15 11:44:03 -0800
  • d68ebeeb9f use var_register in dioph_eq Lev Nachmanson 2024-11-07 15:47:21 -0600
  • 480c48f93d document dioph_eq Lev Nachmanson 2024-11-05 11:54:23 -0800
  • 02a509b6e8 remove a global debug variable Lev Nachmanson 2024-11-05 10:56:13 -0800
  • acc2149270 remove redundant m_row_index from entry Lev Nachmanson 2024-11-05 10:51:52 -0800
  • d4390731f9 take dependencies from open_ml Lev Nachmanson 2024-11-03 18:21:51 -0800
  • 3fcc5a2227 fixes in tigthening Lev Nachmanson 2024-11-03 16:01:12 -0800
  • 9164672d42 check feasibility immediately after tightening a bound Lev Nachmanson 2024-11-02 14:59:55 -0700
  • 58e57352c2 implement explain() Lev Nachmanson 2024-11-01 18:48:23 -0700
  • b30272feed add missing explanations Lev Nachmanson 2024-11-01 17:03:41 -0700
  • e0a08f16d3 fix the build Lev Nachmanson 2024-11-01 12:52:16 -0700
  • 30f5599064 use fixed vars to explain tightening Lev Nachmanson 2024-11-01 12:46:25 -0700
  • 36293ac773 test that pivoting is correct in dioph_eq.cpp Lev Nachmanson 2024-10-30 15:09:55 -0700
  • 0db0efce9f print output file name Lev Nachmanson 2024-10-23 07:26:52 -0700
  • 8904a50103 fix the build Lev Nachmanson 2024-10-21 14:21:02 -0700
  • 5f5f1d4fd1 init m_e_matrix on terms instead of the tableau Lev Nachmanson 2024-10-21 14:11:07 -0700
  • 392c24a145 throttle dioph equalities Lev Nachmanson 2024-10-15 18:55:38 -0700
  • 128d5b4fa0 change type of m_e_matrix Lev Nachmanson 2024-10-15 08:19:48 -0700
  • a63e0d801e add a template instantiotion Lev Nachmanson 2024-10-15 08:04:58 -0700
  • 0f03e7560d handle empty rows in m_e_matrix Lev Nachmanson 2024-10-15 08:01:20 -0700
  • ba7268c895 vector access bugs Lev Nachmanson 2024-10-14 11:19:47 -0700
  • 66f88206f5 bug fixes with tableau Lev Nachmanson 2024-10-13 20:44:15 -0700
  • 62ea6fbe98 bug fixes Lev Nachmanson 2024-10-11 21:16:38 -0700
  • ac491989b8 bug fixes Lev Nachmanson 2024-10-11 15:31:08 -0700
  • 536c51f600 debug dio with static matrix Lev Nachmanson 2024-10-11 10:29:03 -0700
  • 28fbc810e6 unifying vectors into eprime_entry Lev Nachmanson 2024-10-10 21:29:28 -0700
  • 42bdc893a9 dio with static_matrix initial setup Lev Nachmanson 2024-10-10 19:23:37 -0700
  • 9e8b17b5f8 do not use conflicts with fresh vars to create branches Lev Nachmanson 2024-10-08 16:08:22 -0700
  • eaf2f7f165 remove disabling return Lev Nachmanson 2024-10-08 09:33:23 -0700
  • 8aeba62802 remove more warnings Lev Nachmanson 2024-10-07 14:02:13 -0700
  • 552a504f72 remove a warning Lev Nachmanson 2024-10-07 13:55:18 -0700
  • 4bd815852d fix ubuntu's build Lev Nachmanson 2024-10-07 13:54:03 -0700
  • ea50208ad6 prepare using fresh vars in cuts Lev Nachmanson 2024-10-07 13:40:29 -0700
  • 06faf03eaa use cuts from proofs, remove gcc warnings Lev Nachmanson 2024-10-02 16:07:49 -0700
  • 2ebb957cc8 enable cuts from proofs Lev Nachmanson 2024-10-02 15:40:08 -0700
  • 44fd0e48a8 fixes in dio Lev Nachmanson 2024-10-01 10:34:17 -0700
  • a8e667c643 do not eliminate fresh variables when tightening Lev Nachmanson 2024-09-29 11:51:41 -0700
  • 52b0b8d5d5 fixed dio Lev Nachmanson 2024-09-28 07:34:56 -0700
  • 5ac428fcc9 comment out global_max_change Lev Nachmanson 2024-09-27 10:12:28 -0700
  • 89e4f59df2 debug dio Lev Nachmanson 2024-09-26 13:59:00 -0700
  • 798f0e2e8a test tightening with S Lev Nachmanson 2024-09-26 09:24:12 -0700
  • 193116bf84 handle sat with tightening Lev Nachmanson 2024-09-23 15:59:36 -0700
  • b1be8c0957 cosmetics Lev Nachmanson 2024-09-23 10:32:50 -0700
  • 5db46c1d81 use u_dependency in eprime_pair Lev Nachmanson 2024-09-04 10:57:41 -0700
  • 1408fe60ab work on tighten_with_S Lev Nachmanson 2024-09-04 09:20:21 -0700
  • f0b5cd1066 remove a throw Lev Nachmanson 2024-08-30 20:51:14 -0700
  • be8f3e9c3e bug fix Lev Nachmanson 2024-08-30 20:28:03 -0700
  • 0b1e923d2a small optimization Lev Nachmanson 2024-08-30 19:57:22 -0700
  • 66c6bad01c optimize dio changes Lev Nachmanson 2024-08-29 08:46:05 -1000
  • 18c75e6333 less eager dio Lev Nachmanson 2024-08-28 15:18:38 -1000
  • bbeecc6f7c fix the build Lev Nachmanson 2024-08-27 09:53:46 -1000
  • 3d5ee82bd1 handle zero rows correctly Lev Nachmanson 2024-08-27 08:59:33 -1000
  • 78a58b06aa dio passes regression\smt2 tests with limited functionality Lev Nachmanson 2024-08-27 08:44:46 -1000
  • 245d448c66 fix term_o init Lev Nachmanson 2024-08-26 13:34:28 -1000
  • a796d48264 debug dio Lev Nachmanson 2024-08-26 10:18:56 -1000
  • df18885f97 debug dio Lev Nachmanson 2024-08-24 13:03:25 -1000
  • cd13890650 fix in substitution of fresh variables, clean column.h Lev Nachmanson 2024-08-23 07:06:58 -1000
  • f5e646cbcb bug fix in init and getting explanations Lev Nachmanson 2024-08-22 12:44:42 -1000
  • 59e2dab69a create a conflict explanation Lev Nachmanson 2024-08-22 08:40:41 -1000
  • 52653e6e43 a version with less pointers: got a conflict Lev Nachmanson 2024-08-21 17:40:32 -1000
  • 5a36e02c58 in the middle Lev Nachmanson 2024-08-20 16:01:07 -1000
  • 122e0135d2 use std::list Lev Nachmanson 2024-08-20 07:54:12 -1000
  • 3b22d3b19d fix the crash Lev Nachmanson 2024-08-15 18:18:22 -1000
  • abf29b57aa crash Lev Nachmanson 2024-08-15 17:14:03 -1000
  • a5dd59fdfb fix the build Lev Nachmanson 2024-08-14 15:36:39 -1000
  • a1a01b9da6 move some functionality from int_solver to int_solver::imp Lev Nachmanson 2024-08-14 15:18:28 -1000
  • 889292472e fix the build Lev Nachmanson 2024-08-13 13:48:20 -1000