mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 01:14:36 +00:00
Code Activity
7444 commits 45 branches 52 tags 177 MiB
Commit graph

7444 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a206362cef add comments addressing some questions #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-22 11:41:25 -07: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
Nikolaj Bjorner
392334f779 add ability to create and manipulate model objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-22 10:44:32 -07: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
Christoph M. Wintersteiger
b2d590e0c9 Bugfix for MAM. Fixes #1213. Partially addresses #1212. 2017-08-17 16:00:59 +01:00
Christoph M. Wintersteiger
96d0781c9d Whitespace 2017-08-17 11:39:06 +01:00
Nikolaj Bjorner
43c2ccb29a add missing functions to serialize optimize benchmarks for Java #1215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-16 16:38:48 -07:00
Nikolaj Bjorner
4b759fd865 add missing functions to serialize optimize benchmarks for Java #1215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-16 16:18:19 -07:00
Nikolaj Bjorner
bb32a83c4f Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-16 14:33:43 -07:00
Nikolaj Bjorner
370706b2b7 patch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-16 14:33:37 -07:00
Nikolaj Bjorner
97e263299d add logic 'SAT' as an alternative name to QF_FD some solverFor(SAT) works too. #1152 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 01:35:28 -07:00
Nikolaj Bjorner
25752dc169 enable QF_UF mode use same parameters whether with or without static featues, #1141, revert some breaking changes that should not have been part of commit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 01:20:30 -07:00
Nikolaj Bjorner
1690febffd enable QF_UF mode use same parameters whether with or without static featues, #1141 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 00:26:05 -07:00
Nuno Lopes
4b00bc636b revert the patch to remove no-strict-aliasing 
VS 2012 doesnt support C++11 unions..
 2017-08-14 23:00:59 +01:00