Clemens Eisenhofer
e11496bc65
Added decide-callback to user-propagator ( #5978 )
...
* Fixed registering expressions in push/pop
* Reused existing function
* Reverted reusing can_propagate
* Added decide-callback to user-propagator
* Refactoring
* Fixed index
2022-04-15 20:07:17 +02:00
Nikolaj Bjorner
3cc9d7f443
improve pre-processing
2022-04-15 12:55:26 +02:00
Clemens Eisenhofer
b264e6c290
Reverted reusing can_propagate ( #5966 )
...
* Fixed registering expressions in push/pop
* Reused existing function
* Reverted reusing can_propagate
2022-04-12 12:29:53 +02:00
Clemens Eisenhofer
b0d8b27f37
Fixed registering expressions in push/pop ( #5964 )
...
* Fixed registering expressions in push/pop
* Reused existing function
2022-04-11 16:50:13 +02:00
Nikolaj Bjorner
0fa0feb979
allow add_expr during pop
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-06 16:27:10 +02:00
Nikolaj Bjorner
03a2d9a018
fix #5942
2022-04-03 11:03:28 -07:00
Nikolaj Bjorner
81084b8232
#5778 #5937
2022-04-01 13:07:17 -07:00
Nikolaj Bjorner
dd27f7e937
#5935
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-30 17:47:48 -10:00
Clemens Eisenhofer
7bb969ab52
Fixed problem with registering bitvector functions ( #5923 )
2022-03-26 16:36:15 -10:00
Nikolaj Bjorner
d790523c59
#5917
...
Add model.user_functions (default true) to control whether user functions are added to the model.
2022-03-23 09:49:44 -07:00
Nikolaj Bjorner
b4873d226c
fix #5907
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:40:19 -07:00
Nikolaj Bjorner
dfa65443e9
fix name for artifact
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 13:51:58 -07:00
Nikolaj Bjorner
964e513353
re-add bv_eq_axioms, fix #5842
2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
545341e699
fix #5895
2022-03-12 09:17:13 -08:00
Nikolaj Bjorner
580012e19f
fix #5894
...
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
2022-03-10 09:45:09 -08:00
Nuno Lopes
43f7636826
remove some copies/moves
2022-03-09 12:46:41 +00:00
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
