mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
15220 commits 24 branches 48 tags 158 MiB
Commit graph

1350 commits

Author SHA1 Message Date
Nikolaj Bjorner
ecfbc1cc06 trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-26 15:15:27 -07:00
Nikolaj Bjorner
af5e7a1c48 #5211 2021-04-24 10:28:22 -07:00
Nikolaj Bjorner
e0393f85fa #5211 2021-04-22 23:46:05 -07:00
Nikolaj Bjorner
d2f15d1b1a #5211 2021-04-22 23:04:54 -07:00
Nikolaj Bjorner
67ec86fc66 #5211 2021-04-22 22:53:18 -07:00
Nikolaj Bjorner
5d49cb5519 #5211 2021-04-22 22:42:05 -07:00
Nikolaj Bjorner
5cfe273460 #5211 
```
 (declare-fun v5 () Bool)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i6 () Int)
 (declare-fun i9 () Int)
 (declare-fun i10 () Int)
 (assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
 (check-sat)
```
 2021-04-22 22:10:39 -07:00
Nikolaj Bjorner
bcb33a5b3a remove unused functions 2021-04-22 21:46:31 -07:00
Nikolaj Bjorner
4c4810c611 fix #5207 2021-04-22 13:10:11 -07:00
Nikolaj Bjorner
892e6d9ed5 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 05:06:46 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
6b1642e272 fix #5068 2021-04-08 12:39:23 -07:00
Nikolaj Bjorner
e5e663e874 fix for #5153 2021-04-06 20:09:50 -07:00
Nikolaj Bjorner
c629f09f21 fix #5139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:46:47 -07:00
Nikolaj Bjorner
2fdb703865 remove redundant assertion 2021-03-29 15:17:01 -07:00
Nikolaj Bjorner
dfb696becf fix #5119 2021-03-28 16:47:56 -07:00
Nikolaj Bjorner
974ef3c147 port equality propagation changes to new core 2021-03-28 16:15:04 -07:00
Nikolaj Bjorner
a1f484fa35 na 2021-03-19 16:42:45 -07:00
Nikolaj Bjorner
15a7621e27 remove template dependency for trail objects 2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
156139622c delay (lazy) process equalities. 2021-03-17 15:34:04 -07:00
Nikolaj Bjorner
0b8939d86e self-contained function for merge_tf 2021-03-16 15:24:48 -07:00
Nikolaj Bjorner
ff0de59a70 more streamlined diagnostics to prepare for #5106 2021-03-15 16:23:35 -07:00
Nikolaj Bjorner
4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner
18143d8932 fix #5102 2021-03-15 01:01:33 -07:00
Nikolaj Bjorner
1cb0dbae51 missing dependency for python build 2021-03-14 20:45:30 -07:00
Nikolaj Bjorner
155738088f fix internalization on post-visit, increase delay to 100 2021-03-14 17:20:39 -07:00
Nikolaj Bjorner
8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner
9a975a4523 array solver fixes 2021-03-13 06:19:32 -08:00
Nikolaj Bjorner
e08ceee424 compiler 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-08 20:41:10 -08:00
Nikolaj Bjorner
857557ad93 deal with compiler warnings 2021-03-08 20:39:19 -08:00
Nikolaj Bjorner
f29a596070 deal with compiler warnings, from MacOS CI build 2021-03-08 17:14:09 -08:00
Nikolaj Bjorner
5f0ec936e4 count final checks 2021-03-05 15:01:39 -08:00
Nikolaj Bjorner
022a1fd3dd fix #5080 assertion is violated on legal input, add an example 2021-03-05 15:01:39 -08:00
Nikolaj Bjorner
38737db802 fixes and more porting seq_eq_solver to self-contained module 2021-03-04 16:23:22 -08:00
Nikolaj Bjorner
e398959732 move eq solver functionality to common place, fixes to goal2sat 2021-03-04 07:57:31 -08:00
Nikolaj Bjorner
79ababb00a force push 2021-03-03 11:38:33 -08:00
Nikolaj Bjorner
69070a7486 align translation cache with scopes and variable elimination 2021-03-03 11:22:17 -08:00
Nikolaj Bjorner
bef6f1a729 fix build 2021-03-02 13:51:58 -08:00
Nikolaj Bjorner
f725989225 optimize for enumeration datatypes 2021-02-28 21:31:21 -08:00
Nikolaj Bjorner
caae0ba569 rename statistics to pb 2021-02-28 21:31:21 -08:00
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
13f05ae9dc enable wcnf output for weighted maxsat problems 2021-02-28 09:59:36 -08:00
Nikolaj Bjorner
b02cba6106 rename propagation to explain 2021-02-27 17:25:11 -08:00
Nikolaj Bjorner
fb8e2e444e remove xor solver, tune dt_solver for enumeration case 2021-02-27 17:17:39 -08:00
Nikolaj Bjorner
830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner
ea1089e980 fix #4938 2021-02-26 02:06:28 -08:00
Nikolaj Bjorner
080c9c6893 fixes to dt solver 2021-02-25 10:35:02 -08:00
Nuno Lopes
5e034e495f fix compiler warnings 2021-02-19 10:33:41 +00:00
Nikolaj Bjorner
45af1bd243 fix build, move seq_skolem 2021-02-14 14:40:29 -08:00
Nikolaj Bjorner
083d09aa81 fix #5016 2021-02-14 13:52:10 -08:00