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
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