Lev Nachmanson
14312ef8a3
remove some warnings with clang
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-11-02 15:34:41 -07:00
Nikolaj Bjorner
3fa67777e5
fix exception safety in pdd-solver
2023-10-17 19:50:13 -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
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
