mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity
19510 commits 22 branches 48 tags 156 MiB
Commit graph

19510 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 991cffb519 handle multi-arity arrays 2025-02-18 20:38:45 -08:00
Nikolaj Bjorner 674e1b8f98 remove equality check on container 2025-02-18 20:15:42 -08:00
Nikolaj Bjorner ce69b54b5f adjust select/store rule for n-ary arrays 2025-02-18 20:08:56 -08:00
Nikolaj Bjorner 42f6e1300a more review of mbp_arrays 2025-02-18 19:48:54 -08:00
Nikolaj Bjorner a4a84ed083 arrays are not necessarily unary 2025-02-18 19:13:12 -08:00
Nikolaj Bjorner a5e5a35755 code simplification 2025-02-18 19:07:58 -08:00
Nikolaj Bjorner a143ed3bff taking a look at mbp_qel for arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 16:28:49 -08:00
Nikolaj Bjorner dda60737dc updated release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 15:03:24 -08:00
Nikolaj Bjorner fb6ec7d5e7 increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 15:00:26 -08:00
Nikolaj Bjorner 30dba9bde7 use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 14:36:16 -08:00
Nikolaj Bjorner 3c47fd96cf bump timeout for jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 13:41:31 -08:00
Nikolaj Bjorner 2e008a9745 Update release.yml for Azure Pipelines 2025-02-18 13:39:41 -08:00
Nikolaj Bjorner d1575af5d2 Update nightly.yaml for Azure Pipelines 
update timeout to 90
 2025-02-17 21:45:10 -08:00
Nikolaj Bjorner 96e323384f Update azure-pipelines.yml for Azure Pipelines 
set timeout to 90 minutes to see if this helps
 2025-02-17 21:42:15 -08:00
Nikolaj Bjorner 813da35539 fix unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-17 20:36:38 -08:00
Nikolaj Bjorner f8f26788ad convert def into expression tree 
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
 2025-02-17 18:47:00 -08:00
Nikolaj Bjorner f977b48161 adjust solve_for to handle rationals 2025-02-17 13:59:23 -08:00
Nikolaj Bjorner 528efbb535 fixes to failure conditions for unification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 13:41:17 -08:00
Nikolaj Bjorner fe27ca1dd0 remove verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 13:23:56 -08:00
Nikolaj Bjorner 50f9fddfd2 Add unification based projection function 
Heuristic for EMBPR is to unify terms that occur in uninterpreted contents. Walk partitions that are pure f(t) and an impure f(s)
and attempt to unify t with s ensuring that merges from s preserves satisfiability.
 2025-02-16 13:18:21 -08:00
Nikolaj Bjorner b27a2aa7fc remove calls to removed def constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 10:13:00 -08:00
Nikolaj Bjorner a703cf81b1 replace model_ref by model* in tg_project, 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-15 19:34:52 -08:00
Nikolaj Bjorner eee96ec312 bug fixes and cleanup in projection functions 
spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
 2025-02-15 14:11:20 -08:00
Nikolaj Bjorner 0cf2b5f515 add retry, rename to optibot 2025-02-14 08:39:21 -08:00
Nikolaj Bjorner 6b9ce8638f fixes to opt-tool 2025-02-13 22:24:02 -08:00
Nikolaj Bjorner 719ea6a2a7 added ai scripts 2025-02-13 21:11:58 -08:00
Nikolaj Bjorner 9fad15e2ca adding mergeopt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-13 15:00:05 -08:00
Nikolaj Bjorner 01ba749a5d focused query to optimize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-13 10:01:34 -08:00
Nikolaj Bjorner a003139704 update description 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-13 09:59:17 -08:00
Nikolaj Bjorner 45f3ea3bf4 add treesitter functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-13 09:57:26 -08:00
Lev Nachmanson bedc95c4c7 use static_cast to avoid the warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-13 07:07:12 -10:00
Phil Clayton e6a089e63d
Fix build when Z3_API macro is non-empty (#7553) 
API function definitions are updated to be consistent with header files.
 2025-02-13 08:46:08 -08:00
Nikolaj Bjorner d10efa667a stub for treesitter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-12 19:56:33 -08:00
Nikolaj Bjorner 5c18ce8cea genai testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-12 19:55:39 -08:00
Nikolaj Bjorner 4e51af1167 update instructions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 22:05:19 -08:00
Nikolaj Bjorner 94d3c591b5 make sure ackermann works with arrays that have more than one argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 21:28:31 -08:00
Nikolaj Bjorner a3739aa934 add mycop in addition to code complete 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 20:04:52 -08:00
Nikolaj Bjorner 9ea921ba8e update spacer projection for arrays to allow ackerman reduction for non-integer arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 17:38:56 -08:00
Lev Nachmanson e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 957b177c64 set arith.lp.dio_cuts_enable_gomory to False by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5ec10e0250 address the review 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 8a9edd1aa7 fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 79e3f8ab39 disabling dio handler by default, and fix a print out 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 2131e9b4e4 more accurate work with Markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bdb8f54150 Revert "revert the term sorting" 
This reverts commit c79d4708cb.
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5ebee24850 revert the term sorting 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson f2c1fd4c14 try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson cec8dc2e6e try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3f2d2e8348 test 2025-02-11 12:23:00 -10:00
Lev Nachmanson b6701d57f9 try another sort in tightening 2025-02-11 12:23:00 -10:00