Lev Nachmanson
|
d310ae9060
|
rebase with Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
7eac995824
|
misc fixes to grobner state (#109)
* fixes to use list bookkeeping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix reset logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix non-termination bug in simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing reset of values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add configuration to throttle memory usage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix misc. invariant violations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* multiple linear constraints seem to be violated
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
a9a602c1aa
|
memory throttling (#108)
* fixes to use list bookkeeping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix reset logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix non-termination bug in simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing reset of values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add configuration to throttle memory usage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.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 |
|
Nikolaj Bjorner
|
c5187902ad
|
reset also m_values (#107)
* fixes to use list bookkeeping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix reset logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix non-termination bug in simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing reset of values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e8f29b3144
|
fix init 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
|
279bcb733d
|
expose grobner statistics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
83fa083def
|
expose grobner statistics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
f212ba97de
|
non-termination fix (#106)
* fixes to use list bookkeeping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix reset logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix non-termination bug in simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
014e5158c0
|
fix reset (#105)
* fixes to use list bookkeeping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix reset logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
9ae9877353
|
update stats in check_pdd_eq()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
407c8a60db
|
reverse the order of vars for pdd_grobner, use pdd_grobner.reset()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b5364b787c
|
set level2var for m_pdd_manager of pdd_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c152660911
|
add a call m_pdd_manager.set_level2var()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0bb29bca69
|
change core::get_var_weight() to return unsigned, remove some warnings from test/lp/lp.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1cc5935953
|
call m_pdd_grobner.reset()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a922328358
|
integrate with Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b9f74db14c
|
hook up pdd_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c6ea5c2263
|
prepare to hook up pdd_grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
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 |
|