mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
15133 commits 23 branches 48 tags 157 MiB
Commit graph

15133 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