mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
11150 commits 23 branches 48 tags 157 MiB
Commit graph

9125 commits

Author SHA1 Message Date
Nikolaj Bjorner 42ac3a5363 merge with csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 19:48:45 -07:00
Nikolaj Bjorner 9566d379d6 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 19:44:56 -07:00
Nikolaj Bjorner 1ff08c45ce model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 19:36:25 -07:00
Nikolaj Bjorner bd109c4522 fix memory leak when using prime_generator as non-static object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 11:14:25 -07:00
Nikolaj Bjorner 5663aa0b16 double free 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 09:13:22 -07:00
Nikolaj Bjorner 8d3dfd36b2 initialize/finalize cooperate at top-level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 02:37:24 -07:00
Nuno Lopes 04a2cce830 don't use thread-local storage if running a single thread 2019-06-12 09:59:19 +01:00
Nikolaj Bjorner 5c05b62025 deallocate mux, fix script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 01:41:14 -07:00
Nikolaj Bjorner 921a574074 mutex allocation #2336 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-11 19:50:48 -07:00
Nikolaj Bjorner 71c38a08e5 add initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-11 19:28:08 -07:00
Nikolaj Bjorner 583098b8b0 throttle som blowup by default factor of 10 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-11 17:11:54 -07:00
Lev Nachmanson 14ff768a63 limit the size of bit vectors 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-06-11 16:40:54 -07:00
Nikolaj Bjorner 7bfb730fee fix traffic jam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-10 17:45:55 -07:00
Audrey Dutcher 6fa85ad654 Allow building python wheels with binaries from a prebuilt release 2019-06-10 16:23:26 -07:00
Christoph M. Wintersteiger 998b0ff7f4
Fixed corner-case in fp.rem encoding. Fixes #2289. 2019-06-07 18:03:51 +01:00
Nikolaj Bjorner 7255edf216 remove new_sub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-06 17:13:59 -07:00
Nikolaj Bjorner 44b0b0148b deal with warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-06 17:13:38 -07:00
Nikolaj Bjorner e731a44880
Merge pull request #2329 from Z3Prover/nomp 
Nomp
 2019-06-07 02:05:11 +02:00
Nikolaj Bjorner 82da3493ee fix printing of recursive defs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-06 13:11:46 -07:00
Nikolaj Bjorner 71009a9d02 suspend limits during assert and macro expansion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-06 11:07:57 -07:00
Nikolaj Bjorner 7c1e935bc2 rlimit mux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 22:17:09 -07:00
Nikolaj Bjorner fdfb9e4fd5 Merge branch 'master' of https://github.com/z3prover/z3 2019-06-05 16:10:31 -07:00
Nikolaj Bjorner aabc54409c change printing directires 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 16:10:22 -07:00
Nikolaj Bjorner a8b02ddb93 fix #2323 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 13:43:45 -07:00
Nikolaj Bjorner 1ca3381390 fix #2319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:42:19 -07:00
Nuno Lopes a53ff6f21c turn locks into no-ops when compiled with -DSINGLE_THREAD 2019-06-05 12:11:27 +01:00
Nuno Lopes 9b375150eb remove remaining _NO_OMP_ 2019-06-05 10:07:16 +01:00
Nuno Lopes 37882f5afa fix race condition in cooperate 2019-06-05 09:31:45 +01:00
Nikolaj Bjorner 7f74382863 capture i by value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:18 +01:00
Nikolaj Bjorner 27971e3f68 exception behavior in C++11 threads? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 9f3089b098 try with std::vector and ptr_vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner e4e60bff26 include thread in tactical 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner f5511b4174 missing include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 1f84381c4c pfor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 59330b3855 pfor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 9262908ebb mux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 2788f72bbb don't lose equalities over ite, #2317 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-04 20:32:24 -07:00
Nikolaj Bjorner 51b75a132c signed char -> int, update mk_util to catch warnings on fptest, thanks to jfc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 17:22:36 -07:00
Nikolaj Bjorner 6fdef691e5 fix #2316 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 16:37:38 -07:00
Nikolaj Bjorner 1d46d5c870 use signed char per porting issue for ARM/64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 15:53:32 -07:00
Nikolaj Bjorner cccd37101e fix #2314 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-01 20:34:58 -07:00
Bruce Mitchener a12de12515 Use const& to reduce copies. 2019-06-02 09:58:32 +07:00
Nikolaj Bjorner 62de187d02
Merge pull request #2311 from waywardmonkeys/fix-reorder-warning 
Fix -Wreorder warning.
 2019-06-02 02:57:24 +02:00
