Lev Nachmanson
|
610a2837ea
|
rebase with Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
f8deb4ed5f
|
add NOT_IMPLEMENTED_YET
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
|
5e19a52772
|
merge changes from Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
aafdab65bd
|
fix the build and extend options to run grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
1d217595c8
|
add pdd_interval to evaluate intervals of pdd expressions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
fffd764226
|
fix a typedef
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
|
ee255ef8b3
|
merge changes from Z3Prover repository
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
f22d4b50cc
|
define setter and getter for var2var in pdd_eval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
a9f09beb8e
|
add the pdd evaluator and a unit test for it
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
7eb1affc7b
|
after rebasing with Z3Prover
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 |
|
|
Lev Nachmanson
|
1dbffe7367
|
limit expr.size() in grobner by 20
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c3099a5719
|
call algebraic routines only basing on the frequency
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
48f7e69d0e
|
only run grobner when horner fails, introduce concat instead copy
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
919946b567
|
revert the last commit with freeing the memory
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
13ff96b40b
|
more agressive freeing memory from nla_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
62dc731b5b
|
remove some debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
3b61f0b874
|
enable interval multiplication without dependencies
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
0535e24dd1
|
consolidate parameters, add comment (#102)
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* code review of nla_intervals: combine functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge issue
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* tired of looking at compiler warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
580f229a16
|
free memory in nex_creator during GB init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
519bbc5af1
|
reshaffle the template definitions from nla_interval.h to nla_interval.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Nikolaj Bjorner
|
b6c28764f8
|
nla_interval initial review (#101)
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* code review of nla_intervals: combine functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
26956cafb0
|
limit the size of expressions in Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
7ddcfcafad
|
limit explosiion of expressions in Grobner, allow rows containing free vars to Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Nikolaj Bjorner
|
fb69139daa
|
minor (#100)
* 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>
* * -> &, remove unused functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* m_allocated isn't used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* neither is m_tmp_var_set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove eq_stat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* const qualifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* mostly -> to .
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
efe4d6c53c
|
fix the build and restore the nex_pow gt() comparison
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
f17c3c3b12
|
fix ubuntu's build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Nikolaj Bjorner
|
b46c67ce14
|
more code review (#99)
* 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>
* * -> &, remove unused functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* m_allocated isn't used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* neither is m_tmp_var_set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove eq_stat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* const qualifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.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
|
9661f75246
|
add an assert test_find_b_c()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
2fbb4cac9d
|
a fix in nex comparison and impovement of grobner stats
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
ef2520ace2
|
NB's review
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
1df6411580
|
fix a bug in :divide_ignore_coeffs_perform_nex_mul()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
882b8ee63b
|
NB's review
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
3f442ecef9
|
remove m_conflict from nla_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
d0f682b239
|
review of NB
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
0db79b1c79
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
ac0b8ba455
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
7642f74142
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
617e1387f4
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
060c1b0b0b
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
da8a7e256f
|
revert the simplification loops
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
bc302285a1
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
40c81d14d8
|
integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
eee8188abf
|
add trace statement
Signed-off-by: Lev Nachmanson <levnach@hotmail.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
|
03f7c96c5a
|
rename lt to gt in nex_creator etc. to clarify the semantics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
|
Lev Nachmanson
|
9ecae4abad
|
revert changes in smt directory
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|