Nikolaj Bjorner
|
3726960969
|
fix #6969
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-29 17:44:00 -07:00 |
|
Nikolaj Bjorner
|
589024aa1c
|
fix #6969
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-29 17:44:00 -07:00 |
|
Nikolaj Bjorner
|
bd8e5eee4b
|
add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-29 10:21:31 -07:00 |
|
Nikolaj Bjorner
|
e2db2b864b
|
add hook for in-processing simplification for NLA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-25 15:09:21 -07:00 |
|
Nikolaj Bjorner
|
97058b0d5d
|
allow for propagations the trigger make-feasible check
|
2023-10-19 16:08:44 -07:00 |
|
Nikolaj Bjorner
|
bdac86501d
|
add facility to check for missing propagations
|
2023-10-15 20:33:48 -07:00 |
|
Nikolaj Bjorner
|
891ab8bac5
|
#6523
fixup looping
|
2023-10-15 12:37:14 -07:00 |
|
Nikolaj Bjorner
|
6553382ec8
|
remove extra assume-eqs
|
2023-10-15 12:30:24 -07:00 |
|
Nikolaj Bjorner
|
41b1f47d77
|
#6523
deal with memory leak when there is an exception
|
2023-10-15 12:15:28 -07:00 |
|
Nikolaj Bjorner
|
08af965b56
|
updates to monomial bounds
|
2023-10-14 01:33:05 -07:00 |
|
Nikolaj Bjorner
|
d04807e8c3
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-10 13:43:38 -07:00 |
|
Lev Nachmanson
|
b61f4ac51f
|
merge changes from master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-10-05 07:50:13 -07:00 |
|
Lev Nachmanson
|
45c0ed126e
|
remove unnecessery call
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-10-04 17:39:22 -07:00 |
|
Lev Nachmanson
|
edd1761ff3
|
restore the scheme of m_columns_with_changed_bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-10-04 11:06:24 -07:00 |
|
Lev Nachmanson
|
a88aa7ffa5
|
debug new propagation scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-10-03 16:25:49 -07:00 |
|
Nikolaj Bjorner
|
00ba064cd3
|
ensure bounds propagation on changed columns after nla propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-10-03 14:28:59 +09:00 |
|
Lev Nachmanson
|
7de06c4350
|
merging master to unit_prop_on_monomials
|
2023-10-02 16:42:59 -07:00 |
|
Lev Nachmanson
|
a297a2b25c
|
fixes in lar_solver around nl unit propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-10-01 11:39:58 -07:00 |
|
Lev Nachmanson
|
702322a6e9
|
change the order of lp and nlp propagation
|
2023-09-29 15:31:32 -07:00 |
|
Nikolaj Bjorner
|
94eb101873
|
Merge branch 'master' into unit_prop_on_monomials
|
2023-09-26 20:15:58 -07:00 |
|
Nikolaj Bjorner
|
36566d6193
|
port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-26 20:15:22 -07:00 |
|
Nikolaj Bjorner
|
e4e1d6148c
|
port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-26 20:14:42 -07:00 |
|
Nikolaj Bjorner
|
ec2937e2de
|
port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-26 20:08:30 -07:00 |
|
Lev Nachmanson
|
6ff4856e38
|
throttle monomial unit prop and and nl params
|
2023-09-25 16:47:34 -07:00 |
|
Lev Nachmanson
|
896aba31f8
|
move monomial propagation from theory_lra to nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-09-25 14:20:24 -07:00 |
|
Nikolaj Bjorner
|
0a1ade6f95
|
move m_nla_lemma_vector to be internal to nla_core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-25 12:40:52 -07:00 |
|
Lev Nachmanson
|
26a9b776c6
|
clean m_nla_lemma_vector in nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-09-25 12:10:59 -07:00 |
|
Nikolaj Bjorner
|
a3e2e68d93
|
Update theory_lra.cpp
|
2023-09-23 16:26:31 -07:00 |
|
Nikolaj Bjorner
|
421fe94607
|
rmove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-22 17:59:07 -07:00 |
|
Nikolaj Bjorner
|
eac54ba084
|
indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-22 16:54:12 -07:00 |
|
Nikolaj Bjorner
|
940775d12d
|
indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-22 16:48:40 -07:00 |
|
Lev Nachmanson
|
caa929f01f
|
do not use lemmase in monomial propagation
|
2023-09-22 14:27:26 -07:00 |
|
Lev Nachmanson
|
f423642e9b
|
try the lemma scheme
|
2023-09-21 12:18:21 -07:00 |
|
Lev Nachmanson
|
e31cecf5db
|
transfer propagate monomial bounds to nla_solver
|
2023-09-21 11:27:53 -07:00 |
|
Lev Nachmanson
|
536930b4a1
|
make m_ibounds inside of lp_bound_propagator
a reference
|
2023-09-20 17:13:25 -07:00 |
|
Nikolaj Bjorner
|
4d742001ab
|
formatting of else
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-09-19 14:36:21 -07:00 |
|
Lev Nachmanson
|
c5cfd62e0a
|
remove dead code related to nla unit propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2023-09-19 10:56:09 -07:00 |
|
Lev Nachmanson
|
b621c9fa1c
|
remove an extrac check in bound_is_interesting
|
2023-09-15 17:42:18 -07:00 |
|
Lev Nachmanson
|
762ade2a79
|
check m_unassigned_bounds in bound_is_interesting
|
2023-09-15 06:15:22 -07:00 |
|
Lev Nachmanson
|
c309d52283
|
runs a simple test
|
2023-09-13 08:12:00 -07:00 |
|
Lev Nachmanson
|
41f59cb1ed
|
propagate monomial is nla
|
2023-09-05 18:49:59 -07:00 |
|
Lev Nachmanson
|
5509b468e9
|
handle monomial_bounds::unit_propagate()
|
2023-08-31 17:35:41 -07:00 |
|
Nikolaj Bjorner
|
38b131386d
|
add stubs for monomial unit propagation
|
2023-08-30 17:21:48 -07:00 |
|
Lev Nachmanson
|
9aeaed8f53
|
Merge branch 'master' into nl_branches
|
2023-08-21 16:15:20 -07:00 |
|
Nikolaj Bjorner
|
5e3df9ee77
|
Arith min max (#6864)
* prepare for dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* snapshot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* more refactoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* more refactoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* pass in u_dependency_manager
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* address NYIs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* more refactoring names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* eq_explanation update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add outline of bounds improvement functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove unused structs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* more bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* more bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* convert more internals to use u_dependency instead of constraint_index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* convert more internals to use u_dependency instead of constraint_index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remember to push/pop scopes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use the main function for updating bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove reset of shared dep manager
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable improve-bounds, add statistics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-08-19 17:44:09 -07:00 |
|
Lev Nachmanson
|
610313946d
|
split free vars in nla
|
2023-08-18 12:36:14 -07:00 |
|
Nikolaj Bjorner
|
73724f9cab
|
lines that go away
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-08-17 18:45:49 -07:00 |
|
Lev Nachmanson
|
252a30e727
|
use param_ref in nla_solver (#6862)
* use param_ref in nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add parameters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add parameters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* replace nla_setting by command line parameters
* delete nla_setting.h
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-08-17 18:44:27 -07:00 |
|
Nikolaj Bjorner
|
125787c458
|
remove dead code
|
2023-08-07 11:22:34 -07:00 |
|
Nikolaj Bjorner
|
84520d53ea
|
remove out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-08-04 11:33:39 -07:00 |
|