Nikolaj Bjorner
960a024d3d
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-10 13:54:00 -07:00
Nikolaj Bjorner
6445d01557
normalize newlines for if
2023-10-10 13:43:49 -07:00
Nikolaj Bjorner
d04807e8c3
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-10 13:43:38 -07:00
Nikolaj Bjorner
338d7b3283
remove unused variables
2023-10-10 13:42:21 -07:00
Nikolaj Bjorner
f3e9712beb
formatting
2023-10-10 13:42:21 -07:00
Nikolaj Bjorner
e8e636c3ec
fix #6936
2023-10-10 13:42:21 -07:00
Lev Nachmanson
7afa4d0752
Merge pull request #6938 from Z3Prover/uprop
...
fix a bug in unit nl prop. This also speeds up the nl propagation by more than 20 percent.
2023-10-10 09:49:41 -07:00
Lev Nachmanson
180ab727e7
fix a bug in unit nl prop
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-10-10 07:32:07 -07:00
Nikolaj Bjorner
adbee0cd3f
fix #6937
2023-10-10 16:02:59 +09:00
Nikolaj Bjorner
267e9e827d
#6935
2023-10-10 15:52:54 +09:00
Nikolaj Bjorner
4a870966ad
add code to enable unit propagation of bounds
...
set UNIT_PROPAGATE_BOUNDS 1 to use the unit propagation version. It applies unit propagation eagerly (does not depend on checking LIA consistency before final check) and avoid creating new literals in most cases
2023-10-09 16:04:39 +09:00
Nikolaj Bjorner
1bdf66b918
move initialization to header file
2023-10-09 10:55:43 +09:00
Lev Nachmanson
75e29b2a6d
Merge pull request #6905 from Z3Prover/unit_prop_on_monomials
2023-10-08 18:20:44 -07:00
Lev Nachmanson
1ba0f5aba9
cosmetic changes
2023-10-08 10:16:40 -07:00
Lev Nachmanson
3aac528aef
add a comment
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-10-08 07:34:03 -07:00
Nikolaj Bjorner
54f7aac0bc
column value is not necessarily at bounds
2023-10-08 17:18:26 +09:00
Lev Nachmanson
4c228fb02c
Merge branch 'master' into unit_prop_on_monomials
2023-10-06 07:24:05 -07:00
Lev Nachmanson
a94a75459e
fixin nla_solver_test.cpp
2023-10-06 06:51:00 -07:00
Lev Nachmanson
f847d039bc
use the simple version of move_non_basic_column_to_bounds
2023-10-05 20:57:54 -07:00
LufyCZ
19e921290e
increase wasm stack size ( #6931 )
2023-10-06 11:49:54 +09:00
Christoph M. Wintersteiger
23de8056d7
Add RCF functions to OCaml API ( #6932 )
2023-10-06 11:49:22 +09:00
Lev Nachmanson
bf3817ef7c
restore move_non_basic_to_bounds
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-10-05 18:14:52 -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
Nikolaj Bjorner
b0df74c1c1
#6930
...
simplify assumptions and only replay assumptions after constraints are simplified. This allows simplifying assumptions with the current set of constraints independently of whether there is another check-sat.
2023-10-05 17:23:17 +09: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
Clemens Eisenhofer
4133a1cc5a
Fix UP registration in final callback ( #6929 )
...
* Fix registration in final
* Don't make it too complicated...
2023-10-03 09:51:02 +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
Nikolaj Bjorner
ab8fe199c5
fix case for 0 multiplier in monomial_bounds
...
disabled in master - it violates invariants in the lra solver.
2023-10-01 18:41:23 +09:00
Nikolaj Bjorner
50654f1f46
add theory propagation to linear monomial propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-30 08:52:09 +09:00
Lev Nachmanson
702322a6e9
change the order of lp and nlp propagation
2023-09-29 15:31:32 -07:00
Lev Nachmanson
b64fdef41f
better tracking changinc rows and monomials
2023-09-29 15:27:22 -07:00
Lev Nachmanson
f30a2c13be
propagate only one non-fixed monomial intrernally
...
lar_solver
2023-09-28 17:24:34 -07:00
Nikolaj Bjorner
ddcd1ee992
non-fixed term should have bound 0
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-28 09:25:36 -07:00
Nikolaj Bjorner
65e59e3ec4
sketch of internal propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 20:43:38 -07:00
Nikolaj Bjorner
7207f0ff9c
sketch of internal propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 20:40:55 -07:00
Lev Nachmanson
29b5c47a8d
track changed monics efficiently
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-27 09:09:38 -07:00
Nikolaj Bjorner
9033b826f4
debug output with the variable that is fixed and its value
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 00:52:26 -07:00
Nikolaj Bjorner
42767b9aab
Merge branch 'master' into unit_prop_on_monomials
2023-09-26 23:55:37 -07:00
Nikolaj Bjorner
2297b0334b
re-introduce simple implementation of linear monomial propagation for evaluation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 23:53:14 -07:00
Nikolaj Bjorner
6559e5fb32
port over std_vector and std-allocator functionality from monomial propagation branch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 21:15:07 -07:00
Nikolaj Bjorner
aaa587398e
add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:52:34 -07:00
Nikolaj Bjorner
4b85a105bb
Merge branch 'master' into unit_prop_on_monomials
2023-09-26 20:25:43 -07:00
Nikolaj Bjorner
9c63ea3135
port over cosmetics from unit_prop_on_monomials branch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:24:49 -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
ac6310d1a8
Merge branch 'master' into unit_prop_on_monomials
2023-09-26 20:15:16 -07:00