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

4115 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 653416153d use appropriate MaxSAT solver even if there are no soft constraints. Also avoid PB constraints when all soft constraints are false. Reported by Klaus Becker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-02 08:18:51 -08: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 997c3a234d Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-30 14:15:34 -07:00
Nikolaj Bjorner b75780ce2b Merge pull request #280 from NikolajBjorner/master 
Add PB operators to Python API
 2015-10-30 14:15:24 -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 4923b50c53 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-30 06:31:22 -07:00
Christoph M. Wintersteiger 28ba92b298 Python 3.x issues 2015-10-30 06:31:16 -07:00
Christoph M. Wintersteiger 8fffa9f188 Removed trailing whitespace. 2015-10-30 12:20:41 +00:00
Christoph M. Wintersteiger 64fa2db3ff Python 3.x issues 2015-10-29 17:47:07 +00:00
Christoph M. Wintersteiger 7287478370 Fixed Python 3.x issue with commandline output from subprocess.Popen 2015-10-29 15:54:28 +00:00
Christoph M. Wintersteiger 88b027ecce Eliminated unused variable from C example. 2015-10-29 13:32:58 +00:00
Christoph M. Wintersteiger 2818e977b6 Fixed unused variable warnings in examples. 2015-10-29 13:20:56 +00:00
Christoph M. Wintersteiger 5cb4b1d188 Fix for example build rules. 2015-10-29 13:06:48 +00:00
Christoph M. Wintersteiger 5b01828df0 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-29 13:03:26 +00:00
Christoph M. Wintersteiger bd5b455c46 Refactored iz3 example to avoid compiler warnings. 2015-10-29 13:03:19 +00:00
Christoph M. Wintersteiger b47e9d74e9 Refactored example build rules to avoid compiler warnings. 2015-10-29 13:03:02 +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 41c6f22130 Merge branch 'kenmcmil-issue204' 2015-10-28 16:10:04 -07:00
Nikolaj Bjorner 4f7fdb5c14 fix merge conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 16:09:46 -07:00
Christoph M. Wintersteiger eb28ee8999 Python 3.x issues 2015-10-28 22:40:07 +00: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
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