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

81 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
976fadf771 add missing complement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:21:57 +01:00
Nikolaj Bjorner
a82b5e21fe add regular expression operations to C and C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:11:36 +01:00
Nikolaj Bjorner
feb801564b adding range to C API. Issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:28:27 +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
Nikolaj Bjorner
5d9820f3e2 add example of parsing with external declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-07 12:57:07 -07:00
Nikolaj Bjorner
619cce0a52 add mutex preprocessing to maxsat, add parsing functions to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-07 12:42:08 -07:00
Nikolaj Bjorner
527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Nikolaj Bjorner
2d9dced1c7 fix spacing, cast to Bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 20:18:31 -07:00
cttghc
758266b952 Fix omission of Z3_model_has_interp in z3++.h 2016-09-06 18:32:41 -05:00
AlexVonB
c6b0fc444c Fix VisualStudio 2010 compiler warning C4100 
When compiling with Visual Studio 2010 the buildlog warns of the following: `z3++.h: warning C4100: 'e' : unreferenced formal parameter` and `z3++.h: warning C4100: 'c' : unreferenced formal parameter`. This merge request removes this warning.
 2016-09-05 16:22:00 +02: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
2263be1b4d adding consequence examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:24:14 -07:00
Nikolaj Bjorner
0d0d504d62 change names of reserved identifiers. Issue #666 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 14:46:44 -07:00
Nikolaj Bjorner
4c786c5f70 add n-ary disjunction and conjunction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 08:15:50 -07:00
Nikolaj Bjorner
cd937c07f3 return proper ast-option from get_const_interp function insetad of raising exceptions from inside the C API. Fixes discrepancy with documentation and behavior across extensions of the API. Issue #587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 13:29:38 -07:00
xlauko
ae2821dea1 Add srem, urem, shift, ext operators to c++ api 2016-04-28 21:58:05 +02:00
Nikolaj Bjorner
20bbdfe31a moving remaining qsat functionality over 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:35:26 -07:00
Nikolaj Bjorner
f175f864ec merge useful utilities from qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:01:44 -07:00
Jan Mrázek
57265f6eb1 Add methods for obtaining numeral values in C++ API 2016-03-16 00:18:49 +01:00
Nikolaj Bjorner
8d61d36c3f add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 11:45:00 +00:00
Nikolaj Bjorner
a3c4972c85 seq API, tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-03 17:16:13 -08:00
Christoph M. Wintersteiger
b25f517a89 Bugfix for C++ API. 
Fixes #371.
 2015-12-11 14:03:41 +00:00
Christoph M. Wintersteiger
cc8e685f45 whitespace 2015-12-11 14:03:24 +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
Nikolaj Bjorner
fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00
Nikolaj Bjorner
0f602d652a remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 13:47:41 -08:00
Nikolaj Bjorner
b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
Nikolaj Bjorner
3bc94e08b3 move friend definitions to inlined functions. Issue #241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 13:24:13 -07:00
Christoph M. Wintersteiger
57db321daf Merge branch 'WpedanticFix' of https://github.com/Dmitriy403/z3 into Dmitriy403-WpedanticFix 2015-10-19 14:57:34 +01:00
Christoph M. Wintersteiger
1364f39f61 Merge pull request #218 from cgcgbcbc/fix/implies 
fix implies(expr const &, expr const &) in z3++.h
 2015-10-19 14:29:07 +01:00
Guang Chen
cef7ec2157 fix implies(expr const &, expr const &) in z3++.h 2015-09-13 13:29:06 +08:00
Dmitriy Trubenkov
ab88708f9a Remove extra semicolons in C++ headers. Useful for projects builded with -Wpedantic 2015-07-25 23:46:01 +03:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
23a6138d81 initialize potentially unused variables. Fixes issue #112 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-28 14:55:37 -07:00
Nikolaj Bjorner
562ed61a24 add shorthands for creating uninterpreted sorts to context API 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:30:37 -07:00