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

17513 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5c7eaec566 #6364 - remove option of redundant clauses from internalization 
gc-ing definitions leads to unsoundness when they are not replayed.
Instead of attempting to replay definitions theory internalization is irredundant by default.
This is also the old solver behavior where TH_LEMMA is essentially never used, but is valid for top-level theory lemmas.
 2022-10-24 00:38:31 -07:00
Nikolaj Bjorner
c8e1e180ea prefix Boolean variables in log with b 2022-10-23 11:05:50 -07:00
Nikolaj Bjorner
6393ed78d7 remove useless log 2022-10-23 11:05:33 -07:00
Nikolaj Bjorner
ddbca68270 minor formatting update 2022-10-23 11:05:09 -07:00
Nikolaj Bjorner
4a1d76cf49 #6418 - add best-effort for nested and/or (from ite literals) 2022-10-23 11:03:51 -07:00
Nikolaj Bjorner
071a1447e3 fix #6418 2022-10-23 11:03:00 -07:00
Nikolaj Bjorner
e3a44254c9 fix #6415 2022-10-22 11:18:16 -07:00
Nikolaj Bjorner
7eee7914bd align format of quantifier instantiation with new core 
So far the format is

(forall ((x Int)) body) (not (body[t/x]))

The alternative could be the clause

(not (forall ((x Int)) body)) body[t/x]

they just better be consistent between engines
 2022-10-21 15:26:00 -07:00
Nikolaj Bjorner
53adc2afee update debugging information for new core 2022-10-21 15:24:44 -07:00
Nikolaj Bjorner
ad5fa9433f add experiment with quot-rem encoding 
experiment seeks to determine whether quot-rem encoding can substitute the division circuit encoding.
A first test suggests it makes no difference.
 2022-10-21 09:25:45 -07:00
Nikolaj Bjorner
31914d8ecf simplify purified expressions 2022-10-21 03:47:57 -07:00
Nikolaj Bjorner
842e8057bc log also quantifier generation (besides binding) 
We add also logging for quantifier generation.
It is auxiliary information that is of use for diagnostics (axiom profiler).
 2022-10-20 17:49:15 -07:00
Nikolaj Bjorner
c1b355f342 #6364 
throttle on upwards propagation of default was too restrictive
 2022-10-20 17:48:17 -07:00
Nikolaj Bjorner
6d6752b2aa #6364 2022-10-20 16:39:43 -07:00
Nikolaj Bjorner
354bc50400 Update .gitignore 2022-10-20 13:15:43 -07:00
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