mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-12 23:46:39 +00:00
Code Activity
7963 commits 42 branches 51 tags 169 MiB
Commit graph

219 commits

Author SHA1 Message Date
Nikolaj Bjorner
6e87622c8a remove references to deprecated uses of PROOF_MODE #1531 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-10 13:55:01 -05:00
Bruce Mitchener
878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Bruce Mitchener
ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner
5ee30a3cd9 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:24 +01:00
Nikolaj Bjorner
161b6a9983 increase minor version, update java/.net apis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:51:37 -08:00
Nikolaj Bjorner
795e0c641a add method to create bit-vectors directly from an array of Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 14:44:59 -08:00
Nikolaj Bjorner
dbb35b951c make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 08:51:16 -08:00
Nikolaj Bjorner
c9f540b066 additional array functions exposed over API, ping #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:08:48 -07:00
Christoph M. Wintersteiger
db398eca7a Tabs, formatting. 2017-09-17 17:50:05 +01:00
Christoph M. Wintersteiger
d8a02bc040 Fixed AST translation functions in .NET and Java APIs. Fixes #1073. 2017-06-14 13:24:54 +01:00
Nikolaj Bjorner
b978f78c21 add sequence recognizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 20:35:35 -07:00
Nikolaj Bjorner
c2acbc2957 port FuncDecl copy to dotnet, continuation of #1073 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:11:28 -07:00
Nikolaj Bjorner
7023af4528 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-13 19:03:45 -07:00
Nikolaj Bjorner
a59ee8032c fix unsoundness bug in axiomatization of str.at. #1067 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:02:59 -07:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Nikolaj Bjorner
efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner
52e0f3b539 add string accessors to managed APIs #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:10:49 -07:00
Christoph M. Wintersteiger
248dd601ae Whitespace, newlines 2017-05-10 12:44:25 +01:00
Nikolaj Bjorner
e02160c674 expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:07:40 -08:00
Nikolaj Bjorner
3a0e9e8f53 add itos/stoi conversion to API. Issue #895 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 11:31:13 -05:00
Christoph M. Wintersteiger
5c1ffe13d1 x64 build fix for .NET 3.5 API 2017-01-18 13:06:28 +00:00
Christoph M. Wintersteiger
a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Daniel Perelman
3370adcdff Mark void DummyContracts as Conditional to avoid compiling their arguments. 2017-01-11 17:02:26 -08:00
Nikolaj Bjorner
8d09b6e4a8 add at-least and pbge to API, fix for issue #864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:23:00 -08:00
Nikolaj Bjorner
ae9a3bfc24 add operator for issue #860 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 09:14:09 -08:00
Nikolaj Bjorner
976fadf771 add missing complement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:21:57 +01:00
Nikolaj Bjorner
0473d2ef56 add regular expression features to C# API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:17:13 +01:00
Nikolaj Bjorner
4e25bffab6 add range constructor to .NET API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:33:02 +01:00
Christoph M. Wintersteiger
9053e6eba6 Resolved merge conflicts. Added FPA API input validity checks. 2016-11-15 20:19:40 +00:00
Christoph M. Wintersteiger
c81ee05098 Fixes for .NET Core build 2016-11-02 13:36:29 +00:00
Christoph M. Wintersteiger
95d7b33ebb Added is_numeral_negative to .NET and Java APIs 2016-10-27 15:07:10 +01:00
Christoph M. Wintersteiger
c573a7446b Added FPA numeral predicates to .NET API 2016-10-26 18:44:25 +01:00
Christoph M. Wintersteiger
e381cef92c Marked .NET Z3Exception as serializable 2016-10-26 15:12:10 +01:00
Nikolaj Bjorner
461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:32:13 -07:00
Christoph M. Wintersteiger
abcb6040d4 Refactored FPA numeral accessors. 2016-10-24 12:53:57 +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
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
Christoph M. Wintersteiger
9548b88e71 Added dummy code contracts for .NET Core/CoreCLR builds. 2016-10-06 16:24:49 +01:00
Nikolaj Bjorner
310c0f31a1 use type constrsaints for co-variant subtying to enable .net 3.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 12:07:06 +08:00
Christoph M. Wintersteiger
ff3c630207 .NET API: Added MkMul from IEnumerable. 2016-08-09 16:36:32 +01:00
Nikolaj Bjorner
cb2d8d2107 add detection of non-fixed variables to consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 19:12:41 -07:00
Nikolaj Bjorner
074f1ad778 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 11:20:23 -07:00
Nikolaj Bjorner
14f29e7265 add basic built-in consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:20:17 -07:00
Christoph M. Wintersteiger
7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger
0d83f99d8d Fixed comment 2016-07-28 18:06:26 +01:00
Christoph M. Wintersteiger
3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner
5f5ef8b38d adding support for distinct for dt2bv, re-entry harness for ~Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 09:02:56 -07: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
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