mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
5394 commits 49 branches 53 tags 182 MiB
Commit graph

5394 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6895cc7cc6 remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:21:15 -07:00
Nikolaj Bjorner
e375be767d remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:20:20 -07:00
Christoph M. Wintersteiger
140f0bb794 ML API build fix 2016-05-03 13:34:20 +01:00
Christoph M. Wintersteiger
86126e2c01 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-05-03 11:52:21 +01:00
Christoph M. Wintersteiger
126e44dbd8 Merge pull request #5 from martin-neuhaeusser/cwinter 
Fix bug in OCaml API where double values have been wrapped incorrectly.
 2016-05-03 11:45:36 +01:00
Nikolaj Bjorner
67e49b4adc fixing model-based-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-01 17:15:20 -07:00
Nikolaj Bjorner
22507281cf fix model generation in opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 12:23:46 -07:00
Nikolaj Bjorner
4b940bde11 fix compilation of unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 11:46:25 -07:00
Nikolaj Bjorner
e29adbf304 fix issues #581: nested timeouts canceled each-other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 11:18:34 -07:00
Nikolaj Bjorner
a020b13f10 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-29 19:08:29 -07:00
Nikolaj Bjorner
2428bf18f1 add model correction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-29 19:08:10 -07:00
Nikolaj Bjorner
121386779a Merge pull request #580 from yaqwsx/expr_operators_in_c++ 
Add srem, urem, shift, ext operators to c++ api
 2016-04-29 18:51:14 -07:00
Nikolaj Bjorner
c75fd02c95 qsat-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-28 21:31:16 -07:00
xlauko
ae2821dea1 Add srem, urem, shift, ext operators to c++ api 2016-04-28 21:58:05 +02:00
Nikolaj Bjorner
c414c6b5fd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-28 09:48:04 -07:00
Nikolaj Bjorner
932ef442ae model based opt dev 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-28 09:47:55 -07:00
Christoph M. Wintersteiger
47ec3b1f87 Build fix for VS2012 2016-04-28 13:17:39 +01:00
Christoph M. Wintersteiger
f3c74a06eb debug fix for mpf_manager 2016-04-28 12:54:10 +01:00
Christoph M. Wintersteiger
deea4e92f2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-28 12:52:49 +01:00
Christoph M. Wintersteiger
cba82325de Build fix for old systems that don't have a float remainder(...) function. 2016-04-28 12:52:36 +01:00
Nikolaj Bjorner
83d84dcedd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-27 15:09:12 -07:00
Nikolaj Bjorner
6aa6102891 factor out model-based-opt code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 15:08:10 -07:00
Christoph M. Wintersteiger
10cc8c3a75 Build fix for VS2012 and earlier. 2016-04-27 20:15:22 +01:00
Nikolaj Bjorner
68c7d64d00 adding model-based opt facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 11:18:20 -07:00
Christoph M. Wintersteiger
bf49f81622 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-27 13:26:23 +01:00
Nikolaj Bjorner
51e34e8b5f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-26 17:15:36 -07:00
Nikolaj Bjorner
a1aa166ef5 adding local optimization to qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-26 17:15:24 -07:00
Christoph M. Wintersteiger
4e066afa0d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-26 21:13:19 +01:00
Christoph M. Wintersteiger
6455bf8114 New implementation for mpf_manager::rem. 
Relates to #561
 2016-04-26 21:13:02 +01:00
Christoph M. Wintersteiger
fb86b01a8b Merge pull request #576 from delcypher/cmake_fix_windows_install 
[CMake] Fix install of libz3.dll on Windows
 2016-04-26 21:08:24 +01:00
Christoph M. Wintersteiger
e24c6c14e0 Merge pull request #568 from delcypher/cmake_java_bindings 
Teach CMake to build and install the Java bindings
 2016-04-26 21:05:26 +01:00
