mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-13 18:54:43 +00:00
Code Activity
14140 commits 25 branches 49 tags 159 MiB
Commit graph

95 commits

Author SHA1 Message Date
Nikolaj Bjorner
78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner
7e174f50c1 use Z3_char_ptr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 09:14:10 -07:00
Nikolaj Bjorner
1203af83eb expose cardinality declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 12:30:25 -07:00
Nikolaj Bjorner
fcc7bd35e5 fix #2489 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-15 21:04:04 -07:00
Nikolaj Bjorner
f128398bf9 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:57:19 -07:00
Nikolaj Bjorner
86b98e3477 remove trc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-17 10:47:46 -07:00
Nikolaj Bjorner
ae982c5225 add tc and trc functionals for binary relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 04:12:45 +02:00
Nikolaj Bjorner
f55e4ccc41 support indexed relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
5536834019 add API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
dc0e9c1919 completing user print experience with seq/re #2200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 11:46:36 -07:00
Nikolaj Bjorner
9bc4914268 add nth remapping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:32:28 -07:00
Nikolaj Bjorner
092c25d596 fix #2007 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 18:37:30 -08:00
Bruce Mitchener
edf8ba44d1 Switch from using Z3_bool to using bool. 
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
 2018-11-20 11:27:09 +07:00
Bruce Mitchener
56bbed173e Remove usages of Z3_TRUE / Z3_FALSE. 
Now that this is all using stdbool.h, we can just use true/false.

For now, we leave the aliases in place in z3_api.h.
 2018-11-20 00:25:37 +07:00
Nikolaj Bjorner
b02fec91cc fixing python build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-01 09:34:42 -05:00
Nikolaj Bjorner
51a0022450 add recfun to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-27 11:41:18 -05:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
77d68409c2 handle null declarations for kind 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-01 08:43:32 -07:00
Nikolaj Bjorner
1cb3f7c792 fixing #1520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 18:03:13 -07:00
Nikolaj Bjorner
1eb8ccad59 overhaul of error messages. Add warning in dimacs conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 16:04:37 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
4f5775c531 remove interpolation and duality dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 08:33:48 -07:00
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
Nikolaj Bjorner
ce1b135ec3 address accessor inconsistencies between - and from #1506 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-26 14:57:17 +09:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
61934d8106 align semantics of re.allchar with string proposal. #1475 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:08:15 -08:00
Nikolaj Bjorner
2749e547cf fix c example, remove more smtlib1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 18:14:24 -08:00
Nikolaj Bjorner
b8e5fc9f43 remove SMTLIB1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 15:08:28 -08:00
Christoph M. Wintersteiger
048ee090b0 Eliminated the remaining operator kinds for partially unspecified FP operators from the AST API. 2017-09-20 20:19:36 +01:00
Christoph M. Wintersteiger
31cfca0444 Eliminated unspecified operators for fp.to_*bv, fp.to_real. Also fixes #1191. 2017-09-12 19:43:45 +01:00
Christoph M. Wintersteiger
4ceef09156 Renamed FPA-internal functions now that they are exposed. 2017-09-11 15:04:53 +01:00
Christoph M. Wintersteiger
e88487021a Exposed internal FPA func_decl kinds. Added missing FPA simplifications. Fixes #1242. 2017-09-11 14:36:58 +01:00
Dan Liew
a2d7b43554 Update header includes to be relative to src/ directory. 2017-08-17 18:26:53 +01:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
894c60bdf9 fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-19 18:22:30 -05:00
KangJing Huang (Chaserhkj)
e3f32ca3a8 Fix Z3_PRINT_SMTLIB_FULL not working as expected 2017-06-14 02:18:21 -04:00
Nikolaj Bjorner
fda59f5a24 expose operator kinds for internal functions using their sequence variants. Issue #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:32:17 -07: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
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
99b7c26e9f exposing regular expression features to address issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:05:02 +01:00
Nikolaj Bjorner
fe34e8bf00 Add OP_INTERNAL to handle cases of function symbols that don't have external semantics (at least in a way that is supported by means of building terms) Issue #688 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 12:13:54 -07:00
Nikolaj Bjorner
b080e3a216 garbage collect all api::object references when calling del_context. Request issue #679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 22:26:21 -07:00
Nikolaj Bjorner
d7d22cad02 undo comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:38:03 -07:00
Nikolaj Bjorner
53b3edc8cc add cases for recognizing ALL. Issue #674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:18:26 -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
Christoph M. Wintersteiger
617e941015 fp2bv refactoring 2016-05-23 18:10:17 +01:00
Christoph M. Wintersteiger
80731ef364 Exposed OP_FPA_MIN/MAX_I to the API 2016-05-20 19:40:45 +01:00