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

11001 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c69e911a79 adding po evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 16:59:13 -07:00
Nikolaj Bjorner
deb48bffe1 possible fix for #2182 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 10:35:27 -07:00
Christoph M. Wintersteiger
ce8263cf27
Merge branch 'master' of https://github.com/Z3Prover/z3 2019-03-27 17:34:40 +00:00
Christoph M. Wintersteiger
d1d49ef3a9
Fix BV-conversion of fp.roundToIntegral. Fixes #2191. 2019-03-27 17:13:00 +00:00
Nikolaj Bjorner
51a26ceb9e more segfault sources #2205, examining bit2bool internalization for #2282 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 09:50:13 -07:00
Nikolaj Bjorner
5478955199 disable cancelation during propagation at base level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 16:19:50 -07:00
Nikolaj Bjorner
fde7283bb9 support indexed relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 08:39:56 -07:00
Nikolaj Bjorner
b89cd9aea6 display methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 08:15:26 -07:00
Nikolaj Bjorner
3a7bf2cf61
Merge pull request #2206 from Bronsa/master 
fix name clash in ocaml api
 2019-03-26 08:06:47 -07:00
Nicola Mometto
9008beeb01 fix mk_quantifier signature 2019-03-26 14:33:20 +00:00
Nicola Mometto
fa97f4a626 fix name clash in ocaml api 2019-03-26 14:16:31 +00:00
Nikolaj Bjorner
8da1b024b7 fix #2205 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 04:30:29 -07:00
Nikolaj Bjorner
0ae3de9916 virtual -> override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 17:57:06 -07:00
Nikolaj Bjorner
6c96f855db include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 17:54:05 -07:00
Nikolaj Bjorner
63c63606ee include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 17:53:43 -07:00
Nikolaj Bjorner
76cd8367dc adding cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 17:51:15 -07:00
Nikolaj Bjorner
48e0626ffe add API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 17:42:27 -07:00
Nikolaj Bjorner
c4b4744ae9 e_id3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 13:13:50 -07:00
Nikolaj Bjorner
1634a21e75 l -> eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 10:43:29 -07:00
Nikolaj Bjorner
dd9aec5552 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 10:40:08 -07:00
Nikolaj Bjorner
31969b5037 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 04:43:47 -07:00
Nikolaj Bjorner
f83b32e6c3 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-25 03:36:30 -07:00
Nikolaj Bjorner
e4bf1663b6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 20:47:02 -07:00
Nikolaj Bjorner
ceb4c985bf tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 20:21:22 -07:00
Nikolaj Bjorner
4603c647a7 use override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 19:21:54 -07:00
Nikolaj Bjorner
0fa4aaa625 use for pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 19:10:30 -07:00
Nikolaj Bjorner
3125c19049 add sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 18:44:46 -07:00
Nikolaj Bjorner
5c67c9d907 print certificate for #2202, enable CTL-C for API fix #2203 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 17:09:02 -07:00
Nikolaj Bjorner
0a0b0a5cc0 fix python doc regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 13:22:35 -07:00
Nikolaj Bjorner
32164b6c7f fix python doc regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 13:10:11 -07:00
Nikolaj Bjorner
cdc89b6193 add get-info :rlimit option to cmd-context to facilitate timeout based repros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 12:57:08 -07:00
Nikolaj Bjorner
dc0e9c1919 completing user print experience with seq/re #2200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 11:46:36 -07:00
Nikolaj Bjorner
fca8ffd948 fix #2199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-23 16:37:50 -07:00
Nikolaj Bjorner
604c9d38dc don't overwrite last search failure, #2198 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-23 12:54:18 -07:00
Nikolaj Bjorner
489577feba Merge branch 'master' of https://github.com/z3prover/z3 2019-03-22 13:35:24 -07:00
Nikolaj Bjorner
a74ac93bcc fix #2196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 13:34:31 -07:00
Nikolaj Bjorner
3c8fd83c97 implementing last-index-of #2089 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 12:29:50 -07:00
Nikolaj Bjorner
62ec02e50f extend rewriting features for arrays, #2151 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 12:29:50 -07:00
Lev Nachmanson
e59d60fbbe Remove unnecessary null pointer checks 2019-03-22 10:47:11 -07:00
Lev Nachmanson
61ac006cbe Remove unnecessary null pointer checks 2019-03-22 10:32:33 -07:00
Lev Nachmanson
6e5d0b7594 Remove unnecessary null pointer checks 2019-03-22 09:43:34 -07:00
Lev Nachmanson
eae4fd6afd fix the build lp.cpp in test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Lev Nachmanson
885d640301 make explicit rational(double)constructor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Nikolaj Bjorner
057151c7a8 fix #2188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-18 07:56:25 -07:00
Nikolaj Bjorner
93a4afe5d2 add multi-argument select for C# 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:36:29 -07:00
Nikolaj Bjorner
d953bdd2e4 add multi-argument select for C# 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:35:03 -07:00
Nikolaj Bjorner
9bc4914268 add nth remapping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:32:28 -07:00
Nikolaj Bjorner
834cf962a1 expose nth over API, change _getitem_ in python bindings to use nth instead of at, add 'at' operator for the purpose of the previous semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:23:01 -07:00
Nikolaj Bjorner
f534f79a21 include all sorts from declarations, and include sorts from datatypes #2185 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 18:16:09 -07:00
Nikolaj Bjorner
957c3be02f build errors/warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 16:52:18 -07:00