Nikolaj Bjorner
|
c2e5cd78c8
|
change lar_terms to use column indices
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-06 12:13:59 -07:00 |
|
Nuno Lopes
|
3313590b95
|
fix #3713: too much caching in dom-simplify for OR expressions
|
2020-04-06 12:11:26 +01:00 |
|
Nuno Lopes
|
346d852bbd
|
fix build
|
2020-04-06 11:19:04 +01:00 |
|
Nikolaj Bjorner
|
9e7af79094
|
initialization order
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 18:16:40 -07:00 |
|
Nikolaj Bjorner
|
b9c9687caf
|
bool_vector
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 18:14:56 -07:00 |
|
Nikolaj Bjorner
|
da6297f31f
|
bool_vector
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 17:41:19 -07:00 |
|
Nikolaj Bjorner
|
dff5071598
|
compile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 17:03:26 -07:00 |
|
Nikolaj Bjorner
|
daa904c9d2
|
fix #3778
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 15:13:36 -07:00 |
|
Nikolaj Bjorner
|
b79b8c9bc4
|
fix #3777
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 15:08:28 -07:00 |
|
Nikolaj Bjorner
|
406c0792f1
|
fix #3775
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 14:04:00 -07:00 |
|
Nikolaj Bjorner
|
bb1119a6ca
|
fix #3774
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 13:59:28 -07:00 |
|
Nikolaj Bjorner
|
550852bc62
|
fix #3765
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 13:49:26 -07:00 |
|
Nikolaj Bjorner
|
e246f6649e
|
tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 13:31:48 -07:00 |
|
Nikolaj Bjorner
|
b889b110ee
|
bool_vector, some spacer tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 12:59:04 -07:00 |
|
Nikolaj Bjorner
|
2ed26e8e73
|
fix #3762
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 12:10:02 -07:00 |
|
Nikolaj Bjorner
|
efc02282f4
|
fix #3758
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 12:01:17 -07:00 |
|
Nikolaj Bjorner
|
1949a978ce
|
fix #3760
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 11:39:25 -07:00 |
|
Nikolaj Bjorner
|
077f2248ca
|
fix #3756
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 11:32:53 -07:00 |
|
Nikolaj Bjorner
|
54d981e88f
|
fix #3757
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 11:25:29 -07:00 |
|
Nikolaj Bjorner
|
39ffc4ece7
|
fix #3759
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 11:19:23 -07:00 |
|
Nikolaj Bjorner
|
080dbb13b0
|
tv alignment, code review comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 03:35:19 -07:00 |
|
Nikolaj Bjorner
|
fddbac0f52
|
use tv for interfacing on get_term
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 02:42:00 -07:00 |
|
Nikolaj Bjorner
|
296a97d0d3
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 01:03:38 -07:00 |
|
Nikolaj Bjorner
|
399cf75ad4
|
fpa warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 00:55:13 -07:00 |
|
Nikolaj Bjorner
|
9e374d6514
|
remove trace for #3725
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 00:53:16 -07:00 |
|
Nikolaj Bjorner
|
4842c71019
|
fix #3537
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 00:38:14 -07:00 |
|
Nikolaj Bjorner
|
eacde16b3e
|
fix #3199
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:55:44 -07:00 |
|
Nikolaj Bjorner
|
8118292def
|
fix #3754
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:20:44 -07:00 |
|
Nikolaj Bjorner
|
7477e96e59
|
fix #3519
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:18:15 -07:00 |
|
Nikolaj Bjorner
|
5516e420a1
|
disable bapa from smt interface
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:09:28 -07:00 |
|
Nikolaj Bjorner
|
e419565239
|
fix #3751
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:01:30 -07:00 |
|
Nikolaj Bjorner
|
7ae9734db2
|
fix #3752
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 22:56:41 -07:00 |
|
Nikolaj Bjorner
|
2f80acb1bc
|
fix #3543
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 21:56:46 -07:00 |
|
Nikolaj Bjorner
|
0fc8ebc8cc
|
fix #3683
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:56:10 -07:00 |
|
Nikolaj Bjorner
|
7e8753cd3f
|
fix #3726
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:48:09 -07:00 |
|
Nikolaj Bjorner
|
10768bd005
|
fix #3727
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:41:13 -07:00 |
|
Nikolaj Bjorner
|
6ac19ed8d0
|
fix #3728 - fail only model validation if the expression is false, there are too many false positives being reported
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:34:32 -07:00 |
|
Nikolaj Bjorner
|
82d7ca46ba
|
fix #3729
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:06:23 -07:00 |
|
Nikolaj Bjorner
|
fadc3761bd
|
fix #3731 - abuse of parameter combinations, trying to use qsat on arrays, but disabling array equality expansion during model evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 17:06:43 -07:00 |
|
Nikolaj Bjorner
|
8faf35e2e0
|
fix #3735
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 16:47:00 -07:00 |
|
Nikolaj Bjorner
|
9fbe178de4
|
fix #3735
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 16:36:54 -07:00 |
|
Nikolaj Bjorner
|
7838e99f47
|
fix #3749
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 14:45:29 -07:00 |
|
Nikolaj Bjorner
|
8d59355b88
|
fix #3750
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 14:37:51 -07:00 |
|
Nikolaj Bjorner
|
0735491557
|
path fix #3747, this patches incoherent behavior of terms / ival from lar_solver. The variables occurring in terms are mapped to columns and not as original variables/terms. theory_lra has to interact with the column_corresponds_to_term test instead of relying on the terms themselves carrying the relevant information
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 14:27:56 -07:00 |
|
Nikolaj Bjorner
|
121a6de32c
|
fix #3748
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 13:22:30 -07:00 |
|
Nikolaj Bjorner
|
031b3a55ef
|
fix #3733 persist uninterpreted atoms across calls to incremental sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 13:11:39 -07:00 |
|
Nikolaj Bjorner
|
c70e9af09d
|
fix #3734
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 12:53:24 -07:00 |
|
Nikolaj Bjorner
|
64d157d81e
|
fix #3739 - dependencies may be valid even if they are null
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 11:58:39 -07:00 |
|
Nikolaj Bjorner
|
c26d3f5437
|
fix #3740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 11:31:29 -07:00 |
|
Nikolaj Bjorner
|
df1c6c8a21
|
fix #3742
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 11:27:37 -07:00 |
|