Jamie Collinson
88c3119d8d
Create android-build.yml ( #5588 )
2021-10-11 09:24:41 -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
Nikolaj Bjorner
6f55971177
Newderiv ( #5585 )
...
* 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>
Co-authored-by: Margus Veanes <margus@microsoft.com>
2021-10-08 13:06:10 -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
Kartik Singhal
1dcbd2d86c
Correct capitalization of package ( #5569 )
...
See https://stackoverflow.com/a/50004273/1167061
2021-09-25 09:04:06 -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
