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

18334 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
886d3f4351 indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-22 16:55:34 -07:00
Nikolaj Bjorner
eac54ba084 indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-22 16:54:12 -07:00
Nikolaj Bjorner
940775d12d indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-22 16:48:40 -07:00
Lev Nachmanson
caa929f01f do not use lemmase in monomial propagation 2023-09-22 14:27:26 -07:00
Nikolaj Bjorner
5d8779b05d
Merge branch 'master' into unit_prop_on_monomials 2023-09-22 09:46:41 -07:00
Nikolaj Bjorner
eff3f5f65e port bug fixes from unit prop branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-22 09:45:58 -07:00
Lev Nachmanson
576309a16f Revert "reject rows with columns with big numbers for lp bound propagation" 
This reverts commit c0b55d1435.
 2023-09-21 16:30:43 -07:00
Lev Nachmanson
c0b55d1435 reject rows with columns with big numbers for lp bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-21 15:53:53 -07:00
Lev Nachmanson
f423642e9b try the lemma scheme 2023-09-21 12:18:21 -07:00
Lev Nachmanson
e31cecf5db transfer propagate monomial bounds to nla_solver 2023-09-21 11:27:53 -07:00
Lev Nachmanson
536930b4a1 make m_ibounds inside of lp_bound_propagator 
a reference
 2023-09-20 17:13:25 -07:00
Lev Nachmanson
20c02f4f45 fix a lambda bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-20 17:02:35 -07:00
Nikolaj Bjorner
f9de65a464 indetation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-20 15:22:28 -07:00
Nikolaj Bjorner
615aad7779 get rid of int*, use lambda scoping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-20 15:18:37 -07:00
Nikolaj Bjorner
7a74b099ba remove experimental code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-20 15:04:24 -07:00
Lev Nachmanson
24512d5ec2 typo 2023-09-20 14:12:36 -07:00
Lev Nachmanson
9648793206 add features to std_allocator 2023-09-20 14:11:38 -07:00
Lev Nachmanson
f2a0ddb385 Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials 2023-09-19 15:47:01 -07:00
Lev Nachmanson
d77c91b1aa trying to get else on a new line 
with clang-formatter
 2023-09-19 15:46:59 -07:00
Nikolaj Bjorner
f07553ed3a formatting updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 15:18:38 -07:00
Nikolaj Bjorner
db84d21e3b
Merge branch 'master' into unit_prop_on_monomials 2023-09-19 14:44:01 -07:00
Nikolaj Bjorner
fba5de3a25 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 14:43:02 -07:00
Nikolaj Bjorner
4d742001ab formatting of else 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 14:36:21 -07:00