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

4000 commits

Author SHA1 Message Date
Nikolaj Bjorner
4fd1f4a65c add handler for abuse of OP_IMPLIES 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 11:34:55 -07:00
Christoph M. Wintersteiger
89e99c7b4b Fixed use of mk_th_axiom in theory_fpa. 
Relates to #227
 2015-10-31 13:57:17 +00:00
Nikolaj Bjorner
ac3edbbaaa add line/position information to unsupported command reports per zeph pull request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 19:23:31 -07:00
Nikolaj Bjorner
b19fbe4429 make sure to bring constraints into clausal form before using the th_axiom assertion. Old version should not have been used as a template for copying, as in issue #227 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 15:55:18 -07:00
Nikolaj Bjorner
7838213675 eliminate to_real coersions to make mixed integer problems easier to digest. Issue #277 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 15:12:21 -07:00
Nikolaj Bjorner
f2c0a82726 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-30 14:14:23 -07:00
Christoph M. Wintersteiger
8fffa9f188 Removed trailing whitespace. 2015-10-30 12:20:41 +00:00
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
Nikolaj Bjorner
559f373588 adding PB operators to Python API. remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 17:13:24 -07:00
Nikolaj Bjorner
7f5495b134 adding PB operators to Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 17:09:42 -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