Lev Nachmanson
|
d39d64176e
|
introduce a bug into theory_array - looking for a counterexample
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
84933c4435
|
relax the literal check in theory_lra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
3224febd0e
|
remove double shrink
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
c68d15f441
|
build of template
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
1aaf6d879f
|
use same interval manager in pdd_interval as caller
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
f76432933f
|
avoid calling del on memory not owned by object allocator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
abc4c5962b
|
fix #3269
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
f1f974638d
|
track variables used by nla_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
a7158772ad
|
move to scoped intervals for memory management
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
79fefe5fb3
|
local
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
906d52ca1c
|
accept term indices as columns in some lar_solver queries
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
f43f1629cf
|
fix #3273
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
f28c80e3b1
|
reorder fields in lar_solver constructor to avoid a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
b67d136849
|
hide flag on registering variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
3e84d04719
|
fix internalize for multiplication #3119
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
846a9fc25f
|
consistent
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
26631ce38d
|
add a unit test for monics, plus some cosmetic changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
0207878f5f
|
fix #3183 - change relevancy propagation to ensure that div/mod axioms are picked up
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
1e9013fe6d
|
cleanup in var_register
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
719603f185
|
register inner terms with null var
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
a0251ac745
|
do not register equality terms created in lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
285ff9540d
|
make sure that the term external index has not been used
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
f00c026272
|
fix #3173
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Nikolaj Bjorner
|
0f779c9c0d
|
fix #3185 - move handling of to_real within def conversion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
f636a481d3
|
fixes in bound setting in cube, and in lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
a80eb13420
|
fixes in bound setting in cube, and in lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
9cce01e632
|
fix in order lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
6ea0bcb454
|
round the bound for columns and terms when it can be deduced that they are integral
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
b403b96d38
|
remove an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
77ca63db90
|
fix in gomory: revert some changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
cbefa8d2b0
|
fix in gomory cut
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
fad08454c1
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
2b4de6ebbc
|
add option branch_flip to lp_settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
59a82a4482
|
introduce a bug int theory_array.cpp - look for a counter example
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
bf885bf9b3
|
introduce a bug into theory_array - looking for a counterexample
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
28c057fd7b
|
relax the literal check in theory_lra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
2ad94026a0
|
do not produce proportional lemma for non-integral vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
0ee541204f
|
fix in gomory: revert some changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
b8d7af59f4
|
fix in gomory cut
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
6396857ee2
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
87f80ce022
|
add option branch_flip to lp_settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
8e55a77ee7
|
introduce a bug int theory_array.cpp - look for a counter example
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
406bd98a39
|
introduce a bug into theory_array - looking for a counterexample
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
3e4720abbd
|
relax the literal check in theory_lra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
0229ab2811
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
66dd93a035
|
fix a bug in nla_intervals - add explanations when getting intervals from a term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
ab92c20106
|
add option branch_flip to lp_settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
b9bfa950f6
|
introduce a bug int theory_array.cpp - look for a counter example
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
37c72b71f5
|
introduce a bug into theory_array - looking for a counterexample
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
|
Lev Nachmanson
|
c0b49e95c4
|
use lar_solver directly to compare variable values in assume_eqs()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|