mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity
5723 commits 23 branches 48 tags 156 MiB
Commit graph

5723 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 12c47348bc Merge pull request #761 from delcypher/bv2fpa_unbreak_cmake_build 
Unbreak the CMake build broken by 009af4455d
 2016-10-17 11:47:01 +01:00
Nikolaj Bjorner 4fda2adec8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-16 15:46:50 -04:00
Nikolaj Bjorner 58198d7cb6 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:45:39 -04:00
Nikolaj Bjorner aec59e4ff7 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:43:28 -04:00
Dan Liew b2381acceb Unbreak the CMake build broken by 009af4455d 
The commit added an additional source file and dependency but the
corresponding changes weren't added to the CMake build.
 2016-10-15 21:42:20 +01:00
Christoph M. Wintersteiger 13e3484d15 Merge pull request #759 from wintersteiger/fpa-unspec 
Refactored and fixed model conversion for unspecified FP values in theory_fpa.
 2016-10-15 18:43:28 +01:00
Christoph M. Wintersteiger 009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger ab4bb8194e Added unregister_decl to model_core 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger 58af4cae14 More consistent fp.* operators. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger 7e705a2d32 Bug fixes for underspecified FP operations. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger bc257211d6 Whitespace 2016-10-15 18:35:39 +02:00
Nikolaj Bjorner d8ea3023fc Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-10 23:49:59 -07:00
Nikolaj Bjorner 487f15f90a better encodings for at-most-1, #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-10 23:49:45 -07:00
Nikolaj Bjorner 8d2b70a5e2 better encodings for at-most-1, #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-10 23:46:03 -07:00
Nikolaj Bjorner a4382ce538 Merge pull request #757 from angr/master 
Final fixes + metadata for python distribution
 2016-10-10 17:11:19 -07:00
Andrew Dutcher bd80f7b4d5 fix some issues with the windows build 2016-10-10 15:38:08 -07:00
Andrew Dutcher 67a7889188 Update metadata for new distribution 2016-10-10 15:38:02 -07:00
Nikolaj Bjorner 5d9820f3e2 add example of parsing with external declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-07 12:57:07 -07:00
Nikolaj Bjorner 37f7c30e23 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-07 12:42:13 -07:00
Nikolaj Bjorner 619cce0a52 add mutex preprocessing to maxsat, add parsing functions to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-07 12:42:08 -07:00
Christoph M. Wintersteiger 5dec919217 Remove unnecessary "unsafe" qualifier on internal .NET API class. 2016-10-06 16:36:19 +01:00
Christoph M. Wintersteiger 9548b88e71 Added dummy code contracts for .NET Core/CoreCLR builds. 2016-10-06 16:24:49 +01:00
Christoph M. Wintersteiger 4956f6ef5b Test fix for python3 2016-10-05 16:11:07 +01:00
Christoph M. Wintersteiger 56e874e991 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-05 15:34:07 +01:00
Christoph M. Wintersteiger d495b08639 Build/test fix for python3 2016-10-05 15:34:02 +01:00
Nikolaj Bjorner f452895f5f add mutex pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-04 14:45:23 -07:00
Nikolaj Bjorner deed85b260 Merge pull request #752 from deeglaze/patch-1 
Z3_query_constructor documentation clarification
 2016-10-04 11:49:36 -07:00
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
Christoph M. Wintersteiger acdaeca826 Bugfix for ITEs over FP rounding modes. 
Fixes #751.
 2016-10-04 18:04:56 +01:00
Christoph M. Wintersteiger 0bd06930ae whitespace 2016-10-04 18:04:00 +01: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 f00d5b89e0 Merge pull request #750 from angr/fix/python-global-load 
allow python to load libz3 using loader's default search
 2016-09-28 21:15:29 -07:00
Andrew Dutcher 7816c53352 allow python to load libz3 using loader's default search 2016-09-28 21:05:55 -07:00
Nikolaj Bjorner ab3b36269e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-28 16:42:14 -07:00
Nikolaj Bjorner 476b06fa14 fix compiler warnings, gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-28 16:42:07 -07:00
Nikolaj Bjorner 9fa7cd48e9 Merge pull request #747 from LocutusOfBorg/patch-2 
fix build with new gcc and clang compilers
 2016-09-27 18:07:57 -07:00
Nikolaj Bjorner 6f4c139c28 Merge pull request #746 from LocutusOfBorg/patch-1 
Update mpff.cpp to fix build with clang and new gcc
 2016-09-26 08:47:09 -07:00
Gianfranco Costamagna 4817b87b7d fix build with new gcc and clang compilers 2016-09-26 08:06:38 +02:00
Gianfranco Costamagna 9c48fbba2e Update mpff.cpp to fix build with clang and new gcc 2016-09-26 08:05:15 +02: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
Nikolaj Bjorner b758a7a508 disable smt-lib success printing when locally parsing database of common pattern rules. Issue #743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 19:53:48 -07:00
Nikolaj Bjorner 092c52e5b7 fix for package directory. issue #744 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 18:29:26 -07:00
Nikolaj Bjorner 9746794962 Merge pull request #742 from angr/fix-tests 
Fix z3test for build rearrangement
 2016-09-21 18:41:57 -07:00
Andrew Dutcher 4801a27c2d Fix up z3test to a) exist and b) work 2016-09-21 17:18:10 -07:00
Nikolaj Bjorner cf56da8482 add z3test to cmakelists.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:33:30 -07:00