Commit Graph

1583 Commits

Author SHA1 Message Date
Nikolaj Bjorner
1974c224ab add demodulator simplifier
refactor demodulator-rewriter a bit to separate reusable features.
2022-12-04 09:39:28 -08:00
Nikolaj Bjorner
847aec1d30 update dependencies 2022-11-30 22:48:10 -08:00
Nikolaj Bjorner
7b9dfb8e1e update dependencies for python build 2022-11-30 13:43:40 +07:00
Nikolaj Bjorner
4e9f21c2a1 add rewriter and seq simplifiers 2022-11-25 15:16:14 +07:00
Nikolaj Bjorner
203652da74 add converters module to python build 2022-11-03 05:26:06 -07:00
Nikolaj Bjorner
e57674490f adding simplifiers layer
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
2022-11-02 08:51:30 -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
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
ea55f69a92 fix python build 2022-10-16 23:42:11 +02:00
Nikolaj Bjorner
6eb2d2acfa update dependencies for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-28 11:25:36 -07:00
Nikolaj Bjorner
ff679e0fce increment version number 2022-09-11 19:02:44 -07:00
Thomas Pani
adf6e98cdf Handle _out(STRING) parameters in Java API (#6325) 2022-09-06 15:29:12 -07:00
Nikolaj Bjorner
8e6f17ebd0 inc version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-03 15:47:12 -07:00
John Fleisher
f72cdda5fb Change to 4 digit assembly version (#6297)
* WiP: test build specific version number

* update mk_win_dist for assembly-version

* Add print statements for version

* remove stray semicolon

* undo quote change in projectstr

* nit fixes

* revert print formatting for Mac build

* fix spaces
2022-08-31 06:46:06 -07:00
Nikolaj Bjorner
4d29925c3f build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-28 18:43:50 -07:00
Nikolaj Bjorner
ce1f3987d9 fix unsoundness in quantifier propagation #6116 and add initial lemma logging 2022-08-23 19:10:01 -07:00
Nuno Lopes
d5d77dfe64 minor code simplifications 2022-08-20 12:56:45 +01:00
Nikolaj Bjorner
514eaf33aa Merge branch 'master' of https://github.com/z3prover/z3 2022-08-18 19:07:55 -07:00
Nikolaj Bjorner
600b4491aa don't forget parameter documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-18 19:07:39 -07:00
Nikolaj Bjorner
540e36e6cb roll version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-18 15:47:08 -07:00
John Fleisher
b3f4d3fdc7 Publish Z3 symbols (#6280)
* WiP: publish symbols for package

* set debugtype to full

* fix internal nuget feed publishing

* Try pipeline github authorization

* Update github service connection

* WiP: try symbol publish in build

* try Z3Prover for GitHub connection

* WiP: collect symbols

* revert symbol type to pdbonly (only portable is not supported for publishing)

* Publish symbols in nightly and release

* Revert this: comment out publish to test release build pipe

* restore publishing

* Turn of index sources to eliminate warning that it is not supported for Github

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-17 07:30:55 -07:00
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
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