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

4328 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 32f3bd17fb adding translation routine to context to address enhancement request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 14:30:54 -07:00
Nikolaj Bjorner 9acaa49a05 adding translation routine to context to address enhancement request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 14:28:21 -07:00
Nikolaj Bjorner 4b1a730f46 API method for translating context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 12:47:16 -07:00
Nikolaj Bjorner fb624780d5 add checks in internalizer for issues of the form #227 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 12:41:57 -07:00
Christoph M. Wintersteiger 88064fc172 minor theory_fpa refactoring 2015-10-31 19:16:09 +00:00
Christoph M. Wintersteiger 1d7aa9ba2f Fixed rewriter bug in theory_fpa. 2015-10-31 18:53:40 +00:00
Christoph M. Wintersteiger 8491b3bebe Revert "Fixed use of mk_th_axiom in theory_fpa." 
This reverts commit 89e99c7b4b.
 2015-10-31 18:51:32 +00:00
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 2bd2dd3334 Merge pull request #285 from NikolajBjorner/master 
add line/position information to unsupported command reports per zeph…
 2015-10-30 21:21:13 -07: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 eb2193f5ae Merge pull request #283 from NikolajBjorner/master 
make sure to bring constraints into clausal form before using the th_…
 2015-10-30 16:06:19 -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 5489d60874 Merge pull request #282 from NikolajBjorner/master 
enable further simplifications to reduce coercions
 2015-10-30 15:13:47 -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