Lev Nachmanson
e091a2e775
remove the line with clang-format off
2023-07-10 12:05:59 -07:00
Lev Nachmanson
5ed2a82893
set clang format off for lp files ( #6795 )
...
* adding // clang-format off
* set clang-format off at the beginning of lp files
* set clang-format off
* remove dead code
2023-07-03 17:35:16 -07:00
Lev Nachmanson
32ec02778e
use heap to track infeasible columns. ( #6771 )
...
* 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>
2023-06-19 13:50:14 -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
b43ed70874
extend monomial bounds to handle powers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-14 19:13:17 -07:00
Nikolaj Bjorner
179c9c2da2
consolidate methods that add lemma specific information to under "new_lemma"
2020-05-10 18:31:57 -07:00
Nikolaj Bjorner
30de76b529
add occurs check to other nla_basic lemmas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 20:50:27 -07:00
Nikolaj Bjorner
4890c3ce31
fix #4230
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 18:49:00 -07:00
Nikolaj Bjorner
fdc87f286f
na ( #4254 )
...
* remove level of indirection for context and ast_manager in smt_theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add request by #4252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move to def
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4251
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4255
* fix #4257
* add code to debug #4246
* restore new solver as default
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4246
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-09 17:40:02 -07:00
Lev Nachmanson
56690d16da
remove incorrect order lemmas
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-29 10:21:45 -07:00
Lev Nachmanson
8921ed56b5
fix a bug in Horner heuristic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-23 15:58:53 -07:00
Lev Nachmanson
146489ff14
fix the signs for factorns in tangent lemma
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
4c5c17c7d8
fixes for #3376
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
e8c3324c3f
reduce number of redundant arguments and pointers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Lev Nachmanson
a38f58e49f
simplify tang lemma
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
fd1e0e4d80
fixes for mixed case
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
d310ae9060
rebase with Z3Prover
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
971ae50ba3
move m_intervals to nla_core
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
a0bdb8135d
rename monomial to monic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
cc5a12c5c7
port grobner basis
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
33cbd29ed0
mv util/lp to math/lp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
