Nikolaj Bjorner
|
deaad86d6a
|
nit
|
2022-03-01 12:11:10 -08:00 |
|
Clemens Eisenhofer
|
412b05076c
|
User-functions fix (#5868)
|
2022-02-26 09:21:01 -08:00 |
|
Nikolaj Bjorner
|
7b4f1ed530
|
missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-23 04:49:42 -08:00 |
|
Nikolaj Bjorner
|
6af170b058
|
fix #5861
sigh
|
2022-02-22 11:26:09 -08:00 |
|
Nikolaj Bjorner
|
b843618051
|
fix #5798
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-20 13:54:15 -08:00 |
|
Nikolaj Bjorner
|
1e463955c2
|
#4889 avoid double internalize of bvle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-20 09:09:28 -08:00 |
|
Nikolaj Bjorner
|
2e00f2f32d
|
Propagator (#5845)
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* references #5818
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix c++ build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update propagator example (I) (#5835)
* fix #5829
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Adapted the example to the changes in the propagator
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* context goes out of scope in stack allocation, so can't used scoped context when passing objects around
* parameter check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Fixed bug in user-propagator "created" (#5843)
Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
|
2022-02-17 09:21:41 +02:00 |
|
Qix
|
9cf50766a6
|
fix compiler warnings under clang (#5839)
|
2022-02-16 23:36:34 +02:00 |
|
Nikolaj Bjorner
|
6202cd5394
|
fix #5842
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-16 17:38:19 +02:00 |
|
Nikolaj Bjorner
|
aa6ec418e3
|
move idiv test to after cuts/branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-14 19:50:49 +02:00 |
|
Nikolaj Bjorner
|
3d26b501e7
|
fix #5827 #5828
|
2022-02-14 10:31:04 +02:00 |
|
Nikolaj Bjorner
|
0059e88036
|
fix #5808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-07 20:10:32 +02:00 |
|
Nikolaj Bjorner
|
9958cab5cc
|
fix #5808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-07 07:43:30 +02:00 |
|
Nikolaj Bjorner
|
3f3d058567
|
extract also units from search state
|
2022-02-07 06:16:22 +02:00 |
|
Nikolaj Bjorner
|
9d655cc658
|
track all unhandled operators instead of latest
|
2022-02-04 22:07:29 -08:00 |
|
Nikolaj Bjorner
|
474949542e
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2022-02-04 13:08:59 -08:00 |
|
Nikolaj Bjorner
|
05e28e4344
|
fix #5812
|
2022-02-04 13:08:52 -08:00 |
|
Nikolaj Bjorner
|
a326ad4cd9
|
flag incomplete on lambdas #5803
|
2022-01-31 11:54:06 -08:00 |
|
Nikolaj Bjorner
|
c6539deb61
|
fixing null check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 17:25:42 +01:00 |
|
Nikolaj Bjorner
|
435f79eab0
|
tup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 16:40:55 +01:00 |
|
Nikolaj Bjorner
|
9294b2ceb2
|
created
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 16:33:23 +01:00 |
|
Nikolaj Bjorner
|
3de9d37772
|
fix overrides for created_eh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 16:24:08 +01:00 |
|
Nikolaj Bjorner
|
bf6454dccc
|
throw error if created-eh has not been registered
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 13:01:57 +01:00 |
|
Nikolaj Bjorner
|
ea6827505e
|
add missing callback to m_created_eh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-25 10:13:09 +01:00 |
|
Nikolaj Bjorner
|
a1f7676c81
|
remove assertion - literals could be assigned but propagation incomplete
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-21 03:10:41 +01:00 |
|
Nikolaj Bjorner
|
17280846f8
|
added comments to explain #5781
|
2022-01-21 01:40:31 +01:00 |
|
Nikolaj Bjorner
|
af9ae35984
|
term
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-20 14:43:16 +01:00 |
|
Nikolaj Bjorner
|
c527fda0b6
|
term
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-20 14:41:27 +01:00 |
|
Nikolaj Bjorner
|
f1a302bba7
|
term
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-20 14:38:34 +01:00 |
|
Nikolaj Bjorner
|
7a8c969033
|
ensure b_internalized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-20 13:27:23 +01:00 |
|
Nikolaj Bjorner
|
c00591daaf
|
finish is-fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-19 16:28:34 +01:00 |
|
Nikolaj Bjorner
|
e5767bf2b8
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-19 15:19:07 +01:00 |
|
Nikolaj Bjorner
|
0f03ef4ab0
|
for Clemens: ensure fixed values are propagated after registration
Also allow to register expressions that the rewriter changes to ensure they get picked up.
|
2022-01-19 14:38:11 +01:00 |
|
Nikolaj Bjorner
|
d09abdf58e
|
fix #5771
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
|
2022-01-14 15:46:40 -08:00 |
|
Nikolaj Bjorner
|
56d3718cde
|
add simplification with qe-lite as an option #5767
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-12 03:41:21 -08:00 |
|
Nikolaj Bjorner
|
dbd5512d8c
|
ensure enode without recursion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-11 08:35:57 -08:00 |
|
Nikolaj Bjorner
|
055732423c
|
ensure enode without recursion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-11 08:35:25 -08:00 |
|
Nikolaj Bjorner
|
0bc8518cb5
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-07 11:53:27 -08:00 |
|
Nikolaj Bjorner
|
199daead50
|
remove Z3_bool_opt #5757
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-01-07 11:52:10 -08:00 |
|
Nikolaj Bjorner
|
592b1d7f65
|
#5752
|
2022-01-06 13:32:50 -08:00 |
|
Nikolaj Bjorner
|
d7c7fbb8f1
|
setting roots breaks relevancy propagation
|
2022-01-05 21:16:25 -08:00 |
|
Nikolaj Bjorner
|
9d3c8a6a2f
|
na
|
2022-01-01 17:59:31 -08:00 |
|
Nikolaj Bjorner
|
fc77345bec
|
breaking change. Enforce append semantics everywhere for parameter updates #5744
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
|
2021-12-30 19:11:14 -08:00 |
|
Nikolaj Bjorner
|
d88f125818
|
build
|
2021-12-26 15:24:03 -08:00 |
|
Nikolaj Bjorner
|
09ee60ccce
|
update comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-12-21 11:04:07 -08:00 |
|
Nikolaj Bjorner
|
4b813bac1c
|
na
|
2021-12-19 12:31:47 -08:00 |
|
Nikolaj Bjorner
|
f0740bdf60
|
move user propagte declare to context level
declaration of user propagate functions are declared at context level instead of at solver scope.
|
2021-12-18 10:56:42 -08:00 |
|
Nikolaj Bjorner
|
4856581b68
|
na
|
2021-12-17 16:40:19 -08:00 |
|
Nikolaj Bjorner
|
8ca023d541
|
expose propagate created
|
2021-12-17 16:12:47 -08:00 |
|
Nikolaj Bjorner
|
9c8800bdde
|
adding a new toy for Clemens
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-12-17 10:45:59 -08:00 |
|