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

16466 commits

Author SHA1 Message Date
Nikolaj Bjorner e0945f57bb fix #7554 
mbp_qel  uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
 2025-02-18 21:04:34 -08:00
Nikolaj Bjorner 28f3f8046e #7559 2025-02-18 20:50:06 -08:00
Nikolaj Bjorner 11066486d7 #7559 2025-02-18 20:48:13 -08:00
Nikolaj Bjorner 991cffb519 handle multi-arity arrays 2025-02-18 20:38:45 -08:00
Nikolaj Bjorner 674e1b8f98 remove equality check on container 2025-02-18 20:15:42 -08:00
Nikolaj Bjorner ce69b54b5f adjust select/store rule for n-ary arrays 2025-02-18 20:08:56 -08:00
Nikolaj Bjorner 42f6e1300a more review of mbp_arrays 2025-02-18 19:48:54 -08:00
Nikolaj Bjorner a4a84ed083 arrays are not necessarily unary 2025-02-18 19:13:12 -08:00
Nikolaj Bjorner a5e5a35755 code simplification 2025-02-18 19:07:58 -08:00
Nikolaj Bjorner a143ed3bff taking a look at mbp_qel for arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 16:28:49 -08:00
Nikolaj Bjorner 813da35539 fix unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-17 20:36:38 -08:00
Nikolaj Bjorner f8f26788ad convert def into expression tree 
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
 2025-02-17 18:47:00 -08:00
Nikolaj Bjorner f977b48161 adjust solve_for to handle rationals 2025-02-17 13:59:23 -08:00
Nikolaj Bjorner 528efbb535 fixes to failure conditions for unification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 13:41:17 -08:00
Nikolaj Bjorner fe27ca1dd0 remove verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 13:23:56 -08:00
Nikolaj Bjorner 50f9fddfd2 Add unification based projection function 
Heuristic for EMBPR is to unify terms that occur in uninterpreted contents. Walk partitions that are pure f(t) and an impure f(s)
and attempt to unify t with s ensuring that merges from s preserves satisfiability.
 2025-02-16 13:18:21 -08:00
Nikolaj Bjorner b27a2aa7fc remove calls to removed def constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 10:13:00 -08:00
Nikolaj Bjorner a703cf81b1 replace model_ref by model* in tg_project, 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-15 19:34:52 -08:00
Nikolaj Bjorner eee96ec312 bug fixes and cleanup in projection functions 
spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
 2025-02-15 14:11:20 -08:00
Lev Nachmanson bedc95c4c7 use static_cast to avoid the warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-13 07:07:12 -10:00
Phil Clayton e6a089e63d
Fix build when Z3_API macro is non-empty (#7553) 
API function definitions are updated to be consistent with header files.
 2025-02-13 08:46:08 -08:00
Nikolaj Bjorner 94d3c591b5 make sure ackermann works with arrays that have more than one argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 21:28:31 -08:00
Nikolaj Bjorner 9ea921ba8e update spacer projection for arrays to allow ackerman reduction for non-integer arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-11 17:38:56 -08:00
Lev Nachmanson e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 957b177c64 set arith.lp.dio_cuts_enable_gomory to False by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5ec10e0250 address the review 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 8a9edd1aa7 fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 79e3f8ab39 disabling dio handler by default, and fix a print out 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 2131e9b4e4 more accurate work with Markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bdb8f54150 Revert "revert the term sorting" 
This reverts commit c79d4708cb.
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5ebee24850 revert the term sorting 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson f2c1fd4c14 try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson cec8dc2e6e try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3f2d2e8348 test 2025-02-11 12:23:00 -10:00
Lev Nachmanson b6701d57f9 try another sort in tightening 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5b0b224a5c try sorting terms before tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson dcd5783232 remove the fresh definition when removing its column 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 17d68c18aa comment change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson d90b94d0e2 stricter is_in_sync paying attenion to m_row2fresh_defs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 134bed826a throttle the branching in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bd8cf29df7 ignore large changed_columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3ac11cd136 fix assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson cf4e402a0f avoid usisg indexed_vector for term operations 2025-02-11 12:23:00 -10:00
Lev Nachmanson 440d78f237 disallow duplicates in a queue 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 7e02dfe484 add stats on m_dio_branching_conflicts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 0bf3ca87e7 call normalize_e_by_gcd() only when moving an entry from F to S 2025-02-11 12:23:00 -10:00
Lev Nachmanson 99538567a7 rebase with master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson a19e10912f make dio less aggressive, allow other cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson fee707842d register m_added_terms in m_changed_terms 2025-02-11 12:23:00 -10:00
Lev Nachmanson 21f67ef942 out of bounds fixes 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3b3d8cee03 use m_chandedNterms to tighten terms 2025-02-11 12:23:00 -10:00
Lev Nachmanson 65bdd58d3e remove struct entry 2025-02-11 12:23:00 -10:00
Lev Nachmanson a9098a5785 optimise l terms addition 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3e7e903d19 use the trail to undo add_term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 9c510018b3 fix the debug build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 058b9e4a6d optimise rewrite_eqs to avoid fresh variables 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson ed3df333b3 make rewrite_eq boolean, and relax an ASSERT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson ca7c128d3f clean up fresh definitions on a pop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson b027761845 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bb869fd020 don't store fresh definitions in m_e_matrix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson e5ffc3cfae cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson d7de7eb732 remove recalculated entries from S 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson ef55de1646 fix out of bounds bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3990df6d91 substitute variables with a queue on the recalculated entries 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 78d91f3794 simplify dio handler by using bijection m_k2s 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 33f5e303f8 use entry_status for FRESH entries 2025-02-11 12:23:00 -10:00
Lev Nachmanson 0e71adfa35 fix some warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 7bba8bc0c9 fix some warnings 2025-02-11 12:23:00 -10:00
Lev Nachmanson abac52e1d7 remove var_register_dio.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 89eec4cc80 test dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5a72117528 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 0027ae21e8 bug fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5158797233 refine trail iterations with lar.m_terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 9a9ccf19c5 introdure lar_term.ext_coeffs(), dio passes some tests 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 083926c658 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson a0ece6dd2c cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson ceeece6770 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson ac5c50f179 fix ubuntu build in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson c1ece49694 track changed columns in dio\ 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 008e9229a5 use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 57b665d075 work on incremental dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 28556ce625 cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 862dc91cb2 work on incremental dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson fd3bd088a4 remove some warnings 2025-02-11 12:23:00 -10:00
Lev Nachmanson 9a96aa94e6 test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bef313f7a0 test 2025-02-11 12:23:00 -10:00
Lev Nachmanson 7ecac27335 fix a bug in dio 2025-02-11 12:23:00 -10:00
Lev Nachmanson b0383da8f2 fix a bug in dio 2025-02-11 12:23:00 -10:00
Lev Nachmanson 7fe703e229 simplify column 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 8d747865ae cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson deac00ada3 persist dio handler 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 2c8a6f83e4 change int_solver to call find_cube and hnf_cut, conditionally 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 39da4f6dbd remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 28d41783b8 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 397fdf657d fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 63980f3bfd fixes in dio branching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 6bc7662580 passes z3test 2025-02-11 12:23:00 -10:00
Lev Nachmanson 174185582a collect the explanation correctly 2025-02-11 12:23:00 -10:00
Lev Nachmanson bc0fdfe158 remove dead code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson c300843585 cancel bugs fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00