mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 18:06:40 +00:00
Code Activity
16093 commits 43 branches 51 tags 169 MiB
Commit graph

54 commits

Author SHA1 Message Date
Nikolaj Bjorner
0720998bac #5753 2022-01-12 13:12:10 -08:00
Nikolaj Bjorner
cf08cdff9c #5747 2022-01-03 08:54:54 -08:00
Nikolaj Bjorner
a71aa113e0 #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:36:17 -08:00
Nikolaj Bjorner
e8833f4dac working on relevancy=3 2021-12-30 17:07:14 -08:00
Nikolaj Bjorner
fdc253afdd
update arithmetic contract for unbounded (#5696) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-06 08:19:18 -08:00
Nikolaj Bjorner
c826b64e35 prepare release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:41:51 -08:00
Nikolaj Bjorner
87d4ce2659 working on #5614 
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
 2021-11-02 14:55:39 -07:00
Nikolaj Bjorner
a94e2e62af build warnings 2021-11-02 14:55:38 -07:00
Nikolaj Bjorner
72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
Nikolaj Bjorner
3021da87cf #5532 2021-09-04 21:10:26 -07: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
8faad26c3c #5454 2021-08-11 09:46:35 -07:00
Nikolaj Bjorner
08b4c4ea14 #5336 2021-06-08 19:48:05 -07:00
Nikolaj Bjorner
fb6cd8e132 #5324 2021-06-08 15:15:02 -07:00
Nikolaj Bjorner
c194441824 #5324 2021-06-04 10:18:24 -07:00
Nikolaj Bjorner
7c86134e85 #5324 2021-06-03 18:36:44 -07:00
Nikolaj Bjorner
7e330c15e7 #5223 2021-05-05 16:57:06 -07:00
Nikolaj Bjorner
0810720267 #5223 2021-05-02 10:30:35 -07:00
Nikolaj Bjorner
7835388361 #5223 2021-05-01 15:31:05 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
974ef3c147 port equality propagation changes to new core 2021-03-28 16:15:04 -07:00
Nikolaj Bjorner
156139622c delay (lazy) process equalities. 2021-03-17 15:34:04 -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
9a975a4523 array solver fixes 2021-03-13 06:19:32 -08:00
Nikolaj Bjorner
857557ad93 deal with compiler warnings 2021-03-08 20:39:19 -08:00
Nikolaj Bjorner
38737db802 fixes and more porting seq_eq_solver to self-contained module 2021-03-04 16:23:22 -08:00
Nikolaj Bjorner
b02cba6106 rename propagation to explain 2021-02-27 17:25:11 -08:00
Nikolaj Bjorner
830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner
3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
95d98ea8ce throttle equality propagation to shared expressions 2021-01-19 04:51:00 -08:00
Nikolaj Bjorner
523578e3f6 working on new solver core 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner
374ae52d70 testing mbi 2020-12-26 13:49:59 -08:00
Nikolaj Bjorner
372e5ca569 fixes in new solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-25 11:19:31 -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
Nikolaj Bjorner
11477f1ed1 fixes in new solver 
fix logging and lemma signs in arith_solver, move logging of drat equalities to euf
 2020-12-16 10:40:17 -08:00
Nikolaj Bjorner
4d55f83654 misc 2020-12-04 16:59:13 -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
89ffb45c4f fixes to bv/dual-solver, 2020-11-08 17:18:18 -08:00
Nikolaj Bjorner
752f08c9d6 check_feasible is called after column is added for fixed variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 17:18:17 -08:00
Nikolaj Bjorner
2ead7c77ee use value function in lar_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-08 17:18:16 -08:00
Nikolaj Bjorner
d0d06c288a rename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-03 12:13:23 -08:00
Nikolaj Bjorner
620204bbb4
use value function in lar_solver (#4771) 
* use value function in lar_solver

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

* add missing return

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

* check_feasible is called after column is added for fixed variable

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

* na
 2020-11-03 01:08:24 -08:00
Nikolaj Bjorner
5335097768 use get_value/get_ivalue API instead of self-rolled from arith_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 19:38:13 -08:00
Nikolaj Bjorner
ab199dedf9 debug arith/mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 12:13:19 -08:00
Nikolaj Bjorner
d64bc795f0 wrong assert, compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 10:10:59 -07:00
Nikolaj Bjorner
8d76470a8a fixes to mostly solver arith/euf and backtracking scopes 2020-10-26 11:06:41 -07:00
Nikolaj Bjorner
1ee2ba2a9b mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-26 11:06:40 -07:00
Nikolaj Bjorner
72d407a49f
mbp (#4741) 
* adding dt-solver

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

* dt

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

* move mbp to self-contained module

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

* files

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

* Create CMakeLists.txt

* dt

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

* rename to bool_var2expr to indicate type class

* mbp

* na

* add projection

* na

* na

* na

* na

* na

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

* deps

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

* testing arith/q

* na

* newline for model printing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-21 15:48:40 -07:00