3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

15823 commits

Author SHA1 Message Date
Weng Shiwei 066076557f
Add post-install testing for ocaml binding. (#5617)
* Add path flags for cc loader (linux).

* Fix os linking and loading problem (maybe on #4840).

* Add post-install test of OCaml binding on ubuntu.

* Minor.

* Tentative CI for macos.
2021-10-25 11:21:02 +02:00
Nikolaj Bjorner 3a3cef8fce #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-23 18:21:51 +02:00
Nikolaj Bjorner 7f41d6140f use some suggestions from #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-22 12:39:55 -04:00
Nikolaj Bjorner 051616385f remove deprecated escape string from Julia bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-21 19:14:12 -04:00
Weng Shiwei cd8d8bbb63
Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616)
* Fix runtime search path for shared-lib and add '-static' to static-lib.

* Revert the change on `META.in`.
2021-10-21 18:27:54 -04:00
Nikolaj Bjorner f05ac8a429 updated C++ API for escaped and unescaped strings #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-21 14:52:59 -04:00
Nikolaj Bjorner 05e7ed9637 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-21 11:30:03 -04:00
Nikolaj Bjorner 6eed885379 print bounded terms for better efficiency 2021-10-21 10:42:39 -04:00
Nikolaj Bjorner 13da6a02a6 add handling of quantifiers #5612 2021-10-20 12:27:56 -04:00
Nikolaj Bjorner 839a0852fe Merge branch 'master' of https://github.com/z3prover/z3 2021-10-19 12:24:41 -04:00
Nikolaj Bjorner 86147d01ea #5605
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-19 12:24:29 -04:00
Nikolaj Bjorner f9dde2e8a4 #5605
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-19 12:21:54 -04:00
CEisenhofer 3557e0b0c5
Added eq/fixed/final functions in C++ user propagator as methods (#5607) 2021-10-19 10:48:31 -04:00
Nikolaj Bjorner fc3a701888 push-pop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-18 15:36:48 -07:00
Nikolaj Bjorner d5e5dcfe45 add nff and auto-relevant
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-18 15:32:55 -07:00
Nikolaj Bjorner bc2020a39b #5604
retain array interpretation when available
2021-10-17 20:24:26 -07:00
Nikolaj Bjorner 115203e87c fixes to sat.euf ematching #5573 2021-10-16 15:52:37 -07:00
Margus Veanes f78546cd7c
fixed bug of computing butlast of a sequence (#5602) 2021-10-15 18:02:51 -07:00
Nikolaj Bjorner fb9fa1b7d2 updated printer 2021-10-15 17:56:54 -07:00
Margus Veanes cb120c93f4
Regex range bug fix (#5601)
* added a missing derivative case for nonground range

* further missing cases and a bug fix in re.to_str
2021-10-15 15:30:55 -07:00
Simon Cruanes 6302b864c8
tweak GC in OCaml bindings (#5600)
* feat(api/ml): use custom block hints to guide the GC

this forces the GC to collect garbage when a few _large_ objects
(solver, etc.) are dead. The current code would let arbitrarily many
such objects die and not trigger a GC (which would have to come from
OCaml code instead)

* tuning

* try to use caml_alloc_custom_mem with fake sizes

* try to fix leak by explicitly finalizing OCaml context

* chore: use more recent ubuntu for azure CI

* remove finalizer causing segfault in example
2021-10-14 12:46:14 -07:00
Nikolaj Bjorner f60ed2ce92 #5591 2021-10-13 21:38:36 -07:00
Nikolaj Bjorner 7b341313d5 #5593 2021-10-13 17:50:56 -07:00
Nikolaj Bjorner fd77f0c111 fix #5594 2021-10-13 17:17:05 -07:00
Nikolaj Bjorner 96e117d78c Update smt_context.cpp 2021-10-12 17:10:12 -07:00
Nikolaj Bjorner c15968aa9e fix #4901 2021-10-12 17:10:04 -07:00
Nikolaj Bjorner 9a76bf0aa2 #5591
nth issue
2021-10-12 13:59:28 -07:00
Christoph M. Wintersteiger 58fd4fc860
Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes
Assorted fixes for floats
2021-10-12 18:24:49 +01:00
Nikolaj Bjorner 52032b9ef8 #5467 2021-10-12 10:16:15 -07:00
Christoph M. Wintersteiger b471ebdf1c
Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it."
This reverts commit f80fdb4ea3a762cfe95daa0321d9875cfa00c7ae.
2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger 738783a26c
Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it. 2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger c24f438e51
Fix for mk_to_fp_float; pertains to #4841 2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger 00e8ea7962
Make terms that are internalized on the fly relevant 2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger 8e69f76784
Add additional equality in theory_fpa 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger f1acc4b78a
Make fpa2bv debug symbol names optional 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger 515a2a771e
Whitespace 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger e8d6d97ba3
Refine fpa_decl_plugin::is_unique_value 2021-10-12 12:45:08 +00:00
Christoph M. Wintersteiger 12c32663c6
Fix error messsages 2021-10-12 12:45:08 +00:00
Nikolaj Bjorner c3549ec784 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-11 11:03:45 -07:00
Nikolaj Bjorner 73102cffcb fix #5589 2021-10-11 11:03:45 -07:00
Nikolaj Bjorner 75702c3631 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-11 11:03:45 -07:00
Nikolaj Bjorner f7a2d08e74
Update README.md 2021-10-11 10:32:47 -07:00
Jamie Collinson 88c3119d8d
Create android-build.yml (#5588) 2021-10-11 09:24:41 -07:00
Nikolaj Bjorner 0fc9f1d46a fix max/min length to handle concatenation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-09 16:20:32 -07:00
Andrew V. Jones f1b8376739
Rename 'user' to 'user_solver' #5586 (#5587)
Issue #5586 reported that Android builds (targetting, e.g., x86) failed
to compile due to a conflict between:

* `struct user` in `sys/user.h`; and
* `namespace user` in z3's `user_solver.h`

This issue is resolved by renaming `namespace user` to `namespace
user_solver` (matching the header name) to avoid this conflict.

Reported-by: Jamie Collinson <jamiecollinson@gmail.com>

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-10-09 15:07:37 -07:00
Nikolaj Bjorner bfa960c2ce fix internalize regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-08 14:48:17 -07:00
Nikolaj Bjorner 6f55971177
Newderiv (#5585)
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: Margus Veanes <margus@microsoft.com>
2021-10-08 13:06:10 -07:00
Margus Veanes 146f4621c5
Updated regex derivative engine (#5567)
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-08 13:04:49 -07:00
Nikolaj Bjorner c0c3e685e7 disable all propagation until ematch incompleteness is fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-05 11:25:35 -07:00
Nikolaj Bjorner 94cc4ead72 remove arith_lhs simplification from preamble tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-05 10:55:38 -07:00