Lev Nachmanson
|
1f23ae8aae
|
fix the test build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-16 12:58:39 -07:00 |
|
Lev Nachmanson
|
95cb828324
|
make lar_solver pretty printer const on the solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-16 12:58:39 -07:00 |
|
Lev Nachmanson
|
5208b64a6b
|
expose only necessary methods of lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-16 12:58:39 -07:00 |
|
Lev Nachmanson
|
6d8e5400fd
|
return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-16 12:58:39 -07:00 |
|
Nikolaj Bjorner
|
cb4ceeab3a
|
fix #3985
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-16 12:04:46 -07:00 |
|
Nikolaj Bjorner
|
206c3e2c38
|
fix #3979
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-16 10:54:19 -07:00 |
|
Nikolaj Bjorner
|
dde0c514fa
|
warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 17:14:25 -07:00 |
|
Nikolaj Bjorner
|
f67077b7ff
|
warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 17:13:02 -07:00 |
|
Nikolaj Bjorner
|
d465938496
|
add lower bounds on lengths if they are not present
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 15:54:40 -07:00 |
|
Nikolaj Bjorner
|
e6174c89f3
|
bail out of mb branching if lengths are not available
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 15:44:17 -07:00 |
|
Nikolaj Bjorner
|
40b4ca7f86
|
fix #3950
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 15:07:53 -07:00 |
|
Nikolaj Bjorner
|
357ec2fd01
|
fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 13:29:45 -07:00 |
|
Nikolaj Bjorner
|
2e1e9c9082
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 12:25:07 -07:00 |
|
Nikolaj Bjorner
|
3845e0859c
|
fix #3878
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 12:23:18 -07:00 |
|
Nikolaj Bjorner
|
d0f94055e7
|
fix #3966
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 11:05:02 -07:00 |
|
Nikolaj Bjorner
|
068f65c8ac
|
fix #3967 regression from using rewriter mode that splits strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 10:36:33 -07:00 |
|
Nikolaj Bjorner
|
79a2b52de0
|
fix #3971
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 10:29:41 -07:00 |
|
Nikolaj Bjorner
|
1ec977930a
|
fix #3972 regression from changing the way assumptions are initialized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 10:10:07 -07:00 |
|
Nikolaj Bjorner
|
25252af1fc
|
fix #3975
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 08:06:43 -07:00 |
|
Nikolaj Bjorner
|
cce27ff65f
|
fix #3976
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 07:53:46 -07:00 |
|
Nikolaj Bjorner
|
164a73febb
|
fixing #3933 - remove unclear code normalizing itos
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 19:23:23 -07:00 |
|
Nikolaj Bjorner
|
b04c97458d
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 17:34:14 -07:00 |
|
Nikolaj Bjorner
|
835b57b775
|
fix #3961 fix #3940
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 17:33:44 -07:00 |
|
Nikolaj Bjorner
|
7ed9996fc0
|
fix #3962
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 11:05:05 -07:00 |
|
Nikolaj Bjorner
|
5f81913292
|
fix #3951
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 10:51:16 -07:00 |
|
Nikolaj Bjorner
|
5e0c34cae2
|
fix #3953
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 09:43:03 -07:00 |
|
Nikolaj Bjorner
|
2a0537af69
|
fix #3954
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 08:17:57 -07:00 |
|
Nikolaj Bjorner
|
b8c069c6b7
|
fix #3955
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 08:13:17 -07:00 |
|
Nikolaj Bjorner
|
f564c325d3
|
fix #3957
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:46:10 -07:00 |
|
Nikolaj Bjorner
|
d7d6877031
|
fix #3958
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:34:03 -07:00 |
|
Nikolaj Bjorner
|
387964f508
|
fix #3960 fix #3959
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:30:54 -07:00 |
|
Nikolaj Bjorner
|
0f697830fc
|
spelling
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 19:08:05 -07:00 |
|
Nikolaj Bjorner
|
fe7146d93b
|
fix #3913 - change assumption tracking to be granular based on disabled guards
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 19:06:12 -07:00 |
|
Nikolaj Bjorner
|
e1027790ae
|
more to #3926
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 16:04:54 -07:00 |
|
Lev Nachmanson
|
7caae3f5d2
|
small improvements in tableau in rows and bound propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-13 16:04:25 -07:00 |
|
Lev Nachmanson
|
90793931b1
|
small changes in one_iteration_tableau_rows
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-13 16:04:25 -07:00 |
|
Nikolaj Bjorner
|
9223f611ba
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:49:27 -07:00 |
|
Nikolaj Bjorner
|
9f42338de8
|
fix #3926
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:43:27 -07:00 |
|
Nikolaj Bjorner
|
299a6f4aee
|
fix #3939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:00:21 -07:00 |
|
Nikolaj Bjorner
|
d3db2af81d
|
fix #3941
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 13:15:15 -07:00 |
|
Nikolaj Bjorner
|
b4e7730034
|
fix #3938
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 13:05:53 -07:00 |
|
Nikolaj Bjorner
|
6a5695463f
|
fix #3943
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 12:58:18 -07:00 |
|
Nikolaj Bjorner
|
5dafd1fe25
|
fix #3945
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 10:46:47 -07:00 |
|
Nikolaj Bjorner
|
5c4f775b1b
|
fix #3935
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 10:00:42 -07:00 |
|
Nikolaj Bjorner
|
01c12c951c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 18:01:54 -07:00 |
|
Nikolaj Bjorner
|
84a4d9850b
|
fix #3936
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 18:01:20 -07:00 |
|
Nikolaj Bjorner
|
75a460cc15
|
fix #3932
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 17:49:50 -07:00 |
|
Nikolaj Bjorner
|
9b609af8fc
|
fix #3924
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 16:19:54 -07:00 |
|
Nikolaj Bjorner
|
51eaf84eed
|
fix #3931
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 15:37:18 -07:00 |
|
Nikolaj Bjorner
|
c85113acdb
|
fix #3928
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 15:25:08 -07:00 |
|