mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity
18890 commits 23 branches 48 tags 157 MiB
Commit graph

196 commits

Author SHA1 Message Date
Lev Nachmanson a6040a1f3d cautious remove_basis 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson a53ed5bddd change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson b84585beeb more aggressive patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson e5503cdc65 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson 2710afbea1 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Nikolaj Bjorner d372af4782 add stub for cheap equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-30 15:36:27 -07:00
Lev Nachmanson caa384f6c9 make m_inf_set private and cosmetic improvements in nla patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-26 12:44:47 -07:00
Lev Nachmanson 97b480ded3
Expl (#4462) 
* cleaner API for explanation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove an unnecessery check

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* expl

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-24 17:06:39 -07:00
Lev Nachmanson af2f74c05f
smarter explanation.h (#4385) 
* smarter explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* clean explanation API

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* suppress warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-19 12:38:44 -07:00
Lev Nachmanson f2449df06e introduce ul_pair associated_with_row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-05 15:59:09 -07:00
Lev Nachmanson 97fe2c8609 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson d5162d92ad add an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson aa0f5db511 fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson f8037ffda4 always call find_feasible_solution in move_nbasic_columns_to_bounds() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson ba40a5752f better branching with usage_in_terms() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson 530f77281c fixes in branching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-26 16:13:47 -07:00
Lev Nachmanson 8c5993d9a6 max term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-23 18:40:16 -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 5208b64a6b expose only necessary methods of lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-16 12:58:39 -07:00
Lev Nachmanson 6d8e5400fd return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-16 12:58:39 -07:00
Lev Nachmanson 7caae3f5d2 small improvements in tableau in rows and bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-13 16:04:25 -07:00
Nikolaj Bjorner 9b609af8fc fix #3924 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-12 16:19:54 -07:00
Lev Nachmanson 5c9fd90031 work on random_updates 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-07 19:50:50 -07:00
Nikolaj Bjorner c2e5cd78c8 change lar_terms to use column indices 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 12:13:59 -07:00
Nikolaj Bjorner 080dbb13b0 tv alignment, code review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 03:35:19 -07:00
Nikolaj Bjorner 0735491557 path fix #3747, this patches incoherent behavior of terms / ival from lar_solver. The variables occurring in terms are mapped to columns and not as original variables/terms. theory_lra has to interact with the column_corresponds_to_term test instead of relying on the terms themselves carrying the relevant information 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 14:27:56 -07:00
Lev Nachmanson 9d58fccd41 fix in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:43:20 -07:00
Lev Nachmanson 7890555455 fix in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:37:57 -07:00
Lev Nachmanson 7fe46de266 trace random update 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:00:19 -07:00
Lev Nachmanson 55329ea935 more fixes in patching of monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-02 14:47:06 -07:00
Nikolaj Bjorner cc394f0fe9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:42:13 -07:00
Lev Nachmanson cf0952c232 roll back in maximize_term if the integrality is broken 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 17:59:45 -07:00
Lev Nachmanson 3e845010dd replace v by j in lp printouts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 15:59:03 -07:00
Lev Nachmanson 7936df8e0b pass std::function as const aliases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 12:20:47 -07:00
Lev Nachmanson 9be7bda69a fix a bug in column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 7a950dd667 patch reals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 3237bd9243 better tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson f5b62015fc change the return type of ival.var() to tv 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson ea964e5c3b rename int_set to u_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson bc5b68b16e convert term indices to columns in lar_solver::add_equality() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson e2538afd32 better diagnostics in lar_solver and more efficient int_set::resize() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 2975873b91 ensure encapsulation boundaries 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c16d90307b more careful resize in int_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson e0b95979e6 detect the status change in lar_solver::add_equality() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 38eca3b66a fixes in order lemmas and printing terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 316f2194e0 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner e50082b484 add tv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson d758a08497 do not create inf var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6c5d7fbe96 fixes in max term with tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c2e7dd3378 catch the possible infeasible column when adding an equality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 8af245a410 use a simpler encoding for term indices 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 906d52ca1c accept term indices as columns in some lar_solver queries 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f28c80e3b1 reorder fields in lar_solver constructor to avoid a warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner b67d136849 hide flag on registering variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 26631ce38d add a unit test for monics, plus some cosmetic changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 719603f185 register inner terms with null var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a0251ac745 do not register equality terms created in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 285ff9540d make sure that the term external index has not been used 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f636a481d3 fixes in bound setting in cube, and in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a80eb13420 fixes in bound setting in cube, and in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6ea0bcb454 round the bound for columns and terms when it can be deduced that they are integral 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b403b96d38 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 762f265616 merge with master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 02b074e28b compile constraints during internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 19:28:17 -08:00
Lev Nachmanson f45e17c47e fix column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 13:42:39 -08:00
Nikolaj Bjorner 8c016abb12 build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 11:16:57 -08:00
Nikolaj Bjorner 800bc757ae isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:24:45 -08:00
Nikolaj Bjorner 024ca86386 isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:16:14 -08:00
Nikolaj Bjorner a59745c2f2 isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:13:40 -08:00
Lev Nachmanson 06173aa4d7 do not use nl variables in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-04 11:51:37 -08:00
Lev Nachmanson a05dec99cf do not random_update int vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-03 16:01:56 -08:00
Nikolaj Bjorner b0a28160f7 fix #2921 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 10:35:06 -08:00
Lev Nachmanson 35aa98436f fix term columns after rounding in cube() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-30 14:29:36 -08:00
Lev Nachmanson 9694dc0c74 change in the test lp.cpp and in a trace statement 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-29 11:03:18 -08:00
Lev Nachmanson 8ebeaf03b4 rebase with Z3Prover/z3/master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 30d35488d8 get_rid or inf eps 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 0e86c567cc prepare the 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 0b1023c2c7 do not add row with free basic vars in grobner, more tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 687f30a2ce debug grobner and improve printing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 868ea58aef start porting grobner basis functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 006c53e484 remove a wrong assert from lar_solver.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson f4e7002ea3 forgotten changes after a rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 1b8b09cddb fixes in horner's heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 207c1c509f fixes in horner's heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson c95f66e02a toward fetching existing terms intervals from lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson dfe0e85629 toward fetching existing terms intervals from lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 3c5b1086a1 fix remove lar_solver::add_constraint 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 87cc5c8d96 fix a bug in nla_expr 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 130995a3db print terms as monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 3f6ecfb3b6 generate lemmas from nla_intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson c121c5d2d8 remove dead code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 6a6cb3822c before getting explanations for monomials upper and low bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 02133bbcc5 before getting explanations for monomials upper and low bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 9c18ede687 hook up nla_solver it lp bound propagation 
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
Renamed from src/util/lp/lar_solver.cpp (Browse further)