mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
16773 commits 24 branches 48 tags 158 MiB
Commit graph

1746 commits

Author SHA1 Message Date
Nikolaj Bjorner
efa74fe6c6 fix #6180 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-21 12:20:36 -07:00
Nikolaj Bjorner
cf5a8fd248 fix validation code for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-21 08:58:32 -07:00
Nikolaj Bjorner
32c0d1f636 fix #6168 2022-07-20 21:48:47 -07:00
Nikolaj Bjorner
5c54d6564b fix #6143 2022-07-11 12:09:15 -07:00
Nikolaj Bjorner
b68af0c1e5 working on reconciling perf for arithmetic solvers 
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.

The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.

The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
 2022-07-11 07:38:51 -07:00
Nikolaj Bjorner
580ed31afd fix types and incompleteness for feature #6104 2022-07-06 01:08:54 -07:00
Nikolaj Bjorner
f82ca197d2 #6104 also in the new core 2022-07-05 12:38:07 -07:00
Nikolaj Bjorner
0353fc38ff fix #6127 again 
this time adding inheritance to the recfun plugin so it properly contains the recursive definitions from the source.
 2022-07-04 12:42:11 -07:00
Mark Marron
e054f1683c
fixing compiler warn (missing override) (#6125) 2022-06-30 15:39:28 -07:00
Nikolaj Bjorner
8ab8b63a4c fix incorrect mod axiomatization #6116 2022-06-29 12:32:04 -07:00
Nikolaj Bjorner
1a9122663c remove unsound axioms, fix #6115 2022-06-29 11:16:10 -07:00
Nikolaj Bjorner
4c8f6b60ce fix #6107 2022-06-27 20:51:30 -07:00
Nikolaj Bjorner
61f5489223 fix #6107 2022-06-27 16:53:18 -07:00
Nikolaj Bjorner
1fcf7cf0b7 add nl div mod axioms 2022-06-27 09:02:53 -07:00
Clemens Eisenhofer
2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096) 
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
 2022-06-19 10:49:25 -07: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
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
Nikolaj Bjorner
470bf27d1d drat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-11 09:15:32 -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
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
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
f652c57bfe fix proof checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-03 20:17:59 -07:00
Nikolaj Bjorner
3d1e03e00a add start of self-contained proof checker for arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-03 09:11:02 -07:00
Nikolaj Bjorner
a9d70fca1a fix #6061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-31 19:09:10 -07:00
Nikolaj Bjorner
e9cff33feb fix #5068 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-30 11:24:58 -07:00
Nikolaj Bjorner
da3f31697b fix proof checking for bounds propagation 2022-05-30 10:18:16 -07:00
Nikolaj Bjorner
cb279fba2b fix sign for binary propagation hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-29 10:32:05 -07:00
Nikolaj Bjorner
bffa7ff2f6 add hint verification, combine bounds/farkas into one rule 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-29 10:12:05 -07:00
Nikolaj Bjorner
48701826f1 indent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 13:57:03 -07:00
Nikolaj Bjorner
dd46224a1d use structured proof hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 09:37:41 -07:00
Nikolaj Bjorner
8c95dff33b cnf 2022-05-22 09:10:26 -04:00
Nikolaj Bjorner
386c511f54 core opt 2022-05-21 10:27:37 -04:00
Nikolaj Bjorner
7497856ded add ignore int to new arithmetic solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-11 15:14:22 -07:00
Nikolaj Bjorner
ad2445e423 gauss jordan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-09 16:33:15 -07:00
Nikolaj Bjorner
dcc01b874a prep for pragmas 2022-05-09 11:18:15 -07:00
Nikolaj Bjorner
7def610a69 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:31:11 -07:00
Nikolaj Bjorner
14214c5a07 exposing user propagators over .Net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 11:08:40 -07:00
Nikolaj Bjorner
367bfedab0 add min/max diff in final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 07:39:38 -07:00
Nikolaj Bjorner
c29cfa81ae prep for max/min diff 2022-05-04 02:08:11 -07:00
Nikolaj Bjorner
81d97a81af enable nested ADT and sequences 
add API to define forward reference to recursively defined datatype.
The forward reference should be used only when passed to constructor declarations that are used in a datatype definition (Z3_mk_datatypes). The call to Z3_mk_datatypes ensures that the forward reference can be resolved with respect to constructors.
 2022-04-27 09:58:38 +01:00
Nikolaj Bjorner
8e2f09b517 #5778 - ensure arrays used inside of extensionality function are treated as shared 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-25 17:17:59 +01:00