3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00

Commit graph

  • cdb18ac685 document dioph_eq Lev Nachmanson 2024-11-05 11:54:23 -0800
  • eb0aeab2a3 remove a global debug variable Lev Nachmanson 2024-11-05 10:56:13 -0800
  • b99439599b remove redundant m_row_index from entry Lev Nachmanson 2024-11-05 10:51:52 -0800
  • 12ceb1ef26 take dependencies from open_ml Lev Nachmanson 2024-11-03 18:21:51 -0800
  • 2a81a1f043 fixes in tigthening Lev Nachmanson 2024-11-03 16:01:12 -0800
  • bb77ff537b check feasibility immediately after tightening a bound Lev Nachmanson 2024-11-02 14:59:55 -0700
  • 0077a689bd implement explain() Lev Nachmanson 2024-11-01 18:48:23 -0700
  • 1eecedf8cb add missing explanations Lev Nachmanson 2024-11-01 17:03:41 -0700
  • 143f22e0a5 fix the build Lev Nachmanson 2024-11-01 12:52:16 -0700
  • 472306c0b2 use fixed vars to explain tightening Lev Nachmanson 2024-11-01 12:46:25 -0700
  • 24aeaed50a test that pivoting is correct in dioph_eq.cpp Lev Nachmanson 2024-10-30 15:09:55 -0700
  • 09ec973998 print output file name Lev Nachmanson 2024-10-23 07:26:52 -0700
  • 594fa7423f fix the build Lev Nachmanson 2024-10-21 14:21:02 -0700
  • a3b81b54db init m_e_matrix on terms instead of the tableau Lev Nachmanson 2024-10-21 14:11:07 -0700
  • 2bda4d1674 throttle dioph equalities Lev Nachmanson 2024-10-15 18:55:38 -0700
  • 727ac149a7 change type of m_e_matrix Lev Nachmanson 2024-10-15 08:19:48 -0700
  • 282edcfadf add a template instantiotion Lev Nachmanson 2024-10-15 08:04:58 -0700
  • 4710260ede handle empty rows in m_e_matrix Lev Nachmanson 2024-10-15 08:01:20 -0700
  • b0be4d58c7 vector access bugs Lev Nachmanson 2024-10-14 11:19:47 -0700
  • f5f4c848ec bug fixes with tableau Lev Nachmanson 2024-10-13 20:44:15 -0700
  • 9c2ec9b47d bug fixes Lev Nachmanson 2024-10-11 21:16:38 -0700
  • 9434847ce7 bug fixes Lev Nachmanson 2024-10-11 15:31:08 -0700
  • bc2c67c7ea debug dio with static matrix Lev Nachmanson 2024-10-11 10:29:03 -0700
  • df577eecd6 unifying vectors into eprime_entry Lev Nachmanson 2024-10-10 21:29:28 -0700
  • f3b33888ab dio with static_matrix initial setup Lev Nachmanson 2024-10-10 19:23:37 -0700
  • 60a38cdd22 do not use conflicts with fresh vars to create branches Lev Nachmanson 2024-10-08 16:08:22 -0700
  • dc15dbfc31 remove disabling return Lev Nachmanson 2024-10-08 09:33:23 -0700
  • 5f0077626e remove more warnings Lev Nachmanson 2024-10-07 14:02:13 -0700
  • fdae46fb60 remove a warning Lev Nachmanson 2024-10-07 13:55:18 -0700
  • 2c7c708848 fix ubuntu's build Lev Nachmanson 2024-10-07 13:54:03 -0700
  • fa907c5e8c prepare using fresh vars in cuts Lev Nachmanson 2024-10-07 13:40:29 -0700
  • 110593f086 use cuts from proofs, remove gcc warnings Lev Nachmanson 2024-10-02 16:07:49 -0700
  • 4e381609db enable cuts from proofs Lev Nachmanson 2024-10-02 15:40:08 -0700
  • c30600c2ef fixes in dio Lev Nachmanson 2024-10-01 10:34:17 -0700
  • 5f70eb0524 do not eliminate fresh variables when tightening Lev Nachmanson 2024-09-29 11:51:41 -0700
  • 1769c6059e fixed dio Lev Nachmanson 2024-09-28 07:34:56 -0700
  • 2ca7b31d13 comment out global_max_change Lev Nachmanson 2024-09-27 10:12:28 -0700
  • f05d1abccc debug dio Lev Nachmanson 2024-09-26 13:59:00 -0700
  • 8d8ee99db3 test tightening with S Lev Nachmanson 2024-09-26 09:24:12 -0700
  • 7d8212646d handle sat with tightening Lev Nachmanson 2024-09-23 15:59:36 -0700
  • 9118abebc7 cosmetics Lev Nachmanson 2024-09-23 10:32:50 -0700
  • e0185121c5 use u_dependency in eprime_pair Lev Nachmanson 2024-09-04 10:57:41 -0700
  • b20566a488 work on tighten_with_S Lev Nachmanson 2024-09-04 09:20:21 -0700
  • a1a9825e43 remove a throw Lev Nachmanson 2024-08-30 20:51:14 -0700
  • a75eff6525 bug fix Lev Nachmanson 2024-08-30 20:28:03 -0700
  • 0c6dcfedb8 small optimization Lev Nachmanson 2024-08-30 19:57:22 -0700
  • 9ec55de5c6 optimize dio changes Lev Nachmanson 2024-08-29 08:46:05 -1000
  • 7c9cb44c94 less eager dio Lev Nachmanson 2024-08-28 15:18:38 -1000
  • 4fea4259ec fix the build Lev Nachmanson 2024-08-27 09:53:46 -1000
  • 1a99fa56cb handle zero rows correctly Lev Nachmanson 2024-08-27 08:59:33 -1000
  • 178411ad0c dio passes regression\smt2 tests with limited functionality Lev Nachmanson 2024-08-27 08:44:46 -1000
  • dcd80ac95b fix term_o init Lev Nachmanson 2024-08-26 13:34:28 -1000
  • c29d04dc3c debug dio Lev Nachmanson 2024-08-26 10:18:56 -1000
  • 1cb71b4648 debug dio Lev Nachmanson 2024-08-24 13:03:25 -1000
  • db899fd670 fix in substitution of fresh variables, clean column.h Lev Nachmanson 2024-08-23 07:06:58 -1000
  • 5f71604198 bug fix in init and getting explanations Lev Nachmanson 2024-08-22 12:44:42 -1000
  • 0814fa40b0 create a conflict explanation Lev Nachmanson 2024-08-22 08:40:41 -1000
  • 53605d4e0a a version with less pointers: got a conflict Lev Nachmanson 2024-08-21 17:40:32 -1000
  • 876cbc527d in the middle Lev Nachmanson 2024-08-20 16:01:07 -1000
  • 778db5e763 use std::list Lev Nachmanson 2024-08-20 07:54:12 -1000
  • c1e577e932 fix the crash Lev Nachmanson 2024-08-15 18:18:22 -1000
  • 484af98af6 crash Lev Nachmanson 2024-08-15 17:14:03 -1000
  • 0eeef3b806 fix the build Lev Nachmanson 2024-08-14 15:36:39 -1000
  • 0b9b1c4472 move some functionality from int_solver to int_solver::imp Lev Nachmanson 2024-08-14 15:18:28 -1000
  • 66b778cb25 fix the build Lev Nachmanson 2024-08-13 13:48:20 -1000
  • 7050589adf prepare for calling diophantine equations Lev Nachmanson 2024-08-13 13:20:45 -1000
  • 049520483f add parameter to control calling diophantine equations Lev Nachmanson 2024-08-13 12:25:34 -1000
  • 3456af425e with theory propagation Nikolaj Bjorner 2025-02-03 14:08:02 -0800
  • 7808be0935 with theory lemma relevant Nikolaj Bjorner 2025-02-03 13:44:05 -0800
  • ef7893cdca use learned vs relevant distinction for theory lemmas Nikolaj Bjorner 2025-02-03 13:40:06 -0800
  • a513488c54 add conflict throttle, experiment with pb2bv Nikolaj Bjorner 2025-02-03 03:14:20 -0800
  • 17d47ca8c7 fix #7493 Nikolaj Bjorner 2025-02-02 15:00:31 -0800
  • 99cbfa715c Add a sharp throttle to lia2card tactic to control overhead in default tactic mode Nikolaj Bjorner 2025-02-02 13:58:51 -0800
  • fd2a8a554d disable small clause generation for propagation Nikolaj Bjorner 2025-02-01 20:04:29 -0800
  • 0ef26983fc release Nikolaj Bjorner 2025-01-31 17:31:37 -0800
  • aea4490fb2 throttle overhead with lia2card Nikolaj Bjorner 2025-01-31 12:36:59 -0800
  • d465bdbb87 include extensionality constraints for arrays Nikolaj Bjorner 2025-01-31 11:06:40 -0800
  • d6dcc515eb rehearse release Nikolaj Bjorner 2025-01-31 09:49:42 -0800
  • edc5679530 updated release notes Nikolaj Bjorner 2025-01-31 09:49:16 -0800
  • 8ae24e2b38 update release version Nikolaj Bjorner 2025-01-31 09:28:51 -0800
  • 1d622a678e
    Bump docker/build-push-action from 6.12.0 to 6.13.0 (#7535) dependabot[bot] 2025-01-31 09:26:49 -0800
  • 9557e7cacf
    Minor (#7540) Clemens Eisenhofer 2025-01-31 17:22:30 +0100
  • 1408a4589a Guard update list from identity CEisenhofer 2025-01-31 15:17:11 +0100
  • 1ce6e66ac9 generalize logic detection to use sub-string matching Nikolaj Bjorner 2025-01-30 16:34:54 -0800
  • eb825855fa increase the log level on callbacks with bit-indices that get set Nikolaj Bjorner 2025-01-30 16:34:36 -0800
  • c9ac4d6f75 pre-flatten use list before iterating over m_unsat Nikolaj Bjorner 2025-01-30 16:34:17 -0800
  • a3a3921234 Minor CEisenhofer 2025-01-30 23:25:19 +0100
  • e3566288a4 fixes based on benchmarking UFDTLIA/NIA/BV Nikolaj Bjorner 2025-01-29 17:00:26 -0800
  • f1e0950069 fix several crashes exposed by QF_UFDTNIA benchmark sets Nikolaj Bjorner 2025-01-29 16:23:38 -0800
  • bfe4673dac this check is not an invariant in the first place Nikolaj Bjorner 2025-01-29 16:23:18 -0800
  • 51357f6d06 Add selective filter on Ackerman axioms Nikolaj Bjorner 2025-01-29 11:42:39 -0800
  • c2a0919f79
    Removed no progress case in seq-sls (#7537) Clemens Eisenhofer 2025-01-29 18:43:57 +0100
  • 6d3cfb63da add eval1 functionality for replace_all Nikolaj Bjorner 2025-01-29 04:36:55 -0800
  • ab43d2dcf1 fix semantics of check-int64 div operation to align with smtlib semantics Nikolaj Bjorner 2025-01-29 04:29:38 -0800
  • 30d72f79ac remove verbose output of overflow Nikolaj Bjorner 2025-01-29 03:48:11 -0800
  • 3379155a63 add check for root literal assignment Nikolaj Bjorner 2025-01-29 03:14:14 -0800
  • fe5d17d515 handle exception internally, avoid passing rationals to integer operations Nikolaj Bjorner 2025-01-28 20:09:59 -0800
  • 5b175c1bcd fix crashes in sls_datatype Nikolaj Bjorner 2025-01-28 19:24:32 -0800
  • fe713eb8e9 disable quadratic moves for non-integers as sqrt isn't currently defined for rationals Nikolaj Bjorner 2025-01-28 16:53:12 -0800
  • d8430810fe fix mixup between sync and sls managed variables Nikolaj Bjorner 2025-01-28 16:35:50 -0800