mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity
17877 commits 22 branches 48 tags 156 MiB
Commit graph

17877 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner b78c7887f6 updating release-readme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 19:31:35 -07:00
Nikolaj Bjorner 3727f70363 fix #6742 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 19:22:31 -07:00
Nikolaj Bjorner 4a9c4ca2ce initialize poly solver in incremental mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 14:12:29 -07:00
Nikolaj Bjorner d1482287d4 fix #6793, disable unbound_compressor when used in context of a moel converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 14:03:40 -07:00
Nikolaj Bjorner 08599177d0 fix #6808 
remove bv_eq_axioms as an external option to toggle.
Diseqalities have to be enforced for extensionality.
There are no internal code paths where the option is set to false.
 2023-07-13 10:47:55 -07:00
Nikolaj Bjorner d0d434e4f1 fix #6807 2023-07-13 10:23:28 -07:00
Nikolaj Bjorner 3e58f0cff1 build fixes 2023-07-13 09:25:20 -07:00
Nikolaj Bjorner b909b87acc build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 09:13:41 -07:00
Nikolaj Bjorner 939bf1c725 wip - alpha support for polymorphism 
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).

The WIP SMTLIB3 format is assumed to be supporting the following declaration

```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).

The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.

This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
 2023-07-12 18:09:02 -07:00
Nikolaj Bjorner d6f2c23627 #6805 2023-07-11 09:41:29 -07:00
Lev Nachmanson 9ae6c88e3f fix the build 2023-07-10 12:19:32 -07:00
Lev Nachmanson 1840fd17da Merge branch 'master' of https://github.com/z3prover/z3 2023-07-10 12:06:06 -07:00
Lev Nachmanson e091a2e775 remove the line with clang-format off 2023-07-10 12:05:59 -07:00
Nikolaj Bjorner 241e845da8 fix #6802 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-09 12:07:43 -07:00
THE Spellchecker dc0887db5a
Typo Fixes (#6803) 2023-07-09 11:56:10 -07:00
Nikolaj Bjorner 28a0c2d18f Merge branch 'master' of https://github.com/z3prover/z3 2023-07-07 17:23:08 -07:00
Nikolaj Bjorner 5806869ae4 fix #6792, add scaffolding for type variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-07 17:22:56 -07:00
Lev Nachmanson 56b5492752 remove dead code 2023-07-07 15:05:17 -07:00
Lev Nachmanson 0fceb80e0f edit tracing, add lar_solver::column_is_feasible() 2023-07-07 11:48:21 -07:00
Clemens Eisenhofer 4cb158a79b
User Propagator: Return if propagated lemma is redundant (#6791) 
* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied
 2023-07-07 09:58:41 -07:00
Jerry James f5c069f899
Fix regular expression strings with escapes (#6797) 2023-07-07 09:57:07 -07:00
Nikolaj Bjorner f645bcf605 add direct detection for integer expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-07 09:54:18 -07:00
Nikolaj Bjorner f450bc4ae0 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-07 09:29:49 -07:00
Nikolaj Bjorner 8c7525c97f revert log addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-07 09:29:38 -07:00
Nikolaj Bjorner 0ab102cbec fix coefficient extraction and passing in Farkas lemmas, thanks to H. F. Bryant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-07 09:28:47 -07:00
Lev Nachmanson ff875c936f add TRACE stmts, more efficient remove from inf_heap 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-07-06 16:45:22 -07:00
Lev Nachmanson 167e0dc66d Merge branch 'master' of https://github.com/z3prover/z3 2023-07-06 15:07:32 -07:00
Lev Nachmanson 4e327babda remove dead code 2023-07-06 15:07:26 -07:00
Nikolaj Bjorner 68663fd97a fix indentation for python file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-06 09:02:58 -07:00
Nikolaj Bjorner 3782eb1be4 fix #6785 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 19:50:07 -07:00
Nikolaj Bjorner f4b87b3763 fix memory smash in euf completion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 13:04:49 -07:00
Nikolaj Bjorner 14f69c6c01 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-05 12:58:23 -07:00
Nikolaj Bjorner 4ad3324d2e fixes to trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 12:58:17 -07:00
Lev Nachmanson 1c907e8d09 add a comment 2023-07-05 09:14:57 -07:00
Lev Nachmanson e360de6d71 improve tracing and a small fix in 
lp_core_solver_base::make_column_feasible
 2023-07-04 13:23:56 -07:00
Lev Nachmanson 8a49cf62f4 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-04 11:38:20 -07:00
Lev Nachmanson 75897b7a2e a small change in trace feas 2023-07-04 11:38:10 -07:00
Nikolaj Bjorner f0d3cbe39d add dependency tracking to proof from trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-04 16:24:09 +02:00
Nikolaj Bjorner abf5aff0b3 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-04 09:13:12 +02:00
Nikolaj Bjorner ae29a54876 categorize theory axioms as inferences in output to capture justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-04 09:12:58 +02:00
Lev Nachmanson 5ed2a82893
set clang format off for lp files (#6795) 
* adding // clang-format off

* set clang-format off at the beginning of  lp files

* set clang-format off

* remove dead code
 2023-07-03 17:35:16 -07:00
Nikolaj Bjorner 47fc0cf75c Merge branch 'master' of https://github.com/z3prover/z3 2023-07-03 19:30:24 +02:00
Nikolaj Bjorner d9e7b8c21f fixes to trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-03 19:26:19 +02:00
Lev Nachmanson 61948fa1ff find minimal deltas in patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-07-01 07:48:07 -07:00
Lev Nachmanson f5d9ffaca1 clean up and add clang-format off 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-06-30 11:57:42 -07:00
Lev Nachmanson 30a2ced9aa
patching merge (#6780) 
* patching merge

* fix the format and some warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* a fix in the delta calculation

* test patching

* try a new version of get_patching_deltas

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove dead code from lp_tst and try optimizing patching

* add comments, replace VERIFY with lp_assert

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* cleanup

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-06-27 17:53:27 -07:00
Nikolaj Bjorner b2c035ea3f missing negation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 18:46:03 -07:00
Clemens Eisenhofer d42693d5b5
Equalities in C# UP-Propagation (#6786) 
* Query Boolean Assignment in the UP

* UP's decide ref arguments => next_split

* Fixed wrapper

* More fixes

* Equalities in C# UP-Propagation

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 10:59:57 -07:00
Nikolaj Bjorner 7221c84156 fix #6783 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-25 21:21:06 -07:00
Nikolaj Bjorner b451735aa0 fix #6778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-25 21:08:13 -07:00