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

14460 commits

Author SHA1 Message Date
Nikolaj Bjorner 6e7a80b68e change version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 10:59:06 -07:00
Nikolaj Bjorner c481570257 disable pip in trial release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 10:16:57 -07:00
Nikolaj Bjorner f4e8205aca na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 04:39:43 -07:00
Nikolaj Bjorner cfa7c733db
fixing #4670 (#4682)
* fixing #4670

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

* init

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

* arrays

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

* arrays

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

* arrays

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

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 04:35:11 -07:00
Nikolaj Bjorner ee00542e76 update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 04:05:08 -07:00
Nikolaj Bjorner 1c7d27bdf3 fix missing parenthesis in C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 13:32:39 -07:00
Nikolaj Bjorner f976b16e3f add macros to model #4679
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 13:31:13 -07:00
Nikolaj Bjorner 629e981e01 fix regression in get-consequence on QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 12:43:18 -07:00
Nikolaj Bjorner 80879ce58b remove xcode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 07:12:30 -07:00
Nikolaj Bjorner 7327023c88
add variable replay, remove MacOS from Travis (#4681)
* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* dbg

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

* bv

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

* drat and fresh

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

* move ackerman functionality

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

* na

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

* debugability

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

* towards debugability

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

* missing file

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

* na

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

* na

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

* remove csp

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

* replay variables created by solver

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

* remove old function

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

* fix scoped-limit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 05:57:07 -07:00
Margus Veanes af54a79acc
fixing issue #4651 (#4666)
* fixing issue #4651

* regression fix

* fix #4662

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

* na

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

* reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate

* removing temp testing variable

* Allow to skip System.loadLibrary() calls from Java Native class (#4667)

* using intended utility methods for sort detection

* adding ack/model

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

* add smt params dependency

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

* missing file

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

* deps

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

* order

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

* persist fields

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

* dbg build

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

* reset caches

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

* sr

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

* fix cmake build

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

* shuffle dependencies

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

* warnings /errors

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

* update include

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

* missing cmakelists

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

* update cmake

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

* add depend

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

* add depend

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

* virtual method

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

* path

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

* move parameters from ast/rewriter to params

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

* move fpa

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

* fix warnings

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

* remove pragma

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

* dbg

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

* updated sat_smt

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

* na

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

* fix #4651

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

* encoding options #4665

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

* expose name inclusion as optional

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

* fix misc issues around #4661 introduced when adding lazy push/pop to selected theories

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

* remove lazy push from theory_lra

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

* na

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

* fix dotnet build

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

* na

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

* release nodes

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

* free memory in egraph

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

* avoid duplicate class names frame in sat_scc and sat_smt

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

* adding euf

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

* elaborate on smt/drat format outline, expose euf mode as config

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

* mk-var during copy

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

* move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph

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

* with bounded

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

* na

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

* Remove duplicate binary condition. Fixes #4668.

* butterfly effect on fp?

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

* prepare for theory plugins

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

* file

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

* build fix

* remove SMTFD

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

* na

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

* na

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* SMTFD is back (#4676)

* fixing issue #4651

* regression fix

* reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate

* removing temp testing variable

* using intended utility methods for sort detection

* misc edits related to nonground regexes

* bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph

* removed unused method declaration

* improved id to regex value map info in generated dgml

* reorgd callback function for state pretty printer

* updated some comments

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Sergey Vladimirov <vlsergey@gmail.com>
Co-authored-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
2020-09-08 04:13:18 -07:00
Nikolaj Bjorner d02b0cde7a
running updates to bv_solver (#4674)
* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* dbg

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

* bv

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

* drat and fresh

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

* move ackerman functionality

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

* na

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

* debugability

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

* towards debugability

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

* missing file

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

* na

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

* na

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

* remove csp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-07 20:35:32 -07:00
Nikolaj Bjorner 4d1a2a2784 update to xcode 9.2 for Travis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-07 18:55:31 -07:00
Arie Gurfinkel 687a16a796
SMTFD is back (#4676) 2020-09-04 10:50:35 -07:00
Nikolaj Bjorner f370d8d9b4 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 09:34:09 -07:00
Nikolaj Bjorner 7fbaf71d4a na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 09:19:39 -07:00
Nikolaj Bjorner 65bc77d566 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 08:58:08 -07:00
Nikolaj Bjorner fe43f8df8f na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 08:11:43 -07:00
Nikolaj Bjorner aa66be9406 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 07:16:59 -07:00
Nikolaj Bjorner d83d0a83d6 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 14:43:49 -07:00
Nikolaj Bjorner e4b7b7bdf6 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 13:52:24 -07:00
Nikolaj Bjorner 95493f78f9 na 2020-09-02 13:08:52 -07:00
Nikolaj Bjorner 4b22434739 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 13:02:00 -07:00
Nikolaj Bjorner 54a75d6a91 remove SMTFD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 12:39:23 -07:00
Nikolaj Bjorner 7c2fe46eb7 build fix 2020-09-02 12:35:12 -07:00
Nikolaj Bjorner daf7e9e3ef file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 10:43:53 -07:00
Nikolaj Bjorner 116390833b prepare for theory plugins
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-02 10:42:18 -07:00
Nikolaj Bjorner 141edef0d6 butterfly effect on fp?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-01 10:19:43 -07:00
Christoph M. Wintersteiger 527bf72d42
Remove duplicate binary condition. Fixes #4668. 2020-09-01 15:22:01 +00:00
Nikolaj Bjorner ecddaeae66 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-01 07:15:13 -07:00
Nikolaj Bjorner 74a2bf1588 Merge branch 'master' of https://github.com/z3prover/z3 2020-09-01 04:58:41 -07:00
Nikolaj Bjorner 03e92f3f20 with bounded
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-01 04:58:38 -07:00
Nikolaj Bjorner d4e92d4aca move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-01 04:26:31 -07:00
Nikolaj Bjorner fa9cf0fa0c mk-var during copy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-31 20:34:41 -07:00
Nikolaj Bjorner ed7d969366 elaborate on smt/drat format outline, expose euf mode as config
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-31 19:29:23 -07:00
Nikolaj Bjorner 4d41db3028 adding euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-31 14:36:16 -07:00
Nikolaj Bjorner 314bd9277b avoid duplicate class names frame in sat_scc and sat_smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 20:16:48 -07:00
Nikolaj Bjorner bee3077640 free memory in egraph
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 20:13:46 -07:00
Nikolaj Bjorner a003af494b release nodes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 20:09:27 -07:00
Nikolaj Bjorner bbe027f6a1 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 15:03:15 -07:00
Nikolaj Bjorner 25106866b5 fix dotnet build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 14:46:31 -07:00
Nikolaj Bjorner 9f0b303263 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 12:08:15 -07:00
Nikolaj Bjorner 727ea43b16 remove lazy push from theory_lra
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 12:07:14 -07:00
Nikolaj Bjorner 9b5dc0ca26 fix misc issues around #4661 introduced when adding lazy push/pop to selected theories
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 10:57:05 -07:00
Nikolaj Bjorner b992f59aad expose name inclusion as optional
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 10:32:17 -07:00
Nikolaj Bjorner dbe2c9b305 encoding options #4665
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 10:24:42 -07:00
Nikolaj Bjorner e8826bb20f fix #4651
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-30 09:49:12 -07:00
Nikolaj Bjorner 4682b48d3a na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 19:24:43 -07:00
Nikolaj Bjorner 86310a1a27 updated sat_smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 19:21:51 -07:00
Nikolaj Bjorner e9a4e486ae dbg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 19:21:50 -07:00