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

4578 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