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

5834 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger bea7bc5e30 Bugfix for bv2fpa_converter. Fixes #767. 2016-10-26 16:32:44 +01:00
Christoph M. Wintersteiger e381cef92c Marked .NET Z3Exception as serializable 2016-10-26 15:12:10 +01:00
Christoph M. Wintersteiger 93346380e0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 14:08:50 +01:00
Christoph M. Wintersteiger ead970b477 Bugfix for Python API. 
Thanks to John D. Ramsdell for reporting this issue (http://stackoverflow.com/questions/39584779/why-is-the-sort-of-a-bound-variable-forced-not-to-be-a-finite-domain-sort).
 2016-10-26 14:08:33 +01:00
Christoph M. Wintersteiger 1494c605f9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 12:59:49 +01:00
Christoph M. Wintersteiger 86285e1641 disabled unnecessary assertion 2016-10-26 12:59:26 +01:00
Nikolaj Bjorner da4289fadc fix unit tests for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:47:48 -07:00
Nikolaj Bjorner d0c5b86a2a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-25 20:32:20 -07:00
Nikolaj Bjorner 461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:32:13 -07:00
Christoph M. Wintersteiger c7fddf80c2 fixed unhandled case warning in test/qe_arith.cpp 2016-10-25 14:34:00 +01:00
Christoph M. Wintersteiger 8c5c564d6c fixed initialization order warning in pb2bv_rewriter 2016-10-25 14:31:29 +01:00
Christoph M. Wintersteiger 6ea45b4d65 fix for Python API installation 2016-10-25 14:23:55 +01:00
Nikolaj Bjorner fefd00aa49 fix sign of constant in pb constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 20:28:56 -07:00
Nikolaj Bjorner b82b53dc34 add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 17:41:52 -07:00
Nikolaj Bjorner e4d2c5867a remove dead (and incorrect) code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 15:52:47 -07:00
Nikolaj Bjorner a880e5f49b fix incorrection assertion when checking signs of literals, exposed by miTLS regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:12:36 -07:00
Nikolaj Bjorner c68c56b0e7 fix incorrect assertion when checking signs of literals, exposed by mitls regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:09:27 -07:00
Nikolaj Bjorner 33e7dccd42 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 09:11:02 -07:00
Nikolaj Bjorner 0439b795b4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-24 09:10:40 -07:00
Nikolaj Bjorner 99002aeffb Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-24 08:25:19 -07:00
Nikolaj Bjorner 6cf54a226e a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 08:25:02 -07:00
Christoph M. Wintersteiger 79f1d7b4d4 fixed GCC build issue in tests 2016-10-24 15:27:47 +01:00
Christoph M. Wintersteiger df2a569d25 Replaced antiquated header with modern equivalent. 2016-10-24 13:29:17 +01:00
Nikolaj Bjorner 4f3f21bff1 disable local optimization in presence of non-linear constraints, addresses issue #758 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 21:45:35 -07:00
Nikolaj Bjorner a1b7e41d7f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-23 20:53:14 -07:00
Nikolaj Bjorner b92bd89a45 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:53:10 -07:00
Nikolaj Bjorner b476784f23 add missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:52:44 -07:00
Nikolaj Bjorner f609ee6298 add documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:44:25 -07:00
Nikolaj Bjorner ec5d4f1119 add example to exercise at-most-1 constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:35:20 -07:00
Nikolaj Bjorner 3778048eb4 add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:31:59 -07:00
Nikolaj Bjorner 6d3430c689 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-22 21:51:11 -07:00
Nikolaj Bjorner e32e0d460d fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 21:50:45 -07:00
Nikolaj Bjorner 23b9d3ef55 fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 18:50:16 -07:00
Christoph M. Wintersteiger 5bd00d3f83 Bugfixes for the FPA API 2016-10-21 15:39:02 +01:00
Nikolaj Bjorner bb6d826908 use index j to avoid superficial, but typically flagged, name clash with internal index i 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-20 22:17:11 -07:00
Nikolaj Bjorner 9cd7b9b4f6 fix mutex finding for smt-core: it was returning mutexes for negations of literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-20 22:13:23 -07:00
Nikolaj Bjorner ef9486913b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-19 08:57:16 -07:00
Nikolaj Bjorner 527980e440 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-19 08:57:10 -07:00
Christoph M. Wintersteiger f97ffce479 Silenced GCC warning about empty loop body. 2016-10-19 12:31:35 +01:00
Christoph M. Wintersteiger f9bd8f674d whitespace 2016-10-19 12:31:06 +01:00
Christoph M. Wintersteiger 948bf9540f Fix for previous commit. 2016-10-19 12:07:33 +01:00
Christoph M. Wintersteiger 11997afb5d Fixed potential problems with invalidated iterators. 2016-10-19 12:00:34 +01:00
Nikolaj Bjorner 881e82e3fa remove legacy interface to dt2bv tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 23:04:17 -04:00
Nikolaj Bjorner 3aa7eab3e2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-18 22:37:08 -04:00
Nikolaj Bjorner d060359f01 add fd solver for finite domain queries 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 22:34:34 -04:00
Christoph M. Wintersteiger 4546915238 Fixed iterator invalidation bug in theory_arith_nl. 
Indirectly relates to #740
 2016-10-18 17:17:19 +01:00
Christoph M. Wintersteiger 9fef51553c Whitespace 2016-10-18 17:15:43 +01:00
Nikolaj Bjorner 948a1e600e undo breaking commit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 10:27:47 -04:00
Christoph M. Wintersteiger 5ac3bb04ee Tabs 2016-10-18 13:18:59 +01:00
Nikolaj Bjorner edaec81aa2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-17 14:53:13 -04:00