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

Commit graph

  • a511b8bcf0 disable unit tests relying on changed functionality Nikolaj Bjorner 2024-12-31 09:24:41 -0800
  • 3433b14dfa separate fixed from bits to allow updates that break tabu Nikolaj Bjorner 2024-12-30 17:47:18 -0800
  • 983763213b temper verbose output on tabu updates Nikolaj Bjorner 2024-12-30 12:36:47 -0800
  • 81678923a1 take into account for empty vars Nikolaj Bjorner 2024-12-30 11:09:35 -0800
  • 27cb81e7e6
    Several changes to make sls terminate more often with length/extract operations (#7498) Clemens Eisenhofer 2024-12-30 19:53:27 +0100
  • c468ff4f97 Commented out debug output CEisenhofer 2024-12-30 19:35:49 +0100
  • 809267258d Add padding if required CEisenhofer 2024-12-30 19:25:06 +0100
  • 4773bec975 check for null before debug assertions Nikolaj Bjorner 2024-12-30 09:44:23 -0800
  • 0cfaf5ad92 Merge remote-tracking branch 'microsoft/master' into eis-sls3 CEisenhofer 2024-12-30 18:03:14 +0100
  • 0227cebee4 Added missing progressing cases in extraction CEisenhofer 2024-12-30 17:56:43 +0100
  • d8741b4aec have apply-update check can_set instead of caller Nikolaj Bjorner 2024-12-30 08:56:09 -0800
  • bcf66f214f code cleanup, add comments Nikolaj Bjorner 2024-12-30 08:51:41 -0800
  • 322dcec531
    Add 2 new API functions to get depth & groundness of exprs (#7479) Nuno Lopes 2024-12-30 16:49:43 +0000
  • f99e1ee581
    Support BitVectors in the TypeScript Optimize API (#7480) Dmitri 2024-12-30 18:49:30 +0200
  • 19c95f8561
    Add new string repair heuristic (#7496) Clemens Eisenhofer 2024-12-30 17:49:07 +0100
  • e002c57aa2
    Fixed range regex (#7497) Clemens Eisenhofer 2024-12-30 17:48:09 +0100
  • d54e54580d Guarded index check CEisenhofer 2024-12-30 17:30:12 +0100
  • 7c02410e52 Pad/Truncate string in sls extract/length to fit length constraints CEisenhofer 2024-12-30 17:04:22 +0100
  • 9f08f1f228 Added case for str.at CEisenhofer 2024-12-30 14:20:18 +0100
  • 30ffedd46a Fix sls for str.at CEisenhofer 2024-12-30 14:03:37 +0100
  • 602d97f29e Fixed range regex CEisenhofer 2024-12-30 12:31:46 +0100
  • 64b09d87e4 Merge remote-tracking branch 'microsoft/master' into sls-eisenhofer Use a hashset rather than map CEisenhofer 2024-12-30 10:44:08 +0100
  • b42217204a Added parameter to select string update function CEisenhofer 2024-12-30 10:24:07 +0100
  • 85c5feb0b2 Renamed function CEisenhofer 2024-12-30 09:44:28 +0100
  • d81de1a67e align updated version of lookahead with legacy heuristics Nikolaj Bjorner 2024-12-29 21:22:32 -0800
  • 6ea68310c9 fix stack overflow regression in bool_rewriter Nikolaj Bjorner 2024-12-28 18:21:59 -0800
  • 3526d03cca remove VERIFY output Nikolaj Bjorner 2024-12-28 18:01:32 -0800
  • f41134d1b6 h Nikolaj Bjorner 2024-12-28 17:40:15 -0800
  • a5bc5ed813 try uneven lookahead skew Nikolaj Bjorner 2024-12-27 13:55:22 -0800
  • 3aacc62229 api: hint the compiler that logging enabled is unlikely Nuno Lopes 2024-12-28 09:52:36 +0000
  • bd8c870bbe api: avoid some string copies when using mk_external_string Nuno Lopes 2024-12-28 09:42:54 +0000
  • 0b9ed925d6 try dual phase lookahead Nikolaj Bjorner 2024-12-27 13:34:48 -0800
  • 1f55ec5cef fix random update to a legal one Nikolaj Bjorner 2024-12-27 13:01:47 -0800
  • c82518ca36 include cmath to define std::pow Nikolaj Bjorner 2024-12-27 12:29:44 -0800
  • b0eee16109 fix double override bug in bv_lookahead, integrate with bv_eval Nikolaj Bjorner 2024-12-27 12:26:11 -0800
  • c1c6276ae2 Trying different update generation function CEisenhofer 2024-12-27 18:11:48 +0100
  • 8de0005ab3
    Bugfix seq-eq sls (#7495) Clemens Eisenhofer 2024-12-27 17:40:34 +0100
  • 1cd5e22d66 One check was missing CEisenhofer 2024-12-27 14:54:27 +0100
  • 9d7ce8e779 Removed debug code CEisenhofer 2024-12-27 14:29:41 +0100
  • 2a0c1dce18 Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping CEisenhofer 2024-12-27 13:54:29 +0100
  • 5eb71c3be6 integrate lookahead v1 into repair loop Nikolaj Bjorner 2024-12-26 17:49:30 -0800
  • c58171478f remove dead code Nikolaj Bjorner 2024-12-26 13:48:55 -0800
  • d3a6521185 rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead. Nikolaj Bjorner 2024-12-26 13:06:28 -0800
  • 13dcfd26dd remove debug out Nikolaj Bjorner 2024-12-25 15:23:47 -0800
  • c9cae77304 update regex membership to be slightly better tuned Nikolaj Bjorner 2024-12-25 10:56:16 -0800
  • f4ed432244 try a basic heuristic that finds some string that belongs to re. Nikolaj Bjorner 2024-12-25 10:10:59 -0800
  • 09825edcd8 remove compute depth in favor of already existing get_depth Nikolaj Bjorner 2024-12-23 18:49:54 -0800
  • e332904fb2 cosmetic updates Nikolaj Bjorner 2024-12-23 18:49:38 -0800
  • 85d3041a80 avoid platform non-reproducibility due to argument evaluation ordering Nikolaj Bjorner 2024-12-23 17:13:51 -0800
  • 23c4728d68 remove some platform specific behavior Nikolaj Bjorner 2024-12-23 16:28:10 -0800
  • 554191885e remove platform dependent print Nikolaj Bjorner 2024-12-23 16:13:36 -0800
  • 4f4cafbc98 start update with expr-inverter to handle PB Nikolaj Bjorner 2024-12-22 18:17:07 -0800
  • b592ce4707 reserve space in heap to avoid debug check in elim_unconstrained Nikolaj Bjorner 2024-12-22 18:15:44 -0800
  • 97c70ba501 remove some uneeded constructors Nuno Lopes 2024-12-22 15:06:58 +0000
  • fb5bbb8074 read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0 Nikolaj Bjorner 2024-12-22 14:07:29 +0100
  • a214dc32e8 add some comments, fix nyis Nikolaj Bjorner 2024-12-22 13:52:19 +0100
  • 65b678dd42 use bail_out instead of early return to ensure marks are cleared Nikolaj Bjorner 2024-12-22 06:14:38 +0100
  • 78ce6c1c6c revert relevancy override Nikolaj Bjorner 2024-12-21 18:10:10 +0100
  • 3b2315d771 remove verbose output Nikolaj Bjorner 2024-12-21 15:52:57 +0100
  • 578804acf4 fix #7460 Nikolaj Bjorner 2024-12-21 14:42:23 +0100
  • 2044fb460d fix #7490 Nikolaj Bjorner 2024-12-21 14:32:02 +0100
  • 8dec84110b add lia2card tactic as default #7483 Nikolaj Bjorner 2024-12-21 13:11:22 +0100
  • 4f7b6c794e always copy Microsoft.Z3.xml into package directory #7482 Nikolaj Bjorner 2024-12-21 13:10:05 +0100
  • 07b1ee5dcc mask regression on fpa by not auto-setting relevancy=0 Nikolaj Bjorner 2024-12-21 12:41:04 +0100
  • da6a5facca revert change to setup_context that delays it until there are assertions Nikolaj Bjorner 2024-12-21 11:53:46 +0100
  • db9f45dfec set relevancy = 0 in auto-config mode when there are bit-vectors and no quantifiers, #7484 Nikolaj Bjorner 2024-12-20 18:10:46 +0100
  • 114cae50a5 update gcm script Nikolaj Bjorner 2024-12-20 17:27:21 +0100
  • 87f7a20e14 Add (updated and general) solve_for functionality for arithmetic, add congruence_explain to API to retrieve explanation for why two terms are congruent Tweak handling of smt.qi.max_instantations Nikolaj Bjorner 2024-12-19 23:26:42 +0100
  • e4ab2944fe
    Optimize expr_safe_replace for quantifiers when all source patterns are vars (#7481) Nuno Lopes 2024-12-19 22:05:13 +0000
  • c33bc2c8be expr_abstract: save 1 hashtable lookup per app argument when we already know that the app is missing one arg to rewrite Nuno Lopes 2024-12-18 09:50:50 +0000
  • 7153a65e74
    Update expr_safe_replace.cpp Nuno Lopes 2024-12-18 09:34:16 +0000
  • 0429c7002e
    Update expr_safe_replace.cpp Nuno Lopes 2024-12-17 21:33:34 +0000
  • e54dfb5b01
    Update expr_safe_replace.cpp Nuno Lopes 2024-12-17 16:21:26 +0000
  • 2f5c0a6985 remove 2 unneeded lambda captures Nuno Lopes 2024-12-17 16:02:24 +0000
  • 1166c5b666
    Support BitVectors in the TypeScript Optimize API Dmitri 2024-12-17 13:37:47 +0200
  • 4308dfbcdc
    Update z3_api.h Nuno Lopes 2024-12-16 12:13:45 +0000
  • c250209a3f
    Update api_ast.cpp Nuno Lopes 2024-12-16 12:12:24 +0000
  • 6f24123f0c reduce hash table lookups in expr_abstract in half z3-4.13.4 Nuno Lopes 2024-12-16 11:00:55 +0000
  • a6e59ea45e fix build flags for release.yaml Nikolaj Bjorner 2024-12-16 04:41:29 +0100
  • a97ad76bb6 publish pypi Nikolaj Bjorner 2024-12-15 13:00:50 -0800
  • 200ef236da Update RELEASE_NOTES.md Nikolaj Bjorner 2024-12-15 06:01:44 -0800
  • e40972b7f7 Update release.yml Nikolaj Bjorner 2024-12-15 05:55:48 -0800
  • b529a58b91 add unit test for incremental equation edit distance with repair Nikolaj Bjorner 2024-12-15 05:53:28 -0800
  • 31ee56c1ca wip - incremental edit distance algorithm Nikolaj Bjorner 2024-12-13 09:30:39 -0800
  • 538f74d64c extract stats with finalize for parallel mode Nikolaj Bjorner 2024-12-13 09:22:30 -0800
  • b4295620b3
    Add __enter__ and __exit__ methods on Optimize class (#7477) Oskar Haarklou Veileborg 2024-12-13 18:19:04 +0100
  • c9ce32ddff Add __enter__ and __exit__ methods on Optimize class Oskar Haarklou Veileborg 2024-12-13 11:09:08 +0100
  • 1e5c59a06f add repair step for str.replace Nikolaj Bjorner 2024-12-12 09:15:36 -0800
  • e8c2360043 fix #7461 Nikolaj Bjorner 2024-12-09 16:57:17 -0800
  • 8f5658b77d add another baseline heuristic for string equalities, add cases for array axioms. Nikolaj Bjorner 2024-12-09 15:55:11 -0800
  • e5f8327483
    Update emscripten (#7473) Kevin Gibbons 2024-12-06 18:11:14 -0800
  • e6b78c34eb update js readme about tests Kevin Gibbons 2024-12-06 13:05:21 -0800
  • d0f8db45d3 update emscripten version in CI Kevin Gibbons 2024-12-06 13:03:40 -0800
  • bd41f85b2c update typescript and fix errors Kevin Gibbons 2024-12-06 12:57:14 -0800
  • d93a8fd3f0 update prettier Kevin Gibbons 2024-12-06 12:30:09 -0800
  • 2d903aae87 fix return type for async wrapper functions Kevin Gibbons 2024-12-06 12:23:31 -0800
  • df793f9f30 fixes for newer emscripten thread handling behavior Kevin Gibbons 2024-12-06 12:14:57 -0800
  • 4fbf54afd0 fixes to regex membership and edit updates Nikolaj Bjorner 2024-12-06 09:50:30 -0800
  • 1ab0962d43 partial fix to make computed term integer well-formed for solve_for functionality Nikolaj Bjorner 2024-12-05 17:10:52 -0800
  • bcb61ee12c v0 of edit distance repair Nikolaj Bjorner 2024-12-05 14:14:27 -0800