mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-29 14:30:07 +00:00
Code Activity
18018 commits 65 branches 52 tags 178 MiB
Commit graph

147 commits

Author SHA1 Message Date
Nikolaj Bjorner
c24d445886 fix #6355 
conversion from AIG to expressions should always use the optimized conversion function.

the aig-tactic should throttle regarding output bloat from AIG.
If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place.
 2022-09-22 17:05:32 -05:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Nikolaj Bjorner
97af3a6120 fix #6021 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 11:25:24 -07:00
Nikolaj Bjorner
cca49154ff fix #6021 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 11:24:56 -07:00
Nikolaj Bjorner
08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner
9f2b18cac5 add tactic name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:37:57 -08:00
Nikolaj Bjorner
94cc4ead72 remove arith_lhs simplification from preamble tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 10:55:38 -07:00
Nikolaj Bjorner
dc6a8fde34 fix #5340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-15 13:53:22 -05:00
Nikolaj Bjorner
0ce1c34d81 fix #5065 - regression solving str.from_int equations now that it isn't injective any longer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-02 12:59:48 -08:00
Nikolaj Bjorner
4991c6c2c6 fix #5002 
Avoid code path that uses qe_tactic as it isn't protected against parameter abuse
 2021-02-12 13:20:51 -08:00
Nikolaj Bjorner
2d52367368 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-15 16:45:11 -07:00
Nikolaj Bjorner
2328a6e839 add a way to use new smt core for selected logics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-14 10:43:52 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Lev Nachmanson
8c92cf1b32 restore the tactics with nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
e32a6714a5 call nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Nikolaj Bjorner
2d01c64d2c fix #3682 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 12:30:25 -07:00
Nikolaj Bjorner
8b720a0d66 fix #3115 fix #3116 regressions from #3111 etc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-02 16:38:33 -08:00
Nikolaj Bjorner
238ff78374 fix #3082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-24 09:01:31 -08:00
Lev Nachmanson
7eb1affc7b after rebasing with Z3Prover 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
2b11ed241e fix lemma generation for intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
578e24d8c1 bound the size of bit vectors 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
ab1b2ae86d remove dead code and a fix in no_lemmas_hold 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
086e25b7fa lemmas with less equivalence explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9c62b431e4 address the NB's comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9302d8bef3 Guard the creation of solvers in qfnia_tactic.cpp by a define 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1230b46008 perf in equiv_monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
e4cbe980e9 limit the number of tactics in qfnia 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
05da2508bf fix #2873 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 11:08:44 -06:00
Nikolaj Bjorner
55f59364a3 cap memory consumption on int2bv tactic to 100MB 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 14:25:31 -08:00
Nikolaj Bjorner
216affd852 set defrag 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-31 11:55:44 -08:00
Nikolaj Bjorner
84025d5c11 add rewrites for moduli as exercised in example from #2319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-24 19:02:28 -08:00
Nikolaj Bjorner
63840806d8 fix #2546, retrieve model in optsmt lex before iterating 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 11:19:59 +02:00
Nikolaj Bjorner
000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Nikolaj Bjorner
5de35d46eb fix #2390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 08:55:00 +01:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Lev Nachmanson
14ff768a63 limit the size of bit vectors 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-06-11 16:40:54 -07:00
Nikolaj Bjorner
483a973b37 add pre-processing to default tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 20:20:59 +03:00
Nikolaj Bjorner
3e53b6f2db na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-16 19:21:00 +03:00
Nikolaj Bjorner
f79dccccfe fix #2238 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-08 10:15:57 +02:00
Nikolaj Bjorner
cc216f8cc3 fix regressions breaking build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 21:24:44 +01:00
Nikolaj Bjorner
caa15ea04d enable cardinality constraints in nla2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 18:17:07 +01:00
Nikolaj Bjorner
0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Bruce Mitchener
b83d6d77c9 Use nullptr rather than 0/NULL. 2018-11-28 14:57:01 +07:00
Nikolaj Bjorner
0c1408b30e fixing #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-21 13:48:48 -08:00
Nikolaj Bjorner
cf4bf7b591 more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-02 18:44:53 -05:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
d00ffdda82 strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-15 22:35:47 -07:00
Nikolaj Bjorner
fc4627a24f force the new arithmetic solver for QF_LIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 16:33:48 -07:00
Nuno Lopes
d2b77b1170 remove dead code 2018-07-07 19:07:13 +01:00
Nikolaj Bjorner
5a2a8d7d5c
Merge pull request #1715 from levnach/master 
merge lar_solver/int_solver
 2018-07-01 12:20:02 -07:00