mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-04 00:58:07 +00:00
Code Activity
16698 commits 66 branches 52 tags 179 MiB
Commit graph

145 commits

Author SHA1 Message Date
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
Nuno Lopes
5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Lev Nachmanson
9ba4026bc6 avoid going creating hnf_cuts if all involved vars have integral values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

add explanations to hnf cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

nits and virtual methods (#68)

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

cleanup from std::cout

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

handle the case when the number of terms is greater than the number of variables in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

method name's fix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

restore hnf_cutter to work with m_row_count <= m_column_count

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

tune addition of rational numbers (#70)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

give shorter explanations, call hnf only when have a not integral var

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

overhaul of mpq (#71)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix for 32 bit build (#72)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

yes (#74)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix the merge

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixes in maximize_term untested

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix compilation (#75)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* relax check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* change for gcc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 12:16:58 -07:00