mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 05:30:51 +00:00
Code Activity
16288 commits 46 branches 51 tags 172 MiB
Commit graph

140 commits

Author SHA1 Message Date
Nikolaj Bjorner
dfa65443e9 fix name for artifact 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-19 13:51:58 -07:00
Nikolaj Bjorner
964e513353 re-add bv_eq_axioms, fix #5842 2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
6202cd5394 fix #5842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 17:38:19 +02:00
Nikolaj Bjorner
56d3718cde add simplification with qe-lite as an option #5767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-12 03:41:21 -08:00
Nikolaj Bjorner
cdcfbeb6d8 #5532 
remove "reflect" parameter from exposed options. It should be internal only.
 2021-09-03 16:01:59 -07:00
Nikolaj Bjorner
845ba7a11e use a large delay for nlsat 2021-03-14 19:14:44 -07:00
Nikolaj Bjorner
155738088f fix internalization on post-visit, increase delay to 100 2021-03-14 17:20:39 -07:00
Nikolaj Bjorner
8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner
dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner
f519c58ace Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 
Usage:
z3 4924.smt2 smt.candidate_models=true
 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner
a164087384 remove cheap-eqs option as there is already propagate_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 11:04:04 -08:00
Lev Nachmanson
7089610bbd set arith.cheap_eqsTO True 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-07 12:02:57 -08:00
Lev Nachmanson
b90143cc0e set the defalt for cheap_eqs=False, do not run 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-06 18:26:26 -08:00
Nikolaj Bjorner
1269776777 remove experimental option. Fix #4806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 11:46:19 -08:00
Nikolaj Bjorner
07680408a6 add flag to control whether ite-lifting under quantifiers is conservative or full for #4746, use smt.q.lift_ite=2 to obtain legacy behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-27 16:27:24 -07:00
Nikolaj Bjorner
7c2bdfe3fb
delay internalization, relevancy (#4707) 
* delay evaluation

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

* Update bv_solver.cpp

* delay internalize

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

* compiler warnings

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

* remove gc

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

* add bv delay option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-23 17:12:01 -07:00
Nikolaj Bjorner
ca3ec22b7a handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-16 23:29:24 -07:00
Nikolaj Bjorner
be3c3dacb3 add bound refinement propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-12 10:10:31 -07:00
Nikolaj Bjorner
ac64a370d7 change default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-30 15:55:41 -07:00
Nikolaj Bjorner
6cfbda0f08 remove automata references 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-30 15:26:32 -07:00
Lev Nachmanson
b996bc1f02 remove cheap equalities with the table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
7a2aa28644 make the tree option in cheap_eqs the default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-20 11:31:22 -07:00
Lev Nachmanson
09516d74f6 change the default for cheap eqs to table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-15 13:30:45 -07:00
Nikolaj Bjorner
395a304262 add optional feature to bound search within ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-14 21:34:54 -07:00
Lev Nachmanson
23c12b75af remove a duplicate option gb==grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-13 10:03:19 -07:00
Lev Nachmanson
dd30b5e3af some simplifications in cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
110ab5e6ef debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Lev Nachmanson
c58bd3105b adding more aggressive patching in nl 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
9336e823ed make propagating on bounds on monomials and calling nra the default options 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-26 12:44:47 -07:00
Nikolaj Bjorner
24df35a83e guard derivative code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-23 16:02:10 -07:00
Nikolaj Bjorner
eb3f20832e initial pass at using derivatives in regex unfolding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-23 11:53:07 -07:00
Lev Nachmanson
bfd2407e0f
Debug (#4415) 
* fix it explanation.h

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

* fix explanation.h

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

* add options to run bound propagation on monomials etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-21 09:55:01 -07:00
Lev Nachmanson
82fd2a062d make calling nra from nla optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:16:40 -07:00
Nikolaj Bjorner
fdc87f286f
na (#4254) 
* remove level of indirection for context and ast_manager in smt_theory

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

* add request by #4252

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

* move to def

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

* int

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

* fix #4251

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

* fix #4255

* fix #4257

* add code to debug #4246

* restore new solver as default

* na

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

* fix #4246

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-09 17:40:02 -07:00
Nikolaj Bjorner
cceae2e3f0 old solver as default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-07 17:27:22 -07:00
Murphy Berzish
1f15033ca2
z3str3: remove legacy code (#4215) 
* z3str3: remove legacy fixed-length overlap testing

parameter smt.str.fixed_length_overlap_models has been deprecated

* z3str3: remove legacy length/value testing algorithm and binary search heuristic

the following parameters are deprecated:
smt.str.use_binary_search
smt.str.binary_search_start
smt.str.fixed_length_models (the fixed-length model construction is now always used)

* z3str3: remove legacy regex unroll methods

* z3str3: remove unused methods and member variables
 2020-05-06 13:07:04 -07:00
Lev Nachmanson
f2449df06e introduce ul_pair associated_with_row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-05 15:59:09 -07:00
Nikolaj Bjorner
2104624dfa updated release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-05 10:33:25 -07:00
Nikolaj Bjorner
799b6131f2 avoid repeated internalization of lambda #4169 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-30 13:24:26 -07:00
Lev Nachmanson
530f77281c fixes in branching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-26 16:13:47 -07:00
Nikolaj Bjorner
fe7146d93b fix #3913 - change assumption tracking to be granular based on disabled guards 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-13 19:06:12 -07:00
Nikolaj Bjorner
97af74d8cb fix #3917 remove non-native mode for recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 14:19:26 -07:00
Lev Nachmanson
6d12540ceb set arith.solver=6 by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-06 17:38:17 -07:00
Lev Nachmanson
4792ee8110 revert the default arith.solver=2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-06 17:31:56 -07:00
Lev Nachmanson
80994f74bf redirect to the new solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-06 17:31:56 -07:00
Lev Nachmanson
907d310600 get rid of arith.nla parameter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 14:33:40 -07:00
Lev Nachmanson
f9151a7a8e correct the default options: smt.arith.nla=False 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 13:55:23 -07:00
Lev Nachmanson
b34f841421 setting the old defaul options for nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
ab92c20106 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
762f265616 merge with master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00