mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
7602 commits 49 branches 53 tags 182 MiB
Commit graph

7602 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
87c3b5ee51 replace uint by long 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:29:02 +08:00
Nikolaj Bjorner
e4b9080165 include timeout/rlimit parameters in optmize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:04:13 +08:00
Nikolaj Bjorner
48638c6f1e fix for #975, add mask to ensure character encoding is unique within range of bits used for encoding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:34:13 +07:00
Nikolaj Bjorner
7bb5e72e07 add missing string/re operations #977 and adding Pseudo-Boolean operations to Java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:09:30 +07:00
Murphy Berzish
a7f72bf4ef add overlap assumption to other cases in theory_str 2017-04-13 13:46:23 -04:00
Murphy Berzish
7207cabc97 experimental new unsat core based overlap detection 2017-04-12 17:09:35 -04:00
Nikolaj Bjorner
4140afa4cb add regular expression membership for range of int.to.str functions. Issue #957 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-11 10:49:42 +08:00
Nikolaj Bjorner
be3cc91323 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-11 07:40:30 +08:00
Nikolaj Bjorner
67513a2cf5 fix detection of bounds under conjunctions. Issue #971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-11 07:40:09 +08:00
Christoph M. Wintersteiger
b67c1c5501 Fixed valgrind warning. Fixes #972 2017-04-10 16:28:41 +01:00
Christoph M. Wintersteiger
95cf1447ea Added maintainers.txt for qprofdiff 2017-04-10 13:18:45 +01:00
Nikolaj Bjorner
80c10d5833 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-07 21:22:48 -07:00
Nikolaj Bjorner
ec29a03c8f add facility to dispense with cancellation (not activated at this point). Address #961 by expanding recurisve function definitions that are not tautologies if the current model does not validate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-07 21:22:38 -07:00
Christoph M. Wintersteiger
27a1758857 Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body. 2017-04-07 21:19:20 +01:00
Christoph M. Wintersteiger
9a757ffffe Result ordering fix for qprofdiff 2017-04-07 18:12:33 +01:00
Christoph M. Wintersteiger
23f4a0c332 Build fix for qprofdiff 2017-04-07 18:12:26 +01:00
Christoph M. Wintersteiger
f3c990d356 Fixes for qprofdiff 2017-04-07 18:12:16 +01:00
Christoph M. Wintersteiger
d390885757 Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true 2017-04-06 18:37:29 +01:00
Christoph M. Wintersteiger
7d35fcb17e Avoid null pointer warnings in justifications. 2017-04-05 19:42:02 +01:00
Murphy Berzish
eef2bbadad remove obsolete PARAM_STRING from ast 2017-04-04 20:29:48 -04:00
Murphy Berzish
f881e85470 remove old theory_str enums from api 2017-04-04 17:54:18 -04:00
Murphy Berzish
19de682b58 remove references to m_str_fid in api 2017-04-04 17:22:55 -04:00
Murphy Berzish
a8935e99bc Merge branch 'upstream-master' into develop 2017-04-04 16:47:30 -04:00
Nikolaj Bjorner
c4b26cd691 add bypass to allow recursive functions from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 16:38:15 -07:00
Nikolaj Bjorner
582880346e add index option to 'eval' command for box objectives. Issue #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 09:22:56 -07:00
Nikolaj Bjorner
8f798fef1a fix python interface for string extract to take symbolic indices per bug report from Kun Wei 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 08:24:12 -07:00
Nikolaj Bjorner
c99205fa7e return box model based on index. Issue #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 08:12:53 -07:00
Christoph M. Wintersteiger
0fb3161113 Updated declarations in decl_collector 2017-03-31 12:10:51 +01:00
Christoph M. Wintersteiger
ef3d340c85 Improved decl_collector for uninterpreted sorts in :print_benchmark output 2017-03-31 12:04:46 +01:00
Christoph M. Wintersteiger
041520f727 SMT2 compliancy fix; NRA includes conversion of Int numerals 2017-03-28 18:17:22 +01:00
Nikolaj Bjorner
0c4b792dac Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-25 19:32:17 +01:00
Nikolaj Bjorner
3a9857940e add missing axioms for str.at. Issue #953 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-25 19:31:01 +01:00
Nikolaj Bjorner
723b507a88 properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:11:39 -07:00
Nikolaj Bjorner
e05cee757b properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:10:42 -07:00
Christoph M. Wintersteiger
3bbe5eceeb fix for --get-describe 2017-03-24 15:53:46 +00:00
Christoph M. Wintersteiger
f8d022a180 Non-windows build fix 2017-03-24 15:25:18 +00:00
Christoph M. Wintersteiger
fb105afac2 Windows build fix 2017-03-24 15:22:33 +00:00
Christoph M. Wintersteiger
0399e5e2d3 Fixed variable initialization warning 2017-03-24 14:49:24 +00:00
Christoph M. Wintersteiger
d10dec2218 Removed unused variable 2017-03-24 14:31:06 +00:00
Christoph M. Wintersteiger
7f9c37e19d VS2017 SSE4 intrinsics build fix 2017-03-24 14:23:39 +00:00
Christoph M. Wintersteiger
e9cd4d1057 Build fix for systems that don't come with SSE4.1 support by default 2017-03-24 11:51:36 +00:00
Christoph M. Wintersteiger
46ff4ae40d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-24 09:40:23 +00:00
Christoph M. Wintersteiger
866035d786 Disabled debug output 2017-03-24 09:40:18 +00:00
Nikolaj Bjorner
ec47706226 fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 02:23:50 -07:00
Nikolaj Bjorner
5d11a1cdb2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-24 01:31:16 -07:00
Nikolaj Bjorner
c56c7fd649 add handlers for dense difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 01:31:00 -07:00
Christoph M. Wintersteiger
37167a8dd6 Fixed excessive trace output 2017-03-23 19:53:23 +00:00
Nikolaj Bjorner
0313f52cf2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-23 11:10:32 -07:00
Nikolaj Bjorner
62e87d6474 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:10:19 -07:00
Nikolaj Bjorner
1ab7ab9d74 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:09:36 -07:00