Nikolaj Bjorner
|
16478b415b
|
disable order and tangent lemmas on reals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 13:46:25 -07:00 |
|
Nikolaj Bjorner
|
179c9c2da2
|
consolidate methods that add lemma specific information to under "new_lemma"
|
2020-05-10 18:31:57 -07:00 |
|
Nikolaj Bjorner
|
e74faf42ad
|
code review
|
2020-05-10 12:58:05 -07:00 |
|
Nikolaj Bjorner
|
d774ba9da1
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 09:57:24 -07:00 |
|
Nikolaj Bjorner
|
30de76b529
|
add occurs check to other nla_basic lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 20:50:27 -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
|
a0bdb8135d
|
rename monomial to monic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
33cbd29ed0
|
mv util/lp to math/lp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|