Lev Nachmanson
|
08c9953a36
|
implement the case of small factor in basic proportional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
ee6e21c614
|
work on niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e3ff457af5
|
work on niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
efee734ec9
|
return one of the conjuncions for basic proportionality case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
dd0c8e4f6b
|
remove an inifinite loop in basic_proportionality
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
64ecefdf07
|
tinker with bound atom (#80)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
89d086fff0
|
add a case to basic zero scenario
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
029a486884
|
improve printing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
d935bdb6c4
|
create a lemma for basic proportional case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
633265cc6a
|
merging Nikolaj's changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
e16d8118ac
|
going over niil_solver (#79)
* change conflict to th_axiom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* going over niil_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
a9a45b7b47
|
change conflict to th_axiom (#78)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3138c929ee
|
niil_solver basic case progress
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3fb361c886
|
niil_solver basic case progress
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1fce8ee0b1
|
niil_solver basic case progress
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c1b976fbf4
|
niil_solver basic case progress
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
10871ad76e
|
towards basic newtral check
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
08d891891e
|
handle unsorted monomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
237db5cb3d
|
niil_solver basic case zero
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
eca5ddaa04
|
base case zero in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
d8f5ec3b52
|
basic case - zero for niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
95ffc029d4
|
rename var_info to var_lists in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
93ec6360bd
|
map vars to constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
88ea90fbb9
|
handle output from niil_solver (#77)
* handle output from niil_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add proper equality handling
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
49ae42cebd
|
produce the first lemma in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0911fc2bda
|
use explanation.h for conflict explanations everywhere
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
fd0f6bcbf9
|
about to create a lemma in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0340c8c338
|
work on niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b4aaaffc99
|
work on niil base case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
406a021310
|
work on niil_solver base case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
134ebb5712
|
start on generate_lemma in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
31d44471a1
|
remove some warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
9958f42d5c
|
add files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
92b5a9b134
|
work on niil
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
91086baa54
|
check monomial values in niil_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f6291abccb
|
change the type of lar_solver:get_model to a template
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a86601f7d2
|
work on niil_solver::check()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
07c9e22303
|
refactor mon_eq out or nra_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b6f07e2a23
|
roll back changes in get_model
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0dbe8982ce
|
simplify lar_solver::get_model
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
fa5d10b6dd
|
work on switcher
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
253facff46
|
work on switcher
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
032a4efdb6
|
work on switcher
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
a5c62bfcc4
|
preparing niil files
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
c979c694f6
|
remove an unused method
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
ee62f83131
|
fix #2892
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-27 20:59:02 -08:00 |
|
Nikolaj Bjorner
|
ca11dc1fc5
|
remove ad-hoc rewriting of division related to comparison.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-27 17:36:02 -08:00 |
|
comet
|
eea7805551
|
update
|
2020-01-27 15:27:11 -08:00 |
|
Nikolaj Bjorner
|
d12523e4c0
|
fix #2883
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-27 08:57:16 -08:00 |
|
Nikolaj Bjorner
|
9c0e350bc4
|
rewrite3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-26 18:50:58 -08:00 |
|