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

16805 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes f3c00a0a03 attempt to fix windows build bot 2022-06-17 18:05:19 +01:00
Nuno Lopes c3407fc304 fix build of tests 2022-06-17 17:11:18 +01:00
Nuno Lopes fcbbf7ba76 fix build warning+error in c++ example 2022-06-17 16:43:34 +01:00
Nuno Lopes d9fcfdab34 fix debug build 2022-06-17 14:35:33 +01:00
Nuno Lopes 73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Nuno Lopes 70bcf0b51d reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields 
Yes, those 8 bytes are yours now, use responsibly.
 2022-06-17 12:07:15 +01:00
Nikolaj Bjorner 08c44bc6f6 remove unused static features 
remove static features that tax solving time on large instances.
 2022-06-16 15:40:01 -07:00
Nikolaj Bjorner 477e9625ef Don't reset the cache between applications of replace 
tactic/lia2card shows a huge slowdown because the same replace function is called on thousands of assertions. Each time the cache gets reset with thousands of entries - they are all the same.
So don't reset the cache just because... Instead reset the cache if m_refs grows large.
 2022-06-16 15:40:01 -07:00
Nikolaj Bjorner 99b606b861 add logging 2022-06-16 15:40:00 -07:00
Olaf Tomalka 7fdcbbaee9
Add high level bindings for js (#6048) 
* [Draft] Added unfinished code for high level bindings for js

* * Rewrote structure of js api files
* Added more high level apis

* Minor fixes

* Fixed wasm github action

* Fix JS test

* Removed ContextOptions type

* * Added Ints to JS Api
* Added tests to JS Api

* Added run-time checks for contexts

* Removed default contexts

* Merged Context and createContext so that the api behaves the sames as in other constructors

* Added a test for Solver

* Added Reals

* Added classes for IntVals and RealVals

* Added abillity to specify logic for solver

* Try to make CI tests not fail

* Changed APIs after a round of review

* Fix test

* Added BitVectors

* Made sort into getter

* Added initial JS docs

* Added more coercible types

* Removed done TODOs
 2022-06-14 09:55:58 -07:00
Nikolaj Bjorner 3d00d1d56b prepare for equality propagation from Grobner basis 
Attempt to remedy performance regressions from the new solver core for NLA. It misses easy lemmas, presumably due to weaker bounds information.
 2022-06-14 09:51:07 -07:00
Nikolaj Bjorner 8e2027107d fix spacing 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 55421afd61 fix regression in top-sort fix #6060 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 637120ced5 Treat arguments to recursive functions as beta redexes 
An argument to a recursive function would escape the scope of the function application when the recursive function definitions are unfolded. Therefore, such argument occurrences need not be considered for extensional equality / equality sharing.

This filter is mostly relevant for recursive functions that take a lambda expression as argument. Lambda expressions / arrays that occur in shared occurrences are checked for extensionality.
 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 25ad5cb073 prepare ground for drup trim 
By not deleting justifications in base level unit literals it is possible for drup-trim to inspect the trail for dependencies - which clauses were used to derive a literal.
 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 35d4605425 remove spurious output to stdout 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 04f94d818f fix #6091 2022-06-14 09:51:06 -07:00
Dominic Steinhöfel 46bc726391
Better error message for mismatching sorts in substitutions in z3.substitute (#6093) 2022-06-13 13:46:30 -07:00
Nikolaj Bjorner 470bf27d1d drat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-11 09:15:32 -07:00
Nikolaj Bjorner 9cd339841a for Arie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 18:07:54 -07:00
Nikolaj Bjorner 994dab8eb6 add pre-filter for F* use case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 17:56:48 -07:00
Nikolaj Bjorner 8efa3c8ade introduce notion of beta redex to deal with lambdas in non-extensional positions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 17:35:01 -07:00
Nikolaj Bjorner b9b5377c69 add a way to supress lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 14:37:25 -07:00
Nikolaj Bjorner 5db133f875 add a way to supress lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 14:35:20 -07:00
Nikolaj Bjorner 97437bce4c Update sat_params.pyg 2022-06-09 10:09:30 -07:00
Nikolaj Bjorner 828850f298 prepare for trim 2022-06-09 10:08:57 -07:00
Nikolaj Bjorner c5847504ff contains-partition 2022-06-08 12:20:45 -07:00
Nikolaj Bjorner 6a1193eebd reorg if-then-else structure 2022-06-08 10:00:45 -07:00
Nikolaj Bjorner 72a6384353 time overflow before stack overflow 2022-06-08 10:00:16 -07:00
Nikolaj Bjorner e468386359 #5656 
guard __del__ operator by checking if library was unloaded.
 2022-06-08 09:59:29 -07:00
Nikolaj Bjorner dee6c30f1b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-08 08:05:19 -07:00
Nikolaj Bjorner 80604c7bc5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-08 07:00:59 -07:00
Nikolaj Bjorner 51ed13f96a update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-08 06:28:24 -07:00
Nikolaj Bjorner 0e6c64510a display model in add/del format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-07 13:14:36 -07:00
dependabot[bot] a7b6f30b29
Bump docker/metadata-action from 3 to 4 (#6086) 2022-06-07 19:41:36 +01:00
Nikolaj Bjorner 35986f3979 fix #6084 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-07 11:29:57 -07:00
Nikolaj Bjorner fe08c9976e fix #6081 2022-06-06 11:29:11 -07:00
Nikolaj Bjorner cc045debac again 2022-06-06 11:23:18 -07:00
Nikolaj Bjorner bb6c274ad3 fix #6085 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-06 10:00:08 -07:00
Nikolaj Bjorner dca1dcca6d ea 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-06 08:42:47 -07:00
Nikolaj Bjorner b629960afb proof format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-06 07:18:33 -07:00
Nikolaj Bjorner ea365de820 add cut 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-04 11:59:00 -07:00
Nikolaj Bjorner da9382956c use common functionality 2022-06-04 11:36:05 -07:00
Christoph M. Wintersteiger f77608ed88
Add interpreted versions of unspecified cases of fp.to_ieee_bv and fp.to_real (#6077) 2022-06-04 17:53:23 +01:00
Christoph M. Wintersteiger d722c73d4c
Fix corner case in MPF FMA (#6075) 2022-06-04 15:55:26 +01:00
Christoph M. Wintersteiger 6422a6b5a7
Fix rounding bug in to_fp (#6074) 2022-06-04 14:32:08 +01:00
Christoph M. Wintersteiger cb67f90f1a
Merge pull request #6072 from wintersteiger/cwinter_warnings 
Fix a couple compiler warnings
 2022-06-04 11:40:14 +01:00
Christoph M. Wintersteiger 4421f7d575
Merge pull request #6073 from wintersteiger/cwinter_deflt_rm_py 
Change FP default rounding mode in the Python API
 2022-06-04 10:48:38 +01:00
Christoph M. Wintersteiger 33454193d4
Change FP default rounding mode in the Python API 2022-06-04 08:45:52 +01:00
Christoph M. Wintersteiger ed7db892f9
Fix a couple compiler warnings 2022-06-04 08:00:56 +01:00