mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity
16463 commits 45 branches 52 tags 177 MiB
Commit graph

13982 commits

Author SHA1 Message Date
Nikolaj Bjorner
75702c3631 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-11 11:03:45 -07:00
Nikolaj Bjorner
4c81f8676c backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-10 18:23:25 -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
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
5ee5197ea9 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-10-06 13:01:29 -07:00
Nikolaj Bjorner
a50cecaefa wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 16:06:31 -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
be4bc6caed merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-04 17:37:12 -07:00
Nikolaj Bjorner
0d9d4bb46e wip 2021-10-04 14:44:05 -07:00
Nikolaj Bjorner
813674087e wip 2021-10-04 14:43:33 -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
fd8b2ba596 clear regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-29 15:56:01 -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
e1224e116f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:45:03 -07:00
Nikolaj Bjorner
f3328c743e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:43:55 -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
Nikolaj Bjorner
92c1b600c3 tuning eval 2021-09-28 09:56:00 -07:00
Nikolaj Bjorner
2e176a0e02 count lazy bindings 2021-09-28 08:27:46 -07:00
Nikolaj Bjorner
e1edadabec na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-27 17:06:59 -07:00
Nikolaj Bjorner
3abecc3428 add extra commands to API parser 2021-09-27 14:19:43 -07:00
Nikolaj Bjorner
6c71baf77b lifting iff to binary 2021-09-27 03:45:54 -07:00
Nikolaj Bjorner
95e2d174c7 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-25 17:26:18 -07:00
Nikolaj Bjorner
a574eebd05 fixes, tests 2021-09-25 08:38:48 -07:00
Nikolaj Bjorner
e6c413b249 add variable minimization 2021-09-22 14:27:05 -07:00
Nikolaj Bjorner
c82bbaad7d update todos, working on assignment minimization 2021-09-22 13:29:36 -07:00
Nikolaj Bjorner
3447d80310 fix todo on enforcing premises 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 12:26:45 -07:00
Nikolaj Bjorner
e5df395380 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:44:37 -07:00
Nikolaj Bjorner
0013ae5089 elim pointer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:15:32 -07:00
Nikolaj Bjorner
2d78bc9282 simplify Boolean resolve 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:37:46 -07:00
Nikolaj Bjorner
ad267ce294 add notes and unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:16:10 -07:00
Nikolaj Bjorner
dc55fbf30d add notes and unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:04:07 -07:00
Nikolaj Bjorner
d174f87c5e #5532 2021-09-21 20:21:23 -07:00
Nikolaj Bjorner
18d1b368d1 #5532 2021-09-21 20:12:32 -07:00
Nikolaj Bjorner
cabd5b10fa #5532 2021-09-21 18:56:55 -07:00
Nikolaj Bjorner
6478e789e9 optimizations, fixes, TODO items 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 14:50:18 -07:00
Nikolaj Bjorner
444084f396 add notes and tangent lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 11:30:50 -07:00
Nikolaj Bjorner
de20bffafe import goodies from ps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 11:13:03 -07:00
Nikolaj Bjorner
0426b23d0c fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 09:44:37 -07:00
Nikolaj Bjorner
708602dfbb fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:56:13 -07:00
Nikolaj Bjorner
2e96557827 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:55:28 -07:00
Nikolaj Bjorner
23963f274d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 04:58:00 -07:00