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

6025 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
5fee1ea3c0 removed unused variables 2016-10-24 14:08:33 +01:00
Christoph M. Wintersteiger
7517cf485e ML API bugfixes for FPA numeral accessors 2016-10-24 13:32:37 +01:00
Christoph M. Wintersteiger
df2a569d25 Replaced antiquated header with modern equivalent. 2016-10-24 13:29:17 +01:00
Christoph M. Wintersteiger
abcb6040d4 Refactored FPA numeral accessors. 2016-10-24 12:53:57 +01:00
Christoph M. Wintersteiger
0a11e8f3c0 Resolved rebase conflicts 2016-10-24 12:53:57 +01:00
Christoph M. Wintersteiger
8926b3311d Fixed FP numeral special value sig/exp extraction functions. 2016-10-24 12:52:07 +01:00
Christoph M. Wintersteiger
89d38385db Added functions to test FP numerals for special values. 2016-10-24 12:50:05 +01:00
Christoph M. Wintersteiger
6b474adc8a Added accessors to extract sign/exponent/significand BV numerals from FP numerals. 2016-10-24 12:50:05 +01:00
Christoph M. Wintersteiger
5716eaafed whitespace 2016-10-24 12:50:05 +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
Nikolaj Bjorner
9e4450228e adding unit test for enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-17 14:52:37 -04:00
Christoph M. Wintersteiger
7d37203653 Merge pull request #764 from delcypher/cmake_fixes2 
Fix a few CMake build bugs
 2016-10-17 18:45:20 +01:00
Dan Liew
289e51f455 [CMake] Fix building the Java bindings. 
This was broken due to 495ef0f055
and a914822346 adding and removing
source files without updating the CMake build.
 2016-10-17 18:30:49 +01:00
Dan Liew
462d3e8e8b [CMake] Unbreak building the .NET bindings. 
7fefe40f21 broke building the .NET
bindings by renaming the signing key without updating the CMake build.
 2016-10-17 18:19:31 +01:00
Dan Liew
03071db3ed [CMake] Fix building the examples when libz3 is built as a static library. 2016-10-17 18:19:31 +01:00
Dan Liew
4ef55505e7 [CMake] Fix #763 reported by @jirislaby. 
`INTERFACE` was the not appropriate usage requirement to use. However
it only caused a problem when USE_LIB_GMP was enabled. With `INTERFACE`
`-lgmp` was not specified on the link line so `libz3.so` did not have a
reference to the library and linking against `libz3.so` by clients
would fail with missing references to symbols in `libgmp`.
 2016-10-17 18:19:25 +01:00
Christoph M. Wintersteiger
2f6ef0f3be Removed unnecessary variables. 2016-10-17 16:33:09 +01:00
Christoph M. Wintersteiger
707dbd4173 Bugfix for bv2fpa (model) conversion. 
Relates to #740
 2016-10-17 16:19:27 +01:00
Nikolaj Bjorner
2a948da93b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-17 08:18:56 -04:00