Jakob Rath
a339cd1aff
fix
2023-06-28 13:20:57 +02:00
Jakob Rath
54487f3294
slicing::explain_equal
2023-06-28 11:15:16 +02:00
Jakob Rath
7d7735b010
test
2023-06-28 10:41:22 +02:00
Jakob Rath
05ea32f17d
update test
2023-06-28 10:37:07 +02:00
Jakob Rath
b54beca037
clarify
2023-06-28 10:26:39 +02:00
Jakob Rath
92192144b1
slicing: is_equal
2023-06-28 10:24:48 +02:00
Jakob Rath
9e7a392e21
slicing: explain
2023-06-28 10:23:55 +02:00
Jakob Rath
3a7cdc36d6
slicing: mark
2023-06-28 10:23:35 +02:00
Jakob Rath
947335e147
slicing: prepare for explain()
2023-06-28 09:59:21 +02:00
Jakob Rath
0c62b81a56
Rename confusing methods
...
avoid difference between c.is_eq() and c->is_eq()
2023-06-23 11:59:18 +02:00
Jakob Rath
8a50467ba8
Fix mk_slice, add mk_extract/mk_concat
2023-06-16 11:48:01 +02:00
Jakob Rath
982170e6e0
slice2var
2023-06-15 17:12:19 +02:00
Jakob Rath
862707baa0
test2
2023-06-15 17:09:46 +02:00
Jakob Rath
cddfcc1658
get rid of _idx suffix
2023-06-15 16:58:39 +02:00
Jakob Rath
2a3006cce3
Don't track arbitrary hi/lo reference points and just store the slice width
2023-06-15 16:55:26 +02:00
Jakob Rath
8ce85da881
test and bugfix
2023-06-15 16:02:25 +02:00
Jakob Rath
40f794c5b4
test stub
2023-06-15 11:53:06 +02:00
Jakob Rath
136e819cb9
set up test for slicing
2023-06-15 11:43:14 +02:00
Jakob Rath
71ef78fb25
slicing
2023-06-15 10:43:47 +02:00
Jakob Rath
b316534df8
remove unused type parameter
2023-06-12 21:18:30 +02:00
Jakob Rath
a0df8507d9
extract/concat slicing wip
2023-06-12 21:13:20 +02:00
Jakob Rath
8bde66420a
Merge branch 'master' into polysat
2023-06-12 14:02:20 +02:00
Nikolaj Bjorner
ac00306355
fix context simplification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-09 11:30:56 -07:00
Nikolaj Bjorner
d0085b41c1
disable breaking change
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-09 11:15:54 -07:00
Nikolaj Bjorner
555ccc8aab
simplify bounds by subsumption checks
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-09 10:21:45 -07:00
Lev Nachmanson
1006955215
get cached tv value ( #6756 )
2023-06-08 19:46:38 -07:00
Lev Nachmanson
f7ec5c5c64
fix sort_non_basis ( #6755 )
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-06-08 13:08:09 -07:00
Nikolaj Bjorner
1d62964c58
avoid name clash for multiple special relations #6743
2023-06-07 17:55:11 -07:00
Nikolaj Bjorner
ab4b7c50ed
fix #6749
2023-06-07 16:09:50 -07:00
Nikolaj Bjorner
06a8987314
fix #6748
...
destructive equality resolution uses an occurs check function that is only safe for quantifier-free formulas. In the special case where a bound variable is Boolean and occurs on a side of an equality the other side cannot have a quantifier.
2023-06-07 15:59:39 -07:00
Jakob Rath
57e92b2a59
Fix bvnego ( #6750 )
2023-06-07 11:24:40 -07:00
Nikolaj Bjorner
73c3f34d66
remove debug output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-06 16:37:24 -07:00
Nikolaj Bjorner
2bff0a6b8a
regression on quantifier weight computation when weights are 0 vs non-0. It modifies a change made for the fix of #2667 . That fix caused a regression in F*. Reported @mtzguido
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-06 16:35:37 -07:00
Nikolaj Bjorner
68f43ac7a4
make der selective to configuration. For F*, quantifiers are hand or machine generated in specific formats and the tool depends on e-matching to use precisely the format of the quantifiers that have been entered. For other cases of quantifiers, destructive equality resolution (der) can be expected to offer simplifications
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-06-06 16:15:04 -07:00
Nikolaj Bjorner
81068981aa
fix #6746 , fix type errors in java bindings
2023-06-03 09:41:29 +02:00
Clemens Eisenhofer
82667bd86b
Fix UP's decide callback ( #6707 )
...
* Query Boolean Assignment in the UP
* UP's decide ref arguments => next_split
* Fixed wrapper
* More fixes
2023-06-02 09:52:54 +02:00
Nikolaj Bjorner
d59bf55539
fix formatting bug reported by Alex Nutz
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-30 22:19:42 +02:00
Nikolaj Bjorner
621f1f8a85
sanity check parameters #6737
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-30 09:44:06 +02:00
Jakob Rath
52c4716636
m_var2pdd entries may need to change pdd manager
2023-05-29 15:53:04 +02:00
Jakob Rath
129039dc52
Add method to (explicitly) re-assign the pdd manager
2023-05-29 15:53:04 +02:00
Jakob Rath
2795ac5e90
Store pdd_manager as pointer
2023-05-29 15:53:04 +02:00
Manuel Carrasco
230306ddfc
Add solver::interrupt to Python's API. ( #6739 )
2023-05-28 21:04:36 +02:00
Jakob Rath
f54f33551e
Merge branch 'master' into polysat
2023-05-26 15:58:09 +02:00
Nikolaj Bjorner
5e1869d8eb
fix #6734
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-26 09:48:58 +01:00
ditto
11264c38d8
Java user propagator interface ( #6733 )
...
* Java API: user propagator interface
* Java API: improved user propagator interface
* Java API: Add UserPropagatorBase.java
* Remove redundant header file
* Initialize `JavaInfo` object and error handling
* Native.UserPropagatorBase implements AutoCloseable
* Add Override annotation
2023-05-24 18:27:28 +01:00
Nikolaj Bjorner
2c21072c99
remove stub class, it may as well go into NativeStatic.txt as C++
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 18:23:10 +01:00
Nikolaj Bjorner
b93529997e
more stubs #6097
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 16:25:54 +01:00
Nikolaj Bjorner
7963ecaf63
stubs for #6097
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 16:21:34 +01:00
Nikolaj Bjorner
a68f91f0a6
fix #6729
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 14:07:12 +01:00
Nikolaj Bjorner
06ea765b82
fix #6721
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-13 09:46:49 -07:00
