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

16466 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
4f064ee5d6 simplify based on comment from Jamie Sharp #5512 2021-08-28 17:08:34 -07:00
Nuno Lopes
e5a2f08cc9 fix logging of Z3_mk_lambda and Z3_mk_lambda_const 
In preparation of a bug report just for you @NikolajBjorner
 2021-08-29 00:37:45 +01:00
Nikolaj Bjorner
e3a83dd0dd Integrate fixes from #5512 
Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work.
In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier.
 2021-08-28 10:46:45 -07:00
Nikolaj Bjorner
992daa6d2e #5482 
remove overly permissive filter on select_store axiom
 2021-08-27 21:03:30 -07:00
Nikolaj Bjorner
e9a30385cf remove wtm and booth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 15:32:06 -07:00
Jamey Sharp
cd7a826083
bit_blaster unit tests for adder and multiplier (#5514) 
These tests cover a mix of constant and non-constant input bits.
 2021-08-27 14:19:12 -07:00
Nikolaj Bjorner
8f306c6a8f handle constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 11:59:41 -07:00
Nikolaj Bjorner
09696e989e add missing lambda defs per #5509 
the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
 2021-08-27 11:57:26 -07:00
Nikolaj Bjorner
9790a8aa43 #5507 
can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver.
 2021-08-27 09:42:40 -07:00
Nikolaj Bjorner
828fc72754 types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 18:55:53 -07:00
Nikolaj Bjorner
d6848175eb re-add API for creating propagator from a context for "fresh" 2021-08-26 18:12:40 -07:00
Nikolaj Bjorner
f7c1ed8273 missing this 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 10:41:37 -07:00