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

9258 commits

Author SHA1 Message Date
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
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
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
Nikolaj Bjorner 36a2052cca update to TWEAK 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 15:46:48 -07:00
Nikolaj Bjorner 340f30c41d Merge branch 'master' of https://github.com/z3prover/z3 2019-03-14 18:22:49 -07:00
Nikolaj Bjorner 7b50fca02c display dimacs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 18:22:42 -07:00
Andrew Helwer 0a477a0a93
Remove dependency on TargetPlatform macro 
Unnecessary, since dropping support for x86
 2019-03-14 15:46:03 -07:00
Nikolaj Bjorner 038f992ff4 remove platformtarget for dotnetcore spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 12:48:27 -07:00
Nikolaj Bjorner 90b78eb64a use random_next instead of library random 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-13 19:59:05 -07:00
Nikolaj Bjorner c499bd4116
Merge pull request #2180 from levnach/Prover 
snap variables to bounds when maximizing terms
 2019-03-13 19:09:40 -07:00
Nikolaj Bjorner d642ed5591 adding targets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-13 18:03:18 -07:00
Lev Nachmanson f336039da3 snap variables to bounds when maximizing terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-13 15:28:50 -07:00
Nikolaj Bjorner 75b1e8fe27 add tracing for 2157 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-12 20:12:17 -07:00
Nikolaj Bjorner 519e83bce4 Merge branch 'master' of https://github.com/z3prover/z3 2019-03-12 19:07:59 -07:00
Nikolaj Bjorner 8f1c5239be updates for #2151 #2152 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-12 13:39:57 -07:00
Nikolaj Bjorner 05663592ee fix #2173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-10 14:42:00 -07:00
Nikolaj Bjorner 376076ea9b Merge branch 'master' of https://github.com/z3prover/z3 2019-03-09 19:31:37 -08:00
Nikolaj Bjorner 5bc0fb47a8 fix #2169 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-09 19:31:30 -08:00
Nuno Lopes 9736c46375 constify is_threaded if MT is disabled 2019-03-08 11:16:10 +00:00
Nuno Lopes cd4b53500c avoid a few str copies + symbol hiding 2019-03-08 10:13:46 +00:00
Nikolaj Bjorner c7bbf2f8de Merge branch 'master' of https://github.com/z3prover/z3 2019-03-07 00:07:54 -08:00
Nikolaj Bjorner 9d2a106838 unused variable warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-07 00:07:48 -08:00
Nikolaj Bjorner f7773fdcc8 rewrite quantifiers in model evaluator #2171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 22:04:31 -08:00
Nikolaj Bjorner 5abc4a6d68 rewrite quantifiers in model evaluator #2171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 22:03:57 -08:00
Nikolaj Bjorner 65f0da9806
Merge pull request #2170 from mtrberzi/issue2092 
z3str3: fix str.indexof with offset (issue #2092)
 2019-03-06 17:36:46 -08:00
Nikolaj Bjorner de7731fd22
Merge pull request #2167 from Egor18/master 
Fix misprint
 2019-03-06 17:36:28 -08:00
Nikolaj Bjorner 5a02edc8cd add recognizer for distinct 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 10:18:29 -08:00
Murphy Berzish e05596e7e5 z3str3: fix str.indexof with offset (issue #2092) 2019-03-06 11:41:56 -05:00
Egor Bredikhin 21be4e6d16
Fix misprint 2019-03-05 17:09:27 -05:00
Nikolaj Bjorner f00697cf95 fix #2155 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 22:33:28 -08:00
Nikolaj Bjorner 26921d1c9c fix #2155 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 22:32:50 -08:00
Nikolaj Bjorner 5c13acbf9f remove print directive that doesn't compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 20:48:13 -08:00
Nikolaj Bjorner 0c0e79a937 add logging to lar-solver to capture state for unbounded optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 20:33:12 -08:00
Nikolaj Bjorner 19e7b75536 set status optimal also on object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 19:31:51 -08:00
Nikolaj Bjorner 7aa8b4ac2a restrict idiv-bound checks to bounded terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 19:11:22 -08:00
Nikolaj Bjorner 752ac09fee fix #2161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 14:30:59 -08:00
Nikolaj Bjorner 7b4c919fcf stubs for stronger array equality rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 14:11:05 -08:00
Nikolaj Bjorner 6c331279ae fix array regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 13:22:12 -08:00
Nikolaj Bjorner 8b261df77a Merge branch 'master' of https://github.com/z3prover/z3 2019-03-03 13:10:16 -08:00
Nikolaj Bjorner e51b5fd99c fix t154 regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 13:10:11 -08:00
Nikolaj Bjorner 3723c1af0a
Merge pull request #2166 from levnach/Prover 
fixes in indices in lar_solver::maximize_term()
 2019-03-03 13:00:51 -08:00
Lev Nachmanson 06725de477 fixes in indices in lar_solver::maximize_term() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-03 10:57:25 -10:00
Nikolaj Bjorner 8e812ea239 revert fix for #2164 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:51:26 -08:00
Nikolaj Bjorner 7399f78dfd disable model compression for regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:40:59 -08:00
Nikolaj Bjorner 3ee5c0e7d9 fix #2164 address some of simplification shortcommings from #2151 #2152 #2153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 11:33:44 -08:00
Nuno Lopes ccc170a06e model evaluator: cleanup cache when model_eval param changes 2019-03-02 16:42:18 +00:00
Nikolaj Bjorner 210e448666
Merge pull request #2163 from levnach/Prover 
enable lar_solver::constraint_holds
 2019-03-01 08:37:06 -08:00
Nikolaj Bjorner 006590f329 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 14:29:20 -08:00
Nikolaj Bjorner a2dddbd7a5 check pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 14:28:03 -08:00
Lev Nachmanson 69f03952a7 enable lar_solver::constraint_holds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-02-28 12:11:34 -10:00
Nikolaj Bjorner e76cea4684 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 11:44:45 -08:00
Nikolaj Bjorner 6d9b746e70 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 11:42:48 -08:00
Nikolaj Bjorner 69d7d8ff87 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 11:42:17 -08:00
Nikolaj Bjorner 5fa5719c6f fix #2159 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 08:58:58 -08:00
Nikolaj Bjorner b632c08fe0 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 08:35:26 -08:00
Nikolaj Bjorner 4c76d43670 add binary_merge encoding option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 08:35:22 -08:00
Nuno Lopes 6a0c409b0f move a few strings instead of copying 2019-02-28 10:53:27 +00:00
Nikolaj Bjorner e79f7ca1fd
Merge pull request #2150 from Nils-Becker/master 
Logging Support for Theory Solvers
 2019-02-27 17:06:31 +01:00
Nikolaj Bjorner ea9e2f6642 fix #2158 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-26 15:13:47 -08:00
Nikolaj Bjorner c4ee4ffae4 fix pre-prejection> 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-26 07:12:34 -08:00
Nikolaj Bjorner bef509b02e Yakir! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 19:20:35 -08:00
Nikolaj Bjorner d9b4f237fe remove opt dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:18:19 -08:00
Nikolaj Bjorner 46f3b7374c Merge branch 'master' of https://github.com/z3prover/z3 2019-02-25 18:15:28 -08:00
Nikolaj Bjorner 4876426866 project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:15:24 -08:00
Nikolaj Bjorner 15d5be66b6 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-25 18:14:47 -08:00
Nikolaj Bjorner 4ff940a29e mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:14:41 -08:00
nilsbecker 17adecff68 fixing ci issues 
fixing if condition
 2019-02-25 19:10:47 +01:00
Nikolaj Bjorner 6ef3e5e363 integrate some self-contained fixes from #2147 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-24 14:21:34 -08:00
Nikolaj Bjorner 142f3638cf spaces 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-23 22:45:39 +01:00
Nikolaj Bjorner 53b5e1f824
Merge pull request #2148 from danielschemmel/warnings 
Fix three Warnings
 2019-02-23 22:45:04 +01:00
nilsbecker 960708e99e Merge branch 'master' of https://github.com/Z3Prover/z3 2019-02-23 12:34:40 +01:00
nilsbecker c033fb045f 2 things I prevoiusly overlooked 2019-02-23 12:34:17 +01:00
nilsbecker 6ee3941523 more cleanup 2019-02-23 12:08:08 +01:00
Daniel Schemmel 36643aafd2
fix -Wmisleading-indentation 2019-02-23 11:34:33 +01:00
Nikolaj Bjorner 773c613694 fix #2149 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-23 11:10:01 +01:00
Nikolaj Bjorner c0d20f8ea8 add cr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-23 10:59:10 +01:00
Daniel Schemmel c2ebbc9210
fix -Wsign-compare (len can never become negative anyway) 2019-02-23 10:57:41 +01:00
Nikolaj Bjorner 28c675f56e
Merge pull request #2146 from danielschemmel/buffer-1 
Buffer and Vector Modernization Part 1
 2019-02-23 10:55:08 +01:00
nilsbecker a8586746be cleanup for pull request 2019-02-23 02:47:33 +01:00
nilsbecker 6e508d4221 fixing Windows compile issue 2019-02-22 14:09:35 +01:00
Nikolaj Bjorner 72d59ea00a Merge branch 'master' of https://github.com/z3prover/z3 2019-02-22 13:57:18 +01:00
Nikolaj Bjorner 73060ecaec remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-22 13:57:09 +01:00
Christoph M. Wintersteiger 699834261e
Fix translation of FPA numerals in ast_smt_pp. Fixes #2145. 2019-02-22 12:55:01 +00:00
Nikolaj Bjorner bceff4b3fa Merge branch 'master' of https://github.com/z3prover/z3 2019-02-22 11:17:03 +01:00
Nikolaj Bjorner 4c799c144a fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-22 11:14:20 +01:00
nilsbecker ec76efedbe synchronizing with main repository 2019-02-22 00:19:43 +01:00
nilsbecker 28c03ed1de logging support for theory axioms 2019-02-21 19:29:35 +01:00
Nuno Lopes bb7aa16223 stopwatch: fix debug build crash in sat solver 2019-02-21 16:38:48 +00:00
Nuno Lopes 6598aedbb2 fix VS build, take 2 2019-02-21 15:52:52 +00:00
Nuno Lopes 3d7878bafc hopefully fix build with VS 2012 2019-02-21 15:25:26 +00:00
Nuno Lopes 2f33bafd5a stopwatches: fix a few places that would call start/stop multiple times 2019-02-21 14:59:31 +00:00
Daniel Schemmel 721ea2a8d3
Move vector.h to old_vector.h and add a shim vector.h 
To do so, one instance of the class keyword needs to be removed.
 2019-02-21 15:38:08 +01:00
Nuno Lopes 85162d90d1 simplify timer.h 2019-02-21 13:57:38 +00:00
Nuno Lopes 3a7c467822 fix debug build.. 2019-02-21 13:33:52 +00:00
Nuno Lopes 3a5263be95 modernize stopwatch 2019-02-21 13:30:27 +00:00
Daniel Schemmel 2ff2e77739
Move buffer.h to old_buffer.h and add a shim buffer.h 2019-02-21 13:05:58 +01:00
Nuno Lopes a76c0fbbfb simplify timeout mechanism and fix race conditions there 2019-02-21 11:49:41 +00:00
Nuno Lopes f3cd7d646d further simplifications to scoped_timer 2019-02-21 10:42:42 +00:00
Nikolaj Bjorner 598fc810b5 adding FP 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 15:34:47 +01:00
Nikolaj Bjorner 3548057bd1 fix detection of arithmetic operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 14:00:05 +01:00
Nikolaj Bjorner cc216f8cc3 fix regressions breaking build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 21:24:44 +01:00
Nikolaj Bjorner c022d47d60 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-19 18:17:17 +01:00
Nikolaj Bjorner caa15ea04d enable cardinality constraints in nla2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 18:17:07 +01:00
Nuno Lopes 61272fdc0c remove a few more inc/dec refs 2019-02-19 13:36:39 +00:00
Nuno Lopes edf0df634d simplifications to refs 2019-02-19 13:18:20 +00:00
Nuno Lopes 8e4ef19f45 fix debug build 2019-02-19 10:54:41 +00:00
Nuno Lopes 8c2584bcf7 eliminate a few ref incs/decs plus remove unused variable 2019-02-19 10:52:12 +00:00
Nikolaj Bjorner 2138a5232f fix #2142 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 10:16:50 +01:00
Nikolaj Bjorner 7fb2c6a908 turn off model validation unless specified by parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:55:24 +01:00
Nikolaj Bjorner 0aafa8b7ce optimize binary output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:52:42 +01:00
Nikolaj Bjorner 5b57c6b780 unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-17 01:30:26 -08:00
Nikolaj Bjorner 8c085f1a18 removing unused and fixing suspect optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 21:26:29 -08:00
Nikolaj Bjorner ea778eefb2 skip optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 20:58:30 -08:00
Nikolaj Bjorner c1402ad70f tone down verbosity of integrity checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 20:39:15 -08:00
Nikolaj Bjorner 7f51cc7931 fix #2140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 09:54:05 -08:00
Nikolaj Bjorner 4f223542ac fix #2129 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 09:38:47 -08:00
Nikolaj Bjorner f84de9400e also deal with initializing boolean variables in smt context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 17:58:26 -08:00
Nikolaj Bjorner 39f73fa595 ensure that activity works for sat solver from cold state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 16:56:55 -08:00
Nikolaj Bjorner 89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner e4c6dcd84c import csp progress 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:09:18 -08:00
Nikolaj Bjorner 45aa8dd39a remove more references 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:06:38 -08:00
Nikolaj Bjorner 96c05b0289 remove reference to deprecated code in cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:00:02 -08:00
Nikolaj Bjorner 5cdfa7cd1c variations on unit-walk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-13 17:43:15 -08:00
Nikolaj Bjorner 83f0fd5cc2 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-12 15:49:20 -08:00
Nikolaj Bjorner eec1da5a15 move restart test to after propagation, clean up drat generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-12 15:49:12 -08:00
Christoph M. Wintersteiger 64d085c188
Fix bug in fpa2bv_converter, fixes #2136. 2019-02-12 14:02:30 +00:00
Nikolaj Bjorner d9a51f8f8a fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 14:44:12 -08:00
Nikolaj Bjorner 72b220e84a import improvements to lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:28:13 -08:00
Nikolaj Bjorner 6d893e0599 revise unit walk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:16:17 -08:00
Nikolaj Bjorner 5fe40a25dc revise local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:14:20 -08:00
Nikolaj Bjorner 22783a4bcb import more from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:09:28 -08:00
Nikolaj Bjorner 93ee05648e add shortcuts for unit assertions, conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 10:56:36 -08:00
Nikolaj Bjorner d73b7267e3 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-10 18:11:08 -08:00
Nikolaj Bjorner 6cfe66c3c2 re-enabling model evaluation of as-array after tuning normalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 18:11:01 -08:00
Audrey Dutcher 4e687671a5 Tweak python setup.py clean to properly clean the native build 2019-02-10 14:32:02 -08:00
Audrey Dutcher b702cad81e Append std=c++11 instead of replacing CXXFLAGS; see #2130 2019-02-10 14:12:27 -08:00
Nikolaj Bjorner 81d322b79f fix bug in model compression that skips dependencies in function entries. Exposed in t171.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 11:12:26 -08:00
Nikolaj Bjorner c5df6ce96e fix #2131 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 10:07:24 -08:00
Nikolaj Bjorner 24dfdfe9bc disable fixes for #2128 and related as it breaks model evaluation time in regressions, set longer delay for inprocessing in sat solver, report stats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 16:06:02 -08:00
Nikolaj Bjorner c7bd985fac remove asserts for ground defs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:50:02 -08:00
Nikolaj Bjorner 0fd4c4fb06 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:24:14 -08:00
Nikolaj Bjorner d2d42f9810 fix #2127 fix #2128 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:23:22 -08:00
Nikolaj Bjorner b17c946acb fix bug in hoist module, tune num2bits for large bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-08 14:40:06 -08:00
Nikolaj Bjorner d2a3b53d92 fix remaining incorrect uses of new BoolExpr related to #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 12:28:17 -08:00
Nikolaj Bjorner 77942a35dc fix #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 11:20:53 -08:00
Nikolaj Bjorner d21fc642b4 refactor watch_diseq, disable it completely 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 09:57:24 -08:00
Nikolaj Bjorner 6f9082598c tuning relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 08:05:40 -08:00
Nikolaj Bjorner e22f713b19 tune QF_UFBV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 12:02:48 +01:00
Nikolaj Bjorner c9ffe7417c mark destructors virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 07:55:17 +01:00
Nikolaj Bjorner 064c9faf11 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 20:13:21 +01:00
Nikolaj Bjorner c6a7dc7b44 formatting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 20:05:45 +01:00
Nikolaj Bjorner 6c10e27bd5 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-06 19:43:56 +01:00
Nikolaj Bjorner 56598037b6 new rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:40 +01:00
Nikolaj Bjorner d04e72819a abstract solver API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:01 +01:00
Nuno Lopes 904bc34139 remove some debug leftover 2019-02-05 10:02:58 +00:00
Nuno Lopes 73f6806371 rewrite scoped_timer in C++11 way 
the code is much smaller and reused across platforms
I see a small speedup on linux as well
 2019-02-04 17:42:27 +00:00
Nikolaj Bjorner 9cf99e26a6 fix #2123 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 19:54:08 +01:00
Nikolaj Bjorner 0acc042bf7 fix #2120 fix #2122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 17:15:38 +01:00
Nikolaj Bjorner 9fde9fe3a2 fix #2122 for code that isn't exception safe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-02 19:49:16 +01:00
Nikolaj Bjorner a76107e50d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 18:44:52 -08:00
Nikolaj Bjorner 6c464f8aec add assert_and_track to optimize for #2116 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 14:59:36 -08:00
Nikolaj Bjorner d1877f58a5 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-01 13:36:02 -08:00
Nikolaj Bjorner e07f0c0284 tune generation of drat files, add helpful binary clause in lookahead simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 13:35:54 -08:00
Daniel Selsam df73c58195 array resize must m_size 2019-02-01 09:36:03 -08:00
Daniel Selsam cca280ac47 do not echo dimacs while parsing 2019-02-01 09:36:03 -08:00
Nikolaj Bjorner 7fa9768c36 improving drat output perf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 09:16:46 -08:00
Nikolaj Bjorner 1e90be62bc fix drat for lookahead, fixes for binary drat format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-31 14:58:51 -08:00
Nikolaj Bjorner cda78d8d0b #2117 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:34:45 -08:00
Nikolaj Bjorner cb94f82f37 fix #2118 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:31:05 -08:00
Nikolaj Bjorner e004986e99 fix z3++.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:20:38 -08:00
Nikolaj Bjorner 35eb21bc35 fix extraction of trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:06:41 -08:00
Nikolaj Bjorner 08ce6f7ac1 working on binary drat format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 08:54:59 -08:00
Nikolaj Bjorner 8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner e22c657811 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-29 10:50:28 -08:00
Nikolaj Bjorner 58f5531cff fix #2114 introduced while working on #2095 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 08:18:03 -08:00
Nikolaj Bjorner 4f988595c7 fix #2107 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 19:45:19 -08:00
Nikolaj Bjorner 94dae2da3a fix fourth bug produced by repros by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 18:11:18 -08:00
Nikolaj Bjorner d0b2f73c0c change opt.maxlen.enable default to true to prefer this over all other heuristics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-26 13:02:25 -08:00
Nikolaj Bjorner 1297eeb817 fix #2104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-26 11:55:32 -08:00
Nikolaj Bjorner cf6119cdfd fix #2102 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 21:02:25 -08:00
Nikolaj Bjorner e7cabf3e44
Merge pull request #2103 from alcides/master 
Deepcopy works with Python 3.7
 2019-01-25 20:07:40 -08:00
Nikolaj Bjorner 121211a51c maxlexN 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 20:01:38 -08:00
Nikolaj Bjorner 1ed68906fa fix debug assertion code, make maxlex optional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 08:23:41 -08:00
Alcides Fonseca 83717a9c86 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-01-25 14:45:22 +00:00
Alcides Fonseca a785ffe0ba Updated deepcopy to the latest Python API 2019-01-25 14:42:22 +00:00
Nikolaj Bjorner d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner b4f4a1f316 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:47:50 -08:00
Nikolaj Bjorner ad81fee118 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:26:44 -08:00
Nikolaj Bjorner 8da1d6070b throttle big-reductions #2101 #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 14:00:56 -08:00
Nikolaj Bjorner 498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner f7746e2284 address perf #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:58:00 -08:00
Nikolaj Bjorner 9c07167ff8 add new pyg file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:44 -08:00
Nikolaj Bjorner 8e5c1fcfd1 make context_solve configurable and exposed as top-level tactic parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:25 -08:00
Nikolaj Bjorner 412eee0dac throttle number of rounds of ba simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 18:12:39 -08:00
Nikolaj Bjorner f9195c77a7 remove not-handled clause from mod with non-numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 09:46:04 -08:00
Nikolaj Bjorner 49a51a0757 fix #2096, introduced when fixing #2082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 07:06:40 -08:00
Nikolaj Bjorner 6bd87f837a fix Boolean argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 14:14:26 -08:00
Nikolaj Bjorner 8566d88b99 remove validation assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:49:04 -08:00
Nikolaj Bjorner 785fe2f6f7 add main remaining updates from #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:43:05 -08:00
Nikolaj Bjorner 5cdbb1f7be this is still used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:25:34 -08:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner cabe0ee447 integrating additional changes from @yatli pull request #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:51:44 -08:00
Nikolaj Bjorner 1efbc25b3b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-18 18:09:22 -08:00
Nikolaj Bjorner 0b7021d2c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 18:09:19 -08:00
Nikolaj Bjorner c45ab6efed add setting to dump intermediary models #2087 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 15:12:08 -08:00
Nikolaj Bjorner 947fe2ff9c fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:35:07 -08:00
Nikolaj Bjorner 442e47dfce fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:34:26 -08:00
Nikolaj Bjorner f2e636c598 record simplified input clauses as lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 16:37:21 -08:00
Nikolaj Bjorner 247980c5a2 don't assign already assigned literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 11:41:32 -08:00
Nikolaj Bjorner 038971c029
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
Nikolaj Bjorner 16c15d53a9
Merge pull request #1815 from yatli/master 
api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration.
 2019-01-16 10:16:26 -08:00
Nikolaj Bjorner e01a668da0 coordinate drat with clause removal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 02:29:33 -08:00
Nikolaj Bjorner b33f5f879e fix another bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 17:57:11 -08:00
Nikolaj Bjorner 3298486136 don't reach max conflicts if state is inconsistent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:40:38 -08:00
Nikolaj Bjorner 5328454c77 const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:37:23 -08:00
Nikolaj Bjorner 161c83795f remember inconsistent states when cloning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:34:55 -08:00
Nikolaj Bjorner 65bd427e46 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:48:48 -08:00
Nikolaj Bjorner f238460597 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:45:04 -08:00
Nikolaj Bjorner ed7cac8cc0 neatify logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:42:13 -08:00