Lev Nachmanson
bdecbe4ed7
remove a duplicate method
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-05-13 15:38:20 -07:00
Lev Nachmanson
6b28973799
nla review ( #4321 )
...
* simplify the nla_solver interface
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* more simplifications
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* init m_use_nra_model
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* work on NSB comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* work on NSB comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-13 13:52:42 -07:00
Lev Nachmanson
3e4a4c6df2
rebase with master branch
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-05-11 19:12:02 -07:00
Lev Nachmanson
e32a6714a5
call nlsat
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-05-11 19:12:02 -07:00
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
81b3c440ce
fix mixup between constraint indices and lpvar explanations fixes various newly reported unsoundness bugs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-11 13:07:28 -07:00
Nikolaj Bjorner
99043399ce
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-10 20:28:35 -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
caee936af5
build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-10 13:42:19 -07:00
Nikolaj Bjorner
e74faf42ad
code review
2020-05-10 12:58:05 -07:00
Nikolaj Bjorner
1ecc6a21fa
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-10 11:21:15 -07:00
Nikolaj Bjorner
d774ba9da1
fixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-10 09:57:24 -07:00
Nuno Lopes
6c72f39142
fix build
2020-05-10 10:35:46 +01:00
Nikolaj Bjorner
0a6908cd15
abbreviate
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 21:54:58 -07:00
Nikolaj Bjorner
086331a24b
null
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 21:27:45 -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
Nikolaj Bjorner
4890c3ce31
fix #4230
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 18:49:00 -07:00
Nikolaj Bjorner
fdc87f286f
na ( #4254 )
...
* remove level of indirection for context and ast_manager in smt_theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add request by #4252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move to def
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4251
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4255
* fix #4257
* add code to debug #4246
* restore new solver as default
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4246
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 17:40:02 -07:00
Lev Nachmanson
8921ed56b5
fix a bug in Horner heuristic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-23 15:58:53 -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
Nikolaj Bjorner
e8c3324c3f
reduce number of redundant arguments and pointers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
44d2f6da6c
fix #3261
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.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
971ae50ba3
move m_intervals to nla_core
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08: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
f4e7002ea3
forgotten changes after a rebase
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
1a7a537834
work on horner's heuristic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
130995a3db
print terms as monomials
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
8955509023
disable interval lemmas
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
f24bd352e1
throttle intervals
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
999ca2ed70
no intervals
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
3f6ecfb3b6
generate lemmas from nla_intervals
...
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
