mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
18257 commits 23 branches 48 tags 156 MiB
Commit graph

18257 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson b61f4ac51f merge changes from master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-10-05 07:50:13 -07:00
Nikolaj Bjorner b0df74c1c1 #6930 
simplify assumptions and only replay assumptions after constraints are simplified. This allows simplifying assumptions with the current set of constraints independently of whether there is another check-sat.
 2023-10-05 17:23:17 +09: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
Clemens Eisenhofer 4133a1cc5a
Fix UP registration in final callback (#6929) 
* Fix registration in final

* Don't make it too complicated...
 2023-10-03 09:51:02 +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
Nikolaj Bjorner ab8fe199c5 fix case for 0 multiplier in monomial_bounds 
disabled in master - it violates invariants in the lra solver.
 2023-10-01 18:41:23 +09:00
Nikolaj Bjorner 50654f1f46 add theory propagation to linear monomial propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-30 08:52:09 +09:00
Lev Nachmanson 702322a6e9 change the order of lp and nlp propagation 2023-09-29 15:31:32 -07:00
Lev Nachmanson b64fdef41f better tracking changinc rows and monomials 2023-09-29 15:27:22 -07:00
Lev Nachmanson f30a2c13be propagate only one non-fixed monomial intrernally 
lar_solver
 2023-09-28 17:24:34 -07:00
Nikolaj Bjorner ddcd1ee992 non-fixed term should have bound 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-28 09:25:36 -07:00
Nikolaj Bjorner 65e59e3ec4 sketch of internal propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-27 20:43:38 -07:00
Nikolaj Bjorner 7207f0ff9c sketch of internal propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-27 20:40:55 -07:00
Lev Nachmanson 29b5c47a8d track changed monics efficiently 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-27 09:09:38 -07:00
Nikolaj Bjorner 9033b826f4 debug output with the variable that is fixed and its value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-27 00:52:26 -07:00
Nikolaj Bjorner 42767b9aab
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 23:55:37 -07:00
Nikolaj Bjorner 2297b0334b re-introduce simple implementation of linear monomial propagation for evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 23:53:14 -07:00
Nikolaj Bjorner 6559e5fb32 port over std_vector and std-allocator functionality from monomial propagation branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 21:15:07 -07:00
Nikolaj Bjorner aaa587398e add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:52:34 -07:00
Nikolaj Bjorner 4b85a105bb
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 20:25:43 -07:00
Nikolaj Bjorner 9c63ea3135 port over cosmetics from unit_prop_on_monomials branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:24:49 -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 ac6310d1a8
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 20:15:16 -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 368fe80b3d fix the build 2023-09-25 16:55:02 -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 d2c0f7dba7 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-25 12:48:52 -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 87a839c794 fixup unit test for added argument to constructor of nla_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-23 18:07:56 -07:00
Nikolaj Bjorner 010a994a97 Merge branch 'master' of https://github.com/z3prover/z3 into unit_prop_on_monomials 2023-09-23 17:25:35 -07:00
Nikolaj Bjorner db097bae05 use format from unit_prop_on_monomials branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-23 17:24:46 -07: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
Nikolaj Bjorner eea9c0bec6 fix #6914 2023-09-23 11:22:25 -07:00
Nikolaj Bjorner 30d1800c31 #6916 
short circuiting equality consequence appears to have the wrong sign
 2023-09-23 10:32:51 -07:00
Nikolaj Bjorner 421fe94607 rmove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-22 17:59:07 -07:00