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

Commit graph

  • bd3d288a08 tighten only core constrants Lev Nachmanson 2025-02-20 08:40:16 -0800
  • 3a5745aee8 rename hgvk94 2025-02-20 04:08:15 -0500
  • 45ad61438a added logging Nikolaj Bjorner 2025-02-19 17:40:59 -0800
  • 13445858f3 fix hgvk94 2025-02-19 19:41:42 -0500
  • 1fec0fa35b remove verbose output Nikolaj Bjorner 2025-02-19 15:35:51 -0800
  • 01fbc0e8e7 fix Nikolaj Bjorner 2025-02-19 14:55:27 -0800
  • 712231dcda fix Nikolaj Bjorner 2025-02-19 09:39:17 -0800
  • 075773e519 remove proviso for single index arrays Nikolaj Bjorner 2025-02-19 00:02:38 -0800
  • 3e5abef145 fix Nikolaj Bjorner 2025-02-18 21:38:06 -0800
  • e0945f57bb fix Nikolaj Bjorner 2025-02-18 21:04:34 -0800
  • 28f3f8046e Nikolaj Bjorner 2025-02-18 20:50:06 -0800
  • 11066486d7 Nikolaj Bjorner 2025-02-18 20:48:13 -0800
  • 991cffb519 handle multi-arity arrays Nikolaj Bjorner 2025-02-18 20:38:45 -0800
  • 674e1b8f98 remove equality check on container Nikolaj Bjorner 2025-02-18 20:15:42 -0800
  • ce69b54b5f adjust select/store rule for n-ary arrays Nikolaj Bjorner 2025-02-18 20:08:56 -0800
  • 42f6e1300a more review of mbp_arrays Nikolaj Bjorner 2025-02-18 19:48:54 -0800
  • a4a84ed083 arrays are not necessarily unary Nikolaj Bjorner 2025-02-18 19:13:12 -0800
  • a5e5a35755 code simplification Nikolaj Bjorner 2025-02-18 19:07:58 -0800
  • a143ed3bff taking a look at mbp_qel for arrays Nikolaj Bjorner 2025-02-18 16:28:49 -0800
  • dda60737dc updated release notes Nikolaj Bjorner 2025-02-18 15:03:24 -0800
  • fb6ec7d5e7 increase version number Nikolaj Bjorner 2025-02-18 15:00:26 -0800
  • 30dba9bde7 use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil Nikolaj Bjorner 2025-02-18 14:36:16 -0800
  • 3c47fd96cf bump timeout for jobs z3-4.14.0 Nikolaj Bjorner 2025-02-18 13:41:31 -0800
  • 2e008a9745 Update release.yml for Azure Pipelines Nikolaj Bjorner 2025-02-18 13:39:41 -0800
  • d1575af5d2 Update nightly.yaml for Azure Pipelines Nikolaj Bjorner 2025-02-17 21:45:10 -0800
  • 96e323384f Update azure-pipelines.yml for Azure Pipelines Nikolaj Bjorner 2025-02-17 21:42:15 -0800
  • 813da35539 fix unit test Nikolaj Bjorner 2025-02-17 20:36:38 -0800
  • f8f26788ad convert def into expression tree Nikolaj Bjorner 2025-02-17 18:47:00 -0800
  • f977b48161 adjust solve_for to handle rationals Nikolaj Bjorner 2025-02-17 13:59:23 -0800
  • 528efbb535 fixes to failure conditions for unification Nikolaj Bjorner 2025-02-16 13:41:17 -0800
  • fe27ca1dd0 remove verbose output Nikolaj Bjorner 2025-02-16 13:23:56 -0800
  • 50f9fddfd2 Add unification based projection function Nikolaj Bjorner 2025-02-16 13:18:21 -0800
  • b27a2aa7fc remove calls to removed def constructor Nikolaj Bjorner 2025-02-16 10:13:00 -0800
  • d7ffd67e68
    Build fix for eee96ec: create mbp::def w/ brace initialization Jevin Sweval 2025-02-16 13:06:36 -0500
  • a703cf81b1 replace model_ref by model* in tg_project, Nikolaj Bjorner 2025-02-15 19:34:52 -0800
  • eee96ec312 bug fixes and cleanup in projection functions Nikolaj Bjorner 2025-02-15 14:11:20 -0800
  • 0cf2b5f515 add retry, rename to optibot Nikolaj Bjorner 2025-02-14 08:39:21 -0800
  • 6b9ce8638f fixes to opt-tool Nikolaj Bjorner 2025-02-13 22:24:02 -0800
  • 719ea6a2a7 added ai scripts Nikolaj Bjorner 2025-02-13 21:11:58 -0800
  • 9fad15e2ca adding mergeopt Nikolaj Bjorner 2025-02-13 15:00:05 -0800
  • 01ba749a5d focused query to optimize Nikolaj Bjorner 2025-02-13 10:01:34 -0800
  • a003139704 update description Nikolaj Bjorner 2025-02-13 09:59:17 -0800
  • 45f3ea3bf4 add treesitter functionality Nikolaj Bjorner 2025-02-13 09:56:49 -0800
  • bedc95c4c7 use static_cast to avoid the warnings Lev Nachmanson 2025-02-13 07:07:12 -1000
  • e6a089e63d
    Fix build when Z3_API macro is non-empty () Phil Clayton 2025-02-13 16:46:08 +0000
  • 86f5507694 Fix build when Z3_API macro is non-empty Phil Clayton 2025-02-13 09:52:36 +0000
  • d10efa667a stub for treesitter Nikolaj Bjorner 2025-02-12 19:56:33 -0800
  • 5c18ce8cea genai testing Nikolaj Bjorner 2025-02-12 19:55:39 -0800
  • 4e51af1167 update instructions Nikolaj Bjorner 2025-02-11 22:05:19 -0800
  • 94d3c591b5 make sure ackermann works with arrays that have more than one argument Nikolaj Bjorner 2025-02-11 21:28:31 -0800
  • a3739aa934 add mycop in addition to code complete Nikolaj Bjorner 2025-02-11 20:04:52 -0800
  • 9ea921ba8e update spacer projection for arrays to allow ackerman reduction for non-integer arrays Nikolaj Bjorner 2025-02-11 17:38:56 -0800
  • 1a77622714 add prompt to ask for patch, assume directory alignment conflict-throttle Nikolaj Bjorner 2025-02-11 16:01:30 -0800
  • e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts Lev Nachmanson 2025-02-11 10:45:36 -1000
  • 957b177c64 set arith.lp.dio_cuts_enable_gomory to False by default Lev Nachmanson 2025-02-10 11:26:46 -1000
  • 5ec10e0250 address the review Lev Nachmanson 2025-02-10 10:00:20 -1000
  • 8a9edd1aa7 fix the test build Lev Nachmanson 2025-02-10 07:36:07 -1000
  • 79e3f8ab39 disabling dio handler by default, and fix a print out Lev Nachmanson 2025-02-10 06:49:26 -1000
  • 2131e9b4e4 more accurate work with Markovich number Lev Nachmanson 2025-02-09 07:53:55 -0800
  • bdb8f54150 Revert "revert the term sorting" Lev Nachmanson 2025-02-08 20:05:09 -1000
  • 5ebee24850 revert the term sorting Lev Nachmanson 2025-02-08 14:25:10 -1000
  • f2c1fd4c14 try markovich number Lev Nachmanson 2025-02-07 22:39:52 -0800
  • cec8dc2e6e try markovich number Lev Nachmanson 2025-02-07 22:27:25 -0800
  • 3f2d2e8348 test Lev Nachmanson 2025-02-07 15:15:25 -1000
  • b6701d57f9 try another sort in tightening Lev Nachmanson 2025-02-07 14:54:26 -1000
  • 5b0b224a5c try sorting terms before tightening Lev Nachmanson 2025-02-07 12:56:20 -1000
  • dcd5783232 remove the fresh definition when removing its column Lev Nachmanson 2025-02-06 16:50:24 -1000
  • 17d68c18aa comment change Lev Nachmanson 2025-02-06 13:41:14 -1000
  • d90b94d0e2 stricter is_in_sync paying attenion to m_row2fresh_defs Lev Nachmanson 2025-02-06 13:16:42 -1000
  • 134bed826a throttle the branching in dio Lev Nachmanson 2025-02-06 14:28:11 -0800
  • bd8cf29df7 ignore large changed_columns Lev Nachmanson 2025-02-06 05:45:50 -1000
  • 3ac11cd136 fix assert Lev Nachmanson 2025-02-05 18:24:00 -1000
  • cf4e402a0f avoid usisg indexed_vector for term operations Lev Nachmanson 2025-02-05 17:54:58 -1000
  • 440d78f237 disallow duplicates in a queue Lev Nachmanson 2025-02-05 15:41:24 -0800
  • 7e02dfe484 add stats on m_dio_branching_conflicts Lev Nachmanson 2025-02-05 10:38:51 -1000
  • 0bf3ca87e7 call normalize_e_by_gcd() only when moving an entry from F to S Lev Nachmanson 2025-02-04 12:38:16 -1000
  • 99538567a7 rebase with master Lev Nachmanson 2025-02-03 19:21:24 -1000
  • a19e10912f make dio less aggressive, allow other cuts Lev Nachmanson 2025-02-03 13:12:58 -1000
  • fee707842d register m_added_terms in m_changed_terms Lev Nachmanson 2025-02-03 07:50:37 -1000
  • 21f67ef942 out of bounds fixes Lev Nachmanson 2025-02-03 07:12:42 -1000
  • 3b3d8cee03 use m_chandedNterms to tighten terms Lev Nachmanson 2025-02-03 07:02:54 -1000
  • 65bdd58d3e remove struct entry Lev Nachmanson 2025-02-03 06:30:20 -1000
  • a9098a5785 optimise l terms addition Lev Nachmanson 2025-02-01 12:44:45 -1000
  • 3e7e903d19 use the trail to undo add_term Lev Nachmanson 2025-01-29 16:56:41 -1000
  • 9c510018b3 fix the debug build Lev Nachmanson 2025-01-29 17:32:37 -0800
  • 058b9e4a6d optimise rewrite_eqs to avoid fresh variables Lev Nachmanson 2025-01-29 15:37:00 -0800
  • ed3df333b3 make rewrite_eq boolean, and relax an ASSERT Lev Nachmanson 2025-01-29 14:18:52 -0800
  • ca7c128d3f clean up fresh definitions on a pop Lev Nachmanson 2025-01-29 09:19:23 -0800
  • b027761845 debug dio Lev Nachmanson 2025-01-27 15:43:04 -0800
  • bb869fd020 don't store fresh definitions in m_e_matrix Lev Nachmanson 2025-01-25 23:04:13 -0800
  • e5ffc3cfae cleanup Lev Nachmanson 2025-01-25 13:50:08 -0800
  • d7de7eb732 remove recalculated entries from S Lev Nachmanson 2025-01-24 08:45:33 -0800
  • ef55de1646 fix out of bounds bug Lev Nachmanson 2025-01-23 16:12:12 -1000
  • 3990df6d91 substitute variables with a queue on the recalculated entries Lev Nachmanson 2025-01-23 15:55:04 -1000
  • 78d91f3794 simplify dio handler by using bijection m_k2s Lev Nachmanson 2025-01-23 06:51:50 -1000
  • 33f5e303f8 use entry_status for FRESH entries Lev Nachmanson 2025-01-20 18:01:37 -1000
  • 0e71adfa35 fix some warnings Lev Nachmanson 2025-01-20 14:58:24 -0800
  • 7bba8bc0c9 fix some warnings Lev Nachmanson 2025-01-20 12:44:05 -1000
  • 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