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

16896 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 45a4b810de fixup github connection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 15:12:05 -07:00
Nikolaj Bjorner 21033790be add parameter documentation to nightly 2022-08-16 15:07:19 -07:00
Nikolaj Bjorner fe00e95f72 remove \r from output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 09:20:50 -07:00
Nikolaj Bjorner 9d6de2f873 parameters neatified 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 09:14:34 -07:00
Nikolaj Bjorner 498b6de3a7 finish parameter help 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:29:24 -07:00
Nikolaj Bjorner b169292743 add parameter descriptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:26:53 -07:00
Nikolaj Bjorner 583dae2e27 enable nested division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-15 16:11:00 -07:00
dependabot[bot] 681ed957d2 Bump docker/build-push-action from 3.1.0 to 3.1.1 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3.1.0 to 3.1.1.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v3.1.0...v3.1.1)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
 2022-08-15 12:24:41 -07:00
jofleish 88b3e0c944 Update github service connection 2022-08-15 12:24:25 -07:00
jofleish 88f4664c65 Standardize ubutu-latest vmImage 2022-08-15 07:55:45 -07:00
Nikolaj Bjorner e0aa32e6c5 fix #6270 
MBQI asserts auxiliary function definitions to handle models of arrays. This is unsound if the definition contains a model value.
 2022-08-15 00:13:32 -07:00
Nikolaj Bjorner a0d4a8c21c update diagnostics 2022-08-15 00:12:44 -07:00
Nikolaj Bjorner 138f0d269c fix regression found by fuzzers fix #6271 2022-08-14 12:26:33 -07:00
Nikolaj Bjorner 1d87592b13 fixes to mod/div elimination 
elimination of mod/div should be applied to all occurrences of x under mod/div at the same time. It affects performance and termination to perform elimination on each occurrence since substituting in two new variables for eliminated x doubles the number of variables under other occurrences.

Also generalize inequality resolution to use div.

The new features are still disabled.
 2022-08-14 11:34:03 -07:00
Nikolaj Bjorner f014e30d46 disable case1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-13 08:53:19 -07:00
Nikolaj Bjorner d80e2fb61d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-13 08:49:07 -07:00
Nikolaj Bjorner 16a948683f Merge branch 'master' of https://github.com/z3prover/z3 2022-08-13 07:07:34 -07:00
Nikolaj Bjorner fa91a644d3 make extensionality commutative 2022-08-13 07:07:14 -07:00
Nikolaj Bjorner 5669cf65bc bug fixes to mod/div quantifier elimination features 2022-08-13 06:18:13 -07:00
Nikolaj Bjorner 88b6c4a30d pdate decl collection to include functions under arrays 
Signedoff-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-12 13:45:16 -07:00
Bruce Mitchener 72f4ee9230 api: Correctly map OP_BSREM0 to Z3_BSREM0. 2022-08-12 14:40:16 -04:00
Nikolaj Bjorner 550d6914b1 updates to div/mod handling in quantifier projection 
note: the new code remains disabled at this point.
 2022-08-12 14:39:33 -04:00
Nikolaj Bjorner d272becade fixes for division 2022-08-12 11:54:26 -04:00
Nikolaj Bjorner f989521a8c add initial skeleton for xor-solver 2022-08-12 11:54:10 -04:00
Nikolaj Bjorner b6d71fccd8 fix #6265 2022-08-12 10:22:22 -04:00
Nikolaj Bjorner 03385bf78d improve quantifier elimination for arithmetic 
This update changes the handling of mod and adds support for nested div terms.

Simple use cases that are handled using small results are given below.

```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (exists ((x Int)) (and (<= y (* 10 x)) (<= (* 10 x) z))))
(apply qe2)
(reset)

(declare-const y Int)
(assert (exists ((x Int)) (and (> x 0) (= (div x 41) y))))
(apply qe2)
(reset)

(declare-const y Int)
(assert (exists ((x Int)) (= (mod x 41) y)))
(apply qe2)
(reset)
```

The main idea is to introduce definition rows for mod/div terms.
Elimination of variables under mod/div is defined by rewriting the variable to multiples of the mod/divisior and remainder.

The functionality is disabled in this push.
 2022-08-12 10:20:43 -04:00
Nikolaj Bjorner 786280c646 print skolem declarations only for lemma tracing 2022-08-11 11:34:54 +03:00
Nikolaj Bjorner 791ca02ab1 formula simplification example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-11 09:33:36 +03:00
Nikolaj Bjorner b55ad5f20e fix #6267 2022-08-11 09:31:54 +03:00
Nikolaj Bjorner 49064252ac fix issues for user-propagator from new core 2022-08-09 14:56:27 +03:00
Nikolaj Bjorner f27485dae7 avoid push/pop if diseq/eq are not defined 2022-08-09 11:33:29 +03:00
Nikolaj Bjorner 78eaefe5a8 move solver-params to params 2022-08-08 11:34:41 +03:00
Nikolaj Bjorner 77a313ff76 redo #6242 
revert to byte based high watermark
add mb based high watermark
 2022-08-08 11:26:18 +03:00
Nikolaj Bjorner 63f48f8fd4 add options for logging learned lemmas and theory axioms 
- add solver.axioms2files
  - prints negated theory axioms to files. Each file should be unsat
- add solver.lemmas2console
  - prints lemmas to the console.
- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
 2022-08-08 11:18:56 +03:00
Nikolaj Bjorner 410eed9bd5 #6116 2022-08-07 11:09:43 +03:00
Nikolaj Bjorner 8e077d8ef9 #6116 2022-08-07 10:25:04 +03:00
Nikolaj Bjorner 539d44464f #6196 
map can be simplified
 2022-08-07 10:17:24 +03:00
Nikolaj Bjorner f34317d604 #6196 2022-08-07 09:44:10 +03:00
Nikolaj Bjorner a4ea281602 fix #6260 2022-08-06 08:21:52 +03:00
Bruce Mitchener 5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Arie Gurfinkel aa0719abae model_based_opt: fix enabling complete resolution 
a bug prevented an optimization to be enabled
 2022-08-05 18:11:23 +03:00
Nikolaj Bjorner 80c516bb50 squash stores 2022-08-05 13:57:35 +03:00
Bruce Mitchener 6835522a7f z3++.h: No longer include unused sstream. 
This makes some code using the C++ API have to include `<sstream>`
if they used the functionality but didn't include it themselves.
 2022-08-05 09:41:49 +03:00
Nikolaj Bjorner e48474ec0e Merge branch 'master' of https://github.com/z3prover/z3 2022-08-05 09:20:00 +03:00
Nikolaj Bjorner c51af91256 #6257 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-05 09:19:49 +03:00
Arie Gurfinkel a9b7348b4b (cmake): fix visibility on shell z3 binary 
Commit #b361226 changed symbol visibility from a global to a local option.
This creates inconsistency for shell that is compiled as an executable rather
than as z3 component.

This commit adds same local options to shell target in cmake.

Prior to the fix, clang on OSX complains with lots of warnings about symbol visibility
being different in different translation units that are linked together
 2022-08-05 09:00:40 +03:00
Nikolaj Bjorner 78a0f57398 for #6257 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-05 08:09:39 +03:00
Bruce Mitchener 7eb1e6dd23 userPropagator: Compile as C++20. 
Using std::unordered_map::contains requires C++20.
 2022-08-05 07:41:14 +03:00
Bruce Mitchener 1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Bruce Mitchener 08165f5367 No need to return a const bool. 2022-08-05 07:40:19 +03:00