Nikolaj Bjorner 3c3e5d7f7d
Merge pull request #2313 from waywardmonkeys/fix-cppapi-comment-typo 
Fix C++ API comment typo.
 2019-06-02 02:56:52 +02:00
Bruce Mitchener 17a0d75436 Fix C++ API comment typo. 2019-06-01 15:57:56 +07:00
Bruce Mitchener 960b8566f5 Fix some unused variable warnings. 2019-06-01 15:45:17 +07:00
Bruce Mitchener 759811b308 Fix -Wreorder warning. 2019-06-01 15:44:21 +07:00
Nikolaj Bjorner 01f6489892 fix #2310 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 16:22:49 -07:00
Nikolaj Bjorner dd452e0ac1 eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 15:29:27 -07:00
Nikolaj Bjorner e79542cc68 fix #2309 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 07:46:11 -07:00
Nikolaj Bjorner f1dee935d0 remove UNREACHABLE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 17:07:00 -07:00
Nikolaj Bjorner f11cb77c3d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:15:55 -07:00
Nikolaj Bjorner 8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner fc4c162e31 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:59:28 -07:00
Nikolaj Bjorner f128398bf9 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:57:19 -07:00
Nikolaj Bjorner 48fc3d752e add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:49:19 -07:00
Nikolaj Bjorner 25c93410b1 add #2298 to regression/example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-29 07:24:42 -07:00
Nikolaj Bjorner 8f36868285 fix #2300 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 09:35:55 -07:00
Nikolaj Bjorner f99384c6a3 fix nightly regression from solve-eqs context solver addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 04:17:43 -07:00
Nikolaj Bjorner 2d0ff7d68a print literals more compactly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 15:39:35 +02:00
Nikolaj Bjorner 8243139fb0 handle div 0 cases as it is uninterpreted #1683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 07:00:56 +04:00
Nikolaj Bjorner e49e5d7145 fix #2297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 06:55:06 +04:00
Nikolaj Bjorner faf4ba8309 add check for contravariance to fix #2256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner 082a0f4df4 add get_lstring per #2286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner b2845d888e add get_lstring per #2286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner 1616427792 add cmath 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-17 23:38:14 +03:00
Nikolaj Bjorner d2dcb39c11 add smt lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-17 20:24:29 +03:00
Nikolaj Bjorner dd4b8b9ff8 select/map rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-17 00:00:00 +03:00
Nikolaj Bjorner b7f14c5875 update test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 23:48:46 +03:00
Nikolaj Bjorner 335040a4ff track dependencies in context solve 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 23:06:21 +03:00
Nikolaj Bjorner 6e3f05b986 remove useless set-activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 20:24:51 +03:00
Nikolaj Bjorner 483a973b37 add pre-processing to default tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 20:20:59 +03:00
Nikolaj Bjorner f411b3b201 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 20:18:29 +03:00
Nikolaj Bjorner 3e53b6f2db na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 19:21:00 +03:00
Nikolaj Bjorner 828e123369
Merge pull request #2283 from barcharcraz/master 
Change from CMAKE_*_DIR to PROJECT_*_DIR
 2019-05-16 19:06:26 +03:00
