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

3602 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 949c21ca08 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 02:23:56 -07:00
Nikolaj Bjorner fe7c577d99 isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 01:54:52 -07:00
Nikolaj Bjorner f8e2fa0337 fixes issue #93 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-29 11:11:13 -07:00
Nikolaj Bjorner 1714182c38 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 11:08:25 -07:00
Nikolaj Bjorner 203a62bbdb Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 11:07:04 -07:00
Nikolaj Bjorner fcb9bac148 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 11:06:23 -07:00
Christoph M. Wintersteiger fec815b41e Various variable renamings to avoid conflicts with previously defined local variables, function parameters, or members (Visual Studio 2015 warnings). 2015-05-29 18:13:39 +01:00
Nikolaj Bjorner 5acefceada Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 08:58:31 -07:00
Nikolaj Bjorner 137b8c8e04 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 08:55:53 -07:00
Nikolaj Bjorner a2448be0cd print pareto model in check-sat too 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-29 08:55:44 -07:00
Christoph M. Wintersteiger ba88648468 Added has_fp_to_real probe to detect when QF_FP need QF_NRA. 2015-05-29 14:49:53 +01:00
Christoph M. Wintersteiger d35ebd6e57 Bugfix for FP to_fp from non-numeral reals. 2015-05-29 14:49:26 +01:00
Christoph M. Wintersteiger 85419ca503 Added branch into QF_NRA from QF_FP problems containing to_real terms. 2015-05-29 14:21:27 +01:00
Christoph M. Wintersteiger 9428acd578 Bugfix for FPA rewriter. 2015-05-29 13:58:33 +01:00
Christoph M. Wintersteiger f2f6fc1994 Added QF_BVFP logic alias for QF_FPBV 2015-05-29 13:58:23 +01:00
Christoph M. Wintersteiger 9de0e9087e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 12:55:40 +01:00
Christoph M. Wintersteiger d8d0b21e42 Bugfix for dll/so name resolution in Java. 
Fixes #111
 2015-05-29 12:55:17 +01:00
Christoph M. Wintersteiger 3f22201ba3 Bugfix for dll/so name resolution in Java. 2015-05-29 12:25:44 +01:00
Nikolaj Bjorner ed7e0e11a8 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-28 20:55:13 -07:00
Nikolaj Bjorner e47eea2c61 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-28 17:22:34 -07:00
Nikolaj Bjorner ac732a500c add first file 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-28 15:20:25 -07:00
Nikolaj Bjorner 23a6138d81 initialize potentially unused variables. Fixes issue #112 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-28 14:55:37 -07:00
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
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