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

3574 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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