this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
- allow multiple defs to be added with same pool of removed formulas
- fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
\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.
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.
* remove the bound on total iterations in simplex
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove unncesseray checks in get_freedom_interval_for_column()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the build of test-z3
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Revert "remove unncesseray checks in get_freedom_interval_for_column()"
This reverts commit 6770ed85e3.
* optimize get_freedom_interval_for_column() for feasible case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add function lar_solver::status_feasible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* rename status_is_feasible() to is_feasible()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the linux build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
