mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
16778 commits 49 branches 53 tags 182 MiB
Commit graph

16778 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
3764eb1959 #5532 
ensure re-internalization for predicates that are replayed.
Theory internalization is currently not considered in depth.
 2021-09-05 00:24:34 -07:00
Nikolaj Bjorner
3021da87cf #5532 2021-09-04 21:10:26 -07:00
Nikolaj Bjorner
9c91698201 #5532 2021-09-04 18:03:15 -07:00
Nikolaj Bjorner
976c0a391c revisit as-array evaluation 2021-09-04 18:00:36 -07:00
Nikolaj Bjorner
38b82fa742 const rewriting revisited 2021-09-04 17:59:08 -07:00
Nikolaj Bjorner
051ede64e7 #5532 2021-09-04 09:48:46 -07:00
Nikolaj Bjorner
3de9162c7e handle null more gracefully 2021-09-04 09:42:45 -07:00
Nikolaj Bjorner
9c5ef79701 #5532 2021-09-04 09:05:49 -07:00
Nikolaj Bjorner
18e4546404 modernize parameter defaults 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-03 17:42:36 -07:00
Nikolaj Bjorner
cdcfbeb6d8 #5532 
remove "reflect" parameter from exposed options. It should be internal only.
 2021-09-03 16:01:59 -07:00
Nikolaj Bjorner
0ddbbe9bd2 #5532 2021-09-03 15:41:52 -07:00
Nikolaj Bjorner
5633af76cc #5532 2021-09-03 15:25:50 -07:00
Nikolaj Bjorner
a566c7307d #5532 2021-09-03 12:33:04 -07:00
Nikolaj Bjorner
87f5b9282f #5532 2021-09-03 12:20:23 -07:00
Nikolaj Bjorner
c4158ebc33 #5532 2021-09-03 12:02:57 -07:00
Nikolaj Bjorner
20a259cfaa throw less #5519 2021-09-03 10:40:08 -07:00
Nikolaj Bjorner
af5c6e43b9 #5528 2021-09-02 11:21:57 -07:00
Nikolaj Bjorner
55285b2193 make it easier to iterate over arguments of an application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:51:59 -07:00
Nikolaj Bjorner
e9a4a9a390 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:23:59 -07:00
Nikolaj Bjorner
edb26e7be7 Merge branch 'master' of https://github.com/z3prover/z3 2021-09-02 08:53:56 -07:00
Nikolaj Bjorner
02acc38c28 add extra checks that user-supplied assumptions are asserted 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 08:53:47 -07:00
Nikolaj Bjorner
e05ef8ece9 account for updating scoped state by goal2sat #5528 2021-09-02 04:20:19 -07:00
Nikolaj Bjorner
f4abe3db02 #5528 2021-09-02 03:13:46 -07:00
Nikolaj Bjorner
9e306e3b6e more useful diagnostics 2021-09-01 20:50:35 -07:00
Nikolaj Bjorner
968717a532 follow on fix from #5528 
the same bug is also undetected in the main solver
 2021-09-01 20:49:39 -07:00
Nikolaj Bjorner
6907d30717 #5528 2021-09-01 20:44:00 -07:00
Nikolaj Bjorner
a74c01c8b9 #5528 2021-09-01 20:39:54 -07:00
Nikolaj Bjorner
cf9e55fa96 #5516 
expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes.
 2021-09-01 17:44:17 -07:00
Nikolaj Bjorner
ba68fba419 build 2021-09-01 17:10:23 -07:00
Nikolaj Bjorner
0c53c139da add to_string method to make it easier to use without << 2021-09-01 15:37:58 -07:00
Nikolaj Bjorner
7ce4be8455 #5528 2021-09-01 14:01:15 -07:00
Nikolaj Bjorner
a7bc4719c0 fix #5526 
when propagation claims progress, but is a no-op.
 2021-09-01 11:45:21 -07:00
Nikolaj Bjorner
8bdc8d0e1a Update solver_subsumption_tactic.h 
use naming convention with - instead of _ for tactics
 2021-09-01 11:35:06 -07:00
Nikolaj Bjorner
a3ba4e1366 #5528 2021-09-01 11:34:44 -07:00
Nikolaj Bjorner
f91c3d9fd6 round-tripping escapes, again #5519 2021-08-31 20:36:38 -07:00
Nikolaj Bjorner
90f98d5791 fix part of #5519 
generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
 2021-08-31 20:06:06 -07:00
Nikolaj Bjorner
7c782a7ef8 #5518 
patch a gaping hole in recfun
 2021-08-31 19:49:18 -07:00
Nikolaj Bjorner
1426390aec #5518 2021-08-31 16:38:27 -07:00
Nikolaj Bjorner
ab2baa764c #5518 
@wintersteiger
This example exposes a bug in is_unique_value
```
(assert (= (fp.to_real ((_ to_fp 8 24) (_ bv4286579200 32))) (fp.to_real ((_ to_fp 8 24) (_ bv4286578944 32)))))
(check-sat)
```
It returns true for fp representations that map to NaN. It can only return true for fp values that are unique relative to having no other bit-vector representation so not corresponding to an equivalence class of values such as NaN.
I am having it return false. If there is a way to refine the test it will catch some earlier inferences.
 2021-08-31 14:52:45 -07:00
Nikolaj Bjorner
34c8f598a5 #5518 2021-08-31 14:21:10 -07:00
Nikolaj Bjorner
07bbd026ac #5518 2021-08-31 13:02:54 -07:00
Nikolaj Bjorner
0b063f7903 #5518 2021-08-31 12:50:24 -07:00
Nikolaj Bjorner
535f442655 #5518 
regression from adding lambdas in model
 2021-08-31 12:13:27 -07:00
pcarbonn
cd2701da0c
fix the use of ctx in Q() (#5521) 
* fix #4956

* fix: use ctx in Q()
 2021-08-31 10:01:47 -07:00
Nikolaj Bjorner
148cb83b0d #5482 fix default case for model construction 
port mg_merge functionality from theory_array_base that ensures default values in arrays congruent modulo stores are the same
 2021-08-29 17:30:39 -07:00
Nuno Lopes
9b5ec6d004 logging cleanup 
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
 2021-08-29 12:24:19 +01:00
Nuno Lopes
1f4a7c5101 logging: don't call the returned function twice (one for log, one for return) 
Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice
it turns out simplify is not idempotent, so calling it twice can result in different results
thus breaking the log.
 2021-08-29 11:06:19 +01:00
Nuno Lopes
9a172939e0 fix logging in Z3_fpa_get_[es]bits 2021-08-29 10:58:54 +01:00
Nikolaj Bjorner
b1bc890992 fix #5515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 18:05:51 -07:00
Nikolaj Bjorner
e7fcbd9563 bail on first model validation failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 17:08:34 -07:00