mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity
18798 commits 49 branches 53 tags 182 MiB
Commit graph

18798 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
edad727cd5 #6364 
ensure substitutions are applied to eliminate internal variables from results
 2022-10-20 13:14:54 -07:00
Nikolaj Bjorner
5976978062 move std functions up for potential alignment issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 09:11:15 -07:00
Nikolaj Bjorner
fc30461828 unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 09:09:06 -07:00
Nikolaj Bjorner
6292b06c67 ensure that initialization order for euf_solver is aligned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:48:15 -07:00
Nikolaj Bjorner
2f1514a259 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:38:23 -07:00
Nikolaj Bjorner
65ea4925b3 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:37:21 -07:00
Nikolaj Bjorner
2842c27e92 #6364 2022-10-20 04:48:13 -07:00
Nikolaj Bjorner
f6595c161f add examples with proof replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 17:43:56 -07:00
Nikolaj Bjorner
88d10f7fe4 add example for monitoring proof logs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 13:37:51 -07:00
Nikolaj Bjorner
a90c4f65cf increment version per release notes 
incrementing minor version because the API has a new function.
This breaks log replay against old dlls and inclusion against z3++.h.
 2022-10-19 13:21:26 -07:00
dependabot[bot]
f6d554118f
Bump docker/build-push-action from 3.1.1 to 3.2.0 (#6405) 2022-10-19 21:14:43 +01:00
Nikolaj Bjorner
4c79e63c1b Update parse-api.ts 2022-10-19 12:52:58 -07:00
Nikolaj Bjorner
b084852397 update release notes, fix bug in replay of Boolean variables in new core 2022-10-19 12:12:32 -07:00
Nikolaj Bjorner
07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -07:00
Nikolaj Bjorner
77cbd89420 remove once pragma from cpp file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-18 14:57:49 -07:00
Nikolaj Bjorner
eaf52f4c32 fix infinite loop issue in def::operator+, other issues remain though for #6404 
The example from #6404 results in an incorrect result. It uses integer division on private variables where MBQI support is new and not tested for substitutions.
 2022-10-18 14:52:30 -07:00
Nikolaj Bjorner
cdfab8cb13 wip - add bit-vector validator plugins and logging 2022-10-18 14:50:21 -07:00
Nikolaj Bjorner
464d52babe fix #6410 
regression after introducing beta-redex optimization
 2022-10-18 12:34:45 -07:00
Nikolaj Bjorner
f0b85716a9 wip - proof logging fixes 2022-10-18 11:20:56 -07:00
Nikolaj Bjorner
1fc77c8c00 wip - proof checking 
fixes to smt_theory_checker. Generalize it to apply to arrays and fpa.
Missing: bv
 2022-10-18 09:02:50 -07:00
Nikolaj Bjorner
7b3a634b8d wip - features and bug-fixes to proof logging 2022-10-18 07:54:49 -07:00
Nikolaj Bjorner
3bf1b606df remove on-the fly ackerman reduction because it interferes with conflict resolution 2022-10-18 07:53:42 -07:00
Nikolaj Bjorner
b758d5b2b1 wip - proof checking, add support for distinct, other fixes 2022-10-17 17:51:10 -07:00
Walden Yan
f175fcbb54
JS/TS API Array support (#6393) 
* feat: basic array support

Still need deeper type support for Arrays

* fixed broken format rules

* spaces inside curly

* feat: range sort type inference

* feat: better type inference in model eval

* doc: fixed some incorrect documentation

* feat: domain type inference

* feat: addressed suggestions

* feat: addressed suggestions

* chore: moved ts-expect from deps to dev-deps

* test: added z3guide examples

* fix: removed ts-expect from dependencies again

* docs: fixed some documentation
 2022-10-17 11:10:36 -07:00
Nikolaj Bjorner
d4885abdc0 fix #6400 
bi-implication was treated as an atomic formula leading to incorrect projection.
 2022-10-17 11:00:21 -07:00
Nikolaj Bjorner
541aba308c fix #6401 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-17 10:27:15 -07:00
Nikolaj Bjorner
dc1bce33f6 Merge branch 'master' of https://github.com/z3prover/z3 2022-10-17 10:17:40 -07:00
Nikolaj Bjorner
98fe2e637a add generic theory lemma in default case. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-17 10:17:08 -07:00
Gleb Popov
5b76a7c2f2
Enable HAS_MALLOC_USABLE_SIZE on FreeBSD (#6402) 2022-10-17 10:14:04 -07:00
Nikolaj Bjorner
a25247aa7b wip - remove stale skaffolding for retrieving sub-hints. 2022-10-16 17:18:08 -07:00
Nikolaj Bjorner
d88384fd51 fix compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-16 15:03:46 -07:00
Nikolaj Bjorner
3ed791b16a fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-16 15:01:42 -07:00
Nikolaj Bjorner
ea55f69a92 fix python build 2022-10-16 23:42:11 +02:00
Nikolaj Bjorner
ac1552d194 wip - updates to proof logging and self-checking 
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line.

when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation.

new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation.

z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
 2022-10-16 23:33:30 +02:00
Nikolaj Bjorner
993ff40826 fixes to proof logging and checking 2022-10-15 12:42:50 +02:00
Nikolaj Bjorner
4388719848 adjust logging 2022-10-14 18:56:18 +02:00
Nuno Lopes
87e45221fd add missing break stmt to example 
Reported by Henrique Preto
 2022-10-14 09:43:18 +01:00
Nikolaj Bjorner
e2cfc53c9f #6364 
skip proof hint unless proofs are on
 2022-10-13 15:31:58 +02:00
Nikolaj Bjorner
9bf5e3f5fc fixes for #6388 2022-10-13 15:22:19 +02:00
Nikolaj Bjorner
2449ba93c5 add (disabled) experiment to use quot-rem instead of division circuit 2022-10-13 15:20:43 +02:00
Nikolaj Bjorner
8a30128933 formatting updates 2022-10-13 15:20:24 +02:00
Nikolaj Bjorner
93e1db0b0b fix #6398 2022-10-13 11:16:14 +02:00
Nikolaj Bjorner
ddf4895c2f admit timeouts and other resource limits for get-core #6310 2022-10-12 12:09:52 +02:00
Nuno Lopes
a7f018aa03 fix compiler warnings 2022-10-12 10:02:21 +01:00
Nuno Lopes
8ad480ab59 fix compiler warnings 2022-10-12 09:43:50 +01:00
Nikolaj Bjorner
a2e0646eed wip - proof checker 2022-10-12 09:34:49 +02:00
Nikolaj Bjorner
ace727ee0f fix #6391 2022-10-12 09:34:49 +02:00
Nuno Lopes
a41520acf1 mpf: fix some string copies 2022-10-11 11:59:29 +01:00
Nikolaj Bjorner
1b3684c9c1 wip - fixes to implied-eq proof hints 2022-10-11 09:54:00 +02:00
Nikolaj Bjorner
ffeb8f4572 wip - tseitin check 
```
(set-option :sat.euf true)
(set-option :sat.smt.proof tseitinproof.smt2)
(set-option :tactic.default_tactic smt)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)

(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 Bool)
(declare-const a17 Bool)
(declare-const a18 Bool)
(declare-const a19 Bool)

(declare-const x1 Bool)
(declare-const x2 Bool)
(declare-const x3 Bool)
(declare-const x4 Bool)
(declare-const x5 Bool)
(declare-const x6 Bool)
(declare-const x7 Bool)
(declare-const x8 Bool)
(declare-const x9 Bool)

(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const b4 Int)

(assert (= x1 (and a1 a2)))
(assert (= x2 (or a3 a4)))
(assert (= x3 (=> a5 a6)))
(assert (= x4 (=  a7 a8)))
(assert (= x5 (if a9 a10 a11)))
(assert (= x6 (=> a12 a13)))
(assert (= x7 (xor a1 a2 a3)))
(assert (= x7 (xor a1 a2 a3 a4 a5 (not a6))))
(assert (= x8 (= (ite a1 b1 b2) b3)))
(check-sat)
(exit)

```
 2022-10-11 09:21:36 +02:00