Charlie Barto 167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Arie Gurfinkel 6ad8b7817f Add bit2bool to list of known bv operators 2019-05-15 09:26:38 -04:00
Nikolaj Bjorner e0c3b4a77d dealing with quantifier reference counts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-14 23:05:07 +03:00
Nikolaj Bjorner f989e4eb38 fix #2276 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-14 19:20:55 +02:00
Nikolaj Bjorner c42d590db3 Merge branch 'master' of https://github.com/z3prover/z3 2019-05-14 19:05:47 +02:00
Nikolaj Bjorner 4fcc4d07ae fix #2277 fix #2221 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-14 19:05:40 +02:00
Nils Becker 1e2fe9e764 bug fix 2019-05-11 20:13:48 +02:00
Nils Becker 893e604593 generate rewrite proof object early on to avoid logging equality term twice 2019-05-11 17:34:53 +02:00
Nikolaj Bjorner 4d05a11144
Merge pull request #2264 from Nils-Becker/master 
Logging Support for Nested Quantifiers
 2019-05-09 12:02:40 +02:00
Nikolaj Bjorner fc02114bf4 fix #2242, move purify-arith down to after ite elimination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-09 11:55:00 +02:00
Nikolaj Bjorner 4ede0d9ec1 commas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-09 10:16:25 +02:00
Nikolaj Bjorner 6071797ba9 fix again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-08 12:11:43 +02:00
Nikolaj Bjorner f79dccccfe fix #2238 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-08 10:15:57 +02:00
Nikolaj Bjorner 3e059a3a3b one must answer the call of the master of compilers #2258 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 05:49:16 +02:00
Nikolaj Bjorner c012f6ea5b fix #2210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 03:09:48 +02:00
Nikolaj Bjorner cbbb77bf2c allow for string solver none and empty for #2268 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 02:32:39 +02:00
Nikolaj Bjorner 689818c8bb allow empty string theory as a configuration option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-06 17:59:02 +02:00
Nikolaj Bjorner 28ce701e17 fixing 2267 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-06 15:31:55 +02:00
Nikolaj Bjorner 16af728fbe fix #2263 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-02 23:27:35 -07:00
Nils Becker 2c40da23a2 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-05-02 20:09:06 +02:00
Nikolaj Bjorner 606754c09a fix #2262 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-30 19:04:02 -07:00
Nikolaj Bjorner bd46c52f95 fix #2257, remove unsound length constraints for str.to.int because leading digits can be 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 15:51:23 -07:00
Nikolaj Bjorner 9cb1a0f094 fix #2253 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 14:24:53 -07:00
Nikolaj Bjorner 9f1b8db870 adjust for SMTLIBification name change of set operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 14:13:23 -07:00
Nikolaj Bjorner c9b906a518 deal with python globals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 14:03:26 -07:00
Nikolaj Bjorner 92613f26b3 remove additional push/pop on fixedpoint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 13:56:16 -07:00
Nikolaj Bjorner 28773c8d5c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 13:49:44 -07:00
Nikolaj Bjorner 944ce1135b replace __debug__ by Z3_DEBUG #2225 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 13:47:53 -07:00
Nikolaj Bjorner 6af6617e36 fix #2248 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 10:39:44 -07:00
Nikolaj Bjorner e1b52c323c add quotes to install path for .net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 10:19:06 -07:00
Nikolaj Bjorner 40e329fc92 remove push/pop for fixedpoint objects from API #2249 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 10:13:15 -07:00
Nikolaj Bjorner fa88bdb075 fix #2251 thanks to Clark 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 09:44:18 -07:00
Nikolaj Bjorner 7e2afca2c6 add card operator to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-20 13:24:07 -07:00
nilsbecker bd974799fc adding #qvars to [mk-quant] log line 2019-04-20 17:41:16 +02:00
nilsbecker 1c24d340d1 fixing bug causing unbalance between [instance] and [end-of-instance] lines 2019-04-18 14:45:43 +02:00
nilsbecker 28ff338b88 sync 2019-04-17 22:39:06 +02:00
Nikolaj Bjorner aafb16e8ed remove trc from C++ and python 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-17 11:10:57 -07:00
Nikolaj Bjorner 86b98e3477 remove trc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-17 10:47:46 -07:00
Nikolaj Bjorner 502b29c424 add set-has-size to API and python bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 15:38:14 -07:00
Nikolaj Bjorner d4410d0872 address compilation warnings of unused parameters, add shorthands to set parameters on Optimize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 14:32:48 -07:00
Nikolaj Bjorner 153106a6a7 fix initialization ordering to follow declaration order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 12:43:41 -07:00
Nikolaj Bjorner 596acf26ce take second suggestion from #2234 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 10:39:34 -07:00
Christoph M. Wintersteiger c611fbeaee
Fix RoundingMode value generation in FPA theory. Fixes #2239. 2019-04-16 12:50:04 +01:00
Nikolaj Bjorner 6158ea61c8 fix tree-order, change API for special relations to produce function declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 00:04:48 -07:00
Nikolaj Bjorner b4ba44ce9d remove unused candidate function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-13 16:35:10 -07:00
Nikolaj Bjorner f0c013843f operator+ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-13 16:30:47 -07:00
Nikolaj Bjorner 1123b47fb7 bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-13 16:15:38 -07:00
Uli Schlachter ebe58f78cf lp_tokenizer: Add missing verbose print 
Three out of two places that call m_tokens.push_back() in
lp_tokenizer::parse_all() were followed by a verbose print. This commit
adds a verbose print to the third such place.

