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

18001 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 621f1f8a85 sanity check parameters #6737 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-30 09:44:06 +02:00
Manuel Carrasco 230306ddfc
Add solver::interrupt to Python's API. (#6739) 2023-05-28 21:04:36 +02:00
Nikolaj Bjorner 5e1869d8eb fix #6734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-26 09:48:58 +01:00
ditto 11264c38d8
Java user propagator interface (#6733) 
* Java API: user propagator interface

* Java API: improved user propagator interface

* Java API: Add UserPropagatorBase.java

* Remove redundant header file

* Initialize `JavaInfo` object and error handling

* Native.UserPropagatorBase implements AutoCloseable

* Add Override annotation
 2023-05-24 18:27:28 +01:00
Nikolaj Bjorner 2c21072c99 remove stub class, it may as well go into NativeStatic.txt as C++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 18:23:10 +01:00
Nikolaj Bjorner b93529997e more stubs #6097 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 16:25:54 +01:00
Nikolaj Bjorner 7963ecaf63 stubs for #6097 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 16:21:34 +01:00
Nikolaj Bjorner a68f91f0a6 fix #6729 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 14:07:12 +01:00
Nikolaj Bjorner 06ea765b82 fix #6721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-13 09:46:49 -07:00
Michał Górny c9d8e646ed
fix missing <cstdint> include (#6720) 
Fix missing <cstdint> include in src/util/tptr.h that causes build
failure with GCC 13:

```
In file included from /tmp/z3/src/util/region.cpp:53:
/tmp/z3/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’:
/tmp/z3/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type
   29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
      |                                                              ^~~~~~~~~
/tmp/z3/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’
   82 |         m_curr_ptr = ALIGN(char *, new_curr_ptr);
      |                      ^~~~~
/tmp/z3/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘<cstdint>’; did you forget to ‘#include <cstdint>’?
   56 | #include "util/page.h"
  +++ |+#include <cstdint>
   57 |
```
 2023-05-13 09:37:57 -07:00
Tomasz Kłoczko 520e692a43
Fix building with gcc 13 (#6723) 
Trivial fix to build with gcc 13 reported in #6722.

Signed-off-by: Tomasz Kłoczko <kloczek@github.com>
 2023-05-13 09:37:35 -07:00
Nikolaj Bjorner f928b44606 update version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-12 14:53:52 -07:00
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