mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
15083 commits 23 branches 48 tags 156 MiB
Commit graph

15083 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner d03fdf5fed more descriptive naming convention 2021-03-15 15:48:33 -07:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner f00db08221 unused, thanks to AVJ 2021-03-15 13:49:17 -07:00
Nikolaj Bjorner 9098084217 reduce overhead of creating seq-plugin, enable parameter cleanup for #5095 2021-03-15 11:54:44 -07:00
Nikolaj Bjorner d62f6c62b5 fix #5096 fix #5099 2021-03-15 09:43:34 -07:00
Nikolaj Bjorner 18143d8932 fix #5102 2021-03-15 01:01:33 -07:00
Nikolaj Bjorner 1cb0dbae51 missing dependency for python build 2021-03-14 20:45:30 -07:00
Nikolaj Bjorner 845ba7a11e use a large delay for nlsat 2021-03-14 19:14:44 -07:00
Nikolaj Bjorner 155738088f fix internalization on post-visit, increase delay to 100 2021-03-14 17:20:39 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner 9a975a4523 array solver fixes 2021-03-13 06:19:32 -08:00
Nikolaj Bjorner 78f4513441 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-13 06:19:31 -08:00
Murphy Berzish 04ac5f03f7
z3str3: use improved substr axioms from seq_axioms (#5097) 2021-03-12 14:51:16 -06:00
Andrew V. Jones e8917a1a9f
Correcting 'String' to 'STRING' to resolve CMake warning (#5091) 
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
 2021-03-09 15:14:57 -08:00
Nikolaj Bjorner e08ceee424 compiler 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-08 20:41:10 -08:00
Nikolaj Bjorner 857557ad93 deal with compiler warnings 2021-03-08 20:39:19 -08:00
Nikolaj Bjorner 88fbf6510f updates to theory_lra 2021-03-08 17:19:07 -08:00
Nikolaj Bjorner f29a596070 deal with compiler warnings, from MacOS CI build 2021-03-08 17:14:09 -08:00
Nikolaj Bjorner 7eceeff349 move branch of unit variable 2021-03-08 10:09:04 -08:00
Nikolaj Bjorner 3c26a965e1 updated script, add comment to mk_eq_empty 2021-03-07 06:59:58 -08:00
Nikolaj Bjorner 7edc99f807 na 2021-03-06 12:36:19 -08:00
Nikolaj Bjorner 8de96009cd na 2021-03-06 12:36:19 -08:00
Nikolaj Bjorner e83f31949e fix #5074, add rewrite rules to simplify indexof special cases 2021-03-06 12:36:19 -08:00
Graydon Hoare e8b3c90e14
Fix unintentional re-import of package z3 in z3printer, in python3. (#5082) 2021-03-06 10:44:07 -08:00
Nikolaj Bjorner 8d54e83567 updated hitting set sample 2021-03-06 10:18:52 -08:00
Nikolaj Bjorner e804f7743a
Revert "Adjust imports so z3.z3 is still available in python3 (#5079)" (#5081) 
This reverts commit 957d7bfe35.
 2021-03-05 15:26:00 -08:00
Nikolaj Bjorner ea181fe8b2 more useful trace 2021-03-05 15:01:40 -08:00
Nikolaj Bjorner 5f0ec936e4 count final checks 2021-03-05 15:01:39 -08:00
Nikolaj Bjorner 022a1fd3dd fix #5080 assertion is violated on legal input, add an example 2021-03-05 15:01:39 -08:00
Graydon Hoare 957d7bfe35
Adjust imports so z3.z3 is still available in python3 (#5079) 2021-03-04 17:18:39 -08:00
Nikolaj Bjorner 38737db802 fixes and more porting seq_eq_solver to self-contained module 2021-03-04 16:23:22 -08:00
Nikolaj Bjorner 847724fb21 added rewrite for itos 2021-03-04 10:47:47 -08:00
Nikolaj Bjorner e398959732 move eq solver functionality to common place, fixes to goal2sat 2021-03-04 07:57:31 -08:00
Nikolaj Bjorner cf3002c293 fix #5071 2021-03-03 23:13:56 -08:00
Nikolaj Bjorner 79ababb00a force push 2021-03-03 11:38:33 -08:00
Nikolaj Bjorner 69070a7486 align translation cache with scopes and variable elimination 2021-03-03 11:22:17 -08:00
Nikolaj Bjorner 11efe33aa0 fix #5061 2021-03-03 11:19:03 -08:00
Nikolaj Bjorner 8c66691e6d disable propagation in proof mode as it produces ill-formed proof objects. Fixes #5063 2021-03-03 09:51:56 -08:00
Nikolaj Bjorner bef6f1a729 fix build 2021-03-02 13:51:58 -08:00
Nikolaj Bjorner a66362a933 missing new files 2021-03-02 13:00:17 -08:00
Nikolaj Bjorner 0ce1c34d81 fix #5065 - regression solving str.from_int equations now that it isn't injective any longer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-02 12:59:48 -08:00
Nuno Lopes 4c9fed21e2
increase starting size of ast's hash table to 512k entries (instead of 8) (#5040) 2021-03-02 11:45:07 -08:00
Nikolaj Bjorner 56478f917b enable sat.euf in opt, enable smt legacy for lns 2021-03-02 06:21:20 -08:00
Nuno Lopes db04ccb137 scoped_timer: skip extra unneded heap allocation 2021-03-01 14:36:22 +00:00
Nuno Lopes fc558d3946 fix #5059: exit straight away on hard timeout 
dont run atexit handlers as its not safe to do so with multiple threads
code might be inside malloc, for example, and glibc tries to cleanup its heap
state with an atexit handler
 2021-03-01 14:34:41 +00:00
Nikolaj Bjorner 484c83e6c0 revert enum split for legacy solver 2021-03-01 04:13:17 -08:00
Nuno Lopes ff1429413d Z3_subst: avoid unneded cache lookups 2021-03-01 11:14:24 +00:00
Nikolaj Bjorner f725989225 optimize for enumeration datatypes 2021-02-28 21:31:21 -08:00
Nikolaj Bjorner caae0ba569 rename statistics to pb 2021-02-28 21:31:21 -08:00
Nuno Lopes 5b24396ecd Z3_subst: add fast path for quantifier subst 
when replace patterns are ground
 2021-02-28 23:09:52 +00:00