mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
15734 commits 49 branches 53 tags 182 MiB
Commit graph

15734 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
7c2bdfe3fb
delay internalization, relevancy (#4707) 
* delay evaluation

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

* Update bv_solver.cpp

* delay internalize

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

* compiler warnings

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

* remove gc

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

* add bv delay option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-23 17:12:01 -07:00
Lev Nachmanson
1e7998f03a
no big nums in patching (#4705) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-09-23 08:46:41 -07:00
Nikolaj Bjorner
1e6d2fbbdc debugging cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-21 20:02:12 -07:00
Nikolaj Bjorner
b7ec4489a6
bv fixes and tuning (#4703) 
* heap size information

* bv tuning

* fix #4701

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

* throw on set-has-size #4700

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-21 19:54:53 -07:00
Nikolaj Bjorner
ba5c9c3883 fix #4689 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-20 07:27:48 -07:00
Nikolaj Bjorner
d3d05e2e99 add side-constraints in pb2bv-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-20 07:03:06 -07:00
Nikolaj Bjorner
6f63f8761c
optimizations to bv-solver and euf-egraph (#4698) 
* additional bit-vector propagators

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

* rename restrict (not a keyword, but well) #4694, tune euf

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

* merge

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

* add pb rewriting to pb2bv #4697

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-20 06:47:27 -07:00
FabianWolff
ed44a44579
Fix z3.pc file template (#4693) 2020-09-18 12:39:12 -07:00
Nikolaj Bjorner
8691ef1d4d
additional bit-vector propagators (#4695) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-18 12:38:29 -07:00
Nikolaj Bjorner
549753845e
bv and gc of literals (#4692) 
* bv and gc of literals

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

* overload

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

* diseq

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

* diseq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-17 14:24:07 -07:00
Nikolaj Bjorner
2d52367368 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-15 16:45:11 -07:00
Nikolaj Bjorner
545e1c0d31 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-15 15:40:15 -07:00
Nikolaj Bjorner
6a4261d1af debugging bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-15 15:37:31 -07:00
Nikolaj Bjorner
2328a6e839 add a way to use new smt core for selected logics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-14 10:43:52 -07:00
Nikolaj Bjorner
73ce5c5fc8 display similar to sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-13 19:48:04 -07:00
Nikolaj Bjorner
796e2fd9eb
arrays (#4684) 
* 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>

* arrays

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

* na

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

* fill

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

* update drat and fix euf bugs

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>

* const qualifiers

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

* na

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

* reorg ba

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

* reorg

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

* build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-13 19:29:59 -07:00
Nikolaj Bjorner
d56dd1db7b update version' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-11 04:37:35 -07:00
Sergey Vladimirov
6324d2fb55
Set target for java classes to 1.8 (#4685) 2020-09-11 04:05:45 -07:00
Nikolaj Bjorner
c7ba86e227 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 21:49:43 -07:00
Nikolaj Bjorner
f11e2d0eba try again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 20:00:25 -07:00
Nikolaj Bjorner
7dbf30b465 include nupkg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 19:21:46 -07:00
Nikolaj Bjorner
3616688d6b update pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 17:26:47 -07:00
Nikolaj Bjorner
9cb47188ea Update release.yml for Azure Pipelines 2020-09-10 15:41:12 -07:00
Nikolaj Bjorner
79734f26ae move to python3 for release.yml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 11:51:28 -07:00
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