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

6749 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Murphy Berzish 82d472a227 Merge remote-tracking branch 'upstream/master' into develop 2017-03-23 13:35:58 -04:00
Nikolaj Bjorner 26ae3a5abb making simplifier code exception friendlier. Towards getting a handle on #939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 19:06:59 -07:00
Nikolaj Bjorner e47e8c67c0 introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating #939: 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 14:12:47 -07:00