mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
4100 commits 23 branches 48 tags 157 MiB
Commit graph

3391 commits

Author SHA1 Message Date
Nikolaj Bjorner d83f8d08f3 Merge pull request #276 from kenmcmil/issue260 
issue #260 -- support timeout in Z3_compute_interpolant
 2015-10-28 20:30:15 -07:00
Ken McMillan d4dff70f39 issue #260 -- support timeout in Z3_compute_interpolant 2015-10-28 18:02:14 -07:00
Christoph M. Wintersteiger 6a5da9e9c4 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-28 23:32:42 +00:00
Christoph M. Wintersteiger 118d597c22 removed byte order mark 2015-10-28 23:31:08 +00:00
Nikolaj Bjorner aab63dc126 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-28 16:10:34 -07:00
Nikolaj Bjorner 4f7fdb5c14 fix merge conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 16:09:46 -07:00
Ken McMillan 8550de41a6 issue #204 -- throw better exception for non-linear arithmetic 2015-10-28 14:41:27 -07:00
Nikolaj Bjorner 3bc94e08b3 move friend definitions to inlined functions. Issue #241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 13:24:13 -07:00
Nikolaj Bjorner ced04bc15c Merge pull request #272 from NikolajBjorner/master 
Remove old_simplify.bv.hi_div0 option, reconciling it with rewriter.b…
 2015-10-28 12:54:55 -07:00
Nikolaj Bjorner 4d6977eaea Remove old_simplify.bv.hi_div0 option, reconciling it with rewriter.bv.hi_div0. To address issue #237 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 12:53:53 -07:00
Christoph M. Wintersteiger cab42d2c66 Clarified documentation of par-or tactic. 
Relates to #269.
 2015-10-28 18:50:22 +00:00
Christoph M. Wintersteiger ab337de101 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-28 18:44:34 +00:00
Christoph M. Wintersteiger c537084056 Revert "Fixed bug in par-or tactic." 
This reverts commit 89b6589a37.
 2015-10-28 18:42:16 +00:00
Nikolaj Bjorner 6b82b949cf Make Groebner basis computation interruptable. Exponsed in issue #269 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 11:39:59 -07:00
Nikolaj Bjorner 2a95a77706 fix issues #240, #250 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 09:47:17 -07:00
Christoph M. Wintersteiger 89b6589a37 Fixed bug in par-or tactic. 
Fixes #269.
 2015-10-28 15:34:30 +00:00
Christoph M. Wintersteiger 2218f86f03 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-28 14:46:23 +00:00
Christoph M. Wintersteiger 15be8d424c Fixed Python 3.x issues. 2015-10-28 14:19:23 +00:00
Nikolaj Bjorner b197e590a4 fix coercion regression. Issue #263 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-27 19:25:38 -07:00
Nikolaj Bjorner eb735640e7 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-27 19:22:51 -07:00
Nikolaj Bjorner 418b6d4738 Merge pull request #267 from kenmcmil/duality_interp_error_handling 
issue #200
 2015-10-27 18:49:46 -07:00
Ken McMillan 589053fc10 interp: fix gomory cut rule with non-local conclusion (issue #200) 2015-10-27 18:27:25 -07:00
Nikolaj Bjorner 47cb1058b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-27 18:11:35 -07:00
Nikolaj Bjorner 357a92dfef n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-27 18:11:31 -07:00
Christoph M. Wintersteiger eff776acd9 Fixed #include of <hash_set> which is deprecated in VS2015 and will be removed. 
Detailed error:
...\VC\INCLUDE\hash_set(17): error C2338: <hash_set> is deprecated and will be REMOVED. Please use <unordered_set>. You can define _SILENCE_STDEXT_HASH_DEPRECATION_WARNINGS to acknowledge that you have received this warning. (compiling source file ..\..\..\src\test\hashtable.cpp).
 2015-10-27 17:11:40 +00:00
Christoph M. Wintersteiger 97d97f4694 Fixed Python 3.x doctest problems 2015-10-27 16:39:07 +00:00
Christoph M. Wintersteiger 7324ef7c39 Fixed FP function names in Python API. 
Fixes #264
 2015-10-27 12:02:38 +00:00
Christoph M. Wintersteiger 89fb5a44fb Made fresh variable generation in fpa2bv lazy so that it doesn't create unnecessary variables. 2015-10-26 18:10:15 +00:00
Christoph M. Wintersteiger df1c84c182 fixed indentation (Python 3.x problem) 2015-10-26 16:08:55 +00:00
Christoph M. Wintersteiger 5b39d8fa0d bugfix for fpa2bv converter 2015-10-26 15:59:00 +00:00
Christoph M. Wintersteiger d558eaa321 Eliminated unused variable in fpa2bv model converter. 2015-10-26 15:45:21 +00:00
Paul Phillips 64a5247813 Changed references to help-tactics to help-tactic. 2015-10-25 11:45:46 -07:00
Christoph M. Wintersteiger cbf8bd8de1 Enabled proof & core production in fpa2bv and qffp. 2015-10-25 15:56:42 +00:00
Christoph M. Wintersteiger ed94bc2f6b Bugfix for fpa2bv converter. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger 9b5abcd55a Improved support for FPA unspecified min/max values, model validation, and proof generation. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger ca496f20cb Partial refactoring of fpa2bv conversion to support proofs. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger 099775947e Partial fix for fp,min/fp.max models 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger e3ed0159a8 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-25 13:09:59 +00:00
Christoph M. Wintersteiger 21ad1fb623 Bugfix for proof production in asserted_formulas::propagate_values() 
Fixes #259
 2015-10-25 13:09:18 +00:00
Nikolaj Bjorner 05c6ed1698 fixing issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 09:54:05 -07:00
Nikolaj Bjorner ac902dad1a fix another regression and missing detection of bounds, Issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 08:53:12 -07:00
Nikolaj Bjorner ffa78b95ab fix unbounded, issue #252 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-21 14:38:47 -07:00
Christoph M. Wintersteiger e2f2708a9c Fixed array default operator 2015-10-19 21:12:43 +01:00
Christoph M. Wintersteiger d14a471cfd Merge branch 'ag-iz3_exception' of https://github.com/agriggio/z3 into agriggio-ag-iz3_exception 2015-10-19 15:20:50 +01:00
Christoph M. Wintersteiger 6749c19ab1 Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3 
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
 2015-10-19 15:14:45 +01:00
Christoph M. Wintersteiger 954a629296 Merge branch 'zkincaid-uint' 2015-10-19 15:01:07 +01:00
Christoph M. Wintersteiger 059c58e6d8 Merge branch 'uint' of https://github.com/zkincaid/z3 into zkincaid-uint 2015-10-19 15:00:43 +01:00
Christoph M. Wintersteiger 0c774e59c3 Merge branch 'Dmitriy403-WpedanticFix' 2015-10-19 14:57:49 +01:00
Christoph M. Wintersteiger 57db321daf Merge branch 'WpedanticFix' of https://github.com/Dmitriy403/z3 into Dmitriy403-WpedanticFix 2015-10-19 14:57:34 +01:00
Christoph M. Wintersteiger 9d505ec7ff Merge branch 'unstable' of https://github.com/jmgrosen/z3 into jmgrosen 2015-10-19 14:53:06 +01:00