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 |
|
Lev Nachmanson
|
6bc5400c5d
|
add deps from fixed vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
379a1927e6
|
fix a bug in nexvar()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f0b530b0e4
|
experiment with substituting zeros in Horner&Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
20af3dd675
|
add options to substitute vars in Horner and Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
d310ae9060
|
rebase with Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
361964f173
|
fix arith errors add_row for nex grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c6e5d434b2
|
create scalars for fixed variables in rows for grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
dd9935de7d
|
preparing a call to pdd_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
22bec010ba
|
use dep_intervals inside of nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0039b68ca3
|
merged dependency.h from main repo
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
14094bb052
|
code review (#98)
* streamline type conversions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use fixed array allocation for sum
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use fixed array allocation for sum
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* revert creation time allocation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* separate grobner_core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* grobner_core simplifications
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a86d4b0675
|
add dependencies for row in grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e62913999e
|
in grobner optional treatment of fixed vars in rows, remove a field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0b1023c2c7
|
do not add row with free basic vars in grobner, more tracing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f5c8ead995
|
port Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
ede4310b32
|
port Grobner: still producing sat lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
538ad77019
|
fixed vars are treated as scalars optionally
Signed-off-by: Lev Nachmanson <levnach@nachmanson.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
d77e9c444e
|
more efficient create_sum_from_row and other fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
64b189d932
|
fixes in nex expressions simplifications
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
7fbf3e0707
|
port Grobner, add fixed var dependencies to create_sum_from_row()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b3fc12ffdc
|
port Grobner, add fixed var dependency to Horner's scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e987479e8a
|
port grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0c126031b0
|
init of m_active_vars_weights and fixes in is_simplified
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a3d0372e3d
|
move the nex object creation from a row to nla_common
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
|
33cbd29ed0
|
mv util/lp to math/lp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|