3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Commit graph

12434 commits

Author SHA1 Message Date
Nikolaj Bjorner
4c1fcbaa62 fix #4865 2020-12-06 14:13:46 -08:00
Nikolaj Bjorner
746dd745ad fix #4856 2020-12-06 14:06:08 -08:00
Nikolaj Bjorner
c3c7aad1a8 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-06 11:18:37 -08:00
Lev Nachmanson
2e5eb2dde2
Tree fix (#4864)
* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more fixes

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-12-06 11:18:27 -08:00
Addison Crump
b0cecf7747
Make multi-index arrays not so bad (#4857) 2020-12-05 15:45:46 -08:00
Nikolaj Bjorner
4d55f83654 misc 2020-12-04 16:59:13 -08:00
Murphy Berzish
b0fd25f041
z3str3: don't compute intersection difficulty against a null automaton (#4846) 2020-12-04 10:40:03 -06:00
Nikolaj Bjorner
6d427d9dae fix #4839 2020-12-02 12:46:24 -08:00
Nikolaj Bjorner
12198d13ac fix #4794 2020-12-02 12:24:35 -08:00
Nikolaj Bjorner
9156e355d8 log 2020-11-30 11:57:25 -08:00
Addison Crump
3bca1fbcd8
Java type generics (#4832)
* Generify, needs some testing and review

* Remove unnecessary change

* Whoops, ? capture that type

* Misread the docs, whoops

* More permissible arithmetic operations

* Implement believed Optimize generics

* Missed a few generics

* More permissible expr for arrays in parameters

* More permissible expr for bitvecs in parameters

* More permissible expr for bools in parameters

* More permissible expr for fps in parameters

* More permissible expr for fprms in parameters

* More permissible expr for ints in parameters

* More permissible expr for reals in parameters

* Undo breaking name conflict due to type erasure; see notes

* Whoops, fix typing of ReExpr

* Sort corrections for Re, Seq

* More permissible expr for regular expressions in parameters

* Fix name conflict between sequences and regular expressions; see notes

* Minor typo, big implications!

* Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency

* More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture

* Be less dumb and just type it a little differently

* Update examples, make sure to type Expr and FuncDecl sort returns

* General fixups

* Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction

* Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird
2020-11-30 10:04:54 -08:00
Nikolaj Bjorner
bb24b3f2be fix #4836 2020-11-29 21:08:28 -08:00
Nikolaj Bjorner
260f759177 fix #4835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 20:06:32 -08:00
Nikolaj Bjorner
67bbdc7524 fix initialization order
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:48:42 -08:00
Nikolaj Bjorner
64af8981ba fix #4834, regression after delay-propagating disequality axioms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:43:46 -08:00
John Regehr
b7e1b1e118
get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833)
* on POSIX systems, fork() is dangerous in the presence of a thread
pool, because the child process inherits only the thread from the
parent that actually called fork().

this patch winds down the scoped_timer thread pool in preparation for
forking; workers will get freshly created again following the fork
call.
2020-11-29 21:26:53 +00:00
Nikolaj Bjorner
05c5f72ca1 fix #4829
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-28 11:25:36 -08:00
Nikolaj Bjorner
17f04099a5 fix #4831 2020-11-28 11:01:07 -08:00
Nikolaj Bjorner
6e14d3fbd3 fix #4795 2020-11-27 18:00:36 -08:00
Nikolaj Bjorner
df09cb7c95 fix relevancy test 2020-11-27 14:49:05 -08:00
Nikolaj Bjorner
35900ee8ea avoid crash from #4772
To take care of "When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults."
2020-11-27 14:41:28 -08:00
Nikolaj Bjorner
67a8492bd0 more graceful proof checks 2020-11-27 14:40:46 -08:00
Nikolaj Bjorner
6771e44d93 fix #4825 #4824 2020-11-27 13:39:33 -08:00
Nikolaj Bjorner
1619311ff7 fix #4826 2020-11-27 10:42:13 -08:00
Nikolaj Bjorner
f58618aa04 fix java compile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-26 08:09:48 -08:00
Nikolaj Bjorner
b5a6c6bc66 attempt at more graceful timeout handling #4821 2020-11-26 06:33:44 -08:00
Nikolaj Bjorner
d6a5ef4343 add recfuns to Java #4820
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-25 12:25:20 -08:00
Murphy Berzish
6aba325cea
z3str3: reject certain unhandled expressions (#4818) 2020-11-25 12:15:35 -08:00
Nikolaj Bjorner
c27a325017 na 2020-11-23 10:22:21 -08:00
Nikolaj Bjorner
b769c0054b fix error messages for #4816 2020-11-23 10:20:52 -08:00
Nikolaj Bjorner
291502f8e4 this-> 2020-11-22 21:20:13 -08:00
Nikolaj Bjorner
1008b2d4cb fix #4812 2020-11-22 16:21:19 -08:00
Nikolaj Bjorner
193ca57444 fix #4811 2020-11-22 16:05:44 -08:00
Nikolaj Bjorner
65464f5944 include order 2020-11-22 15:39:09 -08:00
Nikolaj Bjorner
797f50e699 DRAT debugging updates 2020-11-22 15:38:57 -08:00
Nikolaj Bjorner
6d0b89a989 fix #4810 2020-11-22 15:37:55 -08:00
Nikolaj Bjorner
065e0652a3 fix crash when parsing datalog format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-21 15:15:28 -08:00
Nikolaj Bjorner
299e1788b8 fix #4808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-21 15:03:17 -08:00
Nikolaj Bjorner
d6106f26ff disable gcd test 2020-11-20 12:18:19 -08:00
Nikolaj Bjorner
1b768c9b3a fix #4805
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-20 12:11:38 -08:00
Nikolaj Bjorner
1269776777 remove experimental option. Fix #4806
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-20 11:46:19 -08:00
Nikolaj Bjorner
ac1b3fc6f2 fix delay blasting and relevancy 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner
9f34af5e18 update justifications only at level 0 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner
ee04bfd174 fix equality propagation 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner
a475e7cf5a Add gcd test to bv-rewriter 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner
6506d33b35 Add GCD test 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner
b7b7970c4a guard table erasure for representative 2020-11-20 11:12:54 -08:00
Nuno Lopes
40159a3a96 fix single-thread build 2020-11-19 21:46:32 +00:00
John Regehr
0fa88efc2b
scoped_timer: wait for timer thread before main thread continues (#4803) 2020-11-19 21:42:55 +00:00
Nikolaj Bjorner
e16acd0965 move std::function initializer to beginning of class
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-16 17:02:15 -08:00