mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity
3664 commits 23 branches 48 tags 157 MiB
Commit graph

3664 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 27f9dec926 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-23 17:30:58 +01:00
Christoph M. Wintersteiger 4da7286a7b Fixed various signed/unsigned conversion warnings. 2015-05-23 17:30:19 +01:00
Christoph M. Wintersteiger d8f6d84217 Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. 
Fixes #103
 2015-05-23 16:53:47 +01:00
Christoph M. Wintersteiger e33ff42766 Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. 
Fixes #103
 2015-05-23 16:49:41 +01:00
Christoph M. Wintersteiger a361e4dcef typo 2015-05-23 16:40:43 +01:00
Christoph M. Wintersteiger f1cc1842e1 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-23 13:25:00 +01:00
Christoph M. Wintersteiger 98f33c3f8b Bug/build fix for hwf::fma 2015-05-23 13:10:07 +01:00
Nuno Lopes 08b5635327 fix unaligned load in hash_string() 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 12:13:39 +01:00
Christoph M. Wintersteiger d5c39798ea Bugfix for hwf 2015-05-23 12:02:53 +01:00
Nuno Lopes c577ab361b fix assorted undefined behaviors caught by clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 11:45:12 +01:00
Christoph M. Wintersteiger 25a29bf5b0 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-22 20:30:26 +01:00
Christoph M. Wintersteiger 6f6cd61817 Bugfix for float-to-float conversion. 
Fixes #77
 2015-05-22 20:30:12 +01:00
Ken McMillan e438143abc fix for github issue #105 2015-05-22 11:02:26 -07:00
Ken McMillan 4546c3e7bb merge 2015-05-22 11:01:55 -07:00
Ken McMillan 13a3bdd7a3 fix proof for extended GCD rule 2015-05-22 10:28:19 -07:00
Nikolaj Bjorner 279ef05713 expose BoolExpr[] for ASTVector and merge common functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-22 08:57:05 -07:00
Nikolaj Bjorner 4d8af9191c Merge pull request #106 from Z3Prover/revert-104-interpolation_return_expr 
Revert "Change ASTVector to Expr[] in interpolation result"
 2015-05-22 08:25:41 -07:00
Nikolaj Bjorner b4f72c8145 Revert "Change ASTVector to Expr[] in interpolation result" 2015-05-22 08:24:45 -07:00
Nikolaj Bjorner 034a9387ee Merge pull request #104 from MarcusVoelker/interpolation_return_expr 
Change ASTVector to Expr[] in interpolation result
 2015-05-22 07:16:18 -07:00
Marcus Völker a229416a2b Change ASTVector to Expr[] in interpolation result 2015-05-22 15:55:09 +02:00
Christoph M. Wintersteiger 8fc0ba0ab5 Moved auxiliary fp.isNaN lemma injection to the right place. 
Fixes #102
 2015-05-22 12:33:53 +01:00
Christoph M. Wintersteiger 891073d3fe typo 2015-05-22 12:01:10 +01:00
Christoph M. Wintersteiger ffbbf08d20 Fixed warning message about unused lock when OpenMP is not available. 2015-05-22 11:59:31 +01:00
Christoph M. Wintersteiger 54cde7cabb Bugfix for hwf::round_to_integral 2015-05-22 11:39:58 +01:00
Christoph M. Wintersteiger 759d9f2dda bugfix for hwf::fma 2015-05-22 11:39:28 +01:00
Christoph M. Wintersteiger 705ace6f0a Naming consistency 2015-05-22 11:39:08 +01:00
Nikolaj Bjorner 8a34bd2bf1 fixes issue #88 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-21 15:08:39 -07:00
Nikolaj Bjorner a3c5207f91 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-21 15:07:24 -07:00
Nikolaj Bjorner c969d78042 throw exception instead of debug mode assertion in ast_manager on malformed input 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-21 15:07:01 -07:00
Nikolaj Bjorner f100d4feda hoist out basic union find 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-21 11:10:42 -07:00
Christoph M. Wintersteiger 6f575689b1 Added injection of auxiliary lemmas for fp.isNaN, so that the value propagation can pick up these values and propagate them. 
Fixes #96.
 2015-05-21 19:02:09 +01:00
Christoph M. Wintersteiger eee076b9f8 Bugfixes for fp.min, fp.max. 
Fixes the fix for #68
 2015-05-21 18:16:02 +01:00
Christoph M. Wintersteiger 8c18bdcca9 Bugfix for fp.roundToIntegral. 
Fixes #69
 2015-05-21 18:12:14 +01:00
Christoph M. Wintersteiger c422b48bf4 Bugfix for hwf_manager::round_to_integral 2015-05-21 15:06:47 +01:00
Ken McMillan caa616f11b fix for github issue 83 2015-05-20 15:37:51 -07:00
Nikolaj Bjorner cd8f82ebc2 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-20 10:41:50 -07:00
Nikolaj Bjorner 9d0e3abd24 use static features to set hidden configuration parameters on small integers and int vs. real 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-20 10:41:41 -07:00
Christoph M. Wintersteiger 51040d3e19 Bugfix for fp.isNormal 2015-05-20 18:32:40 +01:00
Christoph M. Wintersteiger 1e3952406c disabled debug output 2015-05-20 18:14:38 +01:00
Christoph M. Wintersteiger f8145c8b9f Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-20 17:57:34 +01:00
Christoph M. Wintersteiger c377fec7a4 Made fp.* comparison chainable. 2015-05-20 17:57:27 +01:00
Nikolaj Bjorner e915d0f67d Merge pull request #97 from hguenther/unstable 
Expose insert_if_not_there_core method in map class
 2015-05-20 09:25:53 -07:00
Nikolaj Bjorner c876194a43 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-20 09:22:01 -07:00
Nikolaj Bjorner 28f6adf79e disable hybrid relations pending overhaul/deletion of product relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-20 09:21:55 -07:00
Henning Günther 33ddf0bcdf Expose insert_if_not_there_core method in map class 
Signed-off-by: Henning Günther <t-hennig@microsoft.com>
 2015-05-20 14:33:46 +01:00
Ken McMillan ccc1f02216 fix for github issue 54 2015-05-19 18:47:13 -07:00
Nuno Lopes 69a3590490 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-19 16:52:57 +01:00
Nuno Lopes 66e6e67395 fix build on CentOS 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-19 16:52:47 +01:00
Christoph M. Wintersteiger 8f3b133882 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-19 16:52:16 +01:00
Christoph M. Wintersteiger 0197f6e010 Bugfix for fp.rem when the result is zero. 
Fixes #91
 2015-05-19 16:51:56 +01:00