3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00

Commit graph

  • 7ff64fdd2f
    Merge 8e8799dbd3 into efd5d04af5 Don Syme 2025-10-28 13:21:19 +01:00
  • e13e85c4ab swap signs of coefficients compared to sign of variables. They are on different sides of inequality arie Nikolaj Bjorner 2025-10-28 03:16:12 -07:00
  • ae9a09ba26
    Merge 4b18085154 into efd5d04af5 dependabot[bot] 2025-10-27 22:31:21 +00:00
  • 4b18085154
    Bump actions/download-artifact from 5 to 6 dependabot/github_actions/actions/download-artifact-6 dependabot[bot] 2025-10-27 22:31:18 +00:00
  • 84284b7cd3
    Merge dfe0b21af3 into efd5d04af5 dependabot[bot] 2025-10-27 22:25:46 +00:00
  • dfe0b21af3
    Bump actions/upload-artifact from 4 to 5 dependabot/github_actions/actions/upload-artifact-5 dependabot[bot] 2025-10-27 22:25:42 +00:00
  • b8cadfac56 don't add boolean disequality . finite-sets Nikolaj Bjorner 2025-10-27 14:08:12 -07:00
  • a82af886eb formatting Nikolaj Bjorner 2025-10-27 14:01:30 -07:00
  • 580e796358
    Merge 7c51accb30 into efd5d04af5 Don Syme 2025-10-27 13:10:27 -07:00
  • 2f06bcc731 add finite_set to quantifieed theories in smt_setup, fix type signature for map-inverse axioms Nikolaj Bjorner 2025-10-27 20:34:13 +01:00
  • c0ca3b5a0a streamline axioms Nikolaj Bjorner 2025-10-27 18:58:45 +01:00
  • 4464ab9431 fix empty set declaration, add axioms and rewrites Nikolaj Bjorner 2025-10-27 18:18:46 +01:00
  • 4630373a97 add finite sets to datatype recursion, delay initialize finite_set plugin, fix bugs in are_distinct and equality simplification Nikolaj Bjorner 2025-10-27 10:37:19 +01:00
  • d847a28589 bug fixes Nikolaj Bjorner 2025-10-27 05:51:42 +01:00
  • f8a1f98fce try Lazard project upoly Lev Nachmanson 2025-10-26 12:15:50 -07:00
  • c832802183 disable tracking literals, they are not used Nikolaj Bjorner 2025-10-26 16:21:33 +01:00
  • a66cb88c78 fix build Nikolaj Bjorner 2025-10-18 13:30:46 +02:00
  • e980f92a9e enable always add all coeffs in nlsat Lev Nachmanson 2025-10-24 17:47:16 -07:00
  • 7b095ca733 throttle grobner method more actively Lev Nachmanson 2025-10-22 21:36:22 -07:00
  • a15b21bc62 try exponential delay in grobner Lev Nachmanson 2025-10-22 17:00:16 -07:00
  • ba03d35957 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) hwisungi 2025-10-22 05:18:25 -07:00
  • 06d142119f Bump actions/setup-node from 5 to 6 (#7994) dependabot[bot] 2025-10-21 21:17:35 +02:00
  • afaf0e3dd7 Add a fast-path to _coerce_exprs. (#7995) Nelson Elhage 2025-10-21 12:16:54 -07:00
  • 0d285a9b41 add the "noexcept" keyword to value_score=(value_score&&) declaration Lev Nachmanson 2025-10-20 11:53:34 -07:00
  • 0ae54c34fd disable manylinux until segfault is resolved Nikolaj Bjorner 2025-10-20 08:28:08 +02:00
  • 1477ce2a99 build fixes Nikolaj Bjorner 2025-10-19 20:55:45 +02:00
  • 39913667c6 add explicit constructors for nightly mac build failure Nikolaj Bjorner 2025-10-19 20:14:20 +02:00
  • 90d36ed915 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) Nikolaj Bjorner 2025-10-16 13:18:35 +02:00
  • 85e1a39c09 Add finite_set_value_factory for creating finite set values in model generation (#7981) Copilot 2025-10-16 13:16:54 +02:00
  • 351c0401fb restore the method behavior Lev Nachmanson 2025-10-15 16:41:32 -07:00
  • d9ca739499 restore single cell Lev Nachmanson 2025-10-14 17:43:48 -07:00
  • f324c5286c trim parametric datatype test Nikolaj Bjorner 2025-10-15 21:39:39 +02:00
  • 0d85b86334 Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) Copilot 2025-10-15 20:51:21 +02:00
  • 64295b5876 Bump github/codeql-action from 3 to 4 (#7971) dependabot[bot] 2025-10-14 18:08:27 +02:00
  • 23ce6917c5 parameter eval order Lev Nachmanson 2025-10-07 10:30:58 -07:00
  • 6bca12d399 parameter eval order Lev Nachmanson 2025-10-07 10:26:40 -07:00
  • e75da050d2 parameter eval order Lev Nachmanson 2025-10-07 10:21:09 -07:00
  • 4f93fc7b2a parameter eval order Lev Nachmanson 2025-10-07 10:19:24 -07:00
  • 5a3d33a615 parameter eval order Lev Nachmanson 2025-10-07 10:14:02 -07:00
  • 6146fe9ff8 parameter eval order Lev Nachmanson 2025-10-07 10:06:43 -07:00
  • 0a2328af1d parameter eval order Lev Nachmanson 2025-10-07 09:17:12 -07:00
  • 0fbf4010a5 param eval order Lev Nachmanson 2025-10-07 09:13:21 -07:00
  • b22f4d8802 param eval Lev Nachmanson 2025-10-07 09:04:24 -07:00
  • e113d39aa8 parameter evaluation order Lev Nachmanson 2025-10-07 08:53:49 -07:00
  • 28c625a170 parameter eval order Lev Nachmanson 2025-10-07 08:40:24 -07:00
  • 1aaf2f8448 param order evaluation Lev Nachmanson 2025-10-07 08:34:56 -07:00
  • 97bb035416 param order Lev Nachmanson 2025-10-06 15:51:53 -07:00
  • 74c28532f4 param order Lev Nachmanson 2025-10-06 15:44:41 -07:00
  • f8b2268424 base implementation for cardinality constraints Nikolaj Bjorner 2025-10-26 10:35:37 +01:00
  • c72da53d19 align the univariate helper manager with the main polynomial manager Lev Nachmanson 2025-10-25 12:02:54 -07:00
  • 53e4d9562a implement a todo item to calc gcd on uni-polynomials Lev Nachmanson 2025-10-25 11:25:22 -07:00
  • 2eb75d8a71
    Merge 7652d5a3e4 into efd5d04af5 Don Syme 2025-10-25 17:58:36 +02:00
  • efd5d04af5 enable always add all coeffs in nlsat master Lev Nachmanson 2025-10-24 17:47:16 -07:00
  • 4068460a0f fix bogus axioms Nikolaj Bjorner 2025-10-24 13:35:41 +02:00
  • 5079b10597 fix up documentation Nikolaj Bjorner 2025-10-24 13:13:52 +02:00
  • bfe6670b73
    Fix finite_set sort cardinality computation for finite base sorts (#7997) Copilot 2025-10-23 17:30:17 +02:00
  • 69e0793f6c add overloads for finite sets Nikolaj Bjorner 2025-10-23 17:29:11 +02:00
  • 541a554ecd
    Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) Copilot 2025-10-23 17:10:47 +02:00
  • 4c67a7271e extend proof logging Nikolaj Bjorner 2025-10-23 09:48:43 +02:00
  • b96624727d remove ad-hoc membership axioms, enable boundary point saturatino Nikolaj Bjorner 2025-10-23 09:42:25 +02:00
  • 887ecc0c98 throttle grobner method more actively Lev Nachmanson 2025-10-22 21:36:22 -07:00
  • 58e64ea826 try exponential delay in grobner Lev Nachmanson 2025-10-22 17:00:16 -07:00
  • 0fcb0b6492 Fix unit tests for infinite base sorts copilot/fix-finite-set-decl-plugin copilot-swe-agent[bot] 2025-10-22 12:45:37 +00:00
  • 8b3fd63434
    Update finite_set_decl_plugin.cpp Nikolaj Bjorner 2025-10-22 14:20:42 +02:00
  • 2bf1cc7d61
    Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) hwisungi 2025-10-22 05:18:25 -07:00
  • a4bcd74ba5
    Setting up param tuning python prototyping experiment (#7993) parallel Ilana Shapiro 2025-10-22 04:47:11 -07:00
  • 07f6f84645 Reviewed and updated configuration for Python build and added comment for CFG. Hwi-sung Im 2025-10-21 13:46:35 -07:00
  • 7ab0049612 Add documentation for finite set API copilot/add-finite-set-constructors copilot-swe-agent[bot] 2025-10-21 20:29:12 +00:00
  • 4029161cb4 Add C++ bindings for finite sets copilot-swe-agent[bot] 2025-10-21 20:23:13 +00:00
  • d9c354f809 Add Python bindings for finite sets copilot-swe-agent[bot] 2025-10-21 20:19:29 +00:00
  • 2dd4221451 Fix configuration error for non-MSVC compilers. Hwi-sung Im 2025-10-21 13:19:19 -07:00
  • 064f7e3088 Add C API for finite sets copilot-swe-agent[bot] 2025-10-21 20:11:11 +00:00
  • 488dce0edb Implement cardinality computation for finite_set sorts copilot-swe-agent[bot] 2025-10-21 20:08:51 +00:00
  • 39ec6764b6
    Merge branch 'parallel' into param-tuning Ilana Shapiro 2025-10-21 13:02:52 -07:00
  • 0dc50cf668 Initial plan copilot-swe-agent[bot] 2025-10-21 19:38:46 +00:00
  • 68d18c6125 Initial plan copilot-swe-agent[bot] 2025-10-21 19:38:16 +00:00
  • 61f48ab156
    Merge branch 'Z3Prover:master' into param-tuning Ilana Shapiro 2025-10-21 12:32:00 -07:00
  • 68a7d1e1b1
    Bump actions/setup-node from 5 to 6 (#7994) dependabot[bot] 2025-10-21 21:17:35 +02:00
  • 9a2867aeb7
    Add a fast-path to _coerce_exprs. (#7995) Nelson Elhage 2025-10-21 12:16:54 -07:00
  • f6168cad62 Add a fast-path to _coerce_exprs. Nelson Elhage 2025-10-19 13:26:06 -07:00
  • 43197f52d8 expose a status flag for clauses but every single one is being coded as an assumption... Ilana Shapiro 2025-10-20 20:04:12 -07:00
  • ef1862ad2c
    Bump actions/setup-node from 5 to 6 dependabot[bot] 2025-10-20 22:03:36 +00:00
  • 2e4402c8f3 add interpretations when there are ranges Nikolaj Bjorner 2025-10-20 23:21:30 +02:00
  • 06ed96dbda add the "noexcept" keyword to value_score=(value_score&&) declaration Lev Nachmanson 2025-10-20 11:53:34 -07:00
  • f2e7abbdc1 disable manylinux until segfault is resolved Nikolaj Bjorner 2025-10-20 08:28:08 +02:00
  • f520e6875b
    Merge branch 'Z3Prover:master' into param-tuning Ilana Shapiro 2025-10-19 22:25:13 -07:00
  • 564ececf3f fix logic about checking clauses individually, and add proof prefix clause selection (naively) via the OnClause hook Ilana Shapiro 2025-10-19 22:15:16 -07:00
  • da85ed8cdd fix some bugs, it seems to run now Ilana Shapiro 2025-10-19 19:01:16 -07:00
  • 2480b5a359 change multithread to multiprocess seems to have resolved current deadlock Ilana Shapiro 2025-10-19 15:34:49 -07:00
  • 629408ba87 fix some more things but now it hangs Ilana Shapiro 2025-10-19 15:06:18 -07:00
  • 8371f11dac fixes Ilana Shapiro 2025-10-19 12:33:42 -07:00
  • aaaa32b4a0 build fixes Nikolaj Bjorner 2025-10-19 20:55:45 +02:00
  • d65c0fbcd6 add explicit constructors for nightly mac build failure Nikolaj Bjorner 2025-10-19 20:14:20 +02:00
  • 65f38eac16 fixup proof log annotations of rules Nikolaj Bjorner 2025-10-19 10:04:18 +02:00
  • 86d7790c42 update pythonnn prototyping experiment, need to add a couple more things Ilana Shapiro 2025-10-19 00:01:49 -07:00
  • 0baaa3f9ce relax an assert lws Lev Nachmanson 2025-10-18 14:44:23 -07:00
  • c2661e34fc normalize before pushing Lev Nachmanson 2025-10-18 13:14:22 -07:00
  • b85cba762c create a better queue on properties Lev Nachmanson 2025-10-18 12:50:20 -07:00
  • 6485808b49 adding proof hint output Nikolaj Bjorner 2025-10-18 19:26:19 +02:00
  • eb10ab1633
    Rename set.select to set.filter and OP_FINITE_SET_SELECT to OP_FINITE_SET_FILTER (#7989) Copilot 2025-10-18 17:16:32 +02:00