mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
5696 commits 24 branches 48 tags 158 MiB
Commit graph

1070 commits

Author SHA1 Message Date
Dionna Amalie Glaze
f4fd721741 Z3_query_constructor documentation clarification 
Hit a segfault when I assumed the API would allocate these _out parameters for me.
 2016-10-04 13:02:31 -05:00
Nikolaj Bjorner
e3f0aff318 address ubuntu warning and add shortcuts for maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-03 16:22:13 -07:00
Nikolaj Bjorner
186afe7d10 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-02 10:22:23 -07:00
Nikolaj Bjorner
b2db2f1eb6 allow negative weights for weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-02 10:21:58 -07:00
Nikolaj Bjorner
57ebf7bd38 accepting floats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-02 10:08:23 -07:00
Nikolaj Bjorner
136f724445 update python API with facilities for Pseudo-Booleans and += shorthand for adding constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-30 14:18:34 -07:00
Nikolaj Bjorner
279621c1d7 duplicating private member from z3 to avoid build regressions under some environments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-30 07:21:39 -07:00
Nikolaj Bjorner
8cf356224e fix python for 3.x 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 22:24:43 -07:00
Andrew Dutcher
4801a27c2d Fix up z3test to a) exist and b) work 2016-09-21 17:18:10 -07:00
Nikolaj Bjorner
14668b4d44 Merge pull request #735 from angr/new-build 
New packaging for and ability to distribute python bindings
 2016-09-21 15:55:22 -07:00
Nikolaj Bjorner
527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Andrew Dutcher
02217d048b replace all non-portable filepath slashes with os.path.join 2016-09-14 14:19:10 -07:00
Andrew Dutcher
02783d0bfb Minor tweaks to make things more reliable/less obnoxious 2016-09-14 01:49:37 -07:00
Andrew Dutcher
704105306c FINISH IT 2016-09-14 01:40:01 -07:00
Andrew Dutcher
0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Andrew Dutcher
fa6cc19184 Moved python bindings into package 2016-09-14 01:33:07 -07:00
Nikolaj Bjorner
94b67412ec Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-07 11:59:06 -07:00
Nikolaj Bjorner
c5dd441947 fixes to consequence generation and cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-07 11:50:26 -07:00
Nikolaj Bjorner
2d9dced1c7 fix spacing, cast to Bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 20:18:31 -07:00
cttghc
758266b952 Fix omission of Z3_model_has_interp in z3++.h 2016-09-06 18:32:41 -05:00
Nikolaj Bjorner
0e9758a211 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-06 14:39:19 -07:00
AlexVonB
c6b0fc444c Fix VisualStudio 2010 compiler warning C4100 
When compiling with Visual Studio 2010 the buildlog warns of the following: `z3++.h: warning C4100: 'e' : unreferenced formal parameter` and `z3++.h: warning C4100: 'c' : unreferenced formal parameter`. This merge request removes this warning.
 2016-09-05 16:22:00 +02:00
Nikolaj Bjorner
424a8c69bd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-02 03:05:23 -07:00
Nikolaj Bjorner
4d9aadde35 updated consequence finder to fix bug in processing enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 16:15:36 +08:00
Nikolaj Bjorner
310c0f31a1 use type constrsaints for co-variant subtying to enable .net 3.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 12:07:06 +08:00
Nikolaj Bjorner
439e8e6b04 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-20 03:53:55 -07:00
Nikolaj Bjorner
f2b5c11d1c add option for prettier proof printing, Issue #706 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 03:52:45 -07:00
Nikolaj Bjorner
b2383a481a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-18 18:02:22 -07:00
Nikolaj Bjorner
665fccf07a addressing max-segment issue for AMD64 + Debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-18 18:01:29 -07:00
Christoph M. Wintersteiger
244c641234 debug check fix 2016-08-12 13:19:12 +01:00
Christoph M. Wintersteiger
ff3c630207 .NET API: Added MkMul from IEnumerable. 2016-08-09 16:36:32 +01:00
Nikolaj Bjorner
14e8126f16 wrapping interruptable with solver consequence call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-05 11:32:12 -07:00
Nikolaj Bjorner
cb2d8d2107 add detection of non-fixed variables to consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 19:12:41 -07:00
Nikolaj Bjorner
d32019f4c9 fix consequence tracking for negated assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 10:49:06 -07:00
Nikolaj Bjorner
2263be1b4d adding consequence examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:24:14 -07:00
Nikolaj Bjorner
5c99405db3 finish consequence fast path code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 20:15:47 -07:00
Nikolaj Bjorner
074f1ad778 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 11:20:23 -07:00
Nikolaj Bjorner
14f29e7265 add basic built-in consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:20:17 -07:00
Christoph M. Wintersteiger
7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger
0d83f99d8d Fixed comment 2016-07-28 18:06:26 +01:00
Christoph M. Wintersteiger
3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner
5f5ef8b38d adding support for distinct for dt2bv, re-entry harness for ~Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 09:02:56 -07:00
Nikolaj Bjorner
fe34e8bf00 Add OP_INTERNAL to handle cases of function symbols that don't have external semantics (at least in a way that is supported by means of building terms) Issue #688 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 12:13:54 -07:00
Nikolaj Bjorner
cf48eb5f72 mark also ast in parameters as GC roots. Issue #676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-17 19:16:15 -04:00
Nikolaj Bjorner
64674386de fix ubuntu build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 13:39:50 -07:00
Nikolaj Bjorner
6f971a3a86 add object z3 objects to target context during translation, to fix build regression failure on z3test.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 11:44:38 -07:00
Nikolaj Bjorner
b080e3a216 garbage collect all api::object references when calling del_context. Request issue #679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 22:26:21 -07:00
Nikolaj Bjorner
d7d22cad02 undo comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:38:03 -07:00
Nikolaj Bjorner
53b3edc8cc add cases for recognizing ALL. Issue #674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:18:26 -07:00
Nikolaj Bjorner
0d0d504d62 change names of reserved identifiers. Issue #666 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 14:46:44 -07:00