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

Commit graph

  • 75e46778fa
    Make build process work with pyodide (#7442) Audrey Dutcher 2024-11-04 12:09:51 -0700
  • 92065462b4 use std::exception as base class to z3_exception Nikolaj Bjorner 2024-11-04 11:08:15 -0800
  • 79bef28d47 Make build process work with pyodide Audrey Dutcher 2024-11-04 11:34:30 -0700
  • b870ed192a include disequality expansion for non-unit case. Nikolaj Bjorner 2024-11-04 09:26:32 -0800
  • 1957b4d991 fix reporting on cancelation when based on cancel flag Nikolaj Bjorner 2024-11-02 12:48:03 -0700
  • 604714ba40
    js: Add pseudo-boolean high-level functions (#7426) Jonas Jongejan 2024-11-02 15:34:15 -0400
  • 91dc02d862
    Sls (#7439) Nikolaj Bjorner 2024-11-02 12:32:48 -0700
  • 6559584502 use original gai Nikolaj Bjorner 2024-11-02 12:23:36 -0700
  • d702e68fb9 fix build warning Nikolaj Bjorner 2024-11-02 11:26:25 -0700
  • 40b927ff2b remove package and package lock Nikolaj Bjorner 2024-11-02 11:12:54 -0700
  • 7875c95866 Merge branch 'master' into sls Nikolaj Bjorner 2024-11-02 10:41:15 -0700
  • c7ec2afedb fixes to model construction Nikolaj Bjorner 2024-11-01 15:38:30 -0700
  • 040c29a152 update model generation to fix model bug Nikolaj Bjorner 2024-11-01 14:41:15 -0700
  • 55b64e1f29 use glue as computed without adjustment Nikolaj Bjorner 2024-11-01 13:57:56 -0700
  • 289f8360f2 fix non-termination Nikolaj Bjorner 2024-10-29 23:39:39 -0700
  • 0a404f94be rework elim_unconstrained Nikolaj Bjorner 2024-10-29 22:31:26 -0700
  • ecdfab81a6 fix #7434 Nikolaj Bjorner 2024-10-28 17:50:53 -0700
  • fbf3012864 add virtual destructor Nikolaj Bjorner 2024-10-27 22:24:45 -0700
  • 7e9d0537d7 normalizing inequality Nikolaj Bjorner 2024-10-27 22:23:01 -0700
  • 9a5fa60e98 add missing operator handling for bitwise operators Nikolaj Bjorner 2024-10-27 21:51:36 -0700
  • 077b173858 add missing operator handling for bitwise operators Nikolaj Bjorner 2024-10-27 21:32:55 -0700
  • e35eab000c use th-axioms to track origins of assertions Nikolaj Bjorner 2024-10-27 19:08:44 -0700
  • 5e2cefea9f mk_value needs to accept more cases where integer expression doesn't evalate Nikolaj Bjorner 2024-10-27 19:03:20 -0700
  • bdf3689c6e na Nikolaj Bjorner 2024-10-27 18:53:25 -0700
  • 98bc3d392d fixup model generation for theory_intblast Nikolaj Bjorner 2024-10-27 14:08:22 -0700
  • 7e2acad030 add intblast to legacy SMT solver Nikolaj Bjorner 2024-10-27 12:28:36 -0700
  • aa67c3655f bugfixes Nikolaj Bjorner 2024-10-26 16:10:44 -0700
  • 6f37da5a07 validate sls-arith lemmas Nikolaj Bjorner 2024-10-26 14:56:38 -0700
  • c6f5e3232c use independent completion flag for sls to avoid conflating with genuine cancelation Nikolaj Bjorner 2024-10-26 14:48:13 -0700
  • 646eacd2aa check delayed eqs before nla Nikolaj Bjorner 2024-10-26 11:48:26 -0700
  • fb78a9e3a5 change namespace for single threaded Nikolaj Bjorner 2024-10-26 11:28:54 -0700
  • f902feb478 reorder inclusion order to define smt_context before theory_sls Nikolaj Bjorner 2024-10-26 10:46:23 -0700
  • b0fef6429f
    Add assert_and_track support to Optimize class in .NET binding (#7437) Nikolaj Bjorner 2024-10-26 01:33:09 -0700
  • ab2c992aa1 build warnings Nikolaj Bjorner 2024-10-26 01:31:41 -0700
  • d7b1a5e3be add virtual destructor Nikolaj Bjorner 2024-10-26 01:24:22 -0700
  • 0c2e09db7f remove declaration of context Nikolaj Bjorner 2024-10-26 00:11:08 -0700
  • 4a0bbb1d9f Add assert_and_track support to Optimize class in .NET binding Nikolaj Bjorner 2024-10-25 23:58:32 -0700
  • a88daf246e fix build Nikolaj Bjorner 2024-10-25 23:45:14 -0700
  • ba1630f380 fix build Nikolaj Bjorner 2024-10-25 23:40:05 -0700
  • 848bfb14a1 use common infrastructure for sls-smt Nikolaj Bjorner 2024-10-25 23:29:26 -0700
  • 894bfc7e17 fixes Nikolaj Bjorner 2024-10-25 22:46:15 -0700
  • 22ab598d73 bug fixes Nikolaj Bjorner 2024-10-25 17:26:33 -0700
  • ef95b4eaf2 add plugin to smt_context, factor out sls_smt_plugin functionality. Nikolaj Bjorner 2024-10-25 17:15:05 -0700
  • 8b657f27aa add shortcut to retrieve kind of application Nikolaj Bjorner 2024-10-22 13:05:58 -0700
  • 78d1139ba0 add shortcut to retrieve kind of application Nikolaj Bjorner 2024-10-22 13:04:41 -0700
  • 0ebea1c298 remove debug out Nikolaj Bjorner 2024-10-22 11:58:16 -0700
  • 253f7d7675 fix non-termination bug in elim-unconstrained, add parameter validation to fix #7432 Nikolaj Bjorner 2024-10-22 09:59:12 -0700
  • d18831c8d5 Update sat_ddfw.cpp Nikolaj Bjorner 2024-10-20 10:18:51 -0700
  • f453cdec92 update log level Nikolaj Bjorner 2024-10-22 09:58:36 -0700
  • 45ef6d0109
    js: Adding manual release methods (#7428) Jonas Jongejan 2024-10-22 12:15:49 -0400
  • 93086143b3 fix dirty flag setting Nikolaj Bjorner 2024-10-21 19:57:47 -0700
  • b0dd83cc60 debugging parallel integration Nikolaj Bjorner 2024-10-21 13:27:01 -0700
  • 23fe35da6c Add missing line Jonas Jongejan 2024-10-21 15:39:15 -0400
  • c92ab91a5e Add pointer assertion Jonas Jongejan 2024-10-21 15:37:38 -0400
  • 5cee19fa09
    It uses C++20 BTW (#7429) Kirill A. Korinsky 2024-10-21 05:00:36 +0200
  • 185ddd6488 Track shared variables using a unit set Nikolaj Bjorner 2024-10-20 17:54:44 -0700
  • 59b0e46d99 rename aux functions Nikolaj Bjorner 2024-10-20 16:46:19 -0700
  • cc430987b7 add value transfer option Nikolaj Bjorner 2024-10-20 16:38:00 -0700
  • 68ee5108d8 update the interface in sls_solver to transfer phase between SAT and SLS Nikolaj Bjorner 2024-10-20 15:42:26 -0700
  • 203941b8e8
    It uses C++20 BTW Kirill A. Korinsky 2024-10-20 20:53:59 +0200
  • a48044c6e0 adding model-based sls for datatatypes Nikolaj Bjorner 2024-10-20 10:20:38 -0700
  • 194f4d4e5e Add unregister token Jonas Jongejan 2024-10-20 10:51:23 -0400
  • f2dfee2966 js: Adding manual release methods Jonas Jongejan 2024-10-19 16:10:20 -0400
  • d4f46b5ad2 Add check for arg length Jonas Jongejan 2024-10-19 13:23:29 -0400
  • b28c86132e js: Add pseudo-boolean high-level functions Jonas Jongejan 2024-10-19 12:09:45 -0400
  • 3f33e2c098 delay distinct axiom Nikolaj Bjorner 2024-10-18 15:41:42 -0700
  • 6c3fe3cf46 saturate worklist Nikolaj Bjorner 2024-10-18 14:05:10 -0700
  • a72ad44200 fixup interpretation building Nikolaj Bjorner 2024-10-18 13:34:55 -0700
  • aa2292d5c4 fixes to occurs check Nikolaj Bjorner 2024-10-18 10:41:27 -0700
  • 5864fcba6b fixing model construction for underspecified operators Nikolaj Bjorner 2024-10-18 09:34:49 -0700
  • 7b42ab5264 redo dfs Nikolaj Bjorner 2024-10-17 12:59:59 -0700
  • 69c28f8652 fixes Nikolaj Bjorner 2024-10-17 11:35:31 -0700
  • 0218a15f2e fixup finite domain search Nikolaj Bjorner 2024-10-16 20:59:28 -0700
  • 8ababafe42 fixup finite domain search Nikolaj Bjorner 2024-10-16 20:41:20 -0700
  • 6143070157 add missing factory plugins to model Nikolaj Bjorner 2024-10-16 19:47:13 -0700
  • a23a8cdfc5 add variables from definitions Nikolaj Bjorner 2024-10-16 19:08:33 -0700
  • 0755b2b5f7 axiomatize dt Nikolaj Bjorner 2024-10-16 19:01:20 -0700
  • 92376e67f2 better model replay for loose entries Nikolaj Bjorner 2024-10-16 13:07:04 -0700
  • 5a5e39ae74 fix incrementality bug for pre-processing: replay has to be invoked on every push regardless. Nikolaj Bjorner 2024-10-16 12:18:09 -0700
  • 8ff4036f68
    update unit_lim to the correct value (#7423) stormckey 2024-10-17 01:23:13 +0800
  • 3b1afa4f5e update unit_lim to the correct value stormckey 2024-10-16 19:15:25 +0800
  • 180614330a Refactor context management, improve datatype handling, and enhance logging in sls plugins. Nikolaj Bjorner 2024-10-15 20:33:53 -0700
  • af687532aa updated sls-datatype Nikolaj Bjorner 2024-10-15 16:59:34 -0700
  • 295be7579c added cycle detection Nikolaj Bjorner 2024-10-15 13:39:45 -0700
  • a4275dfb15 dt updates Nikolaj Bjorner 2024-10-15 09:36:07 -0700
  • 3896e18227
    fix the code to cube at the correct frequency (#7422) stormckey 2024-10-15 23:56:35 +0800
  • fc96891c09 fix the code to cube at the correct frequency stormckey 2024-10-15 15:45:40 +0800
  • b551f22aca adt Nikolaj Bjorner 2024-10-14 21:17:57 -0700
  • 5fdf300557 adding dt plugin Nikolaj Bjorner 2024-10-14 17:55:52 -0700
  • 5993735b34 simplify string patterns into prefix/suffix constraints Nikolaj Bjorner 2024-10-14 14:32:33 -0700
  • ef20237edd fixes Nikolaj Bjorner 2024-10-14 11:31:34 -0700
  • 54cce7b10b restore use of value_hash Nikolaj Bjorner 2024-10-14 10:46:31 -0700
  • 62478db7d5
    Update docker-image.yml Nikolaj Bjorner 2024-10-13 19:50:56 -0700
  • f136d46fb4 bug fixes Nikolaj Bjorner 2024-10-13 19:23:05 -0700
  • 56b706ac55 fixes for #7420 #7405 Nikolaj Bjorner 2024-10-13 15:52:13 -0700
  • 04824786be fix test for new signature of flip Nikolaj Bjorner 2024-10-13 15:26:08 -0700
  • c1b9a3cc9e allow for alternating Nikolaj Bjorner 2024-10-13 13:32:56 -0700
  • 9b54254fa2 throttle save model Nikolaj Bjorner 2024-10-12 19:09:25 -0700
  • 2bd335db81 alternate Nikolaj Bjorner 2024-10-12 16:11:05 -0700
  • 609c46395f recover shift-weight loop Nikolaj Bjorner 2024-10-12 15:29:48 -0700