mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity
7431 commits 49 branches 53 tags 181 MiB
Commit graph

7431 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
54e28a4fe7 string/sequence static features test 2017-04-24 21:02:22 -04:00
Murphy Berzish
3fe49137d0 fix trace typos 2017-04-24 19:25:35 -04:00
Dan Liew
8a1df3df62 [Doxygen] Add --doxygen-executable command line option to 
`mk_api_doc.py`. This allows a custom path to Doxygen to be specified.
 2017-04-24 21:52:59 +01:00
Dan Liew
2cdb45605d [Doxygen] Switch to using argparse to parse command line arguments 
in `mk_api_doc.py`. Given that we need to add a bunch of new command
line options it makes sense to use a less clumsy and concise API.
 2017-04-24 21:48:34 +01:00
Nikolaj Bjorner
34acaa8f56 update license for space/quotes per #982 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-24 13:34:10 -07:00
Murphy Berzish
8ce93b4ee5 unify tracing in theory_str to 'str' tag 2017-04-24 15:39:25 -04:00
Murphy Berzish
c46f95a629 remove unused parameter from smt_context 2017-04-24 12:39:55 -04:00
Murphy Berzish
9e8a4e2a01 Merge branch 'upstream-master' into develop 
Conflicts:
	src/smt/smt_context.cpp
 2017-04-24 12:28:16 -04:00
Nikolaj Bjorner
049cb957ea Merge pull request #983 from Baltoli/fixpoint-no-return 
Return check result in fixedpoint object
 2017-04-24 08:33:13 -07:00
Dan Liew
ca678c3675 [Doxygen] Fix bug where def_Type directives in z3.h would appear 
in generated doxygen documentation.
 2017-04-24 15:45:57 +01:00
Dan Liew
81ba729aab [Doxygen] Fix script --help functionality. 2017-04-24 15:25:45 +01:00
Bruce Collie
ce67c8277c Return check result in fixedpoint object 
This is a small change to fix a missing return statement.
 2017-04-24 12:59:44 +00:00
Nikolaj Bjorner
5068d2083d tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-22 11:36:03 -07:00
Nikolaj Bjorner
4f455c7a3c Merge pull request #981 from mtrberzi/theory-assumptions 
pre-init assumptions and unsat core validation for smt theories
 2017-04-22 11:27:57 -07:00
Murphy Berzish
367cc4b77f check result of unsat core validation 2017-04-22 13:36:09 -04:00
Murphy Berzish
06cd07e3c2 Merge branch 'theory-assumptions' into develop 
Conflicts:
	src/smt/smt_context.cpp
	src/smt/smt_context.h
	src/smt/smt_theory.h
 2017-04-22 13:31:43 -04:00
Murphy Berzish
a1bb1f2a13 pre-init assumptions and unsat core validation for smt theories 2017-04-22 13:15:00 -04:00
Murphy Berzish
5cfe5e15ac unsat core validation for smt theories 2017-04-21 17:51:14 -04:00
Nikolaj Bjorner
2642ef47ce Merge pull request #980 from delcypher/readme_tweak 
Readme tweak to fix #979
 2017-04-20 11:04:09 -07:00
Dan Liew
2badef9d0b Be more explicit about using Clang as the compiler as noted in #979. 
Referring to the ``mk_make.py`` line might lead someone to think they
need to modify the ``mk_make.py`` file rather than change the command
line invocation.
 2017-04-20 17:25:00 +01:00
Dan Liew
4b0f7bc222 Fix typo noted in #979. g++ is the default compiler rather than the gcc binary. 2017-04-20 17:22:05 +01:00
Christoph M. Wintersteiger
0a0b17540f Added rlimit.inc() for expensive interval exponentiation in the non-linear arithmetic theory. 2017-04-19 13:07:04 +01:00
Christoph M. Wintersteiger
a02a7f4443 Whitespace 2017-04-19 13:04:04 +01:00
Murphy Berzish
bef64961ae add pre-init assumptions for smt theories 2017-04-18 13:12:03 -04:00
Christoph M. Wintersteiger
71da36f85c Added core.extend_nonlocal_patterns parameter to improve unsat cores. 2017-04-18 15:13:11 +01:00
Nikolaj Bjorner
66e61b8a31 issues #963 #912 2017-04-17 03:06:38 -07:00
Nikolaj Bjorner
8b5627e361 additional API per #977 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-16 12:13:30 +09:00
Nikolaj Bjorner
9933c36050 replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 17:06:03 +08:00
Nikolaj Bjorner
ab6abe901f replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:57:30 +08:00
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