Bruce Mitchener
1d9345c3de
Fix typos.
2022-08-05 07:40:50 +03:00
Bruce Mitchener
08165f5367
No need to return a const bool.
2022-08-05 07:40:19 +03:00
Nikolaj Bjorner
9da6895276
add option to select with folding
2022-08-04 16:59:26 +03:00
Nikolaj Bjorner
a8ff976bcc
max maximal unfolding configurable
2022-08-04 16:59:26 +03:00
Nikolaj Bjorner
774ce3d7ab
create special case for osx arm
...
shortcut when store/select are distinct
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-03 07:56:02 +03:00
Jakob Rath
9275d1e57a
sparse_matrix iterators
2022-08-01 18:37:11 +03:00
Bruce Mitchener
77e5d6ab19
Use nullptr consistently instead of 0
or NULL
.
2022-08-01 14:24:32 +03:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. ( #6211 )
2022-07-30 10:07:03 +01:00
Bruce Mitchener
1eb84fe4b9
Mark override methods appropriately. ( #6207 )
2022-07-29 23:29:15 +02:00
Nikolaj Bjorner
8551b217ce
fix #6194
2022-07-27 08:03:57 +02:00
JohnLyu2
3e8daa5965
fix re.range symbolic argument bug in z3str3 ( #6189 )
2022-07-27 04:24:20 +02:00
Nikolaj Bjorner
5c2c0ae900
force-push on new_eq, new_diseq in user propagator, other fixes to Python bindings for user propagator
...
This update allows the python bindings for user-propagator to handle functions that are declared to be registered with the user propagator plugin. It fixes a bug in UserPropagateBase.add to allow registering terms dynamically during search.
It also fixes a bug in theory_user_propagate as scopes were not fully pushed when the solver gets the callbacks for new equalities and new disequalities.
It also adds equality and disequality interfaces to the sat/smt solver version (which isn't being exercised in earnest yet)
2022-07-25 03:42:29 +02:00
Bruce Mitchener
3e38bbb009
Make sure all headers do #pragma once
. ( #6188 )
2022-07-23 10:41:14 -07:00
Nikolaj Bjorner
7f983e7d9e
fix #6174
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 21:22:41 -07:00
Nikolaj Bjorner
1b83a4556b
fix #6178
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 20:48:23 -07:00
Clemens Eisenhofer
95c3dd9224
Added missing decide-callback for tactics ( #6166 )
...
* Added function to select the next variable to split on
* Fixed typo
* Small fixes
* uint -> int
* Fixed missing assignment for binary clauses
* Added missing decide-callback for tactics
2022-07-17 10:07:52 -07:00
Nikolaj Bjorner
b253db2c0a
redundant parenthesis
2022-07-13 16:20:03 -07:00
Nikolaj Bjorner
1378e713ba
fix #6157
2022-07-13 14:37:04 -07:00
Nikolaj Bjorner
8e23af33d7
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-13 14:20:21 -07:00
Nikolaj Bjorner
7d0c789af0
propagate has-length over map/mapi
2022-07-12 20:50:28 -07:00
Nikolaj Bjorner
ca80d99617
fix #6153
2022-07-12 15:49:57 -07:00
Nikolaj Bjorner
43cf053066
fix #6128
2022-07-12 15:43:12 -07:00
Nikolaj Bjorner
49b7e9084f
Merge branch 'master' of https://github.com/z3prover/z3
2022-07-11 09:26:34 -07:00
Clemens Eisenhofer
1f2346073a
Fixed missing assignment for binary clauses ( #6148 )
...
* Added function to select the next variable to split on
* Fixed typo
* Small fixes
* uint -> int
* Fixed missing assignment for binary clauses
2022-07-11 09:24:03 -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
0c42d3b079
small format update
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-06 11:41:48 -07:00
Nikolaj Bjorner
580ed31afd
fix types and incompleteness for feature #6104
2022-07-06 01:08:54 -07:00
Nikolaj Bjorner
d7472f0726
fix #6124
...
expression pointers were changed within a function, but not pinned. So the pointers got stale. To enforce their life-time within the function body (for use in logging) pin the expressions.
2022-07-05 12:48:21 -07:00
Nikolaj Bjorner
de41cfd277
fix #6104
...
add equality reasoning to bit-vector solver to instantiate int2bv(bv2int(x)) = x identity on demand.
2022-07-05 12:23:24 -07:00
Nikolaj Bjorner
71fc83c051
Move out equality use out of the loop
2022-07-04 12:42:39 -07:00
Nikolaj Bjorner
6ed2b444b5
probably won't fix #6127
...
recfun decl plugin does not get copied so recursive functions are lost when cloning.
Fix is risky and use case is limited to threads + recursive definitions
2022-07-03 18:10:52 -07:00
Nikolaj Bjorner
1e8f9078e3
fix unsoundness in explanation handling for nested datatypes and sequences
2022-07-03 17:00:39 -07:00
Nikolaj Bjorner
1a9122663c
remove unsound axioms, fix #6115
2022-06-29 11:16:10 -07:00
Nikolaj Bjorner
ff265235c1
adjust trace output
2022-06-29 08:20:01 -07:00
Nikolaj Bjorner
fd8ee34564
add logging
2022-06-29 08:20:01 -07:00
Nikolaj Bjorner
30165ed40a
fix #6105
...
non-linear division axioms appear incomplete.
Fixed for legacy arithmetic. Fix pending for new arithmetic solver.
2022-06-26 20:37:18 -07:00
Nikolaj Bjorner
56aa4261b6
fix #6082
2022-06-23 07:43:06 -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
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
99b606b861
add logging
2022-06-16 15:40:00 -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
04f94d818f
fix #6091
2022-06-14 09:51:06 -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
6a1193eebd
reorg if-then-else structure
2022-06-08 10:00:45 -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
a9d70fca1a
fix #6061
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-31 19:09:10 -07:00
Nikolaj Bjorner
ca2497eecb
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-15 12:00:41 -07:00