mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
19657 commits 49 branches 53 tags 182 MiB
Commit graph

4351 commits

Author SHA1 Message Date
Nikolaj Bjorner
eed02b6d86 improved logging, use C++11 for loops instead of iterators 2023-11-07 19:57:49 +01:00
Lev Nachmanson
ca6cb0af95 add changes in lp with validate_bound and maximize_term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-11-02 09:59:03 -07:00
Nikolaj Bjorner
49a071988c remove temporary algebraic numbers from upper layers, move to owner module 2023-11-01 03:52:20 -07:00
Nikolaj Bjorner
ea915e5b37 #6971 
clear m_a1, m_a2 before calls that may affect model.
 2023-11-01 03:36:01 -07:00
Nikolaj Bjorner
f97dd34028 tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-30 14:54:04 -07:00
Nikolaj Bjorner
938a89e197 prepare for local version of Gomory cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 19:45:14 -07:00
Nikolaj Bjorner
a957a5673d remove experiment with theory lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 18:48:48 -07:00
Nikolaj Bjorner
3726960969 fix #6969 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 17:44:00 -07:00
Nikolaj Bjorner
589024aa1c fix #6969 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 17:44:00 -07:00
Christoph M. Wintersteiger
9d57bdd2ef
Assorted fixes for floats (#6968) 
* Improve 4be26eb543

* Add-on to 0f4f32c5d0

* Fix mk_numeral

* Fix corner-case in fp.div

* Fixes for corner-cases in mk_to_fp_(un)signed

* Fix out-of-range results in mpf_manager::fma

* Further adjustments for fp.to_fp_(un)signed

* fp.to_fp from real can't be NaN

* fp.to_fp from reals: add bounds

* Fix NaN encodings in theory_fpa.

* Fix fp.fma rounding with tiny floats

* Fix literal creation order in theory_fpa
 2023-10-29 17:29:42 -07:00
Nikolaj Bjorner
bd8e5eee4b add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 10:21:31 -07:00
Clemens Eisenhofer
e7c17e68b8
Fixed next_split call in pop (#6966) 
* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied

* Fix registration in final

* Don't make it too complicated...

* Fixed next_split when called in pop
Made delay_units available even without quantifiers

* Missing push calls before "decide"-callback
 2023-10-28 12:46:43 -07:00
Nikolaj Bjorner
20c54048f7 use cone of influence reduction before calling nlsat. 2023-10-25 16:19:23 -07:00
Nikolaj Bjorner
e2db2b864b add hook for in-processing simplification for NLA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-25 15:09:21 -07:00
Nikolaj Bjorner
97058b0d5d allow for propagations the trigger make-feasible check 2023-10-19 16:08:44 -07:00
Nikolaj Bjorner
11ab583232 fix #6956 2023-10-19 10:34:31 -07:00
Nikolaj Bjorner
bdac86501d add facility to check for missing propagations 2023-10-15 20:33:48 -07:00
Nikolaj Bjorner
891ab8bac5 #6523 
fixup looping
 2023-10-15 12:37:14 -07:00
Nikolaj Bjorner
6553382ec8 remove extra assume-eqs 2023-10-15 12:30:24 -07:00
Nikolaj Bjorner
41b1f47d77 #6523 
deal with memory leak when there is an exception
 2023-10-15 12:15:28 -07:00
Nikolaj Bjorner
d44d78f9d1 remove temporary configuration parameter used for testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-14 01:33:05 -07:00
Nikolaj Bjorner
08af965b56 updates to monomial bounds 2023-10-14 01:33:05 -07:00
Nuno Lopes
fcb03aa56c minor code simplification 2023-10-11 01:38:03 +01:00
Nikolaj Bjorner
d04807e8c3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-10 13:43:38 -07:00
Nikolaj Bjorner
338d7b3283 remove unused variables 2023-10-10 13:42:21 -07:00
Nikolaj Bjorner
adbee0cd3f fix #6937 2023-10-10 16:02:59 +09:00
Lev Nachmanson
b61f4ac51f merge changes from master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-05 07:50:13 -07:00
Lev Nachmanson
45c0ed126e remove unnecessery call 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-04 17:39:22 -07:00
Lev Nachmanson
edd1761ff3 restore the scheme of m_columns_with_changed_bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-04 11:06:24 -07:00
Lev Nachmanson
a88aa7ffa5 debug new propagation scheme 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-03 16:25:49 -07:00
Nikolaj Bjorner
00ba064cd3 ensure bounds propagation on changed columns after nla propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-03 14:28:59 +09:00
Lev Nachmanson
7de06c4350 merging master to unit_prop_on_monomials 2023-10-02 16:42:59 -07:00
Lev Nachmanson
a297a2b25c fixes in lar_solver around nl unit propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-01 11:39:58 -07:00
Lev Nachmanson
702322a6e9 change the order of lp and nlp propagation 2023-09-29 15:31:32 -07:00
Nikolaj Bjorner
94eb101873
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 20:15:58 -07:00
Nikolaj Bjorner
36566d6193 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:15:22 -07:00
Nikolaj Bjorner
e4e1d6148c port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:14:42 -07:00
Nikolaj Bjorner
e8fcc876c9
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 20:14:06 -07:00
Nikolaj Bjorner
ec2937e2de port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:08:30 -07:00
Nikolaj Bjorner
8d2b65b20b add options to allow testing the effect of non-linear hammers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 19:18:44 -07:00
Lev Nachmanson
6ff4856e38 throttle monomial unit prop and and nl params 2023-09-25 16:47:34 -07:00
Lev Nachmanson
896aba31f8 move monomial propagation from theory_lra to nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-25 14:20:24 -07:00
Nikolaj Bjorner
0a1ade6f95 move m_nla_lemma_vector to be internal to nla_core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-25 12:40:52 -07:00
Lev Nachmanson
26a9b776c6 clean m_nla_lemma_vector in nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-25 12:10:59 -07:00
Nuno Lopes
029d726eb8 minor code simplification 2023-09-25 15:33:40 +01:00
Nikolaj Bjorner
3433366bef Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials 2023-09-23 17:20:08 -07:00
Nikolaj Bjorner
85eacf9bb1 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-23 17:20:00 -07:00
Nikolaj Bjorner
61319ffd85 cache is_shared information in the enode 
observed perf overhead for QF_NIA is that assume_eqs in theory_lra incurs significant overhead when calling is_relevant_and_shared. The call to context::is_shared and the loop checking for beta redexes is a main bottleneck. The bottleneck is avoided by caching the result if is_shared inside the enode. It is invalidated for every merge/unmerge.
 2023-09-23 17:19:06 -07:00
Nikolaj Bjorner
a3e2e68d93
Update theory_lra.cpp 2023-09-23 16:26:31 -07:00
Nikolaj Bjorner
acad9fa62c
Update smt_context.cpp 2023-09-23 16:25:46 -07:00