Nikolaj Bjorner
|
9f386306ef
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 10:55:47 -07:00 |
|
Nikolaj Bjorner
|
1a995da0ae
|
fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 10:55:47 -07:00 |
|
Lev Nachmanson
|
907d310600
|
get rid of arith.nla parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 14:33:40 -07:00 |
|
Lev Nachmanson
|
f9151a7a8e
|
correct the default options: smt.arith.nla=False
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 13:55:23 -07:00 |
|
Nikolaj Bjorner
|
4b7bd3a881
|
fix #3536
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 12:59:24 -07:00 |
|
Nikolaj Bjorner
|
f8dcaa8885
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 10:23:00 -07:00 |
|
Lev Nachmanson
|
352f4b5b37
|
use u_set in random_update()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-26 18:11:32 -07:00 |
|
Nikolaj Bjorner
|
12f62e73d5
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:24:34 -07:00 |
|
Nikolaj Bjorner
|
7a04e52c41
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:22:24 -07:00 |
|
Nikolaj Bjorner
|
499843ae7f
|
remove verbose 0 output, #3527
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 14:49:14 -07:00 |
|
Arie Gurfinkel
|
5673ec046b
|
qe_term_graph fix for #3526
|
2020-03-26 16:45:06 -04:00 |
|
Nikolaj Bjorner
|
d4699b181d
|
fix assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 12:49:44 -07:00 |
|
Nikolaj Bjorner
|
73ab95d338
|
remove canonize in seq solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 12:47:30 -07:00 |
|
Nikolaj Bjorner
|
0fa04179d0
|
fix #3522
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 11:06:04 -07:00 |
|
Nikolaj Bjorner
|
5da2169a0e
|
fix #3524
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 10:38:13 -07:00 |
|
Nikolaj Bjorner
|
ee2e81b696
|
fix #3517
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 10:02:41 -07:00 |
|
Nikolaj Bjorner
|
493671aa72
|
fix #3520
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:58:06 -07:00 |
|
Nikolaj Bjorner
|
868a6b3594
|
fix #3521
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
Nikolaj Bjorner
|
37f080b877
|
fix #3523
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
Nikolaj Bjorner
|
c165f69248
|
fix #3525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
Lev Nachmanson
|
fd219abe8c
|
fix test build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b34f841421
|
setting the old defaul options for nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
f5b62015fc
|
change the return type of ival.var() to tv
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
119a491b17
|
tracking stats for max columns in theore_arith_core.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
96cc58f67c
|
instrument the tableau
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
09467ba677
|
restore some class names by replacing u_set to int_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
ab34ef9daf
|
fix crash exposed by #3503
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
ea964e5c3b
|
rename int_set to u_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
bc5b68b16e
|
convert term indices to columns in lar_solver::add_equality()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
e2538afd32
|
better diagnostics in lar_solver and more efficient int_set::resize()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
50db22b2b2
|
fix #3407
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
98dfb1ba86
|
get rid of m_resize_buffer
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
2975873b91
|
ensure encapsulation boundaries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
eac5070a2e
|
remove stdout
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
c16d90307b
|
more careful resize in int_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
0ec12f497c
|
reduce use of m_core as attribute reference, instead pass as parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
6b9e1e936d
|
correcting invariant, fix #3482
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
e0b95979e6
|
detect the status change in lar_solver::add_equality()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
ee8aa50750
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
e16c62d6e2
|
don't reset core after it has been populated for the cut #3451 and presumably other bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
38eca3b66a
|
fixes in order lemmas and printing terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
4b8a063996
|
convert seg fault to assertion violation #3456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b964976b3f
|
remove debug code from theory_lra.cpp and restore gomory.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
8a665e25ed
|
reverting signed mon_eq, try to rely on canonization state during add/pop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
6877840342
|
port from master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
cc74dd6373
|
emonics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
316f2194e0
|
rename
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b52150de22
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
c88d5e6468
|
remove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
2b98c7e157
|
tidy^2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|