mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
4360 commits 49 branches 53 tags 182 MiB
Commit graph

4360 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
49a4df0de1 MPF min/max -+0.0 special cases changed to +0.0 instead of second argument. 
Another piece of fix #68
 2015-05-28 12:54:57 +01:00
Christoph M. Wintersteiger
ee79b1ca9a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-28 12:21:07 +01:00
Christoph M. Wintersteiger
7619d609f9 FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. 
Fixes #68
 2015-05-28 12:20:48 +01:00
Christoph M. Wintersteiger
713126225b FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. 2015-05-28 12:19:55 +01:00
Ken McMillan
3d2ef8bb4a fix for issue #109 2015-05-27 16:05:40 -07:00
Nikolaj Bjorner
534271db08 adding parameters to gomory cut axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 14:48:51 -07:00
Nikolaj Bjorner
e3b1ce1fdc also allw n-ary distrinct 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 10:07:09 -07:00
Nikolaj Bjorner
4f02d380aa make use of uninterpreted_sort shorthand 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:34:47 -07:00
Nikolaj Bjorner
562ed61a24 add shorthands for creating uninterpreted sorts to context API 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:30:37 -07:00
Nikolaj Bjorner
e483efd3f4 fixes to Euclidean solver, fixes #100 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:21:20 -07:00
Nikolaj Bjorner
cb00555635 local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:18:52 -07:00
Nuno Lopes
156ba65359 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-27 17:07:37 +01:00
Nuno Lopes
b10f79a941 dl_compiler: minor simplifications 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-27 17:07:18 +01:00
Christoph M. Wintersteiger
98975e5187 Reordered the default qflia probe to be checked before the more permissive qfauflia. 2015-05-27 14:47:24 +01:00
Christoph M. Wintersteiger
91352369a9 Added conversion functions to ASTVectors in .NET and Java. 
Fixes #108
 2015-05-26 11:20:19 +01:00
John Grosen
64b46f2310 Fix the Python FPRef.__lt__ implementation 2015-05-25 00:31:04 -07:00
Christoph M. Wintersteiger
9912b2cd67 Re-enabled the smt.arith.greatest_error_pivot parameter. 2015-05-23 18:01:00 +01:00
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