mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
4327 commits 23 branches 48 tags 157 MiB
Commit graph

3545 commits

Author SHA1 Message Date
Nikolaj Bjorner 4550b7ed91 Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-12-07 03:27:04 +00:00
Andres Notzli ced9ba17e9 Fix misc issues in Python API docstrings 2015-12-06 19:00:17 -08:00
Nikolaj Bjorner b5fcbd7099 Merge branch 'mono_dotnet_bindings' of https://github.com/delcypher/z3-1 2015-12-06 13:51:43 -08:00
Nikolaj Bjorner 89fe24342d fix size_t mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 11:06:58 -08:00
Nikolaj Bjorner 40e9e4c7f8 more rewrites 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 10:44:19 -08:00
Nikolaj Bjorner 4fe0e07080 indexof 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 16:36:11 -08:00
Nikolaj Bjorner 5296009f46 ground string rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 15:38:54 -08:00
Nikolaj Bjorner 75359c580e add basic rewriting to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 12:02:33 -08:00
Nikolaj Bjorner c04f75cdbb fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 10:30:08 -08:00
Dan Liew c8a2b6645a Teach the build system to generate and install a pkg-config file for the 
".NET" bindings. This file is required for Monodevelop to find the
bindings because Monodevelop uses pkg-config to find packages
(it doesn't use the GAC).

For lack of a better name the GAC (and pkg-config) package name is now
``Microsoft.Z3.Sharp``. I don't want to call it ``Microsoft.Z3`` because
someone may want to create a ``Microsoft.Z3.pc`` file in the future for
the native Z3 library (i.e. C++ or C bindings).

In addition there is a new utility function ``configure_file()``
which reads a template file, applies some substitutions and writes
the result to another file. This very similar to what CMake does.

There is a new environment variable ``Z3_INSTALL_PKGCONFIG_DIR``
which allows pkgconfig directory to be controlled for the install.
 2015-12-05 07:52:31 +00:00
Dan Liew 61d1cd524e Teach the build system to build and install the ".NET bindings" 
under non Windows systems (i.e. Using mono).

Building these bindings is unfortunately on by default because
I didn't want to change the command line interface (i.e. ``--nodotnet``)
which people might be relying on. This should really be changed to
match the other binding flags (e.g. ``--java``) but I will leave
this for now.

To perform the build a C# compiler and the GAC utility are required.
The script will try to automatically detect them but the user can
override this by setting the ``CSC`` and ``GACUTIL`` environment
variables.

In order for the ".NET bindings" to be installed the assembly
(``Microsoft.Z3.dll``) needs to have a strong name which means
we need a Strong name key file which is what the
``Microsoft.Z3.mono.snk`` is for. This is the public and private
key so this key **must never** be used for checking integrity. Instead its
only purpose is to avoid any name clashes in the GAC.

It is also worth noting that slightly different flags needs to
be passed to the C# compiler on non Windows platforms. I don't
understand why some of the flags are being used on Windows but I left
a comment there that hopefully someone can fix...
 2015-12-05 07:52:31 +00:00
Nikolaj Bjorner b77e387265 value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 15:26:53 -08:00
Nikolaj Bjorner a8e366aa24 add basic string factory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 15:24:29 -08:00
Nikolaj Bjorner 75c935a4cb add tokens to parse strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 12:09:15 -08:00
Nikolaj Bjorner 4bbe1d4674 remove unused min-aggregate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 09:23:36 -08:00
Nikolaj Bjorner 3f02beb820 reset-assertions resets everything (also declarations, and we take scopes) when global-declarations is false. v2.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-03 10:18:40 -08:00
Nikolaj Bjorner 8e5dec882b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-03 10:01:41 -08:00
Nikolaj Bjorner a4d9642cf2 parsing of SMT 2.5 style string literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-03 09:46:18 -08:00
Christoph M. Wintersteiger 00271e5531 C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes. 2015-12-03 17:33:25 +00:00
Nikolaj Bjorner 5d61c871b0 add some of the SMT2.5 features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-02 19:14:47 -08:00
Nikolaj Bjorner e9a2b7f9f0 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-02 18:41:22 -08:00
Nikolaj Bjorner e2565d8d82 add some of the SMT2.5 features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-02 18:41:10 -08:00
Christoph M. Wintersteiger d23dce4f7b Bugfix for finite domains in Python API. 2015-12-02 22:34:09 +00:00
Christoph M. Wintersteiger b77f20fb0c Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-02 17:06:42 +00:00
Christoph M. Wintersteiger 2f86ab98a8 Added finite-domain expressions to the Python pretty printer 2015-12-02 17:04:06 +00:00
Christoph M. Wintersteiger 5510e0ddef Added finite-domain constant to Z3_decl_kind 2015-12-02 17:03:37 +00:00
Christoph M. Wintersteiger 5a43d8a469 Whitespace 2015-12-02 17:02:39 +00:00
Christoph M. Wintersteiger cbda38ee80 Added finite domain expressions and numerals to the .NET, Java, and Python APIs. 
Relates to #318
 2015-12-02 17:01:52 +00:00
Nikolaj Bjorner 6580f1daf3 expose main interpolation routines in C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-02 07:40:06 -08:00
Christoph M. Wintersteiger 9e756fb6db Warning fix for Comparable<T> in Java API 2015-12-02 14:42:36 +00:00
Christoph M. Wintersteiger 00ce124db3 Bugfix for Z3_is_numeral for finite-domain numerals. 
Relates to #318
 2015-12-02 14:41:46 +00:00
Christoph M. Wintersteiger 52bbd67cd3 Whitespace 2015-12-02 14:40:47 +00:00
Nikolaj Bjorner 485ac9c39d add macro for converting std::vectors to pointers (leaking abstraction) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-01 16:35:03 -08:00
Nikolaj Bjorner b3e8020c88 bind variables in queries generated from Horn tactic to enforce that rule formulas don't contain free variables. Issue #328 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-01 14:47:33 -08:00
Nikolaj Bjorner aa777bd5c6 Fix for #343. Optimizations introduced on 8-10-2015 were too agressive. Remove unreferened variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-01 13:43:47 -08:00
Nikolaj Bjorner 9fa4bf2f8f Fix for #343. Optimizations introduced on 8-10-2015 were too agressive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-01 13:41:57 -08:00
Dan Liew b0bc50a75c Fixed stray UTF-8 Byte order mark in `InterpolationContext.cs`. 
Old versions of the mono compiler don't like it.
 2015-11-30 15:02:02 +00:00
Nuno Lopes 5d289a8da5 fix leak in asserted_formulas::propagate_values() for proof generation mode 
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-29 10:49:52 +00:00
Nuno Lopes d175c99542 fix ast leak in asserted_formulas::propagate_values() 
Fixes issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-27 20:09:17 +00:00
Christoph M. Wintersteiger db2f973e3e Fixed initialization order in bvarray2uf_tactic 2015-11-27 15:34:06 +00:00
Nuno Lopes 2739930900 fix build with clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-27 12:13:44 +00:00
Christoph M. Wintersteiger 8eea6fd775 Bugfix for FPA float to float conversion. 
Fixes #337
 2015-11-24 17:21:40 +00:00
Christoph M. Wintersteiger 5e37cf9bbf Removed potentially unnecessary string decoding in Python API. 2015-11-23 18:41:31 +00:00
Christoph M. Wintersteiger 6aa5ec9f77 Eliminated unused variables 2015-11-23 13:12:05 +00:00
Christoph M. Wintersteiger 59c1944f92 Bugfix for FP casts (float to float conversion). 
Fixes #331.
 2015-11-22 14:49:04 +00:00
Nuno Lopes d9bafc3fba rewrite scoped_timer for linux 
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory

This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:40:52 +00:00
Nuno Lopes b26735a887 fix build with gcc 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:24:30 +00:00
Nikolaj Bjorner c1a6163bda disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 14:34:31 -08:00
Nikolaj Bjorner 665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:43:27 -08:00
Nikolaj Bjorner fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00