mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
20009 commits 23 branches 48 tags 157 MiB
Commit graph

20009 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
85d80a0ae1 track origin slice for concat nodes 2023-07-19 12:06:02 +02:00
Jakob Rath
af73f26941 slicing: track disequalities 2023-07-19 12:04:45 +02:00
Jakob Rath
970e68c70e slicing: use proper bv sorts for expressions 2023-07-19 08:58:34 +02:00
Nikolaj Bjorner
e8a38c5482 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 19:14:45 -07:00
Nikolaj Bjorner
3d8f75b3d8 enable on-clause with dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 16:59:02 -07:00
Jakob Rath
66f813154b basic slicing integration 2023-07-18 16:19:54 +02:00
Jakob Rath
28ed3bd7ab fix backtracking of m_needs_congruence 2023-07-18 16:00:26 +02:00
Jakob Rath
a96df2292e fix build 2023-07-18 15:13:53 +02:00
Jakob Rath
68b151b0d2 move some todos 2023-07-18 15:11:46 +02:00
Jakob Rath
4742985906 add proposed query interface 2023-07-18 15:07:53 +02:00
Jakob Rath
bac52313da move function impl 2023-07-18 14:53:20 +02:00
Jakob Rath
c124cbae97 Add virtual concat terms on demand during propagation 2023-07-18 14:48:32 +02:00
Jakob Rath
4049716946 explain conflict 2023-07-18 11:26:18 +02:00
Jakob Rath
5e5164ed2c add_value 2023-07-18 11:24:12 +02:00
Jakob Rath
0d80e47350 update deps handling (need to support pvars as well) 2023-07-18 11:22:02 +02:00
Nikolaj Bjorner
9db636c38b Merge branch 'master' of https://github.com/z3prover/z3 2023-07-17 11:00:11 -07:00
Nikolaj Bjorner
3e74989a9d fixup dependencies for trim' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-17 11:00:02 -07:00
Lev Nachmanson
bfc37bd266 add to m_touched_rows only when bound 
propagation is required
 2023-07-17 08:00:01 -10:00
Jakob Rath
11d9e5c862 minor 2023-07-17 19:04:17 +02:00
Jakob Rath
d1cb02b735 use abstract sort also for value slices 2023-07-17 18:31:17 +02:00
Jakob Rath
a2fdb03625 propagate value when splitting a slice 2023-07-17 18:18:12 +02:00
Jakob Rath
490b77d8a1 mk_value_slice 2023-07-17 14:41:45 +02:00
Jakob Rath
30323a6ba1 update unit test 2023-07-17 14:41:45 +02:00
Jakob Rath
741e37c2d7 find is now get_root 2023-07-17 14:41:45 +02:00
Jakob Rath
b8d118a558 use enode* instead of custom slice index; extract explanations from egraph 2023-07-17 14:41:45 +02:00
Jakob Rath
82b1f9297b utils 2023-07-17 14:41:45 +02:00
Nuno Lopes
013d5dc4db remove garbage file 2023-07-17 08:45:18 +01:00
Lev Nachmanson
0a91465e13 comment out debug output 2023-07-16 18:40:53 -10:00
Nikolaj Bjorner
75a9038aa2 add missing dependencies in rup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-16 16:54:26 -07:00
Lev Nachmanson
fd5902f76e relax an assertion in int_solver::patcher 2023-07-16 11:55:42 -10:00
Nikolaj Bjorner
305c1c1dc2 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:52:33 -07:00
Nikolaj Bjorner
715081cbd1 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-15 17:04:54 -07:00
Nikolaj Bjorner
30e8330907 fix #6813 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:03:44 -07:00
Nikolaj Bjorner
8a913981f6 fix #6813 - proofs terms are fragile with respect to simplificiation of not(not(e)). It would be better if proof terms didn't have to track this level of detail, but the legacy proof format assumes strictly checkable proofs. A patch is to fixup terms within the mk_transitivity constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:03:04 -07:00
Lev Nachmanson
144c9a7b82 restore the change_rows population in lar_solver 2023-07-15 10:09:48 -07:00
Lev Nachmanson
401ec04ec3
code cleaning around m_touched_rows of lar_solver (#6814) 2023-07-14 20:19:13 -07:00
Nikolaj Bjorner
3849f665d6 #6523 2023-07-14 10:17:19 -07:00
Nikolaj Bjorner
a8da0a6851 #6696 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 21:48:46 -07:00
Nikolaj Bjorner
dda9242616 revert lt change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 21:39:04 -07:00
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
Jakob Rath
8c17e231ad don't 'find' when creating subslice 2023-07-12 16:45:51 +02:00
Jakob Rath
0fb81fc437 use z3's egraph (wip) 2023-07-12 16:21:38 +02:00