mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity
17822 commits 23 branches 48 tags 156 MiB
Commit graph

17822 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner c2062c9b3d x 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-27 17:32:29 -07:00
Nikolaj Bjorner 1441c0daea move set_var_interval2 to header 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 11:15:29 -07:00
Nikolaj Bjorner e9e1fb2f37 separate out functions that call set_var_interval1/2 into functions for linker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 10:06:11 -07:00
Nikolaj Bjorner f533220482 fixing arith build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 09:28:30 -07:00
Nikolaj Bjorner cd9f0d1a6c fix RISC build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-24 18:02:04 -07:00
Nikolaj Bjorner fc218aeeb5 change internalize_mod to internalize_div to to handle real division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-24 17:25:07 -07:00
Nikolaj Bjorner 4b1fb73e76 change internalize_mod to internalize_div to to handle real division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-24 17:23:53 -07:00
Nikolaj Bjorner 57152430f9 working on multiple intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 18:05:17 -07:00
Nikolaj Bjorner ee86ea83e4 just branch on = 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-27 09:05:00 -07:00
Nikolaj Bjorner 2ee91d866a control branching with parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 19:34:45 -07:00
Nikolaj Bjorner a8f867f145 consolidate settings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 18:41:27 -07:00
Nikolaj Bjorner e84d1e9d96 add branching on literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 08:30:01 -07:00
Nikolaj Bjorner caf314e569 experiment with better gcd test for non-linear arihmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-20 17:05:48 -07:00
Nikolaj Bjorner 3ef0db019a updated patch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-15 11:32:06 -07:00
Nikolaj Bjorner aafc9656e1 patching can break monomials, so rerun nla 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-09 13:34:12 -07:00
Nikolaj Bjorner 37ec667102 new (and fixed) patcher 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-08 14:37:42 -07:00
Nikolaj Bjorner e7065e3984 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-08 09:04:41 -07:00
Nikolaj Bjorner 9c4003d12e fix to arithmetic internalize for multiplier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-06 11:06:13 -07:00
Nikolaj Bjorner 05f63277cf fixes to arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-06 07:05:34 -07:00
Nikolaj Bjorner a7b3dae262 save state of arith 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-03 11:52:15 -07:00
Nikolaj Bjorner ffd4323573 experiment with delayed disequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-01 22:24:55 +02:00
Nikolaj Bjorner ee216b5274 final 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-31 22:09:29 +02:00
Nikolaj Bjorner 88c982ff0b experiments with arith 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-31 16:55:32 +02:00
Nikolaj Bjorner 4303a1f7fe added div/mod handling 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-24 09:33:29 +01:00
Nikolaj Bjorner cc38b27f63 Merge branch 'master' of https://github.com/z3prover/z3 into arith 2023-05-22 16:09:38 +01:00
Nikolaj Bjorner 8a996dc2ac instrument for align solver=2, 6 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 16:09:22 +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 fca9939371 Merge branch 'master' of https://github.com/Z3Prover/z3 into arith 2023-05-14 15:54:16 -07:00
Nikolaj Bjorner e5231c040d arith updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-14 15:53:58 -07: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