mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity
17789 commits 24 branches 48 tags 158 MiB
Commit graph

17789 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e417f7d785 updated release notes for 12.2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-12 12:59:04 -07:00
Nikolaj Bjorner
ba911009e4 disable publish 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-11 16:54:40 -07:00
Nikolaj Bjorner
046b80f6a4 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-11 12:31:05 -07:00
Nikolaj Bjorner
f6ab5a61ac reformat code to remove brackets 2023-05-11 12:31:05 -07:00
Antti Hyvärinen
12e45c9d17
Implement proposed smtlib2 bitvector overflow predicates (#6715) 
* Logical names for function declarations in c++

Currently, for example, the function declaration symbol member for
checking whether multiplication *does not* overflow is called
`m_bv_smul_ovfl`.  Since we are introducing the upcoming smtlib2 symbols
that check that multpliciation *does* overflow, the not overflow check
symbols are renamed to `m_bv_smul_no_ovfl` etc.

* Implement smtlib overflow preds for multiplication

Smtlib2 is being extended to include overflow predicates for bit
vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI).
This commit introduces the predicates `bvumulo` and `bvsmulo` that
return `true` if the unsigned multiplication overflows or the signed
multiplication underflows or overflows, respectively.

* Move mul overflow predicates to BV logic

* Add a todo on illogical argument order

* Implement mk_unary_pred for bv

* Implement bvnego

* Implement bvuaddo

* Implement bvsaddo

* Implement bvusubo

* Implement bvssubo

* Implement bvsdivo
 2023-05-09 10:37:46 -07:00
