3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Commit graph

446 commits

Author SHA1 Message Date
Nikolaj Bjorner
335543b374 adding comparison #2360
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-28 21:14:58 -07:00
Nikolaj Bjorner
b8734273c8 pydoc regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-22 17:49:46 -08:00
Nikolaj Bjorner
5dfc40bf50 python regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 22:29:08 +02:00
Nikolaj Bjorner
b4290d4b3d python regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 22:26:21 +02:00
Nikolaj Bjorner
63a952f254 setting ast to null on destructor to deal with #2350
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 16:40:11 +02:00
Nikolaj Bjorner
cbe52e298b remove tracing, fix doctext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 15:08:26 +02:00
Nikolaj Bjorner
017680898a update doctest
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 11:11:01 +02:00
Nikolaj Bjorner
7c9d2e0d75 pydoc test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-20 22:44:03 +02:00
Nikolaj Bjorner
88d51d3377 fix python doc regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 12:34:56 -07:00
Saurabh Chaturvedi
2fd579bdd2
Fix typo in ForAll Doc 2019-06-15 05:02:37 +05:30
Audrey Dutcher
6fa85ad654 Allow building python wheels with binaries from a prebuilt release 2019-06-10 16:23:26 -07:00
Nikolaj Bjorner
fdfb9e4fd5 Merge branch 'master' of https://github.com/z3prover/z3 2019-06-05 16:10:31 -07:00
Nikolaj Bjorner
aabc54409c change printing directires
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 16:10:22 -07:00
Nikolaj Bjorner
a8b02ddb93 fix #2323
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 13:43:45 -07:00
Nikolaj Bjorner
b7f14c5875 update test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-16 23:48:46 +03:00
Nikolaj Bjorner
6e3f05b986 remove useless set-activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-16 20:24:51 +03:00
Charlie Barto
167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Nikolaj Bjorner
9f1b8db870 adjust for SMTLIBification name change of set operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-27 14:13:23 -07:00
Nikolaj Bjorner
c9b906a518 deal with python globals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-27 14:03:26 -07:00
Nikolaj Bjorner
944ce1135b replace __debug__ by Z3_DEBUG #2225
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-27 13:47:53 -07:00
Nikolaj Bjorner
40e329fc92 remove push/pop for fixedpoint objects from API #2249
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-27 10:13:15 -07:00
Nikolaj Bjorner
aafb16e8ed remove trc from C++ and python
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-17 11:10:57 -07:00
Nikolaj Bjorner
502b29c424 add set-has-size to API and python bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-16 15:38:14 -07:00
Nikolaj Bjorner
6158ea61c8 fix tree-order, change API for special relations to produce function declarations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-16 00:04:48 -07:00
Nikolaj Bjorner
182039eb44 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
f1a2e875b5 fixing #2217
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-05 03:06:41 -07:00
Nikolaj Bjorner
dfd327f287 add tuple and disjoint sum shorthands
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-02 18:36:35 -07:00
Nikolaj Bjorner
8d5507008e adding cmd_context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
0a0b0a5cc0 fix python doc regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-24 13:22:35 -07:00
Nikolaj Bjorner
32164b6c7f fix python doc regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-24 13:10:11 -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
fca8ffd948 fix #2199
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-23 16:37:50 -07:00
Nikolaj Bjorner
3c8fd83c97 implementing last-index-of #2089
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-22 12:29:50 -07:00
Nikolaj Bjorner
834cf962a1 expose nth over API, change _getitem_ in python bindings to use nth instead of at, add 'at' operator for the purpose of the previous semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-17 11:23:01 -07:00
Nikolaj Bjorner
5bc0fb47a8 fix #2169
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-09 19:31:30 -08:00
Nikolaj Bjorner
5fa5719c6f fix #2159
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 08:58:58 -08:00
Nikolaj Bjorner
89bf2d4368 add API for setting variable activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-15 12:05:24 -08:00
Audrey Dutcher
4e687671a5 Tweak python setup.py clean to properly clean the native build 2019-02-10 14:32:02 -08:00
Audrey Dutcher
b702cad81e Append std=c++11 instead of replacing CXXFLAGS; see #2130 2019-02-10 14:12:27 -08:00
Nikolaj Bjorner
c5df6ce96e fix #2131
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-10 10:07:24 -08:00
Nikolaj Bjorner
9cf99e26a6 fix #2123
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-03 19:54:08 +01:00
Nikolaj Bjorner
a76107e50d fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-01 18:44:52 -08:00
Nikolaj Bjorner
6c464f8aec add assert_and_track to optimize for #2116
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-01 14:59:36 -08:00
Nikolaj Bjorner
35eb21bc35 fix extraction of trail
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-30 09:06:41 -08:00
Nikolaj Bjorner
08ce6f7ac1 working on binary drat format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-30 08:54:59 -08:00
Alcides Fonseca
83717a9c86 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-01-25 14:45:22 +00:00
Alcides Fonseca
a785ffe0ba Updated deepcopy to the latest Python API 2019-01-25 14:42:22 +00:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-24 12:21:23 -08:00
Nikolaj Bjorner
efaab6d8fd have sat cleaner use a fixed-point
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-10 11:38:35 -08:00
Nikolaj Bjorner
a63d1b1848 update doctest
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-18 11:57:20 -08:00