mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
15835 commits 23 branches 48 tags 156 MiB
Commit graph

15835 commits

This branch
This branch
All branches
Author SHA1 Message Date
CEisenhofer 47fdd6c060
Added 16 bit string-encoding (#5540) 2021-09-09 11:35:16 +02:00
Nikolaj Bjorner e70f501932 handle potential extra nodes from q_solver 2021-09-09 09:17:11 +02:00
Nikolaj Bjorner c4d0ded7b7 #5532 2021-09-08 06:19:49 +02:00
Nikolaj Bjorner 8c406c161e #5532 add blocking condition for recursion. 2021-09-07 12:28:18 +02:00
Nikolaj Bjorner 93415740b6 left over bugs #5532 
disabling complete const rewriting (temporarily) as it can loop
 2021-09-07 07:00:41 +02:00
Nikolaj Bjorner be4df46f6f #5532 remove unsound rewrite rule that was recently added 2021-09-07 06:42:24 +02:00
Nikolaj Bjorner 72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
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