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

5215 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
Nuno Lopes
417c80edbc fix mem leak in quantifier_info::insert_qinfo on timeout 2016-04-19 02:17:12 -07:00
Nikolaj Bjorner
b512212d41 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:31:36 -07:00
Nikolaj Bjorner
3a6218ac21 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:30:52 -07:00
Nikolaj Bjorner
cff843ca59 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-18 17:22:54 -07:00
Nikolaj Bjorner
4cb57cd4da fix regression introduced by using ref-vectors on non-ref'ed output parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:22:47 -07:00
Nikolaj Bjorner
c3f4124a9f trace down recent exposed regression in goal2sat, incorporate Scott's suggestion on making vector<std::string inaccessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 14:50:10 -07:00
Nikolaj Bjorner
81232808ba add handling for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 11:17:33 -07:00
Nikolaj Bjorner
4761f4f191 add handling for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 11:14:40 -07:00
Christoph M. Wintersteiger
5d0db6d256 Fixed memory leak in goal::update. 
Fixes #567
 2016-04-18 17:18:16 +01:00
Christoph M. Wintersteiger
6db0a15d29 Fixed potential memory leakage issues in fpa2bv_converfter 2016-04-18 17:17:31 +01:00
Christoph M. Wintersteiger
3ffcea0fe4 whitespace 2016-04-18 16:52:12 +01:00
Christoph M. Wintersteiger
14e1e247a4 Revert "nmake->make, little error" 
This reverts commit 8287f7ba82.
 2016-04-17 11:35:27 +01:00
Nikolaj Bjorner
7a317a4f07 Merge pull request #566 from xavdel/patch-1 
nmake->make, little error
 2016-04-16 17:46:04 -07:00
Xavier DELPIERRE
8287f7ba82 nmake->make, little error 2016-04-17 02:39:35 +02:00
Nikolaj Bjorner
0094b36636 fix bounds check to fix segfault reported in issue #565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 12:25:29 -07:00
Nikolaj Bjorner
1c8e0918d8 move to std::vector in replayer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 10:08:29 -07:00
Nikolaj Bjorner
d383fd851a move vector<std::string to std::vector<std::string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:34:27 -07:00
Nikolaj Bjorner
4ebf392da7 Fixes #564: use std::vector on std::strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:26:13 -07:00
Nikolaj Bjorner
0f93853a4c remove labels from evaluation result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 13:17:10 -07:00
Nikolaj Bjorner
aa7b5d80fe extract array terms for evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 09:41:50 -07:00
Nikolaj Bjorner
2033719c14 fix optimization pre-processing reported by Gereon Kremer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-09 20:58:57 -07:00
Nikolaj Bjorner
6e57015a12 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-09 16:51:42 -07:00
Nikolaj Bjorner
cc6f72aba7 fix handing of ite conditions that have to be included in projection, thanks to bug report by Zak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-10 01:48:35 +02:00
Christoph M. Wintersteiger
16e487b32a Bugfix for ackermann helper 2016-04-08 17:20:09 +01:00
Christoph M. Wintersteiger
bd0bd08ecf add is_considered_uninterpreted checks into acker_helper 2016-04-08 16:58:11 +01:00
Christoph M. Wintersteiger
0597b579b1 Bugfixes for bvarray2uf conversion. 2016-04-07 19:10:31 +01:00
Christoph M. Wintersteiger
5971c20653 Bugfixes for bv_trailing. 2016-04-07 13:08:17 +01:00
Christoph M. Wintersteiger
3a532c08a6 Bugfix for func_interp else-case compression 2016-04-06 19:24:08 +01:00
Christoph M. Wintersteiger
e662427060 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 15:39:37 +01:00
Christoph M. Wintersteiger
e527aca296 Bugfix for unspecified else-case in func_interps. 2016-04-06 15:39:32 +01:00
Nuno Lopes
e2b7ad246a bv_trailing: fix compiler warning + use of ast_manager 2016-04-06 15:34:31 +01:00
Christoph M. Wintersteiger
7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01:00
Christoph M. Wintersteiger
86ca224460 Merge pull request #554 from MikolasJanota/trailing 
Trailing
 2016-04-06 14:25:58 +01:00
Mikolas Janota
7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Mikolas Janota
dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00