Nikolaj Bjorner
a4ea281602
fix #6260
2022-08-06 08:21:52 +03:00
Nikolaj Bjorner
2696775088
remove stale assertion
...
with support for substitutions we allow the simplifier to change the state of equations.
2022-07-15 04:03:25 -07:00
Nikolaj Bjorner
7c177584f3
add propagators to grobner
2022-07-14 15:45:07 -07:00
Nikolaj Bjorner
316ed778e0
Tune Grobner equations
...
\brief convert p == 0 into a solved form v == r, such that
v has bounds [lo, oo) iff r has bounds [lo', oo)
v has bounds (oo,hi] iff r has bounds (oo,hi']
The solved form allows the Grobner solver identify more bounds conflicts.
A bad leading term can miss bounds conflicts.
For example for x + y + z == 0 where x, y : [0, oo) and z : (oo,0]
we prefer to solve z == -x - y instead of x == -z - y
because the solution -z - y has neither an upper, nor a lower bound.
The Grobner solver is augmented with a notion of a substitution that is applied before the solver is run.
2022-07-11 16:14:26 -07:00
Nikolaj Bjorner
b68af0c1e5
working on reconciling perf for arithmetic solvers
...
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.
The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.
The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
2022-07-11 07:38:51 -07:00
Nikolaj Bjorner
3d00d1d56b
prepare for equality propagation from Grobner basis
...
Attempt to remedy performance regressions from the new solver core for NLA. It misses easy lemmas, presumably due to weaker bounds information.
2022-06-14 09:51:07 -07:00
Nikolaj Bjorner
5ee9edf46b
fix incorrect bound in order-lemma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-13 14:28:42 -07:00
Nikolaj Bjorner
9ca5b3f304
fix #4449
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-03 21:10:07 -07:00
Lev Nachmanson
06203d227e
cleanup the grobner config init
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
7ad95aa5d2
Nikolaj fixes pdd_manager::reduce() to work with the changed order
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
00e1049ff2
move some grobner settings to pdd_solver.m_config
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
bb6511b425
add parameters to control grobner's explosure
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
7a2dc6e69e
disable pdd_solver::invariant()
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
d6a246777a
Nikolaj implemented lm_lt on dd::pdd
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
d1e9998332
add a config parameter to grobner
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
2b7393778e
apply hardcoded thresholds
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
c1032c3403
remove watch, hoist orbit to track used variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-02 00:39:50 -08:00
Nikolaj Bjorner
1d0572354b
add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-01 20:14:20 -08:00
Nikolaj Bjorner
09dbacdf50
remove unused functionality
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-01 20:14:20 -08:00
Nikolaj Bjorner
6b4ddf352d
port fixes from lev's branch. Rename pdd_grobner to pdd_solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-01 20:14:20 -08:00
