Nikolaj Bjorner
df8ccce08e
#6822 string matching against version number of glibc to ensure inclusino
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-07-21 11:03:20 -07:00
Nikolaj Bjorner
4d31ff7a38
remove unused variable
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-07-21 08:35:09 -07:00
Nikolaj Bjorner
3479cdc10b
separate hint literals
2023-07-20 10:52:58 -07: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
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
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
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