3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00

Commit graph

  • 4be4067f75
    Typescript high-level api for Sets (#7471) Yuantian Ding 2024-12-05 10:00:11 -0500
  • 9db4ac434d fix unsoundness with what appears to be unit literals but really are literals that are justified reassert-all-units Nikolaj Bjorner 2024-12-04 16:08:50 -0800
  • 4d61c19917 add code path to reassert units Nikolaj Bjorner 2024-12-04 15:35:21 -0800
  • a17d4e68eb bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals Nikolaj Bjorner 2024-12-04 15:32:08 -0800
  • 421d754c5a Typescript high-level api for Sets Yuantian Ding 2024-12-04 14:59:49 -0500
  • 6ea4110b30
    Bump docker/build-push-action from 6.9.0 to 6.10.0 (#7469) dependabot[bot] 2024-12-02 15:39:49 -0800
  • 7bb5b38657
    Bump docker/build-push-action from 6.9.0 to 6.10.0 dependabot[bot] 2024-12-02 23:20:23 +0000
  • 8c44f0c291 add ast-mark to make traversal feasible arith-gomory-ite Nikolaj Bjorner 2024-12-02 14:38:34 -0800
  • aec867586a updates to equality solving search Nikolaj Bjorner 2024-12-02 13:41:18 -0800
  • bd5d388f15 try pushing gcd over ite Nikolaj Bjorner 2024-12-02 13:34:32 -0800
  • e6feb8423a sls: fix bug where unsat remains empty after a literal is flipped. The new satisfiable subset should be checked Nikolaj Bjorner 2024-12-01 18:35:56 -0800
  • 24c3cd38d1 add v0 of equality solver Nikolaj Bjorner 2024-11-30 17:25:49 -0800
  • 05e053247d add facility to solve for a linear term over API Nikolaj Bjorner 2024-11-30 09:34:27 -0800
  • d2411567b5 add projection with witnesses Nikolaj Bjorner 2024-11-27 10:26:18 -0800
  • b7b611d84b inherit from std::exception Nikolaj Bjorner 2024-11-27 08:18:37 -0800
  • ab1be5c06e internalize the reduce_args_tactic to reduce the number of heap allocations Nuno Lopes 2024-11-27 12:35:40 +0000
  • 1ccfba6a91 remove unreachble code Nuno Lopes 2024-11-27 12:09:16 +0000
  • 1e62029413 use ztring Nikolaj Bjorner 2024-11-25 17:36:42 -0800
  • fce377e1d7 add basic regex functions Nikolaj Bjorner 2024-11-25 17:34:49 -0800
  • b143a954c5 add notes and additional functions to sls-seq Nikolaj Bjorner 2024-11-25 13:46:16 -0800
  • aed3279d7d add missing new_value_eh when repaired up Nikolaj Bjorner 2024-11-24 19:57:40 -0800
  • 1e839e5ac2 add missing new_value_eh when repaired up Nikolaj Bjorner 2024-11-24 19:42:13 -0800
  • 7ed185aa9e add comments Nikolaj Bjorner 2024-11-24 19:09:50 -0800
  • 4559b23caf add local search functionality to sls_seq_plugin Nikolaj Bjorner 2024-11-24 11:24:17 -0800
  • 65bfcec146 resurrect rewriting of equality over ite rewrite-ite-arith Nikolaj Bjorner 2024-11-22 16:56:08 -0800
  • 0bf9369414 fix bug in rewriter Nikolaj Bjorner 2024-11-22 14:56:41 -0800
  • 5025c3c8a9 add rewrites for hoisting constants from ite expressions Nikolaj Bjorner 2024-11-22 13:59:11 -0800
  • b4e768cfb0 adding plugin for local search strings Nikolaj Bjorner 2024-11-22 13:56:03 -0800
  • 36725758eb fix typos POLING -> POLLING in setup.py and remove unused CFLAGS Nikolaj Bjorner 2024-11-21 11:32:38 -0800
  • 71bad7159b #7418 - circumvent use of timer threads to make WASM integration of z3 easier Nikolaj Bjorner 2024-11-21 11:20:05 -0800
  • 94f0aff47f remove the use-pthread Nikolaj Bjorner 2024-11-19 19:55:03 -0800
  • 76795a44e4 remove -pthread from options Nikolaj Bjorner 2024-11-19 19:50:47 -0800
  • 8965123c0d fix type in setup.py Nikolaj Bjorner 2024-11-19 19:08:29 -0800
  • 10d9c81957 adapt for pyodide built Nikolaj Bjorner 2024-11-19 18:51:04 -0800
  • 012fc1b72b more detailed tracing of where unmaterialized exceptions happen Nikolaj Bjorner 2024-11-19 18:15:42 -0800
  • 7de0c29f12
    Update pyodide.yml Nikolaj Bjorner 2024-11-19 12:58:08 -0800
  • e855a50d9b add exception handling to easier diagnose #7418 Nikolaj Bjorner 2024-11-19 11:46:54 -0800
  • 5168a13efa track exceptions in reason-unknown Nikolaj Bjorner 2024-11-19 09:28:13 -0800
  • a8a50695c9
    Update README.md Nikolaj Bjorner 2024-11-18 13:29:06 -0800
  • 15f954ec3b add picture of z3guide Nikolaj Bjorner 2024-11-18 13:21:35 -0800
  • 24dfc17920
    Update README.md Nikolaj Bjorner 2024-11-18 11:54:34 -0800
  • 4b72e517b7 SLS: log clause , allow more frequent export of SLS state to SMT Nikolaj Bjorner 2024-11-17 20:13:02 -0800
  • 84447b7031 remove incremental mode from EUF, include statistics about restart vs propagation calls to sls Nikolaj Bjorner 2024-11-17 16:58:18 -0800
  • c7ea4964f2 bug fixes to sls Nikolaj Bjorner 2024-11-17 13:07:28 -0800
  • e380903d61
    Update README.md Nikolaj Bjorner 2024-11-16 19:20:04 -0800
  • 2310514e02 fix #7454 Nikolaj Bjorner 2024-11-16 18:20:06 -0800
  • 5fd1231ec0 incorporate ls during propagation Nikolaj Bjorner 2024-11-16 15:28:23 -0800
  • 836802ed71
    Update pyodide.yml Nikolaj Bjorner 2024-11-16 13:36:38 -0800
  • cdc483374c
    Update pyodide.yml Nikolaj Bjorner 2024-11-16 13:01:03 -0800
  • 00c5600b09
    Update pyodide.yml Nikolaj Bjorner 2024-11-16 12:36:53 -0800
  • 750dd68a14 enable par_then and par_or even if single threaded - fall back to sequential mode Nikolaj Bjorner 2024-11-16 12:29:22 -0800
  • f64d077d2a fix re-entrancy bug during flip in arith_base Nikolaj Bjorner 2024-11-16 12:29:03 -0800
  • e4e5735620 update to set single threaded Nikolaj Bjorner 2024-11-16 09:12:32 -0800
  • b929996941 update to set single threaded Nikolaj Bjorner 2024-11-16 09:11:44 -0800
  • f39198d9a8 move build-env setting to correct place Nikolaj Bjorner 2024-11-16 08:32:47 -0800
  • 197951cad4 fixes to sls Nikolaj Bjorner 2024-11-16 08:28:17 -0800
  • 7c5ff7c623 moving compile time flags to setup for pyodide Nikolaj Bjorner 2024-11-16 08:28:00 -0800
  • 8bfe403dd3
    Update pyodide.yml Nikolaj Bjorner 2024-11-16 08:11:36 -0800
  • 60b14f3675
    Update pyodide.yml Nikolaj Bjorner 2024-11-16 08:05:17 -0800
  • e7d083304b
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 19:29:28 -0800
  • bd5f8b17d6
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 19:26:24 -0800
  • 751d666e16
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 19:16:54 -0800
  • 24f9a86539
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 18:49:51 -0800
  • dba167472e
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 18:43:51 -0800
  • 704278caa9
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 18:40:17 -0800
  • 231248d610
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 18:36:13 -0800
  • 329e1ddb10
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 18:30:41 -0800
  • aab6c1e909
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 16:57:11 -0800
  • ccbe6c33ae fixes Nikolaj Bjorner 2024-11-15 09:29:24 -0800
  • 88048901f0
    Update pyodide.yml Nikolaj Bjorner 2024-11-15 08:45:51 -0800
  • ea590def47 remove breaking experiment Nikolaj Bjorner 2024-11-15 08:03:57 -0800
  • 1d8a904e99 build fixes Nikolaj Bjorner 2024-11-14 22:10:59 -0800
  • 77eacef2ae build fixes Nikolaj Bjorner 2024-11-14 22:08:13 -0800
  • 3f407982f3 build fixes Nikolaj Bjorner 2024-11-14 21:55:44 -0800
  • ca6ec0d9e4 fixes to pyodide action Nikolaj Bjorner 2024-11-14 21:45:47 -0800
  • 8e3b9f6686 add sequential option for SLS, fixes to import/export methods SLS<->SMT Nikolaj Bjorner 2024-11-14 21:43:26 -0800
  • 6a9d5910cb add method for resetting limit Nikolaj Bjorner 2024-11-14 21:42:36 -0800
  • 6eae3f0863 add cases for unconstrained sequences and strings Nikolaj Bjorner 2024-11-14 21:40:00 -0800
  • 62db7642ec refine rewriting depth for lt constraints Nikolaj Bjorner 2024-11-14 21:39:33 -0800
  • 3fed840233 update pyodide.yml Audrey Dutcher 2024-11-14 22:15:57 -0700
  • eab49da274
    Update pyodide.yml Nikolaj Bjorner 2024-11-14 20:49:33 -0800
  • 75d0dd891b
    Update pyodide.yml Nikolaj Bjorner 2024-11-14 20:12:30 -0800
  • e53ea005a0
    Update pyodide.yml Nikolaj Bjorner 2024-11-14 19:26:03 -0800
  • 4cdc3d6b1a
    Update pyodide.yml Nikolaj Bjorner 2024-11-14 18:59:53 -0800
  • 4d0394e33f
    Update pyodide.yml Nikolaj Bjorner 2024-11-14 18:54:23 -0800
  • 0dc4c5e58b
    Create pyodide.yml Nikolaj Bjorner 2024-11-14 18:47:43 -0800
  • cb2c497466 Add Pyodide CI and tests pyodide-ci Audrey Dutcher 2024-11-14 11:28:43 -0700
  • d3009dabfc
    Proposed fix for #7451 (#7452) Linus 2024-11-13 18:11:40 +0100
  • 993ddc6ea3
    Proposed fix for #7451 Linus 2024-11-13 12:47:43 +0100
  • c0e748a51a fix #7446, by adding rewrite simplification Nikolaj Bjorner 2024-11-11 19:16:11 -0800
  • 1cc808c58d fix #7446, by adding rewrite simplification Nikolaj Bjorner 2024-11-11 19:08:11 -0800
  • 30ad22a4ef fix #7449 Nikolaj Bjorner 2024-11-11 15:45:18 -0800
  • 879bb4b1f0 avoid circular dependencies in justifications that get updated. fixes #7443 Nikolaj Bjorner 2024-11-10 19:35:01 -0800
  • 1856ab72d9 fix #7448 Nikolaj Bjorner 2024-11-10 14:40:28 -0800
  • 4f060dd2b1 fix #7445 Nikolaj Bjorner 2024-11-10 14:40:04 -0800
  • fa6f3f2dba fixing prop-queue sls Nikolaj Bjorner 2024-11-04 17:18:02 -0800
  • abd16740ce inherit more exceptions from std::exception Nikolaj Bjorner 2024-11-04 13:52:14 -0800
  • a38bf3e22f port to inherit from std::exception Nikolaj Bjorner 2024-11-04 13:25:14 -0800
  • 407bad3693 add noexcept Nikolaj Bjorner 2024-11-04 11:21:55 -0800
  • 42894f729a add noexcept for signature compatibility Nikolaj Bjorner 2024-11-04 11:13:43 -0800