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
Nikolaj Bjorner
33f4e65fa9
redo bindings/fingerprints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-05 10:15:56 -07:00
Nikolaj Bjorner
281fb67d88
unit propagate with fingerprints
2021-10-04 20:01:46 -07:00
Nikolaj Bjorner
8a85cfdb12
fix #5579 -
...
It is only possible to reach this case when new assertions are created.
2021-09-30 09:32:34 -07:00
Nikolaj Bjorner
cbe7dd4a48
missing continue fixes unsound sat result from #5573
2021-09-29 14:26:09 -07:00
Nikolaj Bjorner
ff723f15ff
Update z3++.h
2021-09-29 12:19:02 -07:00
Nikolaj Bjorner
62fd22f555
disable macro finder tactic if there are recursive functions fix #5574
2021-09-29 09:33:52 -07:00
Nikolaj Bjorner
137e5c5263
fix tmp_eq
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-28 14:28:41 -07:00
Nikolaj Bjorner
67ae75bac7
fix tmp_eq
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-28 14:27:46 -07:00
Nikolaj Bjorner
da124e4275
tune q-eval and q-ematch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-28 13:41:37 -07:00
