3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00

Commit graph

  • 2590d672f4 na Nikolaj Bjorner 2024-02-25 20:06:17 -08:00
  • 58474df438 na Nikolaj Bjorner 2024-02-24 14:34:28 -08:00
  • 0e5b504c30 remove bw setting Nikolaj Bjorner 2024-02-24 01:38:18 -08:00
  • a328366c7d move to single path mode for search Nikolaj Bjorner 2024-02-23 19:05:16 -08:00
  • 8f85df05ed fb Nikolaj Bjorner 2024-02-23 04:03:15 -08:00
  • c451e4e50b na Nikolaj Bjorner 2024-02-22 21:33:51 -08:00
  • 63804c5296 na Nikolaj Bjorner 2024-02-22 21:19:06 -08:00
  • 74e73f2b84 reorg to use datatypes Nikolaj Bjorner 2024-02-22 17:45:03 -08:00
  • 48026edd7f move to hide bits Nikolaj Bjorner 2024-02-22 10:35:51 -08:00
  • acc9c21653 move to hide bits Nikolaj Bjorner 2024-02-22 10:33:37 -08:00
  • cfa6bd4534 update python build dependencies Nikolaj Bjorner 2024-02-21 20:33:06 -08:00
  • 5379fabf9d include thread Nikolaj Bjorner 2024-02-21 19:52:32 -08:00
  • b14499f230 prepare for sls experiment Nikolaj Bjorner 2024-02-21 19:29:21 -08:00
  • cf72a916f8 bugfixes, adding plugin solver Nikolaj Bjorner 2024-02-21 14:11:11 -08:00
  • 659e384ee7 bugfixes Nikolaj Bjorner 2024-02-21 02:11:53 -08:00
  • cd6382f1c8 fix alias bug Nikolaj Bjorner 2024-02-20 22:38:07 -08:00
  • 9cde4f7e05 bugfixes Nikolaj Bjorner 2024-02-20 20:42:32 -08:00
  • d7e419b7ed fixes and checks Nikolaj Bjorner 2024-02-20 14:14:12 -08:00
  • ab0459e5aa bugfixes Nikolaj Bjorner 2024-02-20 13:38:04 -08:00
  • 7dc4ce8259 use tuned gcd to compute mult inverse Nikolaj Bjorner 2024-02-20 01:40:27 -08:00
  • 4391c90960 na Nikolaj Bjorner 2024-02-19 15:32:53 +07:00
  • 991537836b fixes based on unit tests Nikolaj Bjorner 2024-02-19 12:59:28 +07:00
  • 046db662f9 na Nikolaj Bjorner 2024-02-19 00:05:37 +07:00
  • 388b2f5eec n/a Nikolaj Bjorner 2024-02-16 14:37:49 +07:00
  • ddf2d28350 add tests for evaluation Nikolaj Bjorner 2024-02-16 09:58:24 +07:00
  • 1cf008dd0a updates Nikolaj Bjorner 2024-02-14 16:59:52 +07:00
  • bd323d6fab save Nikolaj Bjorner 2024-02-13 20:28:18 +07:00
  • f39756c74b initial stab at new bv-sls based on repair actions Nikolaj Bjorner 2024-02-13 16:34:26 +07:00
  • 10687082f1
    Revert "For many linux build, use aarch64 instead of arm64 (#7147)" (#7148) Nikolaj Bjorner 2024-03-05 12:25:31 -08:00
  • 0e51de641e
    Revert "For many linux build, use aarch64 instead of arm64 (#7147)" Nikolaj Bjorner 2024-03-05 12:21:28 -08:00
  • 7694bca5f4
    For many linux build, use aarch64 instead of arm64 (#7147) Steven Moy 2024-03-05 11:27:43 -08:00
  • d8eace8060 For many linux build, use aarch64 instead of arm64 Steven Moy 2024-03-05 11:13:19 -08:00
  • 77a07bb791 detect arm64 for manylinux setup Nikolaj Bjorner 2024-03-04 21:14:19 -08:00
  • 4050a43f2f
    Add arm64 for linux python wheels to nightly (#7145) Steven Moy 2024-03-04 17:28:50 -08:00
  • e4e5ded696 Add arm64 for linux python wheels to nightly Steven Moy 2024-03-04 15:43:01 -08:00
  • 57c20be6eb fix #7143: type punning in test Nuno Lopes 2024-03-04 14:34:02 +00:00
  • 52c46e7979 Merge branch 'poly' of https://github.com/z3prover/z3 into poly Nikolaj Bjorner 2024-03-03 01:55:53 -08:00
  • 91886dafca
    some code cleaning and complexity improvements (#7133) zapashcanon 2024-02-29 17:54:53 +01:00
  • 2880ea3971
    convert formatting tabs to spaces (#7140) John Fleisher 2024-02-26 12:06:28 -05:00
  • c67200ef72 update versions Nikolaj Bjorner 2024-02-26 08:28:18 -08:00
  • 0369695718 Merge branch 'master' of https://github.com/Z3Prover/z3 into jofleish/fixtabs jofleish 2024-02-26 09:47:00 -05:00
  • f00be84bcc convert tabs to spaces for proper formatting in yaml jofleish 2024-02-26 09:45:32 -05:00
  • 4a726208af bad merge? Jakob Rath 2024-02-26 12:02:49 +01:00
  • af017d0906 bad merge? Jakob Rath 2024-02-26 11:56:04 +01:00
  • 183e911a79 Merge remote-tracking branch 'origin/master' into poly Jakob Rath 2024-02-26 11:46:22 +01:00
  • b2166da464 add code for offline validation Jakob Rath 2024-02-26 10:55:07 +01:00
  • 94e2e0c3e6 pass along lemma name Jakob Rath 2024-02-26 10:51:01 +01:00
  • b561795214 fix Jakob Rath 2024-02-26 10:40:37 +01:00
  • fa2c0e0278 enable release publish z3-4.12.6 Nikolaj Bjorner 2024-02-24 14:35:07 -08:00
  • 85425a6e08
    Update nightly.yaml for Azure Pipelines (#7139) John Fleisher 2024-02-24 05:13:35 -05:00
  • af1c7b67b0 Update nightly.yaml for Azure Pipelines Nikolaj Bjorner 2024-02-24 01:32:22 -08:00
  • f0839e289f Update nightly.yaml for Azure Pipelines Nikolaj Bjorner 2024-02-23 19:28:44 -08:00
  • 5a085015e4
    Update nightly.yaml Nikolaj Bjorner 2024-02-23 17:09:59 -08:00
  • d18e9af975
    Update nightly.yaml Nikolaj Bjorner 2024-02-23 15:35:20 -08:00
  • 507e999726 fix indent jofleish 2024-02-23 16:52:00 -05:00
  • b05575125c fix indent jofleish 2024-02-23 16:49:39 -05:00
  • 1ca2bed4ac Fix nightly.yaml jofleish 2024-02-23 16:47:19 -05:00
  • 9e8d07ef67 Update nightly.yaml for Azure Pipelines John Fleisher 2024-02-23 16:32:20 -05:00
  • 19f5e7ffea
    ci: Really fix set-output. (#7138) Bruce Mitchener 2024-02-23 01:36:13 +07:00
  • e835974978 ci: Really fix set-output. Bruce Mitchener 2024-02-23 01:34:55 +07:00
  • 019c0648fa
    Update coverage.yml Nikolaj Bjorner 2024-02-22 09:37:08 -08:00
  • c0621cb760
    ci: Stop using deprecated ::set-output. (#7136) Bruce Mitchener 2024-02-23 00:35:47 +07:00
  • 143a35d370
    Fix typos. (#7137) Bruce Mitchener 2024-02-23 00:35:15 +07:00
  • 0a87d85c7e ci: Stop using deprecated ::set-output. Bruce Mitchener 2024-02-22 22:12:44 +07:00
  • 3e7c213d2f Fix typos. Bruce Mitchener 2024-02-22 22:17:15 +07:00
  • 785f71b1a6 prepare for 12.6 Nikolaj Bjorner 2024-02-21 19:35:24 -08:00
  • 79b7d8a9e2 throttle squash-store #7134 Nikolaj Bjorner 2024-02-21 10:00:11 -08:00
  • a3d00ce356
    Improved Java phantom references (#7131) Thomas Haas 2024-02-21 17:39:58 +01:00
  • f7691d34fd fix generic example Nikolaj Bjorner 2024-02-21 08:16:01 -08:00
  • a18c8e82ae typo Nikolaj Bjorner 2024-02-20 11:42:29 -08:00
  • 2c89a49ba8
    use fold_left instead of filteri because it is not available on old OCaml versions zapashcanon 2024-02-19 16:54:33 +01:00
  • b1b61c9d57
    explicit some parameters to make working without LSP/Merlin easier zapashcanon 2024-02-19 16:16:59 +01:00
  • f8be07689c
    use List.init, fix complexity of a few operations and make some code more readable zapashcanon 2024-02-19 16:15:20 +01:00
  • 78275d2557
    do not use and for non mutually recursive types zapashcanon 2024-02-19 16:07:50 +01:00
  • 199ef30e0c
    conditionally depend on importlib_resources (#7116) Cal Jacobson 2024-02-18 18:20:24 +13:00
  • e69767b739 Formatting Thomas Haas 2024-02-17 13:27:41 +01:00
  • 9fbd790aad Use correct SuppressWarning annotation to silence the compiler Thomas Haas 2024-02-17 13:25:04 +01:00
  • 323b70af5c Updated CMakeLists.txt again. Thomas Haas 2024-02-17 12:40:03 +01:00
  • d8930e7101 Update CMakeLists.txt for building the Java API. Thomas Haas 2024-02-17 12:33:49 +01:00
  • a1528aaadd Made Context.close idempotent (as recommended) Thomas Haas 2024-02-17 11:35:38 +01:00
  • 727643c54e Made Statistics.Entry a static subclass Thomas Haas 2024-02-17 11:30:26 +01:00
  • 862dd9bcd4 Reworked phantom reference handling. - Replaced IDecRefQueue with a new Z3ReferenceQueue class - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count. - Context now owns a single Z3ReferenceQueue for all types of references. Thomas Haas 2024-02-17 11:30:10 +01:00
  • 84d592c1f2 fix #7121 Nikolaj Bjorner 2024-02-16 09:59:57 +07:00
  • 2b14793213 #7117 Nikolaj Bjorner 2024-02-14 17:08:09 +07:00
  • 155dfb10c4
    Fix some typos in identifiers. (#7118) Bruce Mitchener 2024-02-14 09:25:32 +07:00
  • dba2f788df
    ci: Update microsoft/setup-msbuild to v2 from v1.3. (#7119) Bruce Mitchener 2024-02-14 09:24:31 +07:00
  • 4d06c399cc replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat Lev Nachmanson 2024-02-13 10:51:44 -10:00
  • 02dd1c5a01 Fix some typos in identifiers. Bruce Mitchener 2024-02-13 23:26:40 +07:00
  • 839d13542e ci: Update microsoft/setup-msbuild to v2 from v1.3. Bruce Mitchener 2024-02-13 23:20:03 +07:00
  • f1d97c7a3a allow callbacks to be nested Nikolaj Bjorner 2024-02-13 20:30:17 +07:00
  • 3eb42cdf4b minor changes Jakob Rath 2024-02-08 15:25:00 +01:00
  • 705203ea4c display Jakob Rath 2024-02-08 15:13:22 +01:00
  • 8d45c954c5 enable new propagate_from_containing_slice Jakob Rath 2024-02-08 15:11:36 +01:00
  • 0ada7f8e40 bug with sizes Jakob Rath 2024-02-08 14:20:26 +01:00
  • 0cef6bec4e be explicit about intended division semantics Jakob Rath 2024-02-08 13:02:26 +01:00
  • f69506e9cf
    conditionally depend on importlib_resources Cal Jacobson 2024-02-07 23:20:10 -08:00
  • 53f89a81c1
    Fix some typos. (#7115) Bruce Mitchener 2024-02-08 14:06:43 +07:00
  • c81504864c Fix some typos. Bruce Mitchener 2024-02-08 00:44:52 +07:00
  • 85d3e266a4 Update viable::propagate_from_containing_slice to use new get_fixed_sub_slices (wip) Jakob Rath 2024-02-07 17:16:26 +01:00
  • 9283b4169c Add get_fixed_sub_slices Jakob Rath 2024-02-07 15:38:26 +01:00