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

5569 commits

Author SHA1 Message Date
KangJing Huang (Chaserhkj) 5799947183 Fix docstrings for FuncDecl.translate 2017-06-13 02:37:41 -04:00
KangJing Huang (Chaserhkj) 3a692fe33c Add translate method for FuncDecl in java api 2017-06-13 00:37:02 -04:00
Nikolaj Bjorner 2de80b5ce9 add pb built in ops for logic ALL #1045 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 10:08:50 -07:00
Nikolaj Bjorner d95ac58bad remove throw in reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 12:09:35 -07:00
Nikolaj Bjorner f80a622a8f add colon to assertion stack levels #1046 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 11:10:46 -07:00
Nikolaj Bjorner 1654ad7059 adding escape characters to reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-27 14:56:38 -07:00
Nikolaj Bjorner f3a0b7e0cd change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 2017-05-23 20:05:10 -07:00
Nikolaj Bjorner 6f2cd4817b ensure arith.reflect has default true 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 14:09:45 -07:00
Nikolaj Bjorner 3f89c1418b fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:51:14 -07:00
Nikolaj Bjorner 23ff580a67 get rid of timeb dependencies, pull request #1040 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:16:43 -07:00
Nikolaj Bjorner edb164587f get rid of a simplifier dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:12:32 -07:00
Nikolaj Bjorner af4346f16a expose arith reflection, get rid of long m_manager attribute in asserted fromulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:04:29 -07:00
Nikolaj Bjorner 2834fea9b3 fix x64 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:58:21 -07:00
Nikolaj Bjorner 90af406338 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-23 08:51:38 -07:00
Nikolaj Bjorner 8e9739d3b0 work around crash #1039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:51:26 -07:00
Nikolaj Bjorner 2cbeedec69 accept hereditarily finite sorts in datalog engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 19:32:43 -07:00
Nikolaj Bjorner 622d8c951c remove redundant data-type function declarations from pretty-printed output. #1034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 14:40:42 -07:00
Nikolaj Bjorner b782ec35cc avoid print statements from assertions when the assertion does not trigger. Stackoverflow question http://stackoverflow.com/questions/44094927/creating-formula-taking-too-much-time-in-z3py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-21 10:35:59 -07:00
Ken McMillan bf7c6292bd removing FOCI2 interface from interp 2017-05-19 16:21:57 -07:00
Lev Nachmanson 1b62592015 change in a comment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-05-18 13:44:00 -07:00
Nikolaj Bjorner 79a8e9aab0 fix build break #1029 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-18 12:09:51 -07:00
Nikolaj Bjorner 4069e76ab0 remove unused column function field, #1021 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 21:27:43 -07:00
Nikolaj Bjorner ceec81de0b simplify code, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:32:08 -07:00
Nikolaj Bjorner 7fab670719 fix regression, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:21:32 -07:00
Nikolaj Bjorner d2ac59f238 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-14 14:10:01 -07:00
Nikolaj Bjorner 3290a933b5 remove spurious include file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-14 14:09:42 -07:00
Nikolaj Bjorner 22386d3727 Merge pull request #1026 from Owlz/setup_bin_fix 
Fixing z3 binary setup to data_files
 2017-05-14 14:06:16 -07:00
Nikolaj Bjorner a0efdc21c3 add missing locks around mpz operations that access object allocator. Use internal skolem constant for theory assumption to hide it from models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-14 14:04:00 -07:00
Owlz aad186f6a5 Fixing z3 binary setup to data_files 2017-05-14 15:25:17 -04:00
Murphy Berzish 3c692a37eb fix consistency check involving strings with escape characters 2017-05-13 16:13:32 -04:00
Murphy Berzish 14355a15c8 use correct operator for lower bound assignment 
fixes #1022
 2017-05-13 16:02:41 -04:00
Murphy Berzish bf147556a6 add counter to theory_str::mk_fresh_const() 2017-05-13 14:18:05 -04:00
Nikolaj Bjorner 169295c9ba fix build warnings for theory_str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-12 08:06:24 -07:00
Nikolaj Bjorner 07474e4887 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-12 07:59:30 -07:00
Nikolaj Bjorner 64f3b3e316 remove lp_main from test branch to ensure test build only builds a single entry point 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-12 07:59:16 -07:00
Lev Nachmanson 07f2fd43bb Merge remote-tracking branch 'upstream/master' 2017-05-11 17:49:33 -07:00
Lev Nachmanson d0d71a0907 allow more failures in d_solver 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-05-11 17:49:27 -07:00
Nikolaj Bjorner a9e2a1204e add this qualifier for build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 16:58:29 -07:00
Nikolaj Bjorner 7b35eacf63 add this qualifier for build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 16:52:54 -07:00
Nikolaj Bjorner 2ab0f281f3 add this qualifier for build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 16:50:39 -07:00
Nikolaj Bjorner 29a49f4427 convert static random fields to non-static 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 16:46:07 -07:00
Lev Nachmanson cf8b35a6f3 fix init reorder warning 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-05-11 10:54:18 -07:00
Nikolaj Bjorner 431feab1bf fix build warnings part 8 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 09:37:01 -07:00
Nikolaj Bjorner eb8da3fb9d fixing setup for LRA, re-enable LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 09:34:07 -07:00
Nikolaj Bjorner 7e004fe331 fix build warnings part 7, disable LRA for regression t201.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 09:28:59 -07:00
Nikolaj Bjorner 9b3e2a9afe re-enable LRA after fixing dispatch for LRA in smt-setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 09:16:07 -07:00
Nikolaj Bjorner 49d2b86d35 fix build warnings part 6 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 08:57:17 -07:00
Nikolaj Bjorner f176e1e5e5 disable LRA until unit tests are fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 08:40:20 -07:00
Nikolaj Bjorner e9a085a0e2 enable LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 08:23:43 -07:00
Nikolaj Bjorner b9a695633d fix build issues part 4 2017-05-11 08:18:20 -07:00