mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
6583 commits 24 branches 48 tags 158 MiB
Commit graph

1189 commits

Author SHA1 Message Date
Murphy Berzish
f881e85470 remove old theory_str enums from api 2017-04-04 17:54:18 -04:00
Murphy Berzish
19de682b58 remove references to m_str_fid in api 2017-04-04 17:22:55 -04:00
Murphy Berzish
a8935e99bc Merge branch 'upstream-master' into develop 2017-04-04 16:47:30 -04:00
Nikolaj Bjorner
c4b26cd691 add bypass to allow recursive functions from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 16:38:15 -07:00
Nikolaj Bjorner
8f798fef1a fix python interface for string extract to take symbolic indices per bug report from Kun Wei 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 08:24:12 -07:00
Nikolaj Bjorner
62e87d6474 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:10:19 -07:00
Nikolaj Bjorner
1ab7ab9d74 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:09:36 -07:00
Murphy Berzish
5917a34226 Merge branch 'upstream-master' into develop 2017-03-14 15:04:17 -04:00
Nikolaj Bjorner
0668ba5f6c add pb shorthands to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:58:39 -07:00
Nikolaj Bjorner
7634f8b93e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-14 07:47:51 -07:00
Nikolaj Bjorner
1dd2de61ec add sum shorthand to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:43:26 -07:00
hume
0b1d564509 added no exception support to z3++.h 2017-03-14 18:11:00 +08:00
Murphy Berzish
94d5f242b8 Merge branch 'str-at-semantics' into develop 2017-03-13 14:40:40 -04:00
James Bornholt
559c5e5ae6 z3py: With tactical should not try to use context as a parameter 2017-03-11 16:09:25 -08:00
Nikolaj Bjorner
509f7409ba adding fixedpoint object to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-10 23:01:43 +01:00
Murphy Berzish
ab71dea82d theory_str refactoring 2017-02-28 17:47:55 -05:00
Murphy Berzish
9ac0d098ac Merge remote-tracking branch 'upstream/master' into release-1.0 2017-02-28 12:45:04 -05:00
Murphy Berzish
725352234d refactoring theory_str 2017-02-27 13:22:56 -05:00
George Karpenkov
be1e9918f0 Class Optimize#Handle should be static, 
as it already includes an explicit reference to the Optimize class.
 2017-02-27 18:49:02 +01:00
George Karpenkov
b3be83e7c5 Sane indentation + removing extra spaces for Optimize.java 2017-02-27 18:48:44 +01:00
George Karpenkov
d6c79facc7 Java API for getting the objective value as a triple 
See #911 for the motivation,
and e02160c674 for the relevant change
in C API.
 2017-02-27 18:42:44 +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
Murphy Berzish
235ea79043 Merge branch 'upstream-master' into release-1.0 
Conflicts:
	src/cmd_context/check_logic.cpp
	src/cmd_context/cmd_context.cpp
	src/cmd_context/cmd_context.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_context.cpp
 2017-02-18 15:04:44 -05:00
Murphy Berzish
90705cfd5f remove todo from str api 2017-02-17 13:28:52 -05:00
Nikolaj Bjorner
c67cf1653c use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-15 08:46:58 -08:00
Nikolaj Bjorner
216e17e5e2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-13 08:16:43 -08:00
Nikolaj Bjorner
e7a21dfac2 add par_and_then 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-13 08:16:39 -08:00
Nikolaj Bjorner
6fcba26ea6 make parameters accessible from expressions. Issue #896 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-12 09:56:49 -08:00
Nikolaj Bjorner
b3dabc7ccf add missing mod/rem/is_int functionality to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:28:15 -05:00
Nikolaj Bjorner
4c6efbbc8b expose numerator/denominators for Martin and Giles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:02:51 -05: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
Nikolaj Bjorner
2e89c2de3d add par_or tactic to C++ API. #873 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 09:35:04 -08:00
Nikolaj Bjorner
37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Nikolaj Bjorner
60783e5696 fix regression for z3num 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 13:26:58 -08:00
Nikolaj Bjorner
4ec4abd7e3 fix test for int-value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-23 13:31:43 -08:00
Nikolaj Bjorner
1bfd09e16b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-19 19:31:24 -08:00
Nikolaj Bjorner
e23509797a access parameters from Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 19:28:20 -08: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
Nikolaj Bjorner
dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Daniel Perelman
3370adcdff Mark void DummyContracts as Conditional to avoid compiling their arguments. 2017-01-11 17:02:26 -08:00
Christoph M. Wintersteiger
9f49905582 Formatting, whitespace, and Z3_API annotations. 2017-01-10 21:05:27 +00:00
Christoph M. Wintersteiger
d8d869822f Cleaned up #include<iostream> in api* objects. 2017-01-10 21:04:44 +00: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
e9edcdc6e6 moderate exception behavior for issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-05 16:09:16 -05:00
Nikolaj Bjorner
f443bfed87 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-04 19:05:52 -08:00
Nikolaj Bjorner
ddf4bc548f allow disabling exceptions from C++. Issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 19:04:43 -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
2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner
c44dd01292 fix missing else reported in #855 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:56:14 -08:00