Nikolaj Bjorner
62e1ec0698 Merge branch 'master' of https://github.com/z3prover/z3 2023-05-08 12:24:30 -07:00
Nikolaj Bjorner
2e441e38c9 fix #6713 fix #6714 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-08 12:24:20 -07:00
Guillaume Bagan
0c9a5f69fd
JS/TS: add Optimize class (#6712) 
* implement  Optimize class for the high level Typescript API

* javascript and wasm: add _malloc to exported functions

fix the bug https://github.com/Z3Prover/z3/issues/6709

* javascript: add tests for the Optimize class

* javascript: no reason that minimize and optimize must be constants
 2023-05-06 11:53:43 -07:00
Nikolaj Bjorner
6c24a70c44 remove debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-02 13:05:08 -07:00
Nikolaj Bjorner
f17691715b make default argument to ensure_def and mk_def explicit 
- insert also macro definitions into models
 2023-05-02 12:18:31 -07:00
Nikolaj Bjorner
c64d61bd0a formatting updates 2023-05-02 12:17:32 -07:00
Nikolaj Bjorner
392266c278 fix processing of else expression for model table 2023-05-02 12:16:58 -07:00
Nikolaj Bjorner
d5231f8b33 fix regressions #6703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-27 08:43:59 -07:00
Nikolaj Bjorner
c48dc69050 adding stubs to find fixed variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-26 19:39:42 -07:00
Nikolaj Bjorner
ef943347ee ensure assume-eqs is invoked after check-lia statically 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-26 11:16:15 -07:00
Nikolaj Bjorner
d2e3e4895e add instrumentation to theory_lra for shuffling final check 2023-04-26 10:05:00 -07:00
Nikolaj Bjorner
3029fb24a1 remove references to validating 2023-04-26 10:05:00 -07:00
Nikolaj Bjorner
50c855e2eb count gcd conflicts, log row id in rows 2023-04-26 10:05:00 -07:00
Nikolaj Bjorner
59bc070268 count gcd conflicts 2023-04-26 10:05:00 -07:00
Nikolaj Bjorner
ace6e8eea1 add gcd-conflicts stats, formatting updates 2023-04-26 10:04:59 -07:00
Nikolaj Bjorner
8fb4515872 remove redundant function, add checker function to test missed propagations 2023-04-26 10:04:59 -07:00
Nikolaj Bjorner
e689dea99c basic formatting updates 2023-04-26 10:04:59 -07:00
Nikolaj Bjorner
d4fa990b6e return diagnostics 2023-04-26 10:04:59 -07:00
Nikolaj Bjorner
d8156aeff3 weird latent bug in wmax: init() succeeds and it returns undef 2023-04-24 21:14:42 -07:00
Nikolaj Bjorner
fdd5c923ed use only maxres if there is a lexicographic objective, fix #6697 
- maxlex.enable heuristic does not work if it is chained among multiple objectives. Only maxres is set up to commit the proper constraints.
 2023-04-24 20:20:26 -07:00
Nikolaj Bjorner
7a689c3298 disable destructive equality resolution simplification if there are patterns 
- regression from F\star
- reported by @mtzguido (stlc_min.smt2)
 2023-04-24 17:59:41 -07:00
Nikolaj Bjorner
a2bac119d3 differentiate fixed from offset-eq in statistics 2023-04-18 08:40:51 -07:00
Nikolaj Bjorner
ec1480b12a fix #6693 2023-04-18 08:40:29 -07:00
Nikolaj Bjorner
cb041c1b6d fix #6689 2023-04-17 12:05:08 -07:00
Nikolaj Bjorner
1319b64bb0 fix #6692 2023-04-17 09:11:16 -07:00
Nikolaj Bjorner
97b66d13c0 fix soundness bug in disabled code 2023-04-15 17:09:05 -07:00
Nikolaj Bjorner
b75d81f3c2 fix #6690 2023-04-14 16:38:33 -07:00
Nikolaj Bjorner
624907823d add tests for distribution utility and fix loose ends 2023-04-13 11:19:06 -07:00
Nikolaj Bjorner
1a70ac75df fix #6687 2023-04-13 09:01:17 -07:00
Nikolaj Bjorner
b783879752 #6687 2023-04-13 08:45:17 -07:00
Nikolaj Bjorner
7cd8edce1f perf and memory smash fixes to internal node count routine 2023-04-12 21:01:05 -07:00
Nikolaj Bjorner
f0afbcbb87 fix #6686 2023-04-12 20:13:24 -07:00
Nikolaj Bjorner
eba0732629 fix #6675 
disable remove_unused_defs from pb-solver until it is integrated with model reconstruction.
 2023-04-12 19:50:13 -07:00
Nikolaj Bjorner
e8222433c3 count internal nodes, use to block expanding use of hoist, #6683 2023-04-12 19:40:31 -07:00
Nikolaj Bjorner
444238bc53 formatting updates 2023-04-12 19:40:31 -07:00
Nikolaj Bjorner
f61168cd53 module for maintaining probability distributions 2023-04-12 19:40:31 -07:00
Nikolaj Bjorner
0b5c38dea5 fix #6676 get rid of rem0 declare it to be mod0 semantics to simplify code paths 2023-04-11 16:46:43 -07:00
Nikolaj Bjorner
58a2a9c79c fix #6680 2023-04-11 14:42:47 -07:00
Nikolaj Bjorner
ccc4f2d382 fix #6682 2023-04-11 05:10:03 -07:00
Nikolaj Bjorner
368d60f553 add branch / cut selection heuristic from solver=2 
disabled for testing.
 2023-04-10 22:14:16 -07:00
Nikolaj Bjorner
bb44b91e45 fix #6677 2023-04-10 15:11:10 -07:00
Clemens Eisenhofer
98d3fabc24
Bugfix relevancy propagation + UP (old core) (#6678) 
* Some UP bugfixes in the new core

* Bugfix relevancy propagation + UP (old core)

* Revert smt_context.cpp
 2023-04-10 12:57:59 -07:00
Nikolaj Bjorner
4a142b0f81 fix #6623 2023-04-09 21:10:24 -07:00
Nikolaj Bjorner
e6ea81546e fix #6662 2023-04-08 17:14:39 -07:00
Nikolaj Bjorner
af9c760a68 fix #6670 2023-04-08 16:55:23 -07:00