mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-20 14:20:31 +00:00
Code Activity
20040 commits 41 branches 52 tags 175 MiB
Commit graph

20040 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
18d9ab7424 Merge pull request #271 from NikolajBjorner/master 
Make Groebner basis computation interruptable. Exponsed in issue #269
 2015-10-28 11:43:46 -07: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
1523626a2b Merge pull request #270 from NikolajBjorner/master 
fix issues #240, #250
 2015-10-28 09:49:29 -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
1756dd1c13 Merge pull request #268 from NikolajBjorner/master 
Fix for issue #263
 2015-10-27 19:26:52 -07: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
Murphy Berzish
1f3c5cebbf variable classification (WIP) 2015-10-26 15:43:31 -04: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
Nikolaj Bjorner
5c572d8fea Merge pull request #261 from paulp/help-tactic 
Changed references to help-tactics to help-tactic.
 2015-10-25 16:06:41 -07: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
ad58226f43 Merge pull request #256 from NikolajBjorner/master 
fixing issue #254
 2015-10-22 09:55:17 -07: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
5e4f209292 Merge pull request #255 from NikolajBjorner/master 
fix another regression and missing detection of bounds, Issue #254
 2015-10-22 08:55:13 -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
Murphy Berzish
c08f4371f4 begin model generation, wip 2015-10-21 21:32:38 -04:00
Nikolaj Bjorner
87921f4552 Merge pull request #253 from NikolajBjorner/master 
fix unbounded, issue #252
 2015-10-21 14:44:09 -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
a1eee6275f Bugfix for C++ examples. 
Relates to #26
 2015-10-19 19:03:36 +01:00
Christoph M. Wintersteiger
3aedcf0a7e Merge branch 'zkincaid-172' 2015-10-19 19:01:55 +01:00
Christoph M. Wintersteiger
498bafcc4b Merge branch 'ocamlfind_stublibs' of https://github.com/zkincaid/z3 into zkincaid-172 2015-10-19 17:05:55 +01:00
Christoph M. Wintersteiger
6f3b957300 Merge branch 'zardus-76' 2015-10-19 16:52:08 +01:00
Christoph M. Wintersteiger
eb0cdc42d1 Merge branch 'pypy-fix' of https://github.com/zardus/z3 into zardus-76 
# Conflicts:
#	scripts/mk_util.py
 2015-10-19 16:51:43 +01:00