Nikolaj Bjorner
e31913691f Merge pull request #575 from delcypher/cmake_minor_dotnet_tweaks 
[CMake] Minor ".NET" build tweaks
 2016-04-26 08:23:57 -07:00
Dan Liew
fd7b8fe1ab [CMake] On Windows fix the `install` target so that it installs 
``libz3.dll``.

I've left a comment about the installation of ``libz3.lib``. I'm not
sure if we want that installed or not.
 2016-04-26 11:49:46 +01:00
Dan Liew
626e0736d2 [CMake] Implement installation of ".NET" bindings on Windows. 
We don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead we just copy into
installation directory.

There are several reasons for this:

* We can't install the Z3_DOTNET_ASSEMBLY_DLL into the gac in a portable
  way like we can with mono (i.e. the ``-root`` flag).
* It isn't best practice to use ``gacutil.exe``
  on Windows to install into the GAC, see
  https://msdn.microsoft.com/en-us/library/yf1d93sz(v=vs.110).aspx .

Taking this approach should be sufficient because we can now do
something like this

```
mkdir build
cmake -G Ninja -DCMAKE_INSTALL_PREFIX=<some_path> ../
ninja
mkdir <some_path>
ninja install
```

and then put the contents of <some_path> into a zip file which creates a redistributable zip file for Windows.
 2016-04-26 11:24:16 +01:00
Dan Liew
7213280d9b [CMake] Emit a warning when configuring to build the `.NET` bindings under 
a multi-configuration generator (e.g. Visual Studio).

The warning concerns different generated files clobbering each other.
Unfortunately there isn't a clean way to fix this right now. See
http://public.kitware.com/pipermail/cmake/2016-March/063101.html
 2016-04-26 08:56:46 +01:00
Dan Liew
7cedf79b38 [CMake] When building the ".NET" bindings emit `Microsoft.Z3.dll` 
and ``Microsoft.Z3.xml`` to the root build directory rather than
``<root_build_directory>/src/api/dotnet``.

This fixes #573 which makes the behaviour consistent with the Python
build system.
 2016-04-26 08:56:25 +01:00
Nikolaj Bjorner
271b56aa1b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-24 09:21:10 -07:00
Nikolaj Bjorner
d97bddc3b5 revert to legacy syntax to enable older versions of .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-24 09:21:05 -07:00
Christoph M. Wintersteiger
be424d9cbb Bugfixes for fp.roundToIntegral and fp.rem. 
Relates to #561
 2016-04-24 15:14:16 +01:00
Christoph M. Wintersteiger
952e3afb90 bugfix for hwf_manager::rem 2016-04-24 15:11:24 +01:00
Christoph M. Wintersteiger
3131f29816 whitespace 2016-04-24 15:11:03 +01:00
Nikolaj Bjorner
643a87cb5b overloading support for C# expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-23 22:03:27 -07:00
Nikolaj Bjorner
662e43d264 overloading support for C# expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-23 15:50:30 -07:00
Nikolaj Bjorner
e4b7ac37f3 add overloading for arithmetical expressions in C# to handle common cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-22 13:58:02 -07:00
Nikolaj Bjorner
8ee49d16df Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-21 10:49:22 -07:00
Nikolaj Bjorner
20a6b41c5c coalescing is-int check for python 2.x, issue #572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-21 10:49:16 -07:00
Nikolaj Bjorner
d0175b96b8 guarding against null symbols creeping in. Issue #571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-20 14:07:45 -07:00
Martin R. Neuhaeusser
436113896d Fix typo in OCaml bindings 2016-04-19 12:51:16 +02:00
Nuno Lopes
417c80edbc fix mem leak in quantifier_info::insert_qinfo on timeout 2016-04-19 02:17:12 -07:00
Martin R. Neuhaeusser
6889767c9a Fix bug in OCaml API where double values have been wrapped incorrectly. 
This patch fixes a segmentation fault that occurs due to incorrect
wrapping of double values in the OCaml API.
 2016-04-19 10:10:28 +02:00