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

8981 commits

Author SHA1 Message Date
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
Nikolaj Bjorner bce1ee6d39 new files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 09:21:34 -07:00
Nikolaj Bjorner e4eca577f6 fix po model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 175008a6c6 adding po evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner f55e4ccc41 support indexed relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 81b1338af6 display methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 87bc4cf693 virtual -> override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner 57609e57f5 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner b46cedf647 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 8d5507008e adding cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 5536834019 add API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner e3a2168a20 e_id3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 6a9cbe1461 l -> eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 892be69d51 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 168b0bcc44 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 1e751422e1 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner f8b8d5b870 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 10ba731697 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner c714abbff2 use override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 5baef8bcf3 use for pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner 876aa01167 add sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -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
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 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