mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Code Activity
19782 commits 43 branches 52 tags 176 MiB
Commit graph

19782 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
ccb250c32b fix #6671 2023-04-08 16:39:40 -07:00
Clemens Eisenhofer
7b513b4a40
Some UP bugfixes in the new core (#6673) 2023-04-08 12:50:46 -07:00
Nikolaj Bjorner
84b9204616 inherit and reset rlimit counter on children limits 
addresses rlimit leak reported by @mtzguido
 2023-04-05 16:39:21 -07:00
Nikolaj Bjorner
f8242c58dd fix regression from Grobner port 
- scan_for_linear returns true if it finds a new linear equation. It then should break GB.
- if scan_for_linear returns false, it should still allow try_modify_eqs.
This behavior was masked by requiring scan_for_linear to always be true before
allowing try_to_modify_eqs.

based on repro from Guido Martinez @mtzguido
 2023-04-04 22:29:22 -07:00
Nikolaj Bjorner
479f844200 fix #6661 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-02 11:14:20 -07:00
Nikolaj Bjorner
def83ed26e fix #6661 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-02 11:13:37 -07:00
Nikolaj Bjorner
5b385bd2fe fix #6665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-02 10:58:21 -07:00