mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 19:01:50 +00:00
Code Activity
5912 commits 23 branches 48 tags 156 MiB
Commit graph

5912 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 4cae91b096 spacing, unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-17 08:07:23 -04:00
Christoph M. Wintersteiger 12c47348bc Merge pull request #761 from delcypher/bv2fpa_unbreak_cmake_build 
Unbreak the CMake build broken by 009af4455d
 2016-10-17 11:47:01 +01:00
Nikolaj Bjorner fe14a22baa adding enumeration tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 22:19:59 -04:00
Nikolaj Bjorner 4fda2adec8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-16 15:46:50 -04:00
Nikolaj Bjorner 58198d7cb6 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:45:39 -04:00
Nikolaj Bjorner aec59e4ff7 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:43:28 -04:00
Dan Liew b2381acceb Unbreak the CMake build broken by 009af4455d 
The commit added an additional source file and dependency but the
corresponding changes weren't added to the CMake build.
 2016-10-15 21:42:20 +01:00
Christoph M. Wintersteiger 13e3484d15 Merge pull request #759 from wintersteiger/fpa-unspec 
Refactored and fixed model conversion for unspecified FP values in theory_fpa.
 2016-10-15 18:43:28 +01:00
Christoph M. Wintersteiger 009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger ab4bb8194e Added unregister_decl to model_core 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger 58af4cae14 More consistent fp.* operators. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger 7e705a2d32 Bug fixes for underspecified FP operations. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger bc257211d6 Whitespace 2016-10-15 18:35:39 +02:00