Signed-off-by: Uli Schlachter <psychon@znc.in>
 2019-04-13 15:59:30 +02:00
Philipp Paulweber 5708379ebc
MSYS2 and cmake based compilation support for clang and gcc 2019-04-12 14:56:19 +02:00
Nikolaj Bjorner 4dbccbf23a fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-11 14:11:40 -07:00
Nikolaj Bjorner 3c0e8cb182 fix model generation for tc/po 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-11 11:42:55 -07:00
Nikolaj Bjorner 6fee9b90cb fix model generation for tc/po 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-11 11:39:27 -07:00
Nikolaj Bjorner 551d72b294 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-11 04:11:23 +02:00
Nikolaj Bjorner 0d06bc5990 change to more digestible recursive function definition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 17:12:24 -07:00
Nikolaj Bjorner 82658d1bce na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 10:50:46 -07:00
Nikolaj Bjorner 9c9cd5ebf7 add tc and trc functionals for binary relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 04:12:46 +02:00
Nikolaj Bjorner 182039eb44 add tc and trc functionals for binary relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 04:12:45 +02:00
Nikolaj Bjorner ae982c5225 add tc and trc functionals for binary relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 04:12:45 +02:00
Max Zinkus 45595af665
Require verbosity=1 to log parallel tactic progress 2019-04-09 12:35:04 -04:00
Nils Becker 7ead159b2d comments for log_axiom_definitions 2019-04-09 16:54:54 +02:00
Nikolaj Bjorner 6cc82f0401 enable theory_lra on non-linear reals if configured to use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-07 07:23:32 -07:00
Nikolaj Bjorner 9e62a7834d Merge branch 'master' of https://github.com/z3prover/z3 2019-04-05 03:06:58 -07:00
Nikolaj Bjorner f1a2e875b5 fixing #2217 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-05 03:06:41 -07:00
Nikolaj Bjorner 56ac3f86a5 fix justification for implied equalities in special relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-03 17:08:10 -07:00
Nikolaj Bjorner dfd327f287 add tuple and disjoint sum shorthands 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 18:36:35 -07:00
Nikolaj Bjorner 6360798a53 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 17:40:38 -07:00
Nikolaj Bjorner ff6d703c05 add tracing, fix #2214, remove unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 12:20:55 -07:00
Nikolaj Bjorner 5fdf5b67a4 remove not 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 12:17:49 -07:00
Nikolaj Bjorner 7e7cdf3635 update dependencies in legacy build system 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 12:13:50 -07:00
Nikolaj Bjorner a9c20c96ee Merge branch 'master' of https://github.com/z3prover/z3 2019-04-01 12:10:17 -07:00
Nikolaj Bjorner 4fb867a49c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 11:57:07 -07:00
Nikolaj Bjorner 3afe081f62 fixup compiled patterns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-29 11:42:40 -07:00
Nikolaj Bjorner ebc4b93d52 update documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-29 08:41:31 -07:00
Nikolaj Bjorner 1c694fd42f sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 16:11:16 -07:00
Nikolaj Bjorner 7a6823aef1 add special relations tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 10:07:50 -07:00