Christoph M. Wintersteiger
58fd4fc860
Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes
...
Assorted fixes for floats
2021-10-12 18:24:49 +01:00
Nikolaj Bjorner
52032b9ef8
#5467
2021-10-12 10:16:15 -07:00
Christoph M. Wintersteiger
b471ebdf1c
Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it."
...
This reverts commit f80fdb4ea3a762cfe95daa0321d9875cfa00c7ae.
2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger
738783a26c
Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it.
2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger
c24f438e51
Fix for mk_to_fp_float; pertains to #4841
2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger
00e8ea7962
Make terms that are internalized on the fly relevant
2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger
8e69f76784
Add additional equality in theory_fpa
2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger
f1acc4b78a
Make fpa2bv debug symbol names optional
2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger
515a2a771e
Whitespace
2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger
e8d6d97ba3
Refine fpa_decl_plugin::is_unique_value
2021-10-12 12:45:08 +00:00
Christoph M. Wintersteiger
12c32663c6
Fix error messsages
2021-10-12 12:45:08 +00:00
Nikolaj Bjorner
c3549ec784
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-11 11:03:45 -07:00
Nikolaj Bjorner
73102cffcb
fix #5589
2021-10-11 11:03:45 -07:00
Nikolaj Bjorner
75702c3631
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-11 11:03:45 -07:00
Nikolaj Bjorner
f7a2d08e74
Update README.md
2021-10-11 10:32:47 -07:00
Jamie Collinson
88c3119d8d
Create android-build.yml ( #5588 )
2021-10-11 09:24:41 -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
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
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
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
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
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
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
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
de20bffafe
import goodies from ps
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-21 11:13:03 -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
2c266a96c8
#5545
2021-09-20 13:57:34 -07:00
Nikolaj Bjorner
1352aa06f3
#5532
2021-09-20 12:08:04 -07:00
Nikolaj Bjorner
0170f1f461
#5532
2021-09-20 11:39:16 -07:00
Nikolaj Bjorner
fd799089b7
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-20 11:19:26 -07:00
Nikolaj Bjorner
6f31d83633
fix #5541
2021-09-20 10:10:28 -07:00
Jamey Sharp
426306376f
CNF conversion refactoring ( #5547 )
...
* split sat2goal out of goal2sat
These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.
I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.
* limit solver_core methods to those needed by goal2sat
And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.
I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
2021-09-20 08:53:10 -07:00
Duncan Ogilvie
91fb646f55
Fix Z3Config.cmake.in when generating a static library ( #5555 )
2021-09-17 18:03:10 +01:00
