mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
15069 commits 49 branches 53 tags 182 MiB
Commit graph

3668 commits

Author SHA1 Message Date
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
7edc99f807 na 2021-03-06 12:36:19 -08:00
Nikolaj Bjorner
ea181fe8b2 more useful trace 2021-03-05 15:01:40 -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
e398959732 move eq solver functionality to common place, fixes to goal2sat 2021-03-04 07:57:31 -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
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
Nikolaj Bjorner
56478f917b enable sat.euf in opt, enable smt legacy for lns 2021-03-02 06:21:20 -08:00
Nikolaj Bjorner
484c83e6c0 revert enum split for legacy solver 2021-03-01 04:13:17 -08:00
Nikolaj Bjorner
f725989225 optimize for enumeration datatypes 2021-02-28 21:31:21 -08:00
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner
5c47f244e9 fix #5047 2021-02-26 03:37:14 -08:00
Nikolaj Bjorner
ea1089e980 fix #4938 2021-02-26 02:06:28 -08:00
Murphy Berzish
56e4ee3273
z3str3: use assert_axiom_rw more consistently (#5055) 2021-02-25 19:50:18 -06:00
Nikolaj Bjorner
64ba0b631a fixes to seq solver 2021-02-25 10:35:14 -08:00
Nikolaj Bjorner
377d060036 move to separate axiom management 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-23 18:09:45 -08:00
Murphy Berzish
9bde93f812
z3str3: check whether rewritten axioms rewrite to TRUE (#5039) 2021-02-23 10:36:14 -06:00
Murphy Berzish
5599387a34
z3str3: add str.is_digit support (#5038) 2021-02-23 10:36:01 -06:00
Nikolaj Bjorner
d9fb40602e use theory agnostic axioms in more cases 2021-02-21 18:36:53 -08:00
Nuno Lopes
e773e1e78d fix a few more warnings 2021-02-19 12:16:05 +00:00
Nuno Lopes
d6ce9cce95 fix clang warnings 2021-02-19 10:59:22 +00:00
Nikolaj Bjorner
a22fb8a96e revert unit propagation of equality literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 23:11:03 -08:00
Nikolaj Bjorner
27584d68db more rewrite rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 22:14:53 -08:00
Murphy Berzish
27db97c269
Z3str3: add str.to_code and str.from_code (#5015) 2021-02-18 16:51:34 -06:00
Nikolaj Bjorner
ca9fcbd1df na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 13:46:59 -08:00
Nikolaj Bjorner
4f9117a921 Move seq axioms to theory independent module 2021-02-16 05:13:52 -08:00
Nikolaj Bjorner
823830181b butterfly effect with relevancy marking 
bail out of infinite instantiation loop
 2021-02-15 16:37:23 -08:00
Nikolaj Bjorner
a6dce246f6 fix #5031 2021-02-15 14:36:01 -08:00
Nikolaj Bjorner
c387863da1 fix #5032, reset substitution during fold transformation 2021-02-15 14:14:25 -08:00
Nikolaj Bjorner
70b4822571 patch seq theory using purification to avoid unsoundness caused by interaction with canonization and rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-14 17:41:06 -08:00
Nikolaj Bjorner
eac69c5504 incorrect axiomatization 
Fixes repro in https://github.com/Z3Prover/z3/issues/4866#issuecomment-778706682
 2021-02-14 15:29:10 -08:00
Nikolaj Bjorner
45af1bd243 fix build, move seq_skolem 2021-02-14 14:40:29 -08:00
Nikolaj Bjorner
083d09aa81 fix #5016 2021-02-14 13:52:10 -08:00
Nikolaj Bjorner
83f4a006c6 wreckfun 2021-02-12 19:46:47 -08:00
Nikolaj Bjorner
612cc5cfba fix #5014 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-12 16:01:33 -08:00
Nikolaj Bjorner
998cf4c726 fix #5020 
comparison for strict neighbor relation seemed reversed.
Alas, this could introduce additional regressions
 2021-02-12 12:24:27 -08:00
Nikolaj Bjorner
25f53c0467 deal with warnings reported in https://launchpadlibrarian.net/522361319/buildlog_ubuntu-groovy-s390x.z3_4.8.10-1ubuntu4ppa1_BUILDING.txt.gz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 13:49:47 -08:00
Nikolaj Bjorner
5c04b9eee2 fix #5012 
teething stage for from/to code axiomatization
 2021-02-09 16:38:03 -08:00
Nikolaj Bjorner
8ca2de41db turn on from/to code handling #5007 samples 2021-02-09 10:00:08 -08:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
0ec567fe15 integrate v2 of lns 2021-02-04 15:47:40 -08:00
Nikolaj Bjorner
fb1509d011 expose internal API for set_phase 2021-02-02 14:29:06 -08:00
Nikolaj Bjorner
8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner
3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
4455f6caf8 move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail 2021-02-02 03:58:19 -08:00