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

7254 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sangwoo Joh
5845958986 Bugfix: get_objectives in ML API 2017-08-24 18:17:47 +09:00
Nikolaj Bjorner
00888f1be0 Merge pull request #1229 from DewaldDeJager/docstring-function-name-change 
[Doxygen] Fix function name in docstring
 2017-08-23 16:12:10 -07:00
Nikolaj Bjorner
3993c8581c Merge pull request #1228 from delcypher/cmake_support_git_worktrees 
[CMake] Teach CMake to support git worktrees
 2017-08-23 16:11:46 -07:00
Dewald de Jager
40f2afb5af [Doxygen] Fix function name in docstring 
Amending the changes made in fe702d7782
 2017-08-23 23:09:47 +02:00
Dan Liew
58f152a92a [CMake] Teach CMake to support git worktrees. This fixes the bug 
reported by @nbraud reported in #1227.

Previously the CMake build system assumed that the `.git` file must
be a directory. This is not the case when the working directory
is a "git worktree". In this case the `.git` file is just a plain
file that points to a directory within the true `.git` directory.
This commit essentially implements the logic to traverse this extra
level of indirection and removes some assumptions that the `.git`
file is a directory.
 2017-08-23 19:30:24 +01:00
Christoph M. Wintersteiger
dca30ab202 Merge pull request #1225 from nbraud/nbraud/injectivity 
Add injectivity tactic
 2017-08-23 15:51:19 +01:00
Christoph M. Wintersteiger
6f8a954532 added missing addition to smt_params_helper.pyg 2017-08-23 12:37:26 +01:00
Christoph M. Wintersteiger
573dae5f0c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-23 12:14:53 +01:00
Christoph M. Wintersteiger
3e960eadd2 (Re-)added option to disable lemma deletion in the smt_context. 2017-08-23 12:14:19 +01:00
Nicolas Braud-Santoni
b877c962ca injectivity: Add tactic to CMake-based builds 2017-08-23 10:27:55 +00:00
Nicolas Braud-Santoni
ae9ace2321 injectivity: Cleanup whitespace 2017-08-23 10:25:33 +00:00
Nicolas Braud-Santoni
27fd879b8c injectivity: Fixup rewriter 2017-08-22 18:44:34 +00:00
Nicolas Braud-Santoni
33dd168195 Remove unnecessary parameter 2017-08-22 18:09:57 +00:00
Nicolas Braud-Santoni
c0b6d00e8a Update debug output 2017-08-22 18:09:38 +00:00
Nicolas Braud-Santoni
4cb7f72509 First version of the inj. tactic 2017-08-22 17:10:20 +00:00
Nicolas Braud-Santoni
cb87d47f08 obj_hashtable: Constify 2017-08-22 17:10:20 +00:00
Nikolaj Bjorner
26afdd92c9 Merge pull request #1222 from NikolajBjorner/master 
bug fixes and revision of proto_model
 2017-08-21 17:19:27 -07:00
Nikolaj Bjorner
2c8e9aeb9c another crash fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-21 15:23:52 -07:00
Nikolaj Bjorner
e6145fa6df fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-21 14:53:16 -07:00
Nikolaj Bjorner
ebe9db14d5 fix regression exposed by segfault2.smt2 crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-21 14:13:43 -07:00
Christoph M. Wintersteiger
ed5058d225 Fixed typo in ML API. Relates to #1214. 2017-08-21 18:21:31 +01:00
Nikolaj Bjorner
e47cd27c8d compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 16:18:25 -07:00
Nikolaj Bjorner
359ee818a5 purge iterators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 15:35:16 -07:00
Nikolaj Bjorner
9fe9587a9b revert local changes to theory_str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 09:14:08 -07:00
Nikolaj Bjorner
ff734d6aa9 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-20 08:51:32 -07:00
Nikolaj Bjorner
276fdd0e97 register auxiliary constants from projection operation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 08:51:24 -07:00
Nikolaj Bjorner
04084e21c8 Merge pull request #1220 from mtrberzi/regex-fixes 
Small regex fixes in theory_str
 2017-08-20 08:01:59 -07:00
Murphy Berzish
adae32f7ef add re.all to NFA in theory_str 2017-08-19 23:25:34 -04:00
Nikolaj Bjorner
bc8ae21ebe missing parameters for OSX/Linus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 15:14:47 -07:00
Nikolaj Bjorner
a8e7974011 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-18 14:57:54 -07:00
Nikolaj Bjorner
7a977f0106 ensure that timeouts are distinguished from other cancel events #848 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 14:54:54 -07:00
Murphy Berzish
1e445a62d4 improve error message in theory_str when an invalid term in str.to.re is encountered 
addresses #871
 2017-08-18 17:31:40 -04:00
Nikolaj Bjorner
aa81d58bb0 add sequences to ML API #1214 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 14:29:53 -07:00
Nikolaj Bjorner
6feb7ba795 :q 
add sequences to ML API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 14:28:05 -07:00
Nikolaj Bjorner
112fa16bc0 fix #1217 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 09:19:38 -07:00
Nikolaj Bjorner
ee00852151 fix compilation of tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 21:09:23 -07:00
Nikolaj Bjorner
66b24a6c18 change typename to class in optional to deal with compilation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 21:00:14 -07:00
Nikolaj Bjorner
e1d08e9526 remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:41:29 -07:00
Nikolaj Bjorner
a3ccdaf318 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-17 20:28:56 -07:00
Nikolaj Bjorner
ff47c8632b remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:28:49 -07:00
Nikolaj Bjorner
7d8c745c89 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-17 15:59:43 -07:00
Nikolaj Bjorner
d15f8c52a0 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 15:59:40 -07:00
Nikolaj Bjorner
7861cfcef2 Merge pull request #1216 from delcypher/cmake_simpler_include_paths 
Simpler include paths (fixes #534)
 2017-08-17 15:59:23 -07:00
Christoph M. Wintersteiger
abd599f48e Fixed ref-counting bug in smt_model_checker. Fixes #1212. 2017-08-17 19:29:53 +01:00
Christoph M. Wintersteiger
320c81e497 Whitespace 2017-08-17 19:18:14 +01:00
Dan Liew
920c596c23 [CMake] Clean up setting include paths. 
Now that all include paths are relative to the `src/` trees (
one in source tree and one in the build tree) we can simplify
what the CMake build does significantly.

While I'm here I also removed some dead code that wasn't doing
anything useful.
 2017-08-17 18:26:58 +01:00
Dan Liew
a2d7b43554 Update header includes to be relative to src/ directory. 2017-08-17 18:26:53 +01:00
Christoph M. Wintersteiger
3487b368d1 Added diagnostic output for pattern inference. 2017-08-17 17:27:06 +01:00
Christoph M. Wintersteiger
1620796bd1 Whitespace 2017-08-17 17:25:04 +01:00
Nikolaj Bjorner
4ab0ee75fa mam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 08:49:06 -07:00