3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00

Commit graph

  • 4887372bcd Different heuristic CEisenhofer 2025-01-21 11:16:45 +0100
  • 791ad83e4e Trying hybrid eq-repair strategy CEisenhofer 2025-01-21 10:52:03 +0100
  • 3cdcd831b1 fix build breaks Nikolaj Bjorner 2025-01-20 20:36:26 -0800
  • a3f7541719 fix #7517 Nikolaj Bjorner 2025-01-20 19:04:36 -0800
  • fb5834268e fix unit tests, add subsampling mode for false literals Nikolaj Bjorner 2025-01-20 17:34:59 -0800
  • 22e4054674 add clausal lookahead to arithmetic solver as part of portfolio Nikolaj Bjorner 2025-01-20 16:16:46 -0800
  • e69e719485
    Bump docker/build-push-action from 6.10.0 to 6.12.0 dependabot[bot] 2025-01-20 22:30:49 +0000
  • 78b77b9d1e Special case regex membership with constant string CEisenhofer 2025-01-20 16:51:34 +0100
  • 73062fc892 Fixed arguments CEisenhofer 2025-01-20 16:25:16 +0100
  • e5c638dca9 Improve length repair CEisenhofer 2025-01-20 16:16:55 +0100
  • 149bc27e97 use cmake from PyPI only when system executable is not available Michał Górny 2025-01-18 14:22:40 +0100
  • a941f5ae84 reset m_conflict indicator on sls model Nikolaj Bjorner 2025-01-15 20:56:44 -0800
  • 557c01a0e5 fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it Nikolaj Bjorner 2025-01-15 19:52:04 -0800
  • a5e1e7f5d2 set lookahead mode to default Nikolaj Bjorner 2025-01-15 19:10:25 -0800
  • 158dea575b add case for ite Nikolaj Bjorner 2025-01-15 19:07:18 -0800
  • eed3fa6d49 add case for ite Nikolaj Bjorner 2025-01-15 18:54:50 -0800
  • f422e26b3c add case for ite Nikolaj Bjorner 2025-01-15 18:53:26 -0800
  • 5365952796 fix #7510 Nikolaj Bjorner 2025-01-15 13:12:20 -0800
  • a84130e844 prepare update stack for Boolean lookaheads Nikolaj Bjorner 2025-01-15 12:33:31 -0800
  • 498c9a686b throw exceptions where sls lacks support Nikolaj Bjorner 2025-01-15 11:20:03 -0800
  • 5fec07a57e fix unit test Nikolaj Bjorner 2025-01-15 08:38:14 -0800
  • 878fd48819 fix compiler warning Nikolaj Bjorner 2025-01-14 16:38:22 -0800
  • 11909cfdff allow a plateau mode Nikolaj Bjorner 2025-01-14 16:38:12 -0800
  • 076d3dbf13 fix assertion violation in the code path where the simplifier throws a memout exception Nikolaj Bjorner 2025-01-14 16:37:53 -0800
  • 31d4ba0009 re-introduce option to dump arithmetic lemmas to std-out Nikolaj Bjorner 2025-01-14 13:54:56 -0800
  • 8515cebd19 add plateau option Nikolaj Bjorner 2025-01-14 13:54:20 -0800
  • 648cf9602e fix uninitialized variable warnings Nikolaj Bjorner 2025-01-14 13:54:05 -0800
  • 27cc928631 try m_fixed_var_eh Lev Nachmanson 2025-01-14 07:11:53 -1000
  • 8c5abdf818 Can's fix to relevancy propagation Nikolaj Bjorner 2025-01-14 08:14:53 -0800
  • 89ed4d6c8b use monomial variable, not the fixed variable Nikolaj Bjorner 2025-01-14 07:27:59 -0800
  • a08a3ee32b align reslimit with ddfw Nikolaj Bjorner 2025-01-13 18:19:35 -0800
  • 3c5b8bd03d Update parray.h Nikolaj Bjorner 2025-01-13 18:19:12 -0800
  • c01336553e move fixed variable propagation to nla_core/monomial_bounds Nikolaj Bjorner 2025-01-13 18:18:53 -0800
  • 16c60bbeba
    Bump docker/build-push-action from 6.10.0 to 6.11.0 dependabot[bot] 2025-01-13 22:54:18 +0000
  • f3e7c8c9df include QF_SNIA Nikolaj Bjorner 2025-01-13 08:13:39 -0800
  • 943d881340 fixes to hybrid mode Nikolaj Bjorner 2025-01-12 16:59:27 -0800
  • 9770c00592 adjust heuristic in random-inc-dec for finite domains Nikolaj Bjorner 2025-01-12 14:23:18 -0800
  • 97acf71d2d fixup registration with new terms during internalization Nikolaj Bjorner 2025-01-12 14:12:02 -0800
  • d3183fafc7 remove binspr experiment Nikolaj Bjorner 2025-01-12 13:39:26 -0800
  • 8d2b9b41fd fix compiler warnings Nikolaj Bjorner 2025-01-12 13:39:13 -0800
  • 85356c5548 enable propagation when there are changed columns Nikolaj Bjorner 2025-01-12 13:30:31 -0800
  • 558758fcf1 another stab at fixing substring interval extraction combinatorics Nikolaj Bjorner 2025-01-12 11:14:17 -0800
  • fa22b646aa address some build warnings. Nikolaj Bjorner 2025-01-12 10:18:11 -0800
  • b780b54574 optimization of sls-arith and fix build warnings Nikolaj Bjorner 2025-01-12 09:49:48 -0800
  • 49dba337f7 fix ubuntu clang build Nikolaj Bjorner 2025-01-11 20:02:22 -0800
  • 17faabea9e
    Update msvc-static-build-clang-cl.yml Nikolaj Bjorner 2025-01-11 17:51:33 -0800
  • c6f58c8bf7 updates to some_string_in_re per code review comments Nikolaj Bjorner 2025-01-11 17:47:27 -0800
  • c572fc2e4f
    Regex membership (#7506) Clemens Eisenhofer 2025-01-12 02:41:37 +0100
  • 9a237d55ca fix misc build warnings Nikolaj Bjorner 2025-01-11 17:41:24 -0800
  • d97bd48669 adding lookahead mode to arithmetic sls solver Nikolaj Bjorner 2025-01-11 15:47:17 -0800
  • c3855486b2 Fixed gc problem CEisenhofer 2025-01-10 10:44:27 +0100
  • 847278fba8 adding global lookahead variant to sls arith solver Nikolaj Bjorner 2025-01-09 16:47:33 -0800
  • fc3a351d95 Make finding a word in the regex iterative CEisenhofer 2025-01-09 17:17:48 +0100
  • f9ce41bd2b Update theory_lra.cpp Nikolaj Bjorner 2025-01-08 15:41:08 -0800
  • 270c127407 sketch fixed variable callback mechanism Nikolaj Bjorner 2025-01-08 12:50:46 -0800
  • c1a62d346c add missing return Nikolaj Bjorner 2025-01-07 21:02:02 -0800
  • 1cb126f3dd remove assertion that doesn't build Nikolaj Bjorner 2025-01-07 17:16:33 -0800
  • 2dd4faf598 sketch expr_inverter approach for eliminating unconstrained regex containment. Nikolaj Bjorner 2025-01-07 16:53:28 -0800
  • a1f85989eb debug with magic_call deb_magic_call Lev Nachmanson 2025-01-07 13:16:35 -1000
  • c7dfb619a2
    Minor tweaks in README.md (#7504) chausner 2025-01-07 23:31:45 +0100
  • ab9ea4e6e7 Add outline of elimination for regex membership constraints Nikolaj Bjorner 2025-01-07 14:17:20 -0800
  • a23f5c5e49
    Minor tweaks in README.md chausner 2025-01-07 22:50:43 +0100
  • b6c0e6fe4b
    Update README.md Nikolaj Bjorner 2025-01-07 11:02:39 -0800
  • af0113f41f Disable the Code Coverage workflow Nikolaj Bjorner 2025-01-07 11:01:49 -0800
  • 5c60c6662c
    Small seq-sls fixes (#7503) Clemens Eisenhofer 2025-01-07 18:26:00 +0100
  • e133a297ba change score for comparisons to use hamming distance Nikolaj Bjorner 2025-01-07 03:58:44 -0800
  • 2d10779f4a Fixed regex problem CEisenhofer 2025-01-07 11:01:07 +0100
  • b765225ed8 Calculation based on wrong update list CEisenhofer 2025-01-07 10:06:38 +0100
  • f77f259542 fix build Nikolaj Bjorner 2025-01-06 18:12:12 -0800
  • b6f45bcd9f limit lookahead count to 20 Nikolaj Bjorner 2025-01-06 18:06:00 -0800
  • aed0ad3505 limit lookahead count to 10 Nikolaj Bjorner 2025-01-06 17:40:17 -0800
  • 59fad2b10a shave off bv test Nikolaj Bjorner 2025-01-06 17:25:30 -0800
  • e3e650a249 optimzie Nikolaj Bjorner 2025-01-06 15:36:20 -0800
  • 6787d87623 hoist update stack creation Nikolaj Bjorner 2025-01-06 13:16:07 -0800
  • 5a5570ef4e remove type check in insert_update Nikolaj Bjorner 2025-01-06 11:12:08 -0800
  • 67827bfe56 restore nyi trace Nikolaj Bjorner 2025-01-06 08:37:14 -0800
  • a8b88b1850 fish for nyi Nikolaj Bjorner 2025-01-06 07:30:16 -0800
  • e45f186e67 make ite evaluation sensitive to using temporary Boolean assignment Nikolaj Bjorner 2025-01-05 20:59:14 -0800
  • be5a16cc4d fixup scoring function for sle and ule Nikolaj Bjorner 2025-01-05 19:05:33 -0800
  • b3e410b5e4 fixup tabu checks to revised representation Nikolaj Bjorner 2025-01-05 14:24:41 -0800
  • 71a4801c1d add shortcuts to convert to python objects in cases of numerals and strings Nikolaj Bjorner 2025-01-05 12:17:38 -0800
  • cd41b21fa2 fix #7501 Nikolaj Bjorner 2025-01-05 11:59:59 -0800
  • f6e3c5ae79 re-enable fixed tabu Nikolaj Bjorner 2025-01-05 11:49:12 -0800
  • 6b17862886 bug-fixes to root-literal sls Nikolaj Bjorner 2025-01-05 11:31:12 -0800
  • bed085934f bugfixes to bv-sls Nikolaj Bjorner 2025-01-04 20:57:17 -0800
  • 710f757495 fixup parameter handling for enabling bv-lookahead Nikolaj Bjorner 2025-01-04 15:57:02 -0800
  • 05f166f736 add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving Nikolaj Bjorner 2025-01-04 13:40:49 -0800
  • 7e4681d836 enable rotation Nikolaj Bjorner 2025-01-03 11:49:39 -0800
  • 5a57636cd8 use native sdiv Nikolaj Bjorner 2025-01-03 10:56:15 -0800
  • bfcd75595e update test file Nikolaj Bjorner 2025-01-02 21:03:50 -0800
  • 1131d8dbe6 update test file Nikolaj Bjorner 2025-01-02 20:59:40 -0800
  • e9c656701d throttle costly flips by reset and random Nikolaj Bjorner 2025-01-02 20:39:41 -0800
  • 70f7feabc8 flip tabu on predicate being repaired, add model rotation code Nikolaj Bjorner 2025-01-02 14:39:36 -0800
  • f67e1b8b8b only allow flip if it doesn't increase unsat score Nikolaj Bjorner 2025-01-02 08:39:43 -0800
  • 814d7f4d0a block flips to units Nikolaj Bjorner 2025-01-01 16:01:58 -0800
  • cb61af0496 fix restart counters Nikolaj Bjorner 2025-01-01 14:34:09 -0800
  • 0128a1e067 check for bit-vector Nikolaj Bjorner 2025-01-01 13:04:15 -0800
  • b12e72eaad extend lookhaead to work over nested terms with predicates Nikolaj Bjorner 2025-01-01 12:37:39 -0800
  • 234bd402d3 take 1 on flip conditions Nikolaj Bjorner 2024-12-31 12:16:54 -0800
  • b415b82625 take 1 on flip conditions Nikolaj Bjorner 2024-12-31 11:44:38 -0800