* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing the build of lp_tst
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* fixing the build of lp_tst
* remove unnecessery call to contains() before
insert to indexed_uint_set
* formatting, no check for contains()
in indexed_uint_set, always init m_touched_rows to nullptr
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use heap to track infeasible columns
* fix the formatting
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
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.
* avoid creating rows with all but one fixed columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* pb
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* once in a while flip bounds of boxed variables during move_nbasic_to_bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* flip rarely
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* flip rarely
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* flip rarely
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* return an empty model when lar_solver is not ready
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* randomly change bounded base var on demand only
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* randomly change bounded base var on demand only
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
